CanonicalPeriodicWeightedDeficitDerivativeEventuallyZeroTarget
plain-language theorem explainer
Specializes the stronger near-flat Schläfli target (weighted deficit-derivative sum vanishes in a puncture-free neighbourhood of the flat point) to the canonical periodic Freudenthal torus on an N_x × N_y × N_z lattice with each N_i > 2. Gravity and Regge workers cite it when discharging Track 1.B stationarity or second-order Schläfli along the conformal line. Pure abbreviation: plugs the encoded torus triangulation and its flat configuration into the generic target.
Claim. For lattice sizes $N_x,N_y,N_z\in\mathbb{N}$ with each $N_i>2$, the proposition that on the canonical encoded periodic Freudenthal torus of those dimensions, at its canonical flat configuration, the weighted edge-sum of deficit derivatives vanishes throughout a puncture-free neighbourhood of the flat point (for every vertex potential).
background
This module connects the encoded periodic Freudenthal torus scaffold to the physical six-tet cubic Dirichlet model. It does not assert the physical Dirichlet equality for free; it packages the exact theorem obligations needed to instantiate that model on a periodic Freudenthal torus.
The generic target asserts a stronger near-flat Schläfli form: the weighted deficit-derivative sum vanishes in a puncture-free neighbourhood of the flat point. Upstream wording: "This is more than the second-order proof needs, but it is the natural target produced by a near-zero Schläfli cancellation theorem for the conformal line."
The canonical encoded periodic Freudenthal torus supplies the 3D triangulation and incidence consistency (built from the endpoint incidence certificate). The canonical periodic flat configuration is the zero-deficit flat point already discharged for that torus, with no remaining local-chart or global zero-deficit input.
proof idea
Definitional one-line wrapper. It instantiates the generic weighted-deficit-derivative eventually-zero target on three arguments: the triangulation field of the canonical encoded periodic Freudenthal torus, that torus's incidence-consistency proof, and the canonical periodic flat configuration at the same lattice sizes. No tactics, no extra lemmas, no new proof content.
why it matters
Names the strong punctured-neighbourhood Schläfli obligation at the physical periodic instance. Downstream it is the hypothesis of the implication that eventually-zero yields the weaker stationary (second-order) weighted-deficit-derivative target at the same flat configuration, and of the parallel implication that yields second-order Schläfli along the conformal line. It is also a required field of the Track 1.B eventually-zero inputs structure, which bundles this obligation with the mixed-hinge deficit length-chain target.
In the RS gravity stack this sits on the path from the periodic Freudenthal scaffold to the physical six-tet cubic Dirichlet model. The doc-comment records that the strong form implies the stationary form already packaged for the same torus. It is the natural strong target for a near-zero Schläfli cancellation theorem on the conformal line, not a continuum GR claim by itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.