Pith. sign in
theorem

PRCPrimeCalibrationForcesTwoPrimeMixedCompositeCostConsistencyTarget_refuted

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

plain-language theorem explainer

The mixed-orientation cost-consistency target for prime calibration on composite directions 2p is false: no ratio character that is prime-calibrated and sends orbit 2 to its reciprocal is forced to calibrate every composite 2p. Native-cost uniqueness and universal-foundation arguments cite this blocker closure. The proof transports an already-refuted prime-pair product consistency target across a proved equivalence of the two target forms.

Claim. It is not the case that every ratio character $\chi$ which is prime-direction calibrated and satisfies $\chi(2)\sim 2^{-1}$ must, for every native prime $p\neq 2$, force cross-equality calibration of the composite direction $2p$. Equivalently, the universal mixed-orientation cost-consistency target on composites $2p$ fails.

background

In the Primitive Recognition Calculus, ratio characters $\chi$ act on ratio orbits and encode orientation data (identity versus reciprocal) along prime and composite directions. Prime-direction calibration requires $\chi$ to fix native prime directions in a cost-visible way. Cross-equality of orbits is the relation that makes two directions cost-indistinguishable under the native cost.

The mixed composite target packages a strong consistency demand: if $\chi$ is a ratio character, is prime-calibrated, and sends the direction of $2$ to its reciprocal, then for every distinct native prime $p$ the composite direction $2p$ must still be cross-equal to the image prescribed by calibration. The module doc frames this as a cost-visible blocker for native-cost uniqueness under mixed orientation data.

Upstream, the same module already proves that this mixed target is equivalent to a prime-pair product cost-consistency target, and that the pair-product target is refuted (via a further reduction to prime-identity branch uniformity).

proof idea

Term-mode transport of a prior refutation. Assume the mixed composite consistency target. Apply the forward direction of the proved equivalence PRCPrimeCalibrationForcesPrimePairProductCostConsistencyTarget_iff_mixed_composite_cost_consistency to obtain the prime-pair product consistency target. Discharge that assumption by the already-proved refutation PRCPrimeCalibrationForcesPrimePairProductCostConsistencyTarget_refuted. No new analytic content: pure logical transfer across the iff chain.

why it matters

Closes one universal form of the cost-visible blocker in PRC native-cost uniqueness: mixed orientation (2 reciprocal, distinct prime identity) cannot force composite $2p$ calibration. Downstream, the sibling refutation PRCPrimeCalibrationForcesTwoPrimeReciprocalExcludesPrimeIdentityWitnessTarget_refuted routes through this result, and the conditional certificate prc_universal_foundation_conditional_certificate in UniversalFoundation consumes the closed blocker chain.

In the Recognition forcing picture this sits under native J-cost uniqueness (T5 landmark: $J(x)=(x+x^{-1})/2-1$), ruling out alternative character-level cost assignments that would break the RCL-compatible native cost. It does not itself force $\phi$ or $D=3$; it clears a consistency obstruction so those later steps remain unblocked.

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