Encyclopedia Foundation Foundation Primitive Recognition Calculus Prcnative Cost Structural Ledger

ARTICLE 4 claims 4 theorems

Foundation Primitive Recognition Calculus Prcnative Cost Structural Ledger

A structural ledger is a bookkeeping rule that assigns a cost to every ratio, and Recognition Science's library proves that only one such rule can exist.

Verify this page

The structural ledger

A structural ledger is a bookkeeping rule that assigns a cost to every positive ratio. In the framework of Recognition Science, a ledger (a discrete record of events, each with a cost) is the basic object. The structural ledger is the specific version that respects the multiplicative structure of ratios: it treats a ratio and its reciprocal as mirror images, charges nothing for the ratio 1, and obeys a fixed composition law. The central question is whether these conditions pin down a unique cost function.

The answer is yes. The machine-checked library of formal theorems proves the structural uniqueness target: any function satisfying the structural hypotheses must equal the canonical cost function on every ratio. That canonical function is J(x) = (x + 1/x)/2 - 1. The proof is a theorem in the library, with no unproved assumptions beyond the standard logical axioms. This is the structural version of the cost uniqueness result that appears elsewhere in the framework, but here the hypotheses are weaker, so the conclusion is stronger in a precise sense.

The structural ledger also forces positivity: for any positive ratio, the cost is nonnegative. This follows directly from the uniqueness theorem and the explicit form of J. The library proves this as the theorem structural_forces_positive. It also proves that the reciprocal map is an involution, that cost is symmetric under reciprocation, that the unit ratio is the unique zero-cost point, and that no golden-ratio scale exists in the rationals. These facts together form the NativeReciprocalGeneratorSplit structure.

One boundary is important. If the anchor condition (the composition law) is removed, uniqueness fails. The library constructs a counterexample, cubeGeneratedNativeCost, which satisfies the remaining hypotheses but is not the canonical cost. This refutation is itself a theorem. It shows that the composition law is not optional: without it, many cost functions survive.

What this establishes, in plain language, is that the structural ledger is not a convention. Within the framework, the cost of recognition is forced. The library's theorems show that any ledger respecting the structural conditions must be the canonical one, and that removing the composition law opens the door to alternatives. The structural ledger is therefore the unique bookkeeping rule for ratios under the framework's assumptions.

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)
THEOREM structural_forces_positive · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCNativeCostStructuralLedger.lean
structural_forces_positive · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCNativeCostStructuralLedger.lean:768 
/-- **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
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 nativeReciprocalGeneratorSplit_holds · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCNativeCostStructuralLedger.lean
nativeReciprocalGeneratorSplit_holds · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCNativeCostStructuralLedger.lean:1534 
theorem nativeReciprocalGeneratorSplit_holds : NativeReciprocalGeneratorSplit where
  involutive := native_recip_involutive
  cost_symmetric := native_cost_recip_symmetric
  unit_is_cost_zero := fun _ hq => native_recip_fixed_iff_cost_zero hq
  scale_is_a_purchase := no_native_golden_scale

What this page does not claim

This answer does not claim that the structural ledger is the only possible bookkeeping rule outside the framework's assumptions. This answer does not claim that the golden ratio is absent from all cost functions, only from the rational structural ledger. This answer does not claim that the structural uniqueness theorem has been extended to real-valued cost functions.

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