Pith. sign in
theorem

PRCPrimeCalibrationForcesPrimeReciprocalWitnessGlobalizesTarget_refuted

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

plain-language theorem explainer

Prime calibration does not force reciprocal orientation to spread from one native prime witness to every native prime axis. Anyone auditing native-cost uniqueness blockers or the PRC universal-foundation certificate cites this refutation. The proof is a short reduction: the globalization target is equivalent to the already-refuted no-mixed-orientation target, so it fails as well.

Claim. It is false that every ratio-orbit character $\chi$ that is prime-direction calibrated must satisfy reciprocal-witness globalization: having one reciprocal-oriented native prime witness does not force reciprocal orientation on every native prime axis.

background

In the Primitive Recognition Calculus, a ratio character $\chi$ is a map on ratio orbits encoding how multiplicative structure is read as cost. Prime-direction calibration restricts how $\chi$ orients native prime axes. Reciprocal orientation on an axis means the character treats that prime via the reciprocal branch rather than a mixed or direct-only pattern.

The reciprocal-witness globalization target asserts a strong uniformity: if calibration permits even one reciprocal-oriented native prime witness, then every native prime axis must sit on the reciprocal branch. An equivalent formulation is the no-mixed-prime-orientation target (proved equivalent in-module): calibration cannot leave some primes reciprocal and others not.

That no-mixed target is already refuted upstream. The present declaration simply transfers the refutation across the equivalence, closing one more candidate forcing route toward a unique native cost.

proof idea

Assume the reciprocal-witness globalization target. Apply the left-to-right direction of the in-module equivalence PRCPrimeCalibrationForcesPrimeReciprocalWitnessGlobalizesTarget_iff_no_mixed_prime_orientation to obtain the no-mixed-prime-orientation target. Discharge that assumption with the already-proved refutation PRCPrimeCalibrationForcesNoMixedPrimeOrientationTarget_refuted. The argument is a pure logical transfer: no new analytic content, only the iff and the prior negation.

why it matters

Native-cost uniqueness in PRC aims to force the J-cost (the unique solution of the Recognition Composition Law, T5) from calibration and character hypotheses alone. Several intermediate "forcing targets" were proposed; this one claimed that a single reciprocal prime witness globalizes under prime calibration. Refuting it removes that route.

Downstream it is recorded in prc_native_cost_uniqueness_blocker_certificate, which packages proved and refuted factorization/calibration targets as a status board for uniqueness work. It also feeds prc_universal_foundation_conditional_certificate in UniversalFoundation, so the conditional foundation stack knows this globalization claim is closed negatively rather than left open.

Within the forcing chain, this sits below T5 J-uniqueness: it is bookkeeping about which prime-orientation constraints can or cannot pin the native cost character, not a derivation of $J$ itself.

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