CostCeilingCert
The CostCeilingCert structure records whether an LNAL program satisfies the absolute net cost bound of 4 per eight-tick window under the eight-tick invariant. LNAL developers and URC report generators cite it when certifying token-unit preservation in the Recognition Science VM. The verified property is established by a one-line wrapper that invokes the boundary and rotated-window cost lemmas.
claimA structure $C$ with boolean field $ok$ and error list such that $C.ok$ holds precisely when, for every LProgram $P$ and LState $s$ obeying the eight-tick invariant, the window cost at every multiple of 8 satisfies $|windowCostAt(P,s,8k)|≤4$, and there exists a rotation $r≤7$ with the same bound holding at every $r+8k$.
background
LNAL expresses Recognition Science programs whose execution respects the eight-tick octave (T7) via the EightTickInvariant. Cost is the J-functional of the multiplicative recognizer, reparametrized as $H(x)=J(x)+1$ in CostAlgebra; this $H$ converts the Recognition Composition Law into the d'Alembert equation $H(xy)+H(x/y)=2H(x)H(y)$. Upstream lemmas in MultiplicativeRecognizerL4 and ObserverForcing supply the derived cost of comparator events, while OptionAEmpiricalProgram and SimplicialLedger supply the collision-free and edge-length contexts used by the windowCostAt function.
proof idea
The structure is populated by fromSource, which runs parseProgramFull followed by staticChecks. The verified property is discharged by the theorem verified_any: the first conjunct applies cost_ceiling_window_boundaries to obtain the bound at 8k positions; the second conjunct applies cost_ceiling_window_rotated to produce the required rotation $r≤7$. Both steps are direct simpa reductions of the supplied lemmas.
why it matters in Recognition Science
CostCeilingCert is consumed by cost_ceiling_report, cost_ceiling_report_json and lnal_manifest_json in the LNALReports adapter, which emit the aggregate manifest for the URC engine. It supplies the cost-ceiling clause of the LNAL invariants bundle, closing the token δ-unit bound required by the eight-tick forcing chain (T7) and the J-cost functional equation. It leaves open the empirical check of the |net GIVE−REGIVE|≤4 bound against physical simulation data.
scope and limits
- Does not apply to LPrograms that fail the EightTickInvariant.
- Does not bound window costs at offsets other than the stated 8-tick lattice.
- Does not certify parsing success or absence of duplicate names.
- Does not extend the bound to continuous-time or non-discrete state spaces.
Lean usage
let cert := CostCeilingCert.fromSource src; if cert.ok then ... else ...formal statement (Lean)
149structure CostCeilingCert where
150 ok : Bool
151 errors : List String := []
proof body
Definition body.
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 := {}
180 let code := match parsed with
181 | .ok out => out.code
182 | .error _ => #[]
183 let phi := match parsed with
184 | .ok out => out.phi
185 | .error _ => emptyPhi
186 let packets := match parsed with
187 | .ok out => out.packets
188 | .error _ => emptyPackets
189 let rep := staticChecks code phi packets
190 { ok := rep.ok, errors := rep.errors }
191
192/-- SU(3) braid mask certificate: SU3Invariant preserved under lStep. -/