m2TransportedOrbitMoment_smul
plain-language theorem explainer
The transported-orbit second moment m² scales quadratically under constant rescaling of the 4×4 hinge matrix: replacing H by cH multiplies the moment by c². Gravity analysts cite it when assembling all-orbit Bloch folds and checking continuum homogeneity. The proof unfolds the double sum and pulls c² out via the slot-coefficient smul lemma and Finset.mul_sum.
Claim. For every hinge orbit type $\mathrm{ty}$, scalar $c\in\mathbb{R}$, matrix $H\in M_4(\mathbb{R})$, and direction $\mathrm{dir}:\{0,1,2,3\}\to\mathbb{R}$, the transported-orbit second moment satisfies $$m^{(2)}_{\mathrm{tr}}(\mathrm{ty},\,cH,\,\mathrm{dir})=c^{2}\,m^{(2)}_{\mathrm{tr}}(\mathrm{ty},\,H,\,\mathrm{dir}).$$
background
This module builds a continuum-facing multi-orbit 4D Bloch fold. Each of the 24 slots transports its orbit's seed area covector and star deficit kernel by the covering permutation orbitCoveringPerm (the first $S_4$ cover of the orbit representative). The six orbit types are the lattice classes under coordinate permutation: $(1,1)$, $(1,2)$, $(2,1)$, $(1,3)$, $(3,1)$, and the remaining type in the inductive classification.
The object here is the transported-orbit second moment: a double sum over 24 slots and 10 internal indices of the per-slot coefficient built from the transported deficit kernel and area covector evaluated on a direction. The ambient matrix type is $M_4(\mathbb{R})$. Module status records quadratic homogeneity of the full fold (blochFoldAll_smul) as already proved infrastructure; this lemma is the per-orbit moment piece of that story.
Upstream, the slot-coefficient smul identity already gives $c^{2}$ homogeneity at each $(s,t)$ term. The cost-algebra $H$ appearing in depends-on edges is the shifted J-cost $H(x)=J(x)+1=\tfrac12(x+x^{-1})$, not the hinge matrix; it is ambient RS vocabulary, not an argument of this theorem.
proof idea
Term-mode, three lines. Unfold the definition of the transported-orbit moment (double sum of slot coefficients). Rewrite each summand by the already-proved slot-coefficient identity
$$m^{(2)}{\mathrm{slot}}(\mathrm{ty},,cH,,\mathrm{dir},s,t)=c^{2},m^{(2)}{\mathrm{slot}}(\mathrm{ty},,H,,\mathrm{dir},s,t).$$
Factor $c^{2}$ out of the finite sum with Finset.mul_sum. No case split on orbit type is required; the slot lemma is uniform in ty.
why it matters
Quadratic homogeneity is the discrete signature that the Bloch-fold m² is a genuine second variation, matching the continuum Einstein–Hilbert Hessian scaling. This lemma is the direct input to m2TransportedAllOrbitMomentDistinctHinge_smul, which lifts the same $c^{2}$ law to the distinct-hinge weighted all-orbit moment (weights $1/r_\tau$ via orbitStarSize).
In the module roadmap it sits under the proved block: covering-based transport, $(1,1)$ recovery of the factorized fold, and quadratic homogeneity. It does not close the open items (all-orbit m² Tendsto; continuum EH isotropy via the residual $2/N^4$ cell-sum dictionary), and it does not flip gap_action_recovery. Within RS gravity it is bookkeeping that keeps the discrete second moment compatible with the continuum limit once the Tendsto arguments land.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.