IndisputableMonolith.Gravity.WeakFieldConformalRegge
IndisputableMonolith/Gravity/WeakFieldConformalRegge.lean · 854 lines · 44 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/-- **Missing component-level comparison target.**
357
358Philip's question about `M_{ij}` versus `area(f_{ij})` is exactly this datum.
359For a genuine Regge triangulation, one must compute the second-variation
360coefficient matrix `M = bilinearCoefficient W` from the Cayley-Menger /
361dihedral-angle formulas and show that, off diagonal, it is the negative of
362the geometric area/face weight matrix used by the J-cost Dirichlet form.
363
364This structure does **not** assert that the computation has been done. It
365names the theorem-shaped target:
366
367* `geometricArea i j` is the intended `area(f_ij)` / hinge-dual weight;
368* `offDiag_component_match` says `M_ij = -geometricArea_ij` for `i ≠ j`;
369* `schlaefli_row_sum` supplies the diagonal/row-sum closure.
370
371Once an actual component computation produces this structure for a concrete
372mesh, the general weak-field reduction below turns it into the Dirichlet
373energy with those geometric weights. -/
374structure ReggeComponentComparison {n : ℕ} (W : WeakFieldReggeData n) where
375 geometricArea : Fin n → Fin n → ℝ
376 geometricArea_symm : ∀ i j, geometricArea i j = geometricArea j i
377 geometricArea_nonneg : ∀ i j, 0 ≤ geometricArea i j
378 offDiag_component_match :
379 ∀ i j, i ≠ j → bilinearCoefficient W i j = - geometricArea i j
380 schlaefli_row_sum : SchlaefliRowSum W
381
382/-- The Dirichlet form on the negated coefficient matrix is the negation
383 of the Dirichlet form on the original. Pure algebra: each summand
384 `(- M i j) * (ε i - ε j)² = - (M i j * (ε i - ε j)²)`. -/
385theorem dirichletForm_neg
386 {n : ℕ} (M : Fin n → Fin n → ℝ) (ε : LogPotential n) :
387 dirichletForm (fun i j => - M i j) ε = - dirichletForm M ε := by
388 unfold dirichletForm
389 have h1 : ∀ i j, (- M i j) * (ε i - ε j) ^ 2
390 = - (M i j * (ε i - ε j) ^ 2) := by
391 intro i j; ring
392 have hinner : ∀ i, ∑ j : Fin n, (- M i j) * (ε i - ε j) ^ 2
393 = - ∑ j : Fin n, M i j * (ε i - ε j) ^ 2 := by
394 intro i
395 rw [← Finset.sum_neg_distrib]
396 exact Finset.sum_congr rfl (fun j _ => h1 i j)
397 rw [show (fun i => ∑ j, (- M i j) * (ε i - ε j) ^ 2)
398 = (fun i => - ∑ j, M i j * (ε i - ε j) ^ 2) from funext hinner]
399 rw [Finset.sum_neg_distrib]; ring
400
401/-- The Dirichlet form on `edgeArea W` is the negation of the Dirichlet
402 form on `bilinearCoefficient W`. Direct from `dirichletForm_neg`
403 plus the definition `edgeArea = − bilinearCoefficient`. -/
404theorem dirichletForm_edgeArea
405 {n : ℕ} (W : WeakFieldReggeData n) (ε : LogPotential n) :
406 dirichletForm (edgeArea W) ε
407 = - dirichletForm (bilinearCoefficient W) ε := by
408 have h := dirichletForm_neg (bilinearCoefficient W) ε
409 -- `(fun i j => - bilinearCoefficient W i j)` is definitionally `edgeArea W`.
410 exact h
411
412/-- **WEAK-FIELD CONFORMAL REDUCTION (the main theorem).**
413
414 Under the Schläfli row-sum hypothesis (§3) on the linearization
415 data `W`, the second-order Regge action equals the discrete
416 Dirichlet energy on the conformal mode `ε`, with edge weights
417 `A_{ij} = − dArea_{ij} · dDeficit_{ij}`:
418
419 secondOrderReggeAction W ε
420 = (1/2) · Σ_{i,j} ½ · (ε i − ε j)² · A_{ij}
421 = ½ · dirichletForm A ε.
422
423 Multiplying through by `1/κ` recovers Jon's equation (d):
424
425 S^(2)/κ = (1/κ) · Σ_⟨i,j⟩ ½ · (ξ_i − ξ_j)² · A_{ij}.
426
427 Proof:
428 1. Expand `(ξ_i + ξ_j)² = ξ_i² + 2 ξ_i ξ_j + ξ_j²`.
429 2. The `ξ_i²` and `ξ_j²` pieces collapse via Schläfli row-sum.
430 3. The `2 ξ_i ξ_j` piece is `quadraticForm M ε = − dirichletForm M ε`
431 by `dirichlet_eq_neg_quadratic` (§2).
432 4. `dirichletForm (edgeArea W) ε = − dirichletForm M ε`
433 by `dirichletForm_edgeArea`.
434 Combining: LHS = `(1/4)·(0 + 2·(−D) + 0) = −D/2 = (1/2)·(−D)
435 = (1/2) · dirichletForm (edgeArea W) ε = RHS`. -/
436theorem weak_field_conformal_reduction
437 {n : ℕ} (W : WeakFieldReggeData n)
438 (hSchl : SchlaefliRowSum W)
439 (ε : LogPotential n) :
440 secondOrderReggeAction W ε
441 = (1 / 2) * dirichletForm (edgeArea W) ε := by
442 -- Abbreviations.
443 set M : Fin n → Fin n → ℝ := bilinearCoefficient W with hM_def
444 -- Step 1: expand the square.
445 have hexp : ∀ i j, M i j * (ε i + ε j) ^ 2
446 = M i j * (ε i) ^ 2
447 + 2 * (M i j * ε i * ε j)
448 + M i j * (ε j) ^ 2 := by
449 intro i j; ring
450 -- Sum over i, j.
451 have hsum : ∑ i : Fin n, ∑ j : Fin n, M i j * (ε i + ε j) ^ 2
452 = (∑ i : Fin n, ∑ j : Fin n, M i j * (ε i) ^ 2)
453 + 2 * (∑ i : Fin n, ∑ j : Fin n, M i j * ε i * ε j)
454 + (∑ i : Fin n, ∑ j : Fin n, M i j * (ε j) ^ 2) := by
455 have h1 : ∀ i, ∑ j : Fin n, M i j * (ε i + ε j) ^ 2
456 = ∑ j : Fin n, (M i j * (ε i) ^ 2
457 + 2 * (M i j * ε i * ε j)
458 + M i j * (ε j) ^ 2) := fun i =>
459 Finset.sum_congr rfl (fun j _ => hexp i j)
460 simp only [h1, Finset.sum_add_distrib]
461 have hpull : ∀ i, ∑ j : Fin n, 2 * (M i j * ε i * ε j)
462 = 2 * ∑ j : Fin n, M i j * ε i * ε j := fun i =>
463 (Finset.mul_sum _ _ _).symm
464 simp only [hpull, ← Finset.mul_sum]
465 -- Step 2: the (ε i)² and (ε j)² pieces vanish under Schläfli row-sum.
466 have hSchl_M : ∀ i : Fin n, ∑ j : Fin n, M i j = 0 := hSchl
467 have hi2 : ∑ i : Fin n, ∑ j : Fin n, M i j * (ε i) ^ 2 = 0 := by
468 have hpull : ∀ i, ∑ j : Fin n, M i j * (ε i) ^ 2
469 = (∑ j : Fin n, M i j) * (ε i) ^ 2 := fun i =>
470 sum_const_mul_right (fun j => M i j) ((ε i) ^ 2)
471 simp only [hpull, hSchl_M, zero_mul, Finset.sum_const_zero]
472 have hSchl_col : ∀ j : Fin n, ∑ i : Fin n, M i j = 0 := by
473 intro j
474 have heq : ∑ i : Fin n, M i j = ∑ i : Fin n, M j i :=
475 Finset.sum_congr rfl (fun i _ => bilinearCoefficient_symm W i j)
476 rw [heq]; exact hSchl_M j
477 have hj2 : ∑ i : Fin n, ∑ j : Fin n, M i j * (ε j) ^ 2 = 0 := by
478 rw [Finset.sum_comm]
479 have hpull : ∀ j, ∑ i : Fin n, M i j * (ε j) ^ 2
480 = (∑ i : Fin n, M i j) * (ε j) ^ 2 := fun j =>
481 sum_const_mul_right (fun i => M i j) ((ε j) ^ 2)
482 simp only [hpull, hSchl_col, zero_mul, Finset.sum_const_zero]
483 -- Step 3: rewrite the cross term via §2.
484 have hQ : quadraticForm M ε = - dirichletForm M ε :=
485 dirichlet_eq_neg_quadratic M (bilinearCoefficient_symm W) hSchl ε
486 -- Step 4: rewrite the goal RHS via `dirichletForm_edgeArea`.
487 rw [dirichletForm_edgeArea W ε]
488 -- Now expand the LHS.
489 unfold secondOrderReggeAction
490 rw [show (∑ i : Fin n, ∑ j : Fin n, bilinearCoefficient W i j * (ε i + ε j) ^ 2)
491 = (∑ i : Fin n, ∑ j : Fin n, M i j * (ε i + ε j) ^ 2) from rfl]
492 rw [hsum, hi2, hj2]
493 -- Goal: `(1/4) * (0 + 2 * Σ Σ M i j * ε i * ε j + 0) = (1/2) * (- D)`.
494 unfold quadraticForm at hQ
495 rw [hQ]
496 ring
497
498/-- **JON'S EQUATION (d).**
499
500 Multiplying the reduction by `1/κ` and dividing by 2 to absorb the
501 factor at the head of `dirichletForm`:
502
503 secondOrderReggeAction W ε / κ
504 = (1/κ) · Σ_⟨i,j⟩ ½ · (ξ_i − ξ_j)² · A_{ij}.
505
506 The `Σ_⟨i,j⟩ ½ · (ξ_i − ξ_j)² · A_{ij}` form is the "ordered pair"
507 Dirichlet form `(1/2) · dirichletForm`. Below we record the
508 explicit κ-normalized identity. -/
509theorem weak_field_conformal_reduction_kappa
510 {n : ℕ} (W : WeakFieldReggeData n)
511 (hSchl : SchlaefliRowSum W)
512 (κ : ℝ) (hκ : κ ≠ 0)
513 (ε : LogPotential n) :
514 secondOrderReggeAction W ε / κ
515 = (1 / κ) * (1 / 2) * dirichletForm (edgeArea W) ε := by
516 rw [weak_field_conformal_reduction W hSchl ε]
517 field_simp
518
519/-- **THE FLAT-VACUUM CONSISTENCY CHECK.**
520 On the flat vacuum `ξ ≡ 0`, the Dirichlet form vanishes, so the
521 second-order Regge action also vanishes. This is consistent with
522 the linearized Regge action being zero on flat backgrounds. -/
523theorem secondOrderReggeAction_flat
524 {n : ℕ} (W : WeakFieldReggeData n) :
525 secondOrderReggeAction W (fun _ : Fin n => (0 : ℝ)) = 0 := by
526 unfold secondOrderReggeAction
527 have : ∀ i j : Fin n,
528 bilinearCoefficient W i j * ((0 : ℝ) + (0 : ℝ)) ^ 2 = 0 := by
529 intro i j; ring
530 simp only [this, Finset.sum_const_zero, mul_zero]
531
532theorem dirichletForm_flat
533 {n : ℕ} (M : Fin n → Fin n → ℝ) :
534 dirichletForm M (fun _ : Fin n => (0 : ℝ)) = 0 := by
535 unfold dirichletForm
536 have : ∀ i j : Fin n, M i j * ((0 : ℝ) - (0 : ℝ)) ^ 2 = 0 := by
537 intro i j; ring
538 simp only [this, Finset.sum_const_zero, mul_zero]
539
540/-! ## §5. Connection to the existing infrastructure
541
542The reduction here is the *concrete second-order content* of the
543hypothesis `EdgeLengthFromPsi.ReggeDeficitLinearizationHypothesis`. We
544record the connection: a `WeakFieldReggeData` together with the
545Schläfli row-sum property gives a candidate discharge of the
546linearization hypothesis at the bilinear level. -/
547
548/-- The Dirichlet weights `A_{ij}` derived from `WeakFieldReggeData`
549 define a `WeightedLedgerGraph` provided they are non-negative.
550 Non-negativity is a property of the lattice (e.g., automatic for
551 regular cubic lattices where `A_{ij}` is a true area), so we
552 package it as an explicit hypothesis. -/
553def edgeAreaGraph {n : ℕ} (W : WeakFieldReggeData n)
554 (hpos : ∀ i j, 0 ≤ edgeArea W i j) : WeightedLedgerGraph n :=
555 { weight := edgeArea W
556 , weight_nonneg := hpos
557 , weight_symm := edgeArea_symm W }
558
559/-- **BRIDGE TO `laplacian_action`.**
560 The second-order Regge action equals `(1/2) · laplacian_action`
561 on the `edgeAreaGraph`. Concretely:
562
563 S^(2)[ξ] = (1/2) · laplacian_action (edgeAreaGraph W) ε.
564
565 Combined with `EdgeLengthFromPsi.field_curvature_identity_under_linearization`,
566 this is the explicit second-order content of the bridge identity:
567 "J-cost Dirichlet energy = (1/κ) · Regge sum, at second order in ξ". -/
568theorem secondOrder_eq_half_laplacian_action
569 {n : ℕ} (W : WeakFieldReggeData n)
570 (hSchl : SchlaefliRowSum W)
571 (hpos : ∀ i j, 0 ≤ edgeArea W i j)
572 (ε : LogPotential n) :
573 secondOrderReggeAction W ε
574 = (1 / 2) * laplacian_action (edgeAreaGraph W hpos) ε := by
575 rw [weak_field_conformal_reduction W hSchl ε]
576 unfold dirichletForm laplacian_action edgeAreaGraph
577 rfl
578
579/-! ## §5b. Discharging the row-sum condition by a graph Laplacian
580
581The row-sum condition is not a new physical assumption once the
582second-variation bilinear is written in Laplacian form. Given symmetric
583edge-area weights `A_{ij}`, define the bilinear coefficient matrix
584
585 `M_{ij} = δ_{ij} · Σ_k A_{ik} - A_{ij}`.
586
587Then `Σ_j M_{ij} = 0` exactly. This is the finite-dimensional version of
588the flat-background Schläfli statement: a constant conformal rescaling is
589a pure scale mode and cannot create curvature.
590
591The diagonal entries of `M` do not contribute to the Dirichlet energy
592because `(ξ_i - ξ_i)^2 = 0`; the off-diagonal entries recover the edge
593weights `A_{ij}`.
594-/
595
596/-- The Laplacian bilinear coefficient matrix associated with symmetric
597 edge-area weights `A`. The diagonal is chosen so every row sums to
598 zero. -/
599def laplacianCoefficient {n : ℕ} (A : Fin n → Fin n → ℝ)
600 (i j : Fin n) : ℝ :=
601 (if i = j then ∑ k : Fin n, A i k else 0) - A i j
602
603/-- The Laplacian coefficient matrix is symmetric when `A` is symmetric. -/
604theorem laplacianCoefficient_symm {n : ℕ} (A : Fin n → Fin n → ℝ)
605 (hA : ∀ i j, A i j = A j i) :
606 ∀ i j, laplacianCoefficient A i j = laplacianCoefficient A j i := by
607 intro i j
608 unfold laplacianCoefficient
609 by_cases hij : i = j
610 · subst j
611 rfl
612 · have hji : j ≠ i := by intro h; exact hij h.symm
613 simp only [hij, hji, ↓reduceIte, zero_sub]
614 rw [hA i j]
615
616/-- The Laplacian coefficient matrix has exact zero row sums. This is the
617 theorem-level replacement for the `SchlaefliRowSum` hypothesis in the
618 flat conformal sector. -/
619theorem laplacianCoefficient_row_sum {n : ℕ} (A : Fin n → Fin n → ℝ) :
620 ∀ i : Fin n, ∑ j : Fin n, laplacianCoefficient A i j = 0 := by
621 intro i
622 unfold laplacianCoefficient
623 rw [Finset.sum_sub_distrib]
624 have hdiag :
625 (∑ j : Fin n, (if i = j then ∑ k : Fin n, A i k else 0))
626 = ∑ k : Fin n, A i k := by
627 rw [Finset.sum_eq_single i]
628 · simp
629 · intro b _ hb
630 have hne : i ≠ b := fun h => hb h.symm
631 simp [hne]
632 · intro hi
633 exact (hi (Finset.mem_univ i)).elim
634 rw [hdiag]
635 ring
636
637/-- The weak-field Regge data whose bilinear coefficient is the graph
638 Laplacian associated with `A`. We put the whole coefficient into
639 `dDeficit`; `dArea = 1` is a harmless normalization because only the
640 product `dArea · dDeficit` enters the second variation. -/
641def laplacianReggeData {n : ℕ} (A : Fin n → Fin n → ℝ)
642 (hA : ∀ i j, A i j = A j i) : WeakFieldReggeData n :=
643 { dArea := fun _ _ => 1
644 , dDeficit := laplacianCoefficient A
645 , dArea_symm := by intro i j; rfl
646 , dDeficit_symm := laplacianCoefficient_symm A hA
647 }
648
649/-- For `laplacianReggeData`, the bilinear coefficient is exactly the
650 Laplacian coefficient matrix. -/
651theorem bilinearCoefficient_laplacianReggeData {n : ℕ}
652 (A : Fin n → Fin n → ℝ) (hA : ∀ i j, A i j = A j i)
653 (i j : Fin n) :
654 bilinearCoefficient (laplacianReggeData A hA) i j
655 = laplacianCoefficient A i j := by
656 unfold bilinearCoefficient laplacianReggeData
657 ring
658
659/-- **ROW-SUM DISCHARGE.** The Schläfli/flat-mode row-sum condition holds
660 as a theorem for the Laplacian second-variation data. -/
661theorem schlaefliRowSum_laplacianReggeData {n : ℕ}
662 (A : Fin n → Fin n → ℝ) (hA : ∀ i j, A i j = A j i) :
663 SchlaefliRowSum (laplacianReggeData A hA) := by
664 intro i
665 have hrow := laplacianCoefficient_row_sum A i
666 simpa only [bilinearCoefficient_laplacianReggeData A hA] using hrow
667
668/-- The Dirichlet form ignores diagonal entries. -/
669theorem dirichletForm_diag_irrelevant {n : ℕ}
670 (A B : Fin n → Fin n → ℝ)
671 (hOff : ∀ i j, i ≠ j → A i j = B i j)
672 (ε : LogPotential n) :
673 dirichletForm A ε = dirichletForm B ε := by
674 unfold dirichletForm
675 apply congrArg ((fun x : ℝ => (1 / 2) * x))
676 apply Finset.sum_congr rfl
677 intro i _
678 apply Finset.sum_congr rfl
679 intro j _
680 by_cases hij : i = j
681 · subst j
682 ring
683 · rw [hOff i j hij]
684
685/-- If the genuine Regge component comparison is supplied, then the second-order
686Regge action reduces to the Dirichlet form with the supplied geometric
687area/face weights. This is the exact formal shape of the missing
688`M_{ij}` versus `area(f_{ij})` comparison. -/
689theorem componentComparison_gives_geometric_dirichlet
690 {n : ℕ} (W : WeakFieldReggeData n)
691 (cmp : ReggeComponentComparison W)
692 (ε : LogPotential n) :
693 secondOrderReggeAction W ε
694 = (1 / 2) * dirichletForm cmp.geometricArea ε := by
695 rw [weak_field_conformal_reduction W cmp.schlaefli_row_sum ε]
696 congr 1
697 apply dirichletForm_diag_irrelevant
698 intro i j hij
699 unfold edgeArea
700 rw [cmp.offDiag_component_match i j hij]
701 ring
702
703/-- The edge-area matrix induced by the Laplacian Regge data has the same
704 Dirichlet form as the original edge-area weights `A`. Off diagonal it
705 equals `A`; diagonal entries are irrelevant. -/
706theorem dirichletForm_edgeArea_laplacianReggeData {n : ℕ}
707 (A : Fin n → Fin n → ℝ) (hA : ∀ i j, A i j = A j i)
708 (ε : LogPotential n) :
709 dirichletForm (edgeArea (laplacianReggeData A hA)) ε
710 = dirichletForm A ε := by
711 apply dirichletForm_diag_irrelevant
712 intro i j hij
713 unfold edgeArea
714 rw [bilinearCoefficient_laplacianReggeData A hA]
715 unfold laplacianCoefficient
716 simp [hij]
717
718/-- **Component comparison for Laplacian-form Regge data.**
719
720This closes the `M_{ij} = -area(f_{ij})` comparison for the coefficient
721package that the current Lean bridge actually uses: the graph-Laplacian
722second-variation data `laplacianReggeData`.
723
724Scope note: this is not yet the full Cayley-Menger derivative computation for
725a genuine arbitrary Regge triangulation. It proves that once the geometric
726second variation has been put into Laplacian form with symmetric nonnegative
727weights `A`, the component-level comparison is exact:
728
729* off diagonal, `bilinearCoefficient = -A`;
730* the row sums vanish theoremically;
731* the supplied `A` is the geometric-area/face-weight matrix consumed by the
732 Dirichlet form.
733
734The remaining hard geometric task is to derive such an `A` from actual
735Cayley-Menger/dihedral-angle derivatives for a concrete mesh. -/
736def laplacianReggeData_componentComparison {n : ℕ}
737 (A : Fin n → Fin n → ℝ)
738 (hA : ∀ i j, A i j = A j i)
739 (hA_nonneg : ∀ i j, 0 ≤ A i j) :
740 ReggeComponentComparison (laplacianReggeData A hA) where
741 geometricArea := A
742 geometricArea_symm := hA
743 geometricArea_nonneg := hA_nonneg
744 offDiag_component_match := by
745 intro i j hij
746 rw [bilinearCoefficient_laplacianReggeData A hA]
747 unfold laplacianCoefficient
748 simp [hij]
749 schlaefli_row_sum := schlaefliRowSum_laplacianReggeData A hA
750
751/-- With `laplacianReggeData`, the component comparison theorem specializes the
752general comparison result to the expected geometric Dirichlet form. -/
753theorem componentComparison_laplacianReggeData_dirichlet {n : ℕ}
754 (A : Fin n → Fin n → ℝ)
755 (hA : ∀ i j, A i j = A j i)
756 (hA_nonneg : ∀ i j, 0 ≤ A i j)
757 (ε : LogPotential n) :
758 secondOrderReggeAction (laplacianReggeData A hA) ε
759 = (1 / 2) * dirichletForm A ε :=
760by
761 simpa [laplacianReggeData_componentComparison] using
762 componentComparison_gives_geometric_dirichlet
763 (laplacianReggeData A hA)
764 (laplacianReggeData_componentComparison A hA hA_nonneg)
765 ε
766
767/-- **UNCONDITIONAL FLAT-SECTOR REDUCTION.** For any symmetric edge-area
768 weights `A`, the graph-Laplacian second-variation data automatically
769 satisfies the Schläfli row sum and the weak-field conformal Regge
770 action reduces to the Dirichlet form with weights `A`. -/
771theorem weak_field_conformal_reduction_laplacianData {n : ℕ}
772 (A : Fin n → Fin n → ℝ) (hA : ∀ i j, A i j = A j i)
773 (ε : LogPotential n) :
774 secondOrderReggeAction (laplacianReggeData A hA) ε
775 = (1 / 2) * dirichletForm A ε := by
776 rw [weak_field_conformal_reduction
777 (laplacianReggeData A hA)
778 (schlaefliRowSum_laplacianReggeData A hA) ε]
779 rw [dirichletForm_edgeArea_laplacianReggeData A hA ε]
780
781theorem weak_field_conformal_reduction_laplacianData_kappa {n : ℕ}
782 (A : Fin n → Fin n → ℝ) (hA : ∀ i j, A i j = A j i)
783 (κ : ℝ) (hκ : κ ≠ 0) (ε : LogPotential n) :
784 secondOrderReggeAction (laplacianReggeData A hA) ε / κ
785 = (1 / κ) * (1 / 2) * dirichletForm A ε := by
786 rw [weak_field_conformal_reduction_laplacianData A hA ε]
787 field_simp
788
789/-! ## §6. Certificate -/
790
791structure WeakFieldConformalReggeCert where
792 conformal_exact : ∀ {n : ℕ} (a : ℝ) (ha : 0 < a) (ε : LogPotential n)
793 (i j : Fin n),
794 (conformal_edge_length_field a ha ε).length i j ^ 2
795 = a ^ 2 * Real.exp (ε i + ε j)
796 conformal_taylor2 : ∀ {n : ℕ} (a : ℝ) (ha : 0 < a) (ε : LogPotential n)
797 (i j : Fin n),
798 (conformal_edge_length_field a ha ε).length i j ^ 2 / a ^ 2
799 = 1 + (ε i + ε j) + (ε i + ε j) ^ 2 / 2
800 + conformal_remainder (ε i + ε j)
801 graph_laplacian_decomp : ∀ {n : ℕ} (M : Fin n → Fin n → ℝ),
802 (∀ i j, M i j = M j i) → (∀ i, ∑ j : Fin n, M i j = 0) →
803 ∀ ε, quadraticForm M ε = - dirichletForm M ε
804 reduction : ∀ {n : ℕ} (W : WeakFieldReggeData n),
805 SchlaefliRowSum W → ∀ ε,
806 secondOrderReggeAction W ε
807 = (1 / 2) * dirichletForm (edgeArea W) ε
808 reduction_kappa : ∀ {n : ℕ} (W : WeakFieldReggeData n),
809 SchlaefliRowSum W → ∀ (κ : ℝ), κ ≠ 0 → ∀ ε,
810 secondOrderReggeAction W ε / κ
811 = (1 / κ) * (1 / 2) * dirichletForm (edgeArea W) ε
812 row_sum_discharged_laplacian : ∀ {n : ℕ}
813 (A : Fin n → Fin n → ℝ) (hA : ∀ i j, A i j = A j i),
814 SchlaefliRowSum (laplacianReggeData A hA)
815 reduction_laplacian : ∀ {n : ℕ}
816 (A : Fin n → Fin n → ℝ) (hA : ∀ i j, A i j = A j i)
817 (ε : LogPotential n),
818 secondOrderReggeAction (laplacianReggeData A hA) ε
819 = (1 / 2) * dirichletForm A ε
820 reduction_laplacian_kappa : ∀ {n : ℕ}
821 (A : Fin n → Fin n → ℝ) (hA : ∀ i j, A i j = A j i)
822 (κ : ℝ), κ ≠ 0 → ∀ ε : LogPotential n,
823 secondOrderReggeAction (laplacianReggeData A hA) ε / κ
824 = (1 / κ) * (1 / 2) * dirichletForm A ε
825 flat_vanishing_action : ∀ {n : ℕ} (W : WeakFieldReggeData n),
826 secondOrderReggeAction W (fun _ : Fin n => (0 : ℝ)) = 0
827 flat_vanishing_dirichlet : ∀ {n : ℕ} (M : Fin n → Fin n → ℝ),
828 dirichletForm M (fun _ : Fin n => (0 : ℝ)) = 0
829 remainder_flat : conformal_remainder 0 = 0
830
831theorem weakFieldConformalReggeCert : WeakFieldConformalReggeCert where
832 conformal_exact := fun a ha ε i j => conformal_length_sq_exact a ha ε i j
833 conformal_taylor2 := fun a ha ε i j => conformal_length_sq_taylor2 a ha ε i j
834 graph_laplacian_decomp := fun M hsymm hrow ε =>
835 dirichlet_eq_neg_quadratic M hsymm hrow ε
836 reduction := fun W hSchl ε => weak_field_conformal_reduction W hSchl ε
837 reduction_kappa := fun W hSchl κ hκ ε =>
838 weak_field_conformal_reduction_kappa W hSchl κ hκ ε
839 row_sum_discharged_laplacian := fun A hA =>
840 schlaefliRowSum_laplacianReggeData A hA
841 reduction_laplacian := fun A hA ε =>
842 weak_field_conformal_reduction_laplacianData A hA ε
843 reduction_laplacian_kappa := fun A hA κ hκ ε =>
844 weak_field_conformal_reduction_laplacianData_kappa A hA κ hκ ε
845 flat_vanishing_action := fun W => secondOrderReggeAction_flat W
846 flat_vanishing_dirichlet := fun M => dirichletForm_flat M
847 remainder_flat := conformal_remainder_zero
848
849end
850
851end WeakFieldConformalRegge
852end Gravity
853end IndisputableMonolith
854