CostCeilingCert
plain-language theorem explainer
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.
Claim. A 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.