PRCPrimeCalibratedTwoPrimeReciprocalIdentityNonTwoCompositeDefectCharacter_of_non_two_mixed
plain-language theorem explainer
A prime-calibrated mixed character (orbit 2 reciprocal, some odd native prime identity-oriented) yields the calibrated composite-defect model that exposes χ(2p)=p/2. Anyone tracking the mixed↔defect equivalence or the prime-calibration exclusion target cites this. The proof unpacks the existential witness and applies the uncalibrated mixed-to-defect lemma on the character component.
Claim. If there exists a ratio-orbit character $\chi$ that is prime-direction calibrated and mixed in the two-prime sense (reciprocal on the orbit of $2$, identity-oriented on some native prime $p\neq 2$), then there exists such a calibrated $\chi$ realizing the composite defect, i.e. forcing the image $\chi(2\cdot p)=p/2$.
background
In the Primitive Recognition Calculus native-cost uniqueness development, ratio-orbit characters $\chi:\mathrm{RatioOrbit}\to\mathrm{RatioOrbit}$ encode orientation data on multiplicative orbits. Prime-direction calibration fixes how $\chi$ acts on native primes. The mixed model asserts that orbit $2$ is reciprocal while some non-$2$ native prime witness is identity-oriented.
The composite-defect model is the cost-visible sharpening of that blocker: it keeps the same calibration package but exposes the forced composite image $\chi(2\cdot p)=p/2$, which is the actual J-cost failure on a composite orbit. Both objects are existential packages (character + ratio-character axioms + calibration + the mixed or defect predicate).
Upstream, the uncalibrated lemma already converts a mixed character into a composite-defect character once the ratio-character hypotheses are in hand. This declaration lifts that conversion through the calibrated existential wrappers.
proof idea
Term-mode unpack-and-repack. Destructure the mixed calibrated package into witness $\chi$, ratio-character proof, prime-calibration proof, and the mixed predicate. Rebuild the composite-defect package with the same $\chi$, same ratio-character and calibration proofs, and obtain the defect predicate by applying PRCCharacterTwoPrimeReciprocalIdentityNonTwoCompositeDefect_of_non_two_mixed to the ratio-character and mixed components. No new arithmetic is done here.
why it matters
This is one direction of the calibrated mixed↔composite-defect equivalence, so it is the bridge that lets the development treat the Pass-95 mixed blocker and the cost-visible composite failure as interchangeable. Downstream it feeds the two-three local orientation failure route into the composite-defect character, the exclusion-target iff that says prime calibration forces two-prime reciprocity and excludes an identity witness exactly when no composite-defect character exists, and ultimately the conditional universal-foundation certificate.
In the broader Recognition forcing picture this sits inside native-cost uniqueness for the J-cost (T5 landmark $J(x)=(x+x^{-1})/2-1$ and the Recognition Composition Law): ruling out mixed/composite defects is part of forcing character rigidity so the native cost is unique. The declaration itself is only the calibrated packaging step, not the rigidity theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.