calibrated_character_forces_J
plain-language theorem explainer
Any ratio character calibrated at a single orbit point p generates the canonical J-cost at p. Foundation work on continuum cost uniqueness cites this local forcing step. The proof is a one-line term applying character rigidity under the calibration hypothesis.
Claim. Let $\chi$ be a ratio character on ratio orbits. If $\chi$ is calibrated at a point $p$ (i.e. $\chi(p)$ agrees with $p$), then the cost generated by $\chi$ at $p$ equals the canonical orbit cost $J(p)$.
background
In the Primitive Recognition Calculus continuum layer, costs live on ratio orbits. A ratio character $\chi$ is a structure-preserving map on those orbits; the cost it induces at a point is costFromCharacter. The canonical comparison cost on an orbit is the J-cost $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), written here as the orbit embedding of $p$.
Calibration at $p$ means the character agrees with the identity orbit at that point ($\chi(p)\approx p$). Upstream cost axioms fix the second-derivative normalization at the log-origin so that a calibrated functional cannot float by a free scale. The Recognition Composition Law and T5 J-uniqueness in the forcing chain make $J$ the unique symmetric solution once that normalization is pinned.
This module studies how local calibration on the discrete ratio skeleton forces the completed continuum cost to be exactly $J$.
proof idea
One-line term proof: apply the rigidity lemma for costs from characters (costFromCharacter_rigid) to the character hypothesis and the calibration-at-$p$ hypothesis. No extra algebraic rearrangement; rigidity already concludes cross-equality of the generated cost with the canonical orbit cost $J(p)$.
why it matters
Local calibrated forcing is the seed for uniqueness of the recognition cost on completions: once a character matches the identity at one orbit point, its induced cost is forced to $J$ there. That is the continuum-facing form of T5 J-uniqueness in the Unified Forcing Chain.
Sibling results in the same module extend the picture: calibration propagates along the cyclic subgroup generated by $p$ (powers and inverse), and global identities on the completion are recovered from one-point calibration. Even with no recorded downstream users yet, the declaration is the pointwise hinge those completion theorems need before claiming a forced continuum $J$.
It does not by itself settle the full eight-tick or $D=3$ steps; it only locks the cost functional at a calibrated orbit point.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.