PRCCharacterOrbitDirectionReciprocal
plain-language theorem explainer
Predicate asserting that a ratio-orbit character sends the unit-denominator direction of a nonzero distinction position to that direction's reciprocal, under internal cross-multiplication equivalence. Downstream orientation, no-mixing, and prime-witness reflection lemmas cite it as the reciprocal branch. It is a pure definitional Prop with no proof obligations.
Claim. For a map $\chi$ on ratio orbits and a nonzero distinction position $p$, write $d(p)$ for the unit-denominator ratio orbit of $p$. The reciprocal-orientation predicate holds when $\chi(d(p))$ is cross-equivalent to the reciprocal of $d(p)$ (cross-multiplication balance of signed numerator orbits).
background
In the Primitive Recognition Calculus, a RatioOrbit is an integer numerator orbit over a nonzero distinction denominator: the internal display of a rational. Two such displays are related by cross-equivalence when scaled signed numerators balance, the PRC stand-in for rational equality. The total reciprocal sends a nonzero ratio orbit to its inverse and collapses the zero class to zero, matching $\mathbb{Q}$.
The orbit direction of a nonzero distinction $p$ is the ratio orbit with numerator the signed orbit of $p$ and denominator one. Characters here are maps $\chi$ on ratio orbits used to read orientation of native cost against the identity event (the J-cost minimum at state $1$).
This module packages native-cost uniqueness via character constraints. Reciprocal orientation at a single nonzero direction is the local reciprocal branch; the identity branch is the parallel predicate that $\chi$ fixes the direction up to cross-equivalence.
proof idea
Definitional packaging only. The body is the proposition that cross-equivalence holds between $\chi$ applied to the orbit direction of $p$ and the reciprocal of that same direction. No tactics, no lemmas discharged; downstream theorems assume or derive instances of this Prop.
why it matters
Local reciprocal branch marker inside native-cost uniqueness for PRC characters. Downstream it appears in mixed nonunit reciprocal-witness reflection (reciprocal nonunit witnesses force reciprocal prime-axis witnesses), the composite mixed-witness reflection bridge, cross-nonunit no-mixing (identity at one nonunit direction cannot coexist with reciprocal at another), nonunit branch agreement, and exclusion of reciprocal once an identity witness is present.
Those lemmas close orientation coherence so a character cannot mix identity and reciprocal branches across nonunit directions, feeding uniqueness of the native cost readout tied to the J-cost and the forcing chain's J-uniqueness (T5). Without a crisp reciprocal predicate, the reflection and no-mixing arguments have nothing to quantify over.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.