PRCCharacterNonunitIdentityWitnessGlobalizes
plain-language theorem explainer
A character on ratio orbits is said to have a globalizing identity witness when a single nonunit, nonzero orbit direction on which the character acts as the identity forces every other nonunit nonzero direction to do the same. Cost-uniqueness arguments cite this as the witness form of identity branch transport. The body is a pure Prop abbreviation: an existential local identity premise implies a universal identity conclusion.
Claim. For a map $\chi$ on rational orbits, the following holds: if there exists a nonzero nonunit distinction $p$ such that $\chi$ is identity-oriented on the orbit direction of $p$, then for every nonzero nonunit distinction $r$, $\chi$ is identity-oriented on the orbit direction of $r$.
background
In the Primitive Recognition Calculus, DistinctionNat is the base-neutral finite orbit of repeated distinction (zero and successors). Its native unit predicate holds only for the one-step orbit. A RatioOrbit is an integer-numerator display over a nonzero distinction denominator.
Characters here are maps $\chi$ on ratio orbits. Identity orientation of a direction means the character acts as the identity branch on that orbit (as opposed to the reciprocal branch). The reciprocal automorphism and reciprocal recognition event swap source/target and invert the ratio; the canonical identity event sits at the J-cost minimum $x=1$.
This module develops native-cost uniqueness for PRC characters. The present definition packages the witness form of identity branch transport: one identity-oriented nonunit direction, if it exists, fixes the identity branch globally. Local orientation is not bundled into the statement.
proof idea
Definitional Prop, not a proved theorem. The body is the implication from an existential package (some nonzero nonunit $p$ with identity orientation of $\chi$ on $p$) to the universal statement (every nonzero nonunit $r$ has identity orientation). No tactics or lemmas are applied; downstream theorems treat the name as that implication and discharge or transport it by intro/exact against the related branch-transport predicate.
why it matters
This is the witness-shaped interface for identity branch coupling in native-cost uniqueness. Downstream it is shown equivalent to nonunit identity branch transport, and is recovered from orbit-orientation coherence and from local orientation plus reciprocal exclusion. It feeds the one-sided exclusion form (once any nonunit identity witness exists, no nonunit reciprocal witness can coexist) and appears in the native-cost uniqueness blocker certificate.
In the broader Recognition chain, characters and cost uniqueness sit under the forcing path that isolates the J-cost $J(x)=(x+x^{-1})/2-1$ (T5) and the Recognition Composition Law. Pinning the identity branch globally, rather than mixing identity and reciprocal on nonunit directions, is what lets a character-derived cost match the native doubled-trace cost without branch ambiguity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.