freudenthalExplicitFiberClosedFormFiberSum_smul
plain-language theorem explainer
Scalar homogeneity for the closed-form explicit-fiber sum on the canonical periodic Freudenthal torus: scaling the vertex potential by a real constant scales the fiber sum by the same factor. Gravity and Regge-lattice workers cite it when assembling Dirichlet stencil actions that must be linear in the potential. The proof rewrites the sum via vertex coefficients, then pulls the scalar through Finset.sum by associativity of multiplication.
Claim. Let $N_x,N_y,N_z\ge 3$ and let $\xi$ be a vertex potential on the canonical encoded periodic Freudenthal torus of those sizes. For every real scalar $c$, every periodic edge, and every fiber index $d\in\{0,\ldots,6\}$, the closed-form explicit-fiber sum of $c\cdot\xi$ equals $c$ times the closed-form explicit-fiber sum of $\xi$.
background
The 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; it builds the finite-difference and stencil infrastructure that a later equality proof must discharge.
The object here is the closed-form explicit-fiber length-chain sum: each fiber entry uses the flat edge-length directional derivative at a selected periodic cell. The potential lives on vertices of the canonical encoded periodic Freudenthal torus; edges are the torus's periodic edges. Fiber indices run over Fin 7, matching the discrete fiber template used in the length-chain endpoint calculus.
Sibling material in the same file develops periodic-edge Dirichlet stencils, axis displacements, and Hessian-is-Dirichlet certificates. Those constructions need the fiber sum to be homogeneous of degree one in the potential so that scaled trial fields produce scaled action contributions.
proof idea
Term-mode rewrite proof. Both sides are rewritten by freudenthalExplicitFiberClosedFormFiberSum_eq_sum_vertexCoeffs, expressing the fiber sum as a finite sum of per-vertex coefficients. Pi.smul_apply and Finset.mul_sum pull the scalar out of the sum of the scaled potential. Pointwise, Finset.sum_congr reduces to each vertex coefficient: unfold freudenthalExplicitFiberClosedFormVertexCoeff, convert scalar action to multiplication via smul_eq_mul, and finish with mul_assoc. No geometric content is re-proved; only algebraic homogeneity of the closed template.
why it matters
In the gravity domain this is a small but necessary linearity lemma for the physical six-tet cubic Dirichlet instance. The parent module's job is to connect the encoded periodic Freudenthal torus scaffold to PhysicalSixTetCubicDirichletModel; stencil actions and Hessian certificates among the siblings presuppose that fiber sums scale correctly under constant rescaling of the potential.
No downstream consumers are recorded yet (used_by is empty), so the lemma currently sits as local infrastructure rather than a cited bridge into a named chain step. Framework-wise it supports the Regge/cubic-lattice side of Recognition gravity (periodic Freudenthal geometry, finite-difference Dirichlet targets), not the T0–T8 forcing chain or the RCL directly. It closes no open scaffold; it is already a proved algebraic identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.