Encyclopedia Gravity Gravity Weak Field Conformal Regge Weak Field Conformal Reduction Kappa

ARTICLE 3 claims 3 theorems

Gravity Weak Field Conformal Regge Weak Field Conformal Reduction Kappa

In Regge's discrete gravity, a weak-field conformal perturbation turns the action into a sum of squared differences, a machine-checked theorem.

Verify this page

The reduction theorem

Regge calculus is a way of doing general relativity without coordinates: space is chopped into flat pieces, and the geometry lives in the edge lengths of that triangulation. The action is a sum over hinges, each term an area times a deficit angle, a measure of how much the surrounding flat pieces fail to lie flat. In 1961 Tullio Regge wrote this down, and in 1986 Tsvi Piran and Ruth Williams studied small perturbations of it. This page concerns a particular perturbation, one that changes every edge length by a common scale factor, a conformal mode.

When the perturbation is weak, the action simplifies dramatically. Write the edge length as a base length times an exponential of a potential at each vertex. Expanding to second order in that potential, the action becomes a quadratic form. The theorem weak_field_conformal_reduction_kappa, proved in the framework's machine-checked library of formal theorems, states that under a row-sum condition, this second-order action divided by the coupling constant equals a Dirichlet form: a sum over edges of the squared difference of the potentials, weighted by an area factor. In symbols, S(2)/κ = (1/κ) · ½ · Σ⟨i,j⟩ Aij (ξi − ξj)2. The row-sum condition, named after the geometer Ludwig Schläfli, says that for each vertex the sum of the bilinear coefficients over all neighbors is zero; it is what makes the quadratic form depend only on differences, not on the overall level of the potential.

The proof is algebraic and fully formal: it combines an exact Taylor expansion of the squared edge length with a graph-Laplacian identity. The library shows that for any symmetric matrix with zero row sums, the quadratic form equals minus one half the Dirichlet form on differences. The theorem itself is conditional: it assumes the geometric coefficients (the area and deficit responses) are supplied and that they satisfy the Schläfli row-sum condition. The library does not compute those coefficients from Cayley–Menger or dihedral formulas; that remains a geometric input, not a proved result. The reduction is a structural bridge: once the geometry is in place, the action is a discrete energy.

What the theorem does not claim is equally important. It does not say that the Schläfli row-sum condition holds for any particular lattice, nor that the area weights are nonnegative; those are separate hypotheses. It does not derive the coupling constant κ from anything; κ is a parameter, only required to be nonzero. And it does not establish that the conformal mode is the only perturbation, or that the full Regge action reduces this way; Piran and Williams treated a more general perturbation. The theorem is a conditional algebraic fact, not a complete theory of weak-field Regge gravity.

THEOREM weak_field_conformal_reduction_kappa · IndisputableMonolith/Gravity/WeakFieldConformalRegge.lean
weak_field_conformal_reduction_kappa · IndisputableMonolith/Gravity/WeakFieldConformalRegge.lean:498 
/-- **JON'S EQUATION (d).**

    Multiplying the reduction by `1/κ` and dividing by 2 to absorb the
    factor at the head of `dirichletForm`:

        secondOrderReggeAction W ε / κ
            = (1/κ) · Σ_⟨i,j⟩ ½ · (ξ_i − ξ_j)² · A_{ij}.

    The `Σ_⟨i,j⟩ ½ · (ξ_i − ξ_j)² · A_{ij}` form is the "ordered pair"
    Dirichlet form `(1/2) · dirichletForm`. Below we record the
    explicit κ-normalized identity. -/
theorem weak_field_conformal_reduction_kappa
    {n : ℕ} (W : WeakFieldReggeData n)
    (hSchl : SchlaefliRowSum W)
    (κ : ℝ) (hκ : κ ≠ 0)
    (ε : LogPotential n) :
    secondOrderReggeAction W ε / κ
      = (1 / κ) * (1 / 2) * dirichletForm (edgeArea W) ε := by
  rw [weak_field_conformal_reduction W hSchl ε]
  field_simp
THEOREM conformal_length_sq_decomposition · dirichlet_eq_neg_quadratic · IndisputableMonolith/Gravity/WeakFieldConformalRegge.lean
conformal_length_sq_decomposition · IndisputableMonolith/Gravity/WeakFieldConformalRegge.lean:145 
/-- 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
dirichlet_eq_neg_quadratic · IndisputableMonolith/Gravity/WeakFieldConformalRegge.lean:187 
/-- **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_kappa · IndisputableMonolith/Gravity/WeakFieldConformalRegge.lean
weak_field_conformal_reduction_kappa · IndisputableMonolith/Gravity/WeakFieldConformalRegge.lean:498 
/-- **JON'S EQUATION (d).**

    Multiplying the reduction by `1/κ` and dividing by 2 to absorb the
    factor at the head of `dirichletForm`:

        secondOrderReggeAction W ε / κ
            = (1/κ) · Σ_⟨i,j⟩ ½ · (ξ_i − ξ_j)² · A_{ij}.

    The `Σ_⟨i,j⟩ ½ · (ξ_i − ξ_j)² · A_{ij}` form is the "ordered pair"
    Dirichlet form `(1/2) · dirichletForm`. Below we record the
    explicit κ-normalized identity. -/
theorem weak_field_conformal_reduction_kappa
    {n : ℕ} (W : WeakFieldReggeData n)
    (hSchl : SchlaefliRowSum W)
    (κ : ℝ) (hκ : κ ≠ 0)
    (ε : LogPotential n) :
    secondOrderReggeAction W ε / κ
      = (1 / κ) * (1 / 2) * dirichletForm (edgeArea W) ε := by
  rw [weak_field_conformal_reduction W hSchl ε]
  field_simp

What this page does not claim

The theorem does not compute the geometric coefficients from Cayley–Menger data. The theorem does not prove the Schläfli row-sum condition for any particular lattice. The theorem does not derive the value of the coupling constant κ.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND