PRCPrimeCalibrationForcesNonunitIdentityBranchTransportTarget_refuted
plain-language theorem explainer
Refutes the positive-transport form of a branch-coupling blocker: prime-direction calibration of a ratio character does not force an identity-oriented nonunit branch to transport to every nonunit direction. Native-cost uniqueness and universal-foundation certificates cite this closure. The proof is a short reduction through an equivalence to the already-refuted comparable-trace form of the same target.
Claim. It is false that every ratio-orbit character $\chi$ that is prime-direction calibrated must send an identity-oriented nonunit branch to every nonunit direction (the positive branch-transport form of the prime-calibration branch-coupling claim).
background
In the Primitive Recognition Calculus, ratio characters are maps on ratio orbits that encode admissible multiplicative structure for native cost. Prime-direction calibration restricts how $\chi$ behaves on prime generators. The target proposition asserts a strong coupling: if any nonunit direction stays identity-oriented under that calibration, the identity branch must transport to all nonunit directions.
This module isolates uniqueness and blocker statements for native cost built from such characters (doubled-trace and d'Alembert structure appear among siblings). The transport target is one packaging of the same branch-coupling obstruction; a comparable-trace packaging is definitionally linked by an equivalence theorem in-module.
Upstream, the comparable-trace form of the target is already refuted, itself reduced to a prime-floor successor-transport refutation. The present declaration is the transport-side twin of that closure.
proof idea
Assume the branch-transport target. Apply the left-to-right direction of the in-module equivalence that identifies it with the comparable-trace target, then feed the resulting hypothesis to the already-proved refutation of the comparable-trace form. No new analytic work: pure propositional transport along the iff and the prior refutation.
why it matters
Closes one named packaging of the prime-calibration branch-coupling blocker in the native-cost uniqueness stack. Downstream, the witness-globalization and orbit-product no-mixed-orientation refutations reduce to this statement via their own transport equivalences. It also appears in the native-cost uniqueness blocker certificate and is visible to the conditional universal-foundation certificate.
In Recognition terms this is foundation hygiene, not a T5–T8 forcing step: it rules out a false forcing path that would over-couple identity branches under prime calibration, keeping the native-cost uniqueness story free of that obstruction. Parent certificates can then assemble proved factorizations and refuted signed-admissible alternatives without this transport claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.