PRCPrimeCalibrationForcesTwoPrimeMixedCompositeCostConsistencyTarget_not_iff_non_two_composite_cost_defect_character
plain-language theorem explainer
Negation of the mixed two-prime composite cost-consistency target is equivalent to existence of a prime-calibrated ratio character with a non-two composite J-cost defect. Anyone tracking the Pass-95 cost-visible blocker or the PRC uniqueness chain cites this dual form. The proof is a two-direction constructor that flips the already-proved positive iff.
Claim. The universal target "every prime-calibrated ratio character that sends the orbit-$2$ direction to its reciprocal and a distinct native prime $p$ to the identity must still calibrate the composite direction $2\cdot p$" fails if and only if there exists a prime-calibrated ratio character witnessing a composite $J$-cost defect under that mixed reciprocal/identity orientation.
background
In the Primitive Recognition Calculus, ratio characters $\chi$ map ratio orbits to ratio orbits and encode orientation data for cost. Prime-direction calibration requires $\chi$ to fix native prime directions in a controlled way. The mixed orientation of interest sends the orbit-$2$ direction to its reciprocal while sending a distinct native prime $p$ to the identity.
The consistency target asserts that, under those hypotheses, $\chi$ must still satisfy the cross-equality that calibrates the composite direction $2\cdot p$. The dual defect character is an existential model: a prime-calibrated $\chi$ that carries exactly that mixed orientation and fails the composite $J$-cost identity. Upstream, the positive biconditional already equates the target with nonexistence of any such defect character.
This module develops native-cost uniqueness for PRC: cost is forced by character data once prime calibration and d'Alembert/trace hypotheses are in place. The present statement is the negated packaging of that blocker equivalence.
proof idea
Term-mode proof by constructor on the biconditional.
Left-to-right: assume the target fails; argue by contradiction that a defect character is absent; feed that absence into the reverse direction of the upstream iff ...Target_iff_no_composite_cost_defect_character to recover the target, contradicting the assumption.
Right-to-left: assume a defect character and the target; apply the forward direction of the same upstream iff to obtain nonexistence of any defect character, then discharge against the assumed witness.
No new analytic content: pure classical flip of the already-proved positive equivalence.
why it matters
Gives the dual packaging of the cost-visible Pass-95 blocker: target failure is literally the existence of a calibrated mixed-orientation composite $J$-cost defect. Downstream, prc_universal_foundation_conditional_certificate in UniversalFoundation assembles kernel, real-complete ordered field, and trace-logic certificates; this dual form is available wherever the certificate chain needs the blocker stated existentially rather than universally.
In the broader Recognition forcing picture, native cost uniqueness feeds the J-cost story (T5 uniqueness of $J(x)=(x+x^{-1})/2-1$ and the Recognition Composition Law). Closing composite-direction consistency under mixed prime orientations is part of showing that character data cannot smuggle extra cost defects past prime calibration. The declaration itself is fully proved; it does not discharge the larger conditional certificate, only supplies one logical face of the blocker.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.