forced_isJ
plain-language theorem explainer
Over the gate-admissible class of recognition costs, equality with the canonical J-cost is forced: every F that is reciprocal, normalized, RCL-compliant, calibrated, and continuous equals J on the positive reals. Cited by the cost-layer forced register and by the L0-to-Lcost tightening legitimacy theorem. Proof is a direct unpack-and-apply of the published Law of Logic uniqueness result, with Aczél smoothness supplied by an existing instance.
Claim. Every candidate cost $F:\mathbb{R}\to\mathbb{R}$ that is reciprocal, normalized, satisfies the Recognition Composition Law, is calibrated, and is continuous obeys $F(x)=J(x)$ for all $x>0$, where $J(x)=(x+x^{-1})/2-1$. Equivalently, the claim "$F$ equals the canonical cost on $(0,\infty)$" is forced on the gate-admissible class.
background
This module is the first concrete realization of the maximal-forcing scaffold. Realizations are candidate recognition costs $F:\mathbb{R}\to\mathbb{R}$. Admissibility is the five-gate class: reciprocal symmetry, normalization, the Recognition Composition Law (RCL), calibration, and continuity. The Aczél smoothness package is a proved instance from Cost.AczelProof, not an extra hypothesis.
The claim under study asserts that $F$ equals the canonical cost $J$ on the positive reals, with $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$). In the forcing primitive, a claim is forced on an admissible class when it holds in every admissible realization.
Upstream, the Law of Logic cost theorem states that $J$ is the unique reciprocal cost satisfying RCL, normalization, calibration, and continuity (using the global Aczél axiom internally, with no caller-supplied regularity parameters). That uniqueness is exactly what the gate class encodes.
proof idea
One-line wrapper around the published uniqueness theorem. Introduce an arbitrary gate-admissible $F$ and a positive $x$. Unpack admissibility into the five gate hypotheses (reciprocal, normalized, RCL, calibrated, continuous). Feed those five facts, together with the ambient Aczél smoothness instance, into law_of_logic_forces_jcost, which returns $F(x)=J(x)$. No new algebraic content.
why it matters
Phase 2.1 of the cost-layer realization: it discharges forcedness of "equals $J$" over the gate class, turning a real RS uniqueness theorem into a ForcedInvariant entry. Downstream it populates the first forced-register slot (isJForcedInvariant), supplies the forced half of the L0-to-Lcost legitimacy pair (tightening_L0_Lcost_effective: independent over the loose class, forced over the gate class), and lets the cost-universe classifier mark its single claim as forced.
Framework landmark: this is the forcing-register face of T5 J-uniqueness and of the RCL functional equation. It shows the maximal-forcing pattern end to end without fresh axioms, rooting the scaffold in published, sorry-free content rather than a new assumption.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.