PhysicalFiniteDifferenceDirichletAction
plain-language theorem explainer
Type synonym for a physical finite-difference Dirichlet action on an encoded periodic Freudenthal torus: any map from vertex potentials on the torus graph to a real energy. Gravity and discrete-Regge workers cite it when packaging six-tet cubic stencil candidates against the abstract incidence-weight Dirichlet energy. The body is a pure abbreviation to VertexPotential → ℝ, deliberately left open so later stencils can inhabit it.
Claim. For positive integers $N_x,N_y,N_z$ and an encoded periodic Freudenthal torus $P$ on that lattice, a physical finite-difference Dirichlet action is any real-valued functional of vertex potentials on the underlying graph of $P$.
background
The module links the encoded periodic Freudenthal torus scaffold to the physical six-tet cubic Dirichlet model. It does not give the physical equality for free; it packages the exact obligations needed to instantiate that model on a periodic torus.
An encoded periodic Freudenthal torus $P$ carries a graph $K$ (with incidence data $hK$) on which vertex potentials live. The abstract canonical Dirichlet energy is the graph-theoretic quadratic form built from incidence weights. By contrast, the physical side is meant to be a concrete six-tet cubic finite-difference stencil (edge or mixed-axis) on the same lattice.
This abbreviation separates those two layers: it names the type of any candidate physical action without committing to a formula. Downstream candidates (periodic edge stencil, mixed-axis stencil) inhabit this type; the identification target is the pointwise equality of the canonical energy with such a candidate.
proof idea
No proof content. The declaration is a one-line type abbreviation equating the name to the function space of maps from vertex potentials on $P.K$ into $\mathbb{R}$. It deliberately does not expand into a six-tet stencil; that expansion is left to later definitions that return this type.
why it matters
This type is the common carrier for every physical stencil candidate in the six-tet cubic Dirichlet instance. periodicEdgeStencilDirichletAction and canonicalPeriodicMixedAxisStencilAction both return it; PhysicalFiniteDifferenceDirichletTarget takes a value of this type and asserts equality with the canonical incidence-weight Dirichlet energy; PeriodicFreudenthalDirichletCertificate packages continuum-action data of the same shape for the full physical-model identification.
In the Recognition gravity stack this sits on the path from discrete Regge/Freudenthal geometry to a continuum Dirichlet energy on a cubic lattice, which is the discrete precursor to Newtonian and weak-field gravitational action. The module doc is explicit that the physical equality is not free: this placeholder keeps the abstract graph energy and the concrete six-tet stencil formally distinct until a certificate closes the gap.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.