PRCCharacterPrimeIdentityIffTwoPrimeIdentity
plain-language theorem explainer
Defines the identity-iff-two normal form for a ratio-orbit character: fixing any native prime axis under cross-equality is equivalent to fixing the distinguished orbit-2 prime axis. Cited throughout native-cost uniqueness when reducing prime-axis orientation to a single calibrated generator. The body is a pure Prop abbreviation, not a proved statement.
Claim. For a map $\chi$ on ratio orbits, the following holds: for every prime distinction $p$, $\chi$ fixes the prime direction of $p$ under cross-multiplication equality if and only if $\chi$ fixes the distinguished orbit-$2$ prime direction under the same relation.
background
In the Primitive Recognition Calculus, a ratio orbit is an integer numerator over a nonzero distinction-natural denominator. Two ratio orbits are related by cross-equality when the scaled signed numerators balance: $a.num\cdot b.den$ matches $b.num\cdot a.den$ as signed orbits. That is the internal PRC stand-in for rational equality.
A character here is a self-map $\chi$ of ratio orbits. Identity orientation on an axis means $\chi$ sends that axis to something cross-equal to itself. Native primes supply calibrated axes via prime directions; the orbit-$2$ prime direction is the distinguished reference axis used as a normal-form generator.
The surrounding module develops uniqueness of the native cost from character and doubled-trace hypotheses. This definition packages the biconditional that collapses all prime-axis identity checks to the single orbit-$2$ check.
proof idea
Definitional abbreviation only. The Prop is the universal quantification over prime distinction naturals $p$ (with primality witness) of the biconditional between cross-equality of $\chi$ on the $p$-prime direction with that direction, and the same cross-equality on the fixed two-prime direction. No tactics or lemmas are invoked.
why it matters
This normal form is the hinge between local prime-orientation control and global branch uniformity in native-cost uniqueness. Downstream, it is equivalent to prime-identity branch uniformity, implies the one-sided force from any prime identity to the two-prime identity, and is recovered from admissible characters, from branch uniformity, and from local two-prime branch control.
In the Recognition forcing picture this sits under cost uniqueness for the J-cost lineage (T5): characters that preserve identity orientation must do so coherently across the prime lattice, with orbit-$2$ as the generator. Reciprocal twist recovers the converse direction at target level, matching the reciprocal automorphism used elsewhere in the ledger and cost algebra.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.