book集

section Stern の数列
txt \({\rm fusc}\) は次の漸化式を満たす関数として仮定します（存在は示しません）。\(0, 1, 1, 2, 1, 3, 2, 3, 1, 4, \ldots\) と続く数列です。
word fusc
prop fusc𝕄 <- `\\{ And fusc (0) = 0 \\ fusc (1) = 1 \\ n ∈ 𝕄 ⟹ fusc (2 ⋅ n) = fusc (n) \\ n ∈ 𝕄 ⟹ fusc (2 ⋅ n + 1) = fusc (n) + fusc (n suc) \\}`
let/thm Lfusc <- `n ∈ 𝕄 ⟹ fusc (n) ∈ 𝕄 and (n {/}= 0 ⟹ fusc (n) {/}= 0)` ◀ W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 , *𝕄 , fusc𝕄
prf Lord <- `k ∈ 𝕄 ⟹ k < 2 ⋅ k + 1 and (k {/}= 0 ⟹ k < 2 ⋅ k and k suc < 2 ⋅ k + 1)` / <. / ≤. -| L2⋅ , Lpred , Lsuc+ , L0+ , +1 , +𝕄 , +∈𝕄 , 𝕄0s , 1. , 2. p;
    E0 <- `fusc (2 ⋅ 0) = 0 and 2 ⋅ 0 = 0` -| fusc𝕄 , *𝕄 , `2 ∈ 𝕄` p;
    E1 <- `k ∈ 𝕄 and fusc (k) ∈ 𝕄 and fusc (k) {/}= 0 ⟹ fusc (2 ⋅ k) ∈ 𝕄 and fusc (2 ⋅ k) {/}= 0` -| fusc𝕄 p;
    O0 <- `fusc (2 ⋅ 0 + 1) ∈ 𝕄 and fusc (2 ⋅ 0 + 1) {/}= 0` -| fusc𝕄 , *𝕄 , L0+ , `2 ∈ 𝕄` , suc𝕄 , 𝕄0s , 1. p;
    O1 <- `k ∈ 𝕄 and fusc (k) ∈ 𝕄 and fusc (k suc) ∈ 𝕄 and fusc (k suc) {/}= 0 ⟹ fusc (2 ⋅ k + 1) ∈ 𝕄 and fusc (2 ⋅ k + 1) {/}= 0` -| fusc𝕄 , L+=0 , +∈𝕄 p;
    Le <- `[ n ; k col ∈ 𝕄 ] and n = 2 ⋅ k and [ ∀ z ∈ 𝕄 . (z < n ⟹ fusc (z) ∈ 𝕄 and (z {/}= 0 ⟹ fusc (z) {/}= 0)) ] ⟹ fusc (n) ∈ 𝕄 and (n {/}= 0 ⟹ fusc (n) {/}= 0)` -| Lord , E0 , E1 , 𝕄0s v;
    Lo <- `[ n ; k col ∈ 𝕄 ] and n = 2 ⋅ k + 1 and [ ∀ z ∈ 𝕄 . (z < n ⟹ fusc (z) ∈ 𝕄 and (z {/}= 0 ⟹ fusc (z) {/}= 0)) ] ⟹ fusc (n) ∈ 𝕄 and (n {/}= 0 ⟹ fusc (n) {/}= 0)` -| Lord , O0 , O1 , suc𝕄 , 𝕄0s v;
    Ls <- `n ∈ 𝕄 and [ ∀ z ∈ 𝕄 . (z < n ⟹ fusc (z) ∈ 𝕄 and (z {/}= 0 ⟹ fusc (z) {/}= 0)) ] ⟹ fusc (n) ∈ 𝕄 and (n {/}= 0 ⟹ fusc (n) {/}= 0)` -| Lpar , Le , Lo v;
    Lfusc -| SIND𝕄[D_:=`\{ cls n | fusc (n) ∈ 𝕄 and (n {/}= 0 ⟹ fusc (n) {/}= 0) \}`] , Ls v;
    Lfusc -| W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 , *𝕄 , fusc𝕄 h;
