Encyclopedia Cosmology Cosmology Lattice Ball Edges Interface Sq Le Total

ARTICLE 4 claims 4 theorems

Cosmology Lattice Ball Edges Interface Sq Le Total

In a coarse-grained lattice, the number of boundary edges between two regions grows no faster than the square root of the total number of edges, a bound the framework proves exactly.

Verify this page

The interface bound

In the Recognition Science framework, a ledger is a discrete record of events, and a recognition is the act of distinguishing one entry from another. The declaration interface_sq_le_total concerns a specific two-dimensional lattice: a diamond-shaped ball of cells with radius t, where each cell connects to its four orthogonal neighbors. The theorem states that for any radius t of at least 1, the square of the number of interface edges, those connecting cells of different types, is at most 8 times the total number of edges in the ball. This is a proved inequality over the natural numbers, with no gaps and no added assumptions.

The proof is a clean volume-minus-boundary count. The total ordered adjacency count of the diamond is exactly 8t², as proved in the theorem total_edge_card. The interface edges, those where the cell type changes, number exactly 8t - 4, from the theorem interface_card_eq. Substituting these closed forms gives the inequality (8t - 4)² ≤ 8(8t²), which the framework's library verifies by polynomial arithmetic. The same style of bound holds in three dimensions, where the cube of the interface count is at most 8 times the square of the total edge count.

In Recognition Science, this bound is the exact statement of a coarsening principle: carry the bulk coarse, pay only for the interface. The framework proves that the number of carried, or monochromatic, edges is exactly the total minus the interface, which in 2D is 8t² - 8t + 4. As the radius grows, the fraction of edges that are carried approaches 1, meaning almost every adjacency is handled for free, and the engine pays only a vanishing share for the boundary. The inequality interface_sq_le_total is the formal guarantee that this interface cost never outgrows the total by more than a square-root factor.

The declaration does not claim that the interface count is always less than the total, which would be trivial, nor that the bound is tight for every radius. It also does not claim anything about lattices other than the specific 4-neighbor diamond in 2D and the 6-neighbor octahedron in 3D. The theorem is a counting result about a fixed lattice geometry, not a statement about the physical dynamics of coarsening. What it establishes is a precise, machine-checked relationship between two quantities in a discrete model, a relationship the framework uses to reason about the cost of distinguishing regions in a coarse-grained world.

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 interface_sq_le_total · IndisputableMonolith/Cosmology/LatticeBallEdges.lean
interface_sq_le_total · IndisputableMonolith/Cosmology/LatticeBallEdges.lean:266 
/-- **Discrete isoperimetric / surface law.** The forced interface satisfies
`(interface)² ≤ 8 · (total adjacency)`, so the interface grows only as the *square root* of the bulk:
it is a codimension-1 surface, not a bulk quantity. Sharp form of "the cost is sub-extensive,
localized to a perimeter." THEOREM over `ℕ`. -/
theorem interface_sq_le_total (t : ℕ) (ht : 1 ≤ t) :
    (B t).card ^ 2 ≤ 8 * (E t).card := by
  rw [PolarizedBirthInterface.Diamond.interface_card_eq t ht, total_edge_card t]
  obtain ⟨n, rfl⟩ : ∃ n, t = n + 1 := ⟨t - 1, by omega⟩
  have hL : 8 * (n + 1) - 4 = 8 * n + 4 := by omega
  rw [hL]
  nlinarith [Nat.zero_le n]
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 interface_cube_le_total_sq · IndisputableMonolith/Cosmology/LatticeBallEdges.lean
interface_cube_le_total_sq · IndisputableMonolith/Cosmology/LatticeBallEdges.lean:577 
/-- **Discrete isoperimetric / surface law (3-D).** The forced interface satisfies
`(interface)³ ≤ 8 · (total adjacency)²`, the codimension-1 scaling in three dimensions: the interface
is `Θ(t²)` while the total adjacency is `Θ(t³)`, so the interface grows only as the `2/3` power of the
bulk. It is a surface, not a volume. THEOREM over `ℕ`. -/
theorem interface_cube_le_total_sq (t : ℕ) (ht : 1 ≤ t) :
    (B t).card ^ 3 ≤ 8 * (E t).card ^ 2 := by
  rw [PolarizedBirthInterface.Octahedron.interface_card_eq t ht, total_edge_card t]
  obtain ⟨n, rfl⟩ : ∃ n, t = n + 1 := ⟨t - 1, by omega⟩
  have hL : 8 * (n + 1) ^ 2 - 8 * (n + 1) + 4 = 8 * n ^ 2 + 8 * n + 4 := by
    have e1 : 8 * (n + 1) ^ 2 = 8 * n ^ 2 + 16 * n + 8 := by ring
    omega
  rw [hL]
  have hB : 8 * n ^ 2 + 8 * n + 4 ≤ 8 * (n + 1) ^ 2 := by nlinarith [Nat.zero_le n]
  have hE : 8 * (n + 1) ^ 3 ≤ 8 * (n + 1) ^ 3 + 4 * (n + 1) := Nat.le_add_right _ _
  calc (8 * n ^ 2 + 8 * n + 4) ^ 3
      ≤ (8 * (n + 1) ^ 2) ^ 3 := Nat.pow_le_pow_left hB 3
    _ = 8 * (8 * (n + 1) ^ 3) ^ 2 := by ring
    _ ≤ 8 * (8 * (n + 1) ^ 3 + 4 * (n + 1)) ^ 2 :=
        Nat.mul_le_mul_left 8 (Nat.pow_le_pow_left hE 2)

What this page does not claim

Not a claim that the interface count is always smaller than the total count, which is immediate from the definitions. Not a statement about the physical speed or dynamics of coarsening, only a counting relationship on a fixed lattice. Not a result for arbitrary lattice geometries, only for the 4-neighbor diamond and the 6-neighbor octahedron.

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