canonicalPeriodicLocalAngleLengthChainRulePackage
plain-language theorem explainer
For lattice periods at least 3, the canonical encoded periodic Freudenthal torus carries a local angle–length chain-rule package: directional derivatives of tetrahedral dihedral angles under conformal edge scaling match the closed-form edge-length chain rule. Gravity workers wiring the six-tet cubic Dirichlet model on that torus cite it. The package is obtained by feeding the torus flat configuration into the square-edge chain-rule constructor.
Claim. For $N_x,N_y,N_z\ge 3$, the canonical encoded periodic Freudenthal torus on the $N_x\times N_y\times N_z$ lattice admits a local angle–length chain-rule package on its triangulation $K$: for every vertex potential $\eta$, tetrahedron $\tau$, and face index $f$, the map $t\mapsto$ dihedral angle of $\tau$ under the conformal line potential of $\eta$ at scale $t$ is differentiable at every real $t$, with derivative equal to the closed-form edge-length chain-rule value.
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 Dirichlet equality for free; it only supplies the geometric derivative data the model target demands.
A local angle–length chain-rule package on a 3D triangulation $K$ records that each tetrahedral dihedral angle, viewed as a function of a conformal scale $t$ along a vertex potential, has a real derivative equal to a closed-form edge-length chain-rule expression. The remaining analytic debt is the HasDerivAt link from the cofactor/arccos angle formula to that closed form.
Upstream, the canonical encoded periodic Freudenthal torus is the standard periodic six-tet cubic scaffold with incidence data fixed by the endpoint certificate. The square-edge and flat-configuration constructors in the Regge first-variation layer turn a flat edge-length assignment into such a package.
proof idea
One-line assembly, not a new analytic argument. Bind $P$ to the canonical encoded periodic Freudenthal torus for the given periods. Apply the square-edge chain-rule package constructor to $P$'s triangulation and incidence proof, feeding it the flat square-edge package obtained from the canonical periodic flat configuration on the same torus. The flat configuration supplies the edge-length data that make the closed-form chain rule match the conformal dihedral derivatives.
why it matters
In the Track 1.B gravity branch this is the canonical local angle input for the periodic six-tet cubic Dirichlet instance. Downstream, the canonical periodic deficit-derivative package is built from this flat local angle chain rule together with the encoded periodic edge-slot partition, so the deficit package is no longer an arbitrary choice. The sibling local dihedral directional-derivative package likewise specializes through the same torus.
That closes the local first-variation side of the Regge-to-Dirichlet bridge on the periodic Freudenthal scaffold: angle derivatives are forced by flat geometry rather than hand-picked. It does not by itself prove the global Dirichlet equality or the continuum limit; those remain separate obligations in the physical model target and the cubic lattice limit modules.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.