Encyclopedia Cosmology Cosmology Lattice Ball Volume Outer Sum 2d

ARTICLE 2 claims 2 theorems

Cosmology Lattice Ball Volume Outer Sum 2d

A machine-checked theorem gives the exact count of cells in a growing 2D diamond-shaped lattice, and it is a pure arithmetic fact, not a claim about physics.

Verify this page

The 2D diamond area law

In plain mathematics, the declaration establishes a counting formula. Consider the set of integer points (x, y) satisfying |x| + |y| ≤ t, where t is a nonnegative integer. This set forms a diamond shape on the integer grid. The theorem states that the number of such points is exactly 2t² + 2t + 1, a value known as the centered square number. For example, at t = 24, the count is 1201.

The proof is a simple geometric argument. For each fixed value of x, the allowed y values form an interval of length 2(t - |x|) + 1. Summing these interval lengths over all x from -t to t yields the closed form. The theorem named outer_sum_2d is precisely this summation result, and it is proved by induction, peeling off the two new endpoints at each step.

This result is part of a larger framework called Recognition Science, which models reality as a discrete record of events, called a ledger. In this framework, a coarsening engine accumulates its world on an L1 ball that grows by one rung per recognition cycle. The 2D diamond is the shape of this world after t cycles. The counting formula is a theorem in the framework's machine-checked library of formal theorems, proved over the natural numbers with no additional axioms.

What the declaration does not claim is any physical content. It establishes a pure arithmetic identity about lattice points. It does not assert that the physical universe is a 2D diamond, nor does it derive any physical constant. The connection to the framework's broader claims, such as the sub-extensivity of the recognition-active frontier, is a separate matter built on top of this counting result.

THEOREM outer_sum_2d · 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
THEOREM outer_sum_2d · 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

What this page does not claim

The declaration does not claim any physical content about the universe being a 2D diamond. It does not derive any physical constants or make predictions about measurements. It does not establish the sub-extensivity claim by itself; that requires additional theorems about the recognition-active frontier.

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