canonicalPeriodicSecondSchlaefliAlongLineTarget_of_eventuallyZero
plain-language theorem explainer
On the canonical periodic Freudenthal torus with periods $N_x,N_y,N_z>2$, the stronger punctured-neighbourhood (eventually-zero) Schläfli form of the weighted deficit derivative implies the second-order Schläfli identity along the full conformal line. Regge/gravity workers instantiating the six-tet cubic Dirichlet model cite this bridge. Proof is a two-step term: eventually-zero yields stationarity, and stationarity is definitionally equivalent to the second Schläfli target.
Claim. Let $N_x,N_y,N_z\in\mathbb{N}$ with each $>2$. If the weighted deficit derivative vanishes in a punctured neighbourhood of the canonical periodic flat edge-length configuration on the encoded periodic Freudenthal torus (the eventually-zero Schläfli form), then the second-order Schläfli identity holds along the full conformal line at that flat configuration: $V(t)=0$ for all scale parameters $t$, with $V(t)=\sum_e h(t\cdot\xi,e)\,\partial_t\theta_e(\xi,t)$.
background
This module packages the exact obligations needed to instantiate PhysicalSixTetCubicDirichletModel on an encoded periodic Freudenthal torus; it does not give the physical Dirichlet equality for free.
The ambient geometry is the canonical encoded periodic Freudenthal torus at periods $(N_x,N_y,N_z)$, with its flat edge-length configuration. Two Prop-targets sit on that pair: the eventually-zero target (weighted deficit derivative vanishes near the flat point, a strong punctured-neighbourhood Schläfli form) and the second-order Schläfli-along-line target (the conformal identity $V(t)=0$ for every scale $t$).
Classically, $\sum_{e\in\tau}\ell_e,d\theta_{e,\tau}=0$ on each tetrahedron; summing over the six-tet cubic packing and evaluating along the conformal ray produces the line identity. The eventually-zero form is strictly stronger than mere stationarity at the flat point and is known (in-module) to imply the stationary weighted-deficit target.
proof idea
Pure term-mode composition of two in-module bridges, no tactics.
First apply canonicalPeriodicWeightedDeficitDerivativeStationaryTarget_of_eventuallyZero to the hypothesis: the punctured-neighbourhood vanishing upgrades to the stationary weighted-deficit-derivative target at the canonical flat configuration.
Then apply the forward direction of the biconditional canonicalPeriodicWeightedDeficitDerivativeStationaryTarget_iff_secondSchlaefli, which identifies that stationary target with CanonicalPeriodicSecondSchlaefliAlongLineTarget on the same torus and flat configuration. The composite is exactly the claimed implication.
why it matters
The second Schläfli-along-line identity is the single geometric hypothesis that, once proved, closes the full CanonicalPeriodicWeightedDeficitDerivativeStationaryTargetAtN5 without any per-displacement-class decomposition. The module doc frames this as part of wiring the encoded periodic Freudenthal scaffold into the physical six-tet cubic Dirichlet model used on the Regge side of the gravity chain.
No downstream consumers are recorded yet (used_by_count = 0); the lemma is a local obligation-reduction step inside the Dirichlet-instance package. It sits downstream of the classical Schläfli differential identity applied tetrahedron-wise and summed, and upstream of any future discharge of the stationary or Dirichlet targets at concrete periods (e.g. $N=5$). Framework-wise it is pure discrete-geometry infrastructure for the Regge cubic lattice limit, not a forcing-chain (T0–T8) step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.