costUniverse_classifier
plain-language theorem explainer
Every claim in the Law-of-Logic forcing closure of the cost-layer universe is classified: the sole claim (that an admissible recognition cost equals the canonical J-cost) is forced. Maximal-forcing certificates for the cost layer cite this totality result. The proof collapses the claim to the singleton and reuses the already-proved forced status of J-uniqueness.
Claim. For every reality claim $C$ about candidate recognition costs $F:\mathbb{R}\to\mathbb{R}$ in the cost-layer universe, if $C$ lies in the forcing closure generated by the Law of Logic, then $C$ admits a claim classification: either forced under every admissible cost, or independent. Here the only claim in scope is "$F$ equals the canonical cost $J$ on $\mathbb{R}_{>0}$", and it is forced.
background
This module is the first concrete maximal-forcing universe. The realization carrier is a candidate recognition cost $F:\mathbb{R}\to\mathbb{R}$. Admissibility is the conjunction of the five Law-of-Logic gates on costs (reciprocal symmetry, normalization, the Recognition Composition Law, calibration, continuity), with the Aczel smoothness package supplied by a proved instance rather than an extra hypothesis.
The single 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 unique cost forced by T5. A claim is in closure when it belongs to the forcing closure of a primitive (here the Law of Logic) over the universe. Claim classification is the inductive Prop with constructors forced (holds in every admissible realization) and independent (two admissible realizations disagree).
Upstream, Phase 2.1 already discharges that the J-equality claim is forced by wrapping the published uniqueness theorem that the Law of Logic forces $J$.
proof idea
Tactic proof in five steps. Introduce the claim $C$ and the in-closure hypothesis. From in-closure, $C$ is a member of the universe's claim set; that set is a singleton, so membership forces $C$ equal to the J-equality claim. Substitute that equality. Finish by applying the forced constructor of claim classification to the already-established result that the J-equality claim is forced under cost-layer admissibility.
why it matters
This is the classifier half of a real MaximalClosureCert for the cost-layer universe. Downstream, costUniverseCert packages it as classifies := costUniverse_classifier, which discharges maximal forcing closure unconditionally for this universe: every claim in the closure is classified.
Framework-wise it closes Phase 1 + Phase 2.1 of maximal forcing by rooting the scaffold in a published, sorry-free uniqueness theorem (Law of Logic forces $J$) rather than a fresh assumption. That uniqueness is the T5 landmark in the forcing chain and the fixed point of the Recognition Composition Law. The pattern proved end-to-end is: a real RS theorem becomes a forced invariant over an admissible class. Later phases tighten the admissibility gate; this lemma only needs the present cost-layer universe.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.