PRCCharacterTwoPrimeReciprocalIdentityNonTwoCompositeDefect
plain-language theorem explainer
Packages the composite-defect obstruction for ratio characters: if χ sends the 2-orbit to its reciprocal and some native prime p≠2 to the identity, then it must send the composite direction 2p to the mixed value p/2. Uniqueness proofs cite it to equate mixed-branch and cost-defect forms. It is a bare Prop definition (three cross-equality clauses), not a proved statement.
Claim. A map $\chi$ on ratio orbits has the composite-defect property when $\chi$ sends the direction of $2$ to its reciprocal and there exists a native prime orbit $p\neq 2$ such that $\chi$ fixes the direction of $p$ and sends the composite direction $2\cdot p$ to the mixed orbit $p/2$ (all equalities via cross-multiplication of orbit displays).
background
In the Primitive Recognition Calculus, rational comparisons live on RatioOrbit: a signed-orbit numerator over a nonzero distinction-nat denominator. Two such displays are identified by crossEq, the internal cross-multiplication relation (K4.10): numerators and denominators balance after scaling, matching ordinary rational equality on verifier displays.
A ratio character is a map $\chi$ on these orbits. Native cost uniqueness aims to force any admissible character to reproduce the J-cost (defect) calibration. The classical J-cost is $J(x)=(x+x^{-1})/2-1$, forced uniquely in the T5 step of the forcing chain; defect equals J on positives. The present Prop isolates one obstruction branch: reciprocal action on the prime-2 direction, identity on a distinct native prime $p$, and the forced mixed image on the composite $2p$.
Upstream cost defs (rung coarsen, multiplicative recognizer, observer forcing) all reduce recognition cost to this same J/defect functional; the character-side Prop is the orbit-native packaging of the corresponding mismatch.
proof idea
Definition only: the body is the conjunction of (i) cross-equality of $\chi(2)$ with the reciprocal of the 2-direction, (ii) existence of a prime orbit $p\neq 2$ fixed by $\chi$, and (iii) cross-equality of $\chi(2\cdot p)$ with the product of the reciprocal of 2 and the $p$-direction. No tactics, no lemmas discharged.
why it matters
Closes the composite-defect side of the non-two mixed branch in PRC native cost uniqueness. Downstream, it is equivalent (under a ratio-character hypothesis) to the mixed-branch Prop, and equivalent to the cost-visible composite defect that asserts the mixed image is not J-calibrated at $2p$. Conversion theorems (_of_non_two_mixed, _of_cost_defect, the iff forms, and the cost-defect lift) all unpack this definition. It also appears among the open targets of PRCUniversalFoundationOpenTargets.
Framework role: supports the uniqueness path toward the forced J-cost (T5 / RCL), by ruling out characters that flip only the 2-branch while fixing another prime. Without packaging the composite image $p/2$, the mixed obstruction would not connect cleanly to cost defect at composite directions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.