hingeMeasureDirectionalDeriv_canonicalEncodedPeriodic_edge
plain-language theorem explainer
On the canonical encoded periodic Freudenthal torus, the hinge-length directional derivative of a vertex potential along any typed periodic edge equals the edge length scale times the average of the potential at the two endpoints. Gravity and Regge-calculus workers cite it when reducing mixed hinge deficits to explicit fiber sums. The proof unfolds the directional-derivative definition and rewrites edge length and endpoints into periodic coordinates, then finishes by ring.
Claim. Let $N_x,N_y,N_z\ge 3$ and let $P$ be the canonical encoded periodic Freudenthal torus of those sizes. For any vertex potential $\xi$ on $P$ and any typed periodic edge $e$ with displacement class $\mathrm{disp}(e)$ and endpoints $(v_1,v_2)$, the hinge-measure directional derivative of $\xi$ along the corresponding geometric edge of $P$ equals $\sqrt{\mathrm{periodicDispSq}(\mathrm{disp}(e))}\cdot(\xi(v_1)+\xi(v_2))/2$.
background
This module packages the exact 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 geometric substrate is the canonical encoded periodic Freudenthal torus $P$: a finite $N_x\times N_y\times N_z$ periodic lattice (each side at least 3) carrying the Freudenthal edge set and an encoding of vertices and edges into finite index types.
A vertex potential $\xi$ assigns a real value to each lattice vertex. The hinge-measure directional derivative is the first variation of hinge length with respect to $\xi$ along a chosen edge; in the ambient Regge first-variation API it is built from the squared edge length and the two endpoint potentials. Typed periodic edges carry a displacement class and a pair of endpoints in the periodic coordinate chart; periodicDispSqEdge is the squared Euclidean length of that displacement on the torus.
Upstream, the canonical torus is assembled from the endpoint-incidence certificate, and two comparison lemmas identify the encoded global squared edge length and encoded edge vertices with the pure periodic displacement data used on the right-hand side.
proof idea
Tactic proof in three steps. First dsimp unfolds the definition of the hinge-measure directional derivative, exposing the combination of squared edge length and endpoint potentials. Two rewrites then transport the encoded data into typed periodic coordinates: the global squared edge length on the canonical encoding equals periodicDispSqEdge of the edge's displacement, and the encoded edge vertices equal the periodic endpoints (pulled back through the vertex finite equivalence). The resulting algebraic identity is closed by ring.
why it matters
This identity is the coordinate bridge that lets mixed hinge-deficit targets on the physical six-tet cubic Dirichlet instance be written as explicit fiber sums over displacement classes. Downstream it is applied in the closed-form per-displacement and all-bilinear target constructors (canonicalPeriodicMixedHingeDeficitExplicitFiberClosedFormPerDispTarget_of_closedForm, ..._of_endpointTemplate, ..._of_allBilinear, ..._of_perDisp), in the axis-stencil coefficient certificate that matches an explicit-fiber Schläfli/local-length slot to a scaled pair atom after square-root cancellation, and in the negative witness that the flat-unfolded axis-disp-0 fiber target fails.
In the broader Recognition gravity stack this sits inside the Regge cubic-lattice limit path: discrete hinge first variations must match Dirichlet stencil actions before continuum identification. It does not itself force $D=3$ or the eight-tick octave (those are T7/T8 upstream); it supplies the local edge calculus those continuum limits consume once the six-tet cubic model is instantiated.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.