Gravity Weak Field Conformal Regge Bilinear Coefficient Laplacian Regge Data

The coefficient identity

In Regge calculus, gravity is described on a discrete mesh of flat simplices, and the action is a sum over the mesh edges of the edge length times the deficit angle. The Regge action is the discrete analogue of the Einstein-Hilbert action of general relativity. When the mesh is perturbed slightly, the action changes; the second-order change, the quadratic part, is what governs weak-field dynamics. The bilinear coefficient is the number attached to each pair of mesh vertices in that quadratic form: it says how strongly a change at one vertex couples to a change at another.

The declaration bilinearCoefficient_laplacianReggeData states that if you build the perturbation data from a symmetric matrix of weights by taking the graph Laplacian of those weights, then the resulting bilinear coefficient is exactly the Laplacian coefficient. In plainer terms: the coupling between two vertices is the negative of the weight on the edge between them, plus the sum of weights on all edges leaving the first vertex when the two vertices coincide. This is a purely algebraic identity, proved in the machine-checked library of formal theorems. It holds for any finite set of vertices and any symmetric weight matrix; no geometric input is needed beyond the symmetry.

The identity matters because it connects two ways of writing the same physics. One route starts from the geometric Regge action and expands it; the other starts from a graph Laplacian, a standard object in discrete mathematics that measures how a function varies across a network. The declaration shows these two routes agree coefficient by coefficient. That agreement is the algebraic core of a reduction in which the weak-field conformal Regge action becomes a Dirichlet form, a sum of squared differences between neighboring vertex values. The Dirichlet form is the discrete version of the familiar Laplacian energy, and it is what makes the weak-field theory look like a lattice field theory with nearest-neighbor couplings.

The declaration is conditional in a specific sense. It proves the identity for data constructed from a Laplacian, but it does not compute the geometric coefficients from the actual mesh geometry. Those coefficients, the first-order changes in area and deficit angle, are packaged in a structure called WeakFieldReggeData and are not derived in this file. The file also does not verify the Schläfli row-sum condition, the requirement that the sum of coefficients in each row vanishes, for any particular lattice. What the declaration does establish is that once such data are supplied and the row-sum condition holds, the reduction to the Dirichlet form is formal and complete.

In Recognition Science, this result is part of a larger program that derives physical structure from a ledger of recognition events. The discrete ledger picture motivates the graph-theoretic language: the weights are the costs of transitions between states, and the Laplacian is the natural discrete analogue of the continuous Laplacian. The declaration here is a bridge between that abstract ledger structure and the concrete Regge action of gravity. It shows that the ledger's discrete Laplacian and gravity's weak-field action are the same object, seen from two sides. The payoff is that the formal machinery of graph Laplacians, with its well-developed theory of spectra and diffusion, becomes available for the analysis of weak-field gravity on a lattice.

/-- For `laplacianReggeData`, the bilinear coefficient is exactly the
    Laplacian coefficient matrix. -/
theorem bilinearCoefficient_laplacianReggeData {n : ℕ}
    (A : Fin n → Fin n → ℝ) (hA : ∀ i j, A i j = A j i)
    (i j : Fin n) :
    bilinearCoefficient (laplacianReggeData A hA) i j
      = laplacianCoefficient A i j := by
  unfold bilinearCoefficient laplacianReggeData
  ring

/-- For `laplacianReggeData`, the bilinear coefficient is exactly the
    Laplacian coefficient matrix. -/
theorem bilinearCoefficient_laplacianReggeData {n : ℕ}
    (A : Fin n → Fin n → ℝ) (hA : ∀ i j, A i j = A j i)
    (i j : Fin n) :
    bilinearCoefficient (laplacianReggeData A hA) i j
      = laplacianCoefficient A i j := by
  unfold bilinearCoefficient laplacianReggeData
  ring

theorem weak_field_conformal_reduction_laplacianData_kappa {n : ℕ}
    (A : Fin n → Fin n → ℝ) (hA : ∀ i j, A i j = A j i)
    (κ : ℝ) (hκ : κ ≠ 0) (ε : LogPotential n) :
    secondOrderReggeAction (laplacianReggeData A hA) ε / κ
      = (1 / κ) * (1 / 2) * dirichletForm A ε := by
  rw [weak_field_conformal_reduction_laplacianData A hA ε]
  field_simp

What this page does not claim

The declaration does not compute the geometric Regge coefficients from the mesh geometry. It does not prove the Schläfli row-sum condition for any specific lattice. It does not establish that the weak-field Regge action equals the Einstein-Hilbert action in the continuum limit.

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: