Encyclopedia Cosmology Cosmology Lattice Ball Edges
ARTICLE 5 claims 5 theorems
Cosmology Lattice Ball Edges
In a growing lattice, most connections between cells are carried for free; only a shrinking fraction at the boundary costs anything.
Counting the carried edges
A growing crystal of cells on a square grid. At each stage, the crystal is a diamond-shaped ball of radius t. The edges of the crystal are the pairs of neighboring cells that touch. A simple question: how many such adjacencies are there? The answer, proved exactly in the framework's machine-checked library of formal theorems, is 8t² for the two-dimensional diamond. In three dimensions, the ball is an octahedron and the count is 8t³ + 4t. These are not estimates; they are closed-form identities over the natural numbers, proved with no gaps and no extra axioms.
The proof is a clean volume-minus-boundary count. For each of the four unit directions in 2D, count the cells whose neighbor in that direction stays inside the ball. The cells whose neighbor leaves the ball form a one-cell-thick boundary: in 2D, one cell per row, 2t+1 of them. So each direction contributes the ball's volume minus its boundary, and summing over the four directions gives 8t². The 3D case repeats the same idea with six directions and a transverse diamond boundary of size 2t²+2t+1. The framework proves these boundary counts directly, then assembles the totals.
The payoff comes when the framework splits every adjacency into two kinds. A recognition event, a discrete record of a comparison, either forces a distinction between two neighboring cells or carries them as the same. The forced-distinction edges, the interface, number 8t−4 in 2D and 8t²−8t+4 in 3D. Subtract those from the total, and the carried edges, the ones the engine keeps without paying, are exactly 8t²−8t+4 in 2D and 8t³−8t²+12t−4 in 3D. The carried fraction approaches 1 as t grows: almost every adjacency is free, and the engine pays only for the vanishing interface.
In Recognition Science, this is the exact statement of a coarsening principle: carry the bulk coarse, pay only for the interface. The framework proves that the carried edges always outnumber the interface edges for any t at least 1, and that the interface count squared stays below a constant times the total count. The formulas are not asymptotic guesses; they are theorems, and they hold for every finite radius.
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_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
This module does not derive the interface count itself; that is proved in PolarizedBirthInterface. The formulas do not describe physical space directly; they are combinatorial facts about a lattice model. No claim is made here about the dynamics that might produce such a lattice.
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 carried-versus-interface split behave for lattices with more than six neighbors per cell?
- What physical process does the coarsening north star describe, and how does the edge count constrain it?
- Does the exact edge count extend to other regular polytope balls, such as the cross-polytope in higher dimensions?
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 two-dimensional diamond ball of radius t is 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 three-dimensional octahedron ball of radius t is 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 carried monochromatic edges in 2D number exactly 8t² − 8t + 4. carried_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 carried monochromatic edges in 3D number exactly 8t³ − 8t² + 12t − 4. 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 edges always outnumber the interface edges for any radius t at least 1. carried_ge_interface · IndisputableMonolith/Cosmology/LatticeBallEdges.lean