br
txt Calkin–Wilf：どの \(a, b\)（\(b \neq 0\)）も、ある \(n\) と \(g\) で \(a = g\,{\rm fusc}(n)\)、\(b = g\,{\rm fusc}(n+1)\) と書ける。
txt \(a+b\) についての強い帰納法：\(a = 0\) なら \(n = 0\)。\(b \le a\) なら \((a-b, b)\) から \(2n+1\) へ、\(a < b\) なら \((a, b-a)\) から \(2n\) へ（互除法を逆にたどる）。
let/thm LCW <- `[ a ; b col ∈ 𝕄 ] and b {/}= 0 ⟹ [ ∃ n ∈ 𝕄 . [ ∃ g ∈ 𝕄 . a = g ⋅ fusc (n) and b = g ⋅ fusc (n suc) ] ]` ◀ W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 , *𝕄 , fusc𝕄
prf L2s <- `n ∈ 𝕄 ⟹ (2 ⋅ n + 1) suc = 2 ⋅ n suc` -| *𝕄 , +1 , +A , +𝕄 , ⋅∈𝕄 , `2 ∈ 𝕄` , 𝕄0s , 1. , 2. v;
    F2 <- `n ∈ 𝕄 ⟹ fusc (2 ⋅ n) = fusc (n) and fusc ((2 ⋅ n) suc) = fusc (n) + fusc (n suc)` -| fusc𝕄 , +1 , ⋅∈𝕄 , `2 ∈ 𝕄` p;
    F3 <- `n ∈ 𝕄 ⟹ fusc (2 ⋅ n + 1) = fusc (n) + fusc (n suc) and fusc ((2 ⋅ n + 1) suc) = fusc (n suc)` -| fusc𝕄 , L2s , 𝕄0s p;
    Lg <- `[ g ; x ; y col ∈ 𝕄 ] ⟹ g ⋅ y + g ⋅ x = g ⋅ (x + y)` -| Ldist , +C , ⋅∈𝕄 p;
    C0 <- `b ∈ 𝕄 ⟹ [ ∃ n ∈ 𝕄 . [ ∃ g ∈ 𝕄 . 0 = g ⋅ fusc (n) and b = g ⋅ fusc (n suc) ] ]` -| fusc𝕄 , *𝕄 , L⋅1 , 𝕄0s , 1. v;
    CL <- `[ a ; c col ∈ 𝕄 ] and [ ∃ n ∈ 𝕄 . [ ∃ g ∈ 𝕄 . a = g ⋅ fusc (n) and c = g ⋅ fusc (n suc) ] ] ⟹ [ ∃ n ∈ 𝕄 . [ ∃ g ∈ 𝕄 . a = g ⋅ fusc (n) and c + a = g ⋅ fusc (n suc) ] ]` -| F2 , Lg , Lfusc , ⋅∈𝕄 , `2 ∈ 𝕄` , 𝕄0s v;
    CR <- `[ c ; b col ∈ 𝕄 ] and [ ∃ n ∈ 𝕄 . [ ∃ g ∈ 𝕄 . c = g ⋅ fusc (n) and b = g ⋅ fusc (n suc) ] ] ⟹ [ ∃ n ∈ 𝕄 . [ ∃ g ∈ 𝕄 . c + b = g ⋅ fusc (n) and b = g ⋅ fusc (n suc) ] ]` -| F3 , Ldist , Lfusc , ⋅∈𝕄 , +∈𝕄 , `2 ∈ 𝕄` , 𝕄0s , 1. v;
    hyA <- `[ |a ; |b col ∈ 𝕄 ]` ;
    hyB <- `|b {/}= 0` ;
    hyI <- `[ ∀ x ∈ 𝕄 . [ ∀ y ∈ 𝕄 . (x + y < |a + |b and y {/}= 0 ⟹ [ ∃ n ∈ 𝕄 . [ ∃ g ∈ 𝕄 . x = g ⋅ fusc (n) and y = g ⋅ fusc (n suc) ] ]) ] ]` ;
    SB <- `|b ≤ |a ⟹ [ ∃ n ∈ 𝕄 . [ ∃ g ∈ 𝕄 . |a = g ⋅ fusc (n) and |b = g ⋅ fusc (n suc) ] ]` / ≤. -| CR , L<+ , +C , hyI , hyA , hyB , ℕ.' v;
    SC <- `|a < |b ⟹ [ ∃ n ∈ 𝕄 . [ ∃ g ∈ 𝕄 . |a = g ⋅ fusc (n) and |b = g ⋅ fusc (n suc) ] ]` -| C0 , L<d , CL , L<+ , +C , hyI , hyA , ℕ.' v;
    LQ <- `[ ∃ n ∈ 𝕄 . [ ∃ g ∈ 𝕄 . |a = g ⋅ fusc (n) and |b = g ⋅ fusc (n suc) ] ]` -| SB , SC , Ltot , hyA p;
    Lf <- `[ a ; b col ∈ 𝕄 ] and b {/}= 0 and [ ∀ x ∈ 𝕄 . [ ∀ y ∈ 𝕄 . (x + y < a + b and y {/}= 0 ⟹ [ ∃ n ∈ 𝕄 . [ ∃ g ∈ 𝕄 . x = g ⋅ fusc (n) and y = g ⋅ fusc (n suc) ] ]) ] ] ⟹ [ ∃ n ∈ 𝕄 . [ ∃ g ∈ 𝕄 . a = g ⋅ fusc (n) and b = g ⋅ fusc (n suc) ] ]` -| W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 , *𝕄 , fusc𝕄 h[fix];
    LCW -| SIND𝕄[D_:=`\{ cls s | [ ∀ a ∈ 𝕄 . [ ∀ b ∈ 𝕄 . (a + b = s and b {/}= 0 ⟹ [ ∃ n ∈ 𝕄 . [ ∃ g ∈ 𝕄 . a = g ⋅ fusc (n) and b = g ⋅ fusc (n suc) ] ]) ] ] \}`] , Lf , +∈𝕄 v;
    LCW -| W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 , *𝕄 , fusc𝕄 h;

