PRCPrimeCalibrationForcesNonunitOrbitProductLocalOrientationTarget
plain-language theorem explainer
Packages the claim that every prime-calibrated ratio character must propagate local identity-or-reciprocal orientation through products of nonunit orbit factors. Native-cost uniqueness work cites it as an exact Lean target on the path from prime-axis calibration to composite orbit orientation. Pure Prop definition (universal quantification), not a theorem; downstream the target is refuted.
Claim. For every map $\chi$ from ratio orbits to ratio orbits: if $\chi$ is a ratio character (preserves the unit and is multiplicative up to cross-equivalence) and is calibrated on every native prime direction (its induced cost matches canonical $J$-cost on each prime orbit), then $\chi$ propagates local orientation through products of nonunit factors.
background
In the Primitive Recognition Calculus, costs are reconstructed from ratio characters on RatioOrbit (integer numerator over nonzero orbit denominator). A ratio character $\chi$ is quotient-native: it preserves the unit and multiplies up to cross-equivalence rather than definitional equality. Prime-direction calibration means the cost generated by $\chi$ agrees with the canonical $J$-cost on every prime orbit direction.
Product-factor local orientation propagation is the multiplicative step that lifts identity-or-reciprocal orientation from two nonunit factors to their product. It is exactly the bridge from prime-axis orientation to composite orbit positions. The ambient module develops native cost uniqueness via d'Alembert factorization of PRC costs, tying characters to the Recognition Composition Law and the unique $J(x)=(x+x^{-1})/2-1$ of the forcing chain (T5).
proof idea
Definitional packaging only: the body is the universal quantification $\forall\chi,;\mathrm{RatioCharacter}(\chi)\to\mathrm{PrimeCalibrated}(\chi)\to\mathrm{ProductLocalOrientationPropagates}(\chi)$. No tactics, no lemmas applied. Downstream bridge lemmas assume this Prop as a hypothesis and discharge the weaker nonunit-orbit local-orientation target; a separate theorem refutes the Prop outright.
why it matters
Sits on the native-cost uniqueness path: if prime calibration forced product-factor orientation propagation, composite nonunit local orientation would follow, tightening the route from prime $J$-calibration to full character uniqueness. Downstream, PRCPrimeCalibrationForcesNonunitOrbitLocalOrientationTarget_of_product_local_orientation reduces the coarser nonunit target to this one; display-compatible and identity-comparable-trace lemmas offer conditional discharges. The target is refuted (...Target_refuted), and that negation is recorded in PRCNativeCostUniquenessBlockerCertificate and PRCUniversalFoundationOpenTargets. Framework landmark: T5 $J$-uniqueness and RCL factorization; the refutation closes a false forcing route rather than proving uniqueness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.