Foundation Primitive Recognition Calculus Prcnative Cost Selection Prcprime Sign

The failed uniqueness claim

A uniqueness claim says that exactly one object meets a given list of requirements. In mathematics, such claims are the backbone of definitions: they tell you that the object you are studying is not an accident of how you wrote the requirements. The declaration PRCPrimeSignedStrengthenedNativeCostUniquenessTarget_refuted is a machine-checked proof that one particular uniqueness claim, about a cost function in the Recognition Science framework, is false. It does this by producing a second cost function that satisfies every condition in the claim's hypothesis class, yet differs from the intended canonical cost.

The framework's ledger, a discrete record of recognition events, assigns a cost to each possible ratio of two quantities. The intended cost is J(x) = (x + 1/x)/2 - 1, which the framework proves is forced by five plain conditions: reciprocal symmetry, zero cost at unity, a composition law, calibration, and continuity. The refuted claim attempted to strengthen the hypothesis class by adding a primeness condition and a sign condition, in hopes that these extra requirements would still force J uniquely. The proof shows they do not: a function that is zero everywhere, or one that simply subtracts 1 from its input, also satisfies the strengthened conditions, so uniqueness fails.

The refutation is not a failure of the framework's main result. The five-condition theorem that forces J remains proved. What the refuted claim shows is that the specific strengthening, which added prime-signed conditions, is insufficient on its own. The framework's library records this as a continuum price residue wall, a boundary in the space of possible hypothesis classes: the base conditions are too weak, the strengthened ones are too weak, and the prime-signed ones are too weak. Only the full zero-calibrated class, with the literal unit representative, achieves uniqueness.

The practical lesson is about how uniqueness claims are built. Adding conditions to a hypothesis class does not automatically narrow it to one object; sometimes the new conditions are satisfied by multiple functions, and the intended one is not singled out. The machine-checked proof makes this failure explicit and reproducible, rather than a matter of intuition. It also shows the framework's method: every strengthening is tested, and the ones that fail are recorded as refuted targets, not silently dropped.

/-- **Zero-orbit calibration is irreducible.** Without it, the prime-signed
strengthened ledger admits the zero-flat countermodel: uniqueness fails at the
zero orbit, where the canonical cost displays `-1` and the countermodel
displays `0`. -/
theorem PRCPrimeSignedStrengthenedNativeCostUniquenessTarget_refuted :
    ¬ PRCPrimeSignedStrengthenedNativeCostUniquenessTarget := by
  intro h
  have hzero :=
    h zeroFlatNativeCost zeroFlatNativeCost_prime_signed_strengthened_hypotheses
      RatioOrbit.zero
  rw [zeroFlatNativeCost_zero, RatioOrbit.crossEq_iff_toRat_eq,
    RatioOrbit.zero_toRat, onRatioOrbit_toRat, RatioOrbit.zero_toRat] at hzero
  norm_num at hzero

/-- The native cost-selection package holds. -/
theorem costSelectionPackageNative_holds : CostSelectionPackageNative where
  j_unique_native :=
    PRCZeroCalibratedPrimeSignedStrengthenedNativeCostUniquenessTarget_proved
  non_vacuous :=
    ⟨canonicalSelectedNativeCost, canonicalSelectedNativeCost_full_hypotheses,
      canonicalSelectedNativeCost_crossEq_onRatioOrbit⟩
  zero_cost_excluded := constantZeroNativeCost_excluded
  linear_cost_excluded := linearNativeCost_excluded

/-- Decoy exclusion 1 against the full frozen class. -/
theorem constantZeroNativeCost_excluded :
    ¬ PRCZeroCalibratedPrimeSignedStrengthenedNativeCostHypotheses
        constantZeroNativeCost :=
  fun h =>
    constantZeroNativeCost_not_native_hypotheses
      h.prime_signed.signed_strengthened.strengthened.native

/-- Decoy exclusion 2 against the full frozen class. -/
theorem linearNativeCost_excluded :
    ¬ PRCZeroCalibratedPrimeSignedStrengthenedNativeCostHypotheses
        linearNativeCost :=
  fun h =>
    linearNativeCost_not_native_hypotheses
      h.prime_signed.signed_strengthened.strengthened.native

What this page does not claim

The main five-condition theorem that forces J is not overturned by this refutation. The refuted claim does not show that no strengthening of the conditions can ever force J uniquely. The refutation does not identify which specific condition among the prime-signed ones is responsible for the failure.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCNativeCostSelection.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: