finRealLinearFunctional_eq_sum_coord
plain-language theorem explainer
Any additive real functional on finite-dimensional coordinate potentials that scales correctly on single-coordinate basis vectors equals the weighted sum of its basis values. Gravity and discrete-geometry arguments cite it to expand fiber or stencil functionals in vertex coefficients. The proof reconstructs the potential from basis singles, then applies the finite-sum mapping lemma.
Claim. Let $\iota$ be a finite type and $f:(\iota\to\mathbb{R})\to\mathbb{R}$. Suppose $f(\xi+\eta)=f\xi+f\eta$ for all $\xi,\eta$, and $f(c\,e_i)=c\,f(e_i)$ for every scalar $c\in\mathbb{R}$ and coordinate basis vector $e_i$. Then for every potential $\xi$, $f(\xi)=\sum_{i\in\iota}\xi_i\,f(e_i)$.
background
The ambient module packages exact obligations needed to instantiate the physical six-tet cubic Dirichlet model on a periodic Freudenthal torus. It does not freely assert the physical Dirichlet equality; it supplies the algebraic and geometric lemmas that close the instance.
Coordinate potentials are maps $\iota\to\mathbb{R}$. The standard basis vectors are the single-support maps $e_i=\mathrm{Pi.single},i,1$. The hypotheses are additivity of $f$ on the whole space of potentials, plus homogeneity only on those basis rays (not full $\mathbb{R}$-linearity a priori).
The immediate upstream tool is the finite-sum mapping lemma for the same class of functionals: under additivity and basis homogeneity, $f$ sends a finite sum of scaled basis vectors to the corresponding scalar sum of $f$-values. That lemma is the engine used here once the potential is rewritten in the coordinate basis.
proof idea
First rewrite $\xi$ as $\sum_i\mathrm{Pi.single},i,(\xi_i)$ by the standard identity that a finite-support function is the sum of its singles. Pointwise, each single equals the scalar multiple $\xi_i\bullet e_i$, proved by case split on the coordinate index. Congruence of the sum then yields $\xi=\sum_i\xi_i\bullet e_i$.
A short calculation chain applies $f$: replace $\xi$ by the single-sum, then by the scaled-basis sum, then invoke the finite-sum mapping lemma on the universe finset with coefficient map $\xi$. The result is exactly $\sum_i\xi_i,f(e_i)$.
why it matters
This is the coordinate expansion step for explicit-fiber closed forms on the encoded periodic Freudenthal torus. Downstream it feeds the identity that the freudenthal explicit-fiber closed-form fiber sum equals the sum of vertex coefficients, which is how stencil and Dirichlet actions are reduced to vertex data in the physical six-tet cubic instance.
In the broader gravity stack, that reduction sits between the periodic Freudenthal geometry scaffold and the physical finite-difference Dirichlet target. Without a proved basis expansion for the linear functionals that appear as fiber sums, the closed-form comparison to the Dirichlet action cannot be stated vertex-wise. The result is pure finite-dimensional linear algebra, but it is the bridge that lets the geometric encoding talk to the physical model obligations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.