Encyclopedia Foundation Foundation Primitive Recognition Calculus Prcnative Cost Structural Ledger Prcst

ARTICLE 3 claims 3 theorems

Foundation Primitive Recognition Calculus Prcnative Cost Structural Ledger Prcst

A machine-checked proof shows that one proposed uniqueness claim for the recognition cost function is false, and exactly why it fails.

Verify this page

The refuted uniqueness target

The declaration PRCStructuralSansAnchorUniquenessTarget_refuted establishes a negative result: a particular proposed uniqueness claim about the cost function in Recognition Science is false. The cost function, written J(x) = (x + 1/x)/2 - 1, is the framework's measure of the forced expense of a recognition event. The refuted claim stated that any function satisfying a certain set of structural hypotheses, but without an anchoring condition, must equal J on all rational inputs. The proof shows this is not the case.

The counterexample is concrete. The framework's machine-checked library of formal theorems constructs a function called cubeGeneratedNativeCost, which maps each rational input to a value derived from cubing it. This function satisfies all the structural hypotheses in the sans-anchor version, yet it does not agree with J on the input 2: the cube-generated cost sends 2 to 8, while J(2) equals 1/4. Since the claim required agreement on every rational input, one mismatch suffices to refute it.

The proof is a theorem in the framework's library, meaning it is checked by a machine and carries no unproven assumptions beyond the standard logical axioms. The refutation does not touch the main uniqueness result: when the anchoring condition is included, the uniqueness claim is proved, and the framework's core theorem that J is forced by five plain conditions stands. The sans-anchor variant simply lacks enough structure to pin down the cost function uniquely.

What the refutation does not claim is broader. It does not say that no uniqueness result can hold for the cost function, nor that the structural hypotheses are inconsistent. It does not claim that the cube-generated cost is a physically meaningful alternative to J; it is only a mathematical counterexample showing that the sans-anchor hypotheses are too weak. The result is a boundary marker: it shows exactly where the uniqueness proof needs its anchoring condition, and it leaves the proved uniqueness theorem untouched.

THEOREM PRCStructuralSansAnchorUniquenessTarget_refuted · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCNativeCostStructuralLedger.lean
PRCStructuralSansAnchorUniquenessTarget_refuted · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCNativeCostStructuralLedger.lean:1080 
/-- **The anchor is a genuine unit gauge.** The anchor-free structural ledger
does NOT force the canonical cost. Everything else in the ledger is structure;
the last field is a choice of unit. -/
theorem PRCStructuralSansAnchorUniquenessTarget_refuted :
    ¬ PRCStructuralSansAnchorUniquenessTarget := by
  intro huniq
  exact cubeGeneratedNativeCost_two_not_canonical
    (huniq cubeGeneratedNativeCost cubeGeneratedNativeCost_sansAnchor two)
THEOREM cubeGeneratedNativeCost · PRCStructuralSansAnchorUniquenessTarget_refuted · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCNativeCostStructuralLedger.lean
cubeGeneratedNativeCost · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCNativeCostStructuralLedger.lean:925 
/-- The first nontrivial member: the cube cost `J(q³)`. It charges `J(8) = 49/16`
for the orbit `2` where the canonical cost charges `J(2) = 1/4`. -/
def cubeGeneratedNativeCost : RatioOrbit → RatioOrbit :=
  oddPowerGeneratedNativeCost 1
PRCStructuralSansAnchorUniquenessTarget_refuted · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCNativeCostStructuralLedger.lean:1080 
/-- **The anchor is a genuine unit gauge.** The anchor-free structural ledger
does NOT force the canonical cost. Everything else in the ledger is structure;
the last field is a choice of unit. -/
theorem PRCStructuralSansAnchorUniquenessTarget_refuted :
    ¬ PRCStructuralSansAnchorUniquenessTarget := by
  intro huniq
  exact cubeGeneratedNativeCost_two_not_canonical
    (huniq cubeGeneratedNativeCost cubeGeneratedNativeCost_sansAnchor two)
