分割の母関数

方針：番号の大きい因子 $1+G_k$ は、$N$ 次以下では $1$ と同じである（ex-gfp-order の 3）。そこで、部分積に因子を 1 つ付け加えても $N$ 次以下の係数が変わらないことを示す。
段 1（番号 $K_N$ の存在）：$N$ を固定する。仮定から $\operatorname{ord}G_k\le N$ となる $k$ は有限個なので、それらの最大値を $K_N$ とする（1 つもなければ $K_N:=0$）。$k>K_N$ なら $\operatorname{ord}G_k>N$ である。
段 2（因子を 1 つ付け加える）：$K\ge K_N$ とする。分配法則から
$$ P_{K+1}=P_K(1+G_{K+1})=P_K+P_KG_{K+1} $$
である。$K+1>K_N$ なので $\operatorname{ord}G_{K+1}>N$、すなわち $G_{K+1}$ の $0$ 次から $N$ 次までの係数はすべて $0$ である。$m\le N$ について $[x^m](P_KG_{K+1})=\sum_{i=0}^m[x^i]P_K\cdot[x^{m-i}]G_{K+1}$ であり、$m-i\le N$ なので各項の $[x^{m-i}]G_{K+1}$ は $0$ である。よって $P_KG_{K+1}\equiv0$、$P_{K+1}\equiv P_K\pmod{x^{N+1}}$ である。
段 3（1 と 2）：段 2 を $K=K_N,K_N+1,\dots$ と繰り返すと、$P_{K_N}\equiv P_{K_N+1}\equiv P_{K_N+2}\equiv\cdots\pmod{x^{N+1}}$ である。$n\le N$ の $x^n$ の係数は $K\ge K_N$ で一定なので 1 が成り立ち、定めた級数はこの一定の値を係数にもつので 2 が成り立つ。
段 4（3）：$N$ を固定すると、2 により、どちらの級数も $N$ 次以下では「$\operatorname{ord}G_k\le N$ となる有限個の因子の積」に、$\operatorname{ord}G_k>N$ となる有限個の因子 $1+G_k$（ex-gfp-order の 3 により $\pmod{x^{N+1}}$ で $1$）を掛けたものと合同である。有限個の積は順番を変えても同じ（交換法則・結合法則）なので、2 つの級数は $N$ 次以下で一致する。$N$ は任意なので、2 つの級数は等しい。$\square$

方針：$x^n$ の係数は有限個の因子の積で計算できることを確かめ、有限個の積を展開して項を数える。
段 1（無限積が定まる）：$0\in M_k$ なので、$k$ 番目の因子は $1+G_k$、$G_k:=\sum_{m\in M_k,\ m\ge1}x^{km}$ の形である。$G_k$ の項の次数は $k$ 以上なので $\operatorname{ord}G_k\ge k$ であり、$\operatorname{ord}G_k\le N$ となるのは $k\le N$ のときだけである。よって lem-gfp-infinite-product の条件を満たし、無限積が定まる。
段 2（有限積に帰着する）：$n$ を固定する。$k>n$ なら $\operatorname{ord}G_k>n$ なので、lem-gfp-infinite-product の 2（$N=n$、$K=n$）により、無限積の $x^n$ の係数は有限積 $\prod_{k=1}^n\sum_{m\in M_k}x^{km}$ の $x^n$ の係数に等しい。
段 3（展開して数える）：この有限積を展開すると、各因子 $k$ から 1 項 $x^{km_k}$（$m_k\in M_k$）を選んで掛けた $x^{1\cdot m_1+2m_2+\cdots+nm_n}$ を、すべての選び方について足したものになる。よって $x^n$ の係数は、$m_1+2m_2+\cdots+nm_n=n$、$m_k\in M_k$ を満たす組 $(m_1,\dots,m_n)$ の個数である。
段 4（分割との対応）：分割は、各部分 $k$ を使う回数 $m_k$ で決まる。$n$ の分割では $n$ より大きい部分は使えないので、組 $(m_1,\dots,m_n)$ で決まり、部分の和の条件は $\sum_kkm_k=n$ である。逆に、この条件を満たす組から「$k$ を $m_k$ 個並べた」分割がただ 1 つ決まる。したがって段 3 の個数は $c_n$ に等しい。$\square$

方針：有限個の因子の積に $1-x$ を掛けると、高校の公式 $(1-y)(1+y)=1-y^2$ が次々に使えて $1-x^{2^J}$ になる。これを $N$ 次以下で比べる。
段 1（有限積）：$J\ge1$ について $(1-x)\prod_{j=0}^{J-1}(1+x^{2^j})=1-x^{2^J}$ を $J$ についての帰納法で示す。$J=1$ では $(1-x)(1+x)=1-x^2$ である。$J$ で成り立てば、両辺に $1+x^{2^J}$ を掛けて $(1-x^{2^J})(1+x^{2^J})=1-x^{2^{J+1}}$ となり、$J+1$ でも成り立つ。
段 2（無限積が定まる）：$j$ 番目の因子は $1+x^{2^j}$ で $\operatorname{ord}x^{2^j}=2^j$ なので、$2^j\le N$ となる $j$ は有限個である。よって lem-gfp-infinite-product により無限積が定まる。
段 3（$N$ 次以下で比べる）：$N$ を固定し、$2^J>N$ となる $J$ をとる。$j\ge J$ なら $\operatorname{ord}x^{2^j}=2^j>N$ なので、lem-gfp-infinite-product の 2 により $\prod_{j\ge0}(1+x^{2^j})\equiv\prod_{j=0}^{J-1}(1+x^{2^j})\pmod{x^{N+1}}$ である。両辺に $1-x$ を掛けて段 1 を使うと、
$$ (1-x)\prod_{j\ge0}(1+x^{2^j})\equiv1-x^{2^J}\equiv1\pmod{x^{N+1}} $$
である（$2^J>N$ なので $x^{2^J}$ は $N$ 次以下に影響しない）。$N$ は任意なので $(1-x)\prod_{j\ge0}(1+x^{2^j})=1$ であり、両辺に $\frac1{1-x}$ を掛けて主張の等式を得る。
段 4（後半）：lem-gfp-count で、$k$ が 2 の冪なら $M_k=\{0,1\}$、それ以外なら $M_k=\{0\}$ とすると、左辺の $x^n$ の係数は「$n$ を相異なる 2 の冪の和で表す方法の数」である。右辺 $\frac1{1-x}=\sum x^n$ の係数はすべて $1$ なので、表し方はどの $n$ でもちょうど 1 通りである。$\square$

方針：表し方を「$1$ を何回使うか」で分け、残りを半分にすると小さい数の表し方になることから、漸化式を作る。
段 1（対応）：$m\ge0$ とし、$n=2m$ または $n=2m+1$ とする。$n$ の表し方で $1$ を使う回数を $c\in\{0,1,2,3\}$ とする。$1$ 以外の部分はすべて偶数なので、$n-c$ は偶数である。よって $n=2m$ なら $c=0$ か $2$、$n=2m+1$ なら $c=1$ か $3$ である。$1$ 以外の部分をそれぞれ半分にすると、$\frac{n-c}2$ の同じ条件の表し方になる（冪 $2^j$ は $2^{j-1}$ になり、使う回数は変わらない）。逆に $\frac{n-c}2$ の表し方の各部分を 2 倍して $1$ を $c$ 個加えると、元の表し方に戻る。
段 2（漸化式）：段 1 から
$$ f(2m)=f(m)+f(m-1)\quad(c=0,2),\qquad f(2m+1)=f(m)+f(m-1)\quad(c=1,3) $$
である（$m\ge1$。$2m+1$ の式は $m=0$ でも成り立ち、$f(1)=f(0)+f(-1)=1$）。
段 3（帰納法）：$n$ についての強い帰納法で $f(n)=\lfloor\frac n2\rfloor+1$ を示す。$n=0,1$ では $f(0)=1$、$f(1)=1$ で正しい。$n\ge2$ とし、$n=2m$ または $2m+1$（$m\ge1$）と書く。$m,m-1< n$ なので帰納法の仮定が使え、
$$ f(n)=\Bigl(\Bigl\lfloor\frac m2\Bigr\rfloor+1\Bigr)+\Bigl(\Bigl\lfloor\frac{m-1}2\Bigr\rfloor+1\Bigr) $$
である。$m$ が偶数なら $\lfloor\frac m2\rfloor+\lfloor\frac{m-1}2\rfloor=\frac m2+\frac m2-1=m-1$、奇数なら $\frac{m-1}2+\frac{m-1}2=m-1$ なので、$f(n)=(m-1)+2=m+1$ である。$n=2m$ でも $2m+1$ でも $\lfloor\frac n2\rfloor=m$ なので、$f(n)=\lfloor\frac n2\rfloor+1$ である。$\square$