PRCCharacterPrimeIdentityBranchUniform_iff_identity_iff_two
plain-language theorem explainer
For a ratio-orbit character, branch-uniform identity transport across native prime axes is equivalent to the identity-iff-two normal form (identity on any prime axis iff identity on the orbit-2 axis). Anyone reducing prime-identity blockers in native cost uniqueness will cite this. The proof is a two-line Iff package of the already-proved one-sided implications.
Claim. Let $\chi$ be a map on rational orbits. The following are equivalent: (i) if any native prime axis is identity-oriented under $\chi$, then every native prime axis is; (ii) for every native prime axis $p$, $\chi$ is identity-oriented at $p$ if and only if it is identity-oriented at the distinguished orbit-$2$ prime axis.
background
In the Primitive Recognition Calculus, characters act on RatioOrbit displays (signed numerator over a nonzero distinction-nat denominator). Native prime axes are the prime-orbit directions; identity orientation means the character fixes that axis up to the cross-equality relation on orbits.
Two normal forms package the remaining prime-identity obstruction after trace construction is stripped out. Branch uniformity says identity orientation is all-or-nothing across native primes: identity at one forces identity at all. The identity-iff-two form pins that global choice to a single calibrated axis, the distinguished orbit-2 prime direction: identity at any prime is equivalent to identity at 2.
The module develops native cost uniqueness for PRC characters. These two props are the trace-free content of the prime identity transport blocker; the present declaration records that they are interchangeable.
proof idea
Term-mode Iff constructor. The forward direction applies PRCCharacterPrimeIdentityIffTwoPrimeIdentity_of_branch_uniform; the reverse applies PRCCharacterPrimeIdentityBranchUniform_of_identity_iff_two. No new algebra: each one-sided lemma already walks the quantifiers (any prime through the orbit-2 axis, or identity-at-p implies identity-at-r via the common 2-axis).
why it matters
Native cost uniqueness needs a clean handle on when identity orientation can jump between prime axes. Equating branch uniformity with the identity-iff-two normal form lets later certificates pick whichever packaging is convenient without re-proving transport.
Downstream, prc_universal_foundation_conditional_certificate in UniversalFoundation assembles kernel, real-complete ordered field, and trace-logic certificates; this equivalence sits in the uniqueness spine those certificates rely on when discharging prime-identity blockers.
In the broader Recognition forcing chain this is bookkeeping inside the J-cost / character layer (T5 uniqueness of $J(x)=(x+x^{-1})/2-1$), not a new physical constant. It closes a definitional gap so the conditional universal-foundation certificate can treat the two formulations as the same hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.