PRCPrimeCalibrationForcesNonunitIdentityComparableTraceTarget_of_branch_transport
plain-language theorem explainer
Prime calibration that forces identity-branch transport on nonunit directions also forces the stronger comparable-trace form of that constraint. Anyone closing the native-cost uniqueness blocker chain cites this implication. The proof unpacks the universal quantifiers and applies the character-level transport-to-trace lemma.
Claim. If every ratio character that is prime-direction calibrated has the property that an identity-oriented nonunit direction transports its identity branch to every other nonunit direction, then every such character also has the property that identity orientation respects comparability of finite $\delta$-orbit traces on nonunit directions.
background
In the Primitive Recognition Calculus, ratio characters $\chi$ map ratio orbits to ratio orbits and encode branch choices (identity versus reciprocal) along directions. Prime-direction calibration restricts how $\chi$ may act on prime generators. Two blocker targets package the same branch-coupling demand at different strengths.
The branch-transport target asserts: whenever prime calibration leaves one nonunit direction identity-oriented, that identity branch must transport to every nonunit direction. The comparable-trace target sharpens this: identity orientation must respect comparability of finite $\delta$-orbit traces on nonunit directions. At the character level, the lemma that nonunit identity branch transport implies respect for comparable traces is already available.
proof idea
One-line unpacking wrapper. Introduce a ratio character $\chi$ together with the hypotheses that it is a PRC ratio character and is prime-direction calibrated. Apply the assumed branch-transport target to obtain nonunit identity branch transport for $\chi$, then feed that into the character-level lemma which converts branch transport into respect for comparable traces.
why it matters
This implication is one direction of the equivalence between the branch-transport and comparable-trace blocker targets, and it is the bridge used when the product-no-mixed-orientation target is reduced to the comparable-trace form. Both feed the native-cost uniqueness blocker certificate that packages the zero-calibrated factorization results. Within Recognition Science foundation work, these blockers constrain which characters can serve as native costs, supporting the uniqueness path toward the J-cost forced by T5 in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.