Encyclopedia Gravity Gravity Weak Field Conformal Regge
ARTICLE 4 claims 4 theorems
Gravity Weak Field Conformal Regge
A machine-checked proof shows that the leading correction to Einstein's gravity, when written on a discrete lattice, is a simple energy that penalizes differences between neighboring points.
The reduction
In 1961, Tullio Regge proposed a way to do general relativity without coordinates. Instead of a smooth spacetime, he used a lattice of flat pieces, like a geodesic dome, and wrote the gravitational action as a sum over the hinges of the lattice. Each hinge contributes its area times a deficit angle, a measure of how much the surrounding flat pieces fail to lie flat. This is the Regge action, S = (1/κ) · Σ_h A_h · δ_h, where κ is the gravitational coupling, A_h is the area of a hinge, and δ_h is the deficit angle.
The module in question proves, in a machine-checked library of formal theorems, what happens to this action when the lattice is gently deformed. The deformation is a conformal one: each edge length is multiplied by a factor that is the exponential of the average of two numbers, one attached to each endpoint. These numbers, the log-potential values, are the degrees of freedom. Expanding the action to second order in these small numbers, the module shows that the result is a sum over edges of the square of the difference between the two endpoint values, weighted by a geometric coefficient.
This is the key structural result. The second-order Regge action, under the conformal ansatz, becomes a Dirichlet form: an energy that is zero when all the log-potential values are equal, and positive otherwise. The proof rests on two algebraic facts. First, the second-order Taylor expansion of the exponential is exact, with a remainder that is named and handled. Second, for any symmetric matrix with zero row sums, the quadratic form in the log-potentials equals minus one half the Dirichlet form in their differences. This is the graph-Laplacian decomposition.
The reduction is conditional. The module does not compute the geometric coefficients, the areas and deficit angles, from the underlying lattice. That is a separate geometric task, which the module packages as a structure called WeakFieldReggeData. The theorem states that once those coefficients satisfy a row-sum condition, the Schläfli identity, the reduction to the Dirichlet form is formal. The proof has no gaps and no extra axioms.
What this establishes, in plain language, is that the leading correction to discrete gravity, in the conformal sector, is a simple diffusion-like energy. This is the kind of result that makes the framework's claim that gravity is a derived phenomenon concrete: the weak-field limit of the Regge action is not an arbitrary collection of terms, but a specific, recognizable object. The module is a step toward showing that the Einstein-Hilbert action, and its lattice version, emerges from the framework's first principles.
In Recognition Science, this is not a derivation of gravity from the framework's axioms. It is a theorem about the Regge action, which is a classical object. The framework's contribution is to provide the context in which this reduction is a step, not the whole story. The module is a formal proof of a classical result, and it is a piece of the larger project of showing that the framework's structure, with its discrete ledger of recognition events, can give rise to the geometry of spacetime.
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
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 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 SchlaefliRowSum · IndisputableMonolith/Gravity/WeakFieldConformalRegge.lean
/-- The *Schläfli-derived row-sum vanishing* property. On a flat
background, the deficit-angle linearization satisfies Schläfli's
identity, which forces the bilinear-coefficient matrix to have
zero row sums when contracted with the conformal mode.
Concretely: for each vertex `i`,
`Σ_j dArea_{ij} · dDeficit_{ij} = 0`.
This is the geometric content of "uniform `ξ ≡ c` produces no
curvature change" combined with Schläfli's identity. -/
def SchlaefliRowSum {n : ℕ} (W : WeakFieldReggeData n) : Prop :=
∀ i : Fin n, ∑ j : Fin n, bilinearCoefficient W i j = 0
What this page does not claim
This module does not derive the Regge action from Recognition Science first principles. This module does not compute the geometric coefficients from a specific lattice. This module does not prove that the Einstein-Hilbert action emerges from the framework.
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 Regge second-variation coefficients computed from Cayley-Menger or dihedral formulas?
- Which lattices satisfy the Schläfli row-sum condition, and what does that condition mean geometrically?
- How does the Dirichlet form on a lattice relate to the continuum Laplacian in the smooth limit?
- What is the physical interpretation of the log-potential values in the conformal sector?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
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] ringThe second-order conformal Regge action equals one half the Dirichlet form on the edge areas. weak_field_conformal_reduction · 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 the Dirichlet form. dirichlet_eq_neg_quadratic · 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 second-order Taylor expansion of the conformal edge length squared has an explicit remainder. conformal_length_sq_decomposition · IndisputableMonolith/Gravity/WeakFieldConformalRegge.leanTHEOREM SchlaefliRowSum · IndisputableMonolith/Gravity/WeakFieldConformalRegge.lean
/-- The *Schläfli-derived row-sum vanishing* property. On a flat background, the deficit-angle linearization satisfies Schläfli's identity, which forces the bilinear-coefficient matrix to have zero row sums when contracted with the conformal mode. Concretely: for each vertex `i`, `Σ_j dArea_{ij} · dDeficit_{ij} = 0`. This is the geometric content of "uniform `ξ ≡ c` produces no curvature change" combined with Schläfli's identity. -/ def SchlaefliRowSum {n : ℕ} (W : WeakFieldReggeData n) : Prop := ∀ i : Fin n, ∑ j : Fin n, bilinearCoefficient W i j = 0The reduction is conditional on the geometric coefficients satisfying the Schläfli row-sum condition. SchlaefliRowSum · IndisputableMonolith/Gravity/WeakFieldConformalRegge.lean