canonicalPeriodicWeightedDeficitDerivativeStationaryTarget_of_eventuallyZero
plain-language theorem explainer
On the canonical periodic Freudenthal torus (grid sizes > 2), the stronger punctured-neighbourhood vanishing of the weighted deficit derivative at the flat configuration implies first-order Schläfli stationarity there. Gravity and Regge-calculus workers packaging Track 1.B Dirichlet obligations cite this bridge. The proof is a one-line specialization of the abstract eventually-zero-to-stationary lemma to the encoded torus and its flat configuration.
Claim. Let $N_x,N_y,N_z\ge 1$ with each strictly larger than $2$. If the weighted deficit derivative vanishes in a punctured neighbourhood of the canonical periodic flat configuration on the encoded periodic Freudenthal torus of those sizes, then that configuration is a stationary point of the weighted deficit derivative (first-order Schläfli stationarity).
background
This module packages the exact theorem obligations needed to instantiate the physical six-tet cubic Dirichlet model on a periodic Freudenthal torus; it does not assert the physical Dirichlet equality for free.
The ambient geometry is the canonical encoded periodic Freudenthal torus of sizes $N_x,N_y,N_z$ (each $>2$), together with its incidence-consistent triangulation $K$ and the already-discharged canonical periodic flat configuration (zero local deficit, no remaining chart input). Weighted-deficit targets are the Track 1.B Schläfli forms of the nonlinear Regge action: the eventually-zero target is the stronger punctured-neighbourhood vanishing statement; the stationary target is ordinary first-order criticality of that derivative at the flat point.
Upstream, weightedDeficitDerivativeStationary_of_eventuallyZero already proves the abstract implication for any incidence-consistent triangulation and flat configuration. The two named targets here are simply that abstract pair specialized to the canonical torus data.
proof idea
One-line wrapper. Unfold both named targets to their abstract WeightedDeficit forms, then apply weightedDeficitDerivativeStationary_of_eventuallyZero at the triangulation $K$ and incidence proof of the canonical encoded periodic Freudenthal torus, the canonical periodic flat configuration, and the given eventually-zero hypothesis. No further algebraic work.
why it matters
Closes the eventually-zero $\Rightarrow$ stationary step in the canonical periodic Track 1.B chain for the physical six-tet cubic Dirichlet instance. The sole downstream consumer is canonicalPeriodicSecondSchlaefliAlongLineTarget_of_eventuallyZero, which lifts the same hypothesis to the second-order Schläfli-along-a-line target needed for Hessian/Dirichlet packaging.
In the broader Recognition gravity stack this sits under the Regge cubic-lattice limit and Freudenthal length-chain endpoint certificates: stationarity of the weighted deficit at the flat configuration is the first-order half of the discrete Einstein condition before continuum Dirichlet identification. It does not itself force $D=3$ or the eight-tick octave (those are T7/T8 upstream); it only discharges the Schläfli stationarity obligation once the stronger neighbourhood vanishing is known.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.