PRCPrimeCalibrationForcesOrbitProductNoMixedOrientationTarget
plain-language theorem explainer
Open target Prop: every prime-direction-calibrated ratio character has no mixed identity/reciprocal orientations on nonunit product factors. Downstream uniqueness blockers and orientation-coherence lemmas cite it as a single hypothesis. Pure definition packaging an implication; no proof content.
Claim. For every map $\chi$ from ratio orbits to 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), product factors cannot mix identity and reciprocal orientations under native multiplication of nonunit factors.
background
In the Primitive Recognition Calculus, costs live on ratio orbits: integer-numerator displays over nonzero orbit denominators, compared by cross-equivalence rather than definitional equality. A ratio character $\chi$ is a candidate d'Alembert factor of a native cost: it fixes the unit orbit and is multiplicative up to cross-equivalence.
Prime-direction calibration asks that the cost generated from $\chi$ agree with the canonical $J$-cost on every prime orbit. The product no-mixed-orientation predicate is the residual obstruction after same-orientation product algebra is discharged: nonunit factors must not pair one identity-oriented factor with one reciprocal-oriented factor.
Ledger reciprocity ($J(x)=J(x^{-1})$) already forces cost symmetry; the open question is whether prime calibration alone forces the character's orientation data to be coherent enough that mixed product factors are impossible.
proof idea
Definitional packaging only. The body is the universal implication $\forall\chi,;\mathrm{RatioCharacter}(\chi)\to\mathrm{PrimeCalibrated}(\chi)\to\mathrm{ProductNoMixedOrientation}(\chi)$. No tactics, no lemmas applied; the Prop is the claim interface consumed by later reduction theorems.
why it matters
Native cost uniqueness (the PRC route toward T5 $J$-uniqueness) is not closed; the Pass-25 blocker certificate splits the gap into exact Lean targets, and this is the product no-mixing node. Many parent targets reduce to it: no-mixed nonunit orbit orientation, nonunit orbit orientation coherence, identity branch transport, identity witness globalization, and comparable-trace targets all have _of_product_no_mixed wrappers that assume this Prop and discharge the stronger claim.
Once proved, mixed product factors become impossible by nonunit non-self-reciprocity, unlocking a single coherent orientation across nonunit directions and feeding the factorization half of native cost uniqueness. Until then it remains an explicit open interface rather than a silent sorry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.