PhysicalFiniteDifferenceDirichletTarget
plain-language theorem explainer
Defines the remaining physical identification obligation on an encoded periodic Freudenthal torus: the abstract canonical Dirichlet energy must equal a supplied six-tet finite-difference Dirichlet action on every vertex potential. Gravity model builders cite it when wiring the cubic lattice instance to the physical model. The body is a pure Prop quantifying pointwise equality of two real energy functionals.
Claim. Fix nonzero grid sizes $N_x,N_y,N_z$, an encoded periodic Freudenthal torus $P$ on that grid, and a physical finite-difference Dirichlet action $D$ (a real functional on vertex potentials of $P$). The target holds iff for every vertex potential $\xi$, the canonical Dirichlet energy of $\xi$ (from incidence weights) equals $D(\xi)$.
background
This module packages the exact obligations needed to instantiate the physical six-tet cubic Dirichlet model on an encoded periodic Freudenthal torus. It does not assert the physical equality for free; it names the residual identification target.
The abstract side is the canonical Dirichlet energy built from incidence weights on the torus graph $P.K$. The concrete side is a physical finite-difference Dirichlet action: a placeholder type VertexPotential → ℝ meant to be filled later by the six-tet cubic stencil (sum over encoded global periodic edges weighted by flat global edge length). Spatial dimension is the forced $D=3$ of the RS chain; the torus is the periodic Freudenthal scaffold used for cubic lattice continuum limits.
Sibling definitions separate the abstract graph energy from the edge-stencil candidate so that certificates can discharge one identification at a time.
proof idea
Definitional, not a proved theorem. The body is the single universal statement that canonical Dirichlet energy and the supplied physical action $D$ agree on every vertex potential $\xi$. No tactics or upstream lemmas are applied; downstream certificates inhabit this Prop by exhibiting a concrete $D$ and proving the equality.
why it matters
This is the exact remaining physical identification target named in the module: equate incidence-weight Dirichlet energy with the six-tet finite-difference action. Downstream, PeriodicEdgeStencilDirichletTarget specializes it to the periodic edge-stencil action; PeriodicFreudenthalDirichletCertificate packages the broader theorem data for identifying the encoded torus with the physical cubic model. Comparison certificates (exactPeriodicFreudenthalComparisonCertificate_physicalFiniteDifference_identification, canonicalPeriodicEdgeStencilComparisonCertificate_physicalFiniteDifference) inhabit the Prop for concrete actions. In the gravity stack it sits between the Regge/Freudenthal lattice limit and continuum Dirichlet energy, on the $D=3$ cubic scaffold forced by the RS chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.