PRCCharacterPrimeIdentityBranchUniform_iff_canonical_add_trace
plain-language theorem explainer
Branch-uniform prime identity for a ratio-orbit character is equivalent to identity transport along the canonical add-trace merger of prime axes. Anyone tracking the native-cost uniqueness blocker cites this to collapse two formulations of the same obstruction. The proof is a two-constructor Iff package of the already-proved one-way implications.
Claim. For any map $\chi$ 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) identity orientation transports along the canonical finite $\delta$-trace merger $\mathrm{orbitPositionTrace}(p+r)$ of any two prime axes $p,r$.
background
In the Primitive Recognition Calculus, a RatioOrbit is a rational display: signed-orbit numerator over a nonzero distinction-nat denominator. Characters act on these orbits. Native prime axes are the prime-orbit directions; a character is identity-oriented on such an axis when $\chi$ fixes that direction up to the cross-equality relation on orbits.
Two formulations of the remaining prime-identity transport obstruction appear in this module. Branch uniformity says identity orientation on one native prime axis forces it on every other, with no trace data in the statement. The canonical-add-trace form requires that identity orientation transport through the specific finite common extension orbitPositionTrace(p+r), once both prime position traces extend into that merger. As the docs put it, the latter "removes the arbitrary witness from common-trace transport; the only remaining content is that the character respects the canonical finite $\delta$-trace merger of two prime axes."
The local setting is native-cost uniqueness for PRC characters: isolating what still blocks uniqueness of the native cost functional built from such characters.
proof idea
Term-mode Iff introduction. The forward direction is PRCCharacterPrimeIdentityRespectsCanonicalAddTrace_of_branch_uniform: given branch uniformity, the two Trace.Extends hypotheses on the canonical add-trace are ignored and identity transport is read off directly from uniformity. The reverse is PRCCharacterPrimeIdentityBranchUniform_of_canonical_add_trace: given the canonical-add-trace law, branch uniformity follows by applying that law (the extends premises are discharged in the one-way lemma's body, or left as free in the intro pattern shown). No new algebra; pure packaging of the two one-way theorems.
why it matters
This equivalence lets the native-cost uniqueness development treat branch uniformity and canonical-add-trace respect as interchangeable names for one blocker. Downstream it feeds prc_native_cost_uniqueness_blocker_certificate, which assembles the zero-calibrated factorization target and the refutation of the signed-admissible factorization target, and it is listed among the inputs to prc_universal_foundation_conditional_certificate in UniversalFoundation.
In the broader Recognition Science chain, native cost uniqueness is the PRC-side route toward the unique J-cost of T5 ($J(x)=(x+x^{-1})/2-1$) and the Recognition Composition Law. Clearing or certifying this prime-identity transport obstruction is a concrete step on that path: once characters that fix one prime axis must fix all, the admissible character class collapses toward the canonical cost. The declaration itself does not finish uniqueness; it only identifies two faces of the same remaining obstruction so certificates can cite either form.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.