PRCCharacterTwoPrimeIdentityRespectsTraceConnected
plain-language theorem explainer
A ratio-orbit character respects two-prime identity transport when identity orientation at the orbit-2 prime axis, plus a finite δ-trace link to another native prime axis, forces identity orientation at that target. Native-cost uniqueness and prime-calibration arguments cite this as the identity branch of two-prime trace transport. Pure Prop packaging: the body is the quantified implication, with no proof obligations.
Claim. A map $\chi$ on ratio orbits has the two-prime identity trace-transport property when, for every native prime $p$ whose prime axis is finitely $\delta$-trace-connected to the orbit-$2$ prime axis, cross-equality $\chi(\text{two-prime direction}) \simeq \text{two-prime direction}$ implies cross-equality $\chi(\text{prime direction of } p) \simeq \text{prime direction of } p$.
background
In the Primitive Recognition Calculus, ratio data live on RatioOrbit: a signed-orbit numerator over a nonzero distinction-nat denominator. Two such displays are identified by crossEq, the internal PRC cross-multiplication relation (balanced scaled numerators), which is the orbit-native stand-in for rational equality.
Prime axes are built from DistinctionNat primes and their prime-orbit witnesses. The orbit-2 prime axis is the distinguished base; a finite δ-trace connection (PRCPrimeAxisTraceConnected) is a discrete path of orbit steps linking that base axis to the prime axis of another native prime $p$. Local prime orientation of a character $\chi$ means each prime direction is sent to itself or its reciprocal under crossEq; identity orientation is the self case, the algebraic content of matching J-costs on a single prime direction.
This module develops native-cost uniqueness for PRC characters. The present definition isolates the identity half of two-prime branch transport: identity at 2 should ride any finite trace connection out to identity at $p$.
proof idea
Definitional Prop, not a proved theorem. The body is a single universal quantification over native primes $p$ with prime-orbit witness: assume a δ-trace connection from the orbit-2 prime axis to $p$, assume $\chi$ fixes the two-prime direction under crossEq, conclude $\chi$ fixes the prime direction of $p$ under crossEq. No tactics, lemmas, or term construction beyond packaging that implication.
why it matters
Native J-cost uniqueness (T5 in the forcing chain) needs characters to preserve prime orientations consistently. This Prop is the identity-side transport law from orbit 2 along finite δ-traces; its reciprocal twin handles the inverse branch. Downstream, prime-identity transport is recovered from two-prime identity plus a forces-two hypothesis, and reciprocal-twist lemmas swap identity and reciprocal variants.
It appears in the Pass-25 blocker certificate for native cost uniqueness and is the conclusion of the open target PRCPrimeCalibrationForcesTwoPrimeIdentityTraceConnectedTarget: prime calibration of a ratio character should force this transport. That target is listed among universal-foundation open obligations, so closing calibration-implies-transport would discharge a named uniqueness blocker rather than leave an unstructured sorry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.