Foundation Recognition Ledger Floor Ledger Cost Eq Zero Iff

The zero-cost ledger

A bookkeeping system that records defects as counts of primitive distinctions. A defect ledger is a discrete record of events, each event being a copy of some basic type of flaw, and the cost of a ledger is the sum over all entries of the count multiplied by that flaw's weight. The declaration ledgerCost_eq_zero_iff states a simple fact: if every weight is strictly positive, then a ledger has cost zero if and only if it is the empty ledger. The proof is a theorem in a machine-checked library of formal theorems, meaning the statement is verified by a computer from the definitions, with no gaps and no extra axioms.

The statement is a dichotomy: any non-empty ledger, no matter how small, carries a positive cost. This is the floor property that makes the ledger a useful foundation for a theory of recognition. The theorem also connects to a broader structure: the cost function on ledgers is additive, so the cost of combining two ledgers is the sum of their costs, and two copies of the same defect genuinely cost twice as much as one copy. The zero-cost ledger is the unique state where nothing has happened, and the theorem pins that down exactly.

What the declaration does not claim is equally important. It does not say that the empty ledger is the only state with zero cost under a weight function that is merely non-negative; if some weight is zero, then a ledger containing only that flaw also has zero cost. It does not assert anything about the physical world, only about the formal ledger object. And it does not derive the cost function J(x) = (x + 1/x)/2 - 1; that is a separate theorem about a different, continuous cost function, not about this discrete ledger.

/-- With strictly positive weights, a ledger is costless exactly when it is the
empty ledger. This is the recognition-work dichotomy on the free floor. -/
theorem ledgerCost_eq_zero_iff (w : I → ℝ) (hw : ∀ i, 0 < w i)
    (Γ : DefectLedger I) :
    ledgerCost w Γ = 0 ↔ Γ = 0 := by
  constructor
  · intro h
    by_contra hΓ
    have hne : Γ.support.Nonempty := Finsupp.support_nonempty_iff.mpr hΓ
    obtain ⟨i, hi_supp⟩ := hne
    have hi : Γ i ≠ 0 := Finsupp.mem_support_iff.mp hi_supp
    have hpos : 0 < (Γ i : ℝ) * w i :=
      mul_pos (by exact_mod_cast Nat.pos_of_ne_zero hi) (hw i)
    have hnonneg : ∀ j ∈ Γ.support, 0 ≤ (Γ j : ℝ) * w j :=
      fun j _ => mul_nonneg (Nat.cast_nonneg _) (le_of_lt (hw j))
    have hle : (Γ i : ℝ) * w i ≤ ledgerCost w Γ :=
      Finset.single_le_sum hnonneg hi_supp
    linarith
  · intro h; subst h; simp

/-- **Unconditional additivity.** The free ledger needs no restriction of the
independence relation: the cost of a sum is always the sum of the costs. -/
theorem ledgerCost_add (w : I → ℝ) (Γ Δ : DefectLedger I) :
    ledgerCost w (Γ + Δ) = ledgerCost w Γ + ledgerCost w Δ := by
  unfold ledgerCost
  refine Finsupp.sum_add_index' ?_ ?_
  · intro i; simp
  · intro i a b; push_cast; ring

/-- **The cokernel fix.** Two independent copies of the same defect cost `2 w i`,
not `w i`. Multiplicity is genuinely represented, so the free ledger needs no
restriction of independence to avoid `1 = 2`: on this carrier, `1 + 1 = 2`. -/
theorem two_independent_same_defects (w : I → ℝ) (i : I) :
    ledgerCost w (Finsupp.single i 1 + Finsupp.single i 1) = 2 * w i := by
  rw [ledgerCost_add, ledgerCost_single]
  push_cast
  ring

What this page does not claim

The theorem does not apply when some weight is zero; a ledger containing only a zero-weight flaw also has zero cost. The declaration says nothing about physical reality, only about the formal ledger object. The theorem does not derive the continuous cost function J(x) = (x + 1/x)/2 - 1.

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