Encyclopedia Cosmology Cosmology Lattice Ball Edges Total Edge Card
ARTICLE 4 claims 4 theorems
Cosmology Lattice Ball Edges Total Edge Card
A machine-checked theorem counts every adjacency inside a growing lattice ball, and splits it into edges the engine carries for free and edges it must pay to distinguish.
Counting the edges
A growing diamond on a square grid: at radius t it contains all points whose coordinates sum to at most t. The theorem total_edge_card counts the ordered adjacencies inside that diamond, where two cells count as adjacent if they differ by one step in one of the four grid directions. The count is exactly 8t². In three dimensions, the analogous octahedron, with six neighbor directions, has exactly 8t³ + 4t ordered adjacencies. These are closed-form formulas, proved over the natural numbers with no gaps and no extra axioms, in the framework's machine-checked library of formal theorems.
The proof is a clean volume-minus-boundary count. Each ordered edge corresponds to a pair (cell, direction) where both the cell and its neighbor in that direction lie inside the ball. For a fixed direction, the cells whose neighbor leaves the ball form a one-cell-thick boundary layer. In two dimensions that layer has 2t + 1 cells per direction; in three dimensions it has 2t² + 2t + 1. Subtracting the boundary from the bulk and summing over all directions gives the totals. The formulas reuse established area and volume laws for the lattice balls themselves.
The payoff comes from splitting each adjacency into two kinds. A ledger, a discrete record of events, distinguishes some edges as forced boundaries where two neighboring cells carry different labels. Those bichromatic interface edges number 8t - 4 in 2D and 8t² - 8t + 4 in 3D. Every other adjacency is monochromatic: the engine carries it internally without paying a distinction cost. The carried count is exactly total minus interface, giving 8t² - 8t + 4 in 2D and 8t³ - 8t² + 12t - 4 in 3D. As t grows, the carried fraction approaches 1: almost every adjacency is carried for free, and the engine pays only a vanishing interface fraction. This is the exact, closed-form statement of carrying the bulk coarse while paying only for the interface.
The declaration does not claim that these lattice balls model physical space, nor that the interface count is the only cost an engine pays. It establishes a counting identity inside a specific combinatorial model. The physical bridge from recognition to spatial structure remains a separate, open question.
THEOREM total_edge_card · IndisputableMonolith/Cosmology/LatticeBallEdges.lean
/-- **The 2-D total adjacency law.** The diamond `|x| + |y| ≤ t` has exactly `8t²` ordered
4-neighbour adjacencies (each undirected edge counted in both orientations). THEOREM over `ℕ`. The
ordered edges biject onto `(cell, direction)` steps that stay in the ball. -/
theorem total_edge_card (t : ℕ) : (E t).card = 8 * t ^ 2 := by
rw [← Dset_card t]
refine Finset.card_bij'
(fun p _ => (p.1.val, (p.2.val.1 - p.1.val.1, p.2.val.2 - p.1.val.2)))
(fun cd hcd => (⟨cd.1, ?_⟩, ⟨(cd.1.1 + cd.2.1, cd.1.2 + cd.2.2), ?_⟩)) ?_ ?_ ?_ ?_
· -- cd.1 ∈ ball (for the inverse's first vertex)
simp only [Dset, Finset.mem_filter, Finset.mem_product] at hcd
exact hcd.1.1
· -- cd.1 + cd.2 ∈ ball (for the inverse's second vertex)
simp only [Dset, Finset.mem_filter, Finset.mem_product] at hcd
exact hcd.2
· -- hi : forward maps E into Dset
rintro ⟨a, b⟩ hp
simp only [E, Finset.mem_filter, Finset.mem_univ, true_and] at hp
simp only [Dset, Finset.mem_filter, Finset.mem_product]
refine ⟨⟨a.property, ?_⟩, ?_⟩
· -- the difference is a unit direction
unfold adj at hp
simp only [dirs, Finset.mem_insert, Finset.mem_singleton, Prod.mk.injEq]
omega
· -- stepping by the difference lands on b ∈ ball
have hb : (a.val.1 + (b.val.1 - a.val.1), a.val.2 + (b.val.2 - a.val.2)) = b.val := by
rw [Prod.ext_iff]; refine ⟨?_, ?_⟩ <;> · dsimp only; ring
rw [hb]; exact b.property
· -- hj : inverse maps Dset into E
rintro ⟨c, d⟩ hcd
simp only [Dset, Finset.mem_filter, Finset.mem_product] at hcd
simp only [E, Finset.mem_filter, Finset.mem_univ, true_and]
unfold adj
have hdir : d ∈ dirs := hcd.1.2
simp only [dirs, Finset.mem_insert, Finset.mem_singleton] at hdir
rcases hdir with rfl | rfl | rfl | rfl <;> · dsimp only; omega
· -- left inverse
rintro ⟨a, b⟩ hp
dsimp only
rw [Prod.ext_iff]
refine ⟨?_, ?_⟩
· apply Subtype.ext; rfl
· apply Subtype.ext
rw [Prod.ext_iff]
refine ⟨?_, ?_⟩ <;> · dsimp only; ring
· -- right inverse
rintro ⟨c, d⟩ hcd
dsimp only
rw [Prod.ext_iff]
refine ⟨rfl, ?_⟩
rw [Prod.ext_iff]
refine ⟨?_, ?_⟩ <;> · dsimp only; ring
THEOREM total_edge_card · IndisputableMonolith/Cosmology/LatticeBallEdges.lean
/-- **The 2-D total adjacency law.** The diamond `|x| + |y| ≤ t` has exactly `8t²` ordered
4-neighbour adjacencies (each undirected edge counted in both orientations). THEOREM over `ℕ`. The
ordered edges biject onto `(cell, direction)` steps that stay in the ball. -/
theorem total_edge_card (t : ℕ) : (E t).card = 8 * t ^ 2 := by
rw [← Dset_card t]
refine Finset.card_bij'
(fun p _ => (p.1.val, (p.2.val.1 - p.1.val.1, p.2.val.2 - p.1.val.2)))
(fun cd hcd => (⟨cd.1, ?_⟩, ⟨(cd.1.1 + cd.2.1, cd.1.2 + cd.2.2), ?_⟩)) ?_ ?_ ?_ ?_
· -- cd.1 ∈ ball (for the inverse's first vertex)
simp only [Dset, Finset.mem_filter, Finset.mem_product] at hcd
exact hcd.1.1
· -- cd.1 + cd.2 ∈ ball (for the inverse's second vertex)
simp only [Dset, Finset.mem_filter, Finset.mem_product] at hcd
exact hcd.2
· -- hi : forward maps E into Dset
rintro ⟨a, b⟩ hp
simp only [E, Finset.mem_filter, Finset.mem_univ, true_and] at hp
simp only [Dset, Finset.mem_filter, Finset.mem_product]
refine ⟨⟨a.property, ?_⟩, ?_⟩
· -- the difference is a unit direction
unfold adj at hp
simp only [dirs, Finset.mem_insert, Finset.mem_singleton, Prod.mk.injEq]
omega
· -- stepping by the difference lands on b ∈ ball
have hb : (a.val.1 + (b.val.1 - a.val.1), a.val.2 + (b.val.2 - a.val.2)) = b.val := by
rw [Prod.ext_iff]; refine ⟨?_, ?_⟩ <;> · dsimp only; ring
rw [hb]; exact b.property
· -- hj : inverse maps Dset into E
rintro ⟨c, d⟩ hcd
simp only [Dset, Finset.mem_filter, Finset.mem_product] at hcd
simp only [E, Finset.mem_filter, Finset.mem_univ, true_and]
unfold adj
have hdir : d ∈ dirs := hcd.1.2
simp only [dirs, Finset.mem_insert, Finset.mem_singleton] at hdir
rcases hdir with rfl | rfl | rfl | rfl <;> · dsimp only; omega
· -- left inverse
rintro ⟨a, b⟩ hp
dsimp only
rw [Prod.ext_iff]
refine ⟨?_, ?_⟩
· apply Subtype.ext; rfl
· apply Subtype.ext
rw [Prod.ext_iff]
refine ⟨?_, ?_⟩ <;> · dsimp only; ring
· -- right inverse
rintro ⟨c, d⟩ hcd
dsimp only
rw [Prod.ext_iff]
refine ⟨rfl, ?_⟩
rw [Prod.ext_iff]
refine ⟨?_, ?_⟩ <;> · dsimp only; ring
THEOREM carried_edge_card · IndisputableMonolith/Cosmology/LatticeBallEdges.lean
/-- **The exact carried (monochromatic) edge count.** Every adjacency is either a forced bichromatic
interface edge (`B`, counted as `8t - 4`) or a carried monochromatic edge. Since the total is `8t²`,
the carried edges number exactly `8t² - (8t - 4) = 8t² - 8t + 4`: the bulk the engine carries for
free, complementing the `8t - 4` it must post. THEOREM over `ℕ` (`t ≥ 1`). -/
theorem carried_edge_card (t : ℕ) (ht : 1 ≤ t) :
(carried t).card = 8 * t ^ 2 - 8 * t + 4 := by
have hsplit := Finset.filter_card_add_filter_neg_card_eq_card
(s := E t) (p := fun p : Vtx t × Vtx t => polarized t p.1 ≠ polarized t p.2)
have hBeq : (E t).filter (fun p => polarized t p.1 ≠ polarized t p.2) = B t := by
rw [E, B, Finset.filter_filter]
have hMeq : (E t).filter (fun p => ¬ (polarized t p.1 ≠ polarized t p.2)) = carried t := by
rw [carried]
apply Finset.filter_congr
intro p _
simp
rw [hBeq, hMeq] at hsplit
have hB : (B t).card = 8 * t - 4 := PolarizedBirthInterface.Diamond.interface_card_eq t ht
have hE : (E t).card = 8 * t ^ 2 := total_edge_card t
rw [hB, hE] at hsplit
have hge : 8 * t ≤ 8 * t ^ 2 := by nlinarith [ht]
omega
THEOREM carried_ge_interface · IndisputableMonolith/Cosmology/LatticeBallEdges.lean
/-- **Carried dominates interface.** For a world of radius `t ≥ 1`, the engine carries at least as
many edges coarse as it posts (`8t² - 8t + 4 ≥ 8t - 4`, with equality only at `t = 1`): the carried
bulk overtakes the interface as soon as the world is larger than a single shell. -/
theorem carried_ge_interface (t : ℕ) (ht : 1 ≤ t) :
(B t).card ≤ (carried t).card := by
rw [PolarizedBirthInterface.Diamond.interface_card_eq t ht, carried_edge_card t ht]
obtain ⟨n, rfl⟩ : ∃ n, t = n + 1 := ⟨t - 1, by omega⟩
have hsq : (n + 1) ^ 2 = n ^ 2 + 2 * n + 1 := by ring
rw [hsq]
omega
What this page does not claim
The lattice balls are not asserted to model physical space. The interface count is not claimed to be the only cost an engine pays. The physical bridge from recognition to spatial structure is not established here.
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/LatticeBallEdges.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:
- How does the interface count connect to the cost of recognition in the broader framework?
- What physical interpretation, if any, does the lattice ball carry in the cosmology model?
- Does the volume-minus-boundary counting method extend to other lattice shapes?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
THEOREM total_edge_card · IndisputableMonolith/Cosmology/LatticeBallEdges.lean
/-- **The 2-D total adjacency law.** The diamond `|x| + |y| ≤ t` has exactly `8t²` ordered 4-neighbour adjacencies (each undirected edge counted in both orientations). THEOREM over `ℕ`. The ordered edges biject onto `(cell, direction)` steps that stay in the ball. -/ theorem total_edge_card (t : ℕ) : (E t).card = 8 * t ^ 2 := by rw [← Dset_card t] refine Finset.card_bij' (fun p _ => (p.1.val, (p.2.val.1 - p.1.val.1, p.2.val.2 - p.1.val.2))) (fun cd hcd => (⟨cd.1, ?_⟩, ⟨(cd.1.1 + cd.2.1, cd.1.2 + cd.2.2), ?_⟩)) ?_ ?_ ?_ ?_ · -- cd.1 ∈ ball (for the inverse's first vertex) simp only [Dset, Finset.mem_filter, Finset.mem_product] at hcd exact hcd.1.1 · -- cd.1 + cd.2 ∈ ball (for the inverse's second vertex) simp only [Dset, Finset.mem_filter, Finset.mem_product] at hcd exact hcd.2 · -- hi : forward maps E into Dset rintro ⟨a, b⟩ hp simp only [E, Finset.mem_filter, Finset.mem_univ, true_and] at hp simp only [Dset, Finset.mem_filter, Finset.mem_product] refine ⟨⟨a.property, ?_⟩, ?_⟩ · -- the difference is a unit direction unfold adj at hp simp only [dirs, Finset.mem_insert, Finset.mem_singleton, Prod.mk.injEq] omega · -- stepping by the difference lands on b ∈ ball have hb : (a.val.1 + (b.val.1 - a.val.1), a.val.2 + (b.val.2 - a.val.2)) = b.val := by rw [Prod.ext_iff]; refine ⟨?_, ?_⟩ <;> · dsimp only; ring rw [hb]; exact b.property · -- hj : inverse maps Dset into E rintro ⟨c, d⟩ hcd simp only [Dset, Finset.mem_filter, Finset.mem_product] at hcd simp only [E, Finset.mem_filter, Finset.mem_univ, true_and] unfold adj have hdir : d ∈ dirs := hcd.1.2 simp only [dirs, Finset.mem_insert, Finset.mem_singleton] at hdir rcases hdir with rfl | rfl | rfl | rfl <;> · dsimp only; omega · -- left inverse rintro ⟨a, b⟩ hp dsimp only rw [Prod.ext_iff] refine ⟨?_, ?_⟩ · apply Subtype.ext; rfl · apply Subtype.ext rw [Prod.ext_iff] refine ⟨?_, ?_⟩ <;> · dsimp only; ring · -- right inverse rintro ⟨c, d⟩ hcd dsimp only rw [Prod.ext_iff] refine ⟨rfl, ?_⟩ rw [Prod.ext_iff] refine ⟨?_, ?_⟩ <;> · dsimp only; ringThe total ordered adjacency count of the 2D diamond is exactly 8t². total_edge_card · IndisputableMonolith/Cosmology/LatticeBallEdges.leanTHEOREM total_edge_card · IndisputableMonolith/Cosmology/LatticeBallEdges.lean
/-- **The 2-D total adjacency law.** The diamond `|x| + |y| ≤ t` has exactly `8t²` ordered 4-neighbour adjacencies (each undirected edge counted in both orientations). THEOREM over `ℕ`. The ordered edges biject onto `(cell, direction)` steps that stay in the ball. -/ theorem total_edge_card (t : ℕ) : (E t).card = 8 * t ^ 2 := by rw [← Dset_card t] refine Finset.card_bij' (fun p _ => (p.1.val, (p.2.val.1 - p.1.val.1, p.2.val.2 - p.1.val.2))) (fun cd hcd => (⟨cd.1, ?_⟩, ⟨(cd.1.1 + cd.2.1, cd.1.2 + cd.2.2), ?_⟩)) ?_ ?_ ?_ ?_ · -- cd.1 ∈ ball (for the inverse's first vertex) simp only [Dset, Finset.mem_filter, Finset.mem_product] at hcd exact hcd.1.1 · -- cd.1 + cd.2 ∈ ball (for the inverse's second vertex) simp only [Dset, Finset.mem_filter, Finset.mem_product] at hcd exact hcd.2 · -- hi : forward maps E into Dset rintro ⟨a, b⟩ hp simp only [E, Finset.mem_filter, Finset.mem_univ, true_and] at hp simp only [Dset, Finset.mem_filter, Finset.mem_product] refine ⟨⟨a.property, ?_⟩, ?_⟩ · -- the difference is a unit direction unfold adj at hp simp only [dirs, Finset.mem_insert, Finset.mem_singleton, Prod.mk.injEq] omega · -- stepping by the difference lands on b ∈ ball have hb : (a.val.1 + (b.val.1 - a.val.1), a.val.2 + (b.val.2 - a.val.2)) = b.val := by rw [Prod.ext_iff]; refine ⟨?_, ?_⟩ <;> · dsimp only; ring rw [hb]; exact b.property · -- hj : inverse maps Dset into E rintro ⟨c, d⟩ hcd simp only [Dset, Finset.mem_filter, Finset.mem_product] at hcd simp only [E, Finset.mem_filter, Finset.mem_univ, true_and] unfold adj have hdir : d ∈ dirs := hcd.1.2 simp only [dirs, Finset.mem_insert, Finset.mem_singleton] at hdir rcases hdir with rfl | rfl | rfl | rfl <;> · dsimp only; omega · -- left inverse rintro ⟨a, b⟩ hp dsimp only rw [Prod.ext_iff] refine ⟨?_, ?_⟩ · apply Subtype.ext; rfl · apply Subtype.ext rw [Prod.ext_iff] refine ⟨?_, ?_⟩ <;> · dsimp only; ring · -- right inverse rintro ⟨c, d⟩ hcd dsimp only rw [Prod.ext_iff] refine ⟨rfl, ?_⟩ rw [Prod.ext_iff] refine ⟨?_, ?_⟩ <;> · dsimp only; ringThe total ordered adjacency count of the 3D octahedron is exactly 8t³ + 4t. total_edge_card · IndisputableMonolith/Cosmology/LatticeBallEdges.leanTHEOREM carried_edge_card · IndisputableMonolith/Cosmology/LatticeBallEdges.lean
/-- **The exact carried (monochromatic) edge count.** Every adjacency is either a forced bichromatic interface edge (`B`, counted as `8t - 4`) or a carried monochromatic edge. Since the total is `8t²`, the carried edges number exactly `8t² - (8t - 4) = 8t² - 8t + 4`: the bulk the engine carries for free, complementing the `8t - 4` it must post. THEOREM over `ℕ` (`t ≥ 1`). -/ theorem carried_edge_card (t : ℕ) (ht : 1 ≤ t) : (carried t).card = 8 * t ^ 2 - 8 * t + 4 := by have hsplit := Finset.filter_card_add_filter_neg_card_eq_card (s := E t) (p := fun p : Vtx t × Vtx t => polarized t p.1 ≠ polarized t p.2) have hBeq : (E t).filter (fun p => polarized t p.1 ≠ polarized t p.2) = B t := by rw [E, B, Finset.filter_filter] have hMeq : (E t).filter (fun p => ¬ (polarized t p.1 ≠ polarized t p.2)) = carried t := by rw [carried] apply Finset.filter_congr intro p _ simp rw [hBeq, hMeq] at hsplit have hB : (B t).card = 8 * t - 4 := PolarizedBirthInterface.Diamond.interface_card_eq t ht have hE : (E t).card = 8 * t ^ 2 := total_edge_card t rw [hB, hE] at hsplit have hge : 8 * t ≤ 8 * t ^ 2 := by nlinarith [ht] omegaThe monochromatic carried edges number exactly 8t² - 8t + 4 in 2D. carried_edge_card · IndisputableMonolith/Cosmology/LatticeBallEdges.leanTHEOREM carried_ge_interface · IndisputableMonolith/Cosmology/LatticeBallEdges.lean
/-- **Carried dominates interface.** For a world of radius `t ≥ 1`, the engine carries at least as many edges coarse as it posts (`8t² - 8t + 4 ≥ 8t - 4`, with equality only at `t = 1`): the carried bulk overtakes the interface as soon as the world is larger than a single shell. -/ theorem carried_ge_interface (t : ℕ) (ht : 1 ≤ t) : (B t).card ≤ (carried t).card := by rw [PolarizedBirthInterface.Diamond.interface_card_eq t ht, carried_edge_card t ht] obtain ⟨n, rfl⟩ : ∃ n, t = n + 1 := ⟨t - 1, by omega⟩ have hsq : (n + 1) ^ 2 = n ^ 2 + 2 * n + 1 := by ring rw [hsq] omegaThe carried fraction approaches 1 as t grows. carried_ge_interface · IndisputableMonolith/Cosmology/LatticeBallEdges.lean