PRCCharacterPrimeIdentityWitnessGlobalizesNonunit_of_prime_floor_successor_transport
plain-language theorem explainer
If a ratio-orbit character obeys prime-floor identity successor transport, then identity on any prime axis forces identity on every nonunit orbit direction. Native-cost uniqueness proofs cite this to globalize a single prime calibration. The argument case-splits on orbit size and applies the one-sided le/ge transport lemmas.
Claim. Let $\chi$ map ratio orbits to ratio orbits. Suppose $\chi$ satisfies prime-floor identity successor transport: identity orientation both extends and contracts under one $\delta$-successor step once the path is above the self-reciprocal unit orbit. Then, whenever a prime orbit $p$ has $\chi$ fixing the prime direction of $p$ (cross-equality to the identity branch), every nonunit nonzero orbit $r$ likewise has $\chi$ identity-oriented on the direction of $r$.
background
In the Primitive Recognition Calculus, ratio orbits are rational displays: a signed-orbit numerator over a nonzero distinction-orbit denominator. A character $\chi$ acts on these orbits; identity orientation at a nonzero orbit $r$ means $\chi$ fixes the corresponding orbit direction up to cross-equality.
Prime identity witness globalization is the statement that once any calibrated prime axis sits on the identity branch, that identity choice propagates to every nonunit orbit direction (the pure no-prime-identity case is handled by a separate reflection lemma).
The hypothesis packages the corrected successor-transport rule: identity orientation transports along one $\delta$-successor step only above the unit orbit, both extending and contracting. That is the exact layer needed for prime-to-prime trace coherence. Orbit comparison uses the total order on verifier Nats via toNat, so any two nonzero orbits are comparable by size.
proof idea
Tactic proof by introduction and case split. From the prime identity hypothesis, rewrite to identity orientation at the prime direction. Compare $p$ and $r$ by Nat.le_total on their toNat values.
If $p\le r$, apply the le-side lemma: identity at a nonunit prime floor plus successor transport yields identity at $r$. If $r\le p$, apply the ge-side lemma (which also uses that $r$ is nonunit). Both sides are already proved from the same successor-transport package; this theorem only glues them into the global nonunit statement.
why it matters
Native cost uniqueness in PRC needs identity orientation to spread from a single calibrated prime to the whole nonunit lattice; without that, competing characters could disagree off the prime axes and spoil uniqueness of the doubled-trace cost (the J-cost side of T5).
Downstream, the prime-calibration forcing theorem applies this result directly: once calibration forces prime-floor successor transport, globalization of the prime identity witness follows in one line. That target feeds the native-cost uniqueness blocker certificate, which records the proved factorization and refuted signed-admissible alternatives.
In the forcing chain this sits under T5 J-uniqueness and the Recognition Composition Law: characters that preserve the d'Alembert/trace structure must be the identity branch once a prime is fixed, so the native cost is forced.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.