Encyclopedia Cosmology Cosmology Lattice Ball Volume Slice Card

ARTICLE 3 claims 3 theorems

Cosmology Lattice Ball Volume Slice Card

A single theorem counts the lattice points on a line through a growing diamond, the first step toward exact volume laws for a coarsening grid.

Verify this page

The slice count

A lattice is a grid of evenly spaced points, like the intersections on graph paper. The declaration slice_card counts, for a fixed column of that grid, how many points lie inside a diamond-shaped region. The diamond is the set of points whose two coordinates have absolute values summing to at most t, a radius that grows one step per cycle. For a fixed first coordinate x, the theorem states that the number of valid second coordinates is exactly 2(t - |x|) + 1.

The formula has a plain geometric reading. The diamond's width at column x shrinks as x moves away from the center: at the middle column the slice is longest, and at the two tips it collapses to a single point. The expression 2(t - |x|) + 1 is just the count of integers in that shrinking interval. The theorem proves this for every radius t and every column x within the diamond, as a formal result in the framework's machine-checked library.

This single slice count is the load-bearing step for the larger volume laws. Summing the slice widths over all columns gives the total number of points in the 2D diamond: 2t² + 2t + 1, the centered square number. The same fibering trick, applied one dimension higher, yields the 3D octahedron count (2t+1)(2t²+2t+3)/3. Those closed forms let the simulation know exactly how many cells its world holds at any radius, and how many new cells each growth step adds: the new shell in 2D has 4(t+1) points, in 3D it has 4(t+1)² + 2.

What slice_card does not claim is any physical content. It is a theorem about counting integer points in a geometric shape, nothing more. It does not say that the universe is a lattice, that recognition events occupy grid cells, or that the diamond is the actual shape of space. Those are modeling choices made elsewhere in the framework, and this counting theorem is neutral with respect to them. It also does not claim anything about the fine-structure constant, the golden ratio, or any other constant from the forcing chain; it is a standalone combinatorial result.

The practical consequence is that the simulation's bookkeeping is exact. When the coarsening engine reports that its diamond grew to 1201 cells after 24 cycles, or the octahedron to 2625 cells after 12, those numbers are not approximations or simulation artifacts. They are the unique correct counts, proved once and for all for every radius. The slice theorem is the first rung of that ladder, and the rest of the volume laws climb it directly.

THEOREM slice_card · IndisputableMonolith/Cosmology/LatticeBallVolume.lean
slice_card · IndisputableMonolith/Cosmology/LatticeBallVolume.lean:39 
/-- For `|x| ≤ t`, the `y`-slice `{ y ∈ [-t, t] : |x| + |y| ≤ t }` is exactly the interval
`[-(t - |x|), t - |x|]`, hence has `2 (t - |x|) + 1` points. -/
theorem slice_card (t : ℕ) (x : ℤ) (hx : x.natAbs ≤ t) :
    ((Finset.Icc (-(t : ℤ)) t).filter (fun y => x.natAbs + y.natAbs ≤ t)).card
      = 2 * (t - x.natAbs) + 1 := by
  have hset : (Finset.Icc (-(t : ℤ)) t).filter (fun y => x.natAbs + y.natAbs ≤ t)
      = Finset.Icc (-(((t - x.natAbs : ℕ)) : ℤ)) (((t - x.natAbs : ℕ)) : ℤ) := by
    apply Finset.ext
    intro y
    simp only [Finset.mem_filter, Finset.mem_Icc]
    omega
  rw [hset, Int.card_Icc]
  omega
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 outer_sum_2d · three_mul_outer_sum_3d · IndisputableMonolith/Cosmology/LatticeBallVolume.lean
outer_sum_2d · IndisputableMonolith/Cosmology/LatticeBallVolume.lean:69 
/-- The symmetric-interval sum `∑_{x ∈ [-t,t]} (2 (t - |x|) + 1) = 2 t² + 2 t + 1`, by induction
peeling the two new endpoints `±(t+1)` each step. -/
theorem outer_sum_2d (t : ℕ) :
    ∑ x ∈ Finset.Icc (-(t : ℤ)) t, (2 * (t - x.natAbs) + 1) = 2 * t ^ 2 + 2 * t + 1 := by
  induction t with
  | zero => simp
  | succ n ih =>
    have hsplit : Finset.Icc (-((n : ℤ) + 1)) ((n : ℤ) + 1)
        = insert (-((n : ℤ) + 1)) (insert ((n : ℤ) + 1) (Finset.Icc (-(n : ℤ)) (n : ℤ))) := by
      apply Finset.ext
      intro z
      simp only [Finset.mem_insert, Finset.mem_Icc]
      omega
    have hmem2 : ((n : ℤ) + 1) ∉ Finset.Icc (-(n : ℤ)) (n : ℤ) := by
      simp only [Finset.mem_Icc]; omega
    have hmem1 : (-((n : ℤ) + 1))
        ∉ insert ((n : ℤ) + 1) (Finset.Icc (-(n : ℤ)) (n : ℤ)) := by
      simp only [Finset.mem_insert, Finset.mem_Icc]; omega
    have hcast : (((n : ℕ) + 1 : ℕ) : ℤ) = (n : ℤ) + 1 := by push_cast; ring
    rw [show (((n : ℕ) + 1 : ℕ) : ℤ) = (n : ℤ) + 1 from hcast]
    rw [hsplit, Finset.sum_insert hmem1, Finset.sum_insert hmem2]
    -- endpoint contributions: |±(n+1)| = n+1, so each summand is 2*((n+1) - (n+1)) + 1 = 1
    have hendL : 2 * ((n + 1) - (-((n : ℤ) + 1)).natAbs) + 1 = 1 := by
      have : (-((n : ℤ) + 1)).natAbs = n + 1 := by
        rw [Int.natAbs_neg]; omega
      rw [this]; omega
    have hendR : 2 * ((n + 1) - (((n : ℤ) + 1)).natAbs) + 1 = 1 := by
      have : (((n : ℤ) + 1)).natAbs = n + 1 := by omega
      rw [this]; omega
    rw [hendL, hendR]
    -- rewrite the inner sum's summand: for x ∈ [-n,n], (n+1) - |x| = (n - |x|) + 1
    have hcongr : ∑ x ∈ Finset.Icc (-(n : ℤ)) (n : ℤ), (2 * ((n + 1) - x.natAbs) + 1)
        = ∑ x ∈ Finset.Icc (-(n : ℤ)) (n : ℤ), ((2 * (n - x.natAbs) + 1) + 2) := by
      refine Finset.sum_congr rfl (fun x hx => ?_)
      rw [Finset.mem_Icc] at hx
      have hxnat : x.natAbs ≤ n := by omega
      omega
    rw [hcongr, Finset.sum_add_distrib, ih, Finset.sum_const]
    have hcard : (Finset.Icc (-(n : ℤ)) (n : ℤ)).card = 2 * n + 1 := by
      rw [Int.card_Icc]; omega
    rw [hcard]
    ring
