BinaryExamples.lean

1 import MachineTheory.BinaryCertificate
2 import Mathlib.Tactic.NormNum
3 import Mathlib.Tactic.FinCases
4 
5 /-! # Source examples of checked closure and its required assumptions -/
6 namespace Komorebi.MachineTheory.BinaryExamples
7 open HardInquiry BinaryDiagnosis Finset
8 
9 abbrev World := Bool × Bool × Bool
10 abbrev Query := Fin 3 ⊕ World
11 
12 def eight : Model World Query Bool World Unit where
13   permitted := fun _ _ => true
14   next := fun _ x => x
15   observe := fun e x => match e with
16     | .inl i => if i=0 then x.1 else if i=1 then x.2.1 else x.2.2
17     | .inr y => decide (x=y)
18   accept := fun x y => decide (x=y)
19   stepCost := fun _ _ => 1
20   terminalCost := fun _ _ _ => 1
21 
22 theorem eight_scope : Scope eight := by
23   constructor
24   · intro e x; rfl
25   · intro c x y hx hy
26     have hx' : x = c := of_decide_eq_true hx
27     have hy' : y = c := of_decide_eq_true hy
28     exact hx'.trans hy'.symm
29   · intro e; rfl
30   · intro c V _; rfl
31 
32 /-- The source supplies both coordinate queries and singleton queries to this same model. -/
33 def balanced : Tree Query Bool World 3 :=
34   .inr (.inl 0, fun a => some (.inr (.inl 1, fun b =>
35     some (.inr (.inl 2, fun c => some (a,b,c))))))
36 
37 theorem balanced_checked : checkCandidate eight 3 univ balanced = true := by decide
38 
39 theorem balanced_valid : eight.Valid 3 univ balanced :=
40   ((checkCandidate_iff eight 3 univ balanced).mp balanced_checked).1
41 
42 theorem balanced_profile : eight.profile 3 univ balanced = (fun _ => 4,15) := by decide
43 
44 theorem balanced_structure : leaves 3 balanced = 8 ∧ depth 3 balanced = 3 ∧
45     unary 3 balanced = 0 ∧ Model.records 3 balanced = 15 := by decide
46 
47 /-- Every horizon at least three has this frontier, by the general theorem, not enumeration. -/
48 theorem eight_frontier_all (n : ℕ) : eight.solve (3+n) univ = {(fun _ => 4,15)} := by
49   have h := closed_frontier_all_larger_horizons eight eight_scope 3 univ balanced balanced_checked n
50   have he : lowerProfile (univ : Finset World).card = (fun _ => 4,15) := by decide
51   simpa only [he] using h
52 
53 theorem eight_no_two_queries : ¬ ∃ t : Tree Query Bool World 2, eight.Valid 2 univ t :=
54   impossible_below_information_depth eight eight_scope 2 univ (by decide)
55 
56 def stop (h : ℕ) (c : World) : Tree Query Bool World h :=
57   match h with | 0 => c | _+1 => .inl c
58 
59 def equalityStep (h : ℕ) (c : World) (tail : Tree Query Bool World h) :
60     Tree Query Bool World (h+1) :=
61   .inr (.inr c, fun o => some (if o then stop h c else tail))
62 
63 def equality : Tree Query Bool World 7 :=
64   equalityStep 6 (false,false,false)
65     (equalityStep 5 (false,false,true)
66     (equalityStep 4 (false,true,false)
67     (equalityStep 3 (false,true,true)
68     (equalityStep 2 (true,false,false)
69     (equalityStep 1 (true,false,true)
70     (equalityStep 0 (true,true,false) (true,true,true)))))))
71 
72 theorem equality_valid : eight.Valid 7 univ equality := by decide
73 
74 theorem equality_profile : eight.profile 7 univ equality = (fun _ => 8,15) := by decide
75 
76 /-- Smallest storage alone does not close the work/storage frontier. -/
77 theorem equality_rejected : checkCandidate eight 7 univ equality = false := by decide
78 
79 /-- The checker rejecting one candidate supplies no infeasibility conclusion. -/
80 theorem rejected_but_feasible : checkCandidate eight 7 univ equality = false ∧
81     ∃ t : Tree Query Bool World 7, eight.Valid 7 univ t :=
82   ⟨equality_rejected,⟨equality,equality_valid⟩⟩
83 
84 /-- A matching tree shape with a wrong terminal action is not a certificate. -/
85 def wrongLeaves : Tree Query Bool World 3 :=
86   .inr (.inl 0, fun _ => some (.inr (.inl 1, fun _ =>
87     some (.inr (.inl 2, fun _ => some (false,false,false))))))
88 
89 theorem wrong_shape_matches_cost : eight.profile 3 univ wrongLeaves = (fun _ => 4,15) := by decide
90 
91 theorem wrong_leaves_rejected : checkCandidate eight 3 univ wrongLeaves = false ∧
92     ¬ eight.Valid 3 univ wrongLeaves := by decide
93 
94 /-- A three-case binary model makes a redundant query fit inside an optimal depth. -/
95 def three : Model (Fin 3) (Fin 3) Bool (Fin 3) Unit where
96   permitted := fun _ _ => true
97   next := fun _ x => x
98   observe := fun e x => decide (e=x)
99   accept := fun x c => decide (x=c)
100   stepCost := fun _ _ => 1
101   terminalCost := fun _ _ _ => 1
102 
103 theorem three_scope : Scope three := by
104   constructor
105   · intro e x; rfl
106   · intro c x y hx hy
107     exact (of_decide_eq_true hx).trans (of_decide_eq_true hy).symm
108   · intro e; rfl
109   · intro c V _; rfl
110 
111 def cleanThree : Tree (Fin 3) Bool (Fin 3) 2 :=
112   .inr (0,fun o => if o then some (.inl 0)
113     else some (.inr (1,fun p => some (if p then (1 : Fin 3) else (2 : Fin 3)))))
114 
115 def unaryThree : Tree (Fin 3) Bool (Fin 3) 2 :=
116   .inr (0,fun o => if o then some (.inr (0,fun p => if p then some (0 : Fin 3) else none))
117     else some (.inr (1,fun p => some (if p then (1 : Fin 3) else (2 : Fin 3)))))
118 
119 theorem cleanThree_checked : checkCandidate three 2 univ cleanThree = true := by decide
120 
121 theorem unaryThree_valid : three.Valid 2 univ unaryThree := by decide
122 
123 theorem unaryThree_profile : three.profile 2 univ unaryThree = (fun _ => 3,6) := by decide
124 
125 theorem unaryThree_extra_record : unary 2 unaryThree = 1 ∧ Model.records 2 unaryThree = 6 := by decide
126 
127 /-- Optimal work alone does not certify minimum literal storage. -/
128 theorem unaryThree_rejected : checkCandidate three 2 univ unaryThree = false := by decide
129 
130 theorem three_frontier_all (n : ℕ) : three.solve (2+n) univ = {(fun _ => 3,5)} := by
131   have h := closed_frontier_all_larger_horizons three three_scope 2 univ cleanThree cleanThree_checked n
132   have he : lowerProfile (univ : Finset (Fin 3)).card = (fun _ => 3,5) := by decide
133   simpa only [he] using h
134 
135 /-- State reset leaves singleton repair semantics intact, but removes original-state identification. -/
136 def reset : Model World Query Bool World Unit :=
137   { eight with next := fun _ _ => (false,false,false), observe := fun _ _ => false }
138 
139 def resetTree : Tree Query Bool World 1 :=
140   .inr (.inl 0,fun o => if o then none else some (false,false,false))
141 
142 theorem reset_valid_and_small : reset.Valid 1 univ resetTree ∧
143     reset.profile 1 univ resetTree = (fun _ => 2,2) := by decide
144 
145 theorem reset_not_scope : ¬ Scope reset := by
146   intro s
147   have he := s.immutable (.inl 0) (true,true,true)
148   have : (false,false,false) ≠ (true,true,true) := by decide
149   exact this he
150 
151 /-- Changing only the success predicate admits a universal one-step repair. -/
152 def universalRepair : Model World Query Bool World Unit :=
153   { eight with accept := fun _ _ => true }
154 
155 theorem universal_repair_small : universalRepair.Valid 0 univ (false,false,false) ∧
156     universalRepair.profile 0 univ (false,false,false) = (fun _ => 1,1) := by
157   constructor
158   · change universalRepair.Terminal univ (false,false,false)
159     decide
160   · rfl
161 
162 theorem universal_not_scope : ¬ Scope universalRepair := by
163   intro s
164   have he := s.singleton (false,false,false) (false,false,false) (true,true,true) rfl rfl
165   exact (by decide : (false,false,false) ≠ (true,true,true)) he
166 
167 /-- The missing terminal unit changes the online statement, not the number of leaves. -/
168 def freeTerminal : Model World Query Bool World Unit :=
169   { eight with terminalCost := fun _ _ _ => 0 }
170 
171 theorem free_terminal_work : freeTerminal.Valid 3 univ balanced ∧
172     freeTerminal.profile 3 univ balanced = (fun _ => 3,15) := by decide
173 
174 /-- A nonbinary direct reveal violates binary counting if the alphabet is ignored. -/
175 def directFour : Model (Fin 4) Unit (Fin 4) (Fin 4) Unit where
176   permitted := fun _ _ => true
177   next := fun _ x => x
178   observe := fun _ x => x
179   accept := fun x c => decide (x=c)
180   stepCost := fun _ _ => 1
181   terminalCost := fun _ _ _ => 1
182 
183 def directFourTree : Tree Unit (Fin 4) (Fin 4) 1 := .inr ((),fun o => some o)
184 
185 theorem direct_four_small : directFour.Valid 1 univ directFourTree ∧
186     directFour.profile 1 univ directFourTree = (fun _ => 2,5) := by decide
187 
188 /-- Immutability and binary reports alone do not supply informative queries. -/
189 def silent : Model Bool Unit Bool Bool Unit where
190   permitted := fun _ _ => true
191   next := fun _ x => x
192   observe := fun _ _ => false
193   accept := fun x c => decide (x=c)
194   stepCost := fun _ _ => 1
195   terminalCost := fun _ _ _ => 1
196 
197 theorem silent_scope : Scope silent := by
198   constructor
199   · intro e x; rfl
200   · intro c x y hx hy
201     exact (of_decide_eq_true hx).trans (of_decide_eq_true hy).symm
202   · intro e; rfl
203   · intro c V _; rfl
204 
205 theorem silent_update : silent.update univ () false = univ := by decide
206 
207 /-- No finite horizon succeeds, despite fitting the numerical lower bounds at larger horizons. -/
208 theorem silent_impossible (h : ℕ) : ¬ ∃ t : Tree Unit Bool Bool h, silent.Valid h univ t := by
209   induction h with
210   | zero =>
211     rintro ⟨t,ht⟩
212     have hc := terminal_card_one silent silent_scope univ t ht
213     have hn : (univ : Finset Bool).card = 2 := by decide
214     omega
215   | succ h ih =>
216     rintro ⟨t,ht⟩
217     cases t with
218     | inl c =>
219       have hc := terminal_card_one silent silent_scope univ c ht
220       have hn : (univ : Finset Bool).card = 2 := by decide
221       omega
222     | inr ek =>
223       obtain ⟨e,k⟩ := ek
224       cases e
225       obtain ⟨u,_,hu⟩ := (silent.valid_child ht false).mp (by rw [silent_update]; exact univ_nonempty)
226       rw [silent_update] at hu
227       exact ih ⟨u,hu⟩
228 
229 set_option maxRecDepth 8192 in
230 set_option maxHeartbeats 2000000 in
231 /-- The full finite guard is computed on the eight-case source model. -/
232 theorem eight_admission_checked : admissionCheck eight 3 univ balanced = true := by decide
233 
234 theorem reset_guard_rejects : checkScope reset = false := by decide
235 
236 theorem universal_guard_rejects : checkScope universalRepair = false := by decide
237 
238 theorem free_terminal_guard_rejects : checkScope freeTerminal = false := by decide
239 
240 /-- The n=1 boundary includes the final unit-cost repair and one stored record. -/
241 theorem singleton_checked : checkCandidate eight 0 {(false,false,false)} (false,false,false) = true := by decide
242 
243 theorem empty_support_impossible (h : ℕ) :
244     ¬ ∃ t : Tree Query Bool World h, eight.Valid h ∅ t := by
245   rintro ⟨t,ht⟩
246   exact (eight.valid_nonempty ht).ne_empty rfl
247 
248 end Komorebi.MachineTheory.BinaryExamples

Back to source controls