isJClaim_in_closure
plain-language theorem explainer
The uniqueness claim "candidate cost F equals canonical J on (0,∞)" sits in the forcing closure of the cost-layer claim universe, rooted at the Law-of-Logic primitive. Anyone assembling a ForcedInvariant for the cost layer cites this membership. The proof is a one-line set-membership check: the universe's claim set is the singleton {isJClaim}.
Claim. The reality claim "$F = J$ on $(0,\infty)$" belongs to the forcing closure of the cost-layer claim universe under the Law-of-Logic primitive. Equivalently, that claim is an element of the universe's claim set, which is defined to be the singleton containing exactly this uniqueness statement.
background
This module is the first concrete instantiation 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, Recognition Composition Law, calibration, continuity) supplied by the proved Aczel smoothness package, not an extra hypothesis.
The claim under study asserts that $F$ equals the canonical cost $J$ (also written $J(x)=(x+x^{-1})/2-1$) on the positive reals. The cost-layer claim universe packages realizations as functions $\mathbb{R}\to\mathbb{R}$, admissibility as the gate class, and claims as the singleton containing that uniqueness statement.
InClosure is the scope predicate: a claim is in scope for maximal closure from a primitive when it lies in the forcing closure generated by that primitive over the universe. The primitive here is Law-of-Logic (as opposed to bare distinction).
proof idea
Unfold InClosure to membership of the claim in the forcing closure of the cost universe. By definition of that universe, the claim set is exactly the singleton containing the uniqueness claim. The goal therefore reduces to singleton membership, discharged by Set.mem_singleton. No uniqueness or forcing lemma is invoked; this is pure structural membership.
why it matters
This is the closure half of the first populated Phase-2 forced-register slot. Downstream, isJForcedInvariant packages the uniqueness claim with this membership proof and the separate forcedness proof (wrapping the published Law-of-Logic forces $J$ theorem) into a ForcedInvariant over the admissible cost class.
That pattern is the scaffold's end-to-end demo: a real, sorry-free RS uniqueness result (T5 J-uniqueness / RCL gate class) becomes a forced invariant rather than a fresh assumption. The cost universe classifier and independence-over-$L_0$ results sit beside it; this lemma only certifies that the claim is in scope so the register entry typechecks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.