PRCCharacterTwoPrimeReciprocalRespectsTraceConnected_iff_forces
plain-language theorem explainer
For a character χ on ratio orbits, the global normal form “reciprocal at the orbit-2 prime axis forces reciprocal at every native prime axis” is equivalent to the local form that transports the reciprocal branch only along finite δ-trace connections from orbit 2. Native-cost uniqueness and universal-foundation certificates cite this bridge. The proof is a two-constructor term pairing the already-proved one-way implications.
Claim. Let $\chi$ be a map on ratio orbits. The following are equivalent: (i) if $\chi$ is reciprocal-oriented on the distinguished orbit-$2$ prime axis, then $\chi$ is reciprocal-oriented on every native prime axis; (ii) whenever a native prime axis is joined to the orbit-$2$ prime axis by a finite $\delta$-trace connection, reciprocal orientation of $\chi$ at orbit $2$ implies reciprocal orientation at that prime axis.
background
In the Primitive Recognition Calculus, ratio orbits are rational displays: a signed-orbit numerator over a nonzero distinction-nat denominator. A character $\chi$ is a self-map of ratio orbits used to build native costs. Reciprocal orientation at a prime axis means $\chi$ agrees, under the cross-equality relation on orbits, with the reciprocal of that axis direction.
Two normal forms package the same positive reciprocal-branch transport idea. The forces form is global: reciprocal at the calibrated orbit-$2$ prime axis implies reciprocal at every native prime axis. The trace-connected form is local: the same implication is required only when a finite $\delta$-trace path joins orbit $2$ to the target prime axis.
This module develops uniqueness of the native cost built from such characters (the PRC avatar of J-cost uniqueness). The two props are the branch-transport side conditions that feed the uniqueness certificates.
proof idea
Term-mode Iff.intro with no extra tactics. The forward direction is the upstream lemma that any character satisfying the trace-connected transport prop already satisfies the global forces prop (the connection hypothesis is discharged in that lemma’s argument). The reverse direction is the upstream lemma that global forces immediately yields the trace-connected form: after introducing a prime, a connection witness, and reciprocal-at-2, apply forces and drop the unused connection. The present theorem only packages those two arrows as a single biconditional.
why it matters
Native cost uniqueness needs a clean normal form for how reciprocal branches move off the distinguished orbit-2 axis. Equating the global forces statement with the δ-trace transport statement lets later certificates pick whichever packaging is convenient without re-proving branch transport.
Downstream, prc_native_cost_uniqueness_blocker_certificate records the uniqueness blocker package for native costs, and prc_universal_foundation_conditional_certificate folds the same material into the conditional universal-foundation certificate (kernel, real complete ordered field, trace logic). In the broader RS chain this sits under T5 J-uniqueness: characters that respect reciprocal transport are the discrete precursors of the unique cost $J(x)=(x+x^{-1})/2-1$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.