phasedClassDot_smul
plain-language theorem explainer
Homogeneity of the phase-decorated class-weighted sum under scalar multiplication of the 4×4 metric perturbation: scaling the matrix by c scales the whole sum by c. Gravity analysts building bilinear Bloch folds and exact Regge action symbols cite it as the left-slot scalar law. The proof unfolds the finite sum, applies plane-wave class-perturbation homogeneity termwise, then factors c out of the Finset sum.
Claim. For any class weights $v\in\mathbb{R}^{15}$, scalar $c\in\mathbb{R}$, matrix $A\in M_4(\mathbb{R})$, and wave/base data $m,x\in\mathbb{R}^4$, the phased class-weighted sum of midpoint plane-wave class perturbations satisfies $\sum_{d=0}^{14} v_d\,\mathrm{pw}(cA,m,x;d)=c\sum_{d=0}^{14} v_d\,\mathrm{pw}(A,m,x;d)$.
background
Module setting is the QG full-theory campaign for the exact phase-decorated Bloch fold of the committed true-weight flat Hessian on type-(1,1) triangle hinges in one Kuhn cell (72 oriented slots), using the midpoint plane-wave convention of the edge stencil. Scope is the (1,1) orbit only; continuum $m^2$ matching and $S_{\mathrm{RS}}\to\mathrm{EH}$ are explicitly out of lane.
The phased class dot is the weighted sum $\sum_d v_d\cdot\mathrm{planeWaveClassPert}(H,m,x;d)$ over the 15 Regge edge-class channels. The upstream scalar law planeWaveClassPert_smul states that each channel perturbation is homogeneous of degree one in $H$: replacing $H$ by $c\bullet H$ multiplies that channel by $c$ (via class-coefficient homogeneity and associativity of multiplication).
Together these give the natural $\mathbb{R}$-module structure on the left matrix slot of every phase-decorated fold built from class dots.
proof idea
Term-mode proof in four beats. Unfold the definition of the phased class dot to a Finset sum over Fin 15. Rewrite each summand by the upstream lemma planeWaveClassPert_smul, so every term becomes $v_d\cdot(c\cdot\mathrm{pw}(A,m,x;d))$. Transport the outer scalar across the sum via Finset.mul_sum (applied in reverse). Close the remaining pointwise identity by Finset.sum_congr and a one-line ring on each channel.
why it matters
This is the elementary left-homogeneity gate for the entire (1,1) Bloch-fold algebra. Downstream it discharges the scalar step in blochFold11Bilinear_smul_left (bilinearity of the transported (1,1) fold), in the private deficit-dot smul lemmas of Regge4DExactActionSymbol (phasedDeficitDotResolvedT11_smul, T12, and Collapsed), and in the quadratic slot laws exactFlatCrossTermSlot_smul and transportedOrbitSlotTerm_smul (which pick up $c^2$ because two class dots meet).
In the module checklist it sits under the transported phased fold with bilinearity and zero-momentum phase drop. It does not touch continuum EH matching, gap-action recovery, or the open zero-momentum true-weight match ZeroMomTrueWeightMatchOpen; those remain separate lanes. Framework-wise it is pure discrete-gravity bookkeeping inside the Regge Hessian campaign, not a T0–T8 forcing step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.