PRCCharacterTwoPrimeReciprocalIdentityNonTwoCompositeCostDefect_of_composite_defect
plain-language theorem explainer
A ratio-orbit character that sends the two-direction to its reciprocal, fixes a distinct native prime p, and maps the composite 2p to the mixed branch p/2 necessarily fails native J-cost calibration on that composite. Cited when promoting orbit-level mixed-branch defects to cost-visible defects in PRC native-cost uniqueness. Short term proof: cost-image congruence plus the mixed-image J-cost mismatch lemma.
Claim. Let $\chi$ be a map on ratio orbits. Suppose $\chi$ sends the two-prime direction to its reciprocal, fixes some distinct native prime direction $p$, and sends the composite direction $2\cdot p$ to the mixed value $p/2$. Then the cost extracted from $\chi$ fails to match the native $J$-cost $J(q)=((q+q^{-1})/2)-1$ at that composite direction.
background
In the Primitive Recognition Calculus, rational data live as RatioOrbit objects: signed-orbit numerators over nonzero distinction-nat denominators. Equality is the choice-free cross-multiplication relation crossEq (K4.10): two orbits match when scaled numerators balance. Reciprocals and products are total operations on these orbits.
The native cost is the ratio-orbit J-object onRatioOrbit, namely $J(q)=((q+q^{-1})/2)-1$. Characters $\chi:\mathrm{RatioOrbit}\to\mathrm{RatioOrbit}$ induce a cost via costFromCharacter. The composite-defect predicate records a mixed-branch obstruction: $\chi(2)=2^{-1}$, $\chi(p)=p$ for a native prime $p\neq 2$, and $\chi(2\cdot p)=p/2$. The cost-defect strengthening adds that this mixed image is not J-calibrated at $2\cdot p$.
This module develops uniqueness of the native cost among PRC characters. The present lemma is the one-way lift from orbit-level mixed defect to cost-visible defect on the non-two composite branch.
proof idea
Destructure the composite defect into the two-reciprocal clause, a witness prime $p\neq 2$ fixed by $\chi$, and the mixed product image $h_{\mathrm{prod}}$.
Apply onRatioOrbit_congr to $h_{\mathrm{prod}}$ to obtain that costFromCharacter $\chi$ at $2\cdot p$ is crossEq to $J$ of the mixed value $(\mathrm{recip},2)\cdot p$.
Repackage the same witnesses and discharge the cost-defect side condition by contradiction: if the character cost matched native $J$ at the composite, crossEq_symm and crossEq_trans would identify $J(p/2)$ with $J(2\cdot p)$, contradicting two_prime_composite_mixed_image_jcost_mismatch.
why it matters
Native-cost uniqueness for PRC characters must rule out mixed two-prime branches that look harmless at the orbit level but break J-calibration. This lemma supplies the cost-visible half of that obstruction on the non-two composite.
It is consumed by the biconditional equating composite defect with cost defect, by the prime-calibrated lift that packages a full character witness, and by the forcing theorem that, absent any such cost defect, prime calibration implies the two-prime mixed composite cost-consistency target. Those parents sit on the path that pins the unique native cost to the T5 J-cost $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$) forced by the Recognition Composition Law.
No scaffolding remains here: the claim is fully proved and only rearranges existing mismatch and congruence facts.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.