Gravity Recognition Ledger Total Cost Eq Sum Deficits

Total cost as a sum of deficits

A recognition ledger (a discrete record of comparison costs between pairs of cells in a finite lattice) keeps a single number for every pair of cells. The total cost of the whole ledger is the sum of all these pair costs. The deficit at one cell is the sum of the costs of comparing that cell with every other cell. The theorem totalCost_eq_sum_deficits states that the total cost of the entire ledger equals the sum of the deficits of all its cells.

This identity is a bookkeeping fact, not a physical law. It follows directly from the definitions: adding up all the per-cell deficits counts each pair cost exactly twice, once from each endpoint, and the total cost is exactly that same double count. The proof in the machine-checked library of formal theorems is a single line, a reflexivity step, because the two sides unfold to the same double sum. The statement holds for any recognition ledger on any finite lattice, with no extra assumptions about the cost values or the lattice structure.

What the theorem does not claim is just as important. It does not say that the total cost is zero, or that any particular ledger is flat. A separate theorem, totalCost_eq_zero_iff_flat, establishes that the total cost is zero if and only if the ledger is flat, meaning every pair cost is zero. The sum-of-deficits identity is compatible with that, but it does not imply it. The identity also does not say anything about the size of the total cost, only about how to compute it from the deficits.

The practical use of the identity is organizational. It lets a computation of total cost be broken into independent per-cell pieces, which can be evaluated in any order or in parallel. It also gives a clean way to define the total cost of a ledger from its local structure, which matters when the ledger is used as a bookkeeping structure for gravitational action, page curves, or vacuum energy in the framework. The identity itself, however, is neutral: it is pure arithmetic about sums, and it applies to any ledger whatsoever.

/-- Total cost is the sum of deficits. -/
theorem totalCost_eq_sum_deficits {Λ : Type*} [Fintype Λ] [DecidableEq Λ]
    (L : RecognitionLedger Λ) : totalCost L = ∑ i, deficit L i :=
  rfl

/-- Total cost is the sum of deficits. -/
theorem totalCost_eq_sum_deficits {Λ : Type*} [Fintype Λ] [DecidableEq Λ]
    (L : RecognitionLedger Λ) : totalCost L = ∑ i, deficit L i :=
  rfl

/-- The total cost vanishes iff the ledger is flat. -/
theorem totalCost_eq_zero_iff_flat {Λ : Type*} [Fintype Λ] [DecidableEq Λ]
    (L : RecognitionLedger Λ) : totalCost L = 0 ↔ isFlat L := by
  constructor
  · intro h0
    unfold isFlat
    intro i j
    unfold totalCost at h0
    have hsums : ∀ x ∈ Finset.univ, ∑ y : Λ, L.cost x y = 0 := by
      rwa [Finset.sum_eq_zero_iff_of_nonneg
        (fun x _ => Finset.sum_nonneg (fun y _ => L.nonneg x y))] at h0
    have h0i := hsums i (Finset.mem_univ i)
    have hsumj : ∀ y ∈ Finset.univ, L.cost i y = 0 := by
      rwa [Finset.sum_eq_zero_iff_of_nonneg (fun y _ => L.nonneg i y)] at h0i
    exact hsumj j (Finset.mem_univ j)
  · intro hf
    unfold totalCost
    apply Finset.sum_eq_zero
    intro i _
    apply Finset.sum_eq_zero
    intro j _
    exact hf i j

What this page does not claim

The theorem does not assert that any particular ledger has zero total cost. The theorem does not establish that the total cost is zero if and only if the ledger is flat; that is a separate theorem. The identity does not by itself connect the ledger to gravity, page curves, or vacuum energy; those are separate structural claims in the framework.

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/Gravity/RecognitionLedger.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: