Encyclopedia Gravity Gravity Weak Field Conformal Regge Second Order Eq Half Laplacian Action

ARTICLE 3 claims 3 theorems

Gravity Weak Field Conformal Regge Second Order Eq Half Laplacian Action

A machine-checked theorem shows that, under one geometric condition, the weak-field gravity action simplifies to a sum over edge differences, a form familiar from lattice physics.

Verify this page

The reduction

The declaration secondOrder_eq_half_laplacian_action is a formal theorem in the framework's machine-checked library of formal theorems. It concerns the Regge action, a way of writing general relativity without coordinates by discretizing spacetime into flat simplices, or building blocks, whose edge lengths carry the geometry. In the weak-field limit, where the geometry is nearly flat, the action is expanded to second order in small perturbations. The theorem states that this second-order action equals one half times a Dirichlet form, a sum over edges of the squared difference of the perturbation values at the two endpoints, weighted by a geometric factor.

The proof is algebraic and conditional. It assumes a ledger, a discrete record of events or geometric data, with a symmetric matrix of coefficients that satisfies a row-sum condition, meaning each row adds to zero. Under that condition, the theorem shows that the bilinear form, a sum of products of perturbations, is identical to the Dirichlet form on differences. This is a structural identity: it converts a sum that mixes values at different points into a sum of squared differences, which is the standard form of a discrete energy or Laplacian. The result is fully proven with zero axioms, meaning it rests only on the framework's foundational logic.

The theorem does not compute the geometric coefficients themselves. Those coefficients, which describe how edge areas and deficit angles respond to perturbations, are supplied as input data. The row-sum condition, named after the Schläfli identity in geometry, is an assumption that must be verified for the chosen lattice. The framework packages this as a separate geometric task, not part of the algebraic proof. So the theorem is best read as a reduction: once the geometric input is available and the row-sum condition holds, the weak-field conformal Regge action is exactly one half the Dirichlet energy.

In practice, this means the framework has shown that a discrete gravity action, under specific conditions, takes the same mathematical shape as a lattice Laplacian. That connection matters because the Dirichlet form is well studied in physics and mathematics, appearing in elasticity, heat flow, and random walks. The theorem does not claim that the geometric coefficients have been derived from first principles, nor that the row-sum condition holds automatically for any lattice. Those remain open targets for the framework's ongoing work.

THEOREM weak_field_conformal_reduction · IndisputableMonolith/Gravity/WeakFieldConformalRegge.lean
weak_field_conformal_reduction · IndisputableMonolith/Gravity/WeakFieldConformalRegge.lean:412 
/-- **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
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 weakFieldConformalReggeCert · IndisputableMonolith/Gravity/WeakFieldConformalRegge.lean
weakFieldConformalReggeCert · IndisputableMonolith/Gravity/WeakFieldConformalRegge.lean:831 
theorem weakFieldConformalReggeCert : WeakFieldConformalReggeCert where
  conformal_exact := fun a ha ε i j => conformal_length_sq_exact a ha ε i j
  conformal_taylor2 := fun a ha ε i j => conformal_length_sq_taylor2 a ha ε i j
  graph_laplacian_decomp := fun M hsymm hrow ε =>
    dirichlet_eq_neg_quadratic M hsymm hrow ε
  reduction := fun W hSchl ε => weak_field_conformal_reduction W hSchl ε
  reduction_kappa := fun W hSchl κ hκ ε =>
    weak_field_conformal_reduction_kappa W hSchl κ hκ ε
  row_sum_discharged_laplacian := fun A hA =>
    schlaefliRowSum_laplacianReggeData A hA
  reduction_laplacian := fun A hA ε =>
    weak_field_conformal_reduction_laplacianData A hA ε
  reduction_laplacian_kappa := fun A hA κ hκ ε =>
    weak_field_conformal_reduction_laplacianData_kappa A hA κ hκ ε
  flat_vanishing_action := fun W => secondOrderReggeAction_flat W
  flat_vanishing_dirichlet := fun M => dirichletForm_flat M
  remainder_flat := conformal_remainder_zero

What this page does not claim

The theorem does not compute the geometric coefficients from first principles. The theorem does not prove the row-sum condition holds for any specific lattice. The theorem does not claim the reduction applies beyond the conformal weak-field sector.

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