Encyclopedia Gravity Gravity Weak Field Conformal Regge Dirichlet Form Edge Area Laplacian Regge Data
ARTICLE 4 claims 4 theorems
Gravity Weak Field Conformal Regge Dirichlet Form Edge Area Laplacian Regge Data
In the weak-field limit, the Regge action for gravity becomes a simple sum of squared differences between neighboring points, a form familiar from the mathematics of diffusion and vibration.
The Dirichlet reduction
Regge calculus is a way of doing general relativity without coordinates: space is chopped into flat triangular pieces, and the curvature is carried by the angles where the pieces meet. The action, a quantity whose minimization gives the equations of motion, is a sum over the edges of the lattice of each edge's area times the angle deficit at that edge. The declaration dirichletForm_edgeArea_laplacianReggeData proves an algebraic identity about the second-order, weak-field version of that action.
The classical result, known since the 1980s work of Piran and Williams, is that when the edge lengths are perturbed only by a conformal factor (a single scale factor that varies from vertex to vertex), the second-order action reduces to a sum of squared differences of that factor across each edge. The new theorem packages this reduction in a machine-checked library of formal theorems. It states that for any symmetric matrix of edge areas, the second-order Regge action equals one half of the Dirichlet form, a standard quadratic expression: (1/2) Σi,j Aij(εi − εj)2, where εi is the conformal perturbation at vertex i and Aij is the edge area between i and j.
The proof rests on two algebraic facts, both fully verified. First, the exact expansion of the squared edge length in terms of the conformal field: ℓij2/ℓ02 = 1 + (εi + εj) + ½(εi + εj)2 + remainder, where the remainder is exactly the Taylor remainder of the exponential function. Second, a structural identity: for any symmetric matrix with zero row sums, the quadratic form Σi,j Mij εi εj equals −½ Σi,j Mij (εi − εj)2. This identity is what converts the Regge bilinear form into the Dirichlet form.
The theorem is conditional: it assumes the geometric input, packaged as WeakFieldReggeData, which provides the first-order responses of area and deficit angle to the conformal perturbation. It also assumes a row-sum condition, named after Schläfli, that those coefficients must satisfy. The library proves that if those conditions hold, the reduction is formal. It does not compute the actual area and deficit responses from the Cayley–Menger formulas or verify the row-sum condition for any specific lattice; those remain as geometric tasks.
Within the framework, this reduction is a step toward showing that gravity, in the weak-field conformal limit, behaves like a simple lattice field theory whose energy is a sum of squared differences. The practical consequence is that the Regge action becomes a discrete version of the familiar continuum Laplacian, which opens the door to standard tools from graph theory and spectral analysis. What the theorem does not do is claim that the geometric coefficients are known, or that the reduction holds for any particular physical lattice without the Schläfli condition being checked.
THEOREM dirichletForm_edgeArea · IndisputableMonolith/Gravity/WeakFieldConformalRegge.lean
/-- The Dirichlet form on `edgeArea W` is the negation of the Dirichlet
form on `bilinearCoefficient W`. Direct from `dirichletForm_neg`
plus the definition `edgeArea = − bilinearCoefficient`. -/
theorem dirichletForm_edgeArea
{n : ℕ} (W : WeakFieldReggeData n) (ε : LogPotential n) :
dirichletForm (edgeArea W) ε
= - dirichletForm (bilinearCoefficient W) ε := by
have h := dirichletForm_neg (bilinearCoefficient W) ε
-- `(fun i j => - bilinearCoefficient W i j)` is definitionally `edgeArea W`.
exact h
THEOREM conformal_length_sq_decomposition · IndisputableMonolith/Gravity/WeakFieldConformalRegge.lean
/-- The conformal expansion writes `ℓ²/ℓ_0² − 1 − δ¹ − δ²` as the
remainder. This is a tautology after `conformal_length_sq_taylor2`
but it is the form that downstream "second-order action" reductions
need. -/
theorem conformal_length_sq_decomposition
{n : ℕ} (a : ℝ) (ha : 0 < a) (ε : LogPotential n) (i j : Fin n) :
(conformal_edge_length_field a ha ε).length i j ^ 2 / a ^ 2
= 1 + edgeSqFirstOrder ε i j + edgeSqSecondOrder ε i j
+ conformal_remainder (ε i + ε j) := by
unfold edgeSqFirstOrder edgeSqSecondOrder
exact conformal_length_sq_taylor2 a ha ε i j
THEOREM dirichlet_eq_neg_quadratic · IndisputableMonolith/Gravity/WeakFieldConformalRegge.lean
/-- **GRAPH-LAPLACIAN DECOMPOSITION.**
For symmetric `M` with zero row sums,
`Q[ξ; M] = −D[ξ; M]`.
This is the algebraic core of the weak-field reduction. -/
theorem dirichlet_eq_neg_quadratic
{n : ℕ} (M : Fin n → Fin n → ℝ)
(hsymm : ∀ i j, M i j = M j i)
(hrow : ∀ i, ∑ j : Fin n, M i j = 0)
(ε : LogPotential n) :
quadraticForm M ε = - dirichletForm M ε := by
unfold quadraticForm dirichletForm
-- Expand `(ε i − ε j)² = ε i² − 2 ε i ε j + ε j²` and sum.
have hkey : ∀ i j, M i j * (ε i - ε j) ^ 2
= M i j * (ε i) ^ 2 - 2 * (M i j * ε i * ε j)
+ M i j * (ε j) ^ 2 := by
intro i j; ring
-- Sum the identity term-by-term.
have hsum : ∑ i : Fin n, ∑ j : Fin n, M i j * (ε i - ε j) ^ 2
= (∑ i : Fin n, ∑ j : Fin n, M i j * (ε i) ^ 2)
- 2 * (∑ i : Fin n, ∑ j : Fin n, M i j * ε i * ε j)
+ (∑ i : Fin n, ∑ j : Fin n, M i j * (ε j) ^ 2) := by
have h1 : ∀ i, ∑ j : Fin n, M i j * (ε i - ε j) ^ 2
= ∑ j : Fin n, (M i j * (ε i) ^ 2 - 2 * (M i j * ε i * ε j)
+ M i j * (ε j) ^ 2) := by
intro i; exact Finset.sum_congr rfl (fun j _ => hkey i j)
simp only [h1, Finset.sum_add_distrib, Finset.sum_sub_distrib]
have hpull : ∀ i, ∑ j : Fin n, 2 * (M i j * ε i * ε j)
= 2 * ∑ j : Fin n, M i j * ε i * ε j := by
intro i
exact (Finset.mul_sum _ _ _).symm
simp only [hpull, ← Finset.mul_sum]
-- Use the row-sum condition on the `ε i² · M i j` and `ε j² · M i j` pieces.
have hi2 : ∑ i : Fin n, ∑ j : Fin n, M i j * (ε i) ^ 2 = 0 := by
have hpull : ∀ i, ∑ j : Fin n, M i j * (ε i) ^ 2
= (∑ j : Fin n, M i j) * (ε i) ^ 2 := fun i =>
sum_const_mul_right (fun j => M i j) ((ε i) ^ 2)
simp only [hpull, hrow, zero_mul, Finset.sum_const_zero]
have hj2 : ∑ i : Fin n, ∑ j : Fin n, M i j * (ε j) ^ 2 = 0 := by
-- Swap order, then `hrow` (transposed via symmetry).
rw [Finset.sum_comm]
have hpull : ∀ j, ∑ i : Fin n, M i j * (ε j) ^ 2
= (∑ i : Fin n, M i j) * (ε j) ^ 2 := fun j =>
sum_const_mul_right (fun i => M i j) ((ε j) ^ 2)
have hrow' : ∀ j, ∑ i : Fin n, M i j = 0 := by
intro j
have heq : ∑ i : Fin n, M i j = ∑ i : Fin n, M j i :=
Finset.sum_congr rfl (fun i _ => hsymm i j)
rw [heq]; exact hrow j
simp only [hpull, hrow', zero_mul, Finset.sum_const_zero]
-- Plug back in.
rw [hsum, hi2, hj2]
ring
THEOREM weak_field_conformal_reduction · IndisputableMonolith/Gravity/WeakFieldConformalRegge.lean
/-- **WEAK-FIELD CONFORMAL REDUCTION (the main theorem).**
Under the Schläfli row-sum hypothesis (§3) on the linearization
data `W`, the second-order Regge action equals the discrete
Dirichlet energy on the conformal mode `ε`, with edge weights
`A_{ij} = − dArea_{ij} · dDeficit_{ij}`:
secondOrderReggeAction W ε
= (1/2) · Σ_{i,j} ½ · (ε i − ε j)² · A_{ij}
= ½ · dirichletForm A ε.
Multiplying through by `1/κ` recovers Jon's equation (d):
S^(2)/κ = (1/κ) · Σ_⟨i,j⟩ ½ · (ξ_i − ξ_j)² · A_{ij}.
Proof:
1. Expand `(ξ_i + ξ_j)² = ξ_i² + 2 ξ_i ξ_j + ξ_j²`.
2. The `ξ_i²` and `ξ_j²` pieces collapse via Schläfli row-sum.
3. The `2 ξ_i ξ_j` piece is `quadraticForm M ε = − dirichletForm M ε`
by `dirichlet_eq_neg_quadratic` (§2).
4. `dirichletForm (edgeArea W) ε = − dirichletForm M ε`
by `dirichletForm_edgeArea`.
Combining: LHS = `(1/4)·(0 + 2·(−D) + 0) = −D/2 = (1/2)·(−D)
= (1/2) · dirichletForm (edgeArea W) ε = RHS`. -/
theorem weak_field_conformal_reduction
{n : ℕ} (W : WeakFieldReggeData n)
(hSchl : SchlaefliRowSum W)
(ε : LogPotential n) :
secondOrderReggeAction W ε
= (1 / 2) * dirichletForm (edgeArea W) ε := by
-- Abbreviations.
set M : Fin n → Fin n → ℝ := bilinearCoefficient W with hM_def
-- Step 1: expand the square.
have hexp : ∀ i j, M i j * (ε i + ε j) ^ 2
= M i j * (ε i) ^ 2
+ 2 * (M i j * ε i * ε j)
+ M i j * (ε j) ^ 2 := by
intro i j; ring
-- Sum over i, j.
have hsum : ∑ i : Fin n, ∑ j : Fin n, M i j * (ε i + ε j) ^ 2
= (∑ i : Fin n, ∑ j : Fin n, M i j * (ε i) ^ 2)
+ 2 * (∑ i : Fin n, ∑ j : Fin n, M i j * ε i * ε j)
+ (∑ i : Fin n, ∑ j : Fin n, M i j * (ε j) ^ 2) := by
have h1 : ∀ i, ∑ j : Fin n, M i j * (ε i + ε j) ^ 2
= ∑ j : Fin n, (M i j * (ε i) ^ 2
+ 2 * (M i j * ε i * ε j)
+ M i j * (ε j) ^ 2) := fun i =>
Finset.sum_congr rfl (fun j _ => hexp i j)
simp only [h1, Finset.sum_add_distrib]
have hpull : ∀ i, ∑ j : Fin n, 2 * (M i j * ε i * ε j)
= 2 * ∑ j : Fin n, M i j * ε i * ε j := fun i =>
(Finset.mul_sum _ _ _).symm
simp only [hpull, ← Finset.mul_sum]
-- Step 2: the (ε i)² and (ε j)² pieces vanish under Schläfli row-sum.
have hSchl_M : ∀ i : Fin n, ∑ j : Fin n, M i j = 0 := hSchl
have hi2 : ∑ i : Fin n, ∑ j : Fin n, M i j * (ε i) ^ 2 = 0 := by
have hpull : ∀ i, ∑ j : Fin n, M i j * (ε i) ^ 2
= (∑ j : Fin n, M i j) * (ε i) ^ 2 := fun i =>
sum_const_mul_right (fun j => M i j) ((ε i) ^ 2)
simp only [hpull, hSchl_M, zero_mul, Finset.sum_const_zero]
have hSchl_col : ∀ j : Fin n, ∑ i : Fin n, M i j = 0 := by
intro j
have heq : ∑ i : Fin n, M i j = ∑ i : Fin n, M j i :=
Finset.sum_congr rfl (fun i _ => bilinearCoefficient_symm W i j)
rw [heq]; exact hSchl_M j
have hj2 : ∑ i : Fin n, ∑ j : Fin n, M i j * (ε j) ^ 2 = 0 := by
rw [Finset.sum_comm]
have hpull : ∀ j, ∑ i : Fin n, M i j * (ε j) ^ 2
= (∑ i : Fin n, M i j) * (ε j) ^ 2 := fun j =>
sum_const_mul_right (fun i => M i j) ((ε j) ^ 2)
simp only [hpull, hSchl_col, zero_mul, Finset.sum_const_zero]
-- Step 3: rewrite the cross term via §2.
have hQ : quadraticForm M ε = - dirichletForm M ε :=
dirichlet_eq_neg_quadratic M (bilinearCoefficient_symm W) hSchl ε
-- Step 4: rewrite the goal RHS via `dirichletForm_edgeArea`.
rw [dirichletForm_edgeArea W ε]
-- Now expand the LHS.
unfold secondOrderReggeAction
rw [show (∑ i : Fin n, ∑ j : Fin n, bilinearCoefficient W i j * (ε i + ε j) ^ 2)
= (∑ i : Fin n, ∑ j : Fin n, M i j * (ε i + ε j) ^ 2) from rfl]
rw [hsum, hi2, hj2]
-- Goal: `(1/4) * (0 + 2 * Σ Σ M i j * ε i * ε j + 0) = (1/2) * (- D)`.
unfold quadraticForm at hQ
rw [hQ]
ring
What this page does not claim
The geometric coefficients are not computed from Cayley–Menger data. The Schläfli row-sum condition is not verified for any specific lattice. The reduction does not apply to perturbations that mix the conformal mode with other modes. The theorem does not claim that the Dirichlet form is the full Regge action beyond second order.
Verify this page
Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:
$ lake env lean IndisputableMonolith/Gravity/WeakFieldConformalRegge.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)
A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.
Derived articles
This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red:
- How are the first-order area and deficit responses computed from Cayley–Menger formulas?
- For which lattices does the Schläfli row-sum condition hold?
- Does the Dirichlet form reduction extend to non-conformal perturbations?
- How does the discrete Laplacian here connect to the continuum Laplacian in the continuum limit?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
THEOREM dirichletForm_edgeArea · IndisputableMonolith/Gravity/WeakFieldConformalRegge.lean
/-- The Dirichlet form on `edgeArea W` is the negation of the Dirichlet form on `bilinearCoefficient W`. Direct from `dirichletForm_neg` plus the definition `edgeArea = − bilinearCoefficient`. -/ theorem dirichletForm_edgeArea {n : ℕ} (W : WeakFieldReggeData n) (ε : LogPotential n) : dirichletForm (edgeArea W) ε = - dirichletForm (bilinearCoefficient W) ε := by have h := dirichletForm_neg (bilinearCoefficient W) ε -- `(fun i j => - bilinearCoefficient W i j)` is definitionally `edgeArea W`. exact hFor any symmetric matrix of edge areas, the second-order Regge action equals one half of the Dirichlet form. dirichletForm_edgeArea · IndisputableMonolith/Gravity/WeakFieldConformalRegge.leanTHEOREM conformal_length_sq_decomposition · IndisputableMonolith/Gravity/WeakFieldConformalRegge.lean
/-- The conformal expansion writes `ℓ²/ℓ_0² − 1 − δ¹ − δ²` as the remainder. This is a tautology after `conformal_length_sq_taylor2` but it is the form that downstream "second-order action" reductions need. -/ theorem conformal_length_sq_decomposition {n : ℕ} (a : ℝ) (ha : 0 < a) (ε : LogPotential n) (i j : Fin n) : (conformal_edge_length_field a ha ε).length i j ^ 2 / a ^ 2 = 1 + edgeSqFirstOrder ε i j + edgeSqSecondOrder ε i j + conformal_remainder (ε i + ε j) := by unfold edgeSqFirstOrder edgeSqSecondOrder exact conformal_length_sq_taylor2 a ha ε i jThe exact expansion of the squared edge length in terms of the conformal field is ℓ<sub>ij</sub><sup>2</sup>/ℓ<sub>0</sub><sup>2</sup> = 1 + (ε<sub>i</sub> + ε<sub>j</sub>) + ½(ε<sub>i</sub> + ε<sub>j</sub>)<sup>2</sup> + remainder. conformal_length_sq_decomposition · IndisputableMonolith/Gravity/WeakFieldConformalRegge.leanTHEOREM dirichlet_eq_neg_quadratic · IndisputableMonolith/Gravity/WeakFieldConformalRegge.lean
/-- **GRAPH-LAPLACIAN DECOMPOSITION.** For symmetric `M` with zero row sums, `Q[ξ; M] = −D[ξ; M]`. This is the algebraic core of the weak-field reduction. -/ theorem dirichlet_eq_neg_quadratic {n : ℕ} (M : Fin n → Fin n → ℝ) (hsymm : ∀ i j, M i j = M j i) (hrow : ∀ i, ∑ j : Fin n, M i j = 0) (ε : LogPotential n) : quadraticForm M ε = - dirichletForm M ε := by unfold quadraticForm dirichletForm -- Expand `(ε i − ε j)² = ε i² − 2 ε i ε j + ε j²` and sum. have hkey : ∀ i j, M i j * (ε i - ε j) ^ 2 = M i j * (ε i) ^ 2 - 2 * (M i j * ε i * ε j) + M i j * (ε j) ^ 2 := by intro i j; ring -- Sum the identity term-by-term. have hsum : ∑ i : Fin n, ∑ j : Fin n, M i j * (ε i - ε j) ^ 2 = (∑ i : Fin n, ∑ j : Fin n, M i j * (ε i) ^ 2) - 2 * (∑ i : Fin n, ∑ j : Fin n, M i j * ε i * ε j) + (∑ i : Fin n, ∑ j : Fin n, M i j * (ε j) ^ 2) := by have h1 : ∀ i, ∑ j : Fin n, M i j * (ε i - ε j) ^ 2 = ∑ j : Fin n, (M i j * (ε i) ^ 2 - 2 * (M i j * ε i * ε j) + M i j * (ε j) ^ 2) := by intro i; exact Finset.sum_congr rfl (fun j _ => hkey i j) simp only [h1, Finset.sum_add_distrib, Finset.sum_sub_distrib] have hpull : ∀ i, ∑ j : Fin n, 2 * (M i j * ε i * ε j) = 2 * ∑ j : Fin n, M i j * ε i * ε j := by intro i exact (Finset.mul_sum _ _ _).symm simp only [hpull, ← Finset.mul_sum] -- Use the row-sum condition on the `ε i² · M i j` and `ε j² · M i j` pieces. have hi2 : ∑ i : Fin n, ∑ j : Fin n, M i j * (ε i) ^ 2 = 0 := by have hpull : ∀ i, ∑ j : Fin n, M i j * (ε i) ^ 2 = (∑ j : Fin n, M i j) * (ε i) ^ 2 := fun i => sum_const_mul_right (fun j => M i j) ((ε i) ^ 2) simp only [hpull, hrow, zero_mul, Finset.sum_const_zero] have hj2 : ∑ i : Fin n, ∑ j : Fin n, M i j * (ε j) ^ 2 = 0 := by -- Swap order, then `hrow` (transposed via symmetry). rw [Finset.sum_comm] have hpull : ∀ j, ∑ i : Fin n, M i j * (ε j) ^ 2 = (∑ i : Fin n, M i j) * (ε j) ^ 2 := fun j => sum_const_mul_right (fun i => M i j) ((ε j) ^ 2) have hrow' : ∀ j, ∑ i : Fin n, M i j = 0 := by intro j have heq : ∑ i : Fin n, M i j = ∑ i : Fin n, M j i := Finset.sum_congr rfl (fun i _ => hsymm i j) rw [heq]; exact hrow j simp only [hpull, hrow', zero_mul, Finset.sum_const_zero] -- Plug back in. rw [hsum, hi2, hj2] ringFor any symmetric matrix with zero row sums, the quadratic form equals minus one half of the Dirichlet form. dirichlet_eq_neg_quadratic · IndisputableMonolith/Gravity/WeakFieldConformalRegge.leanTHEOREM weak_field_conformal_reduction · IndisputableMonolith/Gravity/WeakFieldConformalRegge.lean
/-- **WEAK-FIELD CONFORMAL REDUCTION (the main theorem).** Under the Schläfli row-sum hypothesis (§3) on the linearization data `W`, the second-order Regge action equals the discrete Dirichlet energy on the conformal mode `ε`, with edge weights `A_{ij} = − dArea_{ij} · dDeficit_{ij}`: secondOrderReggeAction W ε = (1/2) · Σ_{i,j} ½ · (ε i − ε j)² · A_{ij} = ½ · dirichletForm A ε. Multiplying through by `1/κ` recovers Jon's equation (d): S^(2)/κ = (1/κ) · Σ_⟨i,j⟩ ½ · (ξ_i − ξ_j)² · A_{ij}. Proof: 1. Expand `(ξ_i + ξ_j)² = ξ_i² + 2 ξ_i ξ_j + ξ_j²`. 2. The `ξ_i²` and `ξ_j²` pieces collapse via Schläfli row-sum. 3. The `2 ξ_i ξ_j` piece is `quadraticForm M ε = − dirichletForm M ε` by `dirichlet_eq_neg_quadratic` (§2). 4. `dirichletForm (edgeArea W) ε = − dirichletForm M ε` by `dirichletForm_edgeArea`. Combining: LHS = `(1/4)·(0 + 2·(−D) + 0) = −D/2 = (1/2)·(−D) = (1/2) · dirichletForm (edgeArea W) ε = RHS`. -/ theorem weak_field_conformal_reduction {n : ℕ} (W : WeakFieldReggeData n) (hSchl : SchlaefliRowSum W) (ε : LogPotential n) : secondOrderReggeAction W ε = (1 / 2) * dirichletForm (edgeArea W) ε := by -- Abbreviations. set M : Fin n → Fin n → ℝ := bilinearCoefficient W with hM_def -- Step 1: expand the square. have hexp : ∀ i j, M i j * (ε i + ε j) ^ 2 = M i j * (ε i) ^ 2 + 2 * (M i j * ε i * ε j) + M i j * (ε j) ^ 2 := by intro i j; ring -- Sum over i, j. have hsum : ∑ i : Fin n, ∑ j : Fin n, M i j * (ε i + ε j) ^ 2 = (∑ i : Fin n, ∑ j : Fin n, M i j * (ε i) ^ 2) + 2 * (∑ i : Fin n, ∑ j : Fin n, M i j * ε i * ε j) + (∑ i : Fin n, ∑ j : Fin n, M i j * (ε j) ^ 2) := by have h1 : ∀ i, ∑ j : Fin n, M i j * (ε i + ε j) ^ 2 = ∑ j : Fin n, (M i j * (ε i) ^ 2 + 2 * (M i j * ε i * ε j) + M i j * (ε j) ^ 2) := fun i => Finset.sum_congr rfl (fun j _ => hexp i j) simp only [h1, Finset.sum_add_distrib] have hpull : ∀ i, ∑ j : Fin n, 2 * (M i j * ε i * ε j) = 2 * ∑ j : Fin n, M i j * ε i * ε j := fun i => (Finset.mul_sum _ _ _).symm simp only [hpull, ← Finset.mul_sum] -- Step 2: the (ε i)² and (ε j)² pieces vanish under Schläfli row-sum. have hSchl_M : ∀ i : Fin n, ∑ j : Fin n, M i j = 0 := hSchl have hi2 : ∑ i : Fin n, ∑ j : Fin n, M i j * (ε i) ^ 2 = 0 := by have hpull : ∀ i, ∑ j : Fin n, M i j * (ε i) ^ 2 = (∑ j : Fin n, M i j) * (ε i) ^ 2 := fun i => sum_const_mul_right (fun j => M i j) ((ε i) ^ 2) simp only [hpull, hSchl_M, zero_mul, Finset.sum_const_zero] have hSchl_col : ∀ j : Fin n, ∑ i : Fin n, M i j = 0 := by intro j have heq : ∑ i : Fin n, M i j = ∑ i : Fin n, M j i := Finset.sum_congr rfl (fun i _ => bilinearCoefficient_symm W i j) rw [heq]; exact hSchl_M j have hj2 : ∑ i : Fin n, ∑ j : Fin n, M i j * (ε j) ^ 2 = 0 := by rw [Finset.sum_comm] have hpull : ∀ j, ∑ i : Fin n, M i j * (ε j) ^ 2 = (∑ i : Fin n, M i j) * (ε j) ^ 2 := fun j => sum_const_mul_right (fun i => M i j) ((ε j) ^ 2) simp only [hpull, hSchl_col, zero_mul, Finset.sum_const_zero] -- Step 3: rewrite the cross term via §2. have hQ : quadraticForm M ε = - dirichletForm M ε := dirichlet_eq_neg_quadratic M (bilinearCoefficient_symm W) hSchl ε -- Step 4: rewrite the goal RHS via `dirichletForm_edgeArea`. rw [dirichletForm_edgeArea W ε] -- Now expand the LHS. unfold secondOrderReggeAction rw [show (∑ i : Fin n, ∑ j : Fin n, bilinearCoefficient W i j * (ε i + ε j) ^ 2) = (∑ i : Fin n, ∑ j : Fin n, M i j * (ε i + ε j) ^ 2) from rfl] rw [hsum, hi2, hj2] -- Goal: `(1/4) * (0 + 2 * Σ Σ M i j * ε i * ε j + 0) = (1/2) * (- D)`. unfold quadraticForm at hQ rw [hQ] ringThe reduction is conditional on the Schläfli row-sum condition and the geometric input. weak_field_conformal_reduction · IndisputableMonolith/Gravity/WeakFieldConformalRegge.lean