曜日の計算

方針：閏年の集まりを、4 の倍数・100 の倍数・400 の倍数の集まりで表し、個数を引き算と足し算で求める。
段 1（3 つの集まり）。$1$ 以上 $Y$ 以下の整数のうち、4 の倍数の集まりを $A$、100 の倍数の集まりを $B$、400 の倍数の集まりを $C$ とする。ガウス記号と整数の個数 の定理「倍数の個数」により、$A,B,C$ の個数はそれぞれ $\lfloor Y/4\rfloor$、$\lfloor Y/100\rfloor$、$\lfloor Y/400\rfloor$ である。400 の倍数は 100 の倍数であり、100 の倍数は 4 の倍数なので、$C$ は $B$ に含まれ、$B$ は $A$ に含まれる。
段 2（閏年の集まり）。def-dow-calendar の条件 (ii) により、閏年は「$A$ に入り $B$ に入らない年」と「$C$ に入る年」である。前者の集まりを $A\setminus B$ と書く。$C$ は $B$ に含まれるので、$C$ の年は $A\setminus B$ に入らない。したがって 2 つの集まりは重ならず、閏年の個数は「$A\setminus B$ の個数」と「$C$ の個数」の和である。
段 3（個数）。$B$ は $A$ に含まれるので、$A\setminus B$ の個数は $A$ の個数から $B$ の個数を引いたものである。よって
$$ L(Y)=\left(\left\lfloor\frac Y4\right\rfloor-\left\lfloor\frac Y{100}\right\rfloor\right)+\left\lfloor\frac Y{400}\right\rfloor $$
である。$\square$

方針：$P$ から $Q$ までを「$P$ からその年の 3 月 1 日へもどる」「3 月 1 日から 3 月 1 日へ年ごとに進む」「3 月 1 日から $Q$ へ進む」の 3 つに分けて数える。$P$ の値を $Y_1,m_1,d_1$、$Q$ の値を $Y_2,m_2,d_2$ とする。
段 1（年の中の日数）。数え直した $Y$ 年の 3 月 1 日から $m$ 月 $d$ 日までの日数は、$m$ 月 1 日までの $c(m)$ 日と、$m$ 月 1 日から $d$ 日までの $d-1$ 日の和で、$c(m)+d-1$ 日である。
段 2（1 年分の日数）。数え直した $t$ 年の 3 月 1 日から $t+1$ 年の 3 月 1 日までには、3 月から 12 月までと、西暦 $t+1$ 年の 1 月・2 月が入る。2 月が 29 日になるのは西暦 $t+1$ 年が閏年のときだけなので、日数は $t+1$ 年が閏年なら $366$、平年なら $365$ である。一方、$L(t+1)-L(t)$ は「西暦 $t+1$ 年が閏年なら $1$、平年なら $0$」である（$L$ は 1 年から数えた閏年の個数だから）。よって、この 1 年分の日数は
$$ 365+L(t+1)-L(t) $$
である。
段 3（何年分かの日数）。$Y_1\le Y_2$ とする（$Q$ は $P$ より後なので、数え直した年も $Y_1\le Y_2$ である）。$Y_1$ 年の 3 月 1 日から $Y_2$ 年の 3 月 1 日までの日数は、段 2 の日数を $t=Y_1,Y_1+1,\dots,Y_2-1$ について足したもので
$$ \sum_{t=Y_1}^{Y_2-1}\bigl(365+L(t+1)-L(t)\bigr)=365(Y_2-Y_1)+L(Y_2)-L(Y_1) $$
である（$L(t+1)-L(t)$ の和は、隣どうしが打ち消し合って $L(Y_2)-L(Y_1)$ だけが残る）。$Y_1=Y_2$ のときは両辺とも $0$ である。
段 4（合わせる）。$P$ から $Q$ までの日数 $n$ は、「$Y_1$ 年の 3 月 1 日から $Q$ までの日数」から「$Y_1$ 年の 3 月 1 日から $P$ までの日数」を引いたものである。前者は段 3 と段 1 から $365(Y_2-Y_1)+L(Y_2)-L(Y_1)+c(m_2)+d_2-1$、後者は段 1 から $c(m_1)+d_1-1$ である。引き算すると
$$ n=\bigl(365Y_2+L(Y_2)+c(m_2)+d_2\bigr)-\bigl(365Y_1+L(Y_1)+c(m_1)+d_1\bigr) $$
となり、右辺は $Q$ の $G$ から $P$ の $G$ を引いたものである。$\square$

方針：$f(m)=\left\lfloor\dfrac{13(m+1)}5\right\rfloor$ とおき、$m$ が 1 増えるときの $c(m)$ と $f(m)$ の増え方を比べる。
段 1（$f$ の値）。$m=3,4,\dots,14$ について $\dfrac{13(m+1)}5$ とそのガウス記号 $f(m)$ を計算すると、次の表になる。

段 2（増え方の比較）。表の最後の 2 行を比べると、$m=3,4,\dots,13$ のどの $m$ でも
$$ (m\text{ 月の日数})-\bigl(f(m+1)-f(m)\bigr)=28 $$
である（$31-3=28$、$30-2=28$）。$c(m+1)-c(m)$ は $m$ 月の日数なので、
$$ \bigl(c(m+1)-f(m+1)\bigr)-\bigl(c(m)-f(m)\bigr)=28 $$
となる。つまり $c(m)-f(m)$ は、$m$ が 1 増えるごとにちょうど $28$ ずつ増える。
段 3（7 で割った余り）。$m=3$ では $c(3)-f(3)=0-10=-10$ なので、段 2 から
$$ c(m)-f(m)=-10+28(m-3) $$
である（$m=3,4,\dots,14$）。$28$ は $7$ の倍数なので $c(m)-f(m)\equiv-10\equiv-3\pmod7$ であり、$c(m)\equiv f(m)-3\pmod7$ が成り立つ。$\square$

方針：lem-dow-count の $G$ を 7 で割った余りを、$J,K$ と lem-dow-month で書き直し、$h\equiv G+3\pmod7$ を示す。最後に、ある 1 日で曜日の番号と $h$ の余りが一致することを確かめる。
段 1（$365Y$ の余り）。$365=7\cdot52+1$ なので $365\equiv1\pmod7$、$100=7\cdot14+2$ なので $100\equiv2\pmod7$ である。合同式の計算規則 の定理「和・差・積の合同」により
$$ 365Y\equiv Y=100J+K\equiv2J+K\pmod7 $$
である。
段 2（$L(Y)$ を $J,K$ で書く）。prop-dow-leap の 3 つのガウス記号を順に計算する。

• $\dfrac Y4=25J+\dfrac K4$ で、$25J$ は整数なので、$\left\lfloor\dfrac Y4\right\rfloor=25J+\left\lfloor\dfrac K4\right\rfloor$ である（整数 $n$ について $\lfloor x+n\rfloor=\lfloor x\rfloor+n$。ガウス記号と整数の個数 の命題「ガウス記号の基本性質」）。
• $\dfrac Y{100}=J+\dfrac K{100}$ で、$0\le\dfrac K{100}\le\dfrac{99}{100}<1$ なので、$\left\lfloor\dfrac Y{100}\right\rfloor=J$ である。
• $J$ を 4 で割った商を $q$、余りを $s$ とする（$J=4q+s$、$0\le s\le3$）。$\dfrac Y{400}=\dfrac J4+\dfrac K{400}=q+\dfrac s4+\dfrac K{400}$ で、$0\le\dfrac s4+\dfrac K{400}\le\dfrac34+\dfrac{99}{400}<1$ なので、$\left\lfloor\dfrac Y{400}\right\rfloor=q=\left\lfloor\dfrac J4\right\rfloor$ である。
  よって
  $$ L(Y)=25J+\left\lfloor\frac K4\right\rfloor-J+\left\lfloor\frac J4\right\rfloor=24J+\left\lfloor\frac K4\right\rfloor+\left\lfloor\frac J4\right\rfloor $$
  である。
  段 3（$G$ の余り）。段 1・段 2 と lem-dow-month を $G=365Y+L(Y)+c(m)+d$ に代入すると
  $$ G\equiv(2J+K)+\left(24J+\left\lfloor\frac K4\right\rfloor+\left\lfloor\frac J4\right\rfloor\right)+\left(\left\lfloor\frac{13(m+1)}5\right\rfloor-3\right)+d\pmod7 $$
  である。$J$ の係数は $2+24=26$ で、$26=7\cdot3+5$ なので $26J\equiv5J$ である。並べ替えると
  $$ G\equiv d+\left\lfloor\frac{13(m+1)}5\right\rfloor+K+\left\lfloor\frac K4\right\rfloor+\left\lfloor\frac J4\right\rfloor+5J-3=h-3\pmod7 $$
  となり、$h\equiv G+3\pmod7$ が分かった。
  段 4（曜日と一致すること）。lem-dow-count より、日付が 1 日進むと $G$ はちょうど 1 増えるので、段 3 から $h$ を 7 で割った余りも 1 つ進む（$6$ の次は $0$）。曜日の番号も 1 日ごとに 1 つ進む（def-dow-calendar）。したがって、ある 1 日で「$h$ を 7 で割った余り」と「曜日の番号」が一致すれば、その日から前後に何日ずれても一致し続ける。2000 年 1 月 1 日（土曜日、番号 $0$）では、ex-dow-shift の (2) の $Y=1999$、$m=13$、$J=19$、$K=99$ を使って
  $$ h=1+\left\lfloor\frac{13\cdot14}5\right\rfloor+99+\left\lfloor\frac{99}4\right\rfloor+\left\lfloor\frac{19}4\right\rfloor+5\cdot19=1+36+99+24+4+95=259=7\cdot37 $$
  で、余りは $0$ である。よって、すべての日付で $h$ を 7 で割った余りが曜日の番号に等しい。$\square$

段 1（日付があること）。400 は 4 でも 100 でも 400 でも割り切れるので、def-dow-calendar の条件 (ii) により、西暦 $t$ 年と $t+400$ 年は、両方とも閏年か両方とも平年である。だから、ある日付の 400 年後の同じ月・同じ日も存在する（2 月 29 日についても）。
段 2（日数）。数え直した $Y$ 年の 3 月 1 日から $Y+400$ 年の 3 月 1 日までの日数は、lem-dow-count の証明の段 3 から $365\cdot400+L(Y+400)-L(Y)$ である。prop-dow-leap の式で、$\left\lfloor\dfrac{Y+400}4\right\rfloor=\left\lfloor\dfrac Y4\right\rfloor+100$、$\left\lfloor\dfrac{Y+400}{100}\right\rfloor=\left\lfloor\dfrac Y{100}\right\rfloor+4$、$\left\lfloor\dfrac{Y+400}{400}\right\rfloor=\left\lfloor\dfrac Y{400}\right\rfloor+1$ なので（整数を足してもガウス記号の外に出せる）、$L(Y+400)-L(Y)=100-4+1=97$ である。よって日数は
$$ 365\cdot400+97=146000+97=146097=7\cdot20871 $$
である。
段 3（曜日）。ある日付と、その 400 年後の同じ月・同じ日とは、$m$ と $d$ が同じで $Y$ が 400 違う。lem-dow-count より、その間の日数は 2 つの $G$ の差 $365\cdot400+L(Y+400)-L(Y)=146097$ で、7 の倍数である。よって曜日は同じである。$\square$

方針：同じ年の 3 月から 12 月までは $Y,J,K$ が共通なので、13 日の $h$ の違いは $\left\lfloor\frac{13(m+1)}5\right\rfloor$ の違いだけである。
西暦 $y$ 年の $m=3,4,\dots,12$ 月の 13 日では、def-dow-shift により $Y=y$ で、$J,K$ は月によらない。thm-dow-zeller の式は
$$ h=\left\lfloor\frac{13(m+1)}5\right\rfloor+\underbrace{13+K+\left\lfloor\frac K4\right\rfloor+\left\lfloor\frac J4\right\rfloor+5J}_{\text{月によらない数 }s} $$
となる。ex-dow-month の表から、$m=3,\dots,12$ の $\left\lfloor\frac{13(m+1)}5\right\rfloor$ を 7 で割った余りは $3,6,1,4,6,2,5,0,3,5$ で、$0$ から $6$ までのすべてが現れる。これらに同じ数 $s$ を足して 7 で割った余りをとると、異なる余りは異なる余りに移る（$a+s\equiv b+s$ なら $a\equiv b$）ので、やはり $0$ から $6$ までのすべてが現れる。したがって 13 日の曜日として 7 つの曜日がすべて現れ、特に金曜日（番号 $6$）も現れる。$\square$