IndisputableMonolith.Cosmology.DomainCoarsening3D

   1import IndisputableMonolith.Cosmology.DomainCoarsening2D
   2
   3/-!
   4# The coarsening cost in three dimensions: the cost lives on a surface, not in the volume
   5
   6## Status: THEOREM (0 sorry, 0 axiom beyond Mathlib's standard three).
   7
   8This module backs `scripts/cosmogenesis/domain_coarsen_3d.py`, which takes the locked-domain coarsening into
   9the dimension the forcing chain actually selects (T8: D = 3, `Foundation.UnifiedForcingChain`). A locked domain
  10is now a maximal 6-connected component of equal charge, carried as one coarse super-region; the
  11recognition-active interface between domains is a 2D surface, so the engine cost localizes to a surface and a
  12single growing domain of volume `V` is carried at cost set by its surface `~ V^(2/3)`: the sharpest
  13sub-extensive scaling, and the honest endpoint of "carry each region at the coarsest phi-rung its recognition
  14allows" in the dimension reality has.
  15
  16As in 2D, the exact analogue of the 1D identity `runs = boundaries + 1` is the inequality
  17`components <= bichromatic + 1` (a 3D interface can be multiply connected), a connected-graph fact
  18(component-counting-under-edge-deletion). That fact is now a Lean THEOREM, dimension-free, in
  19`Cosmology.InterfaceComponentBound.mono_components_le_bichromatic_succ`: on any connected finite world the
  20monochromatic-component count is at most the bichromatic-edge count plus one. The 3D octahedral lattice is one
  21instance of its connected-ambient hypothesis (wiring the specific 6-neighbour lattice graph and identifying the
  22flood-fill components with the graph components is the routine remaining step; the hard content, the
  23edge-deletion merge bound Mathlib lacked, is discharged there).
  24
  25What IS a clean theorem, and what this module proves, is the SEPARABLE (per-axis fiber) coarsening cost, and
  26the new 3D content is that it is INDEPENDENT OF THE DEPTH. Model the 3D field as a list of planes, each a list
  27of 1D fibers (`List (List (List α))`, indexed `[x][y][z]`). The list of all z-fibers is `grid.flatten` (flatten
  28the x and y levels). Coarsening along z carries `rowCost (grid.flatten)` super-regions (the sum of `runs` over
  29all z-fibers), and `zFiber_cost_eq` proves, for any grid whose fibers are all nonempty,
  30
  31  `rowCost (grid.flatten) = rowInterface (grid.flatten) + (grid.flatten).length`,
  32
  33i.e. the separable coarsening carries exactly (the total z-interface) plus (the number of z-fibers = the x-y
  34cross-sectional cell count) super-regions. The right side has NO dependence on the fiber lengths: deepening the
  35world in z does not increase the carried cost, only adding distinctions does. This is the per-axis backbone of
  36the 3D surface law. The true 3D component coarsening merges across fibers as well, so it is never worse:
  37`components_3D <= rowCost`, bracketed below by the cross-section and above by the volume
  38(`zFiber_cost_le_volume`), and pinned to the interface. Composed with `Cosmology.RecognitionWorkBound` (the
  39resolution cost per cadence cycle is bounded by the cadence INDEPENDENT of the index type, so it covers 3D
  40cells verbatim), the 3D engine's state and work are both bounded by the interface, not the volume.
  41
  42The strict companion `foam_cost_tracks_interface` makes the Phase-15 multi-domain ("recognition foam") claim
  43formal: at a fixed cross-section, strictly more z-interface costs strictly more, so a finely recognized foam is
  44carried at strictly higher cost than a coarse split of the same extent, while changing only the depth costs
  45nothing. The engine pays for recognition activity, not volume. (The numeric foam driver
  46`scripts/cosmogenesis/domain_coarsen_foam_3d.py` measures the true 6-connected component count, which this
  47separable cost upper-bounds.)
  48-/
  49
  50namespace IndisputableMonolith
  51namespace Cosmology
  52namespace DomainCoarsening3D
  53
  54open IndisputableMonolith.Cosmology.DomainCoarsening
  55open IndisputableMonolith.Cosmology.DomainCoarsening2D
  56
  57variable {α : Type*} [DecidableEq α]
  58
  59/-- The list of all 1D z-fibers of a 3D grid indexed `[x][y][z]`: flatten the x and y levels. Each z-fiber is
  60the charge column at a fixed `(x, y)`; the engine coarsens each fiber into its maximal equal-charge runs. -/
  61def zFibers (grid : List (List (List α))) : List (List α) := grid.flatten
  62
  63omit [DecidableEq α] in
  64@[simp] theorem zFibers_nil : zFibers ([] : List (List (List α))) = [] := rfl
  65
  66omit [DecidableEq α] in
  67/-- Every z-fiber is nonempty when every fiber in every plane is nonempty. -/
  68theorem zFibers_nonempty (grid : List (List (List α)))
  69    (h : ∀ plane ∈ grid, ∀ fiber ∈ plane, fiber ≠ []) :
  70    ∀ f ∈ zFibers grid, f ≠ [] := by
  71  intro f hf
  72  rw [zFibers, List.mem_flatten] at hf
  73  obtain ⟨plane, hplane, hfplane⟩ := hf
  74  exact h plane hplane f hfplane
  75
  76/-- **The 3D separable coarsening cost = z-interface + number of z-fibers, independent of the depth.**
  77For any 3D grid whose z-fibers are all nonempty, coarsening along the z-axis carries exactly (the total
  78z-interface) plus (the number of z-fibers = the x-y cross-sectional cell count) super-regions. The right side
  79depends only on the interface and the cross-section, never on the fiber lengths: making the world deeper in z
  80does not increase the carried cost. This is the exact per-axis generalization of the 1D law
  81`runs = boundaries + 1`, summed over every fiber of the 3D grid, and the per-axis backbone of the surface law.
  82The true 3D component coarsening also merges across fibers, so it carries at most this many super-regions. -/
  83theorem zFiber_cost_eq (grid : List (List (List α)))
  84    (h : ∀ plane ∈ grid, ∀ fiber ∈ plane, fiber ≠ []) :
  85    rowCost (zFibers grid) = rowInterface (zFibers grid) + (zFibers grid).length :=
  86  rowwise_cost_eq (zFibers grid) (zFibers_nonempty grid h)
  87
  88/-- The carried separable cost never exceeds the volume: the number of coarse super-regions along z is at most
  89the total number of cells (each fiber coarsens into at most as many runs as it has cells, `runs_le_length`).
  90Together with `zFiber_cost_eq`, the carried cost is bracketed `(#z-fibers) <= rowCost <= (volume)` and pinned
  91to the z-interface, so when the interface grows as a surface while the volume grows as `t^3`, the carried cost
  92is sub-extensive in the volume. -/
  93theorem zFiber_cost_le_volume (grid : List (List (List α))) :
  94    rowCost (zFibers grid) ≤ ((zFibers grid).map List.length).sum := by
  95  show ((zFibers grid).map runs).sum ≤ ((zFibers grid).map List.length).sum
  96  exact List.sum_le_sum (fun fiber _ => runs_le_length fiber)
  97
  98/-- **Depth independence, stated directly.** Two 3D grids with the same total z-interface and the same number
  99of z-fibers carry the same separable cost, regardless of how their fibers differ in length (depth). This is the
 100formal sense in which the 3D cost lives on the interface surface and the cross-section, not in the volume. -/
 101theorem zFiber_cost_depth_independent (g₁ g₂ : List (List (List α)))
 102    (h₁ : ∀ plane ∈ g₁, ∀ fiber ∈ plane, fiber ≠ [])
 103    (h₂ : ∀ plane ∈ g₂, ∀ fiber ∈ plane, fiber ≠ [])
 104    (hiface : rowInterface (zFibers g₁) = rowInterface (zFibers g₂))
 105    (hcross : (zFibers g₁).length = (zFibers g₂).length) :
 106    rowCost (zFibers g₁) = rowCost (zFibers g₂) := by
 107  rw [zFiber_cost_eq g₁ h₁, zFiber_cost_eq g₂ h₂, hiface, hcross]
 108
 109/-- **The cost tracks the recognition interface, not the depth (the Phase-15 foam law, formalized).** Two 3D
 110grids with the same number of z-fibers (the same x-y cross-section): the one whose field carries strictly more
 111z-interface carries strictly more separable cost. This is the exact sense in which a finer, more recognized
 112structure (a foam with more domain walls) costs strictly more to carry than a coarser one at the same extent,
 113while deepening the world in z (changing fiber lengths, with the interface fixed) changes nothing
 114(`zFiber_cost_depth_independent`). The engine pays for recognition activity, not volume. -/
 115theorem foam_cost_tracks_interface (g₁ g₂ : List (List (List α)))
 116    (h₁ : ∀ plane ∈ g₁, ∀ fiber ∈ plane, fiber ≠ [])
 117    (h₂ : ∀ plane ∈ g₂, ∀ fiber ∈ plane, fiber ≠ [])
 118    (hcross : (zFibers g₁).length = (zFibers g₂).length)
 119    (hmore : rowInterface (zFibers g₁) < rowInterface (zFibers g₂)) :
 120    rowCost (zFibers g₁) < rowCost (zFibers g₂) := by
 121  rw [zFiber_cost_eq g₁ h₁, zFiber_cost_eq g₂ h₂, hcross]
 122  omega
 123
 124end DomainCoarsening3D
 125end Cosmology
 126end IndisputableMonolith
 127