slotMatch_mul
plain-language theorem explainer
Constant multiplication distributes through optional six-slot matching: scaling a matched edge value (or zero if unmatched) equals matching the already-scaled values. Downstream Regge regroupings cite it when pulling coefficients out of edge-to-slot incidence sums. The proof is a two-case split on the Option.
Claim. For any real $c$, any optional local edge index $m\in\{\mathrm{some}\,f:f\in\{0,\ldots,5\}\}\cup\{\mathrm{none}\}$, and any map $G$ from six slots to reals, $$c\cdot\begin{cases}G(f)&m=\mathrm{some}\,f\\0&m=\mathrm{none}\end{cases}=\begin{cases}c\,G(f)&m=\mathrm{some}\,f\\0&m=\mathrm{none}.\end{cases}$$
background
This module sits in the QG ReggeTT continuum-symbol campaign, Gate A2 of the Normalization-Gated Schläfli Two-Jet protocol. The setting is a plane-wave edge-length path on a periodic triangulation; action derivatives are written as edge sums of sqrt-length and deficit contributions, then regrouped onto tetrahedra via a canonical edge-to-slot incidence map.
Each global edge may hit a given tet in at most one of six local slots, or miss it. The match expression returns the slot value when the edge is incident and zero otherwise. Pulling a real coefficient through that match is pure bookkeeping, but every regrouped first- and second-variation identity uses it repeatedly when factors such as sqrt-edge derivatives sit outside the incidence match.
The larger program reuses the first-derivative gate at flat space and the tetrahedral Schläfli identity; this lemma is only the scalar-distribution step inside those sums.
proof idea
Term-mode proof by cases on the optional slot index. If the match is none, both sides are zero after simplification. If it is some $f$, both sides reduce definitionally to $c\cdot G(f)$ by reflexivity. No geometric lemmas are invoked.
why it matters
Parent uses are the pathwise Schläfli kill (sum_sqrt_deficitDeriv_eq_zero) and the flat deficit-group regrouping (sum_edgeSqrtDeriv_deficitDeriv_flat). Those theorems convert global edge sums $\sum_e \sqrt{l_e},\delta'_e$ and $\sum_e L'_e\delta'_e$ into per-tet slot sums, then apply the closed-form six-edge Schläfli identity so the entire second group vanishes identically near flat. Without distributing constants through the incidence match, the algebraic regrouping step does not type-check.
In the Gate A2 narrative this is scaffolding arithmetic, not a physics claim: it lets the second variation of the true Regge action at flat reduce to $-\sum_\tau\sum_f L'{\tau f}(0),\theta'{\tau f}(0)$ with no arccos second derivatives. It does not itself touch T0–T8 or the recognition cost $J$; it only keeps the discrete-gravity calculus clean inside the continuum-symbol program.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.