PRCPrimeCalibrationForcesPrimePairProductCostConsistencyTarget_iff_coherent_prime_orientation
plain-language theorem explainer
Prime-direction cost calibration propagates to products of any two native primes if and only if it forces one coherent orientation on every native prime axis. Branch-rigidity work in the Primitive Recognition Calculus cites this to collapse two blocker surfaces into one. The proof is a two-constructor term packaging the already-proved implications in each direction.
Claim. The following two propositions are equivalent. (i) Every ratio character that is prime-direction calibrated has cost consistent on the product of any two native prime directions (via the cross-equality of the character cost). (ii) Every such character has a single coherent orientation across all native prime axes.
background
In the Primitive Recognition Calculus, a ratio character $\chi$ is a map on ratio orbits that encodes how cost is read off multiplicative structure. Prime-direction calibration means $\chi$ already matches the native cost on each prime orbit direction. The product-calibration target asks that this match extend to products of any two such prime directions: the character cost on the product orbit must satisfy the cross-equality that native cost obeys.
The coherent-orientation target is the sharper orientation blocker: once primes are calibrated, mixed independent inversions of prime axes are forbidden; one global orientation must be chosen. Its doc-comment calls this the place where "mixed independent prime inversions must be ruled out." The product target is described as the natural composite surface whose $2\cdot p$ mixed-orientation instance is the current branch-rigidity blocker.
Both targets live in the native-cost uniqueness module, which aims to force the Recognition $J$-cost (and related doubled-trace structure) from prime calibration alone.
proof idea
Pure term proof of an iff. The forward direction applies the already-proved implication from product-cost consistency to coherent prime orientation (itself routed through a two-prime branch-control reduction). The reverse applies the already-proved implication from coherent orientation back to product-cost consistency, which introduces the two prime directions and checks cross-equality on their product. No new algebra is done here; the declaration only packages the two arrows as $\leftrightarrow$.
why it matters
Collapsing the product-calibration surface with the coherent-orientation blocker removes a duplicate obligation on the path to native-cost uniqueness. Downstream, the universal-foundation conditional certificate consumes this layer of the PRC stack (kernel, ordered field, trace logic) when assembling the foundation package. In framework terms this sits under the forcing chain toward $J$-uniqueness (T5) and the Recognition Composition Law: orientation coherence is exactly what stops independent prime inversions from spawning non-$J$ cost characters. The declaration does not close the blocker; it proves the two named targets are the same Prop, so discharging either discharges both.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.