BinaryCertificate.lean

1 import MachineTheory.BinaryExecution
2 import Mathlib.Data.Fintype.Powerset
3 
4 /-!
5 # Finite admission of the complete binary certificate
6 
7 The guard checks actual model fields, including all finite support-dependent
8 terminal charges. It is not cheap by definition, and does not discover its table.
9 -/
10 namespace Komorebi.MachineTheory.BinaryDiagnosis
11 open HardInquiry Finset
12 variable {X E C : Type} [Fintype X] [DecidableEq X] [Fintype E] [Fintype C]
13 
14 def checkScope (M : Model X E Bool C Unit) : Bool :=
15   decide ((∀ e x, M.next e x = x) ∧
16     (∀ c x y, M.accept x c = true → M.accept y c = true → x = y) ∧
17     (∀ e, M.stepCost e () = 1) ∧
18     (∀ c V, V.Nonempty → M.terminalCost c V () = 1))
19 
20 theorem checkScope_iff (M : Model X E Bool C Unit) : checkScope M = true ↔ Scope M := by
21   simp only [checkScope,decide_eq_true_eq]
22   constructor
23   · rintro ⟨hi,hs,hq,ht⟩; exact ⟨hi,hs,hq,ht⟩
24   · intro s; exact ⟨s.immutable,s.singleton,s.query_cost,s.terminal_cost⟩
25 
26 /-- Nothing in the returned certificate supplies the hidden state or performs exhaustive synthesis. -/
27 def admissionCheck (M : Model X E Bool C Unit) (h : ℕ) (V : Finset X) (t : Tree E Bool C h) : Bool :=
28   checkScope M && checkCandidate M h V t
29 
30 theorem admitted_scope_and_candidate (M : Model X E Bool C Unit) (h : ℕ)
31     (V : Finset X) (t : Tree E Bool C h) (ha : admissionCheck M h V t = true) :
32     Scope M ∧ M.Valid h V t ∧ M.profile h V t = lowerProfile V.card := by
33   have hh := Bool.and_eq_true_iff.mp ha
34   exact ⟨(checkScope_iff M).mp hh.1,(checkCandidate_iff M h V t).mp hh.2⟩
35 
36 /-- A true complete gate certifies the entire computed frontier at the requested horizon. -/
37 theorem admitted_frontier (M : Model X E Bool C Unit) (h : ℕ)
38     (V : Finset X) (t : Tree E Bool C h) (ha : admissionCheck M h V t = true) :
39     M.compute h V = {lowerProfile V.card} := by
40   have hh := Bool.and_eq_true_iff.mp ha
41   exact checked_early_return M ((checkScope_iff M).mp hh.1) h V t hh.2
42 
43 /-- The same certificate establishes the frontier at every larger finite horizon. -/
44 theorem admitted_all_horizons (M : Model X E Bool C Unit) (h : ℕ)
45     (V : Finset X) (t : Tree E Bool C h) (ha : admissionCheck M h V t = true) (n : ℕ) :
46     M.solve (h+n) V = {lowerProfile V.card} := by
47   have hh := Bool.and_eq_true_iff.mp ha
48   exact closed_frontier_all_larger_horizons M ((checkScope_iff M).mp hh.1) h V t hh.2 n
49 
50 /-- Admission means that one same candidate satisfies every online/storage budget above it. -/
51 theorem admitted_budget (M : Model X E Bool C Unit) (h : ℕ)
52     (V : Finset X) (t : Tree E Bool C h) (ha : admissionCheck M h V t = true) (b : Profile Unit) :
53     (∃ u : Tree E Bool C h, M.Valid h V u ∧ M.profile h V u ≤ b) ↔
54       lowerProfile V.card ≤ b := by
55   rw [M.computed_budget_iff,admitted_frontier M h V t ha]
56   simp only [mem_singleton,exists_eq_left]
57 
58 end Komorebi.MachineTheory.BinaryDiagnosis

Back to source controls