IndisputableMonolith.Gravity.WeakFieldConformalRegge
IndisputableMonolith/Gravity/WeakFieldConformalRegge.lean · 761 lines · 40 declarations
show as:
view math explainer →
1import Mathlib.Data.Real.Basic
2import Mathlib.Algebra.BigOperators.Group.Finset.Basic
3import Mathlib.Analysis.SpecialFunctions.Exp
4import Mathlib.Analysis.SpecialFunctions.Log.Basic
5import IndisputableMonolith.Constants
6import IndisputableMonolith.Geometry.Schlaefli
7import IndisputableMonolith.Foundation.SimplicialLedger.ContinuumBridge
8import IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi
9
10/-!
11# Weak-Field Conformal Reduction of the Regge Action
12
13This module proves the algebraic core of the reduction Jon is moving into
14Regge's notation in the gravity paper:
15
16 (a) Regge action S = (1/κ) · Σ_h A_h · δ_h
17 (b) Conformal edge ansatz ℓ_{ij} = ℓ_0 · exp((ξ_i + ξ_j)/2)
18 (c) Weak-field expansion expand to second order in ξ
19 (d) Reduction S^(2) = (1/κ) · Σ_⟨i,j⟩ ½ · (ξ_i − ξ_j)² · A_{ij}
20
21Piran–Williams (1986) handle a more general perturbation that does not
22single out the conformal mode. The reduction here picks the conformal
23sector and proves the finite-dimensional algebra that turns a symmetric
24zero-row-sum second-variation matrix into the Dirichlet form on
25differences `(ξ_i − ξ_j)²`. The remaining geometric task is to compute
26the Regge second-variation coefficients from Cayley–Menger/dihedral
27formulas (or an equivalent Piran–Williams specialization) and verify the
28row-sum condition for the chosen lattice.
29
30## Layering
31
32The module is split into three independent algebraic claims plus one
33geometric hypothesis package:
34
35§1. *Conformal expansion (algebraic, fully proven).*
36 `ℓ_{ij}² / ℓ_0² = 1 + (ξ_i + ξ_j) + ½(ξ_i + ξ_j)² + remainder`
37 with the remainder named exactly as `exp(t) - 1 - t - t²/2`.
38
39§2. *Graph-Laplacian decomposition (algebraic, fully proven).*
40 For any symmetric matrix `M` on `Fin n × Fin n` with zero row sums,
41 `Σ_{i,j} M_{ij} ξ_i ξ_j = −½ Σ_{i,j} M_{ij} (ξ_i − ξ_j)²`.
42 This is the structural lemma that turns "Regge bilinear form" into
43 "Dirichlet form".
44
45§3. *Second-order Regge action coefficients (geometric input).*
46 We package the first-order area and deficit responses in a
47 `WeakFieldReggeData` structure and state the Schläfli/flat-mode
48 row-sum condition those coefficients must satisfy. This file does not
49 compute those coefficients from Cayley–Menger data.
50
51§4. *The reduction (composition).*
52 Combining §2 with the row-sum property, the packaged second-order
53 conformal Regge functional equals the discrete Dirichlet energy with
54 weights `A_{ij} = -M_{ij}`.
55
56Zero `sorry`, zero new `axiom`. The file is a conditional theorem: once
57the geometric coefficients and Schläfli row-sum are supplied, the
58Dirichlet reduction is formal.
59
60## References
61
62- Regge, T. (1961). *General relativity without coordinates.* Nuovo
63 Cim. 19, 558–571.
64- Piran, T. & Williams, R. M. (1986). *Three-plus-one formulation of
65 Regge calculus.* Phys. Rev. D 33, 1622–1633.
66- Roček, M. & Williams, R. M. (1981). *Quantum Regge calculus.* Phys.
67 Lett. B 104, 31–37. (linearized Regge action on a regular lattice)
68- Schläfli, L. (1858). *On the multiple integral ∫^n dx dy ··· dz.*
69- Hartle, J. B. & Sorkin, R. (1981). *Boundary terms in the action for
70 the Regge calculus.* Gen. Rel. Grav. 13, 541–549.
71-/
72
73namespace IndisputableMonolith
74namespace Gravity
75namespace WeakFieldConformalRegge
76
77open Constants Real Geometry.Schlaefli Geometry.DihedralAngle
78open Foundation.SimplicialLedger.ContinuumBridge
79open Foundation.SimplicialLedger.EdgeLengthFromPsi
80
81noncomputable section
82
83/-! ## §1. Conformal edge-length expansion
84
85The exact identity `ℓ_{ij}² = ℓ_0² · exp(ξ_i + ξ_j)` factors out the
86conformal field. We expose two clean forms:
87
88* `conformal_length_sq_exact`: the exact form (no expansion, no error).
89* `conformal_length_sq_taylor2`: the second-order Taylor decomposition
90 with an explicit remainder `R(ξ_i + ξ_j)`.
91
92Both are fully proven from the algebra of `Real.exp`. -/
93
94/-- The exact identity:
95 `ℓ_{ij}(ξ)² = ℓ_0² · exp(ξ_i + ξ_j)`. -/
96theorem conformal_length_sq_exact
97 {n : ℕ} (a : ℝ) (ha : 0 < a) (ε : LogPotential n) (i j : Fin n) :
98 (conformal_edge_length_field a ha ε).length i j ^ 2
99 = a ^ 2 * Real.exp (ε i + ε j) := by
100 unfold conformal_edge_length_field
101 simp only
102 have hexp : Real.exp ((ε i + ε j) / 2) ^ 2
103 = Real.exp (ε i + ε j) := by
104 rw [pow_two, ← Real.exp_add]
105 congr 1; ring
106 rw [mul_pow, hexp]
107
108/-- The Taylor expansion of `exp(t) − 1 − t − t²/2` is the third-order
109 remainder. We do *not* prove a quantitative bound here (Mathlib's
110 `Real.exp_taylor_lt` route is heavy); we just expose the algebraic
111 decomposition with the remainder named explicitly. -/
112def conformal_remainder (t : ℝ) : ℝ := Real.exp t - 1 - t - t ^ 2 / 2
113
114/-- The second-order conformal expansion. This is *exact* with the
115 remainder explicitly named: it is just the rearrangement of
116 `exp(t) = 1 + t + t²/2 + R(t)`. -/
117theorem conformal_length_sq_taylor2
118 {n : ℕ} (a : ℝ) (ha : 0 < a) (ε : LogPotential n) (i j : Fin n) :
119 (conformal_edge_length_field a ha ε).length i j ^ 2 / a ^ 2
120 = 1 + (ε i + ε j) + (ε i + ε j) ^ 2 / 2
121 + conformal_remainder (ε i + ε j) := by
122 have ha2 : (a : ℝ) ^ 2 ≠ 0 := pow_ne_zero 2 (ne_of_gt ha)
123 rw [conformal_length_sq_exact a ha ε i j]
124 unfold conformal_remainder
125 field_simp
126 ring
127
128/-- At the flat vacuum `ξ ≡ 0`, the conformal remainder vanishes. -/
129theorem conformal_remainder_zero : conformal_remainder 0 = 0 := by
130 unfold conformal_remainder
131 simp
132
133/-- The first- and second-order coefficients of `ℓ_{ij}² / ℓ_0²` in `ξ`.
134
135 First order: `δ¹(ℓ²/ℓ_0²) = ξ_i + ξ_j`.
136 Second order: `δ²(ℓ²/ℓ_0²) = (ξ_i + ξ_j)² / 2`.
137
138 These are the building blocks for §3. -/
139def edgeSqFirstOrder {n : ℕ} (ε : LogPotential n) (i j : Fin n) : ℝ :=
140 ε i + ε j
141
142def edgeSqSecondOrder {n : ℕ} (ε : LogPotential n) (i j : Fin n) : ℝ :=
143 (ε i + ε j) ^ 2 / 2
144
145/-- The conformal expansion writes `ℓ²/ℓ_0² − 1 − δ¹ − δ²` as the
146 remainder. This is a tautology after `conformal_length_sq_taylor2`
147 but it is the form that downstream "second-order action" reductions
148 need. -/
149theorem conformal_length_sq_decomposition
150 {n : ℕ} (a : ℝ) (ha : 0 < a) (ε : LogPotential n) (i j : Fin n) :
151 (conformal_edge_length_field a ha ε).length i j ^ 2 / a ^ 2
152 = 1 + edgeSqFirstOrder ε i j + edgeSqSecondOrder ε i j
153 + conformal_remainder (ε i + ε j) := by
154 unfold edgeSqFirstOrder edgeSqSecondOrder
155 exact conformal_length_sq_taylor2 a ha ε i j
156
157/-! ## §2. Graph-Laplacian decomposition
158
159The pure-algebraic identity that drives the reduction. If `M_{ij}` is
160symmetric with zero row sums, then `ξ ↦ Σ_{i,j} M_{ij} ξ_i ξ_j` is the
161discrete Dirichlet energy `−½ Σ_{i,j} M_{ij} (ξ_i − ξ_j)²`.
162
163This is the discrete analog of `∫ φ Δφ = −∫ |∇φ|²` (integration by parts
164on a closed manifold) and is what makes a "Regge bilinear form on edges"
165manifestly the same as a "Dirichlet form on vertices". -/
166
167/-- The Dirichlet form generated by a symmetric matrix `M` and a vertex
168 function `ξ`: `D[ξ; M] = ½ Σ_{i,j} M_{ij} (ξ_i − ξ_j)²`. -/
169def dirichletForm {n : ℕ} (M : Fin n → Fin n → ℝ) (ε : LogPotential n) : ℝ :=
170 (1 / 2) * ∑ i : Fin n, ∑ j : Fin n, M i j * (ε i - ε j) ^ 2
171
172/-- The bilinear form: `Q[ξ; M] = Σ_{i,j} M_{ij} ξ_i ξ_j`. -/
173def quadraticForm {n : ℕ} (M : Fin n → Fin n → ℝ) (ε : LogPotential n) : ℝ :=
174 ∑ i : Fin n, ∑ j : Fin n, M i j * ε i * ε j
175
176/-- Helper: pulling a constant out of a sum (right-multiplication form). -/
177private lemma sum_const_mul_right {n : ℕ} (f : Fin n → ℝ) (c : ℝ) :
178 ∑ j : Fin n, f j * c = (∑ j : Fin n, f j) * c := by
179 rw [← Finset.sum_mul]
180
181/-- Helper: pulling a constant out of an inner sum at `j` (when the inner
182 factor depends only on `i`). -/
183private lemma inner_sum_const {n : ℕ} (M : Fin n → Fin n → ℝ) (g : Fin n → ℝ) (i : Fin n) :
184 ∑ j : Fin n, M i j * g i = (∑ j : Fin n, M i j) * g i :=
185 sum_const_mul_right (fun j => M i j) (g i)
186
187/-- **GRAPH-LAPLACIAN DECOMPOSITION.**
188 For symmetric `M` with zero row sums,
189 `Q[ξ; M] = −D[ξ; M]`.
190
191 This is the algebraic core of the weak-field reduction. -/
192theorem dirichlet_eq_neg_quadratic
193 {n : ℕ} (M : Fin n → Fin n → ℝ)
194 (hsymm : ∀ i j, M i j = M j i)
195 (hrow : ∀ i, ∑ j : Fin n, M i j = 0)
196 (ε : LogPotential n) :
197 quadraticForm M ε = - dirichletForm M ε := by
198 unfold quadraticForm dirichletForm
199 -- Expand `(ε i − ε j)² = ε i² − 2 ε i ε j + ε j²` and sum.
200 have hkey : ∀ i j, M i j * (ε i - ε j) ^ 2
201 = M i j * (ε i) ^ 2 - 2 * (M i j * ε i * ε j)
202 + M i j * (ε j) ^ 2 := by
203 intro i j; ring
204 -- Sum the identity term-by-term.
205 have hsum : ∑ i : Fin n, ∑ j : Fin n, M i j * (ε i - ε j) ^ 2
206 = (∑ i : Fin n, ∑ j : Fin n, M i j * (ε i) ^ 2)
207 - 2 * (∑ i : Fin n, ∑ j : Fin n, M i j * ε i * ε j)
208 + (∑ i : Fin n, ∑ j : Fin n, M i j * (ε j) ^ 2) := by
209 have h1 : ∀ i, ∑ j : Fin n, M i j * (ε i - ε j) ^ 2
210 = ∑ j : Fin n, (M i j * (ε i) ^ 2 - 2 * (M i j * ε i * ε j)
211 + M i j * (ε j) ^ 2) := by
212 intro i; exact Finset.sum_congr rfl (fun j _ => hkey i j)
213 simp only [h1, Finset.sum_add_distrib, Finset.sum_sub_distrib]
214 have hpull : ∀ i, ∑ j : Fin n, 2 * (M i j * ε i * ε j)
215 = 2 * ∑ j : Fin n, M i j * ε i * ε j := by
216 intro i
217 exact (Finset.mul_sum _ _ _).symm
218 simp only [hpull, ← Finset.mul_sum]
219 -- Use the row-sum condition on the `ε i² · M i j` and `ε j² · M i j` pieces.
220 have hi2 : ∑ i : Fin n, ∑ j : Fin n, M i j * (ε i) ^ 2 = 0 := by
221 have hpull : ∀ i, ∑ j : Fin n, M i j * (ε i) ^ 2
222 = (∑ j : Fin n, M i j) * (ε i) ^ 2 := fun i =>
223 sum_const_mul_right (fun j => M i j) ((ε i) ^ 2)
224 simp only [hpull, hrow, zero_mul, Finset.sum_const_zero]
225 have hj2 : ∑ i : Fin n, ∑ j : Fin n, M i j * (ε j) ^ 2 = 0 := by
226 -- Swap order, then `hrow` (transposed via symmetry).
227 rw [Finset.sum_comm]
228 have hpull : ∀ j, ∑ i : Fin n, M i j * (ε j) ^ 2
229 = (∑ i : Fin n, M i j) * (ε j) ^ 2 := fun j =>
230 sum_const_mul_right (fun i => M i j) ((ε j) ^ 2)
231 have hrow' : ∀ j, ∑ i : Fin n, M i j = 0 := by
232 intro j
233 have heq : ∑ i : Fin n, M i j = ∑ i : Fin n, M j i :=
234 Finset.sum_congr rfl (fun i _ => hsymm i j)
235 rw [heq]; exact hrow j
236 simp only [hpull, hrow', zero_mul, Finset.sum_const_zero]
237 -- Plug back in.
238 rw [hsum, hi2, hj2]
239 ring
240
241/-- **CONSEQUENCE.** When `M` is symmetric with zero row sums, the
242 Dirichlet form is the natural positive expression of the bilinear:
243 `D[ξ; M] = − Q[ξ; M]`. -/
244theorem dirichlet_form_eq_neg_quadratic
245 {n : ℕ} (M : Fin n → Fin n → ℝ)
246 (hsymm : ∀ i j, M i j = M j i)
247 (hrow : ∀ i, ∑ j : Fin n, M i j = 0)
248 (ε : LogPotential n) :
249 dirichletForm M ε = - quadraticForm M ε := by
250 have h := dirichlet_eq_neg_quadratic M hsymm hrow ε
251 linarith
252
253/-! ## §3. Second-order Regge action under Schläfli
254
255We package the geometric coefficients (linearizations of `A_h` and
256`δ_h` in the conformal field `ξ`) as a structure, then prove that the
257second-order Regge action takes the bilinear form
258 `S^(2)[ξ] = Σ_h A_h^(1)[ξ] · δ_h^(1)[ξ]`
259which combined with the conformal flat-mode invariance and §2 gives
260the Dirichlet reduction.
261
262The structure isolates *exactly* the geometric data the paper relies
263on, separate from the algebra of §1 and §2. -/
264
265/-- The first-order linearization data of a flat-background Regge
266 configuration under conformal vertex perturbations.
267
268 Fields:
269 * `dArea i j` — coefficient of `(ξ_i + ξ_j)/2` in `A_h^(1)` for
270 the hinge attached to edge `⟨i,j⟩`. (Background
271 data: linear response of the hinge area to a
272 unit change in edge length.)
273 * `dDeficit i j` — coefficient of `(ξ_i + ξ_j)/2` in `δ_h^(1)` for
274 the same hinge. (Background data: linear
275 response of the deficit angle.)
276
277 The data is symmetric in `i, j` and lives on a finite vertex set
278 `Fin n`. -/
279structure WeakFieldReggeData (n : ℕ) where
280 dArea : Fin n → Fin n → ℝ
281 dDeficit : Fin n → Fin n → ℝ
282 dArea_symm : ∀ i j, dArea i j = dArea j i
283 dDeficit_symm : ∀ i j, dDeficit i j = dDeficit j i
284
285/-- The bilinear coefficient matrix induced by the linearization data:
286 `M_{ij} = dArea_{ij} · dDeficit_{ij}` (the entry-wise product
287 that appears in `S^(2) = Σ A^(1) δ^(1)` after the conformal
288 expansion).
289
290 This is symmetric because both factors are symmetric. -/
291def bilinearCoefficient {n : ℕ} (W : WeakFieldReggeData n)
292 (i j : Fin n) : ℝ :=
293 W.dArea i j * W.dDeficit i j
294
295theorem bilinearCoefficient_symm {n : ℕ} (W : WeakFieldReggeData n)
296 (i j : Fin n) :
297 bilinearCoefficient W i j = bilinearCoefficient W j i := by
298 unfold bilinearCoefficient
299 rw [W.dArea_symm i j, W.dDeficit_symm i j]
300
301/-- The *Schläfli-derived row-sum vanishing* property. On a flat
302 background, the deficit-angle linearization satisfies Schläfli's
303 identity, which forces the bilinear-coefficient matrix to have
304 zero row sums when contracted with the conformal mode.
305
306 Concretely: for each vertex `i`,
307 `Σ_j dArea_{ij} · dDeficit_{ij} = 0`.
308
309 This is the geometric content of "uniform `ξ ≡ c` produces no
310 curvature change" combined with Schläfli's identity. -/
311def SchlaefliRowSum {n : ℕ} (W : WeakFieldReggeData n) : Prop :=
312 ∀ i : Fin n, ∑ j : Fin n, bilinearCoefficient W i j = 0
313
314/-- The second-order Regge action functional in the conformal mode.
315 Plugging the conformal expansion of `ℓ²` into the linearized Regge
316 action and collecting the order-`ξ²` terms gives this bilinear:
317
318 S^(2)[ξ] = (1/4) · Σ_{i,j} (ξ_i + ξ_j)² · M_{ij}
319 = (1/4) · Σ_{i,j} (ξ_i² + 2 ξ_i ξ_j + ξ_j²) · M_{ij}.
320
321 The factor `1/4` comes from the `(ξ_i + ξ_j)/2` factors entering
322 twice (once from `A_h^(1)`, once from `δ_h^(1)`).
323
324 With the Schläfli row-sum property, the `ξ_i² + ξ_j²` parts
325 vanish on summation and the `2 ξ_i ξ_j` part rearranges via §2 into
326 the Dirichlet form on differences. -/
327def secondOrderReggeAction {n : ℕ} (W : WeakFieldReggeData n)
328 (ε : LogPotential n) : ℝ :=
329 (1 / 4) * ∑ i : Fin n, ∑ j : Fin n,
330 bilinearCoefficient W i j * (ε i + ε j) ^ 2
331
332/-! ## §4. The reduction theorem
333
334The composition of §1 (conformal expansion), §2 (graph-Laplacian
335decomposition), and §3 (Schläfli-anchored second-order form) yields:
336
337 `S^(2)[ξ] = (1/2) · Σ_⟨i,j⟩ A_{ij} · (ξ_i − ξ_j)²`
338
339with `A_{ij} = − bilinearCoefficient W i j` (the sign comes from
340`Q = − D` in §2).
341
342This is the Lean form of equation (d) in Jon's note. -/
343
344/-- The "edge area" weights `A_{ij}` derived from the linearization
345 data. Defined as `−M_{ij} = − dArea · dDeficit`; the sign comes
346 from §2 (`Q = − D`). On standard regular lattices these are
347 non-negative. -/
348def edgeArea {n : ℕ} (W : WeakFieldReggeData n) (i j : Fin n) : ℝ :=
349 - bilinearCoefficient W i j
350
351theorem edgeArea_symm {n : ℕ} (W : WeakFieldReggeData n) (i j : Fin n) :
352 edgeArea W i j = edgeArea W j i := by
353 unfold edgeArea
354 rw [bilinearCoefficient_symm]
355
356/-- The Dirichlet form on the negated coefficient matrix is the negation
357 of the Dirichlet form on the original. Pure algebra: each summand
358 `(- M i j) * (ε i - ε j)² = - (M i j * (ε i - ε j)²)`. -/
359theorem dirichletForm_neg
360 {n : ℕ} (M : Fin n → Fin n → ℝ) (ε : LogPotential n) :
361 dirichletForm (fun i j => - M i j) ε = - dirichletForm M ε := by
362 unfold dirichletForm
363 have h1 : ∀ i j, (- M i j) * (ε i - ε j) ^ 2
364 = - (M i j * (ε i - ε j) ^ 2) := by
365 intro i j; ring
366 have hinner : ∀ i, ∑ j : Fin n, (- M i j) * (ε i - ε j) ^ 2
367 = - ∑ j : Fin n, M i j * (ε i - ε j) ^ 2 := by
368 intro i
369 rw [← Finset.sum_neg_distrib]
370 exact Finset.sum_congr rfl (fun j _ => h1 i j)
371 rw [show (fun i => ∑ j, (- M i j) * (ε i - ε j) ^ 2)
372 = (fun i => - ∑ j, M i j * (ε i - ε j) ^ 2) from funext hinner]
373 rw [Finset.sum_neg_distrib]; ring
374
375/-- The Dirichlet form on `edgeArea W` is the negation of the Dirichlet
376 form on `bilinearCoefficient W`. Direct from `dirichletForm_neg`
377 plus the definition `edgeArea = − bilinearCoefficient`. -/
378theorem dirichletForm_edgeArea
379 {n : ℕ} (W : WeakFieldReggeData n) (ε : LogPotential n) :
380 dirichletForm (edgeArea W) ε
381 = - dirichletForm (bilinearCoefficient W) ε := by
382 have h := dirichletForm_neg (bilinearCoefficient W) ε
383 -- `(fun i j => - bilinearCoefficient W i j)` is definitionally `edgeArea W`.
384 exact h
385
386/-- **WEAK-FIELD CONFORMAL REDUCTION (the main theorem).**
387
388 Under the Schläfli row-sum hypothesis (§3) on the linearization
389 data `W`, the second-order Regge action equals the discrete
390 Dirichlet energy on the conformal mode `ε`, with edge weights
391 `A_{ij} = − dArea_{ij} · dDeficit_{ij}`:
392
393 secondOrderReggeAction W ε
394 = (1/2) · Σ_{i,j} ½ · (ε i − ε j)² · A_{ij}
395 = ½ · dirichletForm A ε.
396
397 Multiplying through by `1/κ` recovers Jon's equation (d):
398
399 S^(2)/κ = (1/κ) · Σ_⟨i,j⟩ ½ · (ξ_i − ξ_j)² · A_{ij}.
400
401 Proof:
402 1. Expand `(ξ_i + ξ_j)² = ξ_i² + 2 ξ_i ξ_j + ξ_j²`.
403 2. The `ξ_i²` and `ξ_j²` pieces collapse via Schläfli row-sum.
404 3. The `2 ξ_i ξ_j` piece is `quadraticForm M ε = − dirichletForm M ε`
405 by `dirichlet_eq_neg_quadratic` (§2).
406 4. `dirichletForm (edgeArea W) ε = − dirichletForm M ε`
407 by `dirichletForm_edgeArea`.
408 Combining: LHS = `(1/4)·(0 + 2·(−D) + 0) = −D/2 = (1/2)·(−D)
409 = (1/2) · dirichletForm (edgeArea W) ε = RHS`. -/
410theorem weak_field_conformal_reduction
411 {n : ℕ} (W : WeakFieldReggeData n)
412 (hSchl : SchlaefliRowSum W)
413 (ε : LogPotential n) :
414 secondOrderReggeAction W ε
415 = (1 / 2) * dirichletForm (edgeArea W) ε := by
416 -- Abbreviations.
417 set M : Fin n → Fin n → ℝ := bilinearCoefficient W with hM_def
418 -- Step 1: expand the square.
419 have hexp : ∀ i j, M i j * (ε i + ε j) ^ 2
420 = M i j * (ε i) ^ 2
421 + 2 * (M i j * ε i * ε j)
422 + M i j * (ε j) ^ 2 := by
423 intro i j; ring
424 -- Sum over i, j.
425 have hsum : ∑ i : Fin n, ∑ j : Fin n, M i j * (ε i + ε j) ^ 2
426 = (∑ i : Fin n, ∑ j : Fin n, M i j * (ε i) ^ 2)
427 + 2 * (∑ i : Fin n, ∑ j : Fin n, M i j * ε i * ε j)
428 + (∑ i : Fin n, ∑ j : Fin n, M i j * (ε j) ^ 2) := by
429 have h1 : ∀ i, ∑ j : Fin n, M i j * (ε i + ε j) ^ 2
430 = ∑ j : Fin n, (M i j * (ε i) ^ 2
431 + 2 * (M i j * ε i * ε j)
432 + M i j * (ε j) ^ 2) := fun i =>
433 Finset.sum_congr rfl (fun j _ => hexp i j)
434 simp only [h1, Finset.sum_add_distrib]
435 have hpull : ∀ i, ∑ j : Fin n, 2 * (M i j * ε i * ε j)
436 = 2 * ∑ j : Fin n, M i j * ε i * ε j := fun i =>
437 (Finset.mul_sum _ _ _).symm
438 simp only [hpull, ← Finset.mul_sum]
439 -- Step 2: the (ε i)² and (ε j)² pieces vanish under Schläfli row-sum.
440 have hSchl_M : ∀ i : Fin n, ∑ j : Fin n, M i j = 0 := hSchl
441 have hi2 : ∑ i : Fin n, ∑ j : Fin n, M i j * (ε i) ^ 2 = 0 := by
442 have hpull : ∀ i, ∑ j : Fin n, M i j * (ε i) ^ 2
443 = (∑ j : Fin n, M i j) * (ε i) ^ 2 := fun i =>
444 sum_const_mul_right (fun j => M i j) ((ε i) ^ 2)
445 simp only [hpull, hSchl_M, zero_mul, Finset.sum_const_zero]
446 have hSchl_col : ∀ j : Fin n, ∑ i : Fin n, M i j = 0 := by
447 intro j
448 have heq : ∑ i : Fin n, M i j = ∑ i : Fin n, M j i :=
449 Finset.sum_congr rfl (fun i _ => bilinearCoefficient_symm W i j)
450 rw [heq]; exact hSchl_M j
451 have hj2 : ∑ i : Fin n, ∑ j : Fin n, M i j * (ε j) ^ 2 = 0 := by
452 rw [Finset.sum_comm]
453 have hpull : ∀ j, ∑ i : Fin n, M i j * (ε j) ^ 2
454 = (∑ i : Fin n, M i j) * (ε j) ^ 2 := fun j =>
455 sum_const_mul_right (fun i => M i j) ((ε j) ^ 2)
456 simp only [hpull, hSchl_col, zero_mul, Finset.sum_const_zero]
457 -- Step 3: rewrite the cross term via §2.
458 have hQ : quadraticForm M ε = - dirichletForm M ε :=
459 dirichlet_eq_neg_quadratic M (bilinearCoefficient_symm W) hSchl ε
460 -- Step 4: rewrite the goal RHS via `dirichletForm_edgeArea`.
461 rw [dirichletForm_edgeArea W ε]
462 -- Now expand the LHS.
463 unfold secondOrderReggeAction
464 rw [show (∑ i : Fin n, ∑ j : Fin n, bilinearCoefficient W i j * (ε i + ε j) ^ 2)
465 = (∑ i : Fin n, ∑ j : Fin n, M i j * (ε i + ε j) ^ 2) from rfl]
466 rw [hsum, hi2, hj2]
467 -- Goal: `(1/4) * (0 + 2 * Σ Σ M i j * ε i * ε j + 0) = (1/2) * (- D)`.
468 unfold quadraticForm at hQ
469 rw [hQ]
470 ring
471
472/-- **JON'S EQUATION (d).**
473
474 Multiplying the reduction by `1/κ` and dividing by 2 to absorb the
475 factor at the head of `dirichletForm`:
476
477 secondOrderReggeAction W ε / κ
478 = (1/κ) · Σ_⟨i,j⟩ ½ · (ξ_i − ξ_j)² · A_{ij}.
479
480 The `Σ_⟨i,j⟩ ½ · (ξ_i − ξ_j)² · A_{ij}` form is the "ordered pair"
481 Dirichlet form `(1/2) · dirichletForm`. Below we record the
482 explicit κ-normalized identity. -/
483theorem weak_field_conformal_reduction_kappa
484 {n : ℕ} (W : WeakFieldReggeData n)
485 (hSchl : SchlaefliRowSum W)
486 (κ : ℝ) (hκ : κ ≠ 0)
487 (ε : LogPotential n) :
488 secondOrderReggeAction W ε / κ
489 = (1 / κ) * (1 / 2) * dirichletForm (edgeArea W) ε := by
490 rw [weak_field_conformal_reduction W hSchl ε]
491 field_simp
492
493/-- **THE FLAT-VACUUM CONSISTENCY CHECK.**
494 On the flat vacuum `ξ ≡ 0`, the Dirichlet form vanishes, so the
495 second-order Regge action also vanishes. This is consistent with
496 the linearized Regge action being zero on flat backgrounds. -/
497theorem secondOrderReggeAction_flat
498 {n : ℕ} (W : WeakFieldReggeData n) :
499 secondOrderReggeAction W (fun _ : Fin n => (0 : ℝ)) = 0 := by
500 unfold secondOrderReggeAction
501 have : ∀ i j : Fin n,
502 bilinearCoefficient W i j * ((0 : ℝ) + (0 : ℝ)) ^ 2 = 0 := by
503 intro i j; ring
504 simp only [this, Finset.sum_const_zero, mul_zero]
505
506theorem dirichletForm_flat
507 {n : ℕ} (M : Fin n → Fin n → ℝ) :
508 dirichletForm M (fun _ : Fin n => (0 : ℝ)) = 0 := by
509 unfold dirichletForm
510 have : ∀ i j : Fin n, M i j * ((0 : ℝ) - (0 : ℝ)) ^ 2 = 0 := by
511 intro i j; ring
512 simp only [this, Finset.sum_const_zero, mul_zero]
513
514/-! ## §5. Connection to the existing infrastructure
515
516The reduction here is the *concrete second-order content* of the
517hypothesis `EdgeLengthFromPsi.ReggeDeficitLinearizationHypothesis`. We
518record the connection: a `WeakFieldReggeData` together with the
519Schläfli row-sum property gives a candidate discharge of the
520linearization hypothesis at the bilinear level. -/
521
522/-- The Dirichlet weights `A_{ij}` derived from `WeakFieldReggeData`
523 define a `WeightedLedgerGraph` provided they are non-negative.
524 Non-negativity is a property of the lattice (e.g., automatic for
525 regular cubic lattices where `A_{ij}` is a true area), so we
526 package it as an explicit hypothesis. -/
527def edgeAreaGraph {n : ℕ} (W : WeakFieldReggeData n)
528 (hpos : ∀ i j, 0 ≤ edgeArea W i j) : WeightedLedgerGraph n :=
529 { weight := edgeArea W
530 , weight_nonneg := hpos
531 , weight_symm := edgeArea_symm W }
532
533/-- **BRIDGE TO `laplacian_action`.**
534 The second-order Regge action equals `(1/2) · laplacian_action`
535 on the `edgeAreaGraph`. Concretely:
536
537 S^(2)[ξ] = (1/2) · laplacian_action (edgeAreaGraph W) ε.
538
539 Combined with `EdgeLengthFromPsi.field_curvature_identity_under_linearization`,
540 this is the explicit second-order content of the bridge identity:
541 "J-cost Dirichlet energy = (1/κ) · Regge sum, at second order in ξ". -/
542theorem secondOrder_eq_half_laplacian_action
543 {n : ℕ} (W : WeakFieldReggeData n)
544 (hSchl : SchlaefliRowSum W)
545 (hpos : ∀ i j, 0 ≤ edgeArea W i j)
546 (ε : LogPotential n) :
547 secondOrderReggeAction W ε
548 = (1 / 2) * laplacian_action (edgeAreaGraph W hpos) ε := by
549 rw [weak_field_conformal_reduction W hSchl ε]
550 unfold dirichletForm laplacian_action edgeAreaGraph
551 rfl
552
553/-! ## §5b. Discharging the row-sum condition by a graph Laplacian
554
555The row-sum condition is not a new physical assumption once the
556second-variation bilinear is written in Laplacian form. Given symmetric
557edge-area weights `A_{ij}`, define the bilinear coefficient matrix
558
559 `M_{ij} = δ_{ij} · Σ_k A_{ik} - A_{ij}`.
560
561Then `Σ_j M_{ij} = 0` exactly. This is the finite-dimensional version of
562the flat-background Schläfli statement: a constant conformal rescaling is
563a pure scale mode and cannot create curvature.
564
565The diagonal entries of `M` do not contribute to the Dirichlet energy
566because `(ξ_i - ξ_i)^2 = 0`; the off-diagonal entries recover the edge
567weights `A_{ij}`.
568-/
569
570/-- The Laplacian bilinear coefficient matrix associated with symmetric
571 edge-area weights `A`. The diagonal is chosen so every row sums to
572 zero. -/
573def laplacianCoefficient {n : ℕ} (A : Fin n → Fin n → ℝ)
574 (i j : Fin n) : ℝ :=
575 (if i = j then ∑ k : Fin n, A i k else 0) - A i j
576
577/-- The Laplacian coefficient matrix is symmetric when `A` is symmetric. -/
578theorem laplacianCoefficient_symm {n : ℕ} (A : Fin n → Fin n → ℝ)
579 (hA : ∀ i j, A i j = A j i) :
580 ∀ i j, laplacianCoefficient A i j = laplacianCoefficient A j i := by
581 intro i j
582 unfold laplacianCoefficient
583 by_cases hij : i = j
584 · subst j
585 rfl
586 · have hji : j ≠ i := by intro h; exact hij h.symm
587 simp only [hij, hji, ↓reduceIte, zero_sub]
588 rw [hA i j]
589
590/-- The Laplacian coefficient matrix has exact zero row sums. This is the
591 theorem-level replacement for the `SchlaefliRowSum` hypothesis in the
592 flat conformal sector. -/
593theorem laplacianCoefficient_row_sum {n : ℕ} (A : Fin n → Fin n → ℝ) :
594 ∀ i : Fin n, ∑ j : Fin n, laplacianCoefficient A i j = 0 := by
595 intro i
596 unfold laplacianCoefficient
597 rw [Finset.sum_sub_distrib]
598 have hdiag :
599 (∑ j : Fin n, (if i = j then ∑ k : Fin n, A i k else 0))
600 = ∑ k : Fin n, A i k := by
601 rw [Finset.sum_eq_single i]
602 · simp
603 · intro b _ hb
604 have hne : i ≠ b := fun h => hb h.symm
605 simp [hne]
606 · intro hi
607 exact (hi (Finset.mem_univ i)).elim
608 rw [hdiag]
609 ring
610
611/-- The weak-field Regge data whose bilinear coefficient is the graph
612 Laplacian associated with `A`. We put the whole coefficient into
613 `dDeficit`; `dArea = 1` is a harmless normalization because only the
614 product `dArea · dDeficit` enters the second variation. -/
615def laplacianReggeData {n : ℕ} (A : Fin n → Fin n → ℝ)
616 (hA : ∀ i j, A i j = A j i) : WeakFieldReggeData n :=
617 { dArea := fun _ _ => 1
618 , dDeficit := laplacianCoefficient A
619 , dArea_symm := by intro i j; rfl
620 , dDeficit_symm := laplacianCoefficient_symm A hA
621 }
622
623/-- For `laplacianReggeData`, the bilinear coefficient is exactly the
624 Laplacian coefficient matrix. -/
625theorem bilinearCoefficient_laplacianReggeData {n : ℕ}
626 (A : Fin n → Fin n → ℝ) (hA : ∀ i j, A i j = A j i)
627 (i j : Fin n) :
628 bilinearCoefficient (laplacianReggeData A hA) i j
629 = laplacianCoefficient A i j := by
630 unfold bilinearCoefficient laplacianReggeData
631 ring
632
633/-- **ROW-SUM DISCHARGE.** The Schläfli/flat-mode row-sum condition holds
634 as a theorem for the Laplacian second-variation data. -/
635theorem schlaefliRowSum_laplacianReggeData {n : ℕ}
636 (A : Fin n → Fin n → ℝ) (hA : ∀ i j, A i j = A j i) :
637 SchlaefliRowSum (laplacianReggeData A hA) := by
638 intro i
639 have hrow := laplacianCoefficient_row_sum A i
640 simpa only [bilinearCoefficient_laplacianReggeData A hA] using hrow
641
642/-- The Dirichlet form ignores diagonal entries. -/
643theorem dirichletForm_diag_irrelevant {n : ℕ}
644 (A B : Fin n → Fin n → ℝ)
645 (hOff : ∀ i j, i ≠ j → A i j = B i j)
646 (ε : LogPotential n) :
647 dirichletForm A ε = dirichletForm B ε := by
648 unfold dirichletForm
649 apply congrArg ((fun x : ℝ => (1 / 2) * x))
650 apply Finset.sum_congr rfl
651 intro i _
652 apply Finset.sum_congr rfl
653 intro j _
654 by_cases hij : i = j
655 · subst j
656 ring
657 · rw [hOff i j hij]
658
659/-- The edge-area matrix induced by the Laplacian Regge data has the same
660 Dirichlet form as the original edge-area weights `A`. Off diagonal it
661 equals `A`; diagonal entries are irrelevant. -/
662theorem dirichletForm_edgeArea_laplacianReggeData {n : ℕ}
663 (A : Fin n → Fin n → ℝ) (hA : ∀ i j, A i j = A j i)
664 (ε : LogPotential n) :
665 dirichletForm (edgeArea (laplacianReggeData A hA)) ε
666 = dirichletForm A ε := by
667 apply dirichletForm_diag_irrelevant
668 intro i j hij
669 unfold edgeArea
670 rw [bilinearCoefficient_laplacianReggeData A hA]
671 unfold laplacianCoefficient
672 simp [hij]
673
674/-- **UNCONDITIONAL FLAT-SECTOR REDUCTION.** For any symmetric edge-area
675 weights `A`, the graph-Laplacian second-variation data automatically
676 satisfies the Schläfli row sum and the weak-field conformal Regge
677 action reduces to the Dirichlet form with weights `A`. -/
678theorem weak_field_conformal_reduction_laplacianData {n : ℕ}
679 (A : Fin n → Fin n → ℝ) (hA : ∀ i j, A i j = A j i)
680 (ε : LogPotential n) :
681 secondOrderReggeAction (laplacianReggeData A hA) ε
682 = (1 / 2) * dirichletForm A ε := by
683 rw [weak_field_conformal_reduction
684 (laplacianReggeData A hA)
685 (schlaefliRowSum_laplacianReggeData A hA) ε]
686 rw [dirichletForm_edgeArea_laplacianReggeData A hA ε]
687
688theorem weak_field_conformal_reduction_laplacianData_kappa {n : ℕ}
689 (A : Fin n → Fin n → ℝ) (hA : ∀ i j, A i j = A j i)
690 (κ : ℝ) (hκ : κ ≠ 0) (ε : LogPotential n) :
691 secondOrderReggeAction (laplacianReggeData A hA) ε / κ
692 = (1 / κ) * (1 / 2) * dirichletForm A ε := by
693 rw [weak_field_conformal_reduction_laplacianData A hA ε]
694 field_simp
695
696/-! ## §6. Certificate -/
697
698structure WeakFieldConformalReggeCert where
699 conformal_exact : ∀ {n : ℕ} (a : ℝ) (ha : 0 < a) (ε : LogPotential n)
700 (i j : Fin n),
701 (conformal_edge_length_field a ha ε).length i j ^ 2
702 = a ^ 2 * Real.exp (ε i + ε j)
703 conformal_taylor2 : ∀ {n : ℕ} (a : ℝ) (ha : 0 < a) (ε : LogPotential n)
704 (i j : Fin n),
705 (conformal_edge_length_field a ha ε).length i j ^ 2 / a ^ 2
706 = 1 + (ε i + ε j) + (ε i + ε j) ^ 2 / 2
707 + conformal_remainder (ε i + ε j)
708 graph_laplacian_decomp : ∀ {n : ℕ} (M : Fin n → Fin n → ℝ),
709 (∀ i j, M i j = M j i) → (∀ i, ∑ j : Fin n, M i j = 0) →
710 ∀ ε, quadraticForm M ε = - dirichletForm M ε
711 reduction : ∀ {n : ℕ} (W : WeakFieldReggeData n),
712 SchlaefliRowSum W → ∀ ε,
713 secondOrderReggeAction W ε
714 = (1 / 2) * dirichletForm (edgeArea W) ε
715 reduction_kappa : ∀ {n : ℕ} (W : WeakFieldReggeData n),
716 SchlaefliRowSum W → ∀ (κ : ℝ), κ ≠ 0 → ∀ ε,
717 secondOrderReggeAction W ε / κ
718 = (1 / κ) * (1 / 2) * dirichletForm (edgeArea W) ε
719 row_sum_discharged_laplacian : ∀ {n : ℕ}
720 (A : Fin n → Fin n → ℝ) (hA : ∀ i j, A i j = A j i),
721 SchlaefliRowSum (laplacianReggeData A hA)
722 reduction_laplacian : ∀ {n : ℕ}
723 (A : Fin n → Fin n → ℝ) (hA : ∀ i j, A i j = A j i)
724 (ε : LogPotential n),
725 secondOrderReggeAction (laplacianReggeData A hA) ε
726 = (1 / 2) * dirichletForm A ε
727 reduction_laplacian_kappa : ∀ {n : ℕ}
728 (A : Fin n → Fin n → ℝ) (hA : ∀ i j, A i j = A j i)
729 (κ : ℝ), κ ≠ 0 → ∀ ε : LogPotential n,
730 secondOrderReggeAction (laplacianReggeData A hA) ε / κ
731 = (1 / κ) * (1 / 2) * dirichletForm A ε
732 flat_vanishing_action : ∀ {n : ℕ} (W : WeakFieldReggeData n),
733 secondOrderReggeAction W (fun _ : Fin n => (0 : ℝ)) = 0
734 flat_vanishing_dirichlet : ∀ {n : ℕ} (M : Fin n → Fin n → ℝ),
735 dirichletForm M (fun _ : Fin n => (0 : ℝ)) = 0
736 remainder_flat : conformal_remainder 0 = 0
737
738theorem weakFieldConformalReggeCert : WeakFieldConformalReggeCert where
739 conformal_exact := fun a ha ε i j => conformal_length_sq_exact a ha ε i j
740 conformal_taylor2 := fun a ha ε i j => conformal_length_sq_taylor2 a ha ε i j
741 graph_laplacian_decomp := fun M hsymm hrow ε =>
742 dirichlet_eq_neg_quadratic M hsymm hrow ε
743 reduction := fun W hSchl ε => weak_field_conformal_reduction W hSchl ε
744 reduction_kappa := fun W hSchl κ hκ ε =>
745 weak_field_conformal_reduction_kappa W hSchl κ hκ ε
746 row_sum_discharged_laplacian := fun A hA =>
747 schlaefliRowSum_laplacianReggeData A hA
748 reduction_laplacian := fun A hA ε =>
749 weak_field_conformal_reduction_laplacianData A hA ε
750 reduction_laplacian_kappa := fun A hA κ hκ ε =>
751 weak_field_conformal_reduction_laplacianData_kappa A hA κ hκ ε
752 flat_vanishing_action := fun W => secondOrderReggeAction_flat W
753 flat_vanishing_dirichlet := fun M => dirichletForm_flat M
754 remainder_flat := conformal_remainder_zero
755
756end
757
758end WeakFieldConformalRegge
759end Gravity
760end IndisputableMonolith
761