Pith. sign in
theorem

PRCPrimeCalibratedTwoAdicAxisTwistCharacter_absurd_of_mixed_composite_cost_consistency

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

plain-language theorem explainer

If prime calibration forces cost-consistency on every mixed composite direction 2·p (orbit 2 reciprocal, distinct prime p identity), then no prime-calibrated two-adic axis-twist character can exist. Cost-uniqueness and character-rigidity arguments cite this to kill the native-valuation counter-model. The proof is a short term composition: the twist yields a forbidden mixed character, which the consistency target excludes by an iff.

Claim. Assume that every ratio-orbit character that is prime-direction calibrated and sends the two-orbit to its reciprocal must still satisfy the cross-equation on each composite direction $2\cdot p$ for native primes $p\neq 2$. Then there is no ratio-orbit character that is simultaneously a ratio character, prime-direction calibrated, and a two-adic axis twist.

background

In the Primitive Recognition Calculus, cost uniqueness is attacked through ratio-orbit characters $\chi$. A ratio character is a map on ratio orbits compatible with the multiplicative structure used to read the native cost (the J-cost side of the Recognition Composition Law). Prime-direction calibration means $\chi$ is fixed on every native prime orbit in the cost-visible way.

The two-adic axis-twist model is the concrete counter-candidate: a calibrated character that twists the two-orbit (sends it reciprocal) while holding non-two primes identity. The mixed composite consistency target is the universal blocker: even under that mixed orientation (orbit 2 reciprocal, distinct prime $p$ identity), prime calibration must still force the cross-equation on the composite direction $2\cdot p$.

Upstream, the twist is known to produce a prime-calibrated two-prime reciprocal/identity non-two mixed character, and the consistency target is equivalent to the non-existence of that mixed character.

proof idea

Term-mode reductio. Introduce a hypothetical prime-calibrated two-adic axis-twist character. Apply PRCPrimeCalibratedTwoPrimeReciprocalIdentityNonTwoPrimeMixedCharacter_of_two_adic_axis_twist to obtain a non-two mixed character witness. Apply the forward direction of PRCPrimeCalibrationForcesTwoPrimeMixedCompositeCostConsistencyTarget_iff_no_non_two_mixed_character to the consistency hypothesis, which asserts that no such mixed character exists. The two facts contradict, so the twist is absurd.

why it matters

This is a local kill-switch for the native-valuation counter-model to character rigidity inside PRC native-cost uniqueness. Downstream it feeds three sibling absurdities: absurdity from prime-identity-forces-two, from prime-pair product cost consistency, and the contraposed form that a twist blocks the mixed composite target. It also lifts to PRCTwoAdicAxisTwistRatioCharacter_absurd_of_mixed_composite_cost_consistency, closing the uncalibrated twist branch the same way.

In the broader Recognition stack this supports the conditional universal-foundation certificate (prc_universal_foundation_conditional_certificate), which packages kernel, real-complete ordered field, and trace-logic passes. The mathematical payload sits under T5 J-uniqueness: ruling out twisted characters is part of forcing the native cost to be the unique J satisfying the Recognition Composition Law, before phi, the eight-tick octave, and D=3 are read off the forcing chain.

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