Encyclopedia Cosmology Cosmology Lattice Ball Edges Three Mul Dset Card

ARTICLE 3 claims 3 theorems

Cosmology Lattice Ball Edges Three Mul Dset Card

A machine-checked theorem gives the exact number of neighbor links inside a growing three-dimensional lattice ball, revealing how much of its structure is carried for free.

Verify this page

Counting Adjacencies

In a three-dimensional grid, take all points within a distance t of the origin, forming a ball. Connect each point to its six immediate neighbors. The declaration three_mul_Dset_card establishes a precise count of these connections: three times the number of ordered adjacencies equals 24t³ + 12t, meaning the total is 8t³ + 4t. This is a proved theorem over the natural numbers, verified by a machine-checked library of formal theorems with no unproven assumptions.

The proof works by a volume-minus-boundary argument. For each of the six directions, count the points whose neighbor in that direction stays inside the ball. Points whose neighbor leaves the ball form a boundary layer; in three dimensions that layer has 2t² + 2t + 1 points. Subtracting the boundary from the bulk for each direction and summing gives the total. The same method yields the two-dimensional analogue: 8t² adjacencies for the square lattice.

The count matters because it splits every adjacency into two kinds. A ledger, a discrete record of events, distinguishes between edges that carry internal structure and edges that mark a forced boundary. The theorem pairs with a companion result: the number of carried edges, those connecting points of the same type, equals 8t³ - 8t² + 12t - 4. As t grows, the fraction of adjacencies that are carried approaches 1, so the engine pays for only a vanishing share of its connections.

In Recognition Science, this closed form supports the claim that a coarsening process can carry the bulk of its structure for free while paying only for the interface. The framework models recognition events as costs, and this count shows the cost of maintaining internal adjacencies grows slower than the total. The theorem is a statement about a specific lattice model, not a claim about physical space itself.

The declaration does not claim that three-dimensional space is physically made of such a lattice, nor that the count applies to any other adjacency scheme. It proves a combinatorial identity for one defined object: the ordered edges of the L1 ball with six-neighbor adjacency. The result is exact and general over t, but its reach is bounded by the model it describes.

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 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

What this page does not claim

The theorem does not assert that physical space is a lattice. The count applies only to the six-neighbor octahedron model, not to other adjacency schemes. The result does not establish any property of the framework's cost function.

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