PRCCharacterPositiveOrbitIdentity_of_all_prime_identity
plain-language theorem explainer
If a ratio-orbit character is multiplicative, reciprocal, unit-preserving, respects cross-equivalence, is product-display compatible, and fixes every prime orbit direction, then it fixes the orbit direction of every nonzero natural distinction. Cost-uniqueness and d'Alembert factorization arguments cite this to promote prime-axis identity to all positive axes. The proof cases on units versus non-units and reduces the non-unit case to a prior composite-orbit lemma.
Claim. Let $\chi$ map ratio orbits to ratio orbits and satisfy the ratio-character axioms (fixes the unit orbit, is multiplicative, and respects reciprocals, all up to cross-equivalence). Suppose $\chi$ respects cross-equivalence, is compatible with the native display of orbit products, and $\chi$ fixes every prime orbit direction. Then for every nonzero distinction $p$, $\chi$ fixes the orbit direction of $p$: $\chi(\mathrm{dir}(p)) \sim \mathrm{dir}(p)$ under cross-equivalence.
background
In the Primitive Recognition Calculus, rational data live as ratio orbits: a signed-orbit numerator over a nonzero distinction denominator. Two ratio orbits are cross-equivalent when cross-multiplication balances as signed orbits; this is the internal rational equality, and it agrees with equality of the rational verifier displays.
A ratio character is a candidate factor for the d'Alembert factorization of a PRC cost. It is stated at the ratio-orbit level and uses cross-equivalence rather than definitional equality, so it stays quotient-native: it fixes the unit orbit, multiplies on products, and sends reciprocals to reciprocals (up to cross-equivalence). Two further interface conditions are needed for raw maps: quotient-respect (equivalent displays get equivalent character values) and product-display compatibility (the character on a product orbit agrees with the character on the ratio product of the factor orbits).
Identity orientation on an arbitrary nonzero orbit direction means the character value on that direction is cross-equivalent to the direction itself. The hypothesis supplies this only on prime axes; the theorem lifts it to every nonzero distinction.
proof idea
Case on whether the nonzero distinction $p$ is a unit.
If $p$ is a unit, its orbit direction is cross-equivalent to the unit ratio orbit (via the rational display: unit distinctions map to $1$). Quotient-respect of $\chi$ moves that equivalence under $\chi$; the character unit axiom and symmetry/transitivity of cross-equivalence then close $\chi(\mathrm{dir}(p)) \sim \mathrm{dir}(p)$.
If $p$ is not a unit, apply the dedicated non-unit lemma that, from the same character axioms, product-display compatibility, and prime-axis identity, already yields identity on every non-unit nonzero orbit direction.
why it matters
Native cost uniqueness in PRC proceeds by showing that any character arising in the d'Alembert factorization of the cost is forced to the identity orientation on positive ratio data, so the cost collapses to the unique $J$-shaped native cost. This theorem is the orbit-direction step: prime-axis identity plus the character interface imply identity on every nonzero orbit direction, which is exactly what composite positions need for trace transport.
It is consumed immediately by the positive-ratio identity theorem in the same module, which lifts the conclusion from orbit directions to general positive ratio orbits. In the broader Recognition forcing chain this sits under $J$-uniqueness (T5) and the Recognition Composition Law: characters that factor costs must not twist positive axes once they fix primes.
No scaffolding remains here; the claim is fully proved and only the downstream ratio-level packaging remains as the next citation target.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.