IndisputableMonolith.Cosmology.PolarizedBirthInterface

   1import Mathlib
   2import IndisputableMonolith.Cosmology.InterfaceComponentBound
   3import IndisputableMonolith.Cosmology.LatticeBallVolume
   4import IndisputableMonolith.Cosmology.PolarizedBirthDomains
   5
   6/-!
   7# The recognition-active interface of the birth field lives on the spine
   8
   9## Status: THEOREM (0 sorry, 0 axiom beyond Mathlib's standard three).
  10
  11Phase 50 (`PolarizedBirthDomains`) proved the *carried* side of the forced conjugate-birth field: the
  12field `+1` on `x > 0`, `-1` on `x < 0`, `0` on the `x = 0` spine is held as exactly 3 locked domains
  13for every radius, so the carried state is `O(1)` while the world is `Θ(t^d)`. This module proves the
  14complementary *interface* side: where the recognition activity (the bichromatic edges, the forced
  15distinctions) actually sits.
  16
  17The result is sharp and structural. Every bichromatic edge of the polarized field has an endpoint on
  18the spine `x = 0` (`bichromatic_endpoint_on_spine`): the charge `sign(x)` changes only across the
  19spine, so a same-row step that flips the charge must touch the column `x = 0`. Hence the entire
  20recognition-active interface is confined to the spine (`interface_on_spine`). The spine itself is a
  21ball one dimension lower: the 2D spine is the segment `|y| ≤ t` (`spine_card = 2t + 1`), the 3D spine
  22is the 2D diamond `|y| + |z| ≤ t` (`spine_card = 2t² + 2t + 1`). So the interface lives on a
  23codimension-1 set whose size is `Θ(t^{d-1})`, and `interface / volume → 0`: the cost localizes to a
  24surface, as a THEOREM, not numeric.
  25
  26Together with Phase 50 this closes both halves of the sub-extensivity picture for the birth field:
  27the carried domains are `O(1)` and the active interface is confined to a `Θ(t^{d-1})` spine, both
  28vanishing as a fraction of the `Θ(t^d)` world.
  29
  30HONEST SCOPE. This proves the interface is *confined to* the spine and that the spine is a
  31codimension-1 ball; it does not separately Lean-count the exact number of interface edges (numerically
  32`8t - 4` ordered edges in 2D), which would need an enumeration of the `toList` edge set. The
  33sub-extensivity content ("the cost lives on a lower-dimensional surface") is exactly
  34spine-confinement plus the spine cardinality, and both are theorems here.
  35-/
  36
  37namespace IndisputableMonolith
  38namespace Cosmology
  39namespace PolarizedBirthInterface
  40
  41open InterfaceComponentBound
  42
  43/-! ### The 2-D diamond: the interface is confined to the spine `x = 0`. -/
  44
  45namespace Diamond
  46
  47open InterfaceComponentBound.Diamond
  48open PolarizedBirthDomains.Diamond
  49
  50/-- **Every active edge touches the spine.** For the polarized diamond field, any two adjacent cells
  51of different charge have an endpoint on the spine `x = 0`. The charge `sign(x)` flips only between
  52columns `x = -1, 0, 1`, and a charge-flipping adjacency must step the `x`-coordinate across `0`, so
  53one endpoint sits on the spine. Pure case analysis: split the `sign` on each endpoint, then the
  54unit-distance adjacency forces the spine. -/
  55theorem bichromatic_endpoint_on_spine (t : ℕ) (a b : Vtx t)
  56    (hadj : adj a.val b.val) (hc : polarized t a ≠ polarized t b) :
  57    a.val.1 = 0 ∨ b.val.1 = 0 := by
  58  unfold adj at hadj
  59  simp only [polarized] at hc
  60  split_ifs at hc <;> omega
  61
  62/-- **The whole recognition-active interface is on the spine.** Every bichromatic edge in the
  63interface list (the forced distinctions the engine posts on the birth field) has an endpoint on the
  64spine `x = 0`. This is the exact list `InterfaceComponentBound.Diamond.mono_le_interface_succ` bounds,
  65now shown to be spine-confined. -/
  66theorem interface_on_spine (t : ℕ) :
  67    ∀ p ∈ (edges t).filter (fun q => decide (polarized t q.1 ≠ polarized t q.2)),
  68      p.1.val.1 = 0 ∨ p.2.val.1 = 0 := by
  69  intro p hp
  70  rw [List.mem_filter] at hp
  71  obtain ⟨hpe, hpc⟩ := hp
  72  rw [mem_edges] at hpe
  73  rw [decide_eq_true_eq] at hpc
  74  exact bichromatic_endpoint_on_spine t p.1 p.2 hpe hpc
  75
  76/-- The spine of the 2-D diamond: the cells on the column `x = 0`. -/
  77def spine (t : ℕ) : Finset (ℤ × ℤ) :=
  78  (InterfaceComponentBound.Diamond.ball t).filter (fun p => p.1 = 0)
  79
  80/-- The spine is the image of the segment `[-t, t]` under `y ↦ (0, y)`: it is a 1-D ball. -/
  81theorem spine_eq_image (t : ℕ) :
  82    spine t = (Finset.Icc (-(t : ℤ)) t).image (fun y => ((0 : ℤ), y)) := by
  83  apply Finset.ext
  84  rintro ⟨x, y⟩
  85  simp only [spine, Finset.mem_filter, Finset.mem_image, Finset.mem_Icc,
  86    InterfaceComponentBound.Diamond.mem_ball_iff, Prod.mk.injEq]
  87  constructor
  88  · rintro ⟨hb, rfl⟩
  89    exact ⟨y, by omega, rfl, rfl⟩
  90  · rintro ⟨z, hz, rfl, rfl⟩
  91    exact ⟨by omega, rfl⟩
  92
  93/-- **The 2-D spine is `2t + 1` cells.** The interface of the birth field is confined to this
  94codimension-1 set (a 1-D ball), which is `Θ(t)` while the world is `Θ(t²)`. -/
  95theorem spine_card (t : ℕ) : (spine t).card = 2 * t + 1 := by
  96  rw [spine_eq_image, Finset.card_image_of_injective _ (by
  97    intro u v h; simpa using h)]
  98  rw [Int.card_Icc]
  99  omega
 100
 101/-- **Interface sub-extensivity (2-D).** The recognition-active interface of the birth field is
 102confined to the spine, a set of `2t + 1` cells, so `spine · t ≤ area`: the interface fraction falls
 103as `~ 1/t`. The cost lives on a 1-D curve while the world is the 2-D area `2t² + 2t + 1`. -/
 104theorem interface_subextensive (t : ℕ) (ht : 1 ≤ t) :
 105    (spine t).card = 2 * t + 1 ∧
 106      (spine t).card * t ≤ (InterfaceComponentBound.Diamond.ball t).card := by
 107  refine ⟨spine_card t, ?_⟩
 108  rw [spine_card t, LatticeBallVolume.Diamond.card_ball]
 109  nlinarith [ht]
 110
 111/-- **Birth-field sub-extensivity, both halves (2-D).** The single capstone tying Phase 50 to Phase 51
 112for the forced conjugate-birth field: (1) it is carried as exactly 3 locked domains for every radius
 113(`O(1)` carried state, Phase 50), (2) its entire recognition-active interface is spine-incident, and
 114(3) the spine times the radius fits in the area, so the interface is confined to a codimension-1 set.
 115Both the carried-domain fraction and the interface support vanish as a fraction of the `Θ(t²)` world:
 116the North-Star "carry each region at the coarsest φ-rung its recognition allows" made exact for the
 117birth field, as a THEOREM. -/
 118theorem birth_field_subextensive (t : ℕ) (ht : 1 ≤ t) :
 119    comp (PolarizedBirthDomains.Diamond.Fmono t) = 3
 120    ∧ (∀ p ∈ (edges t).filter (fun q => decide (polarized t q.1 ≠ polarized t q.2)),
 121         p.1.val.1 = 0 ∨ p.2.val.1 = 0)
 122    ∧ (spine t).card * t ≤ (InterfaceComponentBound.Diamond.ball t).card :=
 123  ⟨PolarizedBirthDomains.Diamond.polarized_components_eq_three t ht,
 124   interface_on_spine t, (interface_subextensive t ht).2⟩
 125
 126end Diamond
 127
 128/-! ### The 3-D octahedron: the interface is confined to the spine disk `x = 0`.
 129
 130The dimension D = 3 is the one the forcing chain selects. The spine is now a 2-D diamond. -/
 131
 132namespace Octahedron
 133
 134open InterfaceComponentBound.Octahedron
 135open PolarizedBirthDomains.Octahedron
 136
 137/-- **Every active edge touches the spine disk.** For the polarized octahedron field, any two
 138adjacent cells of different charge have an endpoint on the spine `x = 0`. Same mechanism as the
 139diamond: `sign(x)` flips only across `x = 0`, and a charge-flipping 6-neighbour step crosses it. -/
 140theorem bichromatic_endpoint_on_spine (t : ℕ) (a b : Vtx t)
 141    (hadj : adj a.val b.val) (hc : polarized t a ≠ polarized t b) :
 142    a.val.1 = 0 ∨ b.val.1 = 0 := by
 143  unfold adj at hadj
 144  simp only [polarized] at hc
 145  split_ifs at hc <;> omega
 146
 147/-- **The whole recognition-active interface is on the spine disk.** Every bichromatic edge in the
 148interface list has an endpoint on the spine `x = 0`. -/
 149theorem interface_on_spine (t : ℕ) :
 150    ∀ p ∈ (edges t).filter (fun q => decide (polarized t q.1 ≠ polarized t q.2)),
 151      p.1.val.1 = 0 ∨ p.2.val.1 = 0 := by
 152  intro p hp
 153  rw [List.mem_filter] at hp
 154  obtain ⟨hpe, hpc⟩ := hp
 155  rw [mem_edges] at hpe
 156  rw [decide_eq_true_eq] at hpc
 157  exact bichromatic_endpoint_on_spine t p.1 p.2 hpe hpc
 158
 159/-- The spine of the 3-D octahedron: the cells on the disk `x = 0`. -/
 160def spine (t : ℕ) : Finset (ℤ × ℤ × ℤ) :=
 161  (InterfaceComponentBound.Octahedron.ball t).filter (fun p => p.1 = 0)
 162
 163/-- The spine is the image of the 2-D diamond under `(y, z) ↦ (0, y, z)`: it is a 2-D ball, one
 164dimension below the octahedron. -/
 165theorem spine_eq_image (t : ℕ) :
 166    spine t = (InterfaceComponentBound.Diamond.ball t).image (fun q => ((0 : ℤ), q.1, q.2)) := by
 167  apply Finset.ext
 168  rintro ⟨x, y, z⟩
 169  rw [spine, Finset.mem_filter, InterfaceComponentBound.Octahedron.mem_ball_iff, Finset.mem_image]
 170  constructor
 171  · rintro ⟨hb, hx⟩
 172    subst hx
 173    refine ⟨(y, z), ?_, rfl⟩
 174    rw [InterfaceComponentBound.Diamond.mem_ball_iff]; omega
 175  · rintro ⟨⟨u, w⟩, huw, heq⟩
 176    rw [InterfaceComponentBound.Diamond.mem_ball_iff] at huw
 177    rw [Prod.mk.injEq, Prod.mk.injEq] at heq
 178    obtain ⟨h0, hu, hw⟩ := heq
 179    exact ⟨by omega, by omega⟩
 180
 181/-- **The 3-D spine is `2t² + 2t + 1` cells** (a 2-D diamond, Phase 49 area law). The interface of
 182the birth field is confined to this codimension-1 disk, which is `Θ(t²)` while the world is `Θ(t³)`. -/
 183theorem spine_card (t : ℕ) : (spine t).card = 2 * t ^ 2 + 2 * t + 1 := by
 184  rw [spine_eq_image, Finset.card_image_of_injective _ (by
 185    intro u v h
 186    rw [Prod.mk.injEq, Prod.mk.injEq] at h
 187    exact Prod.ext h.2.1 h.2.2)]
 188  rw [LatticeBallVolume.Diamond.card_ball]
 189
 190/-- **Interface sub-extensivity (3-D).** The recognition-active interface of the birth field is
 191confined to the spine disk, a set of `2t² + 2t + 1` cells, so `spine · t ≤ 3 · volume`: the interface
 192fraction falls as `~ 1/t`. The cost lives on a 2-D surface while the world is the 3-D volume (the
 193centered-octahedral number, `Θ(t³)`), in the dimension D = 3 the forcing chain selects. -/
 194theorem interface_subextensive (t : ℕ) (ht : 1 ≤ t) :
 195    (spine t).card = 2 * t ^ 2 + 2 * t + 1 ∧
 196      (spine t).card * t ≤ 3 * (InterfaceComponentBound.Octahedron.ball t).card := by
 197  refine ⟨spine_card t, ?_⟩
 198  rw [spine_card t, LatticeBallVolume.Octahedron.three_mul_card_ball t]
 199  nlinarith [ht, Nat.zero_le t]
 200
 201/-- **Birth-field sub-extensivity, both halves (3-D).** The capstone tying Phase 50 to Phase 51 in the
 202dimension D = 3 the forcing chain selects: (1) the forced birth field is carried as exactly 3 locked
 203domains for every radius (Phase 50), (2) its entire interface is spine-incident, and (3) the spine
 204disk times the radius fits in `3 ·` the volume, confining the interface to a codimension-1 disk. Both
 205the carried-domain fraction and the interface support vanish as a fraction of the `Θ(t³)` world. -/
 206theorem birth_field_subextensive (t : ℕ) (ht : 1 ≤ t) :
 207    comp (PolarizedBirthDomains.Octahedron.Fmono t) = 3
 208    ∧ (∀ p ∈ (edges t).filter (fun q => decide (polarized t q.1 ≠ polarized t q.2)),
 209         p.1.val.1 = 0 ∨ p.2.val.1 = 0)
 210    ∧ (spine t).card * t ≤ 3 * (InterfaceComponentBound.Octahedron.ball t).card :=
 211  ⟨PolarizedBirthDomains.Octahedron.polarized_components_eq_three t ht,
 212   interface_on_spine t, (interface_subextensive t ht).2⟩
 213
 214end Octahedron
 215
 216end PolarizedBirthInterface
 217end Cosmology
 218end IndisputableMonolith
 219