three_mul_outer_sum_3d · IndisputableMonolith/Cosmology/LatticeBallVolume.lean:146 
/-- The octahedron outer sum reduces to the centered-octahedral recurrence. We prove the
division-free form `3 · ∑ = 4 t³ + 6 t² + 8 t + 3` by induction, reusing the diamond area law for
each fiber and the 2-D outer sum for the `∑ (t - |x|) = t²` identity that the step needs. -/
theorem three_mul_outer_sum_3d (t : ℕ) :
    3 * (∑ x ∈ Finset.Icc (-(t : ℤ)) t,
            (InterfaceComponentBound.Diamond.ball (t - x.natAbs)).card)
      = 4 * t ^ 3 + 6 * t ^ 2 + 8 * t + 3 := by
  -- rewrite each fiber card via the diamond area law
  have hrw : ∀ s : ℕ, ∑ x ∈ Finset.Icc (-(s : ℤ)) s,
        (InterfaceComponentBound.Diamond.ball (s - x.natAbs)).card
      = ∑ x ∈ Finset.Icc (-(s : ℤ)) s,
          (2 * (s - x.natAbs) ^ 2 + 2 * (s - x.natAbs) + 1) := by
    intro s
    refine Finset.sum_congr rfl (fun x _ => ?_)
    rw [Diamond.card_ball]
  rw [hrw]
  -- now an ℕ identity about a symmetric-interval sum of a quadratic in (t - |x|)
  induction t with
  | zero => simp
  | succ n ih =>
    have hsplit : Finset.Icc (-((n : ℤ) + 1)) ((n : ℤ) + 1)
        = insert (-((n : ℤ) + 1)) (insert ((n : ℤ) + 1) (Finset.Icc (-(n : ℤ)) (n : ℤ))) := by
      apply Finset.ext
      intro z
      simp only [Finset.mem_insert, Finset.mem_Icc]
      omega
    have hmem2 : ((n : ℤ) + 1) ∉ Finset.Icc (-(n : ℤ)) (n : ℤ) := by
      simp only [Finset.mem_Icc]; omega
    have hmem1 : (-((n : ℤ) + 1))
        ∉ insert ((n : ℤ) + 1) (Finset.Icc (-(n : ℤ)) (n : ℤ)) := by
      simp only [Finset.mem_insert, Finset.mem_Icc]; omega
    have hcast : (((n : ℕ) + 1 : ℕ) : ℤ) = (n : ℤ) + 1 := by push_cast; ring
    rw [show (((n : ℕ) + 1 : ℕ) : ℤ) = (n : ℤ) + 1 from hcast]
    rw [hsplit, Finset.sum_insert hmem1, Finset.sum_insert hmem2]
    have hendL : 2 * ((n + 1) - (-((n : ℤ) + 1)).natAbs) ^ 2
          + 2 * ((n + 1) - (-((n : ℤ) + 1)).natAbs) + 1 = 1 := by
      have : (-((n : ℤ) + 1)).natAbs = n + 1 := by rw [Int.natAbs_neg]; omega
      rw [this]; simp
    have hendR : 2 * ((n + 1) - (((n : ℤ) + 1)).natAbs) ^ 2
          + 2 * ((n + 1) - (((n : ℤ) + 1)).natAbs) + 1 = 1 := by
      have : (((n : ℤ) + 1)).natAbs = n + 1 := by omega
      rw [this]; simp
    rw [hendL, hendR]
    -- inner-sum congruence: g((n+1) - |x|) = g((n - |x|)) + 4*(n+1 - |x|) for |x| ≤ n
    have hcongr : ∑ x ∈ Finset.Icc (-(n : ℤ)) (n : ℤ),
            (2 * ((n + 1) - x.natAbs) ^ 2 + 2 * ((n + 1) - x.natAbs) + 1)
        = ∑ x ∈ Finset.Icc (-(n : ℤ)) (n : ℤ),
            ((2 * (n - x.natAbs) ^ 2 + 2 * (n - x.natAbs) + 1)
              + (4 * (n - x.natAbs) + 4)) := by
      refine Finset.sum_congr rfl (fun x hx => ?_)
      rw [Finset.mem_Icc] at hx
      have hxnat : x.natAbs ≤ n := by omega
      have hsub : (n + 1) - x.natAbs = (n - x.natAbs) + 1 := by omega
      rw [hsub]; ring
    rw [hcongr, Finset.sum_add_distrib]
    have hcard : (Finset.Icc (-(n : ℤ)) (n : ℤ)).card = 2 * n + 1 := by
      rw [Int.card_Icc]; omega
    set S := ∑ x ∈ Finset.Icc (-(n : ℤ)) (n : ℤ),
        (2 * (n - x.natAbs) ^ 2 + 2 * (n - x.natAbs) + 1) with hSdef
    set T := ∑ x ∈ Finset.Icc (-(n : ℤ)) (n : ℤ), (4 * (n - x.natAbs) + 4) with hTdef
    -- closed form for the residual increment sum T via the 2-D outer sum
    have hT : T = 4 * n ^ 2 + 8 * n + 4 := by
      rw [hTdef]
      have hcongr2 : ∑ x ∈ Finset.Icc (-(n : ℤ)) (n : ℤ), (4 * (n - x.natAbs) + 4)
          = ∑ x ∈ Finset.Icc (-(n : ℤ)) (n : ℤ), (2 * (2 * (n - x.natAbs) + 1) + 2) := by
        refine Finset.sum_congr rfl (fun x _ => ?_); ring
      rw [hcongr2, Finset.sum_add_distrib, ← Finset.mul_sum, outer_sum_2d, Finset.sum_const, hcard]
      simp only [smul_eq_mul]; ring
    -- regroup so that `3 * S` (the inductive hypothesis) appears as a subterm, then close by ring
    have hcomb : 3 * (1 + (1 + (S + T))) = 3 * S + (3 * T + 6) := by ring
    rw [hcomb, ih, hT]
    ring

What this page does not claim

The universe is a lattice or that recognition events occupy grid cells. The diamond or octahedron is the actual shape of physical space. Any connection between this counting theorem and the fine-structure constant or the golden ratio.

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