finRealLinearFunctional_map_finset_sum
plain-language theorem explainer
An additive map on coordinate potentials that scales on single-coordinate spikes pulls finite linear combinations through the sum: f of a finset combination of basis spikes equals the same combination of the values f(spike). Lattice gravity and Regge stencil code cite it when reducing Dirichlet-type actions to coordinate sums. Proof is Finset induction after f(0)=0 from additivity.
Claim. Let $f:(\iota\to\mathbb{R})\to\mathbb{R}$ satisfy $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 spike $e_i=\mathbf{1}_{\{i\}}$. Then for any finite $s\subset\iota$ and coefficients $g:\iota\to\mathbb{R}$, $$f\Bigl(\sum_{i\in s} g(i)\,e_i\Bigr)=\sum_{i\in s} g(i)\,f(e_i).$$
background
The module packages exact theorem obligations needed to instantiate the physical six-tet cubic Dirichlet model on an encoded periodic Freudenthal torus. It does not assert the physical Dirichlet equality for free; it supplies the algebraic and geometric lemmas the instance requires.
Coordinate potentials are maps $\iota\to\mathbb{R}$. The spike $\mathrm{Pi.single},i,1$ is the standard basis vector $e_i$ with value $1$ at $i$ and $0$ elsewhere. A real functional $f$ on such potentials is assumed only additive and homogeneous on those spikes (not a priori fully $\mathbb{R}$-linear on the whole function space).
This lemma is the finset-sum interchange step used immediately downstream to show that any such $f$ is completely determined by the numbers $f(e_i)$.
proof idea
From additivity alone, $f(0+0)=f(0)+f(0)$ forces $f(0)=0$ (simp and linarith).
Proceed by Finset.induction on $s$. Empty case: both sides are $f(0)$ and the empty sum, so $f(0)=0$. Insert case: rewrite the left-hand sum by Finset.sum_insert, split by additivity, apply the inductive hypothesis on the remainder, and replace the new term by the basis-homogeneity hypothesis; finish with simp on the right-hand insert sum.
why it matters
Direct parent is finRealLinearFunctional_eq_sum_coord in the same module: a finite-dimensional $\mathbb{R}$-linear functional on coordinate potentials is determined by its values on coordinate basis vectors. That characterization is the algebraic hinge for writing Dirichlet-type actions as stencil sums over edges of the periodic Freudenthal lattice.
In the Recognition gravity stack this sits inside the Physical Six-Tet Cubic Dirichlet Instance, which bridges the encoded periodic Freudenthal torus scaffold to the PhysicalSixTetCubicDirichletModel target. It is pure finite-dimensional linear algebra, not a physical claim, but without it the reduction from abstract linear functionals on potentials to concrete edge stencils does not go through.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.