PRCCharacterTwoPrimeReciprocalForcesPrimeReciprocal_of_trace_connected
plain-language theorem explainer
If a ratio-orbit character respects reciprocal-branch transport along finite δ-trace connections from the orbit-2 prime axis, then reciprocal orientation at orbit 2 forces reciprocal orientation at every native prime axis. Native-cost uniqueness arguments cite this to collapse the trace-connected transport hypothesis to the global forcing normal form. The proof is a direct application of universal prime-axis trace connectivity.
Claim. Let $\chi$ be a map on rational orbits. Suppose that whenever the orbit-$2$ prime axis is $\delta$-trace-connected to a native prime axis $p$, reciprocal orientation of $\chi$ at the orbit-$2$ direction transports to reciprocal orientation at $p$. Then reciprocal orientation of $\chi$ at the orbit-$2$ prime direction forces reciprocal orientation at every native prime direction.
background
In the Primitive Recognition Calculus, a ratio orbit packages a signed numerator over a nonzero distinction-nat denominator. Characters $\chi$ on ratio orbits encode branch choices for the native cost; reciprocal orientation means $\chi$ sends a prime direction to its reciprocal under orbit cross-equality.
The distinguished two-step orbit is the calibration prime axis. The forcing normal form asserts: if $\chi$ is reciprocal at that base, it is reciprocal at every native prime axis. The trace-connected variant weakens the claim to primes reachable by a finite $\delta$-trace path from the base.
Upstream, every pair of prime axes is already trace-connected: the proved connectivity lemma builds an explicit orbit-position trace along the sum of the two primes. The two-orbit itself is prime.
proof idea
Term-mode proof by introduction. Fix the reciprocal-at-two hypothesis and an arbitrary native prime $p$ with its primality witness. Apply the trace-connected character hypothesis at $p$, feeding it the universal connectivity certificate for the pair (two-orbit, $p$) together with the reciprocal-at-two assumption. The resulting cross-equality is exactly the pointwise reciprocal orientation demanded by the forcing normal form.
why it matters
This lemma is one direction of the equivalence between the trace-connected and global forcing forms of two-prime reciprocal transport. That equivalence feeds the prime-calibration target reducing reciprocal forcing to a trace-connected hypothesis, and it appears in the native-cost uniqueness blocker certificate that packages factorization and signed-admissible refutation results.
In the Recognition Science chain, native cost uniqueness is the PRC-side realization of T5 J-uniqueness: $J(x)=(x+x^{-1})/2-1$ is forced once reciprocal branch choices are pinned on the prime axes. Closing the transport gap between the calibrated two-axis and arbitrary primes is required before d'Alembert/RCL identities can select a unique native cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.