Foundation Primitive Recognition Calculus Prcnative Cost Structural Ledger Prcsi

The uniqueness theorem

A cost function assigns a number to each possible ratio between two quantities. In the Recognition Science framework, the cost of recognizing one thing as another is not a free choice; it is forced by structural conditions. The declaration PRCSignReversingNativeCostUniquenessTarget_proved is a machine-checked theorem stating that any function F satisfying the framework's sign-reversing native cost hypotheses must equal the canonical cost function on every ratio. In plain terms: if a cost function behaves in the way the hypotheses demand, there is exactly one possible function it can be, namely J(x) = (x + 1/x)/2 - 1.

The theorem is proved in the framework's machine-checked library of formal theorems, in the file PRCNativeCostStructuralLedger.lean. The proof proceeds by showing that the sign-reversing hypotheses imply a stronger set of conditions, and then applying an earlier uniqueness result. The canonical cost function J has the property that J(1) = 0, meaning recognizing something as itself costs nothing, and J(2) = 1/4, so recognizing a ratio of 2 costs one quarter. The theorem also implies that the cost is always nonnegative for positive ratios, which matches the intuition that recognition cannot have negative cost.

What the theorem does not claim is equally important. It does not claim that the sign-reversing hypotheses are the only possible ones; a separate structural version exists with different hypotheses. It does not claim that the canonical cost function is the unique solution without the sign-reversing condition; in fact, a related structural theorem without the anchor condition is explicitly refuted in the library. The theorem also does not assert anything about the golden ratio or about three-dimensional space; those are separate results in the framework that build on this one but are not part of this declaration.

The practical consequence is that within the framework, there is no freedom in choosing the cost function once the hypotheses are accepted. This uniqueness is what allows later results in the framework to derive constants like the golden ratio and the number of spatial dimensions from the cost function alone. For a reader outside the framework, the theorem is a precise statement about a specific mathematical structure, not a claim about the physical world.

/-- Round 4 terminal: the sign-reversing ledger forces the canonical cost. -/
theorem PRCSignReversingNativeCostUniquenessTarget_proved :
    PRCSignReversingNativeCostUniquenessTarget := by
  intro F hF q
  refine PRCZeroCalibratedSignedStrengthenedNativeCostUniquenessTarget_proved F ?_ q
  exact
    { signed_strengthened :=
        { strengthened := hF.strengthened
          signed_unit :=
            signReversing_forces_signed_unit
              hF.strengthened.native.unit_zero hF.sign_reversing }
      zero_calibrated := hF.zero_calibrated }

@[simp] theorem jq_one : jq 1 = 0 := by norm_num [jq]

theorem jq_two : jq 2 = 1 / 4 := by norm_num [jq]

/-- **Positivity is a theorem, not an axiom.** Recognizing a positive imbalance
never pays. -/
theorem structural_forces_positive (F : RatioOrbit → RatioOrbit)
    (hF : PRCStructuralNativeCostHypotheses F) :
    PRCNativeCostPositive F := by
  intro q hq
  have hJ := crossDisp
    (PRCStructuralNativeCostUniquenessTarget_proved F hF q)
  rw [hJ, jq_onRatioOrbit]
  exact jq_nonneg hq

/-- **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)

What this page does not claim

The theorem does not assert anything about the physical world or about the golden ratio or spatial dimensions. The theorem does not claim that the sign-reversing hypotheses are the only possible ones. The theorem does not claim uniqueness without the sign-reversing condition; in fact, a related structural theorem without the anchor condition is refuted.

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: