PRCPrimeCalibrationForcesPrimePairProductCostConsistencyTarget
plain-language theorem explainer
Defines the product-calibration target: every prime-direction-calibrated ratio character must match native cost on products of any two prime directions (via cross-multiplication equality of ratio orbits). Cited throughout the native-cost uniqueness chain as the composite surface that forces coherent prime orientation and rules out mixed-prime witnesses. Pure Prop packaging; no proof content.
Claim. The following proposition holds as a named target: for every map $\chi$ from ratio orbits to ratio orbits that is a PRC ratio character and is prime-direction calibrated, and for every pair of prime distinction-orbits $p,r$, the character-induced cost of the product of the corresponding prime directions is cross-multiplication-equivalent to the native on-orbit cost of that same product.
background
In the Primitive Recognition Calculus, a ratio orbit is a signed-orbit numerator over a nonzero distinction-orbit denominator. Two ratio orbits are identified by cross-multiplication equality (crossEq): the scaled numerators balance as signed orbits. This is the internal PRC stand-in for rational equality.
A ratio character $\chi$ assigns to each ratio orbit another ratio orbit; when it is prime-direction calibrated, its values on native prime directions are fixed to the calibration data. The character induces a cost via costFromCharacter. The native comparison surface is the on-orbit cost of a ratio orbit. Recognition costs elsewhere in the monolith are J-costs (or doubled J under ratio weights); here the comparison is purely orbit-level via cross-equality.
The module packages native-cost uniqueness targets. This definition isolates the composite surface: calibration on primes must propagate to prime-pair products. The doc-comment flags the $2\cdot p$ mixed-orientation instance as the present branch-rigidity blocker.
proof idea
No proof: the declaration is a bare Prop abbreviation. The body is a universal quantification over characters and prime pairs, asserting crossEq between character-cost and native on-orbit cost of the mul of the two prime directions. Downstream theorems treat the name as a hypothesis or as one side of an iff.
why it matters
This target is the hinge of the prime-calibration uniqueness ladder in PRCNativeCostUniqueness. Downstream, it is equivalent to full admissibility of every prime-calibrated ratio character, to coherent prime orientation, to absence of mixed prime-pair witness characters, and to mixed-composite cost consistency. From it one derives no mixed-prime witnesses and absurdity of two-adic axis-twist characters; its negation yields a mixed-prime-witness character.
In framework terms it is the composite check that prime calibration (local on prime directions) forces global cost agreement on the multiplicative semigroup they generate. That agreement is what pins the native cost to the unique J-shape on the rational orbit display, feeding the T5 J-uniqueness story at the PRC layer. The doc-comment’s $2\cdot p$ mixed-orientation case is the remaining rigidity choke point the surrounding iff chain is built to discharge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.