PRCPrimeCalibrationForcesNonunitIdentityComparableTraceTarget_of_product_no_mixed
plain-language theorem explainer
Prime calibration that forbids mixed identity/reciprocal orientations under orbit products already forces identity orientation to respect finite δ-orbit trace comparability on nonunit directions. Anyone closing native-cost uniqueness or the product-no-mix ↔ comparable-trace equivalence cites this bridge. The proof is a two-step term composition through the branch-transport intermediate.
Claim. If prime calibration forces every ratio character to have no mixed identity/reciprocal factor orientations under native orbit multiplication, then prime calibration also forces identity orientation on nonunit directions to respect comparability of finite $\delta$-orbit traces.
background
In the Primitive Recognition Calculus, a ratio character $\chi$ assigns an orientation (identity versus reciprocal) to each ratio orbit. Prime-direction calibration is the standing hypothesis that $\chi$ is calibrated along prime directions. The product no-mixing target says that under native multiplication of orbits, a calibrated character never mixes identity and reciprocal factor orientations.
The nonunit identity comparable-trace target sharpens branch transport: once identity orientation is fixed on nonunit directions, it must respect the order coming from comparing finite $\delta$-orbit traces. The ambient module develops native-cost uniqueness: forcing the native cost functional from calibration axioms alone.
Upstream, product no-mixing already yields nonunit identity branch transport (coherent orientation transport across nonunit directions), and branch transport yields the comparable-trace property pointwise on characters.
proof idea
Pure term-mode composition of two existing implications. First apply the lemma that product no-mixing implies the nonunit identity branch-transport target. Then pass that result to the lemma that branch transport implies the comparable-trace target (which unpacks as a pointwise intro on $\chi$ and applies the character-level transport-to-trace lemma). No fresh case splits or arithmetic.
why it matters
Closes one direction of the biconditional equating product no-mixing with identity comparable-trace, so either formulation can stand for the other in the uniqueness ladder. Also supplies the comparable-trace hypothesis needed to obtain the prime-floor identity successor step-pair target from product no-mixing. Downstream, the native-cost uniqueness blocker certificate and the universal-foundation conditional certificate sit on this chain of calibration forcings. In the broader Recognition Science foundation, the work supports uniqueness of the native cost functional (the PRC route toward J-cost uniqueness in the T5 forcing step), rather than deriving a physical constant directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.