PRCCharacterTwoPrimeReciprocalIdentityNonTwoPrimeMixed_iff_composite_defect_of_character
plain-language theorem explainer
For any ratio-orbit character χ, the sharpened non-two mixed branch (orbit 2 reciprocal, some other native prime identity-oriented) is equivalent to the composite-defect form that also forces χ(2·p)=p/2. Cost-uniqueness and d'Alembert factorization arguments cite this to switch freely between the two obstruction packages. The proof is a pure Iff constructor from the two directed lemmas.
Claim. Let $\chi$ be a ratio-orbit character (unit-preserving, multiplicative, and reciprocal up to cross-equivalence). Then $\chi$ satisfies the sharpened mixed-branch configuration—$\chi$ sends the orbit-$2$ axis to its reciprocal and some native prime axis $p\neq 2$ to the identity—if and only if it satisfies the composite-defect form of that obstruction, which additionally requires $\chi(2\cdot p)=p/2$ up to cross-equivalence.
background
In the Primitive Recognition Calculus, costs are factored in d'Alembert style through ratio-orbit characters. A PRCRatioCharacter is a map $\chi$ on rational orbits that preserves the unit, multiplies, and sends reciprocals to reciprocals, all up to the quotient-native relation crossEq rather than definitional equality.
The mixed-branch package records a concrete obstruction pattern: $\chi$ twists the distinguished two-adic axis to the reciprocal branch while fixing some other native prime axis $p$ pointwise (identity orientation). The composite-defect package strengthens that pattern by demanding the forced value on the product direction $2\cdot p$: multiplicativity plus the two orientations already imply $\chi(2\cdot p)$ must land on the mixed value $p/2$.
Both packages live in the native-cost uniqueness development that classifies which characters can arise from a PRC cost. The character hypothesis is needed only one way: deriving the composite value from the mixed configuration uses multiplicativity of $\chi$.
proof idea
Term-mode Iff introduction. The forward arrow applies PRCCharacterTwoPrimeReciprocalIdentityNonTwoCompositeDefect_of_non_two_mixed, which unpacks the mixed witness $(2\mapsto\mathrm{recip},,p\mapsto\mathrm{id})$ and uses the character axioms (especially multiplicativity) to obtain the product identity $\chi(2\cdot p)=p/2$. The reverse arrow applies PRCCharacterTwoPrimeReciprocalIdentityNonTwoPrimeMixed_of_composite_defect, which simply drops the composite conjunct from the defect package; no character hypothesis is required. The two directed lemmas are packaged as $\langle\cdot,\cdot\rangle$.
why it matters
Native-cost uniqueness must rule out mixed branch characters that would spoil the forced J-cost factorization. Equating the sharpened mixed configuration with its composite-defect form lets later arguments quote whichever packaging is convenient: the short mixed witness when classifying axes, or the explicit $2\cdot p$ defect when comparing against the Recognition Composition Law and the unique J-cost $J(x)=(x+x^{-1})/2-1$ (forcing step T5).
Downstream, the universal foundation conditional certificate (prc_universal_foundation_conditional_certificate) consumes this equivalence as part of assembling the PRC kernel, ordered-field, and trace-logic bundle. Closing the mixed-branch obstruction cleanly is a prerequisite for claiming that every admissible native cost is the standard doubled-trace cost on ratio orbits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.