freudenthalExplicitFiberFlatLocalEdgeLengthDirectionalDeriv_smul
plain-language theorem explainer
The flat Freudenthal local edge-length directional derivative is homogeneous of degree one in the conformal vertex potential: scaling the potential by a real constant scales the derivative by the same constant. Gravity and discrete-Regge workers cite it when pushing scalar factors through fiber-pair expansions on the periodic six-tet cubic lattice. The proof is a three-line unfold-and-ring argument from the explicit definition.
Claim. Let $N_x,N_y,N_z>2$ and let $\xi$ be a conformal vertex potential on the canonical encoded periodic Freudenthal torus of those sizes. For any real scalar $c$, any cubic cell, any of the six tetrahedra in the cell, and any local edge index $k\in\{0,\ldots,5\}$, the flat local edge-length directional derivative of $c\xi$ equals $c$ times that of $\xi$.
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 freely assert the physical Dirichlet equality. Vertices are points of the periodic cubic grid $\mathrm{Fin},N_x\times\mathrm{Fin},N_y\times\mathrm{Fin},N_z$. A vertex potential is a real assignment to the triangulation vertices (conformal factor data for the Regge Hessian).
The object being scaled is the flat Freudenthal local edge-length directional derivative on an encoded periodic tetrahedron, with the squared-edge factor unfolded to the explicit Freudenthal squared-edge list. The underlying scaffold is the canonical encoded periodic Freudenthal torus built from the canonical periodic endpoint incidence. The dimensionless bridge ratio $K=\varphi^{1/2}$ appears only as the triangulation label on that torus, not as a free parameter in the identity.
proof idea
One-line algebraic homogeneity. Unfold the explicit directional-derivative definition, rewrite scalar action on the potential pointwise via $\mathrm{Pi.smul_apply}$ and $\mathrm{smul_eq_mul}$, then close by ring. No geometric lemmas are invoked; the identity is pure linearity of the unfolded formula in $\xi$.
why it matters
Immediate parent is the pair-summand scalar-homogeneity theorem freudenthalExplicitFiberPairFlatExpandedSummand_smul, which lifts this edge-wise fact to expanded fiber-pair contributions on periodic edges. That step is part of the obligation package connecting the encoded periodic Freudenthal torus scaffold to the physical six-tet cubic Dirichlet target (finite-difference Dirichlet action and Hessian comparison on the cubic lattice). In the broader gravity chain it supports discrete-to-continuum Regge correspondence on the six-tet cubic decomposition, without yet discharging the full physical Dirichlet equality.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.