structure
definition
CostCeilingCert
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.URCGenerators.LNALCerts on GitHub at line 149.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
146 { ok := rep.ok, errors := rep.errors }
147
148/-- Cost ceiling certificate (|net GIVE−REGIVE| ≤ 4 per 8‑tick window). -/
149structure CostCeilingCert where
150 ok : Bool
151 errors : List String := []
152deriving Repr
153
154@[simp] def CostCeilingCert.verified (_c : CostCeilingCert) : Prop :=
155 -- At 8k boundaries, window cost is bounded (indeed zero)
156 (∀ (P : IndisputableMonolith.LNAL.LProgram)
157 (s : IndisputableMonolith.LNAL.LState),
158 IndisputableMonolith.LNAL.EightTickInvariant P s →
159 ∀ k, Int.abs (IndisputableMonolith.LNAL.windowCostAt P s (8 * k)) ≤ 4)
160 ∧
161 -- There exists r ≤ 7 such that rotated boundaries are also bounded
162 (∀ (P : IndisputableMonolith.LNAL.LProgram)
163 (s : IndisputableMonolith.LNAL.LState),
164 IndisputableMonolith.LNAL.EightTickInvariant P s →
165 ∃ r, r ≤ 7 ∧ ∀ k,
166 Int.abs (IndisputableMonolith.LNAL.windowCostAt P s (r + 8 * k)) ≤ 4)
167
168@[simp] theorem CostCeilingCert.verified_any (c : CostCeilingCert) :
169 CostCeilingCert.verified c := by
170 constructor
171 · intro P s H k; simpa using
172 (IndisputableMonolith.LNAL.cost_ceiling_window_boundaries (P:=P) (s:=s) H k)
173 · intro P s H; simpa using
174 (IndisputableMonolith.LNAL.cost_ceiling_window_rotated (P:=P) (s:=s) H)
175
176def CostCeilingCert.fromSource (src : String) : CostCeilingCert :=
177 let parsed := parseProgramFull src
178 let emptyPhi : PhiIR.PhiAnalysis := { literals := #[], errors := #[], duplicateNames := [] }
179 let emptyPackets : PhiIR.PacketAnalysis := {}