calibrated_one
plain-language theorem explainer
Any PRC ratio character is automatically calibrated at the unit orbit: it acts as the identity there. Cost-uniqueness and character-rigidity arguments cite this as the base case before closing under products and reciprocals. The proof is a one-line projection of the character's unit field.
Claim. Let $\chi$ be a PRC ratio character on ratio orbits. Then $\chi$ is calibrated at the unit orbit: $\chi(1)$ is cross-equivalent to $1$ itself.
background
In the Primitive Recognition Calculus continuum layer, ratio orbits are the discrete multiplicative skeleton on which cost characters live. A PRC ratio character is a multiplicative map $\chi$ on those orbits obeying the unit, reciprocity, and related structural axioms of the PRC native cost package.
Calibration at an orbit $q$ means $\chi(q)$ is cross-equivalent to $q$: the character acts as the identity along that orbit direction. The module records that the single-point datum the PRC cost hypotheses actually carry is calibration at two; the unit orbit is the free base point forced by the character axioms alone.
Upstream cost language treats calibration as a normalization that pins curvature or a distinguished inconsistent configuration so uniqueness theorems can fire. Here the analogous pin is identity action on selected orbits before rigidity of the full character (and of the induced cost) is proved.
proof idea
One-line term proof: project the unit field of the PRC ratio character hypothesis. That field already states that $\chi$ fixes the unit orbit up to cross-equivalence, which is exactly the definition of calibration at one.
why it matters
This is the base calibration lemma in CharacterRigidityForcing. Sibling results close calibration under multiplication and reciprocity, then feed character-trace rigidity, cost-from-character rigidity, and the doubled-trace rigidity statements in the same module.
In the broader Recognition chain it supports the continuum reading of cost uniqueness: once characters are forced to the identity on a generating set of orbits, the induced cost matches the unique $J$-cost fixed by T5 and the Recognition Composition Law. The unit case costs nothing extra; it is the free anchor before the nontrivial two-point calibration hypothesis is used.
No downstream uses are recorded yet in the graph, so the lemma presently serves the local rigidity suite rather than a named parent theorem outside the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.