isJForcedInvariant
plain-language theorem explainer
Packages the claim that every admissible recognition cost equals the canonical J-cost as a ForcedInvariant under the Law-of-Logic primitive over the cost-layer universe. First populated slot of the Phase 2 forced register. Anyone assembling maximal-forcing certificates or citing cost uniqueness in register form would cite it. The body is a three-field structure instance wiring already-proved components.
Claim. The claim that $F=J$ on $\mathbb{R}_{>0}$, together with a proof that it lies in the closure of the cost-layer claim universe rooted at the Law-of-Logic primitive and a proof that it is forced over the gate class of admissible costs, constitutes a forced invariant for that universe.
background
The module is the first concrete instantiation of the maximal-forcing scaffold. Realizations are candidate costs $F:\mathbb{R}\to\mathbb{R}$. Admissibility is the five-gate class imposed by the Law of Logic: reciprocal symmetry, normalization, the Recognition Composition Law, calibration, and continuity. The claim under study is that $F$ equals the canonical cost $J(x)=(x+x^{-1})/2-1$ on the positive reals.
A forced invariant is a closure claim equipped with a proof of forcedness: a RealityClaim on the universe's realizations, a witness that the claim sits in the primitive's closure, and a proof that every admissible realization satisfies the claim. The cost-layer universe takes realizations $\mathbb{R}\to\mathbb{R}$, admissibility the gate class, and its singleton claim set ${F=J}$.
Upstream, forced_isJ already wraps the published uniqueness theorem law_of_logic_forces_jcost (with the Aczel smoothness package supplied by Cost.AczelProof, not as a fresh hypothesis). The companion lemma places the claim in the universe closure.
proof idea
One-line structure instance. The three fields of ForcedInvariant are filled by name: the claim is the existing isJClaim; membership in the closure is isJClaim_in_closure; forcedness is forced_isJ. No new reasoning is introduced. The heavy lifting sits in forced_isJ, which unpacks the five gate hypotheses and applies law_of_logic_forces_jcost pointwise on $\mathbb{R}_{>0}$.
why it matters
This is the first populated entry of the Phase 2 forced register: a real, sorry-free RS uniqueness theorem is reified as a ForcedInvariant over an admissible class. It closes the Phase 1 + Phase 2.1 pattern end to end for the cost layer, rooting maximal forcing in published J-uniqueness (framework landmark T5: $J(x)=\cosh(\log x)-1$) rather than a fresh assumption.
The module doc states the intent explicitly: prove the forced-register pattern by wrapping law_of_logic_forces_jcost. Downstream the register can be classified as total over its closure (the transitional classifier and certificate siblings sit beside this definition). No used_by edges are recorded yet; the declaration is the seed entry others will consume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.