Encyclopedia Cosmology Cosmology Lattice Ball Edges Three Mul Total Edge Card

ARTICLE 4 claims 4 theorems

Cosmology Lattice Ball Edges Three Mul Total Edge Card

A proved formula counts every connection inside a growing three-dimensional lattice ball, and the count splits into edges the engine carries for free and edges it must pay for.

Verify this page

Counting the edges of a growing lattice ball

A three-dimensional grid of points, like the vertices of a crystal lattice, and draw a ball around the origin that contains every point whose distance from the origin is at most some whole number t. The ball grows as t increases. A natural question asks how many neighboring pairs of points, or edges, lie entirely inside that ball. For a ball in a plain cubic lattice where each point connects to its six nearest neighbors, the answer is a polynomial in t: the total number of edges equals 8t³ + 4t.

That formula is not an approximation. It is an exact statement, proved in a machine-checked library of formal theorems, and it holds for every whole number t. The proof works by a clean volume-minus-boundary argument. Each edge can be described as a point together with a direction: the point and its neighbor in that direction must both lie inside the ball. For any fixed direction, the points whose neighbor in that direction falls outside the ball form a boundary layer, and counting those layers subtracts exactly the right amount from the total volume count. The same method also gives the two-dimensional case, where the ball is a diamond shape with four-neighbor adjacency and the total edge count is 8t².

The declaration three_mul_total_edge_card states the three-dimensional result in a slightly indirect form: three times the total edge count equals 24t³ + 12t, which is just the same as saying the count itself is 8t³ + 4t. Writing it that way makes the proof cleaner, because the volume and boundary terms each carry a factor of three that cancels naturally.

In Recognition Science, this count feeds a larger picture about how a coarse-grained world is built. The framework models a process where each adjacency is either a carried edge, one whose two endpoints share the same internal state, or an interface edge, one where the states differ and the engine must pay a cost to maintain the distinction. The total edge count is the sum of both kinds. The framework proves that the carried edges number exactly 8t³ - 8t² + 12t - 4 in three dimensions, and that the fraction of carried edges approaches 1 as t grows. In plain terms: as the ball gets large, almost every connection is carried for free, and the engine pays only for a vanishingly small fraction of the total.

What the declaration does not claim is just as important as what it proves. It does not say anything about physics, about space itself, or about how this lattice relates to the actual universe. It is a statement about counting edges in a defined combinatorial object. It does not claim that the carried fraction reaches exactly one, only that it approaches one in the limit. And it does not assert that the total edge count formula applies to any other shape of ball, only to the specific octahedral ball with six-neighbor adjacency defined in the framework's library.

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 three_mul_Dset_card · IndisputableMonolith/Cosmology/LatticeBallEdges.lean
three_mul_Dset_card · IndisputableMonolith/Cosmology/LatticeBallEdges.lean:473 
/-- `3 ·` the `(cell, direction)` index count is `24t³ + 12t`: six directions, each `4t³ + 2t`. -/
theorem three_mul_Dset_card (t : ℕ) : 3 * (Dset t).card = 24 * t ^ 3 + 12 * t := by
  have hsum : (Dset t).card
      = ∑ d ∈ dirs,
          ((ball t).filter (fun p => (p.1 + d.1, p.2.1 + d.2.1, p.2.2 + d.2.2) ∈ ball t)).card := by
    rw [Dset, Finset.card_filter, Finset.sum_product, Finset.sum_comm]
    refine Finset.sum_congr rfl (fun d _ => ?_)
    rw [Finset.card_filter]
  rw [hsum, Finset.mul_sum]
  rw [Finset.sum_congr rfl (fun d hd => three_mul_step_card t d hd)]
  rw [Finset.sum_const, dirs_card]
  ring

set_option maxHeartbeats 1000000 in
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 declaration says nothing about physical space or the actual universe. The carried fraction approaches but never equals one for any finite t. The formula applies only to the specific octahedral ball with six-neighbor adjacency, not to other shapes.

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