CharacterCalibratedAt
plain-language theorem explainer
A ratio character χ is calibrated at an orbit q when χ(q) is cross-equivalent to q, so χ acts as the identity on that orbit direction. Calibration at two is the single-point datum the PRC cost hypotheses actually carry. Rigidity and cost-uniqueness arguments cite this predicate to seed propagation from generators. The body is a one-line Prop alias of cross-equivalence.
Claim. A map $\chi$ from ratio orbits to ratio orbits is calibrated at an orbit $q$ when $\chi(q)$ is cross-equivalent to $q$: the signed-orbit cross-multiplication balance of numerators and denominators holds between $\chi(q)$ and $q$.
background
In the Primitive Recognition Calculus, rationals are carried as ratio orbits: a signed-orbit numerator over a nonzero distinction-nat denominator. Equality of displays is not definitional identity but cross-equivalence: two orbits $a,b$ satisfy the internal PRC relation when $a.\mathrm{num}\cdot b.\mathrm{den}$ balances $b.\mathrm{num}\cdot a.\mathrm{den}$ as signed orbits (K4.10).
A PRC ratio character is a map $\chi$ on ratio orbits that is a unit at the one-orbit and multiplicative up to cross-equivalence. It is the candidate factor in the d'Alembert factorization of a PRC cost, kept quotient-native so it never forces a choice of representatives.
This module sits in the continuum character-rigidity forcing layer: the goal is to show that a character calibrated at a generator (classically two) is forced to the identity character on the relevant orbit directions, collapsing the induced cost to the canonical J-cost.
proof idea
Pure definitional abbreviation. The predicate is exactly cross-equivalence of $\chi(q)$ with $q$; there is no proof obligation beyond unfolding. Downstream lemmas typically unfold this name and rewrite via the bridge from cross-equivalence to equality of verifier rational displays.
why it matters
This is the local calibration predicate that every rigidity lemma in the module is stated against. Closure under products, reciprocals, and squares (calibrated_mul, calibrated_recip, calibrated_square) and the unit case (calibrated_one, from the character unit axiom) turn a single-point datum into an identity character on a generated submonoid.
From calibration one obtains trace rigidity: the d'Alembert trace $\chi(p)+\chi(p)^{-1}$ collapses to $p+p^{-1}$, and the character-generated cost equals the canonical PRC cost on that point (character_trace_rigid, costFromCharacter_rigid). That cost is the continuum avatar of the unique J-cost $J(x)=(x+x^{-1})/2-1$ forced at T5 of the unified forcing chain, so calibration is the bridge from discrete PRC character axioms to continuum J-uniqueness.
Prime-calibration forcing of identity on a direction also consumes this predicate, tying the single-point hypothesis the cost axioms actually supply to full directional rigidity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.