laplacian_action
plain-language theorem explainer
laplacian_action supplies the quadratic Dirichlet energy on a weighted ledger graph as half the summed product of edge weights and squared field differences. Discrete gravity researchers cite it when equating the J-cost functional to the linearized Regge action. The definition is a direct algebraic transcription of the graph energy from the quadratic expansion of J in log coordinates.
Claim. For a weighted simplicial graph with nonnegative symmetric edge weights $w_{ij}$ and a real field $ε$ on the vertices, the discrete Laplacian action is given by $½ ∑_{i,j} w_{ij} (ε_i - ε_j)^2$.
background
The Continuum Bridge module closes the gap between the discrete simplicial ledger and Einstein equations by identifying J-cost stationarity with the Regge equations. WeightedLedgerGraph is the structure that holds a nonnegative symmetric weight matrix on a finite set of vertices. Upstream results from Cost.FunctionalEquation and PhiForcingDerived supply the J-cost functional satisfying the Recognition Composition Law, together with its quadratic approximation J(e^δ) ≈ δ²/2 in log coordinates.
proof idea
This is a definition that directly transcribes the quadratic J-cost into the summed graph energy. It applies the log-coordinate expansion of J without additional lemmas or reductions.
why it matters
This definition supplies the discrete quadratic form that enters the field-curvature identity. It is invoked in induced_regge_action to produce the scaled Regge sum and in field_curvature_identity_einstein to equate the action to (1/κ_Einstein) times the regge sum with κ_Einstein = 8φ^5. It completes the step from J_global to the continuum EFE in the module derivation chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.