discrete_laplacian
plain-language theorem explainer
The discrete Laplacian on a weighted ledger graph sums weighted differences of a scalar field ε at each vertex. Researchers deriving the Einstein equations from J-cost stationarity on simplicial structures cite this operator as the discrete counterpart to the Regge action. The definition is introduced directly as a summation over the graph weights without further lemmas.
Claim. For a weighted ledger graph $G$ with edge weights $w_{ij}$ and a scalar field $ε$ on its vertices, the discrete Laplacian at vertex $i$ is defined by $ (Δε)_i = ∑_j w_{ij} (ε_i - ε_j) $.
background
The Continuum Bridge module identifies the J-cost functional on the simplicial ledger with the Regge action up to the factor κ = 8φ⁵. A WeightedLedgerGraph is a finite simplicial structure equipped with a nonnegative symmetric weight function that encodes couplings between vertices. In log coordinates ε = ln ψ the quadratic expansion of J yields a coupling term identical to a discrete Laplacian action, which the module uses to equate J-cost stationarity with Regge stationarity before taking the continuum limit to the Einstein field equations.
proof idea
This is a direct definition that expands to the indicated summation over the graph weights. No upstream lemmas are invoked; the expression serves as the primitive operator for the stationarity theorems that follow in the same module.
why it matters
The definition supplies the discrete operator appearing in the JCostToEFE chain and the ContinuumBridgeCert structure, which certifies that J-cost stationarity on the ledger produces the Einstein field equations. It realizes the module's central claim that the quadratic structure of J-cost matches the Regge action, thereby closing the discrete-to-continuum gap referenced in the derivation chain from J_global through NonlinearConvergence. The construction aligns with the T5 J-uniqueness and the spatial discretization step in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.