PRCPrimeCalibrationForcesTwoPrimeReciprocalExcludesPrimeIdentityWitnessTarget_of_mixed_composite_cost_consistency_direct
plain-language theorem explainer
Mixed-composite cost consistency under prime calibration forces a rigidity law: if the orbit-2 axis is reciprocal-oriented, no native prime may be identity-oriented. Coherent-orientation and pair-product uniqueness routes cite it, as does the universal foundation certificate. The proof case-splits on the witness prime, getting a J-cost image mismatch on the composite 2p when the prime is not 2, and a self-reciprocal contradiction when it is.
Claim. Assume every ratio-orbit character that is prime-direction calibrated and sends the orbit-$2$ axis to its reciprocal still cost-calibrates every mixed composite direction $2\cdot p$ for distinct native primes $p$. Then no such character admits an identity-oriented native prime witness: reciprocal orientation of orbit $2$ excludes identity orientation on every native prime direction.
background
In the Primitive Recognition Calculus, ratio data live on RatioOrbit displays (signed numerator over a nonzero distinction-orbit denominator). Equality of displays is the choice-free cross-multiplication relation crossEq, which balances scaled numerators as signed orbits. Reciprocals of ratio orbits are total, sending zero to zero as in $\mathbb{Q}$.
A PRC ratio character $\chi$ is a multiplicative map on ratio orbits. Prime-direction calibration requires $\chi$ to act as the identity (or a controlled orientation) on native prime axes. The two-prime reciprocal hypothesis says $\chi$ sends the orbit-$2$ prime direction to its reciprocal. Cost is read off characters via costFromCharacter and compared to the native $J$-cost display onRatioOrbit.
The hypothesis target asserts cost consistency on mixed composites: under reciprocal orientation of $2$ and identity orientation of a distinct prime $p$, the composite direction $2\cdot p$ remains cost-calibrated. The conclusion target is the two-specific mixed-witness exclusion: reciprocal $2$ forbids any identity-oriented native prime witness.
proof idea
Introduce a character $\chi$ with the ratio-character, prime-calibration, and two-reciprocal hypotheses, plus an alleged identity-oriented prime witness $p$. Case-split on whether $p$ equals the orbit-$2$ prime.
If $p\neq 2$, feed the mixed data into the consistency hypothesis to obtain a cost equality on the composite $2\cdot p$. Multiplicativity of $\chi$ equates $\chi(2\cdot p)$ with $\chi(2)\cdot\chi(p)$. Congruence of multiplication under the reciprocal and identity orientations rewrites the product as $\mathrm{recip}(2)\cdot p$. Transporting through onRatioOrbit and chaining crossEq yields a cost-image equality that two_prime_composite_mixed_image_jcost_mismatch contradicts.
If $p=2$, the witness identity orientation collapses to a self-reciprocal equation on the orbit-$2$ direction, ruled out by primeDirection_not_crossEq_recip.
why it matters
This is the direct bridge from mixed-composite cost consistency to the two-prime reciprocal exclusion of identity witnesses. Downstream, the pair-product cost-consistency theorem reduces to this lemma after manufacturing the mixed-composite hypothesis, and the coherent prime-orientation target is assembled from the resulting two-prime branch controls. The universal foundation conditional certificate consumes the uniqueness stack that these targets close.
In framework terms the result is a character-rigidity step inside native cost uniqueness: once $J$-cost is forced on composites built from the distinguished prime $2$ and another prime, mixed orientation data cannot survive. That rigidity feeds the route toward unique native cost (the PRC avatar of T5 $J$-uniqueness) without leaving an open mixed-witness loophole on the orbit-$2$ axis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.