PRCCharacterPrimeIdentityRespectsTraceConnected_of_two_prime_identity_and_forces_two
plain-language theorem explainer
If a ratio-orbit character transports identity from the distinguished orbit-2 prime axis along δ-trace connections, and identity at any calibrated prime forces identity at orbit 2, then identity orientation transports between arbitrary prime axes along any finite δ-trace link. Native-cost uniqueness proofs cite this to upgrade the two-prime transport rule to full prime-axis transport. The argument forces identity at 2, then applies the two-prime rule with the proved universal 2-to-r connection.
Claim. Let $\chi$ map ratio orbits to ratio orbits. Suppose identity orientation at the orbit-$2$ prime axis transports along any finite $\delta$-trace connection from that axis to a native prime axis, and suppose identity at any calibrated prime axis forces identity at the orbit-$2$ axis. Then whenever two prime axes are $\delta$-trace connected and $\chi$ fixes the first by cross-equality, $\chi$ also fixes the second by cross-equality.
background
In the Primitive Recognition Calculus, ratio orbits package a signed numerator over a nonzero distinction-natural denominator. Characters $\chi$ act on these orbits; the native cost is recovered from the character via a doubled-trace / d'Alembert route that ultimately pins $J$.
Prime axes are the directions associated to prime distinction-naturals. Cross-equality records that $\chi$ sends an axis to itself (identity orientation) rather than to its reciprocal. Trace connection is a finite $\delta$-trace witness relating two prime axes; the lemma PRCPrimeAxisTraceConnected_proved shows every pair of prime axes is so connected, and in particular the orbit-$2$ axis connects to every native prime axis.
Two intermediate props package the one-sided normal forms used here: identity at any prime forces identity at orbit $2$, and identity at orbit $2$ transports along the $2$-to-target trace link. The target prop is the unrestricted transport of identity along any prime-to-prime trace connection.
proof idea
Term-mode introduction of the target quantifiers (source prime $p$, target prime $r$, a discarded connection hypothesis, and identity at $p$). Apply the forcing hypothesis to $p$ and the given identity to obtain identity at the orbit-$2$ axis. Invoke the proved fact that the orbit-$2$ prime axis is $\delta$-trace connected to $r$. Feed that connection and the forced orbit-$2$ identity into the two-prime transport hypothesis, which yields identity at $r$. The original $p$--$r$ connection is unused; transport is routed through $2$.
why it matters
Native cost uniqueness needs identity orientation to move freely among prime axes so that local prime calibration upgrades to a global character constraint and ultimately forces the unique $J$-cost (T5 in the forcing chain). This lemma is the algebraic glue: it turns the two-prime transport rule plus the one-sided forcing normal form into full prime-identity trace transport.
Downstream it feeds PRCPrimeCalibrationForcesPrimeIdentityTraceTransportTarget_of_two_prime_identity_trace_connected, which lifts the same pattern to the calibration-target layer, and appears in the native-cost uniqueness blocker certificate that packages the closed factorization and signed-admissible refutation targets. Without this reduction, the certificate could not discharge unrestricted prime-axis identity transport from the orbit-$2$ special case alone.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.