未ログイン ／
ログイン
← ファイル一覧
（保存にはログインが要ります）
articles3/73.book
ヘッダ
行番号
title Erdős–Szekeres の定理 import 0-pa formel /common/default thmel /common/zf option review quick:true;
section 鳩の巣原理 word ap txt 列（関数）\(f\) の値を \(f(i)\) と書きます。1点の値だけを変えた列があること（upd𝕄）を仮定します（存在は示しません）。 prop upd𝕄 <- `[ ∃ g \, (g ap (k) = p and [ ∀ i ∈ 𝕄 . (i {/}= k ⟹ g ap (i) = f ap (i)) ]) ]` txt 鳩の巣原理：\(N\) 個の \(i \lt N\) を \(M\) 個の値 \(\lt M\) へ相異なるように送れるなら \(N \le M\)。 let/thm PH <- `[ N ; M col ∈ 𝕄 ] and [ ∀ i ∈ 𝕄 . (i < N ⟹ f ap (i) ∈ 𝕄 and f ap (i) < M) ] and [ ∀ i ∈ 𝕄 . [ ∀ j ∈ 𝕄 . (i < N and j < N and f ap (i) = f ap (j) ⟹ i = j) ] ] ⟹ N ≤ M` ◀ W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 , upd𝕄 prf Pb <- `M ∈ 𝕄 ⟹ 0 ≤ M` / ≤. -| +𝕄 p; Pss <- `[ N ; m col ∈ 𝕄 ] and N ≤ m ⟹ N suc ≤ m suc` / ≤. -| +𝕄 p; P0 <- `[ N ; M col ∈ 𝕄 ] and [ ∀ i ∈ 𝕄 . (i < N suc ⟹ f ap (i) ∈ 𝕄 and f ap (i) < M) ] ⟹ [ ∃ m ∈ 𝕄 . M = m suc ]` -| L<s , L<0 , Lpred , 𝕄0s p; Pf <- `[ N ; m col ∈ 𝕄 ] and [ ∀ i ∈ 𝕄 . (i < N suc ⟹ f ap (i) ∈ 𝕄 and f ap (i) < m suc) ] and [ ∀ i ∈ 𝕄 . [ ∀ j ∈ 𝕄 . (i < N suc and j < N suc and f ap (i) = f ap (j) ⟹ i = j) ] ] and [ ∀ k ∈ 𝕄 . (k < N ⟹ f ap (k) {/}= m) ] ⟹ [ ∀ i ∈ 𝕄 . (i < N ⟹ f ap (i) ∈ 𝕄 and f ap (i) < m) ] and [ ∀ i ∈ 𝕄 . [ ∀ j ∈ 𝕄 . (i < N and j < N and f ap (i) = f ap (j) ⟹ i = j) ] ]` -| L<S , L<K p; Pg1 <- `[ N ; m ; k col ∈ 𝕄 ] and k < N and f ap (k) = m and g ap (k) = f ap (N) and [ ∀ i ∈ 𝕄 . (i {/}= k ⟹ g ap (i) = f ap (i)) ] and [ ∀ i ∈ 𝕄 . (i < N suc ⟹ f ap (i) ∈ 𝕄 and f ap (i) < m suc) ] and [ ∀ i ∈ 𝕄 . [ ∀ j ∈ 𝕄 . (i < N suc and j < N suc and f ap (i) = f ap (j) ⟹ i = j) ] ] ⟹ [ ∀ i ∈ 𝕄 . (i < N ⟹ g ap (i) ∈ 𝕄 and g ap (i) < m) ]` -| L<S , L<K , L<s , L<irr , 𝕄0s v; Pg2 <- `[ N ; k col ∈ 𝕄 ] and k < N and g ap (k) = f ap (N) and [ ∀ i ∈ 𝕄 . (i {/}= k ⟹ g ap (i) = f ap (i)) ] and [ ∀ i ∈ 𝕄 . [ ∀ j ∈ 𝕄 . (i < N suc and j < N suc and f ap (i) = f ap (j) ⟹ i = j) ] ] ⟹ [ ∀ i ∈ 𝕄 . [ ∀ j ∈ 𝕄 . (i < N and j < N and g ap (i) = g ap (j) ⟹ i = j) ] ]` -| L<K , L<s , L<irr , 𝕄0s v; LA <- `[ N ; m ; k col ∈ 𝕄 ] and k < N and f ap (k) = m and [ ∀ i ∈ 𝕄 . (i < N suc ⟹ f ap (i) ∈ 𝕄 and f ap (i) < m suc) ] and [ ∀ i ∈ 𝕄 . [ ∀ j ∈ 𝕄 . (i < N suc and j < N suc and f ap (i) = f ap (j) ⟹ i = j) ] ] and g ap (k) = f ap (N) and [ ∀ i ∈ 𝕄 . (i {/}= k ⟹ g ap (i) = f ap (i)) ] and [ ∀ M ∈ 𝕄 . [ ∀ f \, ([ ∀ i ∈ 𝕄 . (i < N ⟹ f ap (i) ∈ 𝕄 and f ap (i) < M) ] and [ ∀ i ∈ 𝕄 . [ ∀ j ∈ 𝕄 . (i < N and j < N and f ap (i) = f ap (j) ⟹ i = j) ] ] ⟹ N ≤ M) ] ] ⟹ N suc ≤ m suc` -| Pg1 , Pg2 , Pss v; LA2 <- `[ N ; m ; k col ∈ 𝕄 ] and k < N and f ap (k) = m and [ ∀ i ∈ 𝕄 . (i < N suc ⟹ f ap (i) ∈ 𝕄 and f ap (i) < m suc) ] and [ ∀ i ∈ 𝕄 . [ ∀ j ∈ 𝕄 . (i < N suc and j < N suc and f ap (i) = f ap (j) ⟹ i = j) ] ] and [ ∀ M ∈ 𝕄 . [ ∀ f \, ([ ∀ i ∈ 𝕄 . (i < N ⟹ f ap (i) ∈ 𝕄 and f ap (i) < M) ] and [ ∀ i ∈ 𝕄 . [ ∀ j ∈ 𝕄 . (i < N and j < N and f ap (i) = f ap (j) ⟹ i = j) ] ] ⟹ N ≤ M) ] ] ⟹ N suc ≤ m suc` -| upd𝕄 , LA v; LB <- `[ N ; m col ∈ 𝕄 ] and [ ∀ M ∈ 𝕄 . [ ∀ f \, ([ ∀ i ∈ 𝕄 . (i < N ⟹ f ap (i) ∈ 𝕄 and f ap (i) < M) ] and [ ∀ i ∈ 𝕄 . [ ∀ j ∈ 𝕄 . (i < N and j < N and f ap (i) = f ap (j) ⟹ i = j) ] ] ⟹ N ≤ M) ] ] and [ ∀ i ∈ 𝕄 . (i < N suc ⟹ f ap (i) ∈ 𝕄 and f ap (i) < m suc) ] and [ ∀ i ∈ 𝕄 . [ ∀ j ∈ 𝕄 . (i < N suc and j < N suc and f ap (i) = f ap (j) ⟹ i = j) ] ] and [ ∀ k ∈ 𝕄 . (k < N ⟹ f ap (k) {/}= m) ] ⟹ N suc ≤ m suc` -| Pf , Pss v; Ps <- `N ∈ 𝕄 and [ ∀ M ∈ 𝕄 . [ ∀ f \, ([ ∀ i ∈ 𝕄 . (i < N ⟹ f ap (i) ∈ 𝕄 and f ap (i) < M) ] and [ ∀ i ∈ 𝕄 . [ ∀ j ∈ 𝕄 . (i < N and j < N and f ap (i) = f ap (j) ⟹ i = j) ] ] ⟹ N ≤ M) ] ] ⟹ [ ∀ M ∈ 𝕄 . [ ∀ f \, ([ ∀ i ∈ 𝕄 . (i < N suc ⟹ f ap (i) ∈ 𝕄 and f ap (i) < M) ] and [ ∀ i ∈ 𝕄 . [ ∀ j ∈ 𝕄 . (i < N suc and j < N suc and f ap (i) = f ap (j) ⟹ i = j) ] ] ⟹ N suc ≤ M) ] ]` -| P0 , LA2 , LB v; PH -| IND𝕄[C_:=`\{ cls N | [ ∀ M ∈ 𝕄 . [ ∀ f \, ([ ∀ i ∈ 𝕄 . (i < N ⟹ f ap (i) ∈ 𝕄 and f ap (i) < M) ] and [ ∀ i ∈ 𝕄 . [ ∀ j ∈ 𝕄 . (i < N and j < N and f ap (i) = f ap (j) ⟹ i = j) ] ] ⟹ N ≤ M) ] ] \}`] , Pb , Ps , 𝕄0s v; PH -| W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 , upd𝕄 h; br txt 順序の補題。 !let/thm L<≤T <- `[ x ; y ; z col ∈ 𝕄 ] and x < y and y ≤ z ⟹ x < z` ◀ W. , 𝕄0s , IND𝕄 , +𝕄 prf L<≤T / <. -| L≤T , 𝕄0s p; L<≤T -| W. , 𝕄0s , IND𝕄 , +𝕄 h; !let/thm L≤<T <- `[ x ; y ; z col ∈ 𝕄 ] and x ≤ y and y < z ⟹ x < z` ◀ W. , 𝕄0s , IND𝕄 , +𝕄 prf L≤<T / <. / ≤. -| +A , Lsuc+ , +𝕄 , +∈𝕄 , 𝕄0s v; L≤<T -| W. , 𝕄0s , IND𝕄 , +𝕄 h; !let/thm L≠< <- `[ x ; y col ∈ 𝕄 ] and x {/}= y ⟹ x < y or y < x` ◀ W. , 𝕄0s , IND𝕄 , +𝕄 prf Lq <- `[ x ; y col ∈ 𝕄 ] and x ≤ y and x {/}= y ⟹ x < y` / <. / ≤. -| Lpred , Lsuc+ , L0+ , +𝕄 , 𝕄0s v; L≠< -| Ltot , Lq p; L≠< -| W. , 𝕄0s , IND𝕄 , +𝕄 h; br txt 2つの数 \(p, q \lt n\) は \(p \cdot n + q \lt n \cdot n\) で1つの数に表せ（L<sq）、表し方は1通り（Lcode）。 !let/thm L≤≠s <- `[ m ; k col ∈ 𝕄 ] and m ≤ k ⟹ m {/}= k suc` ◀ W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 prf L≤≠s -| L<irr / <. , 𝕄0s p; L≤≠s -| W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 h; !let/thm L<≠s <- `[ m ; k col ∈ 𝕄 ] and m < k ⟹ m {/}= k suc and m suc {/}= k suc` ◀ W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 prf L<≠s -| L≤≠s , L<≤ , suc𝕄 , L<irr p; L<≠s -| W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 h; br !let/thm L<sq <- `[ p ; q ; n col ∈ 𝕄 ] and p < n and q < n ⟹ p ⋅ n + q < n ⋅ n` ◀ W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 , *𝕄 prf M1 <- `[ x ; y ; n col ∈ 𝕄 ] and x < y ⟹ x suc ⋅ n ≤ y ⋅ n` / <. / ≤. -| Rdist , ⋅∈𝕄 , 𝕄0s p; M2 <- `[ x ; q ; n col ∈ 𝕄 ] and q < n ⟹ x + q < x + n` / <. / ≤. -| +A , +C , Lsuc+ , +𝕄 , +∈𝕄 v; L<sq -| M1 , M2 , L<≤T , suc⋅ , ⋅∈𝕄 , +∈𝕄 , 𝕄0s v; L<sq -| W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 , *𝕄 h; !let/thm Lcode <- `[ p ; q ; p1 ; q1 ; n col ∈ 𝕄 ] and q < n and q1 < n and p ⋅ n + q = p1 ⋅ n + q1 ⟹ p = p1 and q = q1` ◀ W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 , *𝕄 prf C1a <- `[ c ; n col ∈ 𝕄 ] and c {/}= 0 ⟹ n ≤ c ⋅ n` / ≤. -| Lpred , suc⋅ , ⋅∈𝕄 p; C1b <- `[ x ; r col ∈ 𝕄 ] ⟹ x ≤ x + r` / ≤. -| +C p; C1 <- `[ c ; n ; q ; r col ∈ 𝕄 ] and q < n and c {/}= 0 ⟹ q {/}= c ⋅ n + r` -| C1a , C1b , L≤T , L≤<T , L<irr , ⋅∈𝕄 , +∈𝕄 v; C2a <- `[ x ; y ; r col ∈ 𝕄 ] ⟹ (x + y) + r = y + (x + r)` -| +A , +C , +∈𝕄 p; C2 <- `[ p ; c ; n ; q ; r col ∈ 𝕄 ] and p ⋅ n + q = (c + p) ⋅ n + r ⟹ q = c ⋅ n + r` -| Rdist , C2a , +K , ⋅∈𝕄 , +∈𝕄 v; C3 <- `[ p ; q ; p1 ; q1 ; n col ∈ 𝕄 ] and p ≤ p1 and q < n and q1 < n and p ⋅ n + q = p1 ⋅ n + q1 ⟹ p = p1 and q = q1` / ≤. -| C1 , C2 , L0+ , L0⋅ , *𝕄 , +𝕄 , ⋅∈𝕄 v; Lcode -| Ltot , L<≤ , C3 v; Lcode -| W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 , *𝕄 h; section 単調な部分列 txt \(f \nearrow k\) は \(f(0) \lt f(1) \lt \cdots \lt f(k)\)、\(f \searrow k\) は \(f(0) > f(1) > \cdots > f(k)\)（値は自然数）。 word ↗ ↘ prop ↗. <- `f ↗ k ⟺ [ ∀ j ∈ 𝕄 . (j ≤ k ⟹ f ap (j) ∈ 𝕄) ] and [ ∀ j ∈ 𝕄 . (j < k ⟹ f ap (j) < f ap (j suc)) ]` prop ↘. <- `f ↘ k ⟺ [ ∀ j ∈ 𝕄 . (j ≤ k ⟹ f ap (j) ∈ 𝕄) ] and [ ∀ j ∈ 𝕄 . (j < k ⟹ f ap (j suc) < f ap (j)) ]` txt 列 \(a\) の部分列は、\(s \nearrow k\) となる添字の列 \(s\) と合成 \(a \circ s\) で表します（\((a \circ s)(j) = a(s(j))\)＝∘𝕄 を仮定します）。 word ∘ prop ∘𝕄 <- `x ∈ 𝕄 ⟹ (f ∘ g) ap (x) = f ap (g ap (x))` txt 単調な列は短く切っても単調（Ltr↗・Ltr↘）。増加列の値は最後の項以下（Lmono）。 !let/thm Ltr↗ <- `[ n ; k col ∈ 𝕄 ] and n ≤ k and f ↗ k ⟹ f ↗ n` ◀ W. , 𝕄0s , IND𝕄 , +𝕄 prf Ltr↗ / ↗. -| L<≤T , L≤T , 𝕄0s p; Ltr↗ -| W. , 𝕄0s , IND𝕄 , +𝕄 h; !let/thm Ltr↘ <- `[ n ; k col ∈ 𝕄 ] and n ≤ k and f ↘ k ⟹ f ↘ n` ◀ W. , 𝕄0s , IND𝕄 , +𝕄 prf Ltr↘ / ↘. -| L<≤T , L≤T , 𝕄0s p; Ltr↘ -| W. , 𝕄0s , IND𝕄 , +𝕄 h; !let/thm Lmono <- `[ m ; k col ∈ 𝕄 ] and m ≤ k and f ↗ k ⟹ f ap (m) ∈ 𝕄 and f ap (m) ≤ f ap (k)` ◀ W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 prf Lb <- `m ∈ 𝕄 and m ≤ 0 and f ↗ 0 ⟹ f ap (m) ∈ 𝕄 and f ap (m) ≤ f ap (0)` / ↗. -| L≤0 , L≤R , 𝕄0s p; Ls <- `k ∈ 𝕄 and [ ∀ m ∈ 𝕄 . (m ≤ k and f ↗ k ⟹ f ap (m) ∈ 𝕄 and f ap (m) ≤ f ap (k)) ] and m ∈ 𝕄 and m ≤ k suc and f ↗ k suc ⟹ f ap (m) ∈ 𝕄 and f ap (m) ≤ f ap (k suc)` / ↗. -| Ltr↗ / ↗. , L≤suc , L<s , L<≤ , L≤T , L≤R , 𝕄0s v; Lmono -| IND𝕄[C_:=`\{ cls k | [ ∀ m ∈ 𝕄 . (m ≤ k and f ↗ k ⟹ f ap (m) ∈ 𝕄 and f ap (m) ≤ f ap (k)) ] \}`] , Lb , Ls , 𝕄0s v; Lmono -| W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 h; txt 部分列の後ろに1項を足して伸ばす（添字の部分 LEs・値の部分 LE↗・LE↘）。 !let/thm LEs <- `[ k ; i ; j col ∈ 𝕄 ] and s ↗ k and s ap (k) = i and i < j and g ap (k suc) = j and [ ∀ m ∈ 𝕄 . (m {/}= k suc ⟹ g ap (m) = s ap (m)) ] ⟹ g ↗ k suc` ◀ W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 prf LEs / ↗. -| L<≠s , L≤≠s , L≤suc , L≤R , L<S , 𝕄0s p; LEs -| W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 h; !let/thm LE↗ <- `[ k ; i ; j col ∈ 𝕄 ] and a ∘ s ↗ k and s ap (k) = i and a ap (j) ∈ 𝕄 and a ap (i) < a ap (j) and g ap (k suc) = j and [ ∀ m ∈ 𝕄 . (m {/}= k suc ⟹ g ap (m) = s ap (m)) ] ⟹ a ∘ g ↗ k suc` ◀ W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 , ∘𝕄 prf LE↗ / ↗. -| ∘𝕄 , L<≠s , L≤≠s , L≤suc , L≤R , L<S , 𝕄0s p; LE↗ -| W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 , ∘𝕄 h; !let/thm LE↘ <- `[ k ; i ; j col ∈ 𝕄 ] and a ∘ s ↘ k and s ap (k) = i and a ap (j) ∈ 𝕄 and a ap (j) < a ap (i) and g ap (k suc) = j and [ ∀ m ∈ 𝕄 . (m {/}= k suc ⟹ g ap (m) = s ap (m)) ] ⟹ a ∘ g ↘ k suc` ◀ W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 , ∘𝕄 prf LE↘ / ↘. -| ∘𝕄 , L<≠s , L≤≠s , L≤suc , L≤R , L<S , 𝕄0s p; LE↘ -| W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 , ∘𝕄 h; txt 有限個の選択：\(i \lt M\) の各 \(i\) にラベルを選んだ列があれば \(M\) にも（LCH）。 !let/thm LCH <- `M ∈ 𝕄 and [ ∀ i ∈ 𝕄 . (i < M ⟹ [ ∃ p ∈ 𝕄 . [ ∃ q ∈ 𝕄 . p < n and q < n and f ap (i) = p ⋅ n + q and [ ∃ s \, (s ↗ p and a ∘ s ↗ p and s ap (p) = i) ] and ¬ [ ∃ s \, (s ↗ p suc and a ∘ s ↗ p suc and s ap (p suc) = i) ] and [ ∃ s \, (s ↗ q and a ∘ s ↘ q and s ap (q) = i) ] and ¬ [ ∃ s \, (s ↗ q suc and a ∘ s ↘ q suc and s ap (q suc) = i) ] ] ]) ] and [ ∃ p ∈ 𝕄 . [ ∃ q ∈ 𝕄 . p < n and q < n and c = p ⋅ n + q and [ ∃ s \, (s ↗ p and a ∘ s ↗ p and s ap (p) = M) ] and ¬ [ ∃ s \, (s ↗ p suc and a ∘ s ↗ p suc and s ap (p suc) = M) ] and [ ∃ s \, (s ↗ q and a ∘ s ↘ q and s ap (q) = M) ] and ¬ [ ∃ s \, (s ↗ q suc and a ∘ s ↘ q suc and s ap (q suc) = M) ] ] ] ⟹ [ ∃ g \, ([ ∀ i ∈ 𝕄 . (i < M suc ⟹ [ ∃ p ∈ 𝕄 . [ ∃ q ∈ 𝕄 . p < n and q < n and g ap (i) = p ⋅ n + q and [ ∃ s \, (s ↗ p and a ∘ s ↗ p and s ap (p) = i) ] and ¬ [ ∃ s \, (s ↗ p suc and a ∘ s ↗ p suc and s ap (p suc) = i) ] and [ ∃ s \, (s ↗ q and a ∘ s ↘ q and s ap (q) = i) ] and ¬ [ ∃ s \, (s ↗ q suc and a ∘ s ↘ q suc and s ap (q suc) = i) ] ] ]) ]) ]` ◀ W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 , upd𝕄 prf hyM <- `|M ∈ 𝕄` ; hyF <- `[ ∀ i ∈ 𝕄 . (i < |M ⟹ [ ∃ p ∈ 𝕄 . [ ∃ q ∈ 𝕄 . p < |n and q < |n and |f ap (i) = p ⋅ |n + q and [ ∃ s \, (s ↗ p and |a ∘ s ↗ p and s ap (p) = i) ] and ¬ [ ∃ s \, (s ↗ p suc and |a ∘ s ↗ p suc and s ap (p suc) = i) ] and [ ∃ s \, (s ↗ q and |a ∘ s ↘ q and s ap (q) = i) ] and ¬ [ ∃ s \, (s ↗ q suc and |a ∘ s ↘ q suc and s ap (q suc) = i) ] ] ]) ]` ; hyC <- `[ ∃ p ∈ 𝕄 . [ ∃ q ∈ 𝕄 . p < |n and q < |n and |c = p ⋅ |n + q and [ ∃ s \, (s ↗ p and |a ∘ s ↗ p and s ap (p) = |M) ] and ¬ [ ∃ s \, (s ↗ p suc and |a ∘ s ↗ p suc and s ap (p suc) = |M) ] and [ ∃ s \, (s ↗ q and |a ∘ s ↘ q and s ap (q) = |M) ] and ¬ [ ∃ s \, (s ↗ q suc and |a ∘ s ↘ q suc and s ap (q suc) = |M) ] ] ]` ; La <- `g ap (|M) = |c and [ ∀ m ∈ 𝕄 . (m {/}= |M ⟹ g ap (m) = |f ap (m)) ] ⟹ [ ∀ i ∈ 𝕄 . (i < |M suc ⟹ [ ∃ p ∈ 𝕄 . [ ∃ q ∈ 𝕄 . p < |n and q < |n and g ap (i) = p ⋅ |n + q and [ ∃ s \, (s ↗ p and |a ∘ s ↗ p and s ap (p) = i) ] and ¬ [ ∃ s \, (s ↗ p suc and |a ∘ s ↗ p suc and s ap (p suc) = i) ] and [ ∃ s \, (s ↗ q and |a ∘ s ↘ q and s ap (q) = i) ] and ¬ [ ∃ s \, (s ↗ q suc and |a ∘ s ↘ q suc and s ap (q suc) = i) ] ] ]) ]` -| hyM , hyF , hyC , L<S , L<irr v; Lg <- `[ ∃ g \, ([ ∀ i ∈ 𝕄 . (i < |M suc ⟹ [ ∃ p ∈ 𝕄 . [ ∃ q ∈ 𝕄 . p < |n and q < |n and g ap (i) = p ⋅ |n + q and [ ∃ s \, (s ↗ p and |a ∘ s ↗ p and s ap (p) = i) ] and ¬ [ ∃ s \, (s ↗ p suc and |a ∘ s ↗ p suc and s ap (p suc) = i) ] and [ ∃ s \, (s ↗ q and |a ∘ s ↘ q and s ap (q) = i) ] and ¬ [ ∃ s \, (s ↗ q suc and |a ∘ s ↘ q suc and s ap (q suc) = i) ] ] ]) ]) ]` -| upd𝕄 , La v; LCH -| W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 , upd𝕄 h[fix]; newpage section 主定理 txt 相異なる \(n^2+1\) 個の数の列は、長さ \(n+1\) の増加部分列か減少部分列を持つ（Erdős–Szekeres）。ここでは値を自然数とします（使うのは値の大小だけです）。 txt 証明：どちらも無いと仮定します。各位置 \(i\) に、\(i\) で終わる最長の増加部分列・減少部分列の長さ \(p+1\)・\(q+1\)（\(p, q \lt n\)）を対応させます（「長さ \(p+1\) のものはあり、\(p+2\) のものは無い」で決める＝LI・LD）。\(i \lt j\) で \(a(i) \lt a(j)\) なら \(i\) で終わる増加部分列を \(j\) まで伸ばせるので \(p\) が違い、\(a(i) > a(j)\) なら \(q\) が違います（INJ1）。よって \(i \mapsto p \cdot n + q\) は \(n^2+1\) 個の位置を \(n^2\) 個の値へ相異なるように送り、鳩の巣原理 PH に反します。 thm `\\{ And n ∈ 𝕄 \\ [ ∀ i ∈ 𝕄 . (i < (n ⋅ n) suc ⟹ a ap (i) ∈ 𝕄) ] \\ [ ∀ i ∈ 𝕄 . [ ∀ j ∈ 𝕄 . (i < (n ⋅ n) suc and j < (n ⋅ n) suc and a ap (i) = a ap (j) ⟹ i = j) ] ] \\} ⟹ [ ∃ s \, (s ↗ n and s ap (n) < (n ⋅ n) suc and (a ∘ s ↗ n or a ∘ s ↘ n)) ] ` ◀ W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 , *𝕄 , upd𝕄 , ∘𝕄 prf hyn <- `|n ∈ 𝕄` ; hyA <- `[ ∀ i ∈ 𝕄 . (i < (|n ⋅ |n) suc ⟹ |a ap (i) ∈ 𝕄) ]` ; hyD <- `[ ∀ i ∈ 𝕄 . [ ∀ j ∈ 𝕄 . (i < (|n ⋅ |n) suc and j < (|n ⋅ |n) suc and |a ap (i) = |a ap (j) ⟹ i = j) ] ]` ; hyNo <- `¬ [ ∃ s \, (s ↗ |n and s ap (|n) < (|n ⋅ |n) suc and (|a ∘ s ↗ |n or |a ∘ s ↘ |n)) ]` ; K0 <- `|n ⋅ |n ∈ 𝕄 and (|n ⋅ |n) suc ∈ 𝕄` -| ⋅∈𝕄 , hyn , 𝕄0s p; B1 <- `[ k ; i col ∈ 𝕄 ] and s ↗ k and |a ∘ s ↗ k and s ap (k) = i and i < (|n ⋅ |n) suc ⟹ k < |n` -| hyNo , Ltot , Ltr↗ , Lmono , L≤<T , hyn , K0 v; B2 <- `[ k ; i col ∈ 𝕄 ] and s ↗ k and |a ∘ s ↘ k and s ap (k) = i and i < (|n ⋅ |n) suc ⟹ k < |n` -| hyNo , Ltot , Ltr↗ , Ltr↘ , Lmono , L≤<T , hyn , K0 v; S0a <- `i ∈ 𝕄 and |a ap (i) ∈ 𝕄 and g ap (0) = i ⟹ g ↗ 0 and |a ∘ g ↗ 0 and |a ∘ g ↘ 0 and g ap (0) = i` / ↗. / ↘. -| ∘𝕄 , L<0 , L≤0 , 𝕄0s p; S0 <- `i ∈ 𝕄 and i < (|n ⋅ |n) suc ⟹ [ ∃ s \, (s ↗ 0 and |a ∘ s ↗ 0 and |a ∘ s ↘ 0 and s ap (0) = i) ]` -| upd𝕄 , S0a , hyA v; LIa <- `i ∈ 𝕄 and i < (|n ⋅ |n) suc and [ ∀ p ∈ 𝕄 . ([ ∃ s \, (s ↗ p and |a ∘ s ↗ p and s ap (p) = i) ] ⟹ [ ∃ s \, (s ↗ p suc and |a ∘ s ↗ p suc and s ap (p suc) = i) ]) ] ⟹ [ ∃ s \, (s ↗ |n and |a ∘ s ↗ |n and s ap (|n) = i) ]` -| IND𝕄[C_:=`\{ cls p | [ ∃ s \, (s ↗ p and |a ∘ s ↗ p and s ap (p) = i) ] \}`] , S0 , hyn v; LI <- `i ∈ 𝕄 and i < (|n ⋅ |n) suc ⟹ [ ∃ p ∈ 𝕄 . p < |n and [ ∃ s \, (s ↗ p and |a ∘ s ↗ p and s ap (p) = i) ] and ¬ [ ∃ s \, (s ↗ p suc and |a ∘ s ↗ p suc and s ap (p suc) = i) ] ]` -| LIa , B1 , L<irr , hyn v; LDa <- `i ∈ 𝕄 and i < (|n ⋅ |n) suc and [ ∀ p ∈ 𝕄 . ([ ∃ s \, (s ↗ p and |a ∘ s ↘ p and s ap (p) = i) ] ⟹ [ ∃ s \, (s ↗ p suc and |a ∘ s ↘ p suc and s ap (p suc) = i) ]) ] ⟹ [ ∃ s \, (s ↗ |n and |a ∘ s ↘ |n and s ap (|n) = i) ]` -| IND𝕄[C_:=`\{ cls p | [ ∃ s \, (s ↗ p and |a ∘ s ↘ p and s ap (p) = i) ] \}`] , S0 , hyn v; LD <- `i ∈ 𝕄 and i < (|n ⋅ |n) suc ⟹ [ ∃ p ∈ 𝕄 . p < |n and [ ∃ s \, (s ↗ p and |a ∘ s ↘ p and s ap (p) = i) ] and ¬ [ ∃ s \, (s ↗ p suc and |a ∘ s ↘ p suc and s ap (p suc) = i) ] ]` -| LDa , B2 , L<irr , hyn v; LabE <- `i ∈ 𝕄 and i < (|n ⋅ |n) suc ⟹ [ ∃ c \, ([ ∃ p ∈ 𝕄 . [ ∃ q ∈ 𝕄 . p < |n and q < |n and c = p ⋅ |n + q and [ ∃ s \, (s ↗ p and |a ∘ s ↗ p and s ap (p) = i) ] and ¬ [ ∃ s \, (s ↗ p suc and |a ∘ s ↗ p suc and s ap (p suc) = i) ] and [ ∃ s \, (s ↗ q and |a ∘ s ↘ q and s ap (q) = i) ] and ¬ [ ∃ s \, (s ↗ q suc and |a ∘ s ↘ q suc and s ap (q suc) = i) ] ] ]) ]` -| LI , LD v; Lsl <- `[ M ; N col ∈ 𝕄 ] and M suc ≤ N ⟹ M < N` / <. -| O p; CHs <- `M ∈ 𝕄 and (M ≤ (|n ⋅ |n) suc ⟹ [ ∃ f \, ([ ∀ i ∈ 𝕄 . (i < M ⟹ [ ∃ p ∈ 𝕄 . [ ∃ q ∈ 𝕄 . p < |n and q < |n and f ap (i) = p ⋅ |n + q and [ ∃ s \, (s ↗ p and |a ∘ s ↗ p and s ap (p) = i) ] and ¬ [ ∃ s \, (s ↗ p suc and |a ∘ s ↗ p suc and s ap (p suc) = i) ] and [ ∃ s \, (s ↗ q and |a ∘ s ↘ q and s ap (q) = i) ] and ¬ [ ∃ s \, (s ↗ q suc and |a ∘ s ↘ q suc and s ap (q suc) = i) ] ] ]) ]) ]) and M suc ≤ (|n ⋅ |n) suc ⟹ [ ∃ g \, ([ ∀ i ∈ 𝕄 . (i < M suc ⟹ [ ∃ p ∈ 𝕄 . [ ∃ q ∈ 𝕄 . p < |n and q < |n and g ap (i) = p ⋅ |n + q and [ ∃ s \, (s ↗ p and |a ∘ s ↗ p and s ap (p) = i) ] and ¬ [ ∃ s \, (s ↗ p suc and |a ∘ s ↗ p suc and s ap (p suc) = i) ] and [ ∃ s \, (s ↗ q and |a ∘ s ↘ q and s ap (q) = i) ] and ¬ [ ∃ s \, (s ↗ q suc and |a ∘ s ↘ q suc and s ap (q suc) = i) ] ] ]) ]) ]` -| LabE , LCH , Lsl , L<≤ , K0 v; CH <- `[ ∃ f \, ([ ∀ i ∈ 𝕄 . (i < (|n ⋅ |n) suc ⟹ [ ∃ p ∈ 𝕄 . [ ∃ q ∈ 𝕄 . p < |n and q < |n and f ap (i) = p ⋅ |n + q and [ ∃ s \, (s ↗ p and |a ∘ s ↗ p and s ap (p) = i) ] and ¬ [ ∃ s \, (s ↗ p suc and |a ∘ s ↗ p suc and s ap (p suc) = i) ] and [ ∃ s \, (s ↗ q and |a ∘ s ↘ q and s ap (q) = i) ] and ¬ [ ∃ s \, (s ↗ q suc and |a ∘ s ↘ q suc and s ap (q suc) = i) ] ] ]) ]) ]` -| IND𝕄[C_:=`\{ cls M | M ≤ (|n ⋅ |n) suc ⟹ [ ∃ f \, ([ ∀ i ∈ 𝕄 . (i < M ⟹ [ ∃ p ∈ 𝕄 . [ ∃ q ∈ 𝕄 . p < |n and q < |n and f ap (i) = p ⋅ |n + q and [ ∃ s \, (s ↗ p and |a ∘ s ↗ p and s ap (p) = i) ] and ¬ [ ∃ s \, (s ↗ p suc and |a ∘ s ↗ p suc and s ap (p suc) = i) ] and [ ∃ s \, (s ↗ q and |a ∘ s ↘ q and s ap (q) = i) ] and ¬ [ ∃ s \, (s ↗ q suc and |a ∘ s ↘ q suc and s ap (q suc) = i) ] ] ]) ]) ] \}`] , CHs , L<0 , L≤R , K0 , 𝕄0s v; Xa↗ <- `[ p ; i ; j col ∈ 𝕄 ] and s ↗ p and |a ∘ s ↗ p and s ap (p) = i and i < j and |a ap (j) ∈ 𝕄 and |a ap (i) < |a ap (j) and g ap (p suc) = j and [ ∀ m ∈ 𝕄 . (m {/}= p suc ⟹ g ap (m) = s ap (m)) ] ⟹ g ↗ p suc and |a ∘ g ↗ p suc and g ap (p suc) = j` -| LEs , LE↗ v; X↗ <- `[ p ; i ; j col ∈ 𝕄 ] and [ ∃ s \, (s ↗ p and |a ∘ s ↗ p and s ap (p) = i) ] and i < j and |a ap (j) ∈ 𝕄 and |a ap (i) < |a ap (j) ⟹ [ ∃ s \, (s ↗ p suc and |a ∘ s ↗ p suc and s ap (p suc) = j) ]` -| upd𝕄 , Xa↗ v; Xa↘ <- `[ p ; i ; j col ∈ 𝕄 ] and s ↗ p and |a ∘ s ↘ p and s ap (p) = i and i < j and |a ap (j) ∈ 𝕄 and |a ap (j) < |a ap (i) and g ap (p suc) = j and [ ∀ m ∈ 𝕄 . (m {/}= p suc ⟹ g ap (m) = s ap (m)) ] ⟹ g ↗ p suc and |a ∘ g ↘ p suc and g ap (p suc) = j` -| LEs , LE↘ v; X↘ <- `[ p ; i ; j col ∈ 𝕄 ] and [ ∃ s \, (s ↗ p and |a ∘ s ↘ p and s ap (p) = i) ] and i < j and |a ap (j) ∈ 𝕄 and |a ap (j) < |a ap (i) ⟹ [ ∃ s \, (s ↗ p suc and |a ∘ s ↘ p suc and s ap (p suc) = j) ]` -| upd𝕄 , Xa↘ v; INJ1 <- `[ i ; j col ∈ 𝕄 ] and i < j and j < (|n ⋅ |n) suc and [ ∃ p ∈ 𝕄 . [ ∃ q ∈ 𝕄 . p < |n and q < |n and c = p ⋅ |n + q and [ ∃ s \, (s ↗ p and |a ∘ s ↗ p and s ap (p) = i) ] and ¬ [ ∃ s \, (s ↗ p suc and |a ∘ s ↗ p suc and s ap (p suc) = i) ] and [ ∃ s \, (s ↗ q and |a ∘ s ↘ q and s ap (q) = i) ] and ¬ [ ∃ s \, (s ↗ q suc and |a ∘ s ↘ q suc and s ap (q suc) = i) ] ] ] and [ ∃ p ∈ 𝕄 . [ ∃ q ∈ 𝕄 . p < |n and q < |n and c = p ⋅ |n + q and [ ∃ s \, (s ↗ p and |a ∘ s ↗ p and s ap (p) = j) ] and ¬ [ ∃ s \, (s ↗ p suc and |a ∘ s ↗ p suc and s ap (p suc) = j) ] and [ ∃ s \, (s ↗ q and |a ∘ s ↘ q and s ap (q) = j) ] and ¬ [ ∃ s \, (s ↗ q suc and |a ∘ s ↘ q suc and s ap (q suc) = j) ] ] ] ⟹ ⊥` -| Lcode , X↗ , X↘ , L≠< , L<T , L<irr , hyA , hyD , hyn , K0 v; INJ <- `[ i ; j col ∈ 𝕄 ] and i < (|n ⋅ |n) suc and j < (|n ⋅ |n) suc and [ ∃ p ∈ 𝕄 . [ ∃ q ∈ 𝕄 . p < |n and q < |n and c = p ⋅ |n + q and [ ∃ s \, (s ↗ p and |a ∘ s ↗ p and s ap (p) = i) ] and ¬ [ ∃ s \, (s ↗ p suc and |a ∘ s ↗ p suc and s ap (p suc) = i) ] and [ ∃ s \, (s ↗ q and |a ∘ s ↘ q and s ap (q) = i) ] and ¬ [ ∃ s \, (s ↗ q suc and |a ∘ s ↘ q suc and s ap (q suc) = i) ] ] ] and [ ∃ p ∈ 𝕄 . [ ∃ q ∈ 𝕄 . p < |n and q < |n and c = p ⋅ |n + q and [ ∃ s \, (s ↗ p and |a ∘ s ↗ p and s ap (p) = j) ] and ¬ [ ∃ s \, (s ↗ p suc and |a ∘ s ↗ p suc and s ap (p suc) = j) ] and [ ∃ s \, (s ↗ q and |a ∘ s ↘ q and s ap (q) = j) ] and ¬ [ ∃ s \, (s ↗ q suc and |a ∘ s ↘ q suc and s ap (q suc) = j) ] ] ] ⟹ i = j` -| INJ1 , L≠< v; Fr <- `[ ∀ i ∈ 𝕄 . (i < (|n ⋅ |n) suc ⟹ [ ∃ p ∈ 𝕄 . [ ∃ q ∈ 𝕄 . p < |n and q < |n and f ap (i) = p ⋅ |n + q and [ ∃ s \, (s ↗ p and |a ∘ s ↗ p and s ap (p) = i) ] and ¬ [ ∃ s \, (s ↗ p suc and |a ∘ s ↗ p suc and s ap (p suc) = i) ] and [ ∃ s \, (s ↗ q and |a ∘ s ↘ q and s ap (q) = i) ] and ¬ [ ∃ s \, (s ↗ q suc and |a ∘ s ↘ q suc and s ap (q suc) = i) ] ] ]) ] ⟹ [ ∀ i ∈ 𝕄 . (i < (|n ⋅ |n) suc ⟹ f ap (i) ∈ 𝕄 and f ap (i) < |n ⋅ |n) ]` -| L<sq , +∈𝕄 , ⋅∈𝕄 , hyn v; Fi <- `[ ∀ i ∈ 𝕄 . (i < (|n ⋅ |n) suc ⟹ [ ∃ p ∈ 𝕄 . [ ∃ q ∈ 𝕄 . p < |n and q < |n and f ap (i) = p ⋅ |n + q and [ ∃ s \, (s ↗ p and |a ∘ s ↗ p and s ap (p) = i) ] and ¬ [ ∃ s \, (s ↗ p suc and |a ∘ s ↗ p suc and s ap (p suc) = i) ] and [ ∃ s \, (s ↗ q and |a ∘ s ↘ q and s ap (q) = i) ] and ¬ [ ∃ s \, (s ↗ q suc and |a ∘ s ↘ q suc and s ap (q suc) = i) ] ] ]) ] ⟹ [ ∀ i ∈ 𝕄 . [ ∀ j ∈ 𝕄 . (i < (|n ⋅ |n) suc and j < (|n ⋅ |n) suc and f ap (i) = f ap (j) ⟹ i = j) ] ]` -| INJ v; Ffin <- `(|n ⋅ |n) suc ≤ |n ⋅ |n` -| CH , Fr , Fi , PH , K0 v; Lc <- `n ∈ 𝕄 and [ ∀ i ∈ 𝕄 . (i < (n ⋅ n) suc ⟹ a ap (i) ∈ 𝕄) ] and [ ∀ i ∈ 𝕄 . [ ∀ j ∈ 𝕄 . (i < (n ⋅ n) suc and j < (n ⋅ n) suc and a ap (i) = a ap (j) ⟹ i = j) ] ] and ¬ [ ∃ s \, (s ↗ n and s ap (n) < (n ⋅ n) suc and (a ∘ s ↗ n or a ∘ s ↘ n)) ] ⟹ (n ⋅ n) suc ≤ n ⋅ n` -| W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 , *𝕄 , upd𝕄 , ∘𝕄 h[fix]; goal -| Lc , L<irr / <. , ⋅∈𝕄 v; goal -| W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 , *𝕄 , upd𝕄 , ∘𝕄 h; !txt 2026-10-07 探索のメモ：本全体 約12秒（キャッシュ無し・Thm の秒の合計）。ラベル（Lab）の式が大きく、Vampire の秒が sos の順・段の切り方で 0.5〜25秒と大きく揺れる。存在を消す段（upd𝕄 で g を得る）は、g を前件に置いた補題＋固定化（LCH の h[fix]・90秒→0.2秒）で速くなった。結論が ⊥ の段は前提が矛盾すると contradictory_axioms で不合格＝結論を (n⋅n)+1 ≤ n⋅n にして L<irr で締める。
表示（保存しません）
保存にはMatheliaへのログインが要ります。