PRCCharacterTwoPrimeReciprocalIdentityNonTwoCompositeDefect_iff_cost_defect
plain-language theorem explainer
For ratio-orbit characters, the composite-defect obstruction (2 maps to reciprocal, a distinct native prime p maps to identity, forcing 2p to the mixed value p/2) is equivalent to its cost-visible form (that mixed image fails J-cost calibration at 2p). Cited when collapsing branch-obstruction language into native-cost uniqueness. Proof is a one-line Iff package of the two already-proved one-way implications.
Claim. For every map $\chi$ from rational orbits to rational orbits, the following are equivalent: (i) $\chi$ sends the prime direction $2$ to its reciprocal, sends some distinct native prime direction $p$ to itself, and sends the composite $2\cdot p$ to the mixed value $p/2$; (ii) those same branch conditions hold and the mixed composite image is not $J$-cost calibrated at the composite direction $2\cdot p$.
background
In the Primitive Recognition Calculus, a rational orbit is an integer-numerator display over a nonzero distinction-nat denominator (K4.7). Characters act on these orbits; the native cost uniqueness development tracks which branch choices (identity vs reciprocal on prime directions) are compatible with the J-cost calibration that Recognition Science forces via the Recognition Composition Law and T5 uniqueness of $J(x)=(x+x^{-1})/2-1$.
The composite-defect predicate records a mixed-branch obstruction: if $\chi$ sends the two-prime direction to the reciprocal branch and a distinct native prime $p$ to the identity branch, then the composite direction $2\cdot p$ is forced to the mixed value $p/2$. The cost-defect sibling strengthens the last clause to a cost-visible failure: that mixed composite image is not J-cost calibrated at $2\cdot p$.
Both one-way implications between these predicates are already proved in-module; this declaration only packages them as a biconditional so downstream certificates can switch languages freely.
proof idea
Term-mode Iff constructor. Introduce the character $\chi$, then supply the ordered pair of already-proved implications: composite-defect implies cost-defect, and cost-defect implies composite-defect. No new case analysis; the second direction simply drops the unused cost-calibration conjunct when unpacking the cost-defect hypothesis.
why it matters
Native-cost uniqueness must treat branch language and cost language as interchangeable when ruling out mixed reciprocal/identity assignments on the two-prime and a distinct prime. This biconditional is the switch. It is consumed by the conditional universal-foundation certificate in UniversalFoundation, which assembles kernel, real-complete ordered field, and trace-logic certificates into a single PRC foundation package. In the broader forcing chain it supports the T5 J-uniqueness story: only cost-calibrated characters survive, so mixed composite images of the $2$/$p$ type are excluded on cost grounds rather than by ad-hoc branch bookkeeping.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.