PRCCharacterTwoPrimeReciprocalRespectsTraceConnected
plain-language theorem explainer
Property of a ratio-orbit character: if the reciprocal branch holds at the prime-2 direction and a finite δ-trace connects the 2-axis to another native prime axis, then the reciprocal branch holds at that prime. Cited by native-cost uniqueness blockers, the two-prime reciprocal forcing lemmas, and the reciprocal/identity twist bridge. Pure propositional definition packaging a quantified implication; no proof obligations.
Claim. For a map $\chi$ on ratio orbits, and for every native prime $p$ whose prime axis is $\delta$-trace-connected to the prime axis of $2$: if $\chi$ sends the $2$-prime direction to its reciprocal (equality under cross-multiplication of ratio orbits), then $\chi$ sends the $p$-prime direction to its reciprocal.
background
In the Primitive Recognition Calculus, rational data live as ratio orbits: a signed-orbit numerator over a nonzero distinction-nat denominator. Two ratio orbits are identified by crossEq when cross-multiplication balances as signed orbits (the internal PRC stand-in for rational equality). The total reciprocal on ratio orbits sends zero to zero and otherwise swaps numerator and denominator in the nonzero case.
Characters here are maps $\chi$ on ratio orbits used to read off native cost data. The two-prime direction is the distinguished prime-axis display at orbit $2$. Trace-connectedness (PRCPrimeAxisTraceConnected) asserts a finite $\delta$-trace path from the orbit-$2$ prime axis to the target native prime axis $p$.
The surrounding module develops uniqueness of the native cost via character constraints (doubled-trace d'Alembert structure, cross-equation matching). This definition is the reciprocal-branch, trace-connected transport hypothesis along that axis graph.
proof idea
Propositional definition only: no tactics and no lemmas applied. It packages a universal quantifier over native primes $p$ (with primality witness), an implication from prime-axis $\delta$-trace-connection to orbit $2$, and a further implication from reciprocal-branch agreement of $\chi$ at the two-prime direction to the same reciprocal-branch agreement at the $p$-prime direction, both stated via cross-multiplication equality of ratio orbits.
why it matters
This is the trace-connected packaging of positive reciprocal branch transport from orbit $2$. Downstream it is equivalent (in this module) to the forcing form that drops the connection hypothesis and simply pushes the reciprocal branch from $2$ to every native prime; the two directions of that equivalence are recorded as of-trace-connected and of-forces lemmas, plus the iff.
It also bridges to the identity-branch twin via reciprocal twist: reciprocal-trace-connected for the twisted character yields identity-trace-connected for $\chi$, and conversely. Those bridges feed the Pass-25 native-cost uniqueness blocker certificate, which splits remaining uniqueness work into exact Lean targets, and appear among the open targets listed by the universal foundation module. In the broader RS chain this is local scaffolding toward character uniqueness for the native cost (the PRC route into J-uniqueness / T5), not a closed forcing step by itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.