PRCPrimeCalibratedTwoPrimeReciprocalIdentityNonTwoCompositeCostDefectCharacter_absurd_of_mixed_composite_consistency
plain-language theorem explainer
Under prime calibration, mixed orientation data that sends the two-orbit reciprocal and a distinct native prime identity cannot produce a composite J-cost defect on the product direction. Anyone discharging the Pass 95 cost-visible blocker, or the mixed-composite consistency target, cites this. The argument unpacks the putative defect witness and applies the consistency target directly to its cost-failure clause.
Claim. Assume that every prime-calibrated ratio character $\chi$ which sends the two-orbit to its reciprocal and a distinct native prime $p$ to the identity also cost-calibrates the composite direction $2\cdot p$. Then there is no prime-calibrated ratio character that simultaneously carries those mixed orientations and fails the native J-cost identity on a non-two composite.
background
In the Primitive Recognition Calculus, a ratio character $\chi$ is a map on ratio orbits that encodes orientation data for prime and composite directions. Prime-direction calibration requires $\chi$ to act consistently on native prime orbits. The two-orbit is the distinguished even generator; its reciprocal orientation paired with an identity orientation on a distinct prime $p$ is the mixed-orientation regime.
The consistency target asserts a universal cost-visible constraint: under that mixed data, prime calibration must still calibrate the composite direction $2\cdot p$. The defect character is the dual existential model: a calibrated $\chi$ that realizes two-reciprocal plus prime-identity while the composite J-cost identity fails. The module develops native-cost uniqueness for the PRC cost functional (the J-cost of Recognition Science, $J(x)=(x+x^{-1})/2-1$), so these two Props are the positive and negative faces of the same blocker.
proof idea
One short unpacking argument. Introduce a hypothetical defect witness and destructure it to a ratio character $\chi$ that is a PRC ratio character, prime-direction calibrated, and carries the two-prime-reciprocal / non-two-composite cost-defect package. Further unpack that package to the two-reciprocal hypothesis, a prime $p\neq 2$ with identity orientation, and the composite cost-failure clause. Apply the assumed mixed-composite consistency target at exactly those data; the resulting cost-calibration fact contradicts the failure clause.
why it matters
This is one direction of the biconditional equating the mixed-composite consistency target with nonexistence of the calibrated composite-cost-defect character. That iff is the clean interface used when swapping between universal (forall-character) and existential-blocker language in the native-cost uniqueness development. It also feeds the bridge that identifies the reciprocal-excludes-prime-identity target with mixed-composite cost consistency, and appears in the conditional universal-foundation certificate.
In framework terms the result is a local obstruction to non-J cost functionals: mixed prime orientations cannot hide a composite J-cost failure once prime calibration is imposed. That sits under the T5 J-uniqueness landmark (the cost $J(x)=\cosh(\log x)-1$ forced by the Recognition Composition Law) inside the PRC native-cost uniqueness pass. Closing this blocker is part of making the cost functional unique before promoting the universal foundation certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.