PRCPrimeCalibrationForcesTwoPrimeMixedCompositeCostConsistencyTarget_of_no_composite_cost_defect
plain-language theorem explainer
Absence of a prime-calibrated ratio character with a cost-visible mixed composite defect implies the universal consistency target: prime calibration forces J-cost agreement on the composite direction 2p even when orbit 2 is reciprocal and a distinct prime p is identity-oriented. Native-cost uniqueness arguments cite this as one half of the equivalence between that target and nonexistence of the defect model. The proof is a short contradiction that packages the mixed data into the calibrated defect character.
Claim. If there is no ratio character that is prime-direction calibrated and exhibits a cost-visible composite defect at $2\cdot p$ under mixed orientations (orbit $2$ reciprocal, distinct prime $p$ identity), then every prime-calibrated ratio character sending the direction of $2$ to its reciprocal must $J$-cost-calibrate the composite direction $2\cdot p$ for every distinct native prime $p$.
background
In the Primitive Recognition Calculus, a ratio character is a map on ratio orbits that encodes orientation data for prime and composite directions. Prime-direction calibration requires that native primes land on identity-oriented orbits in a controlled way. The mixed orientation package sends the direction of $2$ to its reciprocal while sending a distinct native prime $p$ to the identity; the composite direction $2\cdot p$ is then the natural place to test cost consistency.
Cost visibility is measured by cross-equality of orbits against the native $J$-cost (the unique cost forced by the Recognition Composition Law, $J(x)=(x+x^{-1})/2-1$). A cost-visible composite defect is the failure of that cross-equality at $2\cdot p$ under the mixed data. The calibrated defect character packages existence of a ratio character that is both prime-calibrated and carries such a cost-visible defect; the doc-comment calls it the Pass 95 blocker rewritten to expose the actual composite $J$-cost failure.
The target proposition is the universal form of the blocker: prime calibration must still force $J$-cost agreement on $2\cdot p$ even under that mixed orientation data. Upstream lemmas lift mixed non-two data first to a plain composite defect, then to the cost-visible form used here.
proof idea
Term-mode proof by contradiction on the target. Fix a ratio character $\chi$ that is prime-calibrated, sends the direction of $2$ reciprocal, and carries an identity witness at a distinct native prime $p$. Assume the composite cost-consistency conclusion fails at $2\cdot p$.
Apply the upstream lift ...Defect_of_non_two_mixed to turn the mixed reciprocal/identity package into a plain composite defect, then ...CostDefect_of_composite_defect to obtain the cost-visible composite defect on $\chi$. Package $(\chi,$ character, prime calibration, cost defect$)$ into the calibrated defect character. That existential contradicts the hypothesis that no such character exists, closing the proof.
why it matters
This is one direction of the local equivalence between the mixed-composite cost-consistency target and nonexistence of the calibrated cost-defect character. The sibling iff theorem uses it as the right-to-left arrow; a further iff identifies the target with the reciprocal-excludes-prime-identity witness form. Downstream, prc_universal_foundation_conditional_certificate consumes this layer inside the conditional universal-foundation certificate.
In the Recognition framework the result is a native-cost uniqueness gate on the forcing chain: once $J$ is unique (T5) and the composition law is in force, prime calibration cannot tolerate a mixed-orientation composite cost break at $2\cdot p$. Closing that gate is part of showing the native cost is the only character-compatible cost on ratio orbits, which feeds the broader uniqueness story behind the phi-ladder and the eight-tick structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.