calibrated_square
plain-language theorem explainer
Calibration of a PRC ratio character at an orbit point p extends automatically to the square p·p. Researchers proving single-point calibration implies full character rigidity (or cost uniqueness on ratio orbits) cite this square case. The proof is a one-line specialization of the two-factor multiplicative calibration lemma.
Claim. Let $\chi$ be a PRC ratio character on ratio orbits. If $\chi$ is calibrated at $p$ (i.e. $\chi(p)$ is cross-equivalent to $p$), then $\chi$ is calibrated at the product orbit $p\cdot p$.
background
In the Primitive Recognition Calculus continuum layer, a ratio character $\chi$ is a multiplicative map on ratio orbits. Calibration at a point $q$ means $\chi$ acts as the identity on that orbit direction: $\mathrm{crossEq}(\chi(q), q)$. The module treats calibration at a generator (classically the orbit of two) as the single-point datum that PRC cost hypotheses actually supply.
Multiplicativity of $\chi$ lets calibration travel along products. The sibling lemma calibrated_mul already shows that calibration at $p$ and at $q$ yields calibration at $p\cdot q$. The square case is the diagonal specialization needed when only one calibrated generator is in hand.
Local setting is character rigidity forcing: once calibration propagates along the multiplicative monoid generated by the calibrated point, later lemmas rigidify the associated cost and doubled-trace functionals.
proof idea
One-line term wrapper. Apply the two-argument lemma that calibration is preserved under orbit multiplication, feeding the same calibration hypothesis at $p$ in both slots. No extra arithmetic or cross-equivalence rewriting is required.
why it matters
Closes the two-generator (square) step in the calibration-propagation toolkit inside CharacterRigidityForcing. Downstream helpers in the same module (cost/trace rigidity from calibration, character-trace rigidity, cost-from-character rigidity) rely on being able to move calibration from a seed orbit to its powers and products; the square case is the first pure power. In the broader Recognition chain this supports uniqueness of the PRC native cost once a character is pinned at a single calibrated direction, feeding the continuum side of cost uniqueness rather than a new forcing axiom. No external used-by edges are recorded yet; the immediate consumers are the rigidity lemmas that follow in-module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.