IndisputableMonolith.Cosmology.PolarizedBirthDomains
IndisputableMonolith/Cosmology/PolarizedBirthDomains.lean · 419 lines · 14 declarations
show as:
view math explainer →
1import Mathlib
2import IndisputableMonolith.Cosmology.InterfaceComponentBound
3import IndisputableMonolith.Cosmology.LatticeBallVolume
4
5/-!
6# The forced birth field is carried at O(1) cost: carried-state sub-extensivity
7
8## Status: THEOREM (0 sorry, 0 axiom beyond Mathlib's standard three).
9
10Phase 48 (`InterfaceComponentBound`) proved the locked-domain count is at most the interface plus
11one on the diamond and octahedron, for any charge field. Phase 49 (`LatticeBallVolume`) proved the
12world's size in closed form (`2t² + 2t + 1` cells in 2D, the centered-octahedral number in 3D). This
13module pins down the carried state for the *forced conjugate-birth (polarized) field* itself: the
14field the 2D/3D shell birth installs, namely `+1` on the fine half `x > 0`, `-1` on the coarse half
15`x < 0`, and `0` on the `x = 0` spine.
16
17For that field the number of locked domains is **at most 3, independent of the radius** (the fine
18half, the coarse half, and the spine are each one 4-connected / 6-connected monochromatic region).
19So a world of `Θ(t^d)` cells is carried as O(1) super-regions: the carried-state fraction
20`components / volume → 0`. This is the sharpest possible sub-extensivity, and it is the North-Star
21claim "carry each region at the coarsest φ-rung its recognition allows" made exact for the birth
22configuration, as a THEOREM (not numeric).
23
24The proof reuses the Phase-48 descent idea, generalized to descent toward a *finite set* of roots:
25`clos_someRoot_of_descent` says that if a height vanishes only on a list of roots and every other
26cell steps down a monochromatic edge, then every cell connects to one of the roots;
27`comp_le_of_roots` turns "every class is represented among `roots`" into `components ≤ roots.length`.
28The polarized height `(|x| - [x ≠ 0]) + |y| (+ |z|)` descends within each charge level to its own
29root (`(1,0)`, `(-1,0)`, `(0,0)` in 2D), so the three roots cover every cell and `components ≤ 3`.
30
31HONEST SCOPE. This is the carried state of the *birth* field. The live engine then diffuses the
32spine by forced resolution, creating additional small interface components; those are bounded above
33by the Phase-48 interface bound, not counted here. The "carried at O(1)" statement is exact for the
34forced conjugate birth, which is the configuration the shell creation installs each cadence cycle.
35-/
36
37namespace IndisputableMonolith
38namespace Cosmology
39namespace PolarizedBirthDomains
40
41open InterfaceComponentBound
42
43variable {V : Type*}
44
45/-! ### General: descent toward a finite set of roots bounds the component count. -/
46
47/-- **Descent toward a finite set of roots.** If a height `h : V → ℕ` vanishes only on the cells in
48`roots`, and every cell of positive height has an edge (in either orientation) to a strictly-lower
49cell, then every cell is connected to some root in `roots`. Strong induction on `h v`, exactly as
50`InterfaceComponentBound.clos_root_of_descent` but with several roots instead of one. -/
51theorem clos_someRoot_of_descent [Finite V] (E : List (V × V)) (h : V → ℕ) (roots : List V)
52 (hzero : ∀ v, h v = 0 → v ∈ roots)
53 (hdesc : ∀ v, h v ≠ 0 → ∃ u, ((v, u) ∈ E ∨ (u, v) ∈ E) ∧ h u < h v) :
54 ∀ v, ∃ r ∈ roots, clos E v r := by
55 have e := clos_equiv E
56 have H : ∀ n, ∀ v, h v = n → ∃ r ∈ roots, clos E v r := by
57 intro n
58 induction n using Nat.strong_induction_on with
59 | _ n ih =>
60 intro v hv
61 rcases Nat.eq_zero_or_pos (h v) with h0 | hpos
62 · exact ⟨v, hzero v h0, e.refl v⟩
63 · have hvne : h v ≠ 0 := by omega
64 obtain ⟨u, hedge, hlt⟩ := hdesc v hvne
65 have hvu : clos E v u := by
66 rcases hedge with he | he
67 · exact Relation.EqvGen.rel v u he
68 · exact e.symm (Relation.EqvGen.rel u v he)
69 obtain ⟨r, hr, hur⟩ := ih (h u) (by omega) u rfl
70 exact ⟨r, hr, e.trans hvu hur⟩
71 intro v
72 exact H (h v) v rfl
73
74/-- **Few roots bound the component count.** If every cell's component is represented by some root in
75`roots`, the number of components is at most `roots.length`. (The quotient map, restricted to the
76roots, hits every class.) -/
77theorem comp_le_of_roots [Finite V] (E : List (V × V)) (roots : List V)
78 (hcov : ∀ v : V, ∃ r ∈ roots, clos E v r) : comp E ≤ roots.length := by
79 classical
80 haveI : Fintype (Quotient (cs E)) := Fintype.ofFinite _
81 have himg : (Finset.univ : Finset (Quotient (cs E)))
82 ⊆ roots.toFinset.image (Quotient.mk (cs E)) := by
83 intro q _
84 obtain ⟨v, rfl⟩ := Quotient.exists_rep q
85 obtain ⟨r, hr, hvr⟩ := hcov v
86 rw [Finset.mem_image]
87 exact ⟨r, List.mem_toFinset.2 hr, Quotient.sound ((clos_equiv E).symm hvr)⟩
88 calc comp E = Fintype.card (Quotient (cs E)) := by
89 rw [comp, Nat.card_eq_fintype_card]
90 _ = (Finset.univ : Finset (Quotient (cs E))).card := by rw [Finset.card_univ]
91 _ ≤ (roots.toFinset.image (Quotient.mk (cs E))).card := Finset.card_le_card himg
92 _ ≤ roots.toFinset.card := Finset.card_image_le
93 _ ≤ roots.length := List.toFinset_card_le roots
94
95/-- **Charge is a monochromatic-closure invariant.** Two cells connected through monochromatic edges
96carry the same charge. Induction on the equivalence-closure derivation: the generating (monochromatic)
97edges are equal-charge by construction; reflexivity, symmetry, and transitivity preserve equality. -/
98theorem clos_mono_charge {β : Type*} [DecidableEq β] (E : List (V × V)) (c : V → β) {u v : V}
99 (h : clos (E.filter (fun p => decide (c p.1 = c p.2))) u v) : c u = c v := by
100 induction h with
101 | rel x y hxy =>
102 simp only [gen, List.mem_filter, decide_eq_true_eq] at hxy
103 exact hxy.2
104 | refl x => rfl
105 | symm x y _ ih => exact ih.symm
106 | trans x y z _ _ ih1 ih2 => exact ih1.trans ih2
107
108/-- **Three distinct charges force at least three components.** If three cells carry pairwise-distinct
109charges, they lie in three distinct monochromatic components (charge is a closure invariant), so the
110induced charge map on the quotient hits three values and the component count is at least 3. -/
111theorem three_le_comp_of_three_charges {β : Type*} [Finite V] [DecidableEq β] (E : List (V × V))
112 (c : V → β) (a b d : V) (hab : c a ≠ c b) (had : c a ≠ c d) (hbd : c b ≠ c d) :
113 3 ≤ comp (E.filter (fun p => decide (c p.1 = c p.2))) := by
114 classical
115 set F := E.filter (fun p => decide (c p.1 = c p.2)) with hF
116 haveI : Fintype (Quotient (cs F)) := Fintype.ofFinite _
117 set q : Quotient (cs F) → β :=
118 Quotient.lift c (fun x y h => clos_mono_charge E c (hF ▸ h)) with hq
119 have hqa : q (Quotient.mk (cs F) a) = c a := rfl
120 have hqb : q (Quotient.mk (cs F) b) = c b := rfl
121 have hqd : q (Quotient.mk (cs F) d) = c d := rfl
122 have hsub : ({c a, c b, c d} : Finset β) ⊆ Finset.image q Finset.univ := by
123 intro w hw
124 rw [Finset.mem_image]
125 simp only [Finset.mem_insert, Finset.mem_singleton] at hw
126 rcases hw with rfl | rfl | rfl
127 · exact ⟨Quotient.mk (cs F) a, Finset.mem_univ _, hqa⟩
128 · exact ⟨Quotient.mk (cs F) b, Finset.mem_univ _, hqb⟩
129 · exact ⟨Quotient.mk (cs F) d, Finset.mem_univ _, hqd⟩
130 have hcard : ({c a, c b, c d} : Finset β).card = 3 := by
131 rw [Finset.card_insert_of_not_mem (by simp [hab, had]),
132 Finset.card_insert_of_not_mem (by simp [hbd]), Finset.card_singleton]
133 calc 3 = ({c a, c b, c d} : Finset β).card := hcard.symm
134 _ ≤ (Finset.image q Finset.univ).card := Finset.card_le_card hsub
135 _ ≤ (Finset.univ : Finset (Quotient (cs F))).card := Finset.card_image_le
136 _ = Fintype.card (Quotient (cs F)) := Finset.card_univ
137 _ = comp F := by rw [comp, Nat.card_eq_fintype_card]
138
139/-! ### The 2-D diamond: the polarized birth field has at most 3 locked domains. -/
140
141namespace Diamond
142
143open InterfaceComponentBound.Diamond
144
145/-- The forced conjugate-birth charge on the diamond: `+1` on the fine half `x > 0`, `-1` on the
146coarse half `x < 0`, `0` on the `x = 0` spine. -/
147def polarized (t : ℕ) (v : Vtx t) : ℤ :=
148 if 0 < v.val.1 then 1 else if v.val.1 < 0 then -1 else 0
149
150/-- The monochromatic edge list of the polarized diamond: adjacent same-charge cell pairs. -/
151noncomputable def Fmono (t : ℕ) : List (Vtx t × Vtx t) :=
152 (edges t).filter (fun p => decide (polarized t p.1 = polarized t p.2))
153
154/-- The descent height toward the three roots: `(|x| - [x ≠ 0]) + |y|`, which vanishes exactly at
155`(1,0)`, `(-1,0)`, `(0,0)` and decreases along a same-charge step toward the relevant root. -/
156def hgt (t : ℕ) (v : Vtx t) : ℕ :=
157 (v.val.1.natAbs - (if v.val.1 = 0 then 0 else 1)) + v.val.2.natAbs
158
159/-- A monochromatic edge between two diamond cells: adjacency plus equal polarized charge. -/
160theorem mem_Fmono (t : ℕ) (a b : Vtx t)
161 (hadj : adj a.val b.val) (hc : polarized t a = polarized t b) : (a, b) ∈ Fmono t := by
162 rw [Fmono, List.mem_filter]
163 exact ⟨(mem_edges t a b).2 hadj, by simpa using hc⟩
164
165/-- The three roots of the polarized diamond (need `t ≥ 1` for the `±1` halves to be present). -/
166def roots (t : ℕ) (ht : 1 ≤ t) : List (Vtx t) :=
167 [ ⟨(1, 0), by rw [mem_ball_iff]; omega⟩
168 , ⟨(-1, 0), by rw [mem_ball_iff]; omega⟩
169 , ⟨(0, 0), by rw [mem_ball_iff]; omega⟩ ]
170
171/-- A zero-height cell is one of the three roots. -/
172theorem hzero (t : ℕ) (ht : 1 ≤ t) :
173 ∀ v : Vtx t, hgt t v = 0 → v ∈ roots t ht := by
174 rintro ⟨⟨x, y⟩, hmem⟩ h0
175 simp only [hgt] at h0
176 rw [roots]
177 by_cases hx : x = 0
178 · subst hx
179 have hy : y = 0 := by simp only [Int.natAbs_zero] at h0; omega
180 subst hy
181 simp [List.mem_cons]
182 · have hx1 : x.natAbs = 1 := by
183 rw [if_neg hx] at h0; omega
184 have hy : y = 0 := by
185 rw [if_neg hx] at h0; omega
186 subst hy
187 rcases Int.natAbs_eq_iff.1 hx1 with hxp | hxn
188 · subst hxp; simp [List.mem_cons]
189 · have : x = -1 := by simpa using hxn
190 subst this; simp [List.mem_cons]
191
192/-- From any off-root diamond cell there is a monochromatic edge to a strictly-lower cell: move the
193non-zero coordinate toward the root of the cell's own charge level. -/
194theorem hdesc (t : ℕ) :
195 ∀ v : Vtx t, hgt t v ≠ 0 →
196 ∃ u, ((v, u) ∈ Fmono t ∨ (u, v) ∈ Fmono t) ∧ hgt t u < hgt t v := by
197 rintro ⟨⟨x, y⟩, hmem⟩ hv
198 rw [mem_ball_iff] at hmem
199 simp only [hgt] at hv ⊢
200 rcases lt_trichotomy y 0 with hy | hy | hy
201 · -- y < 0: step to (x, y+1), same x so same charge
202 refine ⟨⟨(x, y + 1), by rw [mem_ball_iff]; omega⟩, Or.inl (mem_Fmono t _ _ ?_ ?_), ?_⟩
203 · unfold adj; dsimp only; omega
204 · simp only [polarized]
205 · dsimp only; split_ifs <;> omega
206 · -- y = 0: step the x-coordinate toward ±1 (only possible when |x| ≥ 2)
207 subst hy
208 rcases lt_trichotomy x 0 with hx | hx | hx
209 · -- x < 0; root is (-1,0); descend needs x ≤ -2
210 have hx2 : x ≤ -2 := by
211 rcases lt_or_ge x (-1) with h | h
212 · omega
213 · exfalso; have : x = -1 := by omega
214 subst this; simp at hv
215 refine ⟨⟨(x + 1, 0), by rw [mem_ball_iff]; omega⟩, Or.inl (mem_Fmono t _ _ ?_ ?_), ?_⟩
216 · unfold adj; dsimp only; omega
217 · simp only [polarized]; dsimp only; split_ifs <;> omega
218 · dsimp only; split_ifs <;> omega
219 · exfalso; subst hx; simp at hv
220 · -- x > 0; root is (1,0); descend needs x ≥ 2
221 have hx2 : 2 ≤ x := by
222 rcases lt_or_ge 1 x with h | h
223 · omega
224 · exfalso; have : x = 1 := by omega
225 subst this; simp at hv
226 refine ⟨⟨(x - 1, 0), by rw [mem_ball_iff]; omega⟩, Or.inl (mem_Fmono t _ _ ?_ ?_), ?_⟩
227 · unfold adj; dsimp only; omega
228 · simp only [polarized]; dsimp only; split_ifs <;> omega
229 · dsimp only; split_ifs <;> omega
230 · -- y > 0: step to (x, y-1), same x so same charge
231 refine ⟨⟨(x, y - 1), by rw [mem_ball_iff]; omega⟩, Or.inl (mem_Fmono t _ _ ?_ ?_), ?_⟩
232 · unfold adj; dsimp only; omega
233 · simp only [polarized]
234 · dsimp only; split_ifs <;> omega
235
236/-- **The polarized birth field is carried as at most 3 super-regions, every radius.** For the forced
237conjugate-birth charge on the diamond of radius `t ≥ 1`, the number of locked (monochromatic
2384-connected) domains is at most 3: the fine half, the coarse half, and the spine. THEOREM for all
239radii. -/
240theorem polarized_components_le_three (t : ℕ) (ht : 1 ≤ t) :
241 comp (Fmono t) ≤ 3 := by
242 have hcov := clos_someRoot_of_descent (Fmono t) (hgt t) (roots t ht) (hzero t ht)
243 (by
244 intro v hv
245 obtain ⟨u, hedge, hlt⟩ := hdesc t v hv
246 exact ⟨u, hedge, hlt⟩)
247 have := comp_le_of_roots (Fmono t) (roots t ht) hcov
248 simpa [roots] using this
249
250/-- **The polarized birth field has exactly 3 locked domains, every radius (2-D).** The upper bound
251`≤ 3` (descent toward the three roots) meets the lower bound `≥ 3` (the three roots carry the three
252distinct charges `+1`, `-1`, `0`, and charge is a closure invariant). So the carried state is exactly
2533 for all `t ≥ 1`: the fine half, the coarse half, and the spine. -/
254theorem polarized_components_eq_three (t : ℕ) (ht : 1 ≤ t) : comp (Fmono t) = 3 := by
255 refine le_antisymm (polarized_components_le_three t ht) ?_
256 exact three_le_comp_of_three_charges (edges t) (polarized t)
257 ⟨(1, 0), by rw [mem_ball_iff]; omega⟩
258 ⟨(-1, 0), by rw [mem_ball_iff]; omega⟩
259 ⟨(0, 0), by rw [mem_ball_iff]; omega⟩
260 (by simp only [polarized]; dsimp only; decide)
261 (by simp only [polarized]; dsimp only; decide)
262 (by simp only [polarized]; dsimp only; decide)
263
264/-- **Carried-state sub-extensivity for the birth field (2-D).** The polarized diamond fills
265`2t² + 2t + 1` cells (Phase 49) but is carried as exactly 3 super-regions, so the carried state times
266the radius is at most the area for every `t ≥ 1`: `3 t ≤ card (ball t)`, the carried cost is `O(1)`
267while the world is `Θ(t²)`. -/
268theorem polarized_carried_subextensive (t : ℕ) (ht : 1 ≤ t) :
269 comp (Fmono t) = 3 ∧ 3 * t ≤ (InterfaceComponentBound.Diamond.ball t).card := by
270 refine ⟨polarized_components_eq_three t ht, ?_⟩
271 rw [LatticeBallVolume.Diamond.card_ball]
272 nlinarith [ht]
273
274end Diamond
275
276/-! ### The 3-D octahedron: the polarized birth field has at most 3 locked domains.
277
278Identical structure to the diamond, with the spine now a 2-D disk (`x = 0`) and the two halves 3-D.
279The dimension D = 3 is the one the forcing chain selects. -/
280
281namespace Octahedron
282
283open InterfaceComponentBound.Octahedron
284
285/-- The forced conjugate-birth charge on the octahedron: `+1` on the fine half `x > 0`, `-1` on the
286coarse half `x < 0`, `0` on the `x = 0` spine disk. -/
287def polarized (t : ℕ) (v : Vtx t) : ℤ :=
288 if 0 < v.val.1 then 1 else if v.val.1 < 0 then -1 else 0
289
290/-- The monochromatic edge list of the polarized octahedron. -/
291noncomputable def Fmono (t : ℕ) : List (Vtx t × Vtx t) :=
292 (edges t).filter (fun p => decide (polarized t p.1 = polarized t p.2))
293
294/-- The descent height toward the three roots: `(|x| - [x ≠ 0]) + |y| + |z|`. -/
295def hgt (t : ℕ) (v : Vtx t) : ℕ :=
296 (v.val.1.natAbs - (if v.val.1 = 0 then 0 else 1)) + v.val.2.1.natAbs + v.val.2.2.natAbs
297
298theorem mem_Fmono (t : ℕ) (a b : Vtx t)
299 (hadj : adj a.val b.val) (hc : polarized t a = polarized t b) : (a, b) ∈ Fmono t := by
300 rw [Fmono, List.mem_filter]
301 exact ⟨(mem_edges t a b).2 hadj, by simpa using hc⟩
302
303/-- The three roots of the polarized octahedron (need `t ≥ 1`). -/
304def roots (t : ℕ) (ht : 1 ≤ t) : List (Vtx t) :=
305 [ ⟨(1, 0, 0), by rw [mem_ball_iff]; omega⟩
306 , ⟨(-1, 0, 0), by rw [mem_ball_iff]; omega⟩
307 , ⟨(0, 0, 0), by rw [mem_ball_iff]; omega⟩ ]
308
309theorem hzero (t : ℕ) (ht : 1 ≤ t) :
310 ∀ v : Vtx t, hgt t v = 0 → v ∈ roots t ht := by
311 rintro ⟨⟨x, y, z⟩, hmem⟩ h0
312 simp only [hgt] at h0
313 rw [roots]
314 by_cases hx : x = 0
315 · subst hx
316 have hy : y = 0 := by simp only [Int.natAbs_zero] at h0; omega
317 have hz : z = 0 := by simp only [Int.natAbs_zero] at h0; omega
318 subst hy; subst hz
319 simp [List.mem_cons]
320 · have hx1 : x.natAbs = 1 := by rw [if_neg hx] at h0; omega
321 have hy : y = 0 := by rw [if_neg hx] at h0; omega
322 have hz : z = 0 := by rw [if_neg hx] at h0; omega
323 subst hy; subst hz
324 rcases Int.natAbs_eq_iff.1 hx1 with hxp | hxn
325 · subst hxp; simp [List.mem_cons]
326 · have : x = -1 := by simpa using hxn
327 subst this; simp [List.mem_cons]
328
329theorem hdesc (t : ℕ) :
330 ∀ v : Vtx t, hgt t v ≠ 0 →
331 ∃ u, ((v, u) ∈ Fmono t ∨ (u, v) ∈ Fmono t) ∧ hgt t u < hgt t v := by
332 rintro ⟨⟨x, y, z⟩, hmem⟩ hv
333 rw [mem_ball_iff] at hmem
334 simp only [hgt] at hv ⊢
335 rcases lt_trichotomy z 0 with hz | hz | hz
336 · refine ⟨⟨(x, y, z + 1), by rw [mem_ball_iff]; omega⟩, Or.inl (mem_Fmono t _ _ ?_ ?_), ?_⟩
337 · unfold adj; dsimp only; omega
338 · simp only [polarized]
339 · dsimp only; split_ifs <;> omega
340 · subst hz
341 rcases lt_trichotomy y 0 with hy | hy | hy
342 · refine ⟨⟨(x, y + 1, 0), by rw [mem_ball_iff]; omega⟩, Or.inl (mem_Fmono t _ _ ?_ ?_), ?_⟩
343 · unfold adj; dsimp only; omega
344 · simp only [polarized]
345 · dsimp only; split_ifs <;> omega
346 · subst hy
347 rcases lt_trichotomy x 0 with hx | hx | hx
348 · have hx2 : x ≤ -2 := by
349 rcases lt_or_ge x (-1) with h | h
350 · omega
351 · exfalso; have : x = -1 := by omega
352 subst this; simp at hv
353 refine ⟨⟨(x + 1, 0, 0), by rw [mem_ball_iff]; omega⟩, Or.inl (mem_Fmono t _ _ ?_ ?_), ?_⟩
354 · unfold adj; dsimp only; omega
355 · simp only [polarized]; dsimp only; split_ifs <;> omega
356 · dsimp only; split_ifs <;> omega
357 · exfalso; subst hx; simp at hv
358 · have hx2 : 2 ≤ x := by
359 rcases lt_or_ge 1 x with h | h
360 · omega
361 · exfalso; have : x = 1 := by omega
362 subst this; simp at hv
363 refine ⟨⟨(x - 1, 0, 0), by rw [mem_ball_iff]; omega⟩, Or.inl (mem_Fmono t _ _ ?_ ?_), ?_⟩
364 · unfold adj; dsimp only; omega
365 · simp only [polarized]; dsimp only; split_ifs <;> omega
366 · dsimp only; split_ifs <;> omega
367 · refine ⟨⟨(x, y - 1, 0), by rw [mem_ball_iff]; omega⟩, Or.inl (mem_Fmono t _ _ ?_ ?_), ?_⟩
368 · unfold adj; dsimp only; omega
369 · simp only [polarized]
370 · dsimp only; split_ifs <;> omega
371 · refine ⟨⟨(x, y, z - 1), by rw [mem_ball_iff]; omega⟩, Or.inl (mem_Fmono t _ _ ?_ ?_), ?_⟩
372 · unfold adj; dsimp only; omega
373 · simp only [polarized]
374 · dsimp only; split_ifs <;> omega
375
376/-- **The polarized birth field is carried as at most 3 super-regions, every radius (3-D).** For the
377forced conjugate-birth charge on the octahedron of radius `t ≥ 1`, the number of locked
378(monochromatic 6-connected) domains is at most 3: the fine half, the coarse half, and the spine disk.
379THEOREM for all radii, in the dimension D = 3 the forcing chain selects. -/
380theorem polarized_components_le_three (t : ℕ) (ht : 1 ≤ t) :
381 comp (Fmono t) ≤ 3 := by
382 have hcov := clos_someRoot_of_descent (Fmono t) (hgt t) (roots t ht) (hzero t ht)
383 (by
384 intro v hv
385 obtain ⟨u, hedge, hlt⟩ := hdesc t v hv
386 exact ⟨u, hedge, hlt⟩)
387 have := comp_le_of_roots (Fmono t) (roots t ht) hcov
388 simpa [roots] using this
389
390/-- **The polarized birth field has exactly 3 locked domains, every radius (3-D).** Upper bound `≤ 3`
391(descent toward the three roots) meets lower bound `≥ 3` (the three roots carry charges `+1`, `-1`,
392`0`). The carried state is exactly 3 for all `t ≥ 1`, in the dimension D = 3 the forcing chain
393selects: the fine half, the coarse half, and the spine disk. -/
394theorem polarized_components_eq_three (t : ℕ) (ht : 1 ≤ t) : comp (Fmono t) = 3 := by
395 refine le_antisymm (polarized_components_le_three t ht) ?_
396 exact three_le_comp_of_three_charges (edges t) (polarized t)
397 ⟨(1, 0, 0), by rw [mem_ball_iff]; omega⟩
398 ⟨(-1, 0, 0), by rw [mem_ball_iff]; omega⟩
399 ⟨(0, 0, 0), by rw [mem_ball_iff]; omega⟩
400 (by simp only [polarized]; dsimp only; decide)
401 (by simp only [polarized]; dsimp only; decide)
402 (by simp only [polarized]; dsimp only; decide)
403
404/-- **Carried-state sub-extensivity for the birth field (3-D).** The polarized octahedron fills the
405centered-octahedral number of cells (Phase 49: `3 · card = 4t³ + 6t² + 8t + 3`, i.e. `Θ(t³)`) but is
406carried as exactly 3 super-regions, so `3 t² ≤ card (ball t)` for every `t`: the carried cost is
407`O(1)` while the world is `Θ(t³)`. -/
408theorem polarized_carried_subextensive (t : ℕ) (ht : 1 ≤ t) :
409 comp (Fmono t) = 3 ∧ 3 * t ^ 2 ≤ (InterfaceComponentBound.Octahedron.ball t).card := by
410 refine ⟨polarized_components_eq_three t ht, ?_⟩
411 have h := LatticeBallVolume.Octahedron.three_mul_card_ball t
412 nlinarith [h, Nat.zero_le t]
413
414end Octahedron
415
416end PolarizedBirthDomains
417end Cosmology
418end IndisputableMonolith
419