calibration_propagates_to_cyclic_subgroup
plain-language theorem explainer
If a PRC ratio character is calibrated at one orbit point p, calibration extends to p squared and to the reciprocal of p, and the cost it generates at p equals the canonical J-cost. Researchers tracking one-point calibration forcing on the completion cite this for the cyclic-subgroup step. The proof is a one-line term application of the prime-direction identity lemma.
Claim. Let $\chi$ be a PRC ratio character on ratio orbits. If $\chi$ is calibrated at an orbit point $p$, then $\chi$ is calibrated at $p\cdot p$ and at $p^{-1}$, and the cost generated by $\chi$ at $p$ equals the canonical recognition cost $J(p)=(p+p^{-1})/2-1$ on the orbit display.
background
In the Primitive Recognition Calculus continuum layer, costs live on the quotient-native carrier of ratio orbits rather than on $\mathbb{R}$, keeping the development choice-free. A PRC ratio character is a structure-preserving map on those orbits. Calibration at a point means the character agrees with the forced gauge there, so the cost it generates matches the canonical recognition cost.
That cost is $J(x)=(x+x^{-1})/2-1$, the unique solution of the Recognition Composition Law under normalization (T5 J-uniqueness). Reciprocal symmetry of $J$ supplies the one-parameter gauge: the identity and reciprocal automorphisms generate the same cost. The module commits to the completion $R_\delta$ as ambient continuum and asks what cost the recognition laws force on it.
Upstream, the prime-direction identity lemma packages local forcing that turns one calibrated point into identity along the cyclic direction that point generates, returning calibration at the square and reciprocal together with the cost identity.
proof idea
One-line term proof. Apply the upstream lemma prime_calibration_forces_identity_on_direction to the character hypothesis and the calibration-at-$p$ hypothesis. That lemma returns the three conjuncts at once: calibration at $p\cdot p$, calibration at the reciprocal of $p$, and cross-equality of the character-generated cost at $p$ with the canonical orbit display of $J(p)$. No further case split or induction appears in this wrapper.
why it matters
This is the propagation clause of the module capstone on forced $J$ on the completion: calibration at $p$ forces calibration on the cyclic subgroup generated by $p$, and the local cost equals $J(p)$. It sits between single-point calibration and the named open target that one-point calibration (at two) should force global identity on all primes.
In the forcing chain it supports T5 J-uniqueness on the completion: reciprocal-symmetric RCL, normalization, and one calibration datum force $J$, unique up to the reciprocal gauge. The all-primes global step remains open; this lemma closes only the cyclic-subgroup fragment. The field-display link to $J$ on $\mathbb{R}$ is deliberately not routed here, so Classical.choice stays out of the capstone.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.