PRCCharacterPrimeIdentityRespectsComparableTrace_of_nonunit_identity_comparable_trace
plain-language theorem explainer
If a ratio-orbit character transports identity orientation between nonunit directions whenever their finite δ-orbit traces are comparable, then it does the same between prime axes. Anyone calibrating native cost uniqueness via prime-axis identity will cite this specialization. The proof is a one-line unpacking: prime orbits are nonzero and nonunit, so the nonunit law applies directly.
Claim. Let $\chi$ map ratio orbits to ratio orbits. Suppose that whenever two nonzero nonunit distinction naturals $p,r$ have comparable finite $\delta$-orbit traces (one extends the other), identity orientation of $\chi$ at the $p$-direction implies identity orientation at the $r$-direction. Then the same holds restricted to prime orbits: comparable prime-axis traces transport identity orientation of $\chi$ from one prime direction to the other.
background
In the Primitive Recognition Calculus, a RatioOrbit is a rational display: signed-orbit numerator over a nonzero distinction-natural denominator. Characters $\chi$ act on these orbits. Identity orientation at a direction means $\chi$ fixes that prime (or nonunit) direction up to the cross-equality relation on ratio orbits.
Two finite $\delta$-orbit position traces are comparable when one extends the other under the trace extension order. The nonunit identity law says identity orientation transports between any two nonzero nonunit directions with comparable traces. The prime identity law is the same statement restricted to prime orbits.
The module develops native cost uniqueness for PRC characters. Structural comparability of any two orbit traces is already available upstream; what remains is that the character itself respect that order when carrying identity orientation. The nonunit form is the broader transport law; the prime form is the calibration target used later.
proof idea
One-line specialization. Introduce prime orbits $p,r$, their prime-orbit witnesses, the comparable-trace hypothesis, and identity at $p$. A prime-orbit witness unpacks to nonzero plus nonunit (and the prime property). Feed those components, the trace comparability, and the identity hypothesis into the assumed nonunit identity-respects-comparable-trace law. The conclusion is exactly identity orientation at the $r$ prime direction.
why it matters
Native cost uniqueness needs identity orientation to propagate along prime axes under trace order, so that prime calibration pins the character. This lemma closes the gap from the broader nonunit transport hypothesis to the prime-axis law that calibration actually quotes.
Its sole downstream consumer is the calibration lift: if prime calibration forces the nonunit identity-comparable-trace target, then it forces the prime identity-comparable-trace target, by applying this specialization to the character. That sits inside the PRC native-cost uniqueness chain that forces the J-cost shape (the T5 landmark $J(x)=(x+x^{-1})/2-1$) from recognition composition and character constraints.
No open scaffold remains here: the claim is fully proved and only specializes an already-stated Prop.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.