Gravity Weak Field Conformal Regge Component Comparison Laplacian Regge Data Dir

The Dirichlet reduction

Regge calculus is a way of doing general relativity without coordinates. Instead of a smooth spacetime, one builds a network of flat triangular pieces, like a geodesic dome, and writes the gravitational action as a sum over the edges of the network. In 1961 Tullio Regge showed that this sum, involving each edge's length and the angle by which surrounding pieces fail to lie flat, approaches the usual continuum action as the network is refined. The framework's library of machine-checked formal theorems studies this discrete action in a special limit.

The limit in question is the weak-field, conformal one. Imagine each edge length is allowed to vary only through a small, smoothly varying factor attached to its endpoints, a conformal mode. Expanding the Regge action to second order in this small variation produces a quadratic form: a sum over pairs of points of a coefficient times the square of the difference between the variations at the two points. That expression is the Dirichlet form, the same mathematical object that measures the energy of a stretched membrane or the dissipation in a resistor network. The central theorem, componentComparison_laplacianReggeData_dirichlet, proves that for a symmetric, nonnegative matrix of such coefficients, the second-order Regge action is exactly one half times this Dirichlet form.

The proof rests on a structural identity. For any symmetric matrix whose row sums vanish, the quadratic form built from products of the variations equals minus one half the Dirichlet form built from their squared differences. This identity, proved in the library, is what converts the Regge bilinear form into the Dirichlet form. The vanishing row-sum condition is the discrete analogue of the Schläfli identity, a classical fact about how the volume of a polyhedron changes when its dihedral angles vary. The library packages this condition as a hypothesis, and the theorem shows that when it holds, the reduction is exact.

What the theorem does not claim is equally important. It does not compute the geometric coefficients that appear in the action from the actual edge lengths and angles of a lattice. That computation, from Cayley–Menger determinants or a specialization of the Piran–Williams perturbation, remains a separate geometric task. The theorem is conditional: once those coefficients are supplied and the row-sum condition verified, the Dirichlet reduction follows formally. It also does not assert that any particular lattice, such as a cubic one, satisfies the row-sum condition; that is a geometric fact to be checked case by case.

The payoff is a clean separation of concerns. The algebraic heart of the weak-field conformal reduction is now a proved theorem, independent of any particular lattice geometry. A researcher who wants to apply it to a specific network knows exactly what remains to be checked: the geometric coefficients and their row sums. This turns a messy calculation into a well-defined verification task, and it opens the door to studying the resulting Dirichlet form with the full machinery of spectral theory, the same tools used for diffusion and vibration problems.

/-- With `laplacianReggeData`, the component comparison theorem specializes the
general comparison result to the expected geometric Dirichlet form. -/
theorem componentComparison_laplacianReggeData_dirichlet {n : ℕ}
    (A : Fin n → Fin n → ℝ)
    (hA : ∀ i j, A i j = A j i)
    (hA_nonneg : ∀ i j, 0 ≤ A i j)
    (ε : LogPotential n) :
    secondOrderReggeAction (laplacianReggeData A hA) ε
      = (1 / 2) * dirichletForm A ε :=
by
  simpa [laplacianReggeData_componentComparison] using
    componentComparison_gives_geometric_dirichlet
      (laplacianReggeData A hA)
      (laplacianReggeData_componentComparison A hA hA_nonneg)
      ε

/-- **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

/-- 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

The geometric coefficients of the Regge action are not computed from edge lengths and angles in this theorem. No particular lattice is shown to satisfy the Schläfli row-sum condition. The theorem does not apply to non-conformal perturbations of the edge lengths.

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: