CanonicalPeriodicLocalConformalSchlaefliAngleSqEdgeChainRuleNearZeroTarget
plain-language theorem explainer
Specializes the non-flat local Schläfli angle chain rule in squared-edge coordinates, localized near the flat point, to the triangulation of any canonical encoded periodic Freudenthal torus of size Nx×Ny×Nz (each side >2). Gravity and Regge workers cite it when discharging the chain-rule half of the local conformal Schläfli identity on the physical six-tet cubic lattice. The body is a one-line abbreviation applying the generic target Prop to that torus's K.
Claim. For $N_x,N_y,N_z\in\mathbb{N}$ with each $>2$, let $K$ be the triangulation of the canonical encoded periodic Freudenthal torus of size $N_x\times N_y\times N_z$. The claim is the proposition that $K$ satisfies the non-flat local angle chain rule in squared-edge coordinates near the flat point: for every vertex potential $\xi$, eventually as the line parameter $t\to 0$, each local dihedral derivative equals the closed-form squared-edge gradient paired with the derivative of the six conformal squared-edge coordinates.
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; it wires the encoded periodic scaffold to the model target.
The upstream generic target states: at a nearby line parameter, each actual local dihedral derivative is the closed-form squared-edge gradient paired with the derivative of the six conformal squared-edge coordinates. That Prop is parameterized by an arbitrary 3D triangulation $K$.
Here $K$ is taken from the canonical encoded periodic Freudenthal torus of dimensions $N_x,N_y,N_z$ (each side strictly larger than 2, nonzero). That torus is built from the canonical periodic endpoint incidence, so the edge and hinge bookkeeping is cell-independent by construction.
proof idea
Definitional packaging only: no tactics, no lemmas discharged. The body applies the generic LocalConformalSchlaefliAngleSqEdgeChainRuleNearZeroTarget Prop to the triangulation field .K of canonicalEncodedPeriodicFreudenthalTorus Nx Ny Nz hx hy hz. The size hypotheses $N_x,N_y,N_z>2$ are threaded through so the torus construction typechecks.
why it matters
This Prop is the chain-rule half of the local conformal Schläfli identity on the physical six-tet cubic lattice. Downstream, the theorem canonicalPeriodicLocalConformalSchlaefliAngleSqEdgeChainRuleNearZeroTarget closes it for every canonical periodic Freudenthal torus near the flat point. A combiner theorem then joins this chain-rule obligation with the closed-form zero to obtain the full near-zero Schläfli target. An $N=5$ abbreviation pins the standard finite test size.
In the Recognition gravity stack this sits inside the Regge cubic-lattice limit path: the six-tet Freudenthal decomposition of the cubic cell, with conformal squared-edge coordinates, is the discrete geometry on which the Dirichlet action and Hessian zero-mode analysis run. Closing the chain rule is one of the exact obligations the module was built to package.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.