PRCCharacterNonunitIdentityRespectsComparableTrace
plain-language theorem explainer
Defines the trace-order form of nonunit identity transport for a ratio-orbit character: if two nonzero nonunit orbit directions have comparable finite δ-traces, identity orientation at one forces identity orientation at the other. Cited when reducing global nonunit identity-branch transport to a local trace-order law. Pure Prop packaging; no proof content.
Claim. A map $\chi$ on rational orbits respects comparable-trace nonunit identity if, for all nonzero nonunit distinction numbers $p$ and $r$ whose native orbit-position traces are comparable under extension (one is a prefix of the other), identity orientation of $\chi$ at $p$ implies identity orientation of $\chi$ at $r$.
background
In the Primitive Recognition Calculus, a finite trace is built by successive distinction acts (empty or extend-by-one). Trace extension means one trace is the other followed by a suffix. Distinction numbers are the base-neutral finite orbits of repeated distinction; the only multiplicative unit is the one-step orbit.
Each nonzero distinction number carries a native orbit-position trace defined by recursion on the $\delta$-orbit, without importing verifier naturals as object theory. A ratio orbit is an integer numerator over a nonzero orbit denominator. Characters here are maps $\chi$ on ratio orbits; orbit-direction identity is the orientation predicate that $\chi$ acts as the identity branch at a given nonzero direction.
The local setting is native-cost uniqueness for PRC characters: one must force that identity orientation, once present on a nonunit direction, propagates across the nonunit locus. Because orbit-position traces are totally ordered by extension length, comparability is the natural order-theoretic packaging of that transport.
proof idea
Definitional Prop only: the body is a universal quantification over nonzero nonunit distinction numbers $p,r$, a comparability hypothesis that one of orbitPositionTrace p and orbitPositionTrace r extends the other, and the implication from orbit-direction identity at $p$ to the same at $r$. No tactics or lemmas are applied; downstream theorems discharge or consume the Prop as a hypothesis interface.
why it matters
This is the trace-order packaging of nonunit identity-branch transport inside PRC native-cost uniqueness. Downstream, it is shown equivalent to global nonunit identity-branch transport (both directions of the iff), and it is recovered from prime-comparable identity respect and from prime-floor successor transport. It also feeds the reverse implication that comparable-trace nonunit identity yields prime-floor orbit identity successor transport, and appears in the native-cost uniqueness blocker certificate.
In the Recognition forcing chain this sits under the uniqueness apparatus for the native cost (the $J$-shaped cost forced at T5 via the Recognition Composition Law). Exposing transport as a trace-order law isolates the next obligation: prove the order law from prime-local orientation and product-display compatibility, rather than assuming global branch transport outright.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.