PRCCharacterTwoPrimeReciprocalIdentityNonTwoCompositeDefect_of_non_two_mixed
plain-language theorem explainer
Any ratio-orbit character that is reciprocal on the orbit-2 axis and identity on a distinct native prime p must send the composite direction 2p to the mixed value p/2. Cost-uniqueness arguments cite this to convert the mixed-branch hypothesis into an explicit composite-defect obstruction. The proof is a short crossEq chain: multiplicativity of the character plus congruence of the two axis images.
Claim. Let $\chi$ be a ratio-orbit character (unit-preserving, multiplicative, and reciprocal up to cross-equivalence). If $\chi$ sends the orbit-$2$ direction to its reciprocal and sends some native prime direction $p\neq 2$ to itself, then $\chi$ also sends the composite direction $2\cdot p$ to the mixed value $p/2$ (again up to cross-equivalence).
background
In the Primitive Recognition Calculus, rational data live on RatioOrbit: signed-orbit numerators over nonzero distinction-nat denominators. Equality is the internal cross-multiplication relation crossEq (K4.10), not definitional equality, so statements stay quotient-native.
A PRCRatioCharacter is a map $\chi$ on ratio orbits that preserves the unit, multiplies, and takes reciprocals, all up to crossEq. It is the candidate d'Alembert factor for a native PRC cost.
The mixed-branch hypothesis says $\chi$ is reciprocal on the distinguished two-prime axis and identity on some other native prime axis $p$. The composite-defect form strengthens that by requiring $\chi(2\cdot p)$ to equal the mixed product $(\mathrm{recip},2)\cdot p$, i.e. the $p/2$ direction. Upstream, crossEq is transitive via an integer-bridge cancellation, and characters supply multiplicativity on every pair of orbits.
proof idea
Destructure the mixed hypothesis into the two-axis reciprocal fact, a prime witness $p\neq 2$, and the identity fact on that prime axis.
Apply character multiplicativity to the pair (two-prime direction, prime-$p$ direction) to obtain
$\chi(2\cdot p)\sim\chi(2)\cdot\chi(p)$ under crossEq.
Congruence of multiplication under the two axis images then rewrites the right-hand side as $(\mathrm{recip},2)\cdot p$.
Transitivity of crossEq glues the two steps, and the resulting package is exactly the composite-defect predicate.
why it matters
This lemma is the forward half of the iff that equates the non-two mixed branch with its composite-defect form for any ratio character. Downstream, the prime-calibrated lift uses it to promote mixed characters to composite-defect characters, and the no-composite-cost-defect route feeds the forcing target that prime calibration cannot sustain a two-prime mixed composite cost inconsistency.
In the Recognition stack this sits inside native cost uniqueness for the PRC d'Alembert factorization: mixed reciprocal/identity assignments on prime axes are not free; multiplicativity forces a concrete composite value. That obstruction is part of pinning the admissible cost characters that ultimately support J-uniqueness (T5) and the forced self-similar scale $\varphi$ (T6) once the native cost is identified with the J-cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.