Cosmology Graded Rung Cost Total Cost Eq Interface Cost

The cost ledger

In a discrete ledger, a recognition event is a forced distinction: the system must pay a cost whenever it marks one state as different from another. The question is how much it pays. A theorem in the framework's machine-checked library of formal theorems answers this for a wide class of cases: the total cost of a configuration equals exactly the cost of its interfaces, the boundaries where the state changes. The bulk, where the state is uniform, costs zero.

The theorem is called totalCost_eq_interfaceCost. It states that for any finite set of edges and any integer-valued state field on the vertices, if the field changes by at most one unit across every edge (the unit-step condition), then the total cost equals the interface cost. The proof splits the total into two sums: one over edges where the state is equal, one where it differs. The equal-state sum is zero because the cost function J satisfies J(1) = 0. The differing-state sum is exactly the interface cost by definition. The theorem holds for any such field, not just a binary one.

This matters because the live engine does not carry a simple binary field. It carries a graded profile, where each region sits at a coarseness level (a phi-rung), and the refinement process descends one rung at a time. The unit-step condition is exactly what that process maintains. So the theorem applies to the real engine, not just to an idealized special case. It proves that the engine pays J(phi) per forced unit-rung distinction, and carries the entire same-rung bulk for free, for any rung profile.

The theorem does not claim that the unit-step condition is always satisfied. It is a hypothesis of the theorem, proved for the birth field and maintained by the engine's refinement, but not a fitted parameter. The theorem also does not claim anything about the value of J(phi) itself, only that it is positive. The closed form, total cost equals the number of interface edges times J(phi), follows as a corollary, but the core identity is the equality of total and interface cost.

/-- **The total cost equals the interface cost**, because the carried bulk contributes nothing. -/
theorem totalCost_eq_interfaceCost (k : V → ℤ) (E : Finset (V × V)) :
    totalCost k E = interfaceCost k E := by
  have hsplit := Finset.sum_filter_add_sum_filter_not E (fun p => k p.1 ≠ k p.2) (edgeCost k)
  have hzero : ∑ p ∈ E.filter (fun p => ¬ (k p.1 ≠ k p.2)), edgeCost k p = 0 := by
    apply Finset.sum_eq_zero
    intro p hp
    rw [Finset.mem_filter] at hp
    exact edgeCost_carried k (not_not.mp hp.2)
  rw [hzero, add_zero] at hsplit
  simp only [totalCost, interfaceCost]
  exact hsplit.symm

/-- A carried (equal-rung) adjacency costs exactly zero: `J(phi^0) = J(1) = 0`. -/
theorem edgeCost_carried (k : V → ℤ) {p : V × V} (h : k p.1 = k p.2) :
    edgeCost k p = 0 := by
  have hz : k p.1 - k p.2 = 0 := sub_eq_zero.mpr h
  rw [edgeCost, hz, Jpow_zero]

/-- **The forced minimal-distinction property.** A rung field `k` posts only single-rung distinctions
across the edge set `E`: every adjacency changes the rung by at most one, `k p.1 - k p.2 in {0,+1,-1}`.
A unit recognition step resolves at most one phi-rung; the live engine maintains this because T-3
descends one rung at a time. -/
def UnitStep (k : V → ℤ) (E : Finset (V × V)) : Prop :=
  ∀ p ∈ E, k p.1 - k p.2 = 0 ∨ k p.1 - k p.2 = 1 ∨ k p.1 - k p.2 = -1

What this page does not claim

The theorem does not claim that the unit-step condition is always satisfied; it is a hypothesis. The theorem does not claim any specific value for J(phi), only that it is positive. The theorem does not claim anything about the physical process that maintains the unit-step condition.

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/Cosmology/GradedRungCost.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: