two_prime_composite_mixed_image_jcost_mismatch
plain-language theorem explainer
For any prime distinction-orbit p, the native cost images of the mixed products 2^{-1}·p and 2·p fail cross-equality as ratio orbits. Downstream uniqueness arguments cite this to block two-prime-reciprocal characters that would treat a prime direction as identity. The proof pushes the assumed equality to rationals and obtains p^{2}=1, contradicting primality.
Claim. Let $p$ be a prime distinction-natural. Write $2$ for the two-prime direction and $p$ for the prime direction of $p$. Then the native cost images of the mixed products $2^{-1}\cdot p$ and $2\cdot p$ are not cross-equal as ratio orbits: $\neg\,\mathrm{crossEq}\bigl(\mathrm{cost}(2^{-1}p),\,\mathrm{cost}(2p)\bigr)$.
background
In the Primitive Recognition Calculus, ratio orbits are the internal stand-in for positive rationals built from signed δ-orbits. Cross-equality (crossEq) is the PRC-native rational relation: two orbits match when cross-multiplication balances numerators against denominators. Upstream, crossEq_iff_toRat_eq records that this agrees with ordinary equality of the verifier displays in ℚ.
Prime distinction-naturals carry a primeOrbit witness (nonzero and non-unit). The two-prime direction and the prime direction of p are the corresponding ratio-orbit generators; their product and the product with the reciprocal of two give the mixed composites 2p and p/2. The map onRatioOrbit is the native cost display used throughout this uniqueness module (the J-cost image on ratio orbits).
The local setting is native-cost uniqueness for PRC ratio characters: one must show that only the canonical J-cost survives prime-pair product calibration, and that two-adic axis twists and two-prime-reciprocal identities produce cost defects on mixed composites.
proof idea
Assume cross-equality of the two cost images. First rule out p.toNat = 0 from the prime-orbit witness (via injectivity of toNat and toNat_zero). Rewrite the goal with crossEq_iff_toRat_eq and the toRat lemmas for onRatioOrbit, mul, recip, twoPrimeDirection, and primeDirection. After field_simp (using p ≠ 0 in ℚ) and ring_nf, the equality collapses to (p.toNat : ℚ)² = 1, hence p.toNat² = 1 in ℕ. A short case split shows p.toNat ≤ 1 and therefore p.toNat = 1. But then p is a unit, contradicting the non-unit half of primeOrbit.
why it matters
This is a concrete cost-defect lemma inside PRC native-cost uniqueness. It feeds seven parents in the same module: the two-prime-reciprocal exclusion from prime-pair product consistency; the composite cost-defect lift; the direct prime-calibration force that excludes prime-identity witnesses; the refutation of PRCNativeCostUniquenessTarget; the no-admissible-factor result for two-adic axis-twist generated cost; and the two statements that two-adic axis-twist / two-adic-generated native cost fail prime-pair product calibration.
Framework-wise it supports the J-uniqueness strand (T5): alternative characters that flip the two-prime axis or identify a prime direction with identity cannot match the canonical cost on mixed two-prime composites. Closing these defects is what lets the module refute non-canonical native costs rather than merely postulate uniqueness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.