JMonotoneCert
plain-language theorem explainer
The declaration aliases the J-monotone per-window budget certificate from the core certificates module into the LNAL invariants bundle. LNAL compiler verification teams cite it when assembling token budget proofs under the recognition cost. Construction is a direct re-export of the verified property and source constructor with no added computation.
Claim. The J-monotone per-window budget certificate is the re-export of the core certificate, where the recognition cost $J(x) = (x + x^{-1})/2 - 1$ remains monotone across windows.
background
The LNAL invariants certificate bundles VM preservation and token δ-unit bound. The J function supplies the recognition cost used for budget monotonicity. Upstream, the bridge ratio is defined as $K = ϕ^{1/2}$ and the curvature functional satisfies $K(λ) = λ^2 / λ_rec^2 - 1$, vanishing at the recursive fixed point.
proof idea
One-line wrapper aliasing the J-monotone certificate, its verified property, and fromSource constructor directly from the certificates module.
why it matters
This declaration embeds the J-monotone certificate inside the LNAL invariants bundle, supporting the recognition composition law and T5 J-uniqueness step in the forcing chain. It supplies modular budget certification for URC generators without downstream uses listed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.