isJClaim
plain-language theorem explainer
Packages the cost-layer assertion that a candidate recognition cost F equals the canonical J-cost on (0,∞) as a RealityClaim on functions ℝ→ℝ. Anyone citing the maximal-forcing cost universe, ForcedInvariant register, or Phase 2.1 uniqueness wrap will reference this claim object. It is a pure structure definition: label plus the pointwise equality predicate; no proof work.
Claim. The cost-layer reality claim on candidate costs $F:\mathbb{R}\to\mathbb{R}$ asserts that $F(x)=J(x)$ for every $x>0$, where $J(x)=(x+x^{-1})/2-1$ is the canonical recognition cost.
background
Maximal forcing in this module is the first concrete ClaimUniverse: realizations are candidate recognition costs $F:\mathbb{R}\to\mathbb{R}$, admissibility is the five-gate Law-of-Logic class (reciprocal symmetry, normalization, Recognition Composition Law, calibration, continuity), and the single claim under closure is equality with the canonical cost.
A RealityClaim is a pair of audit label and predicate holds on realizations. The canonical cost is $J(x)=(x+x^{-1})/2-1$ (also $\cosh(\log x)-1$), the unique function forced by those gates; this is the T5 J-uniqueness landmark and the content of the Recognition Composition Law identity $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$.
Upstream, Cost.Jcost and the cosmology Jcost aliases supply the same formula. The AczelSmoothnessPackage instance from Cost.AczelProof is already proved, so the gate class is not an extra hypothesis.
proof idea
Definition only: fills the RealityClaim structure on carrier $\mathbb{R}\to\mathbb{R}$ by setting the audit label to the string "F = Jcost on (0,∞)" and the holds predicate to pointwise equality $F,x=\mathrm{Cost.Jcost},x$ for all $x>0$. No tactics, no lemmas applied.
why it matters
This is the sole claim object of the cost-layer universe. Downstream, costUniverse sets claims := {isJClaim}; forced_isJ proves Forced Lcost.admissible isJClaim by wrapping law_of_logic_forces_jcost (Phase 2.1); isJClaim_in_closure and isJForcedInvariant place it in the ForcedInvariant register as the first populated Phase 2 slot; costUniverse_classifier and costUniverseCert then classify the whole closure and discharge maximal_forcing_closure for this universe.
Framework-wise it is the claim form of T5 J-uniqueness: once the five gates hold, F must be J on the positive reals. It roots maximal forcing in a published sorry-free uniqueness theorem rather than a fresh axiom, and is the claim against which L0-to-Lcost gate tightening is later shown to be effective (isJ_independent_over_L0, tightening_L0_Lcost_effective).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.