IndisputableMonolith.Cosmology.LatticeBallVolume
IndisputableMonolith/Cosmology/LatticeBallVolume.lean · 281 lines · 5 declarations
show as:
view math explainer →
1import Mathlib
2import IndisputableMonolith.Cosmology.InterfaceComponentBound
3
4/-!
5# Lattice-ball cardinalities: the area and volume laws of the coarsening engine
6
7The scale-adaptive coarsening engine accumulates its world on an L1 ball that grows by one rung per
8recognition cycle: the 2D diamond `|x| + |y| ≤ t` and the 3D octahedron `|x| + |y| + |z| ≤ t`. The
9numeric runs report the *total* cell count after `t` cycles ("the diamond grew to 1201 cells" at
10`t = 24`; "the octahedron grew to 2625 cells" at `t = 12`). This module lifts those counts to closed
11forms, as THEOREMs over `ℕ`, with no `sorry` and no new axioms.
12
13* `Diamond.card_ball t = 2 t² + 2 t + 1` (the centered square number). At `t = 24` this is `1201`.
14* `Octahedron.three_mul_card_ball t : 3 * card (ball t) = 4 t³ + 6 t² + 8 t + 3` (the centered
15 octahedral number `(2t+1)(2t²+2t+3)/3`, division-free). At `t = 12` the count is `2625`.
16
17Why this matters for the simulation: the accumulated world is `Θ(t^d)` while the recognition-active
18frontier born each cycle is the shell `card (ball t) - card (ball (t-1))`, which these laws make
19`4 t` (diamond) and `4 t² + 2` (octahedron), i.e. `Θ(t^{d-1})`. The active fraction
20`shell / ball → 0`: the cost localizes to a perimeter. The interface-component bound
21(`InterfaceComponentBound`) and these volume laws together are the geometric backbone of the
22sub-extensivity claim of Phases 13/14/15.
23
24Both proofs reduce a `d`-dimensional ball to a fibered sum over the first coordinate of `(d-1)`-balls,
25so the octahedron law is built on the diamond law. The diamond slice over a fixed `x` is the integer
26interval `[-(t - |x|), t - |x|]`, of width `2(t - |x|) + 1`; summing that over `x ∈ [-t, t]` gives the
27closed form by induction (peeling the two new endpoints each step).
28-/
29
30namespace IndisputableMonolith
31namespace Cosmology
32namespace LatticeBallVolume
33
34open Finset
35open scoped BigOperators
36
37/-! ### The 1-D slice: lattice points in `[-t, t]` with `|x| + |y| ≤ t` for fixed `x`. -/
38
39/-- For `|x| ≤ t`, the `y`-slice `{ y ∈ [-t, t] : |x| + |y| ≤ t }` is exactly the interval
40`[-(t - |x|), t - |x|]`, hence has `2 (t - |x|) + 1` points. -/
41theorem slice_card (t : ℕ) (x : ℤ) (hx : x.natAbs ≤ t) :
42 ((Finset.Icc (-(t : ℤ)) t).filter (fun y => x.natAbs + y.natAbs ≤ t)).card
43 = 2 * (t - x.natAbs) + 1 := by
44 have hset : (Finset.Icc (-(t : ℤ)) t).filter (fun y => x.natAbs + y.natAbs ≤ t)
45 = Finset.Icc (-(((t - x.natAbs : ℕ)) : ℤ)) (((t - x.natAbs : ℕ)) : ℤ) := by
46 apply Finset.ext
47 intro y
48 simp only [Finset.mem_filter, Finset.mem_Icc]
49 omega
50 rw [hset, Int.card_Icc]
51 omega
52
53/-! ### The 2-D diamond area law. -/
54
55/-- Fibered form of the diamond cardinality: sum the slice widths over the first coordinate. -/
56theorem diamond_card_eq_sum (t : ℕ) :
57 (InterfaceComponentBound.Diamond.ball t).card
58 = ∑ x ∈ Finset.Icc (-(t : ℤ)) t, (2 * (t - x.natAbs) + 1) := by
59 have hb : InterfaceComponentBound.Diamond.ball t
60 = (Finset.Icc (-(t : ℤ)) t ×ˢ Finset.Icc (-(t : ℤ)) t).filter
61 (fun p => p.1.natAbs + p.2.natAbs ≤ t) := rfl
62 rw [hb, Finset.card_filter, Finset.sum_product]
63 refine Finset.sum_congr rfl (fun x hx => ?_)
64 rw [Finset.mem_Icc] at hx
65 have hxnat : x.natAbs ≤ t := by omega
66 dsimp only
67 rw [← slice_card t x hxnat, Finset.card_filter]
68
69/-- The symmetric-interval sum `∑_{x ∈ [-t,t]} (2 (t - |x|) + 1) = 2 t² + 2 t + 1`, by induction
70peeling the two new endpoints `±(t+1)` each step. -/
71theorem outer_sum_2d (t : ℕ) :
72 ∑ x ∈ Finset.Icc (-(t : ℤ)) t, (2 * (t - x.natAbs) + 1) = 2 * t ^ 2 + 2 * t + 1 := by
73 induction t with
74 | zero => simp
75 | succ n ih =>
76 have hsplit : Finset.Icc (-((n : ℤ) + 1)) ((n : ℤ) + 1)
77 = insert (-((n : ℤ) + 1)) (insert ((n : ℤ) + 1) (Finset.Icc (-(n : ℤ)) (n : ℤ))) := by
78 apply Finset.ext
79 intro z
80 simp only [Finset.mem_insert, Finset.mem_Icc]
81 omega
82 have hmem2 : ((n : ℤ) + 1) ∉ Finset.Icc (-(n : ℤ)) (n : ℤ) := by
83 simp only [Finset.mem_Icc]; omega
84 have hmem1 : (-((n : ℤ) + 1))
85 ∉ insert ((n : ℤ) + 1) (Finset.Icc (-(n : ℤ)) (n : ℤ)) := by
86 simp only [Finset.mem_insert, Finset.mem_Icc]; omega
87 have hcast : (((n : ℕ) + 1 : ℕ) : ℤ) = (n : ℤ) + 1 := by push_cast; ring
88 rw [show (((n : ℕ) + 1 : ℕ) : ℤ) = (n : ℤ) + 1 from hcast]
89 rw [hsplit, Finset.sum_insert hmem1, Finset.sum_insert hmem2]
90 -- endpoint contributions: |±(n+1)| = n+1, so each summand is 2*((n+1) - (n+1)) + 1 = 1
91 have hendL : 2 * ((n + 1) - (-((n : ℤ) + 1)).natAbs) + 1 = 1 := by
92 have : (-((n : ℤ) + 1)).natAbs = n + 1 := by
93 rw [Int.natAbs_neg]; omega
94 rw [this]; omega
95 have hendR : 2 * ((n + 1) - (((n : ℤ) + 1)).natAbs) + 1 = 1 := by
96 have : (((n : ℤ) + 1)).natAbs = n + 1 := by omega
97 rw [this]; omega
98 rw [hendL, hendR]
99 -- rewrite the inner sum's summand: for x ∈ [-n,n], (n+1) - |x| = (n - |x|) + 1
100 have hcongr : ∑ x ∈ Finset.Icc (-(n : ℤ)) (n : ℤ), (2 * ((n + 1) - x.natAbs) + 1)
101 = ∑ x ∈ Finset.Icc (-(n : ℤ)) (n : ℤ), ((2 * (n - x.natAbs) + 1) + 2) := by
102 refine Finset.sum_congr rfl (fun x hx => ?_)
103 rw [Finset.mem_Icc] at hx
104 have hxnat : x.natAbs ≤ n := by omega
105 omega
106 rw [hcongr, Finset.sum_add_distrib, ih, Finset.sum_const]
107 have hcard : (Finset.Icc (-(n : ℤ)) (n : ℤ)).card = 2 * n + 1 := by
108 rw [Int.card_Icc]; omega
109 rw [hcard]
110 ring
111
112/-- **The 2-D diamond area law, every radius.** The L1 ball `|x| + |y| ≤ t` has exactly
113`2 t² + 2 t + 1` lattice points (the centered square number). At `t = 24` this is `1201`, the cell
114count the 2D coarsening run reports. THEOREM over `ℕ`. -/
115theorem Diamond.card_ball (t : ℕ) :
116 (InterfaceComponentBound.Diamond.ball t).card = 2 * t ^ 2 + 2 * t + 1 := by
117 rw [diamond_card_eq_sum, outer_sum_2d]
118
119/-! ### The 3-D octahedron volume law (reduces to the diamond law fiber by fiber). -/
120
121/-- Fibered form of the octahedron cardinality: each `x`-fiber is a diamond of radius `t - |x|`. -/
122theorem octa_card_eq_sum (t : ℕ) :
123 (InterfaceComponentBound.Octahedron.ball t).card
124 = ∑ x ∈ Finset.Icc (-(t : ℤ)) t,
125 (InterfaceComponentBound.Diamond.ball (t - x.natAbs)).card := by
126 have hb : InterfaceComponentBound.Octahedron.ball t
127 = (Finset.Icc (-(t : ℤ)) t ×ˢ (Finset.Icc (-(t : ℤ)) t ×ˢ Finset.Icc (-(t : ℤ)) t)).filter
128 (fun p => p.1.natAbs + p.2.1.natAbs + p.2.2.natAbs ≤ t) := rfl
129 rw [hb, Finset.card_filter, Finset.sum_product]
130 refine Finset.sum_congr rfl (fun x hx => ?_)
131 rw [Finset.mem_Icc] at hx
132 have hxnat : x.natAbs ≤ t := by omega
133 dsimp only
134 -- the (y,z)-fiber over x equals the diamond of radius (t - |x|)
135 have hfib : (Finset.Icc (-(t : ℤ)) t ×ˢ Finset.Icc (-(t : ℤ)) t).filter
136 (fun q : ℤ × ℤ => x.natAbs + q.1.natAbs + q.2.natAbs ≤ t)
137 = InterfaceComponentBound.Diamond.ball (t - x.natAbs) := by
138 apply Finset.ext
139 rintro ⟨y, z⟩
140 rw [InterfaceComponentBound.Diamond.mem_ball_iff]
141 simp only [Finset.mem_filter, Finset.mem_Icc, Finset.mem_product]
142 omega
143 -- the inner (y,z)-sum is exactly the diamond-fiber card
144 rw [← hfib, Finset.card_filter]
145
146/-- The octahedron outer sum reduces to the centered-octahedral recurrence. We prove the
147division-free form `3 · ∑ = 4 t³ + 6 t² + 8 t + 3` by induction, reusing the diamond area law for
148each fiber and the 2-D outer sum for the `∑ (t - |x|) = t²` identity that the step needs. -/
149theorem three_mul_outer_sum_3d (t : ℕ) :
150 3 * (∑ x ∈ Finset.Icc (-(t : ℤ)) t,
151 (InterfaceComponentBound.Diamond.ball (t - x.natAbs)).card)
152 = 4 * t ^ 3 + 6 * t ^ 2 + 8 * t + 3 := by
153 -- rewrite each fiber card via the diamond area law
154 have hrw : ∀ s : ℕ, ∑ x ∈ Finset.Icc (-(s : ℤ)) s,
155 (InterfaceComponentBound.Diamond.ball (s - x.natAbs)).card
156 = ∑ x ∈ Finset.Icc (-(s : ℤ)) s,
157 (2 * (s - x.natAbs) ^ 2 + 2 * (s - x.natAbs) + 1) := by
158 intro s
159 refine Finset.sum_congr rfl (fun x _ => ?_)
160 rw [Diamond.card_ball]
161 rw [hrw]
162 -- now an ℕ identity about a symmetric-interval sum of a quadratic in (t - |x|)
163 induction t with
164 | zero => simp
165 | succ n ih =>
166 have hsplit : Finset.Icc (-((n : ℤ) + 1)) ((n : ℤ) + 1)
167 = insert (-((n : ℤ) + 1)) (insert ((n : ℤ) + 1) (Finset.Icc (-(n : ℤ)) (n : ℤ))) := by
168 apply Finset.ext
169 intro z
170 simp only [Finset.mem_insert, Finset.mem_Icc]
171 omega
172 have hmem2 : ((n : ℤ) + 1) ∉ Finset.Icc (-(n : ℤ)) (n : ℤ) := by
173 simp only [Finset.mem_Icc]; omega
174 have hmem1 : (-((n : ℤ) + 1))
175 ∉ insert ((n : ℤ) + 1) (Finset.Icc (-(n : ℤ)) (n : ℤ)) := by
176 simp only [Finset.mem_insert, Finset.mem_Icc]; omega
177 have hcast : (((n : ℕ) + 1 : ℕ) : ℤ) = (n : ℤ) + 1 := by push_cast; ring
178 rw [show (((n : ℕ) + 1 : ℕ) : ℤ) = (n : ℤ) + 1 from hcast]
179 rw [hsplit, Finset.sum_insert hmem1, Finset.sum_insert hmem2]
180 have hendL : 2 * ((n + 1) - (-((n : ℤ) + 1)).natAbs) ^ 2
181 + 2 * ((n + 1) - (-((n : ℤ) + 1)).natAbs) + 1 = 1 := by
182 have : (-((n : ℤ) + 1)).natAbs = n + 1 := by rw [Int.natAbs_neg]; omega
183 rw [this]; simp
184 have hendR : 2 * ((n + 1) - (((n : ℤ) + 1)).natAbs) ^ 2
185 + 2 * ((n + 1) - (((n : ℤ) + 1)).natAbs) + 1 = 1 := by
186 have : (((n : ℤ) + 1)).natAbs = n + 1 := by omega
187 rw [this]; simp
188 rw [hendL, hendR]
189 -- inner-sum congruence: g((n+1) - |x|) = g((n - |x|)) + 4*(n+1 - |x|) for |x| ≤ n
190 have hcongr : ∑ x ∈ Finset.Icc (-(n : ℤ)) (n : ℤ),
191 (2 * ((n + 1) - x.natAbs) ^ 2 + 2 * ((n + 1) - x.natAbs) + 1)
192 = ∑ x ∈ Finset.Icc (-(n : ℤ)) (n : ℤ),
193 ((2 * (n - x.natAbs) ^ 2 + 2 * (n - x.natAbs) + 1)
194 + (4 * (n - x.natAbs) + 4)) := by
195 refine Finset.sum_congr rfl (fun x hx => ?_)
196 rw [Finset.mem_Icc] at hx
197 have hxnat : x.natAbs ≤ n := by omega
198 have hsub : (n + 1) - x.natAbs = (n - x.natAbs) + 1 := by omega
199 rw [hsub]; ring
200 rw [hcongr, Finset.sum_add_distrib]
201 have hcard : (Finset.Icc (-(n : ℤ)) (n : ℤ)).card = 2 * n + 1 := by
202 rw [Int.card_Icc]; omega
203 set S := ∑ x ∈ Finset.Icc (-(n : ℤ)) (n : ℤ),
204 (2 * (n - x.natAbs) ^ 2 + 2 * (n - x.natAbs) + 1) with hSdef
205 set T := ∑ x ∈ Finset.Icc (-(n : ℤ)) (n : ℤ), (4 * (n - x.natAbs) + 4) with hTdef
206 -- closed form for the residual increment sum T via the 2-D outer sum
207 have hT : T = 4 * n ^ 2 + 8 * n + 4 := by
208 rw [hTdef]
209 have hcongr2 : ∑ x ∈ Finset.Icc (-(n : ℤ)) (n : ℤ), (4 * (n - x.natAbs) + 4)
210 = ∑ x ∈ Finset.Icc (-(n : ℤ)) (n : ℤ), (2 * (2 * (n - x.natAbs) + 1) + 2) := by
211 refine Finset.sum_congr rfl (fun x _ => ?_); ring
212 rw [hcongr2, Finset.sum_add_distrib, ← Finset.mul_sum, outer_sum_2d, Finset.sum_const, hcard]
213 simp only [smul_eq_mul]; ring
214 -- regroup so that `3 * S` (the inductive hypothesis) appears as a subterm, then close by ring
215 have hcomb : 3 * (1 + (1 + (S + T))) = 3 * S + (3 * T + 6) := by ring
216 rw [hcomb, ih, hT]
217 ring
218
219/-- **The 3-D octahedron volume law, every radius.** The L1 ball `|x| + |y| + |z| ≤ t` has exactly
220the centered octahedral number `(2t+1)(2t²+2t+3)/3` of lattice points, stated division-free as
221`3 · card = 4 t³ + 6 t² + 8 t + 3`. At `t = 12` the count is `2625`, the cell count the 3D coarsening
222run reports. THEOREM over `ℕ`, reducing fiber by fiber to the diamond area law. -/
223theorem Octahedron.three_mul_card_ball (t : ℕ) :
224 3 * (InterfaceComponentBound.Octahedron.ball t).card = 4 * t ^ 3 + 6 * t ^ 2 + 8 * t + 3 := by
225 rw [octa_card_eq_sum, three_mul_outer_sum_3d]
226
227/-- The octahedron count at the radius the 3D run uses: `card (ball 12) = 2625`. -/
228theorem Octahedron.card_ball_twelve :
229 (InterfaceComponentBound.Octahedron.ball 12).card = 2625 := by
230 have h := Octahedron.three_mul_card_ball 12
231 norm_num at h
232 omega
233
234/-- The diamond count at the radius the 2D run uses: `card (ball 24) = 1201`. -/
235theorem Diamond.card_ball_twentyfour :
236 (InterfaceComponentBound.Diamond.ball 24).card = 1201 := by
237 rw [Diamond.card_ball]; norm_num
238
239/-! ### Boundary-shell laws: the per-cycle growth lives on a codimension-1 shell.
240
241The coarsening engine grows the world one radius per cycle, so the cells *added* at cycle `t+1`
242are the shell `ball (t+1) \ ball t`, whose count is `card_ball (t+1) - card_ball t`. These
243recurrences are the discrete derivative of the Phase-49 area/volume laws, and they are the exact
244geometric content of "the cost localizes to a perimeter / a surface": in 2D the per-cycle growth is
245linear (`4(t+1)`, a 1-D perimeter), in 3D it is quadratic (`4(t+1)² + 2`, a 2-D surface). This is the
246geometric boundary shell of newly recognized cells; it is distinct from the charge-dependent
247bichromatic interface bounded in `InterfaceComponentBound`. -/
248
249/-- **The 2-D perimeter (per-cycle growth) law.** Going from radius `t` to `t+1` adds exactly
250`4(t+1)` cells: the new cells form a 1-D perimeter shell. Equivalently, the shell at radius `s ≥ 1`
251has `4s` cells. Immediate from the area law `Diamond.card_ball`. -/
252theorem Diamond.shell_card (t : ℕ) :
253 (InterfaceComponentBound.Diamond.ball (t + 1)).card
254 = (InterfaceComponentBound.Diamond.ball t).card + 4 * (t + 1) := by
255 simp only [Diamond.card_ball]; ring
256
257/-- **The 3-D surface (per-cycle growth) law, division-free.** Going from radius `t` to `t+1` adds
258exactly `4(t+1)² + 2` cells (so `3 ·` the increment is `12(t+1)² + 6`): the new cells form a 2-D
259surface shell, the sharpest sub-extensive growth `~ V^(2/3)`. Immediate from the volume law
260`Octahedron.three_mul_card_ball`. -/
261theorem Octahedron.three_mul_shell_card (t : ℕ) :
262 3 * (InterfaceComponentBound.Octahedron.ball (t + 1)).card
263 = 3 * (InterfaceComponentBound.Octahedron.ball t).card + (12 * (t + 1) ^ 2 + 6) := by
264 simp only [Octahedron.three_mul_card_ball]; ring
265
266/-- The last 2-D shell the run adds (radius 24) has `4 · 24 = 96` cells. -/
267theorem Diamond.shell_card_twentyfour :
268 (InterfaceComponentBound.Diamond.ball 24).card
269 = (InterfaceComponentBound.Diamond.ball 23).card + 96 := by
270 have h := Diamond.shell_card 23; norm_num at h ⊢; exact h
271
272/-- The last 3-D shell the run adds (radius 12) has `4 · 12² + 2 = 578` cells (so `3 · 578 = 1734`). -/
273theorem Octahedron.three_mul_shell_card_twelve :
274 3 * (InterfaceComponentBound.Octahedron.ball 12).card
275 = 3 * (InterfaceComponentBound.Octahedron.ball 11).card + 1734 := by
276 have h := Octahedron.three_mul_shell_card 11; norm_num at h ⊢; exact h
277
278end LatticeBallVolume
279end Cosmology
280end IndisputableMonolith
281