PRCPrimeCalibrationForcesPrimeIdentityForcesTwoPrimeIdentityTarget
plain-language theorem explainer
Defines the open target that every prime-calibrated ratio character must send the orbit-2 prime axis to itself whenever it fixes any native prime axis. Native-cost uniqueness work cites it as the one-sided distinguished-axis obligation. The body is a pure Prop abbreviation packaging three character hypotheses into a single universal statement.
Claim. For every map $\chi$ on rational ratio-orbits that is a ratio character and is calibrated on every native prime direction (its induced cost matches canonical $J$-cost on each prime orbit), the following holds: if $\chi$ fixes any prime-direction orbit pointwise under cross-equality, then $\chi$ also fixes the distinguished orbit-$2$ prime direction.
background
In the Primitive Recognition Calculus, ratio data live on RatioOrbit: a signed numerator over a nonzero distinction-nat denominator. A ratio character $\chi$ is a self-map of these orbits used to manufacture a candidate native cost via costFromCharacter. Prime-direction calibration demands that this cost agree with the canonical $J$-cost on every prime orbit (cross-equality of orbit values).
The one-sided normal form packaged here says that identity at any calibrated prime axis forces identity at the distinguished orbit-$2$ axis. Upstream, the reciprocal automorphism and the identity event (the $J$-cost minimum at ratio $1$) fix the branch language: identity versus reciprocal twist. The reverse direction is recovered later by applying the same statement to the reciprocal twist of $\chi$.
Locally this module splits native-cost uniqueness into exact Lean targets rather than a single closed theorem. This definition is one of those named targets.
proof idea
No proof: the declaration is a def of a Prop. It universally quantifies over maps $\chi$ on ratio-orbits, assumes the ratio-character predicate and prime-direction calibration, and concludes the already-defined one-sided normal form (identity on any prime axis forces identity on the orbit-$2$ axis). The body is a straight abbreviation of those three layers.
why it matters
This target is a hub in the native-cost uniqueness blocker certificate: many equivalence theorems rewrite it into exclusion of mixed composite defects, non-two composite cost defects, two-prime mixed characters, and mixed-composite cost consistency. Downstream, the absurdity theorem for prime-calibrated two-adic axis-twist characters takes this target as hypothesis and derives a contradiction, so closing it would kill a concrete counter-character family.
In the Recognition forcing picture this is the distinguished-axis step that pins the two-adic (octave) direction once primes are $J$-calibrated, aligning with the eight-tick / $2^3$ landmark and the uniqueness of the native cost that feeds T5 $J$-uniqueness. It remains an open obligation inside the Pass-25 certificate rather than a proved lemma.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.