CanonicalPeriodicLocalConformalSchlaefliAlongLineTarget
plain-language theorem explainer
Specializes the local along-line Schläfli identity to the triangulation of the canonical encoded periodic Freudenthal torus on an Nx×Ny×Nz lattice (each extent >2). Gravity workers cite it when discharging the non-flat tetrahedral calculus obligation for the physical six-tet cubic Dirichlet model. The body is a one-line abbreviation applying the generic target to that torus complex.
Claim. For integers $N_x,N_y,N_z>2$, let $K$ be the triangulation of the canonical encoded periodic Freudenthal torus of those extents. The claim is the proposition that for every vertex potential $\xi$, every real line parameter $t$, and every tetrahedron $\tau$ in $K$, the length-weighted sum of actual dihedral-angle derivatives along the conformal line vanishes: $\sum_{f}\sqrt{\ell_f^2(t)}\,\partial_t\theta_f(t)=0$.
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 the torus.
The classical Schläfli identity relates edge-length and dihedral-angle variations on a tetrahedron. The upstream target LocalConformalSchlaefliAlongLineTarget asks for the non-flat along-line form: at every parameter $t$ on a conformal line through a vertex potential, and for every tetrahedron, the local length-weighted sum of actual dihedral derivatives vanishes. Its doc-comment states this is "the tetrahedral calculus content of Schläfli away from the flat point," using actual line derivatives rather than the flat-point closed form.
The complex is the canonical encoded periodic Freudenthal torus built from the periodic Freudenthal lattice with extents $N_x,N_y,N_z>2$. Its triangulation field $K$ is the argument fed into the generic Schläfli target.
proof idea
One-line definitional wrapper. It applies the generic local along-line Schläfli target to the triangulation $K$ of canonicalEncodedPeriodicFreudenthalTorus Nx Ny Nz hx hy hz. No lemmas are invoked and no obligations are discharged; the definition merely names the specialized proposition.
why it matters
This target is one of the two localized non-flat obligations that feed the physical six-tet cubic Dirichlet instance. Downstream, canonicalPeriodicConformalSchlaefliAlongLineTarget_of_expansion_and_local shows the full along-line Schläfli target follows from this local tetrahedral identity plus a global expansion/reindexing of $\sum_e h_e\delta'_e$ into those local sums. The concrete lattice pin CanonicalPeriodicLocalConformalSchlaefliAlongLineTargetAtN5 specializes to the $5\times5\times5$ case used in certificates.
In the RS gravity stack this sits under the Regge-action / Dirichlet correspondence on the cubic lattice: packaging Schläfli calculus on the periodic torus is a prerequisite before the physical model can be instantiated. It does not itself close the Dirichlet equality; it names one of the exact obligations the module is designed to expose.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.