PRCCharacterTwoThreeCompositeLocalOrientation
plain-language theorem explainer
A ratio character has local orientation at the first mixed composite 2·3 when its image of that direction is cross-equivalent to the direction itself or to its reciprocal. Native-cost uniqueness arguments cite this as the positive local-orientation side of the two-adic branch blocker. The body is a pure Prop abbreviation: a two-way disjunction of cross-multiplication equalities.
Claim. A map $\chi$ from ratio orbits to ratio orbits has $2\cdot 3$ composite-local orientation when $\chi(2\cdot 3)$ is cross-multiplication equivalent either to the orbit $2\cdot 3$ itself or to its reciprocal.
background
In the Primitive Recognition Calculus, rationals are carried as ratio orbits: a signed-orbit numerator over a nonzero distinction-nat denominator. Two such displays are identified by cross-equivalence (crossEq): the internal PRC relation that balances scaled numerators and denominators as signed orbits, matching ordinary rational equality on verifier displays.
A ratio character is a map on these orbits. The first mixed composite direction is the orbit for $2\cdot 3$. Local orientation at that composite means the character does not send the mixed direction to an exotic orbit; it must land on one of the two canonical choices, the composite or its reciprocal.
This sits in the native-cost uniqueness module, which studies which characters can arise from doubled-trace / J-cost data and which two-adic axis twists survive calibration. The definition isolates the local geometric constraint before global uniqueness or factorization is imposed.
proof idea
Definitional, not a proof. The predicate is the disjunction of two crossEq atoms: $\chi$ applied to the $2\cdot 3$ composite direction is cross-equivalent to that same direction, or cross-equivalent to its reciprocal. No lemmas are applied; the body is the Prop surface used by later targets and refutations.
why it matters
This is the positive local-orientation interface for the current two-adic branch blocker. Downstream, the universal target asserts that every ratio character carrying a two-adic axis twist still satisfies this orientation; the matching failure character asserts existence of a twist character that violates it.
The absurdity theorem shows that two-adic axis twist plus the ratio-character axioms already force failure of this orientation, and a companion existence theorem packages that into an explicit countermodel witness. Those feed the refutation that prime calibration cannot force nonunit-orbit local orientation, and they appear on the universal-foundation open-target ledger as a negative entry: a route that cannot force the final native-cost surface.
In framework terms this is bookkeeping inside native J-cost uniqueness (the T5 J-cost line), not a new forcing step: it pins exactly where two-adic twisting breaks composite-local canonicity before cost uniqueness can close.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.