PRCPrimeCalibratedTwoPrimeReciprocalIdentityNonTwoPrimeMixedCharacter_of_composite_defect
plain-language theorem explainer
A calibrated composite-defect character (with forced image χ(2p)=p/2) yields a calibrated mixed character: orbit 2 reciprocal and some non-2 prime identity-oriented. Character-rigidity and native-cost uniqueness arguments cite this direction of the equivalence. The proof unpacks the existential witness and applies the uncalibrated composite-to-mixed implication on the character component.
Claim. If there exists a ratio-orbit character $\chi$ that is prime-direction calibrated and exhibits the two-prime reciprocal / non-two composite defect (forced $\chi(2p)=p/2$), then there exists a ratio-orbit character that is prime-direction calibrated and mixed in the sharpened sense: orbit $2$ is reciprocal while some native prime $p\neq 2$ is identity-oriented.
background
In the Primitive Recognition Calculus, ratio-orbit characters $\chi:\mathrm{RatioOrbit}\to\mathrm{RatioOrbit}$ encode how multiplicative structure is read before native cost is recovered. Prime-direction calibration fixes the action on prime orbits so that cost comparisons stay on the native ladder. The mixed model asserts that orbit $2$ is reciprocal while some non-$2$ native prime is identity-oriented; the composite-defect model strengthens this by exposing the forced composite image $\chi(2p)=p/2$.
The module develops native-cost uniqueness by blocking non-rigid characters. The composite-defect character is the cost-visible form of the Pass-95 blocker; the mixed character is the sharpened calibrated two-adic axis-twist model used as the native valuation route against character rigidity.
Upstream, the uncalibrated implication already sends a composite-defect character to a mixed character by discarding the product witness and retaining the reciprocal-$2$ and identity-$p$ data.
proof idea
Term-mode unpacking of an existential. Destructure the composite-defect hypothesis into a witness $\chi$ together with the ratio-character, prime-direction calibration, and uncalibrated composite-defect facts. Reassemble the same $\chi$ with the same calibration hypotheses, replacing the composite-defect conjunct by the conclusion of PRCCharacterTwoPrimeReciprocalIdentityNonTwoPrimeMixed_of_composite_defect applied to that conjunct. No new arithmetic is performed at this layer.
why it matters
Supplies one direction of the calibrated mixed $\leftrightarrow$ composite-defect equivalence, which immediately feeds the iff theorem equating those two Props. That equivalence rewrites the prime-calibration exclusion target as the negation of the composite-defect character, closing a rigidity branch in native-cost uniqueness.
Downstream it is also consumed by the conditional universal-foundation certificate in UniversalFoundation, which packages kernel, real-complete ordered field, and trace-logic passes. Within Recognition Science this sits in the foundation layer that forces the unique native cost (the $J$-cost of the T5 uniqueness step) by eliminating twisted characters before the forcing chain proceeds to $\varphi$, the eight-tick octave, and $D=3$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.