flat_is_vacuum
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.