prime_calibration_forces_identity_on_direction
plain-language theorem explainer
A ratio character calibrated at one orbit direction p is forced to stay the identity on p² and p⁻¹, and the cost it generates at p equals the canonical PRC J-cost. Anyone proving uniqueness of J on the continuum completion cites this single-direction rigidity. The proof is a three-conjunct term packing calibrated multiplicativity, reciprocal closure, and cost rigidity.
Claim. Let $\chi$ be a PRC ratio character on ratio orbits. If $\chi$ is calibrated at an orbit $p$ (i.e. $\chi(p)$ is cross-equivalent to $p$), then $\chi$ is calibrated at $p\cdot p$ and at $p^{-1}$, and the cost generated by $\chi$ at $p$ is cross-equivalent to the canonical PRC cost $J$ evaluated on the orbit $p$.
background
In the Primitive Recognition Calculus continuum layer, ratio orbits are the multiplicative directions on which characters and costs live. A PRC ratio character $\chi$ is a multiplicative, reciprocal-respecting map on those orbits. Calibration at $q$ means $\chi(q)$ is cross-equivalent to $q$ itself: $\chi$ acts as the identity character on that direction. The single-point datum the cost hypotheses actually carry is calibration at the distinguished axis two, but the local lemma is stated for a general orbit $p$.
The cost pulled from a character is compared to the canonical PRC display onRatioOrbit, which is the orbit-level form of the J-cost $J(x)=(x+x^{-1})/2-1$ forced later in the chain (T5). Cross-equivalence is the native equality relation on ratio orbits (via rational displays).
Upstream, calibration is already closed under products and reciprocals, and a calibrated character's cost at the calibration point matches the canonical J-display. This theorem packages those three facts as the single-prime-direction rigidity step.
proof idea
Pure term-mode conjunction. The first conjunct is calibrated_mul applied twice to the same calibration hypothesis (so $\chi$ stays identity on $p\cdot p$). The second is calibrated_recip (identity on $p^{-1}$). The third is costFromCharacter_rigid, which reduces cost matching at a calibration point to the orbit cross-equivalence lemma onRatioOrbit_crossEq. No extra case analysis or induction.
why it matters
This is the per-direction rigidity brick for forcing the canonical J-cost on the continuum completion. Downstream, calibration_propagates_to_cyclic_subgroup re-exports the same triple (calibration on $p^2$ and $p^{-1}$, cost equals $J(p)$), and the capstone forced_J_on_completion uses it: on $R_\delta$, reciprocal-symmetric RCL plus normalization plus one calibration datum force the cost to $J(x)=(x+1/x)/2-1$ up to the reciprocal gauge.
In the Recognition forcing chain this feeds T5 J-uniqueness and the Recognition Composition Law at the continuum level. The module states honestly that the all-primes target remains open: one-point calibration at two forcing identity on every nonzero ratio orbit is still a named Prop, not proved here. This lemma supplies the cyclic-subgroup step; independent prime directions are the remaining content left by PRCNativeCostUniqueness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.