PRCCharacterOrbitDirectionIdentity
plain-language theorem explainer
Identity orientation of a ratio-orbit character at an arbitrary nonzero orbit position: the character fixes that direction up to cross-multiplication equivalence. Anyone proving nonunit coherence, mixed-witness reflection, or composite trace transport cites this predicate. It is a one-line Prop abbreviation packaging crossEq of the character image against the bare orbit direction.
Claim. For a map $\chi$ on ratio orbits and a nonzero distinction position $p$, the identity-orientation predicate holds when $\chi$ applied to the unit-denominator direction of $p$ is cross-multiplication equivalent to that same direction: $\chi(\mathrm{dir}(p)) \sim_{\times} \mathrm{dir}(p)$.
background
In the Primitive Recognition Calculus, distinction naturals are the base-neutral finite orbits of repeated distinction. A ratio orbit is an integer numerator over a nonzero orbit denominator. Cross-equivalence equates two ratio orbits when the scaled signed numerators balance under cross-multiplication; it is the internal PRC stand-in for rational equality.
The orbit direction of a nonzero $p$ is the ratio orbit with numerator the signed orbit of $p$ and denominator one. Characters here are maps on ratio orbits used to build native cost and doubled-trace displays. The surrounding module develops uniqueness of the native cost functional from character hypotheses, including d'Alembert-type relations and trace-matching.
The doc-comment stresses that identity orientation is stated for arbitrary nonzero positions, not only prime axes, so that trace transport can pass through composite orbit positions.
proof idea
Definitional abbreviation, not a proved theorem. The body is the single proposition that the character image of the orbit direction is cross-equivalent to the direction itself. No tactics or lemmas are applied; downstream results unfold or pattern-match on this Prop.
why it matters
This predicate is the identity half of orientation language used throughout native-cost uniqueness. Downstream it appears in mixed-nonunit reflection laws (identity and reciprocal halves), the composite bridge that forces mixed prime-axis witnesses from mixed nonunit witnesses, cross-nonunit no-mixing, and nonunit branch agreement.
By allowing identity orientation at composite (nonunit) positions, it supports the reflection path from nonunit witnesses down to prime-axis witnesses, which product propagation alone does not supply. That closes a coherence gap needed before character-derived cost can be identified with the unique J-cost forced later in the foundation chain (T5 J-uniqueness via the Recognition Composition Law).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.