Encyclopedia Cosmology Cosmology Lattice Ball Volume Diamond Card Eq Sum

ARTICLE 5 claims 4 theorems 1 model

Cosmology Lattice Ball Volume Diamond Card Eq Sum

A machine-checked theorem counts the cells inside a growing diamond-shaped region, revealing a simple quadratic law behind a simulation's raw numbers.

Verify this page

The diamond count

A diamond-shaped lattice ball is the set of integer grid points (x, y) satisfying |x| + |y| ≤ t, where t is a nonnegative integer radius. This region grows like a square rotated 45 degrees, and its total number of points is the centered square number 2t² + 2t + 1. At radius 24, that count is exactly 1201. The declaration diamond_card_eq_sum establishes this count by expressing it as a sum over vertical slices: for each fixed x from -t to t, the allowed y values form an interval of width 2(t - |x|) + 1, and summing these widths over all x gives the closed form.

The result is a theorem in the framework's machine-checked library of formal theorems, proved over the natural numbers with no gaps and no added axioms. It is the two-dimensional case of a broader pair of laws: the three-dimensional octahedron |x| + |y| + |z| ≤ t has the centered octahedral count (2t+1)(2t²+2t+3)/3, which at radius 12 equals 2625. Both laws matter because the coarsening engine, a simulation that accumulates a world one radius per cycle, reports exactly these totals. The diamond theorem is the foundation: the octahedron proof slices it into diamonds of smaller radius, so the 3D law reduces fiber by fiber to the 2D one.

The deeper payoff is the boundary shell. Each cycle adds the cells on the shell between radius t and t+1, and the theorems show this growth is 4(t+1) cells in 2D and 4(t+1)² + 2 in 3D. The active frontier is thus one dimension smaller than the accumulated world: a perimeter in 2D, a surface in 3D. As t grows, the fraction of newly added cells relative to the total shrinks to zero, meaning the cost of recognition localizes to the boundary rather than the bulk. This geometric fact underpins the framework's claim that the simulation's cost is sub-extensive, growing slower than the volume it fills.

What the theorem does not claim is equally important. It is a pure counting statement about lattice points; it says nothing about physics, forces, or why the diamond shape was chosen. The shell it counts is the geometric boundary of newly added cells, distinct from any charge-dependent interface in the broader framework. And while the closed forms match the simulation's reported totals, the theorem does not assert that the simulation itself is correct or that its dynamics follow from these counts. Those are separate claims with separate evidence.

MODEL diamond_card_eq_sum · IndisputableMonolith/Cosmology/LatticeBallVolume.lean
diamond_card_eq_sum · IndisputableMonolith/Cosmology/LatticeBallVolume.lean:55 
/-- Fibered form of the diamond cardinality: sum the slice widths over the first coordinate. -/
theorem diamond_card_eq_sum (t : ℕ) :
    (InterfaceComponentBound.Diamond.ball t).card
      = ∑ x ∈ Finset.Icc (-(t : ℤ)) t, (2 * (t - x.natAbs) + 1) := by
  have hb : InterfaceComponentBound.Diamond.ball t
      = (Finset.Icc (-(t : ℤ)) t ×ˢ Finset.Icc (-(t : ℤ)) t).filter
          (fun p => p.1.natAbs + p.2.natAbs ≤ t) := rfl
  rw [hb, Finset.card_filter, Finset.sum_product]
  refine Finset.sum_congr rfl (fun x hx => ?_)
  rw [Finset.mem_Icc] at hx
  have hxnat : x.natAbs ≤ t := by omega
  dsimp only
  rw [← slice_card t x hxnat, Finset.card_filter]
THEOREM diamond_card_eq_sum · IndisputableMonolith/Cosmology/LatticeBallVolume.lean
diamond_card_eq_sum · IndisputableMonolith/Cosmology/LatticeBallVolume.lean:55 
/-- Fibered form of the diamond cardinality: sum the slice widths over the first coordinate. -/
theorem diamond_card_eq_sum (t : ℕ) :
    (InterfaceComponentBound.Diamond.ball t).card
      = ∑ x ∈ Finset.Icc (-(t : ℤ)) t, (2 * (t - x.natAbs) + 1) := by
  have hb : InterfaceComponentBound.Diamond.ball t
      = (Finset.Icc (-(t : ℤ)) t ×ˢ Finset.Icc (-(t : ℤ)) t).filter
          (fun p => p.1.natAbs + p.2.natAbs ≤ t) := rfl
  rw [hb, Finset.card_filter, Finset.sum_product]
  refine Finset.sum_congr rfl (fun x hx => ?_)
  rw [Finset.mem_Icc] at hx
  have hxnat : x.natAbs ≤ t := by omega
  dsimp only
  rw [← slice_card t x hxnat, Finset.card_filter]