section 有理数
subsection 順序対・写像
word \pr
abbr pr
word ◁ ▷
prop ◁.
prop ▷.
prop/thm pr:0 ◀ W.
prf pr:0 -| ◁. , ▷. p; pr:0 -| W. h;
word ^^pr
prop ^^pr. <- `X ^^pr Y =_ \{ \< pr x ; y \> Cls x ; y | x ∈ X and y ∈ Y \}`
txt \(X \to Y\) は \(X\) から \(Y\) への写像全体の集合、\(X \overset{S}{\to} Y\) は全射全体の集合。
word → →S
prop →. <- `X → Y =_ \{ cls f ⊂ X ^^pr Y | [ ∀ x ∈ X . [ ∃！ y \, \< pr x ; y \> ∈ f ] ] \}`
prop →S. <- `X →S Y =_ \{ cls f ∈ X → Y | [ ∀ y ∈ Y . [ ∃ x \, \< pr x ; y \> ∈ f ] ] \}`

subsection 整数と有理数
txt 整数は自然数 \(n\) と \(-n\)、有理数は分数 \(a \div b\)（\(a\) は整数、\(b\) は 0 でない自然数）。
txt \(-\) と \(\div\) については約分（÷K）だけを仮定します。
word -
word ÷
word ℤ ℚ
prop ℤ. <- `ℤ =_ \{ cls a | a ∈ 𝕄 or [ ∃ n ∈ 𝕄 . a = - n ] \}`
prop ℚ. <- `ℚ =_ \{ a ÷ b Cls a ; b | a ∈ ℤ and b ∈ 𝕄 and b {/}= 0 \}`

prop ÷K <- `\\{ And [ c ; a ; b col ∈ 𝕄 ] and c {/}= 0 ⟹ (c ⋅ a) ÷ (c ⋅ b) = a ÷ b \\ [ c ; a ; b col ∈ 𝕄 ] and c {/}= 0 ⟹ (- (c ⋅ a)) ÷ (c ⋅ b) = (- a) ÷ b \\}`

section 主定理
txt 偶数 \(2n\) に \({\rm fusc}(n) \div {\rm fusc}(n+1)\)、奇数 \(2n+1\) に \(-{\rm fusc}(n) \div {\rm fusc}(n+1)\) を対応させる（Calkin–Wilf の数え上げに符号を付けたもの）。
txt 有理数 \(\pm a \div b\) は、LCW で \(a = g\,{\rm fusc}(n)\)、\(b = g\,{\rm fusc}(n+1)\) と書いて約分すれば値に現れるので、この対応は全射。
thm `[ ∃ f \, f ∈ 𝕄 →S ℚ ]` ◀ W. , ax_s , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 , *𝕄 , fusc𝕄 , ÷K
prf f_ := `\{ \< pr k ; q \> Cls k ; q | [ ∃ n ∈ 𝕄 . (k = 2 ⋅ n and q = fusc (n) ÷ fusc (n suc)) or (k = 2 ⋅ n + 1 and q = (- fusc (n)) ÷ fusc (n suc)) ] \}` ;
    hyF <- `|f =_ f_` ;
    Lsub <- `f_ ⊂_ 𝕄 ^^pr ℚ` //// W.!=. -| Lfusc , ⋅∈𝕄 , +∈𝕄 , suc𝕄 , `2 ∈ 𝕄` , 𝕄0s , 1. v;
    Lmem <- `\< pr k ; q \> ∈ |f ⟹ [ ∃ n ∈ 𝕄 . (k = 2 ⋅ n and q = fusc (n) ÷ fusc (n suc)) or (k = 2 ⋅ n + 1 and q = (- fusc (n)) ÷ fusc (n suc)) ]` -| hyF , pr:0 v;
    LV <- `[ n ; m col ∈ 𝕄 ] and ((k = 2 ⋅ n and q = fusc (n) ÷ fusc (n suc)) or (k = 2 ⋅ n + 1 and q = (- fusc (n)) ÷ fusc (n suc))) and ((k = 2 ⋅ m and r = fusc (m) ÷ fusc (m suc)) or (k = 2 ⋅ m + 1 and r = (- fusc (m)) ÷ fusc (m suc))) ⟹ q = r` -| L2K , L1K , Lne v;
    Luni <- `\< pr k ; q \> ∈ |f and \< pr k ; r \> ∈ |f ⟹ q = r` -| Lmem , LV v;
    Lfto <- `k ∈ 𝕄 ⟹ [ ∃ q \, \< pr k ; q \> ∈ |f ]` -| hyF , Lpar v;
    Lg0 <- `[ g ; y col ∈ 𝕄 ] and g ⋅ y {/}= 0 ⟹ g {/}= 0` -| L0⋅ p;
    S+ <- `[ a ; b col ∈ 𝕄 ] and b {/}= 0 ⟹ [ ∃ k \, \< pr k ; a ÷ b \> ∈ |f ]` -| hyF , LCW , ÷K , Lg0 , Lfusc , ⋅∈𝕄 , `2 ∈ 𝕄` , 𝕄0s v;
    S- <- `[ a ; b col ∈ 𝕄 ] and b {/}= 0 ⟹ [ ∃ k \, \< pr k ; (- a) ÷ b \> ∈ |f ]` -| hyF , LCW , ÷K , Lg0 , Lfusc , ⋅∈𝕄 , `2 ∈ 𝕄` , 𝕄0s v;
    Lsur <- `q ∈ ℚ ⟹ [ ∃ k \, \< pr k ; q \> ∈ |f ]` / ℚ. // W.!=. -| S+ , S- v;
    Lfsub <- `|f ⊂_ 𝕄 ^^pr ℚ` -| hyF , Lsub v;
    LfS <- `|f ∈ 𝕄 →S ℚ` /// W.!=.!ℚ. -| Lfsub , Lfto , Luni , Lsur v;
    goal -| LfS p;
    goal -| W. , ax_s , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 , *𝕄 , fusc𝕄 , ÷K h[fix];

articles3/3b.book

`articles3/3b.book`