IndisputableMonolith.Cosmology.PolarizedBirthInterfaceCost
IndisputableMonolith/Cosmology/PolarizedBirthInterfaceCost.lean · 367 lines · 22 declarations
show as:
view math explainer →
1import Mathlib
2import IndisputableMonolith.Cosmology.LatticeBallEdges
3import IndisputableMonolith.Cost
4import IndisputableMonolith.Constants
5
6/-!
7# The recognition COST of the coarsening ledger: carried bulk is free, the interface is paid
8
9`LatticeBallEdges` (Phase 54) closed the edge-*count* ledger: every adjacency of the polarized birth
10field is either a carried monochromatic edge or a forced bichromatic interface edge, and it counted
11each side exactly (`total = interface + carried`). This module weights that ledger by the actual
12recognition cost the engine posts, the forced cost `J(x) = (x + x⁻¹)/2 - 1` (`Cost.Jcost`, unique by
13`Cost.FunctionalEquation`) evaluated at the phi-rung gap between two cells' charges.
14
15The charge of the polarized field is `sign(x) ∈ {+1, 0, -1}` (`PolarizedBirthDomains.polarized`), and
16the cost of one ordered adjacency is `J(φ^(charge p - charge q))`. Two facts pin it down:
17
18* a **carried** (monochromatic) edge has equal charges, so it spans `0` phi-rungs and costs
19 `J(φ^0) = J(1) = 0` exactly (`Cost.Jcost_unit0`). The bulk is carried for *literally zero*
20 recognition cost.
21* an **interface** (bichromatic) edge has one endpoint on the `x = 0` spine and the other at
22 `x = ±1` (`edge_structure`), so the charges differ by exactly `±1`: it spans one phi-rung and costs
23 `J(φ^(±1)) = J(φ)` exactly (`Cost.Jcost_symm`, reciprocal symmetry).
24
25So the entire recognition cost of the field is the interface count times `J(φ)`:
26
27* 2D diamond: `totalCost t = (8t - 4) • J(φ)`, `carriedCost t = 0` (`Diamond`).
28* 3D octahedron: `totalCost t = (8t² - 8t + 4) • J(φ)`, `carriedCost t = 0` (`Octahedron`).
29
30with `J(φ) = (√5 - 2)/2 > 0` (`Jcost_phi_pos`), a genuine positive cost. This is the literal,
31cost-unit statement of the north star's compute-watch law: cost scales with the recognition activity
32(the codimension-1 interface), not with the bulk volume the engine carries coarse for free.
33
34THEOREM over `ℝ` and `ℕ` with 0 `sorry` and only the three standard axioms (`propext`,
35`Classical.choice`, `Quot.sound`).
36-/
37
38namespace IndisputableMonolith
39namespace Cosmology
40namespace PolarizedBirthInterfaceCost
41
42open Finset
43open scoped BigOperators
44
45/-! ## §0. The phi-rung cost, shared by both dimensions -/
46
47/-- The recognition cost of an ordered adjacency whose two cells' charges differ by `d` phi-rungs:
48`J(φ^d)`. The forced cost `J` is `Cost.Jcost`; `φ` is the forced golden ratio `Constants.phi`. -/
49noncomputable def Jpow (d : ℤ) : ℝ := Cost.Jcost (Constants.phi ^ d)
50
51/-- A zero-rung gap (a carried, monochromatic edge) costs nothing: `J(φ^0) = J(1) = 0`. -/
52lemma Jpow_zero : Jpow 0 = 0 := by
53 rw [Jpow, zpow_zero, Cost.Jcost_unit0]
54
55/-- A one-rung-up gap costs `J(φ)`. -/
56lemma Jpow_one : Jpow 1 = Cost.Jcost Constants.phi := by
57 rw [Jpow, zpow_one]
58
59/-- A one-rung-down gap costs `J(φ)` too, by reciprocal symmetry `J(φ⁻¹) = J(φ)`. -/
60lemma Jpow_neg_one : Jpow (-1) = Cost.Jcost Constants.phi := by
61 have h : Constants.phi ^ (-1 : ℤ) = Constants.phi⁻¹ := by
62 rw [zpow_neg, zpow_one]
63 rw [Jpow, h, ← Cost.Jcost_symm Constants.phi_pos]
64
65/-- Either a single rung up or a single rung down costs exactly `J(φ)`: the recognition cost of a
66forced interface distinction. -/
67lemma Jpow_of_abs_one {d : ℤ} (h : d = 1 ∨ d = -1) : Jpow d = Cost.Jcost Constants.phi := by
68 rcases h with h | h <;> subst h
69 · exact Jpow_one
70 · exact Jpow_neg_one
71
72/-- `J(φ) > 0`: a forced interface distinction has a genuine, strictly positive recognition cost.
73`J(φ) = (φ - 1)²/(2φ) = (√5 - 2)/2`. -/
74lemma Jcost_phi_pos : 0 < Cost.Jcost Constants.phi := by
75 rw [Cost.Jcost_eq_sq Constants.phi_ne_zero]
76 apply div_pos
77 · have hne : Constants.phi - 1 ≠ 0 := sub_ne_zero.mpr Constants.phi_ne_one
78 positivity
79 · have := Constants.phi_pos; linarith
80
81/-! ## §1. The 2D diamond cost ledger -/
82
83namespace Diamond
84
85open InterfaceComponentBound.Diamond
86open PolarizedBirthDomains.Diamond (polarized)
87open PolarizedBirthInterface.Diamond (B interface_card_eq)
88open LatticeBallEdges.Diamond (E carried)
89
90/-- **The level gap across a bichromatic edge is exactly `±1`.** Adjacent cells of different charge
91have one endpoint on the `x = 0` spine (charge `0`) and the other at `x = ±1` (charge `±1`), because
92a unit step changes `x` by at most one and so cannot cross from `+1` to `-1`. Hence the charge
93difference is `+1` or `-1`. -/
94theorem level_diff (t : ℕ) (a b : Vtx t) (hadj : adj a.val b.val)
95 (hpol : polarized t a ≠ polarized t b) :
96 polarized t a - polarized t b = 1 ∨ polarized t a - polarized t b = -1 := by
97 unfold adj at hadj
98 simp only [polarized] at hpol ⊢
99 split_ifs at hpol ⊢ <;> omega
100
101/-- The recognition cost the engine posts across one ordered adjacency of the polarized diamond:
102`J` at the phi-rung gap between the two cells' charges. -/
103noncomputable def edgeCost (t : ℕ) (p : Vtx t × Vtx t) : ℝ :=
104 Jpow (polarized t p.1 - polarized t p.2)
105
106/-- A carried (monochromatic) edge costs exactly `0`: equal charges span no phi-rung. -/
107theorem edgeCost_carried_zero (t : ℕ) (p : Vtx t × Vtx t) (hp : p ∈ carried t) :
108 edgeCost t p = 0 := by
109 rw [carried, Finset.mem_filter] at hp
110 have hd : polarized t p.1 - polarized t p.2 = 0 := sub_eq_zero.mpr hp.2
111 rw [edgeCost, hd, Jpow_zero]
112
113/-- A forced interface (bichromatic) edge costs exactly `J(φ)`: its charges differ by one phi-rung. -/
114theorem edgeCost_interface (t : ℕ) (p : Vtx t × Vtx t) (hp : p ∈ B t) :
115 edgeCost t p = Cost.Jcost Constants.phi := by
116 simp only [B, Finset.mem_filter, Finset.mem_univ, true_and] at hp
117 obtain ⟨hadj, hpol⟩ := hp
118 simp only [edgeCost]
119 exact Jpow_of_abs_one (level_diff t p.1 p.2 hadj hpol)
120
121/-- The total interface recognition cost: the sum of `edgeCost` over the bichromatic edges. -/
122noncomputable def interfaceCost (t : ℕ) : ℝ := ∑ p ∈ B t, edgeCost t p
123
124/-- The total carried recognition cost: the sum of `edgeCost` over the monochromatic edges. -/
125noncomputable def carriedCost (t : ℕ) : ℝ := ∑ p ∈ carried t, edgeCost t p
126
127/-- The total recognition cost of the field: the sum of `edgeCost` over every adjacency. -/
128noncomputable def totalCost (t : ℕ) : ℝ := ∑ p ∈ E t, edgeCost t p
129
130/-- **Carried cost is exactly zero.** The whole bulk the engine carries coarse costs no recognition. -/
131theorem carriedCost_eq_zero (t : ℕ) : carriedCost t = 0 := by
132 simp only [carriedCost]
133 apply Finset.sum_eq_zero
134 intro p hp
135 exact edgeCost_carried_zero t p hp
136
137/-- The interface cost is the interface edge count times `J(φ)`. -/
138theorem interfaceCost_eq_card (t : ℕ) :
139 interfaceCost t = (B t).card • Cost.Jcost Constants.phi := by
140 simp only [interfaceCost]
141 rw [Finset.sum_congr rfl (fun p hp => edgeCost_interface t p hp), Finset.sum_const]
142
143/-- **The total cost equals the interface cost**, because the carried bulk contributes nothing. -/
144theorem totalCost_eq_interfaceCost (t : ℕ) : totalCost t = interfaceCost t := by
145 have hsplit := Finset.sum_filter_add_sum_filter_not (E t)
146 (fun p => polarized t p.1 ≠ polarized t p.2) (edgeCost t)
147 have hBeq : (E t).filter (fun p => polarized t p.1 ≠ polarized t p.2) = B t := by
148 rw [E, B, Finset.filter_filter]
149 have hMeq : (E t).filter (fun p => ¬ (polarized t p.1 ≠ polarized t p.2)) = carried t := by
150 rw [carried]
151 apply Finset.filter_congr
152 intro p _
153 simp
154 rw [hBeq, hMeq] at hsplit
155 have hzero : ∑ p ∈ carried t, edgeCost t p = 0 := by
156 apply Finset.sum_eq_zero
157 intro p hp
158 exact edgeCost_carried_zero t p hp
159 rw [hzero, add_zero] at hsplit
160 simp only [totalCost, interfaceCost]
161 exact hsplit.symm
162
163/-- **The exact interface recognition cost is `(8t - 4) • J(φ)`** (`t ≥ 1`). -/
164theorem interfaceCost_card (t : ℕ) (ht : 1 ≤ t) :
165 interfaceCost t = (8 * t - 4) • Cost.Jcost Constants.phi := by
166 rw [interfaceCost_eq_card, interface_card_eq t ht]
167
168/-- **The total recognition cost of the polarized diamond field is `(8t - 4) • J(φ)`** (`t ≥ 1`):
169the carried bulk is free, and the whole cost sits on the `8t - 4` interface edges. -/
170theorem totalCost_card (t : ℕ) (ht : 1 ≤ t) :
171 totalCost t = (8 * t - 4) • Cost.Jcost Constants.phi := by
172 rw [totalCost_eq_interfaceCost, interfaceCost_card t ht]
173
174/-- The total cost in real-multiplication form, `(8t - 4) * J(φ)` (`t ≥ 1`). -/
175theorem totalCost_mul (t : ℕ) (ht : 1 ≤ t) :
176 totalCost t = ((8 * t - 4 : ℕ) : ℝ) * Cost.Jcost Constants.phi := by
177 rw [totalCost_card t ht, nsmul_eq_mul]
178
179/-- **The run-total recognition cost over a full forward run** from radius `1` to `T` is exactly
180`8(T - 1) • J(φ)`. The cost the engine posts to grow the whole world is `Θ(T)`, strictly
181sub-extensive against the brute-force volume-times-ticks `Θ(T³)`: the compute-watch law in cost
182units, integrated over the run. -/
183theorem runCost_growth (T : ℕ) (hT : 1 ≤ T) :
184 totalCost T - totalCost 1 = ((8 * T - 8 : ℕ) : ℝ) * Cost.Jcost Constants.phi := by
185 rw [totalCost_mul T hT, totalCost_mul 1 le_rfl]
186 have h4 : 4 ≤ 8 * T := by omega
187 have h8 : 8 ≤ 8 * T := by omega
188 have e1 : ((8 * T - 4 : ℕ) : ℝ) = 8 * (T : ℝ) - 4 := by
189 rw [Nat.cast_sub h4]; push_cast; ring
190 have e2 : ((8 * 1 - 4 : ℕ) : ℝ) = 4 := by norm_num
191 have e3 : ((8 * T - 8 : ℕ) : ℝ) = 8 * (T : ℝ) - 8 := by
192 rw [Nat.cast_sub h8]; push_cast; ring
193 rw [e1, e2, e3]; ring
194
195/-- **The per-cycle recognition cost increment** of advancing the diamond by one cadence cycle
196(`t → t+1`) is the constant `8 • J(φ)` (`t ≥ 1`): the differential form of the compute-watch law.
197In 2D the recognition-active interface is a `1`-dimensional curve whose length gains a constant `8`
198ordered edges per shell, so the cost the engine posts each cycle is constant, `O(1)`, independent of
199how large the world already is. -/
200theorem costIncrement (t : ℕ) (ht : 1 ≤ t) :
201 totalCost (t + 1) - totalCost t = 8 * Cost.Jcost Constants.phi := by
202 rw [totalCost_mul (t + 1) (by omega), totalCost_mul t ht]
203 have e1 : ((8 * (t + 1) - 4 : ℕ) : ℝ) = 8 * (t : ℝ) + 4 := by
204 rw [Nat.cast_sub (by omega)]; push_cast; ring
205 have e2 : ((8 * t - 4 : ℕ) : ℝ) = 8 * (t : ℝ) - 4 := by
206 rw [Nat.cast_sub (by omega)]; push_cast; ring
207 rw [e1, e2]; ring
208
209/-- **2D headline (Phase 55).** For a polarized diamond of radius `t ≥ 1`: the carried bulk costs
210exactly zero recognition, the total cost is `(8t - 4) • J(φ)` (the interface count times the
211one-rung cost), and `J(φ) > 0` is a genuine positive cost. "Carry the bulk free, pay only for the
212interface," in exact cost units. -/
213theorem t55_cost_ledger (t : ℕ) (ht : 1 ≤ t) :
214 carriedCost t = 0
215 ∧ totalCost t = (8 * t - 4) • Cost.Jcost Constants.phi
216 ∧ totalCost t = interfaceCost t
217 ∧ 0 < Cost.Jcost Constants.phi :=
218 ⟨carriedCost_eq_zero t, totalCost_card t ht, totalCost_eq_interfaceCost t, Jcost_phi_pos⟩
219
220end Diamond
221
222/-! ## §2. The 3D octahedron cost ledger -/
223
224namespace Octahedron
225
226open InterfaceComponentBound.Octahedron
227open PolarizedBirthDomains.Octahedron (polarized)
228open PolarizedBirthInterface.Octahedron (B interface_card_eq)
229open LatticeBallEdges.Octahedron (E carried)
230
231/-- **The level gap across a bichromatic edge is exactly `±1`** (3D). Same argument as 2D: a unit
2326-neighbour step changes `x` by at most one, so the only way two adjacent cells differ in charge is
233one on the spine `x = 0` and one at `x = ±1`. -/
234theorem level_diff (t : ℕ) (a b : Vtx t) (hadj : adj a.val b.val)
235 (hpol : polarized t a ≠ polarized t b) :
236 polarized t a - polarized t b = 1 ∨ polarized t a - polarized t b = -1 := by
237 unfold adj at hadj
238 simp only [polarized] at hpol ⊢
239 split_ifs at hpol ⊢ <;> omega
240
241/-- The recognition cost of one ordered adjacency of the polarized octahedron. -/
242noncomputable def edgeCost (t : ℕ) (p : Vtx t × Vtx t) : ℝ :=
243 Jpow (polarized t p.1 - polarized t p.2)
244
245/-- A carried (monochromatic) octahedron edge costs exactly `0`. -/
246theorem edgeCost_carried_zero (t : ℕ) (p : Vtx t × Vtx t) (hp : p ∈ carried t) :
247 edgeCost t p = 0 := by
248 rw [carried, Finset.mem_filter] at hp
249 have hd : polarized t p.1 - polarized t p.2 = 0 := sub_eq_zero.mpr hp.2
250 rw [edgeCost, hd, Jpow_zero]
251
252/-- A forced interface (bichromatic) octahedron edge costs exactly `J(φ)`. -/
253theorem edgeCost_interface (t : ℕ) (p : Vtx t × Vtx t) (hp : p ∈ B t) :
254 edgeCost t p = Cost.Jcost Constants.phi := by
255 simp only [B, Finset.mem_filter, Finset.mem_univ, true_and] at hp
256 obtain ⟨hadj, hpol⟩ := hp
257 simp only [edgeCost]
258 exact Jpow_of_abs_one (level_diff t p.1 p.2 hadj hpol)
259
260/-- The total interface recognition cost (3D). -/
261noncomputable def interfaceCost (t : ℕ) : ℝ := ∑ p ∈ B t, edgeCost t p
262
263/-- The total carried recognition cost (3D). -/
264noncomputable def carriedCost (t : ℕ) : ℝ := ∑ p ∈ carried t, edgeCost t p
265
266/-- The total recognition cost of the octahedron field (3D). -/
267noncomputable def totalCost (t : ℕ) : ℝ := ∑ p ∈ E t, edgeCost t p
268
269/-- **Carried cost is exactly zero** (3D). -/
270theorem carriedCost_eq_zero (t : ℕ) : carriedCost t = 0 := by
271 simp only [carriedCost]
272 apply Finset.sum_eq_zero
273 intro p hp
274 exact edgeCost_carried_zero t p hp
275
276/-- The interface cost is the interface edge count times `J(φ)` (3D). -/
277theorem interfaceCost_eq_card (t : ℕ) :
278 interfaceCost t = (B t).card • Cost.Jcost Constants.phi := by
279 simp only [interfaceCost]
280 rw [Finset.sum_congr rfl (fun p hp => edgeCost_interface t p hp), Finset.sum_const]
281
282/-- **The total cost equals the interface cost** (3D). -/
283theorem totalCost_eq_interfaceCost (t : ℕ) : totalCost t = interfaceCost t := by
284 have hsplit := Finset.sum_filter_add_sum_filter_not (E t)
285 (fun p => polarized t p.1 ≠ polarized t p.2) (edgeCost t)
286 have hBeq : (E t).filter (fun p => polarized t p.1 ≠ polarized t p.2) = B t := by
287 rw [E, B, Finset.filter_filter]
288 have hMeq : (E t).filter (fun p => ¬ (polarized t p.1 ≠ polarized t p.2)) = carried t := by
289 rw [carried]
290 apply Finset.filter_congr
291 intro p _
292 simp
293 rw [hBeq, hMeq] at hsplit
294 have hzero : ∑ p ∈ carried t, edgeCost t p = 0 := by
295 apply Finset.sum_eq_zero
296 intro p hp
297 exact edgeCost_carried_zero t p hp
298 rw [hzero, add_zero] at hsplit
299 simp only [totalCost, interfaceCost]
300 exact hsplit.symm
301
302/-- **The exact interface recognition cost is `(8t² - 8t + 4) • J(φ)`** (`t ≥ 1`). -/
303theorem interfaceCost_card (t : ℕ) (ht : 1 ≤ t) :
304 interfaceCost t = (8 * t ^ 2 - 8 * t + 4) • Cost.Jcost Constants.phi := by
305 rw [interfaceCost_eq_card, interface_card_eq t ht]
306
307/-- **The total recognition cost of the polarized octahedron field is `(8t² - 8t + 4) • J(φ)`**
308(`t ≥ 1`): the 3D bulk is carried free, the cost sits on the `8t² - 8t + 4` interface edges. -/
309theorem totalCost_card (t : ℕ) (ht : 1 ≤ t) :
310 totalCost t = (8 * t ^ 2 - 8 * t + 4) • Cost.Jcost Constants.phi := by
311 rw [totalCost_eq_interfaceCost, interfaceCost_card t ht]
312
313/-- The total cost in real-multiplication form, `(8t² - 8t + 4) * J(φ)` (`t ≥ 1`). -/
314theorem totalCost_mul (t : ℕ) (ht : 1 ≤ t) :
315 totalCost t = ((8 * t ^ 2 - 8 * t + 4 : ℕ) : ℝ) * Cost.Jcost Constants.phi := by
316 rw [totalCost_card t ht, nsmul_eq_mul]
317
318/-- **The run-total recognition cost over a full forward run** from radius `1` to `T` is exactly
319`8T(T - 1) • J(φ)`. In the dimension `T8` forces (D=3) the cost the engine posts to grow the whole
320world is `Θ(T²)`, strictly sub-extensive against the brute-force `Θ(T⁴)`: the compute-watch law in
321cost units, integrated over the run. -/
322theorem runCost_growth (T : ℕ) (hT : 1 ≤ T) :
323 totalCost T - totalCost 1 = ((8 * T ^ 2 - 8 * T : ℕ) : ℝ) * Cost.Jcost Constants.phi := by
324 rw [totalCost_mul T hT, totalCost_mul 1 le_rfl]
325 have hTT : 8 * T ≤ 8 * T ^ 2 := by nlinarith [hT]
326 have e1 : ((8 * T ^ 2 - 8 * T + 4 : ℕ) : ℝ) = 8 * (T : ℝ) ^ 2 - 8 * (T : ℝ) + 4 := by
327 rw [Nat.cast_add, Nat.cast_sub hTT]; push_cast; ring
328 have e2 : ((8 * 1 ^ 2 - 8 * 1 + 4 : ℕ) : ℝ) = 4 := by norm_num
329 have e3 : ((8 * T ^ 2 - 8 * T : ℕ) : ℝ) = 8 * (T : ℝ) ^ 2 - 8 * (T : ℝ) := by
330 rw [Nat.cast_sub hTT]; push_cast; ring
331 rw [e1, e2, e3]; ring
332
333/-- **The per-cycle recognition cost increment** of advancing the octahedron by one cadence cycle
334(`t → t+1`) is `16t • J(φ)` (`t ≥ 1`): the differential form of the compute-watch law in the
335dimension `T8` forces (D=3). The recognition-active interface is now a `2`-dimensional surface whose
336area gains `16t` ordered edges per shell, so the cost the engine posts each cycle grows `Θ(t)`, the
337honest 3D statement (not the constant `O(1)` of 2D), still strictly sub-extensive in the `Θ(t³)`
338bulk. -/
339theorem costIncrement (t : ℕ) (ht : 1 ≤ t) :
340 totalCost (t + 1) - totalCost t = (16 * t : ℝ) * Cost.Jcost Constants.phi := by
341 rw [totalCost_mul (t + 1) (by omega), totalCost_mul t ht]
342 have hle1 : 8 * (t + 1) ≤ 8 * (t + 1) ^ 2 := by nlinarith [Nat.le_add_left 1 t]
343 have hle2 : 8 * t ≤ 8 * t ^ 2 := by nlinarith [ht]
344 have e1 : ((8 * (t + 1) ^ 2 - 8 * (t + 1) + 4 : ℕ) : ℝ)
345 = 8 * (t : ℝ) ^ 2 + 8 * (t : ℝ) + 4 := by
346 rw [Nat.cast_add, Nat.cast_sub hle1]; push_cast; ring
347 have e2 : ((8 * t ^ 2 - 8 * t + 4 : ℕ) : ℝ) = 8 * (t : ℝ) ^ 2 - 8 * (t : ℝ) + 4 := by
348 rw [Nat.cast_add, Nat.cast_sub hle2]; push_cast; ring
349 rw [e1, e2]; ring
350
351/-- **3D headline (Phase 55).** For a polarized octahedron of radius `t ≥ 1`: the carried bulk costs
352exactly zero recognition, the total cost is `(8t² - 8t + 4) • J(φ)` (the interface count times the
353one-rung cost), and `J(φ) > 0`. The dimension `T8` forces (D=3) version of "carry the bulk free, pay
354only for the interface." -/
355theorem t55_cost_ledger (t : ℕ) (ht : 1 ≤ t) :
356 carriedCost t = 0
357 ∧ totalCost t = (8 * t ^ 2 - 8 * t + 4) • Cost.Jcost Constants.phi
358 ∧ totalCost t = interfaceCost t
359 ∧ 0 < Cost.Jcost Constants.phi :=
360 ⟨carriedCost_eq_zero t, totalCost_card t ht, totalCost_eq_interfaceCost t, Jcost_phi_pos⟩
361
362end Octahedron
363
364end PolarizedBirthInterfaceCost
365end Cosmology
366end IndisputableMonolith
367