PRCCharacterTwoPrimeReciprocalIdentityNonTwoCompositeDefect_of_cost_defect
plain-language theorem explainer
Any ratio-orbit character with the cost-visible non-two composite defect also satisfies the plain composite-defect obstruction: reciprocal on the 2-direction, identity on a distinct native prime p, and mixed image on 2p. Cited when stripping J-cost calibration data from mixed-branch arguments. Proof is a one-line projection that discards the unused cost conjunct.
Claim. Let $\chi$ be a map on ratio orbits. If $\chi$ has the cost-visible composite defect (sends the $2$-direction to its reciprocal, sends some native prime direction $p\neq 2$ to itself, and fails $J$-cost calibration at the composite direction $2p$), then $\chi$ has the plain composite defect: the same reciprocal and identity branch data, with $\chi(2p)$ equal to the mixed value $p/2$.
background
In the Primitive Recognition Calculus, ratio orbits are rational displays: a signed numerator orbit over a nonzero distinction-nat denominator (K4.7). Characters here are maps $\chi$ on those orbits that record branch choices (identity vs reciprocal) along prime and composite directions.
The plain composite defect packages the mixed-branch obstruction: $\chi$ sends the $2$-direction to the reciprocal branch, a distinct native prime $p$ to the identity branch, and the composite direction $2p$ to the mixed value $p/2$. The cost-visible variant adds that the mixed composite image is not $J$-cost calibrated at $2p$.
This module develops native-cost uniqueness for such characters. The two defect Props differ only by that final cost conjunct; the present lemma is the forgetful direction between them.
proof idea
One-line projection. Unpack the cost-defect hypothesis as a dependent pair (reciprocal-on-2 data, witness prime $p$ with primality and $p\neq 2$, identity-on-$p$, mixed product image, and the cost-calibration failure). Repack the same fields without the final cost conjunct to inhabit the plain defect Prop. No arithmetic or orbit lemmas are invoked.
why it matters
Closes the easy half of the local equivalence between plain and cost-visible composite defects, which the sibling iff theorem packages both ways. Downstream, the prime-calibrated lift uses this forgetful step to promote cost-defect characters to plain-defect characters under prime calibration. That chain feeds prc_universal_foundation_conditional_certificate in UniversalFoundation, part of the PRC kernel and trace-logic certificate stack.
In framework terms this is bookkeeping inside native-cost uniqueness for characters, not a forcing-chain landmark (T5–T8). It keeps mixed-branch obstruction statements interchangeable whether or not $J$-cost calibration is tracked, so later uniqueness arguments can drop cost data without re-proving branch identities.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.