Gravity Recognition Ledger Flat Ledger Total Cost Zero

The zero-cost flat ledger

A ledger is a discrete record of events. In Recognition Science, the recognition ledger assigns a non-negative cost to every pair of cells in a finite substrate lattice, recording the accumulated cost of comparing them. The total cost is simply the sum of all these pairwise costs across the whole lattice.

The declaration flatLedger_totalCost_zero establishes a precise fact: the flat ledger, the one where every pairwise cost is zero, has total cost exactly zero. This is proved in the machine-checked library of formal theorems. The proof is immediate from the definitions, but the statement matters because it is the base case for the whole framework: a ledger with no comparisons to pay for has no total cost.

The same library also proves the converse direction in a separate theorem: if a ledger's total cost is zero, then the ledger is flat. Since all costs are non-negative, a zero total forces every individual cost to be zero. Together these two theorems give a complete characterization: total cost zero if and only if flat.

In Recognition Science, this flat ledger is the starting point for gravity. The framework models gravitational action as the continuum limit of total ledger cost restricted to hinges, and the flat ledger is the zero-cost ground state of that action. The theorem guarantees that this ground state exists and has the expected cost.

What the theorem does not claim is that the flat ledger is the only ledger with zero total cost, nor that it is physically realized. Other ledgers may also have zero total cost if their costs cancel in the sum, though the non-negativity condition rules that out. The theorem also does not claim that the flat ledger is stable or that perturbations away from it have positive cost; those are separate questions.

/-- The flat ledger has zero total cost. -/
theorem flatLedger_totalCost_zero (Λ : Type*) [Fintype Λ] [DecidableEq Λ] :
    totalCost (flatLedger Λ) = 0 :=
  (totalCost_eq_zero_iff_flat _).mpr (flatLedger_isFlat Λ)

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

/-- The total cost is non-negative. -/
theorem totalCost_nonneg {Λ : Type*} [Fintype Λ] [DecidableEq Λ]
    (L : RecognitionLedger Λ) : 0 ≤ totalCost L := by
  unfold totalCost
  apply Finset.sum_nonneg
  intro i _
  apply Finset.sum_nonneg
  intro j _
  exact L.nonneg i j

What this page does not claim

The flat ledger is the unique ledger with zero total cost. The flat ledger is physically realized in any known system. The theorem says anything about the stability of the flat ledger.

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: