Pith. sign in
theorem

PRCPrimeCalibrationForcesTwoPrimeMixedCompositeCostConsistencyTarget_not_of_ratio_character_axis_twist

proved
show as:
module
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCNativeCostUniqueness
domain
Foundation
line
11271 · github
papers citing
none yet

plain-language theorem explainer

If a ratio character realizes the two-adic axis twist, the universal mixed-composite cost-consistency target fails. Cost-uniqueness and foundation auditors cite this to rule that branch out of the prime-calibration story. The proof is a two-step term composition: upgrade the uncalibrated twist to a prime-calibrated one, then apply the already-proved negation for that stronger hypothesis.

Claim. Assume there exists a ratio-orbit character $\chi$ that exhibits two-adic axis-twist branch behavior. Then it is not the case that every prime-direction-calibrated ratio character which sends the orbit of $2$ to its reciprocal must calibrate every mixed composite direction $2\cdot p$ for distinct native primes $p$.

background

In the Primitive Recognition Calculus native-cost uniqueness development, ratio characters are maps $\chi$ on ratio orbits that encode orientation and calibration data for the cost functional. The two-adic axis twist is a concrete branch pattern: the character flips the $2$-direction while leaving other structure intact. The uncalibrated construction target packages existence of such a $\chi$ that is already a ratio character and carries that twist.

The mixed-composite consistency target is the cost-visible blocker: once a character is prime-direction calibrated and sends orbit $2$ to its reciprocal, it must still calibrate every composite direction $2\cdot p$ for distinct native primes $p$. That is the universal form of the obstruction the uniqueness argument must either force or exclude.

Upstream, the module already proves that any ratio-character axis twist upgrades automatically to a prime-calibrated two-adic axis-twist character, and that any such prime-calibrated twist falsifies the mixed-composite consistency target. This declaration simply chains those two facts from the weaker uncalibrated hypothesis.

proof idea

One-line term proof. Apply PRCPrimeCalibratedTwoAdicAxisTwistCharacter_of_ratio_character_axis_twist to the hypothesis to obtain a prime-calibrated two-adic axis-twist character, then feed that into PRCPrimeCalibrationForcesTwoPrimeMixedCompositeCostConsistencyTarget_not_of_two_adic_axis_twist, which already shows the consistency target is false under the stronger calibrated twist. No new case analysis.

why it matters

This sits in the native-cost uniqueness ladder that feeds the conditional universal-foundation certificate. Downstream, the two-three local orientation-failure character is reduced to this same negation via a construction of a ratio-character axis twist, so the present lemma is the shared sink for several pathological branches. The parent certificate prc_universal_foundation_conditional_certificate aggregates kernel, ordered-field, and trace-logic pieces; excluding axis-twist countermodels is part of keeping the cost side of that certificate coherent.

In framework terms this is foundation work beneath J-uniqueness (T5) and the Recognition Composition Law: it constrains which orientation characters can coexist with prime calibration before the native cost is forced. It does not itself produce $J(x)=\cosh(\log x)-1$; it clears a concrete obstruction class on the way there.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.