PRCCharacterPrimeIdentityRespectsComparableTrace_of_successor_step
plain-language theorem explainer
If a ratio character preserves identity orientation under one successor step on nonzero δ-orbits, then identity orientation transports between any two prime axes whose finite orbit traces are comparable by extension. Native-cost uniqueness arguments cite this to upgrade the one-step law to the prime-to-prime trace-order law. The proof routes identity through the unit orbit direction via the successor bridge, then rebuilds it at the target prime.
Claim. Let $\chi$ map rational orbits to rational orbits. Suppose identity orientation is invariant under one successor step on every nonzero distinction-orbit direction: for all $p\neq 0$, $\chi$ fixes the direction of $p$ if and only if it fixes the direction of $\mathrm{succ}(p)$. Then whenever $p$ and $r$ are prime-orbit axes whose position traces are comparable by extension, identity orientation of $\chi$ at $p$ implies identity orientation of $\chi$ at $r$.
background
Primitive Recognition Calculus works with DistinctionNat, the base-neutral finite orbit of repeated distinction (zero and successor), and with RatioOrbit, a rational display of signed numerator over nonzero orbit denominator. Orbit directions and prime directions are the corresponding ratio-orbit axes; identity orientation means the character $\chi$ is cross-equal to that axis (fixes it rather than sending it to a reciprocal or other class).
The one-step hypothesis is smaller than prime-to-prime transport: it only asks that identity orientation be invariant under a single successor on nonzero $\delta$-orbits, before primality is imposed. The target property is the exact trace-order law: if two prime axes have comparable finite orbit-position traces (one extends the other), identity at the first prime forces identity at the second. Structural comparability of traces is already available upstream; what remains is that the character respect that order.
Upstream lemmas close the bridge through the unit: from identity at any nonzero $p$ and the successor law one obtains identity at $1$, and from identity at $1$ one obtains identity at any nonzero $r$.
proof idea
Tactic proof, four steps. Introduce primes $p,r$, the unused comparability hypothesis, and identity of $\chi$ at the prime direction of $p$. Rephrase that hypothesis as orbit-direction identity at $p$. Apply PRCCharacterOrbitIdentity_one_of_identity with the successor-step law to pull identity down to DistinctionNat.one (using one_ne_zero). Apply PRCCharacterOrbitIdentity_of_one with the same successor law to push identity from $1$ out to $r$. Comparability is not consulted: successor invariance already gives full nonzero-to-nonzero transport of identity orientation.
why it matters
This is a forcing step inside native-cost uniqueness for the Primitive Recognition Calculus: the J-cost side of the Recognition Composition Law needs characters that respect trace order on prime axes. Downstream, PRCPrimeCalibrationForcesPrimeIdentityComparableTraceTarget_of_successor_step is a one-line wrapper that feeds calibrated successor identity into this theorem, and the result sits on the path to prc_native_cost_uniqueness_blocker_certificate, which packages the zero-calibrated factorization target and the refutation of signed-admissible alternatives.
In the broader RS chain this supports T5-style J-uniqueness at the PRC layer: once identity orientation is locked under successor steps, prime-axis identity becomes a global property of comparable traces, so the native cost extracted from the character cannot drift between prime rungs. It does not itself name $\phi$ or the eight-tick octave; it supplies the orientation-transport lemma those later calibrations rely on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.