PRCCharacterPrimeIdentityWitnessGlobalizesNonunit
plain-language theorem explainer
Prime identity witness globalization packages the claim that if any prime axis of a ratio-orbit character lands on the identity branch (cross-equivalent to itself), then identity orientation propagates to every nonzero nonunit orbit direction. Native-cost uniqueness certificates and no-mixed-prime-witness lemmas cite it as a named hypothesis. The body is a pure Prop quantifier chain, not a proved theorem.
Claim. Let $\chi$ map ratio orbits to ratio orbits. The prime-identity-witness globalization property asserts: if there exists a prime distinction orbit $p$ such that $\chi$ sends the prime direction of $p$ to a ratio orbit cross-equivalent to that same prime direction, then for every nonzero nonunit distinction orbit $r$, $\chi$ has identity orientation on the direction of $r$.
background
In the Primitive Recognition Calculus (PRC), distinction naturals are the base-neutral finite orbits of repeated distinction acts. A prime orbit is a nonzero, nonunit position with no nontrivial factorization. Ratio orbits display signed integer numerators over nonzero distinction denominators; cross-equivalence is the internal PRC rational relation via balanced scaled numerators (cross-multiplication on $\delta$-orbit positions).
A ratio character $\chi$ reorients these displays. The identity event in observer forcing sits at the J-cost minimum $x=1$. Orbit-direction identity for $\chi$ at $r$ means $\chi$ fixes the direction of $r$ on the identity branch. The module develops native-cost uniqueness by forcing characters that match the doubled-trace cost to be the canonical J-cost character; prime axes are the calibration hinges.
Upstream, primeOrbit, crossEq, and RatioOrbit supply the arithmetic language; identity orientation is the local predicate this globalizes.
proof idea
Definitional Prop, not a proved theorem. The body is a nested universal quantifier: for every prime $p$ with a prime-orbit witness, if $\chi$ of the prime direction is cross-equivalent to that prime direction, then for every nonzero nonunit $r$ the orbit-direction identity predicate holds for $\chi$ at $r$. No tactics or lemmas are applied; downstream theorems discharge or assume this Prop as a named hypothesis.
why it matters
This is a named blocker target in the native-cost uniqueness program. Downstream, no-mixed-prime-witnesses follows from it, and conversely (under character, product-display compatibility, and prime-local orientation) the two are equivalent. Prime-floor successor transport also implies it, and it is re-exported as the witness-globalized form of the prime-floor blocker: if any calibrated prime axis picks identity, every nonunit direction must pick identity.
It sits inside the Pass-25 uniqueness certificate structure that splits remaining gaps into exact Lean targets. In the broader Recognition chain this supports uniqueness of the native cost matching the T5 J-cost $J(x)=(x+x^{-1})/2-1$, by ruling out characters that flip some primes to identity while leaving other nonunit directions non-identity. The complementary no-prime-identity case is handled by a separate prime-witness reflection lemma.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.