costUniverseCert
plain-language theorem explainer
Packages a maximal-closure certificate for the cost-layer universe under the Law of Logic: every claim in that universe's closure is classified. Anyone citing the end-to-end cost forcing (admissible costs forced to equal J) uses this as the discharge token. The body is a one-field structure instance that installs the existing cost-universe classifier.
Claim. There is a maximal-closure certificate for the cost-layer universe under the Law of Logic: every claim in the closure of that universe is classified. In particular, the forcing-closure property holds unconditionally for the cost universe.
background
This module is the first concrete instantiation of the maximal-forcing scaffold. The carrier is a candidate recognition cost $F:\mathbb{R}\to\mathbb{R}$. Admissibility is the conjunction of the five Law-of-Logic gate conditions on costs: reciprocal symmetry, normalization, the Recognition Composition Law, calibration, and continuity. The Aczel smoothness package is supplied by a proved instance, not an extra hypothesis.
The claim under closure is that $F$ equals the canonical cost $J$ on the positive reals, where $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$). The cost universe is the admissible class of such $F$ together with that equality claim. Upstream, Phase 2.1 already wraps the published uniqueness theorem so that "equals $J$" is forced over the tightened admissible class.
A MaximalClosureCert is the bookkeeping object that records a classifier for every claim in a universe's closure, discharging the generic maximal-forcing-closure obligation for that universe.
proof idea
One-field structure instance. The certificate type asks only for a classifier; the definition sets that field to the already-constructed cost-universe classifier. No new arithmetic or uniqueness argument is performed here; the work sits in the classifier and in the upstream forcing of $J$ over the admissible class.
why it matters
This is the discharge token that makes the cost-layer universe a finished maximal-forcing instance rather than a scaffold. The module roots the program in an existing sorry-free uniqueness theorem (Law of Logic forces $J$) instead of a fresh assumption, and this certificate is what lets maximal_forcing_closure fire unconditionally for that universe.
In the Recognition framework it sits at the cost end of the forcing chain: T5 $J$-uniqueness and the Recognition Composition Law are the mathematical content being packaged. The surrounding notes stress that the $L_0\to L_{\mathrm{cost}}$ gate tightening is effective, not cosmetic: over the loose continuous class, "equals $J$" is independent (canonical $J$ satisfies it; constant zero does not), so the gates genuinely force $J$. No downstream consumers are wired yet in the graph; the declaration closes the cost-universe side of the maximal-forcing pattern.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.