Encyclopedia Cosmology Cosmology Domain Coarsening3 D Z Fiber Cost Eq

ARTICLE 4 claims 4 theorems

Cosmology Domain Coarsening3 D Z Fiber Cost Eq

A machine-checked theorem shows that in a three-dimensional grid, the cost of recording a pattern depends on its surface, not on how deep the volume is.

Verify this page

The cost of depth

In the Recognition Science framework, reality keeps a ledger, a discrete record of recognition events, and the cost of maintaining that record is forced by a proved uniqueness theorem. The framework's library, a machine-checked collection of formal theorems, applies this idea to a three-dimensional grid of cells, each holding a charge. The declaration zFiber_cost_eq proves a precise statement about how the cost of coarsening, or simplifying, this grid behaves when you look along one axis, the z-axis.

Think of the grid as a stack of flat planes, each plane a list of vertical columns. The theorem says that the cost of coarsening all these columns is exactly equal to two things added together: the total number of boundaries between different charges along the columns, plus the total number of columns themselves. The number of columns is just the size of the x-y cross-section. The key result is that this total cost has no dependence on the length of the columns. Making the world deeper in the z-direction does not increase the carried cost; only adding more distinctions within a column does.

This is the formal backbone of a surface law. The true three-dimensional coarsening, which merges across columns as well, is never worse than this per-axis cost. The carried cost is bracketed below by the cross-section and above by the total volume, and it is pinned to the interface between different charges. A companion theorem, foam_cost_tracks_interface, makes this precise: at a fixed cross-section, a field with more z-interface costs strictly more to carry, while changing only the depth costs nothing. The engine pays for recognition activity, not for volume.

What the theorem does not claim is equally important. It proves a statement about a separable, per-axis coarsening cost, not about the full connected-component coarsening of the three-dimensional grid. The theorem's condition requires every z-fiber to be nonempty. It does not claim that the true three-dimensional cost is exactly this value; it only establishes an upper bound. The physical bridge from this topological theorem to a claim about the actual three-dimensional space we inhabit remains an open target, not a proved result.

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 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 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 claim that the true three-dimensional component coarsening cost is exactly this separable value. The theorem does not claim that the physical three-dimensional space we inhabit is governed by this cost law without a further bridge. The theorem does not claim that the cost is independent of depth for coarsening along the x or y axes.

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