PRCPrimeCalibrationForcesPrimeIdentityBranchUniformityTarget_iff_canonical_add_trace
plain-language theorem explainer
Equivalence of two prime-calibration targets for identity orientation: global branch uniformity on native prime axes, versus transport of identity orientation along canonical additive orbit-position traces. Downstream refutations and uniqueness certificates cite it to move a negative result from one formulation to the other. The proof is a two-constructor Iff packaging of the already-proved one-way implications.
Claim. The assertion that every prime-direction-calibrated ratio character is identity-branch-uniform on native prime axes is equivalent to the assertion that every such character transports identity orientation through the finite common extension given by the canonical additive orbit-position trace.
background
In the Primitive Recognition Calculus, ratio characters $\chi$ assign orbit data on the ratio-orbit space. A character is prime-direction calibrated when its native prime axes are oriented consistently with the identity branch of the cost. Two residual targets record what that calibration is still asked to force.
The branch-uniformity target asks that identity orientation on any native prime axis force every native prime axis onto the identity branch (a trace-free global condition). The canonical-add-trace target asks the same orientation to transport along the concrete finite common extension $\mathrm{orbitPositionTrace}(p+r)$. Both sit inside the native-cost uniqueness development, where J-cost uniqueness and d'Alembert structure for doubled traces are already in play.
The two one-way implications are already proved in-module: branch uniformity yields canonical-add-trace respect, and conversely canonical-add-trace respect yields branch uniformity, each by specializing the corresponding character-level lemma.
proof idea
Term-mode Iff introduction. The forward arrow is the existing theorem that branch uniformity implies the canonical-add-trace target; the reverse arrow is the existing theorem that the canonical-add-trace target implies branch uniformity. No new character-level work is done here.
why it matters
This bridge lets a refutation of branch uniformity become a refutation of the canonical-add-trace target (and conversely). The parent PRCPrimeCalibrationForcesPrimeIdentityCanonicalAddTraceTarget_refuted applies the reverse direction of the equivalence exactly that way. The same link is recorded in the native-cost uniqueness blocker certificate and is visible to the conditional universal-foundation certificate.
In the Recognition forcing chain this is bookkeeping inside the native-cost uniqueness layer that supports J-uniqueness (T5) and the Recognition Composition Law, not a new physical constant. It closes a formulation gap so that residual prime-identity targets can be treated as a single obstruction class.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.