PRCPrimeCalibratedTwoPrimeReciprocalIdentityNonTwoPrimeMixedCharacter_iff_composite_defect
plain-language theorem explainer
The calibrated mixed-character model (orbit 2 reciprocal, a non-2 native prime identity-oriented) is equivalent to the calibrated composite-defect model that forces χ(2·p)=p/2. Anyone tracking the character-rigidity branch of native cost uniqueness cites this bridge. The proof is a pure Iff constructor pairing the two already-proved one-way implications.
Claim. The following are equivalent: (i) there exists a ratio-orbit character $\chi$ that is prime-direction calibrated and mixed in the sense that orbit $2$ is reciprocal while some non-$2$ native prime is identity-oriented; (ii) there exists a ratio-orbit character $\chi$ that is prime-direction calibrated and exhibits the composite defect $\chi(2\cdot p)=p/2$ for a non-$2$ native prime $p$.
background
In the Primitive Recognition Calculus, ratio-orbit characters $\chi:\mathrm{RatioOrbit}\to\mathrm{RatioOrbit}$ encode how multiplicative structure is read before the native cost is recovered. A character is prime-direction calibrated when its action on prime orbits is fixed to a preferred orientation; the two-adic orbit is special because reciprocal versus identity orientation on $2$ changes the composite images.
The mixed-character model asserts existence of a calibrated $\chi$ with orbit $2$ reciprocal and some non-$2$ native prime identity-oriented. The composite-defect model is the same package with the forced image $\chi(2\cdot p)=p/2$ made explicit; that image is the cost-visible failure mode used to refute character rigidity.
Both sides live in the native-cost uniqueness module, which isolates whether non-J characters can still satisfy the doubled-trace and d'Alembert constraints that force the Recognition Composition Law cost $J(x)=(x+x^{-1})/2-1$.
proof idea
Term-mode Iff introduction. The forward arrow is the existing lemma that any calibrated non-two mixed character yields a calibrated composite-defect character (by exposing $\chi(2\cdot p)=p/2$). The reverse arrow is the existing lemma that any calibrated composite-defect character yields a calibrated non-two mixed character (by reading the mixed orientation off the same witness). No new algebraic work is done here; the declaration only packages the two directions.
why it matters
This equivalence collapses two presentations of the same blocker on the character-rigidity branch: the mixed-orientation witness and the cost-visible composite defect. Downstream, the universal foundation conditional certificate assembles kernel, real-complete ordered field, and trace-logic certificates; having a single iff means either formulation can be discharged without re-proving transport. In the broader forcing chain the target is uniqueness of $J$ (T5) under the Recognition Composition Law; composite defects of the form $\chi(2\cdot p)=p/2$ are exactly the non-$J$ images that must be ruled out before native cost uniqueness closes. The declaration does not itself kill the blocker; it only identifies the two models so later passes can attack one surface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.