PRCCharacterPrimeIdentityRespectsTraceConnected_iff_trace_coherence
plain-language theorem explainer
For a ratio-orbit character χ, identity orientation that transports along finite δ-trace links between prime axes is equivalent to global prime identity coherence: identity at one calibrated prime forces identity at every calibrated prime. Native-cost uniqueness and orientation-blocker arguments cite this collapse. The proof is a two-constructor Iff package of the two directed lemmas.
Claim. Let $\chi$ map ratio orbits to ratio orbits. The following are equivalent: (i) whenever two prime axes are joined by a finite $\delta$-trace component and $\chi$ orients the first axis as the identity, it orients the second as the identity; (ii) if $\chi$ orients any calibrated prime axis as the identity, then it orients every calibrated prime axis as the identity.
background
In the Primitive Recognition Calculus, a character $\chi$ assigns to each ratio orbit another orbit and is meant to encode orientation choices (identity versus reciprocal) along prime axes. The local ratio-character laws only constrain multiplication and reciprocal; they do not by themselves relate orientation choices on distinct primes.
Prime identity trace-coherence asserts the missing cross-prime rule in full strength: identity orientation at one calibrated prime forces identity orientation at every calibrated prime. The weaker transport form requires the same conclusion only when the two prime axes lie in a common finite $\delta$-trace component ("respects prime-axis trace connection").
The module develops native cost uniqueness from doubled-trace and d'Alembert structure on these characters. Collapsing the transport form with global coherence removes a connectivity hypothesis that would otherwise block uniqueness arguments.
proof idea
Term-mode Iff introduction. The forward direction is the existing lemma that global trace-coherence follows from the connected-transport form. The reverse direction is the existing lemma that connected transport follows from global coherence. No further rewriting or case analysis appears in the body.
why it matters
Native cost uniqueness needs a single, connectivity-free statement that identity orientation cannot be mixed across primes. This equivalence licenses using either formulation interchangeably when assembling the uniqueness blocker certificate (prc_native_cost_uniqueness_blocker_certificate), which packages zero-calibrated factorization targets and refutations of signed admissible factorizations.
In the broader Recognition chain, characters feed the J-cost uniqueness story (T5: $J(x)=(x+x^{-1})/2-1$) and the multiplicative recognizer calculus. Closing the cross-prime orientation gap is a local prerequisite before native cost can be forced unique on the phi-ladder side of the foundation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.