IndisputableMonolith.Cosmology.LatticeBallEdges
IndisputableMonolith/Cosmology/LatticeBallEdges.lean · 613 lines · 22 declarations
show as:
view math explainer →
1import Mathlib
2import IndisputableMonolith.Cosmology.InterfaceComponentBound
3import IndisputableMonolith.Cosmology.LatticeBallVolume
4import IndisputableMonolith.Cosmology.PolarizedBirthDomains
5import IndisputableMonolith.Cosmology.PolarizedBirthInterface
6import IndisputableMonolith.Cosmology.PolarizedBirthInterfaceCount
7
8/-!
9# Total adjacency count of the coarsening world, and the exact carried-versus-interface split
10
11`PolarizedBirthInterfaceCount` counts the *interface* exactly: the bichromatic (forced-distinction)
12edges of the polarized birth field number `8t - 4` in 2D and `8t² - 8t + 4` in 3D. That is the cost
13the engine pays. This module counts the *other* side of the ledger: the total number of adjacencies,
14and hence the *monochromatic* (carried-internal) edges the engine carries for free.
15
16The total ordered adjacency count of the L1 ball is a closed form, a THEOREM over `ℕ` with no `sorry`
17and no new axioms:
18
19* `Diamond.total_edge_card t = 8 t²` (the 2D diamond, 4-neighbour adjacency).
20* `Octahedron.three_mul_total_edge_card t : 3 · card = 24 t³ + 12 t`, i.e. `8 t³ + 4 t` (the 3D
21 octahedron, 6-neighbour adjacency).
22
23The proof is a clean "volume minus boundary" count. The ordered edges biject onto pairs `(cell, dir)`
24with `cell` and `cell + dir` both in the ball, summed over the unit directions. For a fixed direction
25`d`, the cells whose `d`-neighbour leaves the ball form a codimension-1 boundary: in 2D one cell per
26row (`2t + 1` of them, the silhouette `Icc (-t) t`), in 3D one cell per `(y,z)` of the transverse
27diamond (`card (Diamond.ball t) = 2t² + 2t + 1` of them). So each direction contributes
28`card (ball) - card (boundary)` edges, and summing over the `2d` directions gives the total. Both
29counts reuse the Phase-49 area/volume laws (`LatticeBallVolume`) for the bulk and the boundary.
30
31The payoff (in `PolarizedBirthInterface`, `carried_edge_card`): every adjacency is either a carried
32monochromatic edge or a forced bichromatic interface edge, so the monochromatic carried edges number
33exactly `total - interface = 8t² - (8t - 4) = 8t² - 8t + 4` in 2D. The carried fraction
34`mono / total = 1 - (8t - 4)/(8t²) → 1`: almost every adjacency is carried for free, and the engine
35pays only the vanishing interface fraction. This is the exact, closed-form statement of "carry the
36bulk coarse, pay only for the interface" that the coarsening north star asserts.
37-/
38
39namespace IndisputableMonolith
40namespace Cosmology
41namespace LatticeBallEdges
42
43open Finset
44open scoped BigOperators
45
46namespace Diamond
47
48open InterfaceComponentBound.Diamond
49
50/-- The four unit directions of the 4-neighbour lattice. -/
51def dirs : Finset (ℤ × ℤ) := {(1, 0), (-1, 0), (0, 1), (0, -1)}
52
53theorem dirs_card : dirs.card = 4 := by decide
54
55/-- The total ordered adjacency set of the diamond, as a `Finset` of vertex pairs. This is exactly
56the `edges` set of `InterfaceComponentBound`, whose `toList` is the engine's edge list. -/
57noncomputable def E (t : ℕ) : Finset (Vtx t × Vtx t) :=
58 Finset.univ.filter (fun p => adj p.1.val p.2.val)
59
60/-- The `(cell, direction)` index set: a cell of the ball together with a unit direction whose step
61stays in the ball. The ordered edges biject onto this set. -/
62def Dset (t : ℕ) : Finset ((ℤ × ℤ) × (ℤ × ℤ)) :=
63 (ball t ×ˢ dirs).filter (fun p => (p.1.1 + p.2.1, p.1.2 + p.2.2) ∈ ball t)
64
65/-- **Right boundary count.** The cells whose `+x` neighbour leaves the ball are exactly the
66rightmost cell of each row, one per `y ∈ [-t, t]`, so there are `2t + 1` of them. -/
67theorem boundary_xpos (t : ℕ) :
68 ((ball t).filter (fun p => (p.1 + 1, p.2) ∉ ball t)).card = 2 * t + 1 := by
69 rw [show 2 * t + 1 = (Finset.Icc (-(t : ℤ)) t).card from by rw [Int.card_Icc]; omega]
70 refine Finset.card_bij' (fun p _ => p.2) (fun y _ => (((t : ℤ) - y.natAbs), y)) ?_ ?_ ?_ ?_
71 · rintro ⟨x, y⟩ hp
72 simp only [Finset.mem_filter, mem_ball_iff] at hp
73 simp only [Finset.mem_Icc]; omega
74 · intro y hy
75 simp only [Finset.mem_Icc] at hy
76 simp only [Finset.mem_filter, mem_ball_iff]
77 refine ⟨by omega, by omega⟩
78 · rintro ⟨x, y⟩ hp
79 simp only [Finset.mem_filter, mem_ball_iff] at hp
80 simp only [Prod.mk.injEq, and_true, true_and]
81 omega
82 · intro y _; rfl
83
84/-- **Left boundary count.** Symmetric to `boundary_xpos`: `2t + 1` leftmost cells. -/
85theorem boundary_xneg (t : ℕ) :
86 ((ball t).filter (fun p => (p.1 + -1, p.2) ∉ ball t)).card = 2 * t + 1 := by
87 rw [show 2 * t + 1 = (Finset.Icc (-(t : ℤ)) t).card from by rw [Int.card_Icc]; omega]
88 refine Finset.card_bij' (fun p _ => p.2) (fun y _ => ((-((t : ℤ) - y.natAbs)), y)) ?_ ?_ ?_ ?_
89 · rintro ⟨x, y⟩ hp
90 simp only [Finset.mem_filter, mem_ball_iff] at hp
91 simp only [Finset.mem_Icc]; omega
92 · intro y hy
93 simp only [Finset.mem_Icc] at hy
94 simp only [Finset.mem_filter, mem_ball_iff]
95 refine ⟨by omega, by omega⟩
96 · rintro ⟨x, y⟩ hp
97 simp only [Finset.mem_filter, mem_ball_iff] at hp
98 simp only [Prod.mk.injEq, and_true, true_and]
99 omega
100 · intro y _; rfl
101
102/-- **Top boundary count.** The cells whose `+y` neighbour leaves the ball: one per column. -/
103theorem boundary_ypos (t : ℕ) :
104 ((ball t).filter (fun p => (p.1, p.2 + 1) ∉ ball t)).card = 2 * t + 1 := by
105 rw [show 2 * t + 1 = (Finset.Icc (-(t : ℤ)) t).card from by rw [Int.card_Icc]; omega]
106 refine Finset.card_bij' (fun p _ => p.1) (fun x _ => (x, ((t : ℤ) - x.natAbs))) ?_ ?_ ?_ ?_
107 · rintro ⟨x, y⟩ hp
108 simp only [Finset.mem_filter, mem_ball_iff] at hp
109 simp only [Finset.mem_Icc]; omega
110 · intro x hx
111 simp only [Finset.mem_Icc] at hx
112 simp only [Finset.mem_filter, mem_ball_iff]
113 refine ⟨by omega, by omega⟩
114 · rintro ⟨x, y⟩ hp
115 simp only [Finset.mem_filter, mem_ball_iff] at hp
116 simp only [Prod.mk.injEq, and_true, true_and]
117 omega
118 · intro x _; rfl
119
120/-- **Bottom boundary count.** The cells whose `-y` neighbour leaves the ball: one per column. -/
121theorem boundary_yneg (t : ℕ) :
122 ((ball t).filter (fun p => (p.1, p.2 + -1) ∉ ball t)).card = 2 * t + 1 := by
123 rw [show 2 * t + 1 = (Finset.Icc (-(t : ℤ)) t).card from by rw [Int.card_Icc]; omega]
124 refine Finset.card_bij' (fun p _ => p.1) (fun x _ => (x, (-((t : ℤ) - x.natAbs)))) ?_ ?_ ?_ ?_
125 · rintro ⟨x, y⟩ hp
126 simp only [Finset.mem_filter, mem_ball_iff] at hp
127 simp only [Finset.mem_Icc]; omega
128 · intro x hx
129 simp only [Finset.mem_Icc] at hx
130 simp only [Finset.mem_filter, mem_ball_iff]
131 refine ⟨by omega, by omega⟩
132 · rintro ⟨x, y⟩ hp
133 simp only [Finset.mem_filter, mem_ball_iff] at hp
134 simp only [Prod.mk.injEq, and_true, true_and]
135 omega
136 · intro x _; rfl
137
138/-- For each unit direction, the cells whose `d`-neighbour stays in the ball number `2t²`: the bulk
139`card (ball) = 2t² + 2t + 1` minus the `2t + 1` boundary cells. -/
140theorem step_card (t : ℕ) (d : ℤ × ℤ) (hd : d ∈ dirs) :
141 ((ball t).filter (fun p => (p.1 + d.1, p.2 + d.2) ∈ ball t)).card = 2 * t ^ 2 := by
142 have hvol : (ball t).card = 2 * t ^ 2 + 2 * t + 1 := LatticeBallVolume.Diamond.card_ball t
143 simp only [dirs, Finset.mem_insert, Finset.mem_singleton] at hd
144 rcases hd with rfl | rfl | rfl | rfl
145 · have hbd := boundary_xpos t
146 have hsplit := Finset.filter_card_add_filter_neg_card_eq_card
147 (s := ball t) (p := fun p : ℤ × ℤ => (p.1 + 1, p.2) ∈ ball t)
148 simp only [add_zero] at *
149 omega
150 · have hbd := boundary_xneg t
151 have hsplit := Finset.filter_card_add_filter_neg_card_eq_card
152 (s := ball t) (p := fun p : ℤ × ℤ => (p.1 + -1, p.2) ∈ ball t)
153 simp only [add_zero] at *
154 omega
155 · have hbd := boundary_ypos t
156 have hsplit := Finset.filter_card_add_filter_neg_card_eq_card
157 (s := ball t) (p := fun p : ℤ × ℤ => (p.1, p.2 + 1) ∈ ball t)
158 simp only [add_zero] at *
159 omega
160 · have hbd := boundary_yneg t
161 have hsplit := Finset.filter_card_add_filter_neg_card_eq_card
162 (s := ball t) (p := fun p : ℤ × ℤ => (p.1, p.2 + -1) ∈ ball t)
163 simp only [add_zero] at *
164 omega
165
166/-- The `(cell, direction)` index set has `8t²` elements: four directions, each contributing `2t²`
167in-ball steps. -/
168theorem Dset_card (t : ℕ) : (Dset t).card = 8 * t ^ 2 := by
169 have hsum : (Dset t).card
170 = ∑ d ∈ dirs, ((ball t).filter (fun p => (p.1 + d.1, p.2 + d.2) ∈ ball t)).card := by
171 rw [Dset, Finset.card_filter, Finset.sum_product, Finset.sum_comm]
172 refine Finset.sum_congr rfl (fun d _ => ?_)
173 rw [Finset.card_filter]
174 rw [hsum]
175 rw [Finset.sum_congr rfl (fun d hd => step_card t d hd)]
176 rw [Finset.sum_const, dirs_card]
177 ring
178
179/-- **The 2-D total adjacency law.** The diamond `|x| + |y| ≤ t` has exactly `8t²` ordered
1804-neighbour adjacencies (each undirected edge counted in both orientations). THEOREM over `ℕ`. The
181ordered edges biject onto `(cell, direction)` steps that stay in the ball. -/
182theorem total_edge_card (t : ℕ) : (E t).card = 8 * t ^ 2 := by
183 rw [← Dset_card t]
184 refine Finset.card_bij'
185 (fun p _ => (p.1.val, (p.2.val.1 - p.1.val.1, p.2.val.2 - p.1.val.2)))
186 (fun cd hcd => (⟨cd.1, ?_⟩, ⟨(cd.1.1 + cd.2.1, cd.1.2 + cd.2.2), ?_⟩)) ?_ ?_ ?_ ?_
187 · -- cd.1 ∈ ball (for the inverse's first vertex)
188 simp only [Dset, Finset.mem_filter, Finset.mem_product] at hcd
189 exact hcd.1.1
190 · -- cd.1 + cd.2 ∈ ball (for the inverse's second vertex)
191 simp only [Dset, Finset.mem_filter, Finset.mem_product] at hcd
192 exact hcd.2
193 · -- hi : forward maps E into Dset
194 rintro ⟨a, b⟩ hp
195 simp only [E, Finset.mem_filter, Finset.mem_univ, true_and] at hp
196 simp only [Dset, Finset.mem_filter, Finset.mem_product]
197 refine ⟨⟨a.property, ?_⟩, ?_⟩
198 · -- the difference is a unit direction
199 unfold adj at hp
200 simp only [dirs, Finset.mem_insert, Finset.mem_singleton, Prod.mk.injEq]
201 omega
202 · -- stepping by the difference lands on b ∈ ball
203 have hb : (a.val.1 + (b.val.1 - a.val.1), a.val.2 + (b.val.2 - a.val.2)) = b.val := by
204 rw [Prod.ext_iff]; refine ⟨?_, ?_⟩ <;> · dsimp only; ring
205 rw [hb]; exact b.property
206 · -- hj : inverse maps Dset into E
207 rintro ⟨c, d⟩ hcd
208 simp only [Dset, Finset.mem_filter, Finset.mem_product] at hcd
209 simp only [E, Finset.mem_filter, Finset.mem_univ, true_and]
210 unfold adj
211 have hdir : d ∈ dirs := hcd.1.2
212 simp only [dirs, Finset.mem_insert, Finset.mem_singleton] at hdir
213 rcases hdir with rfl | rfl | rfl | rfl <;> · dsimp only; omega
214 · -- left inverse
215 rintro ⟨a, b⟩ hp
216 dsimp only
217 rw [Prod.ext_iff]
218 refine ⟨?_, ?_⟩
219 · apply Subtype.ext; rfl
220 · apply Subtype.ext
221 rw [Prod.ext_iff]
222 refine ⟨?_, ?_⟩ <;> · dsimp only; ring
223 · -- right inverse
224 rintro ⟨c, d⟩ hcd
225 dsimp only
226 rw [Prod.ext_iff]
227 refine ⟨rfl, ?_⟩
228 rw [Prod.ext_iff]
229 refine ⟨?_, ?_⟩ <;> · dsimp only; ring
230
231/-- The engine's edge list has `8t²` entries: the same total adjacency count, as a list length. -/
232theorem edges_length (t : ℕ) : (InterfaceComponentBound.Diamond.edges t).length = 8 * t ^ 2 := by
233 rw [InterfaceComponentBound.Diamond.edges, Finset.length_toList]
234 exact total_edge_card t
235
236open PolarizedBirthDomains.Diamond (polarized)
237open PolarizedBirthInterface.Diamond (B)
238
239/-- The carried (monochromatic) adjacencies of the polarized birth field: the equal-charge edges,
240internal to a locked domain, which the engine carries coarse for free. -/
241noncomputable def carried (t : ℕ) : Finset (Vtx t × Vtx t) :=
242 (E t).filter (fun p => polarized t p.1 = polarized t p.2)
243
244/-- **The exact carried (monochromatic) edge count.** Every adjacency is either a forced bichromatic
245interface edge (`B`, counted as `8t - 4`) or a carried monochromatic edge. Since the total is `8t²`,
246the carried edges number exactly `8t² - (8t - 4) = 8t² - 8t + 4`: the bulk the engine carries for
247free, complementing the `8t - 4` it must post. THEOREM over `ℕ` (`t ≥ 1`). -/
248theorem carried_edge_card (t : ℕ) (ht : 1 ≤ t) :
249 (carried t).card = 8 * t ^ 2 - 8 * t + 4 := by
250 have hsplit := Finset.filter_card_add_filter_neg_card_eq_card
251 (s := E t) (p := fun p : Vtx t × Vtx t => polarized t p.1 ≠ polarized t p.2)
252 have hBeq : (E t).filter (fun p => polarized t p.1 ≠ polarized t p.2) = B t := by
253 rw [E, B, Finset.filter_filter]
254 have hMeq : (E t).filter (fun p => ¬ (polarized t p.1 ≠ polarized t p.2)) = carried t := by
255 rw [carried]
256 apply Finset.filter_congr
257 intro p _
258 simp
259 rw [hBeq, hMeq] at hsplit
260 have hB : (B t).card = 8 * t - 4 := PolarizedBirthInterface.Diamond.interface_card_eq t ht
261 have hE : (E t).card = 8 * t ^ 2 := total_edge_card t
262 rw [hB, hE] at hsplit
263 have hge : 8 * t ≤ 8 * t ^ 2 := by nlinarith [ht]
264 omega
265
266/-- **Discrete isoperimetric / surface law.** The forced interface satisfies
267`(interface)² ≤ 8 · (total adjacency)`, so the interface grows only as the *square root* of the bulk:
268it is a codimension-1 surface, not a bulk quantity. Sharp form of "the cost is sub-extensive,
269localized to a perimeter." THEOREM over `ℕ`. -/
270theorem interface_sq_le_total (t : ℕ) (ht : 1 ≤ t) :
271 (B t).card ^ 2 ≤ 8 * (E t).card := by
272 rw [PolarizedBirthInterface.Diamond.interface_card_eq t ht, total_edge_card t]
273 obtain ⟨n, rfl⟩ : ∃ n, t = n + 1 := ⟨t - 1, by omega⟩
274 have hL : 8 * (n + 1) - 4 = 8 * n + 4 := by omega
275 rw [hL]
276 nlinarith [Nat.zero_le n]
277
278/-- **Carried dominates interface.** For a world of radius `t ≥ 1`, the engine carries at least as
279many edges coarse as it posts (`8t² - 8t + 4 ≥ 8t - 4`, with equality only at `t = 1`): the carried
280bulk overtakes the interface as soon as the world is larger than a single shell. -/
281theorem carried_ge_interface (t : ℕ) (ht : 1 ≤ t) :
282 (B t).card ≤ (carried t).card := by
283 rw [PolarizedBirthInterface.Diamond.interface_card_eq t ht, carried_edge_card t ht]
284 obtain ⟨n, rfl⟩ : ∃ n, t = n + 1 := ⟨t - 1, by omega⟩
285 have hsq : (n + 1) ^ 2 = n ^ 2 + 2 * n + 1 := by ring
286 rw [hsq]
287 omega
288
289end Diamond
290
291namespace Octahedron
292
293open InterfaceComponentBound.Octahedron
294
295/-- The six unit directions of the 6-neighbour lattice. -/
296def dirs : Finset (ℤ × ℤ × ℤ) :=
297 {(1, 0, 0), (-1, 0, 0), (0, 1, 0), (0, -1, 0), (0, 0, 1), (0, 0, -1)}
298
299theorem dirs_card : dirs.card = 6 := by decide
300
301/-- The total ordered adjacency set of the octahedron, as a `Finset` of vertex pairs. -/
302noncomputable def E (t : ℕ) : Finset (Vtx t × Vtx t) :=
303 Finset.univ.filter (fun p => adj p.1.val p.2.val)
304
305/-- The `(cell, direction)` index set: a cell of the ball together with a unit direction whose step
306stays in the ball. The ordered edges biject onto this set. -/
307def Dset (t : ℕ) : Finset ((ℤ × ℤ × ℤ) × (ℤ × ℤ × ℤ)) :=
308 (ball t ×ˢ dirs).filter
309 (fun p => (p.1.1 + p.2.1, p.1.2.1 + p.2.2.1, p.1.2.2 + p.2.2.2) ∈ ball t)
310
311/-- **+x boundary count.** The octahedron cells whose `+x` neighbour leaves the ball are exactly the
312maximal-`x` cell of each `(y, z)` transverse diamond, one per point of `Diamond.ball t`, so there are
313`2t² + 2t + 1` of them. The boundary is a codimension-1 diamond. -/
314theorem boundary_xpos (t : ℕ) :
315 ((ball t).filter (fun p => (p.1 + 1, p.2.1, p.2.2) ∉ ball t)).card
316 = 2 * t ^ 2 + 2 * t + 1 := by
317 rw [← LatticeBallVolume.Diamond.card_ball t]
318 refine Finset.card_bij' (fun p _ => (p.2.1, p.2.2))
319 (fun q _ => (((t : ℤ) - q.1.natAbs - q.2.natAbs), q.1, q.2)) ?_ ?_ ?_ ?_
320 · rintro ⟨x, y, z⟩ hp
321 simp only [Finset.mem_filter, mem_ball_iff] at hp
322 simp only [InterfaceComponentBound.Diamond.mem_ball_iff]; omega
323 · intro q hq
324 rw [InterfaceComponentBound.Diamond.mem_ball_iff] at hq
325 simp only [Finset.mem_filter, mem_ball_iff]
326 refine ⟨by omega, by omega⟩
327 · rintro ⟨x, y, z⟩ hp
328 simp only [Finset.mem_filter, mem_ball_iff] at hp
329 simp only [Prod.mk.injEq, and_true, true_and]
330 omega
331 · intro q _; rfl
332
333/-- **-x boundary count.** Symmetric: `2t² + 2t + 1` minimal-`x` cells. -/
334theorem boundary_xneg (t : ℕ) :
335 ((ball t).filter (fun p => (p.1 + -1, p.2.1, p.2.2) ∉ ball t)).card
336 = 2 * t ^ 2 + 2 * t + 1 := by
337 rw [← LatticeBallVolume.Diamond.card_ball t]
338 refine Finset.card_bij' (fun p _ => (p.2.1, p.2.2))
339 (fun q _ => ((-((t : ℤ) - q.1.natAbs - q.2.natAbs)), q.1, q.2)) ?_ ?_ ?_ ?_
340 · rintro ⟨x, y, z⟩ hp
341 simp only [Finset.mem_filter, mem_ball_iff] at hp
342 simp only [InterfaceComponentBound.Diamond.mem_ball_iff]; omega
343 · intro q hq
344 rw [InterfaceComponentBound.Diamond.mem_ball_iff] at hq
345 simp only [Finset.mem_filter, mem_ball_iff]
346 refine ⟨by omega, by omega⟩
347 · rintro ⟨x, y, z⟩ hp
348 simp only [Finset.mem_filter, mem_ball_iff] at hp
349 simp only [Prod.mk.injEq, and_true, true_and]
350 omega
351 · intro q _; rfl
352
353/-- **+y boundary count.** `2t² + 2t + 1` maximal-`y` cells, one per `(x, z)` transverse diamond. -/
354theorem boundary_ypos (t : ℕ) :
355 ((ball t).filter (fun p => (p.1, p.2.1 + 1, p.2.2) ∉ ball t)).card
356 = 2 * t ^ 2 + 2 * t + 1 := by
357 rw [← LatticeBallVolume.Diamond.card_ball t]
358 refine Finset.card_bij' (fun p _ => (p.1, p.2.2))
359 (fun q _ => (q.1, ((t : ℤ) - q.1.natAbs - q.2.natAbs), q.2)) ?_ ?_ ?_ ?_
360 · rintro ⟨x, y, z⟩ hp
361 simp only [Finset.mem_filter, mem_ball_iff] at hp
362 simp only [InterfaceComponentBound.Diamond.mem_ball_iff]; omega
363 · intro q hq
364 rw [InterfaceComponentBound.Diamond.mem_ball_iff] at hq
365 simp only [Finset.mem_filter, mem_ball_iff]
366 refine ⟨by omega, by omega⟩
367 · rintro ⟨x, y, z⟩ hp
368 simp only [Finset.mem_filter, mem_ball_iff] at hp
369 simp only [Prod.mk.injEq, and_true, true_and]
370 omega
371 · intro q _; rfl
372
373/-- **-y boundary count.** `2t² + 2t + 1` minimal-`y` cells. -/
374theorem boundary_yneg (t : ℕ) :
375 ((ball t).filter (fun p => (p.1, p.2.1 + -1, p.2.2) ∉ ball t)).card
376 = 2 * t ^ 2 + 2 * t + 1 := by
377 rw [← LatticeBallVolume.Diamond.card_ball t]
378 refine Finset.card_bij' (fun p _ => (p.1, p.2.2))
379 (fun q _ => (q.1, (-((t : ℤ) - q.1.natAbs - q.2.natAbs)), q.2)) ?_ ?_ ?_ ?_
380 · rintro ⟨x, y, z⟩ hp
381 simp only [Finset.mem_filter, mem_ball_iff] at hp
382 simp only [InterfaceComponentBound.Diamond.mem_ball_iff]; omega
383 · intro q hq
384 rw [InterfaceComponentBound.Diamond.mem_ball_iff] at hq
385 simp only [Finset.mem_filter, mem_ball_iff]
386 refine ⟨by omega, by omega⟩
387 · rintro ⟨x, y, z⟩ hp
388 simp only [Finset.mem_filter, mem_ball_iff] at hp
389 simp only [Prod.mk.injEq, and_true, true_and]
390 omega
391 · intro q _; rfl
392
393/-- **+z boundary count.** `2t² + 2t + 1` maximal-`z` cells, one per `(x, y)` transverse diamond. -/
394theorem boundary_zpos (t : ℕ) :
395 ((ball t).filter (fun p => (p.1, p.2.1, p.2.2 + 1) ∉ ball t)).card
396 = 2 * t ^ 2 + 2 * t + 1 := by
397 rw [← LatticeBallVolume.Diamond.card_ball t]
398 refine Finset.card_bij' (fun p _ => (p.1, p.2.1))
399 (fun q _ => (q.1, q.2, ((t : ℤ) - q.1.natAbs - q.2.natAbs))) ?_ ?_ ?_ ?_
400 · rintro ⟨x, y, z⟩ hp
401 simp only [Finset.mem_filter, mem_ball_iff] at hp
402 simp only [InterfaceComponentBound.Diamond.mem_ball_iff]; omega
403 · intro q hq
404 rw [InterfaceComponentBound.Diamond.mem_ball_iff] at hq
405 simp only [Finset.mem_filter, mem_ball_iff]
406 refine ⟨by omega, by omega⟩
407 · rintro ⟨x, y, z⟩ hp
408 simp only [Finset.mem_filter, mem_ball_iff] at hp
409 simp only [Prod.mk.injEq, and_true, true_and]
410 omega
411 · intro q _; rfl
412
413/-- **-z boundary count.** `2t² + 2t + 1` minimal-`z` cells. -/
414theorem boundary_zneg (t : ℕ) :
415 ((ball t).filter (fun p => (p.1, p.2.1, p.2.2 + -1) ∉ ball t)).card
416 = 2 * t ^ 2 + 2 * t + 1 := by
417 rw [← LatticeBallVolume.Diamond.card_ball t]
418 refine Finset.card_bij' (fun p _ => (p.1, p.2.1))
419 (fun q _ => (q.1, q.2, (-((t : ℤ) - q.1.natAbs - q.2.natAbs)))) ?_ ?_ ?_ ?_
420 · rintro ⟨x, y, z⟩ hp
421 simp only [Finset.mem_filter, mem_ball_iff] at hp
422 simp only [InterfaceComponentBound.Diamond.mem_ball_iff]; omega
423 · intro q hq
424 rw [InterfaceComponentBound.Diamond.mem_ball_iff] at hq
425 simp only [Finset.mem_filter, mem_ball_iff]
426 refine ⟨by omega, by omega⟩
427 · rintro ⟨x, y, z⟩ hp
428 simp only [Finset.mem_filter, mem_ball_iff] at hp
429 simp only [Prod.mk.injEq, and_true, true_and]
430 omega
431 · intro q _; rfl
432
433/-- For each unit direction, `3 ·` the count of in-ball steps is `4t³ + 2t`: the bulk
434`3 · card (ball) = 4t³ + 6t² + 8t + 3` minus `3 ·` the `2t² + 2t + 1` codimension-1 boundary. -/
435theorem three_mul_step_card (t : ℕ) (d : ℤ × ℤ × ℤ) (hd : d ∈ dirs) :
436 3 * ((ball t).filter (fun p => (p.1 + d.1, p.2.1 + d.2.1, p.2.2 + d.2.2) ∈ ball t)).card
437 = 4 * t ^ 3 + 2 * t := by
438 have hvol : 3 * (ball t).card = 4 * t ^ 3 + 6 * t ^ 2 + 8 * t + 3 :=
439 LatticeBallVolume.Octahedron.three_mul_card_ball t
440 simp only [dirs, Finset.mem_insert, Finset.mem_singleton] at hd
441 rcases hd with rfl | rfl | rfl | rfl | rfl | rfl
442 · have hbd := boundary_xpos t
443 have hsplit := Finset.filter_card_add_filter_neg_card_eq_card
444 (s := ball t) (p := fun p : ℤ × ℤ × ℤ => (p.1 + 1, p.2.1, p.2.2) ∈ ball t)
445 simp only [add_zero] at *
446 omega
447 · have hbd := boundary_xneg t
448 have hsplit := Finset.filter_card_add_filter_neg_card_eq_card
449 (s := ball t) (p := fun p : ℤ × ℤ × ℤ => (p.1 + -1, p.2.1, p.2.2) ∈ ball t)
450 simp only [add_zero] at *
451 omega
452 · have hbd := boundary_ypos t
453 have hsplit := Finset.filter_card_add_filter_neg_card_eq_card
454 (s := ball t) (p := fun p : ℤ × ℤ × ℤ => (p.1, p.2.1 + 1, p.2.2) ∈ ball t)
455 simp only [add_zero] at *
456 omega
457 · have hbd := boundary_yneg t
458 have hsplit := Finset.filter_card_add_filter_neg_card_eq_card
459 (s := ball t) (p := fun p : ℤ × ℤ × ℤ => (p.1, p.2.1 + -1, p.2.2) ∈ ball t)
460 simp only [add_zero] at *
461 omega
462 · have hbd := boundary_zpos t
463 have hsplit := Finset.filter_card_add_filter_neg_card_eq_card
464 (s := ball t) (p := fun p : ℤ × ℤ × ℤ => (p.1, p.2.1, p.2.2 + 1) ∈ ball t)
465 simp only [add_zero] at *
466 omega
467 · have hbd := boundary_zneg t
468 have hsplit := Finset.filter_card_add_filter_neg_card_eq_card
469 (s := ball t) (p := fun p : ℤ × ℤ × ℤ => (p.1, p.2.1, p.2.2 + -1) ∈ ball t)
470 simp only [add_zero] at *
471 omega
472
473/-- `3 ·` the `(cell, direction)` index count is `24t³ + 12t`: six directions, each `4t³ + 2t`. -/
474theorem three_mul_Dset_card (t : ℕ) : 3 * (Dset t).card = 24 * t ^ 3 + 12 * t := by
475 have hsum : (Dset t).card
476 = ∑ d ∈ dirs,
477 ((ball t).filter (fun p => (p.1 + d.1, p.2.1 + d.2.1, p.2.2 + d.2.2) ∈ ball t)).card := by
478 rw [Dset, Finset.card_filter, Finset.sum_product, Finset.sum_comm]
479 refine Finset.sum_congr rfl (fun d _ => ?_)
480 rw [Finset.card_filter]
481 rw [hsum, Finset.mul_sum]
482 rw [Finset.sum_congr rfl (fun d hd => three_mul_step_card t d hd)]
483 rw [Finset.sum_const, dirs_card]
484 ring
485
486set_option maxHeartbeats 1000000 in
487/-- **The 3-D total adjacency law, division-free.** The octahedron `|x| + |y| + |z| ≤ t` has exactly
488`8t³ + 4t` ordered 6-neighbour adjacencies (stated as `3 · card = 24t³ + 12t`). THEOREM over `ℕ`. -/
489theorem three_mul_total_edge_card (t : ℕ) : 3 * (E t).card = 24 * t ^ 3 + 12 * t := by
490 rw [show (E t).card = (Dset t).card from ?_, three_mul_Dset_card t]
491 refine Finset.card_bij'
492 (fun p _ => (p.1.val, (p.2.val.1 - p.1.val.1, p.2.val.2.1 - p.1.val.2.1,
493 p.2.val.2.2 - p.1.val.2.2)))
494 (fun cd hcd => (⟨cd.1, ?_⟩,
495 ⟨(cd.1.1 + cd.2.1, cd.1.2.1 + cd.2.2.1, cd.1.2.2 + cd.2.2.2), ?_⟩)) ?_ ?_ ?_ ?_
496 · simp only [Dset, Finset.mem_filter, Finset.mem_product] at hcd
497 exact hcd.1.1
498 · simp only [Dset, Finset.mem_filter, Finset.mem_product] at hcd
499 exact hcd.2
500 · rintro ⟨a, b⟩ hp
501 simp only [E, Finset.mem_filter, Finset.mem_univ, true_and] at hp
502 simp only [Dset, Finset.mem_filter, Finset.mem_product]
503 refine ⟨⟨a.property, ?_⟩, ?_⟩
504 · unfold adj at hp
505 simp only [dirs, Finset.mem_insert, Finset.mem_singleton, Prod.mk.injEq]
506 omega
507 · have hb : (a.val.1 + (b.val.1 - a.val.1), a.val.2.1 + (b.val.2.1 - a.val.2.1),
508 a.val.2.2 + (b.val.2.2 - a.val.2.2)) = b.val := by
509 rw [Prod.ext_iff, Prod.ext_iff]
510 refine ⟨?_, ?_, ?_⟩ <;> · dsimp only; ring
511 rw [hb]; exact b.property
512 · rintro ⟨c, d⟩ hcd
513 simp only [Dset, Finset.mem_filter, Finset.mem_product] at hcd
514 simp only [E, Finset.mem_filter, Finset.mem_univ, true_and]
515 unfold adj
516 have hdir : d ∈ dirs := hcd.1.2
517 simp only [dirs, Finset.mem_insert, Finset.mem_singleton] at hdir
518 rcases hdir with rfl | rfl | rfl | rfl | rfl | rfl <;> · dsimp only; omega
519 · rintro ⟨a, b⟩ hp
520 dsimp only
521 rw [Prod.ext_iff]
522 refine ⟨?_, ?_⟩
523 · apply Subtype.ext; rfl
524 · apply Subtype.ext
525 rw [Prod.ext_iff, Prod.ext_iff]
526 refine ⟨?_, ?_, ?_⟩ <;> · dsimp only; ring
527 · rintro ⟨c, d⟩ hcd
528 dsimp only
529 rw [Prod.ext_iff]
530 refine ⟨rfl, ?_⟩
531 rw [Prod.ext_iff, Prod.ext_iff]
532 refine ⟨?_, ?_, ?_⟩ <;> · dsimp only; ring
533
534/-- **The 3-D total adjacency count.** Dividing the division-free law, the octahedron has exactly
535`8t³ + 4t` ordered 6-neighbour adjacencies. -/
536theorem total_edge_card (t : ℕ) : (E t).card = 8 * t ^ 3 + 4 * t := by
537 have h := three_mul_total_edge_card t
538 omega
539
540/-- The engine's octahedron edge list has `8t³ + 4t` entries. -/
541theorem edges_length (t : ℕ) :
542 (InterfaceComponentBound.Octahedron.edges t).length = 8 * t ^ 3 + 4 * t := by
543 rw [InterfaceComponentBound.Octahedron.edges, Finset.length_toList]
544 exact total_edge_card t
545
546open PolarizedBirthDomains.Octahedron (polarized)
547open PolarizedBirthInterface.Octahedron (B)
548
549/-- The carried (monochromatic) adjacencies of the polarized octahedron birth field. -/
550noncomputable def carried (t : ℕ) : Finset (Vtx t × Vtx t) :=
551 (E t).filter (fun p => polarized t p.1 = polarized t p.2)
552
553/-- **The exact carried (monochromatic) edge count in 3-D.** Total `8t³ + 4t` minus the interface
554`8t² - 8t + 4` gives carried `8t³ - 8t² + 12t - 4`: the bulk the octahedron coarsening carries free,
555complementing the `Θ(t²)` interface it must post. THEOREM over `ℕ` (`t ≥ 1`). -/
556theorem carried_edge_card (t : ℕ) (ht : 1 ≤ t) :
557 (carried t).card = 8 * t ^ 3 - 8 * t ^ 2 + 12 * t - 4 := by
558 have hsplit := Finset.filter_card_add_filter_neg_card_eq_card
559 (s := E t) (p := fun p : Vtx t × Vtx t => polarized t p.1 ≠ polarized t p.2)
560 have hBeq : (E t).filter (fun p => polarized t p.1 ≠ polarized t p.2) = B t := by
561 rw [E, B, Finset.filter_filter]
562 have hMeq : (E t).filter (fun p => ¬ (polarized t p.1 ≠ polarized t p.2)) = carried t := by
563 rw [carried]
564 apply Finset.filter_congr
565 intro p _
566 simp
567 rw [hBeq, hMeq] at hsplit
568 have hB : (B t).card = 8 * t ^ 2 - 8 * t + 4 := PolarizedBirthInterface.Octahedron.interface_card_eq t ht
569 have hE : (E t).card = 8 * t ^ 3 + 4 * t := total_edge_card t
570 rw [hB, hE] at hsplit
571 obtain ⟨n, rfl⟩ : ∃ n, t = n + 1 := ⟨t - 1, by omega⟩
572 have h2 : (n + 1) ^ 2 = n ^ 2 + 2 * n + 1 := by ring
573 have h3 : (n + 1) ^ 3 = n ^ 3 + 3 * n ^ 2 + 3 * n + 1 := by ring
574 rw [h2, h3] at hsplit ⊢
575 omega
576
577/-- **Discrete isoperimetric / surface law (3-D).** The forced interface satisfies
578`(interface)³ ≤ 8 · (total adjacency)²`, the codimension-1 scaling in three dimensions: the interface
579is `Θ(t²)` while the total adjacency is `Θ(t³)`, so the interface grows only as the `2/3` power of the
580bulk. It is a surface, not a volume. THEOREM over `ℕ`. -/
581theorem interface_cube_le_total_sq (t : ℕ) (ht : 1 ≤ t) :
582 (B t).card ^ 3 ≤ 8 * (E t).card ^ 2 := by
583 rw [PolarizedBirthInterface.Octahedron.interface_card_eq t ht, total_edge_card t]
584 obtain ⟨n, rfl⟩ : ∃ n, t = n + 1 := ⟨t - 1, by omega⟩
585 have hL : 8 * (n + 1) ^ 2 - 8 * (n + 1) + 4 = 8 * n ^ 2 + 8 * n + 4 := by
586 have e1 : 8 * (n + 1) ^ 2 = 8 * n ^ 2 + 16 * n + 8 := by ring
587 omega
588 rw [hL]
589 have hB : 8 * n ^ 2 + 8 * n + 4 ≤ 8 * (n + 1) ^ 2 := by nlinarith [Nat.zero_le n]
590 have hE : 8 * (n + 1) ^ 3 ≤ 8 * (n + 1) ^ 3 + 4 * (n + 1) := Nat.le_add_right _ _
591 calc (8 * n ^ 2 + 8 * n + 4) ^ 3
592 ≤ (8 * (n + 1) ^ 2) ^ 3 := Nat.pow_le_pow_left hB 3
593 _ = 8 * (8 * (n + 1) ^ 3) ^ 2 := by ring
594 _ ≤ 8 * (8 * (n + 1) ^ 3 + 4 * (n + 1)) ^ 2 :=
595 Nat.mul_le_mul_left 8 (Nat.pow_le_pow_left hE 2)
596
597/-- **Carried dominates interface (3-D).** For a world of radius `t ≥ 1`, the octahedron coarsening
598carries strictly more edges free than it posts (`8t³ - 8t² + 12t - 4 ≥ 8t² - 8t + 4`): the carried
599bulk overtakes the `Θ(t²)` interface for every world larger than a single shell. -/
600theorem carried_ge_interface (t : ℕ) (ht : 1 ≤ t) :
601 (B t).card ≤ (carried t).card := by
602 rw [PolarizedBirthInterface.Octahedron.interface_card_eq t ht, carried_edge_card t ht]
603 obtain ⟨n, rfl⟩ : ∃ n, t = n + 1 := ⟨t - 1, by omega⟩
604 have e2 : 8 * (n + 1) ^ 2 = 8 * n ^ 2 + 16 * n + 8 := by ring
605 have e3 : 8 * (n + 1) ^ 3 = 8 * n ^ 3 + 24 * n ^ 2 + 24 * n + 8 := by ring
606 omega
607
608end Octahedron
609
610end LatticeBallEdges
611end Cosmology
612end IndisputableMonolith
613