BinaryDiagnosis.lean

1 import MachineTheory.BinaryStructure
2 
3 /-!
4 # Core 5.3: lower bounds for the actual inquiry model
5 
6 Immutability and singleton success are premises of identification, not consequences
7 of binary reports. Terminal work is charged. Total availability is not needed for
8 the lower bound, so the source's total-query case is included as a specialization.
9 -/
10 namespace Komorebi.MachineTheory.BinaryDiagnosis
11 open HardInquiry Finset
12 variable {X E C : Type} [DecidableEq X]
13 
14 /-- The exact scope in which counting hidden cases counts required repair leaves. -/
15 structure Scope (M : Model X E Bool C Unit) : Prop where
16   immutable : ∀ e x, M.next e x = x
17   singleton : ∀ c x y, M.accept x c = true → M.accept y c = true → x = y
18   query_cost : ∀ e, M.stepCost e () = 1
19   terminal_cost : ∀ c V, V.Nonempty → M.terminalCost c V () = 1
20 
21 /-- Validity rules out internal nodes with no possible successor. -/
22 theorem valid_live (M : Model X E Bool C Unit) (h : ℕ) (V : Finset X)
23     (t : Tree E Bool C h) (ht : M.Valid h V t) : Live h t := by
24   induction h generalizing V with
25   | zero => trivial
26   | succ h ih =>
27     cases t with
28     | inl c => trivial
29     | inr ek =>
30       obtain ⟨e,k⟩ := ek
31       constructor
32       · obtain ⟨x,hx⟩ := ht.1.1
33         obtain ⟨u,hu,_⟩ := (M.valid_child ht (M.observe e x)).mp ⟨_,M.actual_next_mem hx e⟩
34         cases ho : M.observe e x with
35         | false =>
36           rw [ho] at hu
37           exact Or.inl (by simp only [hu,ne_eq,reduceCtorEq,not_false_eq_true])
38         | true =>
39           rw [ho] at hu
40           exact Or.inr (by simp only [hu,ne_eq,reduceCtorEq,not_false_eq_true])
41       · intro o u hu
42         exact ih (M.update V e o) u (by simpa only [hu] using ht.2 o)
43 
44 theorem update_immutable (M : Model X E Bool C Unit) (s : Scope M)
45     (V : Finset X) (e : E) (o : Bool) :
46     M.update V e o = V.filter (fun x => M.observe e x = o) := by
47   have he : M.next e = id := funext (s.immutable e)
48   simp only [Model.update,he,Finset.image_id]
49 
50 /-- The two reachable supports partition, rather than duplicate, the initial cases. -/
51 theorem binary_card_split (M : Model X E Bool C Unit) (s : Scope M)
52     (V : Finset X) (e : E) :
53     V.card = (M.update V e false).card + (M.update V e true).card := by
54   rw [update_immutable M s,update_immutable M s]
55   have he : V.filter (fun x => M.observe e x = true) = V.filter (fun x => ¬ M.observe e x = false) := by
56     ext x
57     cases M.observe e x <;> simp
58   rw [he]
59   exact (Finset.card_filter_add_card_filter_not (s := V) (fun x => M.observe e x = false)).symm
60 
61 omit [DecidableEq X] in
62 /-- No two distinct immutable cases can share an acceptable repair leaf. -/
63 theorem terminal_card_one (M : Model X E Bool C Unit) (s : Scope M)
64     (V : Finset X) (c : C) (ht : M.Terminal V c) : V.card = 1 := by
65   obtain ⟨x,hx⟩ := ht.1
66   have he : V = {x} := by
67     ext y
68     simp only [mem_singleton]
69     constructor
70     · intro hy
71       exact s.singleton c y x (ht.2 y hy) (ht.2 x hx)
72     · intro hy
73       simpa only [hy] using hx
74   simp only [he,card_singleton]
75 
76 /-- Recursive distinct-leaf accounting is derived from the actual success predicate. -/
77 theorem cases_le_leaves (M : Model X E Bool C Unit) (s : Scope M)
78     (h : ℕ) (V : Finset X) (t : Tree E Bool C h) (ht : M.Valid h V t) :
79     V.card ≤ leaves h t := by
80   induction h generalizing V with
81   | zero => exact (terminal_card_one M s V t ht).le
82   | succ h ih =>
83     cases t with
84     | inl c => exact (terminal_card_one M s V c ht).le
85     | inr ek =>
86       obtain ⟨e,k⟩ := ek
87       have branch : ∀ o, (M.update V e o).card ≤ ((k o).map (leaves h)).getD 0 := by
88         intro o
89         cases ho : k o with
90         | none =>
91           have he : M.update V e o = ∅ := by simpa only [ho] using ht.2 o
92           simp only [he,card_empty,Option.map_none,Option.getD_none,le_refl]
93         | some u =>
94           exact ih (M.update V e o) u (by simpa only [ho] using ht.2 o)
95       rw [binary_card_split M s V e]
96       exact Nat.add_le_add (branch false) (branch true)
97 
98 /-- In this exact deterministic scope, every retained leaf has precisely one case. -/
99 theorem cases_eq_leaves (M : Model X E Bool C Unit) (s : Scope M)
100     (h : ℕ) (V : Finset X) (t : Tree E Bool C h) (ht : M.Valid h V t) :
101     V.card = leaves h t := by
102   induction h generalizing V with
103   | zero => exact terminal_card_one M s V t ht
104   | succ h ih =>
105     cases t with
106     | inl c => exact terminal_card_one M s V c ht
107     | inr ek =>
108       obtain ⟨e,k⟩ := ek
109       have branch : ∀ o, (M.update V e o).card = ((k o).map (leaves h)).getD 0 := by
110         intro o
111         cases ho : k o with
112         | none =>
113           have he : M.update V e o = ∅ := by simpa only [ho] using ht.2 o
114           simp only [he,card_empty,Option.map_none,Option.getD_none]
115         | some u => exact ih _ u (by simpa only [ho] using ht.2 o)
116       rw [binary_card_split M s V e,branch false,branch true]
117       rfl
118 
119 /-- Every redundant unary query increases installed storage by exactly one record. -/
120 theorem records_exact (M : Model X E Bool C Unit) (s : Scope M)
121     (h : ℕ) (V : Finset X) (t : Tree E Bool C h) (ht : M.Valid h V t) :
122     (M.profile h V t).2 = 2 * V.card - 1 + unary h t := by
123   have hc := cases_eq_leaves M s h V t ht
124   have hr := records_identity h t (valid_live M h V t ht)
125   have hn : 0 < V.card := Finset.card_pos.mpr (M.valid_nonempty ht)
126   rw [M.profile_records]
127   omega
128 
129 /-- Minimum literal storage excludes all unary nodes in this scope. -/
130 theorem minimum_records_iff_no_unary (M : Model X E Bool C Unit) (s : Scope M)
131     (h : ℕ) (V : Finset X) (t : Tree E Bool C h) (ht : M.Valid h V t) :
132     (M.profile h V t).2 = 2 * V.card - 1 ↔ unary h t = 0 := by
133   rw [records_exact M s h V t ht]
134   omega
135 
136 /-- Under unit costs, the full worst-case work is actual query depth plus repair. -/
137 theorem work_eq_depth_succ (M : Model X E Bool C Unit) (s : Scope M)
138     (h : ℕ) (V : Finset X) (t : Tree E Bool C h) (ht : M.Valid h V t) :
139     (M.profile h V t).1 () = 1 + depth h t := by
140   induction h generalizing V with
141   | zero => exact s.terminal_cost t V ht.1
142   | succ h ih =>
143     cases t with
144     | inl c => exact s.terminal_cost c V ht.1
145     | inr ek =>
146       obtain ⟨e,k⟩ := ek
147       have hf := ht.2 false
148       have hg := ht.2 true
149       have live := (valid_live M (h+1) V (.inr (e,k)) ht).1
150       change M.stepCost e () + _ = 1 + depth (h+1) (.inr (e,k))
151       rw [s.query_cost e]
152       cases he : k false with
153       | none =>
154         cases hgk : k true with
155         | none => simp only [he,hgk,ne_eq,not_true_eq_false,or_self] at live
156         | some r =>
157           have hr := ih _ r (by simpa only [hgk] using hg)
158           simp [depth,he,hgk,Model.optional,Fintype.univ_bool,hr]
159       | some l =>
160         have hl := ih _ l (by simpa only [he] using hf)
161         cases hgk : k true with
162         | none =>
163           simp [depth,he,hgk,Model.optional,Fintype.univ_bool,hl]
164         | some r =>
165           have hr := ih _ r (by simpa only [hgk] using hg)
166           simp only [depth,he,hgk,Option.map_some,Option.getD_some,Model.optional,
167             Fintype.univ_bool,Finset.sup_insert,Finset.sup_singleton,hr,hl]
168           omega
169 
170 /-- General lower bounds, including actual depth and literal unary records. -/
171 theorem binary_lower_bounds (M : Model X E Bool C Unit) (s : Scope M)
172     (h : ℕ) (V : Finset X) (t : Tree E Bool C h) (ht : M.Valid h V t) :
173     Nat.clog 2 V.card ≤ depth h t ∧
174     1 + Nat.clog 2 V.card ≤ (M.profile h V t).1 () ∧
175     2 * V.card - 1 ≤ (M.profile h V t).2 := by
176   have hc := cases_le_leaves M s h V t ht
177   have hd := Nat.clog_le_of_le_pow (hc.trans (leaves_le_pow_depth h t))
178   refine ⟨hd,?_,?_⟩
179   · rw [work_eq_depth_succ M s h V t ht]
180     exact Nat.add_le_add_left hd 1
181   · rw [M.profile_records]
182     have hr := records_lower h t (valid_live M h V t ht)
183     omega
184 
185 /-- No controller can compensate for an insufficient experiment horizon. -/
186 theorem impossible_below_information_depth (M : Model X E Bool C Unit) (s : Scope M)
187     (h : ℕ) (V : Finset X) (hh : h < Nat.clog 2 V.card) :
188     ¬ ∃ t : Tree E Bool C h, M.Valid h V t := by
189   rintro ⟨t,ht⟩
190   exact (not_le_of_gt hh) ((binary_lower_bounds M s h V t ht).1.trans (depth_le_horizon h t))
191 
192 /-- Coordinatewise unavoidable work and storage; no assumption that they are attainable. -/
193 def lowerProfile (n : ℕ) : Profile Unit := (fun _ => 1 + Nat.clog 2 n, 2*n-1)
194 
195 theorem lowerProfile_le (M : Model X E Bool C Unit) (s : Scope M)
196     (h : ℕ) (V : Finset X) (t : Tree E Bool C h) (ht : M.Valid h V t) :
197     lowerProfile V.card ≤ M.profile h V t := by
198   have hb := binary_lower_bounds M s h V t ht
199   refine ⟨?_,hb.2.2⟩
200   intro r
201   cases r
202   exact hb.2.1
203 
204 variable [Fintype E] [Fintype C]
205 
206 /-- Core 5.3: a VALID candidate meeting BOTH bounds closes the exact Pareto search. -/
207 theorem checked_candidate_closes_frontier (M : Model X E Bool C Unit) (s : Scope M)
208     (h : ℕ) (V : Finset X) (t : Tree E Bool C h) (ht : M.Valid h V t)
209     (hw : (M.profile h V t).1 () = 1 + Nat.clog 2 V.card)
210     (hm : (M.profile h V t).2 = 2 * V.card - 1) :
211     M.solve h V = {lowerProfile V.card} := by
212   classical
213   have he : M.profile h V t = lowerProfile V.card := by
214     apply Prod.ext
215     · funext r; cases r; exact hw
216     · exact hm
217   have hs : lowerProfile V.card ∈ M.solve h V := by
218     apply (M.exact_frontier h V _).mpr
219     exact ⟨⟨t,ht,he⟩,fun u hu _ => lowerProfile_le M s h V u hu⟩
220   ext p
221   simp only [mem_singleton]
222   constructor
223   · intro hp
224     obtain ⟨u,hu,hup⟩ := M.solve_witness h V p hp
225     have hl : lowerProfile V.card ≤ p := hup ▸ lowerProfile_le M s h V u hu
226     exact le_antisymm (M.solve_antichain h V hp hs hl) hl
227   · rintro rfl; exact hs
228 
229 /-- Early return agrees with the actual executable profile recurrence. -/
230 theorem checked_candidate_closes_compute (M : Model X E Bool C Unit) (s : Scope M)
231     (h : ℕ) (V : Finset X) (t : Tree E Bool C h) (ht : M.Valid h V t)
232     (hw : (M.profile h V t).1 () = 1 + Nat.clog 2 V.card)
233     (hm : (M.profile h V t).2 = 2 * V.card - 1) :
234     M.compute h V = {lowerProfile V.card} := by
235   rw [M.compute_eq_solve]
236   exact checked_candidate_closes_frontier M s h V t ht hw hm
237 
238 /-- A data-only certificate gate; a false result means no certificate, not infeasibility. -/
239 def checkCandidate (M : Model X E Bool C Unit) (h : ℕ) (V : Finset X)
240     (t : Tree E Bool C h) : Bool :=
241   decide (M.Valid h V t ∧ M.profile h V t = lowerProfile V.card)
242 
243 omit [Fintype E] [Fintype C] in
244 theorem checkCandidate_iff (M : Model X E Bool C Unit) (h : ℕ) (V : Finset X)
245     (t : Tree E Bool C h) : checkCandidate M h V t = true ↔
246       M.Valid h V t ∧ M.profile h V t = lowerProfile V.card := by
247   simp only [checkCandidate,decide_eq_true_eq]
248 
249 /-- The executable certificate does not run the exhaustive profile synthesizer. -/
250 theorem checked_early_return (M : Model X E Bool C Unit) (s : Scope M)
251     (h : ℕ) (V : Finset X) (t : Tree E Bool C h)
252     (hc : checkCandidate M h V t = true) : M.compute h V = {lowerProfile V.card} := by
253   obtain ⟨hv,hp⟩ := (checkCandidate_iff M h V t).mp hc
254   apply checked_candidate_closes_compute M s h V t hv
255   · exact congrArg (fun p : Profile Unit => p.1 ()) hp
256   · exact congrArg Prod.snd hp
257 
258 /-- Any larger allowed horizon has the same frontier once both bounds are attained. -/
259 theorem closed_frontier_all_larger_horizons (M : Model X E Bool C Unit) (s : Scope M)
260     (h : ℕ) (V : Finset X) (t : Tree E Bool C h)
261     (hc : checkCandidate M h V t = true) (n : ℕ) :
262     M.solve (h+n) V = {lowerProfile V.card} := by
263   obtain ⟨hv,hp⟩ := (checkCandidate_iff M h V t).mp hc
264   obtain ⟨u,hu,hup⟩ := M.pad_horizon h n V t hv
265   have he := hup.trans hp
266   exact checked_candidate_closes_frontier M s (h+n) V u hu
267     (congrArg (fun p : Profile Unit => p.1 ()) he) (congrArg Prod.snd he)
268 
269 end Komorebi.MachineTheory.BinaryDiagnosis

Back to source controls