PRCPrimeCalibrationForcesTwoPrimeReciprocalExcludesPrimeIdentityWitnessTarget_iff_no_composite_cost_defect_character
plain-language theorem explainer
Equates the orbit-2 mixed-witness exclusion target with nonexistence of any prime-calibrated ratio character that carries both a two-prime reciprocal/identity mix and a non-two composite J-cost defect. Native-cost uniqueness and character-rigidity arguments cite this to swap between the exclusion Prop and the cost-visible Pass-95 blocker. Proof is a two-direction constructor via the plain-defect iff plus the two defect↔cost-defect conversions.
Claim. The following are equivalent: (i) every prime-direction-calibrated ratio character $\chi$ with reciprocal orientation on the orbit-$2$ prime axis excludes any identity-oriented native prime witness; (ii) there is no prime-calibrated ratio character that simultaneously realizes a two-prime reciprocal/identity mixed witness and a composite $J$-cost defect off the prime $2$.
background
In the Primitive Recognition Calculus, a ratio character $\chi$ is a map on ratio orbits that encodes how multiplicative structure is read by the recognition kernel. Prime-direction calibration fixes the orientation of each prime axis (identity versus reciprocal). The orbit-$2$ axis is special: the mixed-witness exclusion target asserts that if that axis is reciprocal-oriented, no identity-oriented native prime witness may coexist.
The opposing model is a calibrated character that carries both the two-prime reciprocal/identity mix and a composite defect. The cost-visible variant exposes the actual composite $J$-cost failure (the Pass 95 blocker), rather than a plain structural defect. Here $J$ is the unique cost from the Recognition Composition Law, $J(x)=(x+x^{-1})/2-1$.
An upstream plain-defect iff already equates the exclusion target with nonexistence of the non-cost composite-defect character. Two conversion lemmas identify the plain and cost-visible defect models, so the cost-visible form is interchangeable with the plain one under calibration.
proof idea
Term-mode constructor on the biconditional.
Forward: from the exclusion hypothesis and a cost-defect character, apply ...DefectCharacter_of_cost_defect to obtain a plain composite-defect character, then discharge by the plain iff (..._iff_no_composite_defect_character.mp).
Reverse: from nonexistence of any cost-defect character, feed the plain iff's .mpr a short intro that turns a plain defect into a cost defect via ...CostDefectCharacter_of_composite_defect, yielding the exclusion target.
No new arithmetic: pure Prop plumbing between the plain and cost-visible blockers.
why it matters
Closes the cost-visible side of the orbit-2 mixed-witness exclusion in the PRC native-cost uniqueness development. Downstream, ..._iff_no_non_two_composite_cost_defect_character chains this with the prime-identity forces two-prime-identity target, and ..._iff_mixed_composite_cost_consistency rephrases the same exclusion as mixed composite cost consistency. Both feed character-rigidity toward unique native $J$-cost (forcing-chain T5).
It is also a decl_use edge into prc_universal_foundation_conditional_certificate in UniversalFoundation, so the cost-defect formulation sits on the conditional certificate path for the PRC universal foundation. The open question it packages is whether any such calibrated cost-defect character exists: constructing one would refute the present rigidity route; proving none exist discharges the Pass 95 blocker in cost language.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.