laplacian_action_flat
plain-language theorem explainer
The J-cost Dirichlet energy on a weighted ledger graph vanishes identically for the constant zero potential. Researchers closing the recognition-to-Regge bridge cite this to fix the zero-energy reference before invoking the linearization hypothesis. The argument is a direct algebraic reduction obtained by unfolding the action definition and simplifying the resulting expression on the zero function.
Claim. For any natural number $n$ and weighted ledger graph $G$, the J-cost Dirichlet energy of $G$ evaluated on the constant zero potential equals zero: $E_J(G,0)=0$.
background
In the EdgeLengthFromPsi module the recognition potential on simplices is converted to a conformal edge-length field. The J-cost Dirichlet energy is realized as the quadratic form laplacian_action, which matches the linearized Regge sum once the ReggeDeficitLinearizationHypothesis is assumed. The module supplies the missing map from potential differences to edge-length variations while keeping every theorem either an algebraic identity or an explicit hypothesis-discharge statement.
proof idea
The proof is a one-line wrapper that unfolds the definition of laplacian_action and applies the simp tactic, which reduces the expression on the zero function to the zero scalar.
why it matters
This supplies the flat_jcost component of EdgeLengthFromPsiCert and the flat_jcost field of continuumFieldCurvatureCert. It confirms that the J-cost energy vanishes on the flat vacuum, consistent with the Regge sum vanishing under the linearization hypothesis, thereby supporting the field-curvature identity of the Gravity from Recognition draft with coupling $κ=8φ^5$. It touches the open task of discharging ReggeDeficitLinearizationHypothesis from an explicit Cayley-Menger or Cheeger-Müller-Schrader computation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.