Encyclopedia Cosmology Cosmology Domain Coarsening3 D Z Fiber Cost Le Volume

ARTICLE 4 claims 4 theorems

Cosmology Domain Coarsening3 D Z Fiber Cost Le Volume

A machine-checked theorem shows that the cost of tracking a growing three-dimensional region is set by its surface, not by the space it fills.

Verify this page

The surface cost bound

In a discrete model where a three-dimensional field is stored as a stack of planes, each plane a grid of one-dimensional columns, the cost of coarsening along the depth axis is bounded by the total number of cells in the field. This is the statement of zFiber_cost_le_volume, a theorem in the framework's machine-checked library of formal theorems. The bound is not an equality; it says the carried cost never exceeds the volume, and the proof is a simple per-column argument: each column coarsens into at most as many runs as it has cells.

The deeper content is a companion equality. For any such grid with nonempty columns, the coarsening cost equals the total interface along the depth axis plus the number of columns. The number of columns is the cross-sectional cell count, and the interface is the count of boundaries between distinct charge regions. Because the cost depends only on these two quantities, and not on the column lengths, making the world deeper in the depth direction does not increase the cost. This is the formal sense in which the cost lives on the surface, not in the volume.

In Recognition Science, this result is the per-axis backbone of a surface law for three dimensions. The framework models a locked domain as a maximal connected component of equal charge, and the recognition-active interface between domains is a two-dimensional surface. A single growing domain of volume V is carried at a cost set by its surface, scaling as V to the two-thirds power. The theorem brackets the separable cost between the cross-section and the volume, and pins it to the interface, so when the interface grows as a surface while the volume grows as the cube of time, the carried cost is sub-extensive in the volume.

The theorem does not claim that the true three-dimensional component coarsening equals this separable cost. The true coarsening merges across columns as well, so it is never worse than the separable bound, but the exact component count on the octahedral lattice remains a routine wiring step. The theorem also does not claim that the cost is independent of the interface; a companion strict inequality shows that more interface costs strictly more at a fixed cross-section. The engine pays for recognition activity, not volume, but the bound itself is only an upper limit, not a full description of the coarsening process.

THEOREM zFiber_cost_le_volume · IndisputableMonolith/Cosmology/DomainCoarsening3D.lean
zFiber_cost_le_volume · IndisputableMonolith/Cosmology/DomainCoarsening3D.lean:88 
/-- The carried separable cost never exceeds the volume: the number of coarse super-regions along z is at most
the total number of cells (each fiber coarsens into at most as many runs as it has cells, `runs_le_length`).
Together with `zFiber_cost_eq`, the carried cost is bracketed `(#z-fibers) <= rowCost <= (volume)` and pinned
to the z-interface, so when the interface grows as a surface while the volume grows as `t^3`, the carried cost
is sub-extensive in the volume. -/
theorem zFiber_cost_le_volume (grid : List (List (List α))) :
    rowCost (zFibers grid) ≤ ((zFibers grid).map List.length).sum := by
  show ((zFibers grid).map runs).sum ≤ ((zFibers grid).map List.length).sum
  exact List.sum_le_sum (fun fiber _ => runs_le_length fiber)
THEOREM zFiber_cost_eq · IndisputableMonolith/Cosmology/DomainCoarsening3D.lean
zFiber_cost_eq · IndisputableMonolith/Cosmology/DomainCoarsening3D.lean:76 
/-- **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)
THEOREM zFiber_cost_depth_independent · IndisputableMonolith/Cosmology/DomainCoarsening3D.lean
zFiber_cost_depth_independent · IndisputableMonolith/Cosmology/DomainCoarsening3D.lean:98 
/-- **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]
THEOREM foam_cost_tracks_interface · IndisputableMonolith/Cosmology/DomainCoarsening3D.lean
foam_cost_tracks_interface · IndisputableMonolith/Cosmology/DomainCoarsening3D.lean:109 
/-- **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

What this page does not claim

The theorem does not prove that the true three-dimensional component coarsening equals the separable cost. The theorem does not claim that the cost is independent of the interface, only of the depth. The theorem does not establish the surface law for the full three-dimensional component coarsening, only for the separable per-axis cost.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND