target_OnePointCalibrationForcesGlobalIdentity
plain-language theorem explainer
One-point calibration of a PRC ratio character at the distinguished axis 2 forces calibration at every nonzero ratio orbit. Anyone closing native cost uniqueness or forcing J on the completion cites this open target. The declaration is only the Prop packaging that gap: no proof is given here; single-prime rigidity is upstream, multi-prime propagation remains open.
Claim. For every map $\chi$ from ratio orbits to ratio orbits that is a PRC ratio character (fixes the unit orbit up to cross-equivalence and is multiplicative up to cross-equivalence), if $\chi$ is calibrated at the orbit $2$ (meaning $\chi(2)$ is cross-equivalent to $2$), then $\chi$ is calibrated at every ratio orbit $q$ whose rational display is nonzero.
background
In the primitive recognition calculus, costs factor through ratio characters on quotient-native ratio orbits. A ratio orbit is an integer numerator over a nonzero distinction-nat denominator; its verifier display toRat recovers an ordinary rational. A PRC ratio character $\chi$ is a map on ratio orbits that fixes the unit orbit and is multiplicative, both up to cross-equivalence (the quotient-native equality), so the structure stays native rather than field-level.
Calibration at an orbit $q$ means $\chi(q)$ is cross-equivalent to $q$ itself: $\chi$ acts as the identity character along that direction. The cost hypotheses only supply calibration at the distinguished axis $2$ (the ratio orbit with numerator the signed orbit of two and denominator one). Module context is continuum character-rigidity forcing: per-direction rigidity is available; global identity from one point is the remaining statement.
Upstream, PRCRatioCharacter and CharacterCalibratedAt fix the vocabulary. Doc on calibration: "Calibration at two is the single-point datum the PRC cost hypotheses actually carry."
proof idea
There is no proof. This is a bare Prop definition packaging an open target. The body is the universal statement: any PRC ratio character calibrated at two is calibrated at every nonzero ratio orbit. Sibling lemmas in the module give single-direction and cyclic-subgroup rigidity (trace rigidity, cost-from-character rigidity, calibrated square/recip/mul); they do not discharge multi-prime propagation. Treat the declaration as a named hypothesis interface for downstream forcing, not as a theorem.
why it matters
Native cost uniqueness leaves open the all-prime-directions claim: one-point data at two should force the identity character everywhere nonzero. This Prop is that claim. Downstream, ForcedJOnCompletion aliases it as target_global_identity_from_one_point_calibration and builds cyclic-subgroup propagation (calibration_propagates_to_cyclic_subgroup): calibration at $p$ forces calibration at $p^2$ and $p^{-1}$ and pins the generated cost to $J(p)$. Closing this target would let one-point calibration at two flood every prime direction and force the global identity character, hence force $J$ on the completion.
In the Recognition forcing chain this sits under T5 J-uniqueness and the Recognition Composition Law: unique multiplicative characters calibrated on a generating set pin the cost to $J(x)=(x+x^{-1})/2-1$. Until proved, continuum forcing of $J$ from PRC-native data remains conditional on this Prop.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.