BoundaryExamples.lean

1 import PaperX.Residual
2 import PaperX.Compactness
3 
4 /-!
5 Hypothesis checks and exact finite models. These examples distinguish a root
6 from a branch and finite-level occupancy from a universal arithmetic claim.
7 -/
8 set_option autoImplicit false
9 namespace PaperX.BoundaryExamples
10 open PaperX.Compactness
11 
12 /-- Finite, nonempty levels with a non-surjective transition at every depth. -/
13 def pruningTower : Tower where
14   Level := fun _ => Bool
15   parent := fun _ _ => false
16 
17 theorem pruning_finite : FiniteLevels pruningTower := by
18   intro n
19   change ∃ xs : List Bool, ∀ x : Bool, x ∈ xs
20   refine ⟨[false, true], ?_⟩
21   intro x
22   cases x <;> simp
23 
24 theorem pruning_nonempty (n : Nat) : Nonempty (pruningTower.Level n) := ⟨false⟩
25 
26 theorem pruning_nonsurjective (n : Nat) :
27     ¬ ∃ x : pruningTower.Level (n+1), pruningTower.parent n x = true := by
28   rintro ⟨x, hx⟩
29   cases hx
30 
31 theorem pruning_has_branch : Nonempty (Branch pruningTower) :=
32   finite_branch_compactness pruningTower pruning_finite pruning_nonempty
33 
34 theorem pruning_branch_values (b : Branch pruningTower) (n : Nat) :
35     b.value n = false := (b.compatible n).symm
36 
37 /-- An occupied root whose next level is empty. -/
38 def dyingTower : Tower where
39   Level := fun n => {x : Fin 1 // n = 0}
40   parent := fun n x => False.elim (by have h := x.2; omega)
41 
42 theorem dying_has_root : Nonempty (dyingTower.Level 0) := ⟨⟨0, rfl⟩⟩
43 
44 theorem dying_finite : FiniteLevels dyingTower := by
45   intro n
46   by_cases hn : n = 0
47   · subst n
48     change ∃ xs : List {x : Fin 1 // (0 : Nat) = 0}, ∀ x, x ∈ xs
49     refine ⟨[⟨0, rfl⟩], ?_⟩
50     intro x
51     have hx : x = ⟨0, rfl⟩ := by
52       apply Subtype.ext
53       apply Fin.ext
54       have h := x.1.2
55       omega
56     exact List.mem_singleton.mpr hx
57   · refine ⟨[], ?_⟩
58     intro x
59     exact False.elim (hn x.2)
60 
61 theorem dying_empty_level : ¬ Nonempty (dyingTower.Level 1) := by
62   rintro ⟨x⟩
63   have h := x.2
64   omega
65 
66 theorem root_not_enough : ¬ Nonempty (Branch dyingTower) :=
67   empty_level_obstruction dyingTower 1 dying_empty_level
68 
69 /-- Removing finiteness invalidates the compactness inference. Each level has
70 all natural numbers >= its depth, and reduction preserves the number. -/
71 def escapingTower : Tower where
72   Level := fun n => {k : Nat // n ≤ k}
73   parent := fun n x => ⟨x.1, by have h := x.2; omega⟩
74 
75 theorem escaping_levels_nonempty (n : Nat) : Nonempty (escapingTower.Level n) :=
76   ⟨⟨n, Nat.le_refl n⟩⟩
77 
78 theorem escaping_no_branch : ¬ Nonempty (Branch escapingTower) := by
79   rintro ⟨b⟩
80   have constant : ∀ n, (b.value n).1 = (b.value 0).1 := by
81     intro n
82     induction n with
83     | zero => rfl
84     | succ n ih =>
85       have hp := congrArg Subtype.val (b.compatible n)
86       change (b.value (n+1)).1 = (b.value n).1 at hp
87       exact hp.trans ih
88   have hbound := (b.value ((b.value 0).1 + 1)).2
89   have heq := constant ((b.value 0).1 + 1)
90   omega
91 
92 /-- Exact scalar finite-level root enumeration; no probabilistic arithmetic. -/
93 def roots (p depth : Nat) : List Nat :=
94   (List.range (p^depth)).filter (fun x => (x*x+1) % (p^depth) == 0)
95 
96 theorem roots_mod2 : roots 2 1 = [1] := by decide
97 
98 theorem roots_mod4 : roots 2 2 = [] := by decide
99 
100 theorem roots_mod3 : roots 3 1 = [] := by decide
101 
102 theorem roots_mod7 : roots 7 1 = [] := by decide
103 
104 theorem roots_mod5 : roots 5 1 = [2, 3] := by decide
105 
106 theorem roots_mod25 : roots 5 2 = [7, 18] := by decide
107 
108 /-- The sign characters merge mod 2 but separate mod 4. -/
109 theorem signs_same_mod2 : (1 : Int) % 2 = (-1 : Int) % 2 := by decide
110 
111 theorem signs_different_mod4 : (1 : Int) % 4 ≠ (-1 : Int) % 4 := by decide
112 
113 /-- Matrix arithmetic over the two-element field, represented by Fin 2. -/
114 def add2 (x y : Fin 2) : Fin 2 := ⟨(x.1+y.1)%2, Nat.mod_lt _ (by decide)⟩
115 def mul2 (x y : Fin 2) : Fin 2 := ⟨(x.1*y.1)%2, Nat.mod_lt _ (by decide)⟩
116 abbrev Matrix2 := Fin 2 → Fin 2 → Fin 2
117 
118 def identity2 : Matrix2 := fun i j => if i = j then 1 else 0
119 
120 def matmul2 (a b : Matrix2) : Matrix2 := fun i j =>
121   add2 (mul2 (a i 0) (b 0 j)) (mul2 (a i 1) (b 1 j))
122 
123 def trace2 (a : Matrix2) : Fin 2 := add2 (a 0 0) (a 1 1)
124 
125 theorem identity2_idempotent : matmul2 identity2 identity2 = identity2 := by
126   funext i j
127   revert i j
128   decide
129 
130 theorem identity2_trace_zero : trace2 identity2 = 0 := by decide
131 
132 theorem identity2_nonzero : identity2 ≠ (fun _ _ => 0) := by
133   intro h
134   have he := congrFun (congrFun h 0) 0
135   change (1 : Fin 2) = 0 at he
136   exact (by decide : (1 : Fin 2) ≠ 0) he
137 
138 end PaperX.BoundaryExamples

Back to source controls