Encyclopedia Cosmology Cosmology Lattice Ball Edges Carried Ge Interface

ARTICLE 3 claims 3 theorems

Cosmology Lattice Ball Edges Carried Ge Interface

In a growing lattice, nearly every connection between neighboring cells is carried for free; only a vanishing fraction demands payment.

Verify this page

Carried edges and interface edges

A growing crystal of cells on a square grid. At each stage, the crystal is a diamond-shaped ball of cells. Between neighboring cells there are adjacencies, edges that connect one cell to the next. The declaration carried_ge_interface concerns two kinds of these edges. Some edges connect cells that share the same internal state; the framework calls these carried edges, meaning the engine carries them without extra cost. Other edges connect cells of different states; these are interface edges, the ones the engine pays for as it forces a distinction between neighboring regions.

The theorem states a simple inequality: in both two and three dimensions, for any crystal of radius at least one, the number of carried edges is at least the number of interface edges. In two dimensions, the carried edges number exactly 8t² - 8t + 4, while the interface edges number 8t - 4, where t is the radius. In three dimensions, the carried edges number 8t³ - 8t² + 12t - 4, and the interface edges number 8t² - 8t + 4. The inequality is not a close call; it holds by a wide margin that grows with the crystal's size.

The deeper point is what happens as the crystal grows. The total number of adjacencies in two dimensions is 8t², and the interface edges are 8t - 4. The fraction of edges that are interface edges is therefore (8t - 4)/(8t²), which shrinks toward zero as t grows. In three dimensions the same pattern holds: the interface fraction vanishes as the crystal expands. Almost every adjacency in a large crystal is a carried edge, and the engine pays only for a vanishing slice of the boundary. This is the exact, closed-form statement of a principle the framework calls carrying the bulk coarse and paying only for the interface.

The proof is a clean volume-minus-boundary count. Each adjacency corresponds to a cell and a direction: the cell plus one step in that direction must still lie inside the crystal. For a fixed direction, the cells whose neighbor leaves the crystal form a codimension-one boundary layer. In two dimensions that layer has 2t + 1 cells; in three dimensions it has 2t² + 2t + 1 cells. Subtracting the boundary from the bulk and summing over all directions gives the total edge count. The carried edges are then the total minus the interface edges, since every adjacency is one or the other.

What the declaration does not claim is just as important. It does not say that the engine actually operates this way in physical spacetime; the bridge from these lattice counts to physical recognition is a separate, open question. It does not claim that the inequality is tight, only that it holds. And it does not assert anything about the fine-structure constant or any measured physical constant; the counts are pure combinatorial theorems about integer lattices.

THEOREM carried_ge_interface · 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
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 lattice counts do not by themselves establish any claim about physical spacetime. The inequality is not asserted to be tight; it is a lower bound, not an equality. No measured physical constant follows from these combinatorial theorems.

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