flat_is_vacuum
Zero potential is a stationary point of J-cost on any weighted simplicial graph. Researchers closing the discrete-to-continuum gap in Recognition Science cite this when confirming vacuum solutions before deriving the Regge equations. The proof is a direct term-mode reduction: unfold the Laplacian definition, apply sub_self and mul_zero, then invoke the zero-sum theorem.
claimLet $G$ be a weighted simplicial graph on $n$ vertices. For the zero potential function, the discrete Laplacian satisfies $L_G(0)(i)=0$ for every vertex $i$.
background
The ContinuumBridge module shows that J-cost on the simplicial ledger equals the Regge action up to the factor $8φ^5$. WeightedLedgerGraph is the structure carrying nonnegative symmetric edge weights that encode the discrete ledger. discrete_laplacian is the quadratic Dirichlet energy induced by J-cost on log-potentials, exactly the discrete Laplacian action on the graph.
proof idea
Term-mode proof. Introduce arbitrary vertex $i$, unfold discrete_laplacian, simplify the difference and product terms via sub_self and mul_zero, then apply Finset.sum_const_zero to obtain the zero result.
why it matters in Recognition Science
This fact supplies the flat-vacuum clause inside continuum_bridge_cert, which assembles the full chain from J-cost stationarity through the Regge equations to the Einstein field equations. It anchors the quadratic expansion of J around the identity (T5) before the continuum limit is taken in NonlinearConvergence.
scope and limits
- Does not treat nonzero potentials or curvature sources.
- Does not establish convergence of the discrete equations to the continuum EFE.
- Applies only to finite graphs with $n$ vertices.
- Uses only nonnegativity and symmetry of weights; no further metric assumptions.
Lean usage
theorem vacuum_in_cert (G : WeightedLedgerGraph n) : (flat_is_vacuum G) := by exact flat_is_vacuum Gformal statement (Lean)
261theorem flat_is_vacuum {n : ℕ} (G : WeightedLedgerGraph n) :
262 ∀ i, discrete_laplacian G (fun _ => (0 : ℝ)) i = 0 := by
proof body
Term-mode proof.
263 intro i
264 unfold discrete_laplacian
265 simp only [sub_self, mul_zero]
266 exact Finset.sum_const_zero
267
268/-- Flat spacetime has zero J-cost. -/