IndisputableMonolith.Cosmology.PolarizedBirthInterfaceCount
IndisputableMonolith/Cosmology/PolarizedBirthInterfaceCount.lean · 453 lines · 14 declarations
show as:
view math explainer →
1import Mathlib
2import IndisputableMonolith.Cosmology.InterfaceComponentBound
3import IndisputableMonolith.Cosmology.LatticeBallVolume
4import IndisputableMonolith.Cosmology.PolarizedBirthDomains
5import IndisputableMonolith.Cosmology.PolarizedBirthInterface
6
7/-!
8# The exact interface edge count of the birth field, and constant recognition activity per cycle
9
10## Status: THEOREM (0 sorry, 0 axiom beyond Mathlib's standard three).
11
12Phase 51 (`PolarizedBirthInterface`) proved the recognition-active interface of the forced
13conjugate-birth field is confined to the codimension-1 spine and that the spine is sub-extensive,
14but it bounded only the spine *cells*, leaving the exact number of interface *edges* numeric. This
15module closes that: it counts the bichromatic ordered-edge list exactly.
16
17For the 2-D diamond the interface edge count is `8t - 4` (`interface_card_eq`), the ordered-edge
18count the engine's `comp`/`mono_le_interface_succ` machinery actually uses (twice the `4t - 2`
19undirected perimeter, since `edges` lists each adjacency in both orientations). The proof bridges
20the `toList` edge filter to a `Finset.card` (`interface_length_eq_card`), then counts that Finset by
21an explicit bijection (`Finset.card_bij'`) onto `{interior spine y} × {side, orientation}`: every
22bichromatic edge has exactly one spine endpoint `(0, y)` and one neighbour `(±1, y)`, so the data of
23the edge is exactly `(y, side, orientation)` with `|y| ≤ t - 1`.
24
25The headline corollary is `interface_increment_const`: the interface grows by exactly `8` ordered
26edges per cadence cycle (`t → t + 1`), a constant **independent of the world size**. The polarized
27birth posts a constant number of forced distinctions per cycle even as the world grows as `Θ(t²)`.
28This is the literal Lean statement of the compute-watch principle the simulation runs on: cost
29scales with recognition activity (the interface increment, `O(1)` per cycle), not with volume.
30
31The `Octahedron` namespace lifts the same count to the dimension the forcing chain selects (D = 3).
32There the interface is a 2-D surface: the bichromatic edges sit on the spine disk `x = 0`, in
33bijection with `{interior spine (y,z)} × {side, orientation}` where the interior spine is a 2-D
34diamond of radius `t - 1`, so the exact ordered count is `8t² - 8t + 4` (`Octahedron.interface_card_eq`,
35four times the Phase-49 area law `2(t-1)² + 2(t-1) + 1`). The per-cycle increment is then `16t`
36(`Octahedron.interface_increment_linear`), `Θ(t)` rather than `O(1)`. That is the honest 3-D statement:
37in three dimensions the forced recognition activity per cadence cycle grows linearly with the radius,
38because the recognition-active interface is a growing codimension-1 disk, not a fixed-size band. Cost
39still tracks recognition activity; in D = 3 that activity is `Θ(t)` per cycle, sub-extensive in the
40`Θ(t³)` volume but not constant.
41
42Both namespaces also carry `interface_total_growth`, the net interface edges introduced over a full
43forward run from radius `1` to `T`: `8T - 8 = 8(T-1)` in 2D and `8T² - 8T = 8T(T-1)` in 3D, the
44difference of the start and end interface sizes. This is `Θ(T^(D-1))`, strictly sub-extensive against
45the brute-force `Θ(T^(D+1))` spacetime cost (volume times cycles), the closed-form compute-watch
46run-total: a full run posts `Θ(T^(D-1))` net forced distinctions, not `Θ(T^(D+1))`.
47-/
48
49namespace IndisputableMonolith
50namespace Cosmology
51namespace PolarizedBirthInterface
52
53open InterfaceComponentBound
54
55namespace Diamond
56
57open InterfaceComponentBound.Diamond
58open PolarizedBirthDomains.Diamond
59
60/-- The bichromatic ordered-edge set of the polarized diamond field, as a `Finset`. This is the
61interface: the forced distinctions the engine posts. -/
62noncomputable def B (t : ℕ) : Finset (Vtx t × Vtx t) :=
63 Finset.univ.filter (fun p => adj p.1.val p.2.val ∧ polarized t p.1 ≠ polarized t p.2)
64
65/-- **Bridge: the interface edge-list length equals the Finset cardinality.** The `toList` edge set
66filtered to bichromatic pairs has length equal to the cardinality of the bichromatic edge `Finset`,
67because the edge list is `Nodup` (a `Finset.toList`) and filtering preserves `Nodup`. -/
68theorem interface_length_eq_card (t : ℕ) :
69 ((edges t).filter (fun p => decide (polarized t p.1 ≠ polarized t p.2))).length = (B t).card := by
70 have hnd : ((edges t).filter (fun p => decide (polarized t p.1 ≠ polarized t p.2))).Nodup := by
71 apply List.Nodup.filter
72 exact Finset.nodup_toList _
73 rw [← List.toFinset_card_of_nodup hnd]
74 congr 1
75 ext q
76 obtain ⟨a, b⟩ := q
77 simp only [List.mem_toFinset, List.mem_filter, mem_edges, decide_eq_true_eq, B,
78 Finset.mem_filter, Finset.mem_univ, true_and]
79
80/-- **Structure of a bichromatic edge.** Any adjacent pair of different polarized charge has exactly
81one endpoint on the spine `x = 0` and the other at `x = ±1`, and they share the `y`-coordinate. Pure
82case analysis on the two `sign(x)` values plus the unit-distance adjacency. This is the workhorse
83that pins the edge data to `(y, side, orientation)`. -/
84theorem edge_structure (t : ℕ) (a b : Vtx t) (hadj : adj a.val b.val)
85 (hpol : polarized t a ≠ polarized t b) :
86 (a.val.1 = 0 ∧ (b.val.1 = 1 ∨ b.val.1 = -1) ∧ a.val.2 = b.val.2) ∨
87 (b.val.1 = 0 ∧ (a.val.1 = 1 ∨ a.val.1 = -1) ∧ a.val.2 = b.val.2) := by
88 unfold adj at hadj
89 simp only [polarized] at hpol
90 split_ifs at hpol <;> omega
91
92/-- The index set parameterising the interface edges: the interior spine `y`-coordinate
93(`|y| ≤ t - 1`, the cells that actually have an `x = ±1` neighbour) times `(side, orientation)`. -/
94def idx (t : ℕ) : Finset (ℤ × Bool × Bool) :=
95 (Finset.Icc (-(t : ℤ) + 1) ((t : ℤ) - 1)) ×ˢ (Finset.univ : Finset (Bool × Bool))
96
97/-- The index set has `8t - 4` elements: `(2t - 1)` interior spine cells times `4` (side, orient). -/
98theorem idx_card (t : ℕ) (ht : 1 ≤ t) : (idx t).card = 8 * t - 4 := by
99 rw [idx, Finset.card_product, Int.card_Icc]
100 have h4 : (Finset.univ : Finset (Bool × Bool)).card = 4 := by decide
101 rw [h4]
102 omega
103
104/-- The spine cell `(0, y)` of an index lies in the ball. -/
105theorem memSpine (t : ℕ) (a : ℤ × Bool × Bool) (ha : a ∈ idx t) :
106 ((0 : ℤ), a.1) ∈ ball t := by
107 rw [idx, Finset.mem_product, Finset.mem_Icc] at ha
108 obtain ⟨⟨hlo, hhi⟩, -⟩ := ha
109 rw [InterfaceComponentBound.Diamond.mem_ball_iff]
110 omega
111
112/-- The neighbour cell `(±1, y)` of an index lies in the ball (since `|y| ≤ t - 1`). -/
113theorem memNbr (t : ℕ) (a : ℤ × Bool × Bool) (ha : a ∈ idx t) :
114 (((if a.2.1 then (1 : ℤ) else -1)), a.1) ∈ ball t := by
115 rw [idx, Finset.mem_product, Finset.mem_Icc] at ha
116 obtain ⟨⟨hlo, hhi⟩, -⟩ := ha
117 rw [InterfaceComponentBound.Diamond.mem_ball_iff]
118 split <;> · simp only [Int.natAbs_one, Int.natAbs_neg]; omega
119
120/-- The index data of a bichromatic edge: `(spine y, side of the ±1 neighbour, orientation)`. -/
121def edgeIndex (t : ℕ) (p : Vtx t × Vtx t) : ℤ × Bool × Bool :=
122 if p.1.val.1 = 0 then (p.1.val.2, decide (0 < p.2.val.1), true)
123 else (p.2.val.2, decide (0 < p.1.val.1), false)
124
125/-- The bichromatic edge reconstructed from its index data. -/
126def edgeFromIndex (t : ℕ) (a : ℤ × Bool × Bool) (ha : a ∈ idx t) : Vtx t × Vtx t :=
127 if a.2.2 then
128 (⟨((0 : ℤ), a.1), memSpine t a ha⟩, ⟨((if a.2.1 then (1 : ℤ) else -1), a.1), memNbr t a ha⟩)
129 else
130 (⟨((if a.2.1 then (1 : ℤ) else -1), a.1), memNbr t a ha⟩, ⟨((0 : ℤ), a.1), memSpine t a ha⟩)
131
132/-- **The exact 2-D interface edge count is `8t - 4`** (ordered edges). The bichromatic edge set is in
133bijection with `{interior spine y} × {side, orientation}`: every bichromatic edge has exactly one
134spine endpoint `(0, y)` and one neighbour `(±1, y)` sharing the `y`-coordinate, so the edge is fully
135determined by `(y, side, orientation)` with `|y| ≤ t - 1`. -/
136theorem interface_card_eq (t : ℕ) (ht : 1 ≤ t) : (B t).card = 8 * t - 4 := by
137 rw [← idx_card t ht]
138 refine Finset.card_bij' (fun p _ => edgeIndex t p) (fun a ha => edgeFromIndex t a ha) ?_ ?_ ?_ ?_
139 · -- hi : edgeIndex maps B into idx
140 rintro ⟨a, b⟩ hp
141 simp only [B, Finset.mem_filter, Finset.mem_univ, true_and] at hp
142 obtain ⟨hadj, hpol⟩ := hp
143 have hbm := b.property
144 have ham := a.property
145 rw [InterfaceComponentBound.Diamond.mem_ball_iff] at ham hbm
146 show edgeIndex t (a, b) ∈ idx t
147 rcases edge_structure t a b hadj hpol with ⟨h0, hbpm, hyeq⟩ | ⟨h0, hapm, hyeq⟩
148 · dsimp only [edgeIndex]
149 rw [if_pos h0, idx]
150 have key : b.val.2.natAbs ≤ t - 1 := by
151 have hb : b.val.1.natAbs + b.val.2.natAbs ≤ t := by
152 have hmem := b.property
153 rwa [InterfaceComponentBound.Diamond.mem_ball_iff] at hmem
154 have h1 : b.val.1.natAbs = 1 := by rcases hbpm with hb1 | hb1 <;> rw [hb1] <;> decide
155 omega
156 have hbnd : a.val.2 ∈ Finset.Icc (-(t : ℤ) + 1) ((t : ℤ) - 1) := by
157 rw [Finset.mem_Icc, hyeq]
158 omega
159 exact Finset.mem_product.mpr ⟨hbnd, Finset.mem_univ _⟩
160 · have hne : ¬ (a.val.1 = 0) := by rcases hapm with h | h <;> omega
161 dsimp only [edgeIndex]
162 rw [if_neg hne, idx]
163 have key : a.val.2.natAbs ≤ t - 1 := by
164 have ha : a.val.1.natAbs + a.val.2.natAbs ≤ t := by
165 have hmem := a.property
166 rwa [InterfaceComponentBound.Diamond.mem_ball_iff] at hmem
167 have h1 : a.val.1.natAbs = 1 := by rcases hapm with ha1 | ha1 <;> rw [ha1] <;> decide
168 omega
169 have hbnd : b.val.2 ∈ Finset.Icc (-(t : ℤ) + 1) ((t : ℤ) - 1) := by
170 rw [Finset.mem_Icc, ← hyeq]
171 omega
172 exact Finset.mem_product.mpr ⟨hbnd, Finset.mem_univ _⟩
173 · -- hj : edgeFromIndex maps idx into B
174 rintro a ha
175 show edgeFromIndex t a ha ∈ B t
176 simp only [B, Finset.mem_filter, Finset.mem_univ, true_and]
177 unfold edgeFromIndex
178 split
179 · refine ⟨?_, ?_⟩
180 · unfold adj; dsimp only; split <;> omega
181 · simp only [polarized]; dsimp only; split_ifs <;> omega
182 · refine ⟨?_, ?_⟩
183 · unfold adj; dsimp only; split <;> omega
184 · simp only [polarized]; dsimp only; split_ifs <;> omega
185 · -- left_inv : edgeFromIndex (edgeIndex p) = p
186 rintro ⟨a, b⟩ hp
187 simp only [B, Finset.mem_filter, Finset.mem_univ, true_and] at hp
188 obtain ⟨hadj, hpol⟩ := hp
189 rcases edge_structure t a b hadj hpol with ⟨h0, hbpm, hyeq⟩ | ⟨h0, hapm, hyeq⟩
190 · apply Prod.ext
191 · apply Subtype.ext
192 simp only [edgeIndex, edgeFromIndex, h0]
193 rw [Prod.ext_iff]
194 exact ⟨h0.symm, rfl⟩
195 · apply Subtype.ext
196 simp only [edgeIndex, edgeFromIndex, h0]
197 rw [Prod.ext_iff]
198 refine ⟨?_, hyeq⟩
199 rcases hbpm with hb1 | hb1 <;> simp [hb1]
200 · have hne : ¬ (a.val.1 = 0) := by rcases hapm with h | h <;> omega
201 apply Prod.ext
202 · apply Subtype.ext
203 simp only [edgeIndex, edgeFromIndex, if_neg hne]
204 rw [Prod.ext_iff]
205 refine ⟨?_, hyeq.symm⟩
206 rcases hapm with ha1 | ha1 <;> simp [ha1]
207 · apply Subtype.ext
208 simp only [edgeIndex, edgeFromIndex, if_neg hne]
209 rw [Prod.ext_iff]
210 rcases edge_structure t a b hadj hpol with ⟨h0', _, _⟩ | ⟨h0', _, _⟩
211 · exact absurd h0' hne
212 · exact ⟨h0'.symm, rfl⟩
213 · -- right_inv : edgeIndex (edgeFromIndex a) = a
214 rintro a ha
215 obtain ⟨y, side, orient⟩ := a
216 show edgeIndex t (edgeFromIndex t (y, side, orient) ha) = (y, side, orient)
217 cases orient <;> cases side <;>
218 simp [edgeFromIndex, edgeIndex]
219
220/-- **The concrete interface edge-list length is `8t - 4`.** Bridging the exact `Finset` count
221`interface_card_eq` through `interface_length_eq_card`, the actual bichromatic edge list the engine
222filters out of `edges t` has length exactly `8t - 4`. This is the form the numeric layer sees. -/
223theorem interface_length_eq (t : ℕ) (ht : 1 ≤ t) :
224 ((edges t).filter (fun p => decide (polarized t p.1 ≠ polarized t p.2))).length = 8 * t - 4 := by
225 rw [interface_length_eq_card, interface_card_eq t ht]
226
227/-- **Constant per-cycle recognition activity (the compute-watch law, in Lean).** Advancing the
228diamond birth field by one cadence cycle (`t → t + 1`) adds exactly `8` ordered interface edges,
229*independent of `t`* and hence independent of the world volume (which grows as `Θ(t²)`). The forced
230distinctions the engine must post per cycle are `O(1)`, so the simulation's cost scales with
231recognition activity, never with volume. -/
232theorem interface_increment_const (t : ℕ) (ht : 1 ≤ t) :
233 (B (t + 1)).card - (B t).card = 8 := by
234 rw [interface_card_eq (t + 1) (by omega), interface_card_eq t ht]
235 omega
236
237/-- **Total interface growth over a forward run (2-D).** The net number of interface edges the
238polarized birth introduces over a full run from radius `1` to radius `T` is exactly `8T - 8 = 8(T-1)`,
239the difference of the start and end interface sizes. This is `Θ(T)`, sub-extensive against the
240brute-force spacetime cost `Θ(T³)` (volume `Θ(T²)` times `T` cycles): the compute-watch total. -/
241theorem interface_total_growth (T : ℕ) (hT : 1 ≤ T) :
242 (B T).card - (B 1).card = 8 * T - 8 := by
243 rw [interface_card_eq T hT, interface_card_eq 1 (le_refl 1)]
244 omega
245
246end Diamond
247
248namespace Octahedron
249
250open InterfaceComponentBound.Octahedron
251open PolarizedBirthDomains.Octahedron
252
253/-- The bichromatic ordered-edge set of the polarized octahedron field, as a `Finset`. -/
254noncomputable def B (t : ℕ) : Finset (Vtx t × Vtx t) :=
255 Finset.univ.filter (fun p => adj p.1.val p.2.val ∧ polarized t p.1 ≠ polarized t p.2)
256
257/-- **Bridge: the interface edge-list length equals the Finset cardinality.** Same `Nodup`-filter
258argument as the 2-D case. -/
259theorem interface_length_eq_card (t : ℕ) :
260 ((edges t).filter (fun p => decide (polarized t p.1 ≠ polarized t p.2))).length = (B t).card := by
261 have hnd : ((edges t).filter (fun p => decide (polarized t p.1 ≠ polarized t p.2))).Nodup := by
262 apply List.Nodup.filter
263 exact Finset.nodup_toList _
264 rw [← List.toFinset_card_of_nodup hnd]
265 congr 1
266 ext q
267 obtain ⟨a, b⟩ := q
268 simp only [List.mem_toFinset, List.mem_filter, mem_edges, decide_eq_true_eq, B,
269 Finset.mem_filter, Finset.mem_univ, true_and]
270
271/-- **Structure of a bichromatic edge (3-D).** Any adjacent pair of different polarized charge has
272exactly one endpoint on the spine disk `x = 0` and the other at `x = ±1`, sharing both transverse
273coordinates `(y, z)`. Pure case analysis on the two `sign(x)` values plus unit-distance adjacency. -/
274theorem edge_structure (t : ℕ) (a b : Vtx t) (hadj : adj a.val b.val)
275 (hpol : polarized t a ≠ polarized t b) :
276 (a.val.1 = 0 ∧ (b.val.1 = 1 ∨ b.val.1 = -1) ∧ a.val.2.1 = b.val.2.1 ∧ a.val.2.2 = b.val.2.2) ∨
277 (b.val.1 = 0 ∧ (a.val.1 = 1 ∨ a.val.1 = -1) ∧ a.val.2.1 = b.val.2.1 ∧ a.val.2.2 = b.val.2.2) := by
278 unfold adj at hadj
279 simp only [polarized] at hpol
280 split_ifs at hpol <;> omega
281
282/-- The index set parameterising the 3-D interface edges: the interior spine disk
283`{(y, z) : |y| + |z| ≤ t - 1}` (a 2-D diamond, the cells that actually have an `x = ±1` neighbour)
284times `(side, orientation)`. -/
285def idx (t : ℕ) : Finset ((ℤ × ℤ) × Bool × Bool) :=
286 (InterfaceComponentBound.Diamond.ball (t - 1)) ×ˢ (Finset.univ : Finset (Bool × Bool))
287
288/-- The index set has `8t² - 8t + 4` elements: the interior spine disk is a 2-D diamond of radius
289`t - 1` with `2(t-1)² + 2(t-1) + 1` cells (the Phase-49 area law), times `4` (side, orient). -/
290theorem idx_card (t : ℕ) (ht : 1 ≤ t) : (idx t).card = 8 * t ^ 2 - 8 * t + 4 := by
291 obtain ⟨n, rfl⟩ : ∃ n, t = n + 1 := ⟨t - 1, by omega⟩
292 rw [idx, Finset.card_product]
293 have h4 : (Finset.univ : Finset (Bool × Bool)).card = 4 := by decide
294 have e1 : n + 1 - 1 = n := by omega
295 rw [e1, h4, LatticeBallVolume.Diamond.card_ball n]
296 have e2 : (n + 1) ^ 2 = n ^ 2 + 2 * n + 1 := by ring
297 rw [e2]
298 omega
299
300/-- The spine cell `(0, y, z)` of an index lies in the ball. -/
301theorem memSpine (t : ℕ) (a : (ℤ × ℤ) × Bool × Bool) (ha : a ∈ idx t) :
302 ((0 : ℤ), a.1) ∈ ball t := by
303 rw [idx, Finset.mem_product] at ha
304 obtain ⟨hy, -⟩ := ha
305 rw [InterfaceComponentBound.Diamond.mem_ball_iff] at hy
306 rw [InterfaceComponentBound.Octahedron.mem_ball_iff]
307 omega
308
309/-- The neighbour cell `(±1, y, z)` of an index lies in the ball (since `|y| + |z| ≤ t - 1`). -/
310theorem memNbr (t : ℕ) (ht : 1 ≤ t) (a : (ℤ × ℤ) × Bool × Bool) (ha : a ∈ idx t) :
311 (((if a.2.1 then (1 : ℤ) else -1)), a.1) ∈ ball t := by
312 rw [idx, Finset.mem_product] at ha
313 obtain ⟨hy, -⟩ := ha
314 rw [InterfaceComponentBound.Diamond.mem_ball_iff] at hy
315 rw [InterfaceComponentBound.Octahedron.mem_ball_iff]
316 split <;> · simp only [Int.natAbs_one, Int.natAbs_neg]; omega
317
318/-- The index data of a bichromatic 3-D edge: `(spine (y,z), side of the ±1 neighbour, orientation)`. -/
319def edgeIndex (t : ℕ) (p : Vtx t × Vtx t) : (ℤ × ℤ) × Bool × Bool :=
320 if p.1.val.1 = 0 then (p.1.val.2, decide (0 < p.2.val.1), true)
321 else (p.2.val.2, decide (0 < p.1.val.1), false)
322
323/-- The bichromatic 3-D edge reconstructed from its index data. -/
324def edgeFromIndex (t : ℕ) (ht : 1 ≤ t) (a : (ℤ × ℤ) × Bool × Bool) (ha : a ∈ idx t) :
325 Vtx t × Vtx t :=
326 if a.2.2 then
327 (⟨((0 : ℤ), a.1), memSpine t a ha⟩, ⟨((if a.2.1 then (1 : ℤ) else -1), a.1), memNbr t ht a ha⟩)
328 else
329 (⟨((if a.2.1 then (1 : ℤ) else -1), a.1), memNbr t ht a ha⟩, ⟨((0 : ℤ), a.1), memSpine t a ha⟩)
330
331/-- **The exact 3-D interface edge count is `8t² - 8t + 4`** (ordered edges). The bichromatic edge set
332is in bijection with `{interior spine (y,z)} × {side, orientation}`: every bichromatic edge has one
333spine endpoint `(0, y, z)` and one neighbour `(±1, y, z)` sharing `(y, z)`, so the edge is fully
334determined by `(y, z, side, orientation)` with `|y| + |z| ≤ t - 1`. The interior spine is a 2-D
335diamond, so the count is `4 ·` its area law `2(t-1)² + 2(t-1) + 1 = 2t² - 2t + 1`. -/
336theorem interface_card_eq (t : ℕ) (ht : 1 ≤ t) : (B t).card = 8 * t ^ 2 - 8 * t + 4 := by
337 rw [← idx_card t ht]
338 refine Finset.card_bij' (fun p _ => edgeIndex t p) (fun a ha => edgeFromIndex t ht a ha) ?_ ?_ ?_ ?_
339 · -- hi : edgeIndex maps B into idx
340 rintro ⟨a, b⟩ hp
341 simp only [B, Finset.mem_filter, Finset.mem_univ, true_and] at hp
342 obtain ⟨hadj, hpol⟩ := hp
343 show edgeIndex t (a, b) ∈ idx t
344 rcases edge_structure t a b hadj hpol with ⟨h0, hbpm, hy1, hy2⟩ | ⟨h0, hapm, hy1, hy2⟩
345 · dsimp only [edgeIndex]
346 rw [if_pos h0, idx]
347 have key : b.val.2.1.natAbs + b.val.2.2.natAbs ≤ t - 1 := by
348 have hb : b.val.1.natAbs + b.val.2.1.natAbs + b.val.2.2.natAbs ≤ t := by
349 have hmem := b.property
350 rwa [InterfaceComponentBound.Octahedron.mem_ball_iff] at hmem
351 have h1 : b.val.1.natAbs = 1 := by rcases hbpm with hb1 | hb1 <;> rw [hb1] <;> decide
352 omega
353 have hbnd : a.val.2 ∈ InterfaceComponentBound.Diamond.ball (t - 1) := by
354 rw [InterfaceComponentBound.Diamond.mem_ball_iff, hy1, hy2]
355 omega
356 exact Finset.mem_product.mpr ⟨hbnd, Finset.mem_univ _⟩
357 · have hne : ¬ (a.val.1 = 0) := by rcases hapm with h | h <;> omega
358 dsimp only [edgeIndex]
359 rw [if_neg hne, idx]
360 have key : a.val.2.1.natAbs + a.val.2.2.natAbs ≤ t - 1 := by
361 have ha : a.val.1.natAbs + a.val.2.1.natAbs + a.val.2.2.natAbs ≤ t := by
362 have hmem := a.property
363 rwa [InterfaceComponentBound.Octahedron.mem_ball_iff] at hmem
364 have h1 : a.val.1.natAbs = 1 := by rcases hapm with ha1 | ha1 <;> rw [ha1] <;> decide
365 omega
366 have hbnd : b.val.2 ∈ InterfaceComponentBound.Diamond.ball (t - 1) := by
367 rw [InterfaceComponentBound.Diamond.mem_ball_iff, ← hy1, ← hy2]
368 omega
369 exact Finset.mem_product.mpr ⟨hbnd, Finset.mem_univ _⟩
370 · -- hj : edgeFromIndex maps idx into B
371 rintro a ha
372 show edgeFromIndex t ht a ha ∈ B t
373 simp only [B, Finset.mem_filter, Finset.mem_univ, true_and]
374 unfold edgeFromIndex
375 split
376 · refine ⟨?_, ?_⟩
377 · unfold adj; dsimp only; split <;> omega
378 · simp only [polarized]; dsimp only; split_ifs <;> omega
379 · refine ⟨?_, ?_⟩
380 · unfold adj; dsimp only; split <;> omega
381 · simp only [polarized]; dsimp only; split_ifs <;> omega
382 · -- left_inv : edgeFromIndex (edgeIndex p) = p
383 rintro ⟨a, b⟩ hp
384 simp only [B, Finset.mem_filter, Finset.mem_univ, true_and] at hp
385 obtain ⟨hadj, hpol⟩ := hp
386 rcases edge_structure t a b hadj hpol with ⟨h0, hbpm, hy1, hy2⟩ | ⟨h0, hapm, hy1, hy2⟩
387 · apply Prod.ext
388 · apply Subtype.ext
389 simp only [edgeIndex, edgeFromIndex, h0, if_true]
390 rw [Prod.ext_iff]
391 exact ⟨h0.symm, rfl⟩
392 · apply Subtype.ext
393 simp only [edgeIndex, edgeFromIndex, h0, if_true]
394 rw [Prod.ext_iff]
395 refine ⟨?_, Prod.ext_iff.mpr ⟨hy1, hy2⟩⟩
396 rcases hbpm with hb1 | hb1 <;> simp [hb1]
397 · have hne : ¬ (a.val.1 = 0) := by rcases hapm with h | h <;> omega
398 apply Prod.ext
399 · apply Subtype.ext
400 simp only [edgeIndex, edgeFromIndex, if_neg hne]
401 rw [Prod.ext_iff]
402 refine ⟨?_, Prod.ext_iff.mpr ⟨hy1.symm, hy2.symm⟩⟩
403 rcases hapm with ha1 | ha1 <;> simp [ha1]
404 · apply Subtype.ext
405 simp only [edgeIndex, edgeFromIndex, if_neg hne]
406 rw [Prod.ext_iff]
407 exact ⟨h0.symm, rfl⟩
408 · -- right_inv : edgeIndex (edgeFromIndex a) = a
409 rintro a ha
410 obtain ⟨yz, side, orient⟩ := a
411 show edgeIndex t (edgeFromIndex t ht (yz, side, orient) ha) = (yz, side, orient)
412 cases orient <;> cases side <;>
413 simp [edgeFromIndex, edgeIndex]
414
415/-- **The concrete 3-D interface edge-list length is `8t² - 8t + 4`.** -/
416theorem interface_length_eq (t : ℕ) (ht : 1 ≤ t) :
417 ((edges t).filter (fun p => decide (polarized t p.1 ≠ polarized t p.2))).length
418 = 8 * t ^ 2 - 8 * t + 4 := by
419 rw [interface_length_eq_card, interface_card_eq t ht]
420
421/-- **Linear per-cycle recognition activity (3-D).** Advancing the octahedron birth field by one
422cadence cycle (`t → t + 1`) adds exactly `16t` ordered interface edges. Unlike the 2-D case (where the
423increment is the constant `8`), in three dimensions the forced recognition activity per cycle grows
424`Θ(t)`: the interface is a 2-D surface whose area grows linearly per shell. This is the honest 3-D
425form of the compute-watch law: cost per cycle still tracks recognition activity, but in D = 3 that
426activity is `Θ(t)`, not `O(1)`, because the recognition-active interface is a growing codim-1 disk. -/
427theorem interface_increment_linear (t : ℕ) (ht : 1 ≤ t) :
428 (B (t + 1)).card - (B t).card = 16 * t := by
429 rw [interface_card_eq (t + 1) (by omega), interface_card_eq t ht]
430 have e : (t + 1) ^ 2 = t ^ 2 + 2 * t + 1 := by ring
431 have hsq : t ≤ t ^ 2 := by nlinarith [ht]
432 rw [e]
433 omega
434
435/-- **Total interface growth over a forward run (3-D).** The net number of interface edges the
436polarized octahedron birth introduces over a full run from radius `1` to radius `T` is exactly
437`8T² - 8T = 8T(T-1)`, the difference of the start and end interface sizes. This is `Θ(T²)`,
438sub-extensive against the brute-force spacetime cost `Θ(T⁴)` (volume `Θ(T³)` times `T` cycles): the
4393-D compute-watch total. A full forward run to radius `T` posts `Θ(T²)` net forced distinctions, not
440the `Θ(T⁴)` a volume-times-ticks accounting would charge. -/
441theorem interface_total_growth (T : ℕ) (hT : 1 ≤ T) :
442 (B T).card - (B 1).card = 8 * T ^ 2 - 8 * T := by
443 rw [interface_card_eq T hT, interface_card_eq 1 (le_refl 1)]
444 simp only [one_pow, mul_one]
445 have hsq : T ≤ T ^ 2 := by nlinarith [hT]
446 omega
447
448end Octahedron
449
450end PolarizedBirthInterface
451end Cosmology
452end IndisputableMonolith
453