THEOREM diamond_card_eq_sum · IndisputableMonolith/Cosmology/LatticeBallVolume.lean
diamond_card_eq_sum · IndisputableMonolith/Cosmology/LatticeBallVolume.lean:55 
/-- Fibered form of the diamond cardinality: sum the slice widths over the first coordinate. -/
theorem diamond_card_eq_sum (t : ℕ) :
    (InterfaceComponentBound.Diamond.ball t).card
      = ∑ x ∈ Finset.Icc (-(t : ℤ)) t, (2 * (t - x.natAbs) + 1) := by
  have hb : InterfaceComponentBound.Diamond.ball t
      = (Finset.Icc (-(t : ℤ)) t ×ˢ Finset.Icc (-(t : ℤ)) t).filter
          (fun p => p.1.natAbs + p.2.natAbs ≤ t) := rfl
  rw [hb, Finset.card_filter, Finset.sum_product]
  refine Finset.sum_congr rfl (fun x hx => ?_)
  rw [Finset.mem_Icc] at hx
  have hxnat : x.natAbs ≤ t := by omega
  dsimp only
  rw [← slice_card t x hxnat, Finset.card_filter]
THEOREM octa_card_eq_sum · IndisputableMonolith/Cosmology/LatticeBallVolume.lean
octa_card_eq_sum · IndisputableMonolith/Cosmology/LatticeBallVolume.lean:121 
/-- Fibered form of the octahedron cardinality: each `x`-fiber is a diamond of radius `t - |x|`. -/
theorem octa_card_eq_sum (t : ℕ) :
    (InterfaceComponentBound.Octahedron.ball t).card
      = ∑ x ∈ Finset.Icc (-(t : ℤ)) t,
          (InterfaceComponentBound.Diamond.ball (t - x.natAbs)).card := by
  have hb : InterfaceComponentBound.Octahedron.ball t
      = (Finset.Icc (-(t : ℤ)) t ×ˢ (Finset.Icc (-(t : ℤ)) t ×ˢ Finset.Icc (-(t : ℤ)) t)).filter
          (fun p => p.1.natAbs + p.2.1.natAbs + p.2.2.natAbs ≤ t) := rfl
  rw [hb, Finset.card_filter, Finset.sum_product]
  refine Finset.sum_congr rfl (fun x hx => ?_)
  rw [Finset.mem_Icc] at hx
  have hxnat : x.natAbs ≤ t := by omega
  dsimp only
  -- the (y,z)-fiber over x equals the diamond of radius (t - |x|)
  have hfib : (Finset.Icc (-(t : ℤ)) t ×ˢ Finset.Icc (-(t : ℤ)) t).filter
        (fun q : ℤ × ℤ => x.natAbs + q.1.natAbs + q.2.natAbs ≤ t)
      = InterfaceComponentBound.Diamond.ball (t - x.natAbs) := by
    apply Finset.ext
    rintro ⟨y, z⟩
    rw [InterfaceComponentBound.Diamond.mem_ball_iff]
    simp only [Finset.mem_filter, Finset.mem_Icc, Finset.mem_product]
    omega
  -- the inner (y,z)-sum is exactly the diamond-fiber card
  rw [← hfib, Finset.card_filter]
THEOREM diamond_card_eq_sum · IndisputableMonolith/Cosmology/LatticeBallVolume.lean
diamond_card_eq_sum · IndisputableMonolith/Cosmology/LatticeBallVolume.lean:55 
/-- Fibered form of the diamond cardinality: sum the slice widths over the first coordinate. -/
theorem diamond_card_eq_sum (t : ℕ) :
    (InterfaceComponentBound.Diamond.ball t).card
      = ∑ x ∈ Finset.Icc (-(t : ℤ)) t, (2 * (t - x.natAbs) + 1) := by
  have hb : InterfaceComponentBound.Diamond.ball t
      = (Finset.Icc (-(t : ℤ)) t ×ˢ Finset.Icc (-(t : ℤ)) t).filter
          (fun p => p.1.natAbs + p.2.natAbs ≤ t) := rfl
  rw [hb, Finset.card_filter, Finset.sum_product]
  refine Finset.sum_congr rfl (fun x hx => ?_)
  rw [Finset.mem_Icc] at hx
  have hxnat : x.natAbs ≤ t := by omega
  dsimp only
  rw [← slice_card t x hxnat, Finset.card_filter]

What this page does not claim

The theorem does not assert any physical law or force; it only counts lattice points. It does not claim the diamond shape is the only possible region for the coarsening engine. It does not prove the simulation's dynamics are correct, only that the reported cell totals match these closed forms.

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