PRCCharacterPrimeIdentityRespectsComparableTrace
plain-language theorem explainer
Identity orientation on prime axes transports along comparable δ-orbit traces: if a ratio map χ fixes one prime direction under cross-equality and the two prime orbit traces are comparable by extension, then χ fixes the other. Used throughout native-cost uniqueness when discharging prime-local identity coherence. Pure Prop definition packaging the exact trace-order law; no proof content.
Claim. For a map $\chi$ on ratio orbits, whenever $p$ and $r$ are prime distinction-nats whose finite orbit-position traces are comparable by extension (one extends the other), if $\chi$ is cross-equal to the identity on the prime direction of $p$, then $\chi$ is cross-equal to the identity on the prime direction of $r$.
background
In the Primitive Recognition Calculus, a finite trace is built by successive distinction acts; Extends T U means $U$ is $T$ followed by a suffix. Each distinction-nat carries an orbit-position trace. Two such traces are comparable when one extends the other.
A ratio orbit is an integer numerator over a nonzero orbit denominator. Cross-equality is the internal rational relation: two ratio orbits match when the cross-multiplied signed orbits balance. The prime direction of a prime orbit is the canonical ratio-orbit axis attached to that prime.
Identity orientation means $\chi$ sends that axis to a cross-equal copy of itself (the PRC counterpart of the zero-cost self-comparison law). The structural fact that any two orbit-position traces are comparable is already available upstream; this definition isolates the residual demand on $\chi$: identity orientation must transport between comparable prime axes.
proof idea
Definitional Prop, not a proved theorem. The body is a four-quantifier implication: for prime orbits $p,r$ with prime-orbit witnesses, if the orbit-position traces are comparable by extension either way, and if $\chi$ is cross-equal to the identity on the prime direction of $p$, conclude the same for $r$. No tactics or lemmas are applied; downstream results discharge or consume the predicate.
why it matters
This is the exact trace-order law required for ratio characters in the native-cost uniqueness development. Downstream it is equivalent to prime-identity trace coherence, is implied by nonunit-identity comparable-trace respect and by successor-step / floor-successor transport, and immediately yields common-trace-extension respect (via the already-proved orbit-trace comparability).
It sits in the chain that forces the native cost to match the unique $J$-cost of the Recognition Composition Law (forcing landmark T5: $J(x)=(x+x^{-1})/2-1$). Parent uses include lifting prime-local orientation to nonunit axes and packaging identity transport for composite orbit positions. Without this Prop as a named hypothesis interface, the character-to-cost uniqueness theorems cannot state their prime-axis coherence assumptions cleanly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.