Encyclopedia Cosmology Cosmology Lattice Ball Edges Three Mul Step Card

ARTICLE 4 claims 4 theorems

Cosmology Lattice Ball Edges Three Mul Step Card

A machine-checked proof counts the edges of a growing three-dimensional lattice ball, revealing that almost all connections are carried for free.

Verify this page

Counting edges in a growing lattice

In the mathematics of discrete grids, a natural question is how many connections, or edges, exist inside a growing ball of lattice points. For a three-dimensional octahedral ball of radius t, where t is a positive whole number, the total number of ordered edges is 8t³ + 4t. This count includes every directed pair of adjacent points, so each undirected connection is counted twice, once in each direction.

The proof works by a clean volume-minus-boundary argument. For each of the six unit directions, one counts the cells whose neighbor in that direction still lies inside the ball. The cells that fail this test form a two-dimensional boundary layer, and their number is 2t² + 2t + 1. Subtracting this boundary from the total volume and summing over all six directions gives the total edge count. The same method works in two dimensions, where the diamond-shaped ball of radius t has 8t² ordered edges.

The declaration three_mul_step_card is a formal theorem about a single direction. It states that for any fixed unit direction d, three times the number of cells whose d-neighbor remains in the ball equals 4t³ + 2t. The factor of three appears because the proof works with a symmetrized count. This is a proved result in the machine-checked library of formal theorems, with no unproved assumptions.

In Recognition Science, this edge count feeds a larger picture. The framework models a discrete ledger of recognition events, where each adjacency is either a carried monochromatic edge or a forced bichromatic interface edge. The total minus the interface gives the carried edges: 8t³ - 8t² + 12t - 4 in three dimensions. As t grows, the carried fraction approaches 1, meaning almost every adjacency is carried for free and the engine pays only a vanishing interface fraction. This is the exact, closed-form statement of the coarsening principle: carry the bulk coarse, pay only for the interface.

What three_mul_step_card does not claim is also precise. It does not assert anything about the physical universe, only about a formal combinatorial object. It does not claim that the edge count applies to any particular lattice beyond the octahedral and diamond shapes defined in the library. And it does not claim that the interface fraction vanishes for any finite t; it only approaches zero as t grows without bound.

THEOREM three_mul_step_card · IndisputableMonolith/Cosmology/LatticeBallEdges.lean
three_mul_step_card · IndisputableMonolith/Cosmology/LatticeBallEdges.lean:433 
/-- For each unit direction, `3 ·` the count of in-ball steps is `4t³ + 2t`: the bulk
`3 · card (ball) = 4t³ + 6t² + 8t + 3` minus `3 ·` the `2t² + 2t + 1` codimension-1 boundary. -/
theorem three_mul_step_card (t : ℕ) (d : ℤ × ℤ × ℤ) (hd : d ∈ dirs) :
    3 * ((ball t).filter (fun p => (p.1 + d.1, p.2.1 + d.2.1, p.2.2 + d.2.2) ∈ ball t)).card
      = 4 * t ^ 3 + 2 * t := by
  have hvol : 3 * (ball t).card = 4 * t ^ 3 + 6 * t ^ 2 + 8 * t + 3 :=
    LatticeBallVolume.Octahedron.three_mul_card_ball t
  simp only [dirs, Finset.mem_insert, Finset.mem_singleton] at hd
  rcases hd with rfl | rfl | rfl | rfl | rfl | rfl
  · have hbd := boundary_xpos t
    have hsplit := Finset.filter_card_add_filter_neg_card_eq_card
      (s := ball t) (p := fun p : ℤ × ℤ × ℤ => (p.1 + 1, p.2.1, p.2.2) ∈ ball t)
    simp only [add_zero] at *
    omega
  · have hbd := boundary_xneg t
    have hsplit := Finset.filter_card_add_filter_neg_card_eq_card
      (s := ball t) (p := fun p : ℤ × ℤ × ℤ => (p.1 + -1, p.2.1, p.2.2) ∈ ball t)
    simp only [add_zero] at *
    omega
  · have hbd := boundary_ypos t
    have hsplit := Finset.filter_card_add_filter_neg_card_eq_card
      (s := ball t) (p := fun p : ℤ × ℤ × ℤ => (p.1, p.2.1 + 1, p.2.2) ∈ ball t)
    simp only [add_zero] at *
    omega
  · have hbd := boundary_yneg t
    have hsplit := Finset.filter_card_add_filter_neg_card_eq_card
      (s := ball t) (p := fun p : ℤ × ℤ × ℤ => (p.1, p.2.1 + -1, p.2.2) ∈ ball t)
    simp only [add_zero] at *
    omega
  · have hbd := boundary_zpos t
    have hsplit := Finset.filter_card_add_filter_neg_card_eq_card
      (s := ball t) (p := fun p : ℤ × ℤ × ℤ => (p.1, p.2.1, p.2.2 + 1) ∈ ball t)
    simp only [add_zero] at *
    omega
  · have hbd := boundary_zneg t
    have hsplit := Finset.filter_card_add_filter_neg_card_eq_card
      (s := ball t) (p := fun p : ℤ × ℤ × ℤ => (p.1, p.2.1, p.2.2 + -1) ∈ ball t)
    simp only [add_zero] at *
    omega
THEOREM total_edge_card · IndisputableMonolith/Cosmology/LatticeBallEdges.lean
total_edge_card · IndisputableMonolith/Cosmology/LatticeBallEdges.lean:179 
/-- **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
carried_edge_card · IndisputableMonolith/Cosmology/LatticeBallEdges.lean:244 
/-- **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_ge_interface · IndisputableMonolith/Cosmology/LatticeBallEdges.lean:278 
/-- **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 theorem makes no statement about physical space or cosmology. The edge count applies only to the specific octahedral and diamond lattices defined in the library. The interface fraction does not reach zero for any finite radius; it only approaches zero as t grows.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND