PRCCharacterTwoPrimeReciprocalForcesPrimeReciprocal
plain-language theorem explainer
Names the positive reciprocal-branch transport rule: if a ratio-orbit character orients the distinguished orbit-2 prime axis as reciprocal, every native prime axis is reciprocal-oriented. Downstream uniqueness and globalization lemmas cite this Prop as one half of reciprocal-witness globalization. Pure definitional packaging of an implication; no proof obligations.
Claim. For a map $\chi$ on ratio orbits, write $\mathrm{crossEq}$ for the internal cross-multiplication equivalence of ratio orbits and $\mathrm{recip}$ for total reciprocal. If $\mathrm{crossEq}(\chi(d_2),\mathrm{recip}(d_2))$ holds for the distinguished orbit-$2$ prime direction $d_2$, then for every prime distinction orbit $p$ one has $\mathrm{crossEq}(\chi(d_p),\mathrm{recip}(d_p))$ at the corresponding prime direction $d_p$.
background
In the Primitive Recognition Calculus, a ratio orbit is an integer numerator over a nonzero distinction-orbit denominator (K4.7). Two ratio orbits are related by crossEq when scaled numerators balance as signed orbits (K4.10); this is the native stand-in for rational equality. Total reciprocal on ratio orbits sends zero to zero and otherwise inverts the display (K4.12).
A PRC ratio character is a map $\chi$ on ratio orbits used to read orientation of calibrated prime axes. The distinguished orbit-2 prime direction is the canonical two-axis; each prime distinction orbit $p$ has its own prime direction. Reciprocal orientation at an axis means $\chi$ lands cross-equivalent to the reciprocal of that axis.
The module develops native-cost uniqueness by forcing characters to match the J-cost branch structure. This Prop isolates the two-to-all half of positive reciprocal-branch transport.
proof idea
Definitional Prop, not a proved theorem. The body is the bare implication: assume cross-equivalence of $\chi$ on the orbit-2 prime direction with its reciprocal; conclude the same cross-equivalence at every prime direction. No tactics, no lemmas applied inside the def itself. Downstream theorems discharge or consume instances of this Prop by specializing globalization or local-orientation hypotheses.
why it matters
This is one conjunct of the split distinguished-axis form of reciprocal-witness globalization: the split packages the two-to-all rule together with the converse all-to-two rule. Downstream, it is equivalent (under local prime orientation) to exclusion of prime-identity orientation at the two-axis, and it is implied by full reciprocal-witness globalization and by the trace-connected transport form.
In the Recognition forcing chain, reciprocal orientation selects the positive J-branch compatible with T5 J-uniqueness and the Recognition Composition Law. Packaging the two-to-all transport as a named Prop lets uniqueness arguments cite a single normal form rather than re-unfolding quantifiers over all prime axes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.