PRCCharacterTwoPrimeIdentityRespectsTraceConnected_of_prime_identity_trace_connected
plain-language theorem explainer
If a ratio-orbit character transports identity orientation along every finite δ-trace link between prime axes, then it does so in the special case that starts at the prime-2 axis. Anyone calibrating native cost uniqueness via two-prime identity transport cites this reduction. The proof is a one-line specialization of the general prime-identity transport hypothesis at the two-orbit.
Claim. Let $\chi$ be a map on rational orbits. Suppose that whenever two prime axes are linked by a finite $\delta$-trace connection and $\chi$ fixes the first prime direction (identity orientation), then $\chi$ also fixes the second. Then the same holds when the source axis is the prime-$2$ axis: identity at $2$ transports along any finite $\delta$-trace connection from $2$ to a target native prime axis.
background
In the Primitive Recognition Calculus, ratio orbits package a signed numerator over a nonzero distinction-nat denominator. Characters are maps $\chi$ on these orbits; native cost uniqueness asks which characters can arise as cost data.
Prime axes carry preferred directions. Identity orientation means $\chi$ fixes a prime direction up to the cross-equality relation on orbits (the algebraic content of equal $J$-costs on that axis). A finite $\delta$-trace connection is a witnessed path relating two prime axes inside one connected component of the trace relation.
The general hypothesis says identity orientation transports along every such prime-to-prime trace link. The two-prime target is the special case with source fixed as the two-step orbit (the prime $2$), which is independently known to be prime. This module builds the uniqueness ladder that forces the native $J$-cost from calibration and transport axioms.
proof idea
One-line specialization. Introduce the target prime $p$, its primality witness, the trace connection from two to $p$, and the identity hypothesis at the two-prime direction. Apply the general prime-identity transport property at source twoOrbit (with the theorem that two is prime) and the same target data; the conclusion is exactly two-prime identity transport.
why it matters
Native cost uniqueness needs identity at $2$ to propagate to every native prime axis that is trace-connected to $2$. This lemma converts the fully general prime-to-prime transport axiom into that two-prime form, so calibration hypotheses can be stated at the two-axis and still reach all primes.
Downstream it feeds PRCPrimeCalibrationForcesTwoPrimeIdentityTraceConnectedTarget_of_prime_identity_trace_transport, which packages the forcing target, and appears in the native-cost uniqueness blocker certificate and the conditional universal-foundation certificate. In the broader RS chain this is bookkeeping inside the uniqueness of $J$ (T5 / RCL), not a new physical constant, but without it the two-prime calibration route does not close.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.