PRCPrimeCalibrationForcesNonunitIdentityBranchTransportTarget
plain-language theorem explainer
Packages the open target that every prime-calibrated ratio character must transport identity orientation from one nonunit direction to all nonunit directions. Native-cost uniqueness work cites it as the positive branch-coupling blocker. The body is a pure Prop abbreviation: character axioms plus prime calibration imply the nonunit identity-branch transport law.
Claim. Every map $\chi$ on ratio orbits that is a ratio character (unit-preserving and multiplicative up to cross-equivalence) and is calibrated on every native prime direction (its generated cost matches canonical $J$-cost on each prime orbit) satisfies nonunit identity-branch transport: if any nonunit direction is identity-oriented under $\chi$, then every nonunit direction is identity-oriented.
background
In the primitive recognition calculus, costs factor through ratio characters on RatioOrbit (signed numerator over a nonzero distinction denominator). A ratio character $\chi$ is quotient-native: it fixes the unit orbit and is multiplicative up to cross-equivalence, the native equality on orbits.
Prime-direction calibration demands that the cost generated from $\chi$ agrees with the canonical $J$-cost on every prime orbit. The identity event is the $J$-minimum at state $1$. Nonunit identity-branch transport is the positive form of branch coupling: once one nonunit direction is identity-oriented, that orientation must hold for every nonunit direction (the same law as no-mixing, stated as transport).
This module isolates exact Lean targets for the still-open native cost uniqueness argument; the present definition is one such target Prop.
proof idea
Definitional packaging only. The Prop is the universal quantification over maps $\chi$ of the implication chain: ratio-character axioms, then prime-direction calibration, then the already-defined nonunit identity-branch transport predicate on $\chi$. No tactics or lemmas are invoked in the body.
why it matters
This is the positive-transport half of the branch-coupling blocker in the Pass-25 native cost uniqueness certificate. Downstream it is conjoined with the reciprocal-transport target into the pair target, and it appears in the blocker certificate structure that records which uniqueness subgoals remain open.
Several discharge routes are already wired: from branch agreement, from nonunit orbit-orientation coherence, from comparable-trace sharpening, and from identity-witness globalization. An iff with the comparable-trace form is proved. Closing any of those upstream targets would settle this one and advance the uniqueness chain toward the forced $J$-cost (T5) factorization at the ratio-orbit level.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.