Gravity Weak Field Conformal Regge Component Comparison Gives Geometric Dirichle

The reduction theorem

Regge calculus is a way of doing general relativity without coordinates: spacetime is chopped into flat tetrahedral pieces, and the curvature is concentrated along their shared triangular faces. The Regge action, written by Tullio Regge in 1961 as S = (1/κ) · Σ_h A_h · δ_h, sums over each hinge h the product of its area A_h and its deficit angle δ_h, the angle by which the surrounding flat pieces fail to close flat. In the weak-field limit, where the geometry is nearly flat, this action can be expanded in small perturbations. The theorem here concerns a particular choice of perturbation, the conformal mode, which rescales all edge lengths by a smoothly varying factor.

The classical result, proved in the machine-checked library of formal theorems, is that under one geometric condition the second-order conformal Regge action equals a discrete Dirichlet energy. The Dirichlet form, familiar from the theory of elasticity and harmonic functions, is a sum over pairs of neighboring sites of a weight times the squared difference of the field values: (1/2) Σ_{i,j} M_{ij} (ε_i − ε_j)². The theorem states that if the Regge data satisfy the Schläfli row-sum condition, meaning that for each vertex the sum of the bilinear coefficients over all neighbors is zero, then the second-order action is exactly one half times this Dirichlet form, with the geometric areas as weights. The proof is algebraic: it uses the identity that for a symmetric matrix with zero row sums, the quadratic form Σ M_{ij} ε_i ε_j equals minus one half the Dirichlet form Σ M_{ij} (ε_i − ε_j)². This is the structural lemma that converts the Regge bilinear form into the Dirichlet form.

The theorem is conditional. It does not compute the actual geometric coefficients from the Cayley–Menger or dihedral angle formulas; that remains a separate geometric task. It assumes the row-sum condition holds, which is a property the physical coefficients must satisfy, not something the theorem proves for a specific lattice. The file also packages a certificate structure, WeakFieldConformalReggeCert, which bundles the data and the row-sum hypothesis, and proves that this certificate exists. The reduction itself is fully formal: zero axioms beyond the standard three, zero sorry. The chain of reasoning is: expand the conformal edge lengths to second order, apply the graph-Laplacian decomposition to the symmetric zero-row-sum matrix, and identify the resulting expression with the Dirichlet form.

In Recognition Science, this theorem is one step in a program that derives physical structure from a discrete ledger of recognition events. The framework models spacetime as a weighted graph, where the weights are the geometric areas, and the Dirichlet form is the natural energy of a field on that graph. The reduction shows that the weak-field gravitational action, in the conformal sector, is exactly the energy of a scalar field on the discrete geometry. This is a bridge between the continuum action of general relativity and the discrete graph-theoretic picture the framework uses. The physical significance is that the conformal mode of gravity behaves like a free scalar field on the lattice, with the geometric areas playing the role of the metric on the graph.

/-- If the genuine Regge component comparison is supplied, then the second-order
Regge action reduces to the Dirichlet form with the supplied geometric
area/face weights.  This is the exact formal shape of the missing
`M_{ij}` versus `area(f_{ij})` comparison. -/
theorem componentComparison_gives_geometric_dirichlet
    {n : ℕ} (W : WeakFieldReggeData n)
    (cmp : ReggeComponentComparison W)
    (ε : LogPotential n) :
    secondOrderReggeAction W ε
      = (1 / 2) * dirichletForm cmp.geometricArea ε := by
  rw [weak_field_conformal_reduction W cmp.schlaefli_row_sum ε]
  congr 1
  apply dirichletForm_diag_irrelevant
  intro i j hij
  unfold edgeArea
  rw [cmp.offDiag_component_match i j hij]
  ring

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

/-- If the genuine Regge component comparison is supplied, then the second-order
Regge action reduces to the Dirichlet form with the supplied geometric
area/face weights.  This is the exact formal shape of the missing
`M_{ij}` versus `area(f_{ij})` comparison. -/
theorem componentComparison_gives_geometric_dirichlet
    {n : ℕ} (W : WeakFieldReggeData n)
    (cmp : ReggeComponentComparison W)
    (ε : LogPotential n) :
    secondOrderReggeAction W ε
      = (1 / 2) * dirichletForm cmp.geometricArea ε := by
  rw [weak_field_conformal_reduction W cmp.schlaefli_row_sum ε]
  congr 1
  apply dirichletForm_diag_irrelevant
  intro i j hij
  unfold edgeArea
  rw [cmp.offDiag_component_match i j hij]
  ring

What this page does not claim

The theorem does not compute the Regge second-variation coefficients from Cayley–Menger data. The theorem does not prove that the Schläfli row-sum condition holds for any particular lattice. The theorem does not establish a physical equivalence between general relativity and the Recognition Science 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: