forced_J_on_completion
plain-language theorem explainer
On the continuum completion R_δ, any ratio character calibrated at a single point p is forced to generate the canonical cost J(p)=(p+p⁻¹)/2−1, unique up to reciprocal gauge. Calibration propagates to p² and p⁻¹. Cite this as the continuum-level J-uniqueness capstone (T5 on RatioOrbit). The proof is a five-component term packing rigidity, reciprocal symmetry, cyclic propagation, and the rational display formula.
Claim. Let $\chi$ be a PRC ratio character on ratio orbits, calibrated at a point $p$. Then: (1) the cost generated by $\chi$ at $p$ equals the canonical orbit cost $J(p)$; (2) $J(p)\simeq J(p^{-1})$ (reciprocal gauge); (3) calibration at $p$ forces calibration at $p^{2}$ and at $p^{-1}$; (4) on the rational display, $J(p)=(p+p^{-1})/2-1$.
background
The module works on the quotient-native carrier RatioOrbit for the continuum completion $R_\delta$. The continuum itself is a named commitment (not forced by distinction; cf. RealLineNonNativity). What is forced on that completion is the recognition cost.
A PRC ratio character $\chi$ is a structure-preserving map on ratio orbits. Character calibration at $p$ is a one-point datum fixing the cost generated by $\chi$ against the canonical orbit cost. The canonical cost on orbits is onRatioOrbit, which on the rational display equals $(q+q^{-1})/2-1$. Reciprocal symmetry of this cost is the one-parameter gauge: $\chi=\mathrm{id}$ and $\chi=\mathrm{recip}$ generate the same cost.
Upstream, character rigidity and prime-calibration propagation supply the local forcing and the step from one calibrated point to $p^{2}$ and $p^{-1}$. The Recognition Composition Law and T5 J-uniqueness in the forcing chain are the global landmarks this continuum statement instantiates on RatioOrbit, choice-free.
proof idea
Pure term proof: a 5-tuple of prior lemmas, no tactics.
costFromCharacter_rigidunder the character and calibration hypotheses gives forcing: cost-from-$\chi$ at $p$ cross-equals the canonical orbit cost.reciprocal_symmetric pgives the gauge $J(p)\simeq J(p^{-1})$. 3–4. The two projections ofprime_calibration_forces_identity_on_directionpush calibration from $p$ to $p\cdot p$ and to $p^{-1}$.onRatioOrbit_toRat psupplies the rational-display identity $J(p)=(p+p^{-1})/2-1$.
No Classical.choice is pulled in; the field-display link to Cost.Jcost on $\mathbb{R}$ is deliberately not routed here.
why it matters
Doc-comment labels this THE CAPSTONE of continuum cost forcing: reciprocal-symmetric RCL, normalization, and one calibration datum force $J(x)=(x+1/x)/2-1$ on $R_\delta$, unique up to the proved reciprocal gauge. That is T5 (J-uniqueness) realized on the quotient-native completion carrier.
No used_by edges yet; sibling existence (forced_cost_exists_on_completion) and the open target target_OnePointCalibrationForcesGlobalIdentity (all-primes / one-point calibration at two forcing global identity) are the natural consumers. The theorem closes local cyclic propagation and the formula on RatioOrbit while leaving global identity-from-one-point as the named open step.
Framework landmarks: T5 J-formula, RCL, and the deliberate separation between forcing the cost on the completion versus forcing the continuum itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.