PRCPrimeCalibrationForcesTwoPrimeMixedCompositeCostConsistencyTarget_not_of_two_adic_axis_twist
plain-language theorem explainer
Existence of a prime-calibrated two-adic axis-twist ratio character refutes the mixed-composite cost-consistency target. Anyone tracking character rigidity or native cost uniqueness in PRC cites this as the direct negation bridge. The proof is a one-line contrappositive application of the matching absurdity lemma.
Claim. If there exists a ratio-orbit character $\chi$ that is a PRC ratio character, prime-direction calibrated, and a two-adic axis twist, then the universal mixed-composite cost-consistency target fails: it is not the case that every such prime-calibrated character sending the $2$-direction to its reciprocal must calibrate every composite direction $2\cdot p$ for distinct native primes $p\neq 2$.
background
Primitive Recognition Calculus (PRC) studies cost uniqueness on ratio orbits before the full J-cost forcing chain. A PRC ratio character is a map $\chi$ on ratio orbits preserving the multiplicative structure used to read cost. Prime-direction calibration means $\chi$ acts as the identity (or a fixed calibrated choice) on native prime directions. A two-adic axis twist is a concrete deformation that twists the $2$-adic axis while remaining prime-calibrated; the module treats constructing such a model as the native-valuation route to refuting the current character-rigidity branch.
The mixed-composite cost-consistency target is the cost-visible blocker: if a prime-calibrated character sends the orbit of $2$ to its reciprocal, then for every distinct native prime $p$ it must still calibrate the composite direction $2\cdot p$ under that mixed orientation data. Upstream, the absurdity lemma already shows that this target is incompatible with any calibrated two-adic axis-twist character.
proof idea
Term-mode contrappositive wrapper. Assume the mixed-composite consistency target. Feed that hypothesis into PRCPrimeCalibratedTwoAdicAxisTwistCharacter_absurd_of_mixed_composite_cost_consistency, which concludes there is no calibrated two-adic axis-twist character. Apply the resulting negation to the given twist hypothesis and obtain the contradiction. No further case analysis or orbit arithmetic is performed here.
why it matters
Closes one concrete negation edge in the native-cost uniqueness ledger: the two-adic axis-twist model is officially incompatible with the mixed-composite consistency target. Downstream, the sibling theorem for the broader two-adic axis-twist ratio character reduces immediately to this result. The same fact is consumed by prc_universal_foundation_conditional_certificate in UniversalFoundation, which packages kernel, real-complete ordered field, and trace-logic certificates into the conditional universal-foundation certificate.
In the larger Recognition stack this sits under foundation work that feeds character rigidity toward unique native cost, prior to citing T5 J-uniqueness ($J(x)=(x+x^{-1})/2-1$) and the Recognition Composition Law. It does not itself force $J$ or $\varphi$; it removes one obstructing character class from the cost-consistency branch.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.