THEOREM PRCStructuralNativeCostUniquenessTarget_proved · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCNativeCostStructuralLedger.lean
PRCStructuralNativeCostUniquenessTarget_proved · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCNativeCostStructuralLedger.lean:687 
/-- **Round 5 terminal.** The structural ledger forces the canonical cost. -/
theorem PRCStructuralNativeCostUniquenessTarget_proved :
    PRCStructuralNativeCostUniquenessTarget := by
  intro F hF q
  obtain ⟨χ, hχ, hFχ⟩ :=
    PRCZeroCalibratedNativeCostCharacterFactorizationTarget_proved F hF.native
      hF.zero_calibrated
  have hcal := structural_character_calibrated_on_positive_integers hF hχ hFχ
  have hresp : PRCCharacterRespectsCrossEq χ :=
    PRCCharacterRespectsCrossEq_of_normalizeRatio_canonical hχ
      PRCNormalizeRatioCanonicalTarget_proved
  have hchi : ∀ a b : RatioOrbit, a.toRat = b.toRat →
      (χ a).toRat = (χ b).toRat := by
    intro a b hab
    exact crossDisp
      (hresp a b (dispCross hab))
  -- every positive integer orbit is calibrated
  have hposcal : ∀ (a : RatioOrbit), IsPosIntOrbit a →
      RatioOrbit.crossEq (costFromCharacter χ a) (onRatioOrbit a) := by
    rintro a ⟨n, hn, han⟩
    have hdisp : a.toRat = (natOrbit n).toRat := by rw [natOrbit_toRat, han]
    rw [RatioOrbit.crossEq_iff_toRat_eq, costFromCharacter_jq, jq_onRatioOrbit,
      han]
    have hn' := hcal n hn
    rw [← hchi a (natOrbit n) hdisp] at hn'
    exact hn'
  have hprime : PRCCharacterPrimeDirectionCalibrated χ := fun p hp =>
    hposcal _ (primeDirection_isPosInt hp)
  have hpair : PRCCharacterPrimePairProductCostConsistent χ := by
    intro p hp r hr
    refine hposcal _ ⟨p.toNat * r.toNat, ?_, ?_⟩
    · obtain ⟨a, ha, _⟩ := primeDirection_isPosInt hp
      obtain ⟨b, hb, _⟩ := primeDirection_isPosInt hr
      have hpn : 1 ≤ p.toNat := by
        have h := primeDirection_toRat_ne_zero p hp
        rw [primeDirection_toRat] at h
        exact Nat.one_le_iff_ne_zero.mpr (by exact_mod_cast h)
      have hrn : 1 ≤ r.toNat := by
        have h := primeDirection_toRat_ne_zero r hr
        rw [primeDirection_toRat] at h
        exact Nat.one_le_iff_ne_zero.mpr (by exact_mod_cast h)
      exact Nat.one_le_iff_ne_zero.mpr (Nat.mul_ne_zero (by omega) (by omega))
    · rw [RatioOrbit.mul_toRat, primeDirection_toRat, primeDirection_toRat]
      push_cast
      ring
  have hsignCost :
      RatioOrbit.crossEq (costFromCharacter χ negativeOneRatio)
        (onRatioOrbit negativeOneRatio) :=
    RatioOrbit.crossEq_trans (RatioOrbit.crossEq_symm (hFχ negativeOneRatio))
      (signReversing_forces_signed_unit hF.native.unit_zero hF.sign_reversing)
  have hsign : PRCCharacterSignedUnitCalibrated χ :=
    costFromCharacter_negativeOne_forces_signed_unit hχ hsignCost
  exact RatioOrbit.crossEq_trans (hFχ q)
    (PRCNativeCostSignedAdmissibleCharacterRigidityTarget_proved χ
      ⟨⟨hχ, hprime, hpair⟩, hsign⟩ q)

What this page does not claim

The refutation does not claim that the structural hypotheses are inconsistent or contradictory. It does not claim that the cube-generated cost is a physically meaningful alternative to J. It does not claim that no uniqueness result can hold for the cost function under any hypothesis set.

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/PRCNativeCostStructuralLedger.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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND