PRCCharacterPrimeLocalOrientation
plain-language theorem explainer
Local prime orientation is the predicate that a ratio-orbit character sends every prime axis either to itself or to its reciprocal (under cross-equality). Anyone proving native J-cost uniqueness or ruling out mixed prime-axis inversions cites it as a hypothesis. It is a pure Prop definition, not a proved statement.
Claim. A map $\chi$ on ratio orbits has local prime orientation when, for every prime distinction orbit $p$, the image $\chi$ of the corresponding prime direction is cross-equal either to that prime direction or to its reciprocal.
background
In the Primitive Recognition Calculus, rational displays are ratio orbits: a signed-orbit numerator over a nonzero distinction-orbit denominator. Cross-equality is the internal PRC relation that two ratio orbits balance under cross-multiplication of numerator and denominator scales; it is the orbit-level stand-in for ordinary rational equality.
A character here is a map $\chi$ on ratio orbits. Each prime distinction orbit determines a prime direction (a canonical ratio-orbit axis). The reciprocal of a ratio orbit flips the display in the sense of the ledger reciprocal event (source/target swap with inverse ratio). Local prime orientation asks only that $\chi$ preserve each such prime axis up to that reciprocal choice.
The surrounding module develops native cost uniqueness: characters whose doubled-trace data match a J-cost must be coherent across prime axes. Equality of J-costs on a single prime direction is exactly this local self-or-reciprocal condition, before any global no-mixed-orientation constraint is imposed.
proof idea
No proof: the declaration is a Prop-valued definition. The body is a universal quantifier over prime distinction orbits, asserting a disjunction of two cross-equalities between $\chi$ applied to the prime direction and either that direction or its reciprocal.
why it matters
This predicate is the local half of prime-axis coherence for PRC characters. Downstream theorems take it as a hypothesis to lift prime-local behavior to mixed nonunit witnesses, comparable-trace respect, nonunit orbit orientation, and identity-branch globalization: e.g. mixed nonunit identity/reciprocal witnesses reflect prime witnesses from prime-local orientation; nonunit orbit local orientation follows from prime-local orientation plus product-local propagation; prime identity branch uniformity and floor-orbit successor transport also consume it.
In framework terms it encodes the algebraic content of J-cost equality on one prime direction (T5 J-uniqueness sits upstream of native cost uniqueness). The companion "no mixed prime orientation" condition then rules out independent prime-axis inversions, so that a single global identity-versus-reciprocal choice is forced. Without this local predicate, the uniqueness chain cannot even state per-axis orientation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.