sum15_support
plain-language theorem explainer
If a real function on the fifteen edge classes vanishes off the seven indices {1,3,5,7,9,11,13}, its sum over all classes equals the sum of those seven values. Used to collapse full-star directional sums for the type-(1,3) Regge deficit class kernel. Proof partitions Fin 15 into support and complement, zeros the complement, and unfolds the universe via nested inserts.
Claim. Let $f:\{0,\ldots,14\}\to\mathbb{R}$. If $f(d)=0$ whenever $d\notin\{1,3,5,7,9,11,13\}$, then $\sum_{d=0}^{14} f(d)=f(1)+f(3)+f(5)+f(7)+f(9)+f(11)+f(13)$.
background
This module is the type-(1,3) periodic-lattice star deficit class kernel in the QG full-theory campaign, the next kernel-checked increment after the type-(1,1) seed orbit. Scope is the triangle hinge with absolute masks ${0,1,15}$ (difference masks $(1,14)$, local flat squared lengths $(1,3,4)$) and its full periodic Freudenthal star on the 15-class edge stencil.
The fifteen indices label edge classes of the 4D Regge stencil. For type $(1,3)$, the full-star deficit class kernel is supported exactly on the odd classes $(1,3,5,7,9,11,13)$, with values $(-\sqrt{3},-\sqrt{3},+\sqrt{3},-\sqrt{3},+\sqrt{3},+\sqrt{3},-\sqrt{3})$. The type-$(1,1)$ sibling lemma uses the complementary support ${2,3,6,7,10,11,14}$.
Directional quantities such as full-star derivatives are written as $\sum_{d:\mathrm{Fin},15} K(d),w(d)$. Once off-support kernel entries are known to vanish, this support lemma reduces the sum to seven explicit terms.
proof idea
Classical proof. First show the sum of $f$ over the complement finset ${0,2,4,6,8,10,12,14}$ is zero: Finset.sum_eq_zero, then for each $d$ in that set run fin_cases and discharge the seven nonzero-index hypotheses of $hz$ by decide.
Rewrite Finset.univ as the nested insert of ${1,3,5,7,9,11,13}$ into that complement (equality by decide). Apply Finset.sum_insert repeatedly with the complement sum already zero, then ring to match the seven-term right-hand side.
why it matters
Bookkeeping lemma that makes the type-(1,3) full-star gates computable. Downstream, fullStar_homothety_stationary rewrites the weighted directional sum via this support reduction and checks that class weights yield exactly $0$ (homothety stationarity). fullStar_uniformScale_decoy does the same for the constant weight $1$, obtaining $-\sqrt{3}$.
These are items 5–6 of deliverable A in the module: the full-star deficit class kernel on $(1,3,5,7,9,11,13)$ and the gates (nonvacuity, hinge-fixing transposition, uniform-scaling decoy, homothety stationarity). The lemma is the $(1,3)$ twin of the type-$(1,1)$ support lemma on ${2,3,6,7,10,11,14}$.
It does not close the open transport of this kernel to type $(3,1)$, nor the flat Hessian assembly over all hinges, nor $S_{RS}\to$ Einstein–Hilbert convergence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.