Cosmology Domain Coarsening3 D

The surface cost

Cosmology domain coarsening in three dimensions is the framework's account of how a recognition engine, a system that keeps a discrete record of events, groups a 3D field of charges into uniform regions and pays a cost to carry each region. The central result is a surface law: the cost of carrying a single growing domain of volume V scales like V^(2/3), the sharpest possible sub-extensive scaling. The engine pays for the boundary between regions, not the space inside them.

The module proves this for a separable model, where the 3D field is treated as a stack of planes, each a list of 1D fibers. Coarsening along the z-axis carries exactly the total z-interface plus the number of z-fibers, which equals the x-y cross-sectional cell count. The key theorem, zFiber_cost_eq, states this identity: rowCost (grid.flatten) = rowInterface (grid.flatten) + (grid.flatten).length. The right side has no dependence on fiber lengths. Deepening the world in z does not increase the carried cost; only adding distinctions does. This is the per-axis backbone of the surface law.

The true 3D component coarsening merges across fibers as well, so it is never worse than this separable cost. The module brackets the carried cost between the cross-section and the volume, and pins it to the interface. A strict companion theorem, foam_cost_tracks_interface, formalizes the Phase-15 foam claim: at a fixed cross-section, strictly more z-interface costs strictly more, so a finely recognized foam is carried at strictly higher cost than a coarse split of the same extent, while changing only the depth costs nothing.

A connected-graph fact supports the 3D picture: on any connected finite world, the monochromatic-component count is at most the bichromatic-edge count plus one, the 3D analogue of the 1D identity runs = boundaries + 1. This is proved dimension-free in the library. The engine's state and work are both bounded by the interface, not the volume. The cost of recognition is forced by the structure of the world, and in three dimensions that structure lives on surfaces.

/-- **The 3D separable coarsening cost = z-interface + number of z-fibers, independent of the depth.**
For any 3D grid whose z-fibers are all nonempty, coarsening along the z-axis carries exactly (the total
z-interface) plus (the number of z-fibers = the x-y cross-sectional cell count) super-regions. The right side
depends only on the interface and the cross-section, never on the fiber lengths: making the world deeper in z
does not increase the carried cost. This is the exact per-axis generalization of the 1D law
`runs = boundaries + 1`, summed over every fiber of the 3D grid, and the per-axis backbone of the surface law.
The true 3D component coarsening also merges across fibers, so it carries at most this many super-regions. -/
theorem zFiber_cost_eq (grid : List (List (List α)))
    (h : ∀ plane ∈ grid, ∀ fiber ∈ plane, fiber ≠ []) :
    rowCost (zFibers grid) = rowInterface (zFibers grid) + (zFibers grid).length :=
  rowwise_cost_eq (zFibers grid) (zFibers_nonempty grid h)

/-- **Depth independence, stated directly.** Two 3D grids with the same total z-interface and the same number
of z-fibers carry the same separable cost, regardless of how their fibers differ in length (depth). This is the
formal sense in which the 3D cost lives on the interface surface and the cross-section, not in the volume. -/
theorem zFiber_cost_depth_independent (g₁ g₂ : List (List (List α)))
    (h₁ : ∀ plane ∈ g₁, ∀ fiber ∈ plane, fiber ≠ [])
    (h₂ : ∀ plane ∈ g₂, ∀ fiber ∈ plane, fiber ≠ [])
    (hiface : rowInterface (zFibers g₁) = rowInterface (zFibers g₂))
    (hcross : (zFibers g₁).length = (zFibers g₂).length) :
    rowCost (zFibers g₁) = rowCost (zFibers g₂) := by
  rw [zFiber_cost_eq g₁ h₁, zFiber_cost_eq g₂ h₂, hiface, hcross]

/-- **The cost tracks the recognition interface, not the depth (the Phase-15 foam law, formalized).** Two 3D
grids with the same number of z-fibers (the same x-y cross-section): the one whose field carries strictly more
z-interface carries strictly more separable cost. This is the exact sense in which a finer, more recognized
structure (a foam with more domain walls) costs strictly more to carry than a coarser one at the same extent,
while deepening the world in z (changing fiber lengths, with the interface fixed) changes nothing
(`zFiber_cost_depth_independent`). The engine pays for recognition activity, not volume. -/
theorem foam_cost_tracks_interface (g₁ g₂ : List (List (List α)))
    (h₁ : ∀ plane ∈ g₁, ∀ fiber ∈ plane, fiber ≠ [])
    (h₂ : ∀ plane ∈ g₂, ∀ fiber ∈ plane, fiber ≠ [])
    (hcross : (zFibers g₁).length = (zFibers g₂).length)
    (hmore : rowInterface (zFibers g₁) < rowInterface (zFibers g₂)) :
    rowCost (zFibers g₁) < rowCost (zFibers g₂) := by
  rw [zFiber_cost_eq g₁ h₁, zFiber_cost_eq g₂ h₂, hcross]
  omega

/-- Every z-fiber is nonempty when every fiber in every plane is nonempty. -/
theorem zFibers_nonempty (grid : List (List (List α)))
    (h : ∀ plane ∈ grid, ∀ fiber ∈ plane, fiber ≠ []) :
    ∀ f ∈ zFibers grid, f ≠ [] := by
  intro f hf
  rw [zFibers, List.mem_flatten] at hf
  obtain ⟨plane, hplane, hfplane⟩ := hf
  exact h plane hplane f hfplane

What this page does not claim

The module does not prove that the true 6-connected component count equals the separable row cost. The module does not derive the physical three-dimensionality of space; that remains an open bridge. The module does not claim the cost is exactly V^(2/3) for arbitrary shapes, only for the separable model.

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/DomainCoarsening3D.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: