PrefixAdmission.lean

1 import MachineTheory.PrefixSemantics
2 import MachineTheory.BinaryCertificate
3 
4 /-!
5 # An explicit admission boundary for capacity-pruned search
6 
7 The outer `none` rejects the scope certificate. A completed inner `none` means
8 finite-depth infeasibility ONLY after all scope, menu and row conditions pass.
9 The exhaustive finite guard is itself preparation, not an uncharged cheap test.
10 -/
11 namespace Komorebi.MachineTheory.OrderedCompiler
12 open HardInquiry BinaryDiagnosis
13 variable {X E C : Type} [Fintype X] [DecidableEq X]
14   [Fintype E] [DecidableEq E] [Fintype C] [DecidableEq C]
15 
16 def guard (M : Model X E Bool C Unit) (es : List E) (cs : List C) (xs : List X) : Bool :=
17   checkScope M && decide (xs.Nodup ∧ (∀ e,e∈es) ∧ ∀ c,c∈cs)
18 
19 theorem guard_iff (M : Model X E Bool C Unit) (es : List E) (cs : List C) (xs : List X) :
20     guard M es cs xs=true ↔ Scope M ∧ xs.Nodup ∧ (∀ e,e∈es) ∧ ∀ c,c∈cs := by
21   simp only [guard,Bool.and_eq_true_iff,checkScope_iff,decide_eq_true_eq]
22 
23 def checkedSearch (M : Model X E Bool C Unit) (es : List E) (cs : List C)
24     (h : ℕ) (xs : List X) : Option (Run (Tree E Bool C h)) :=
25   if guard M es cs xs then some (search streamScanner M es cs h xs) else none
26 
27 theorem admitted_contract (M : Model X E Bool C Unit) (es : List E) (cs : List C)
28     (h : ℕ) (xs : List X) (r : Run (Tree E Bool C h))
29     (hr : checkedSearch M es cs h xs=some r) :
30     Scope M ∧ xs.Nodup ∧ (∀ e,e∈es) ∧ (∀ c,c∈cs) ∧ r=search streamScanner M es cs h xs := by
31   unfold checkedSearch at hr
32   split at hr
33   · have hg := (guard_iff M es cs xs).mp ‹guard M es cs xs=true›
34     exact ⟨hg.1,hg.2.1,hg.2.2.1,hg.2.2.2,(Option.some.inj hr).symm⟩
35   · cases hr
36 
37 /-- This is about a completed admitted search, not a timeout or a rejected model. -/
38 theorem admitted_search_sound_complete (M : Model X E Bool C Unit) (es : List E) (cs : List C)
39     (h : ℕ) (xs : List X) (r : Run (Tree E Bool C h))
40     (hr : checkedSearch M es cs h xs=some r) :
41     (∀ t,r.answer=some t → M.Valid h xs.toFinset t) ∧
42     (r.answer=none ↔ ¬ ∃ t : Tree E Bool C h,M.Valid h xs.toFinset t) := by
43   obtain ⟨hs,hn,he,hc,hh⟩ := admitted_contract M es cs h xs r hr
44   rw [hh]
45   exact streaming_sound_complete M hs es cs he hc h xs hn
46 
47 theorem admitted_search_preserves_reference (M : Model X E Bool C Unit) (es : List E) (cs : List C)
48     (h : ℕ) (xs : List X) (r : Run (Tree E Bool C h))
49     (hr : checkedSearch M es cs h xs=some r) :
50     r.answer=(search fullScanner M es cs h xs).answer ∧
51     r.reads≤(search fullScanner M es cs h xs).reads := by
52   obtain ⟨_,_,_,_,hh⟩ := admitted_contract M es cs h xs r hr
53   rw [hh]
54   exact streaming_preserves_search M es cs h xs
55 
56 
57 /-- The new ordered compiler and the unchanged Pareto synthesizer agree on finite feasibility. -/
58 theorem admitted_failure_iff_empty_frontier (M : Model X E Bool C Unit) (es : List E) (cs : List C)
59     (h : ℕ) (xs : List X) (r : Run (Tree E Bool C h))
60     (hr : checkedSearch M es cs h xs=some r) :
61     r.answer=none ↔ M.compute h xs.toFinset=∅ := by
62   rw [M.compute_eq_solve]
63   exact (admitted_search_sound_complete M es cs h xs r hr).2.trans
64     (M.no_tree_iff_empty h xs.toFinset)
65 
66 end Komorebi.MachineTheory.OrderedCompiler
67 

Back to source controls