m2TransportedOrbitMomentFull_smul
plain-language theorem explainer
The full-jet m² moment of one transported hinge orbit scales by c² when the metric perturbation matrix is scaled by c. Gravity analysts working the 4D Regge–Bloch continuum fold cite this for quadratic homogeneity of per-orbit aggregates. The proof unfolds the double sum over slots and pulls c² out via the slot-coefficient scaling lemma and Finset.mul_sum.
Claim. For every hinge-orbit type $\tau$, scalar $c\in\mathbb{R}$, matrix $H\in M_4(\mathbb{R})$, and direction $\mathrm{dir}:\{0,1,2,3\}\to\mathbb{R}$, the full-jet transported orbit m² moment satisfies $m^2_{\mathrm{trans}}(\tau,\,cH,\,\mathrm{dir})=c^2\,m^2_{\mathrm{trans}}(\tau,\,H,\,\mathrm{dir})$.
background
This module builds a continuum-facing multi-orbit 4D Bloch fold: each of the 24 slots transports its orbit seed area covector and star deficit kernel by the covering permutation of the orbit representative. The six lattice orbit types under coordinate permutation are the inductive HingeOrbitType family (t11, t12, t21, t13, t31, and the remaining type in the classification).
Mat4 is the abbreviation for real $4\times 4$ matrices, the ambient space of metric perturbations. The full-jet orbit moment is the double sum, over slots $s\in\mathrm{Fin},24$ and hinge indices $t\in\mathrm{Fin},10$, of the per-slot full coefficients. Those slot coefficients already scale by $c^2$ under $H\mapsto cH$ (upstream slot-smul theorem), which is the algebraic input here.
The module status list records quadratic homogeneity of the all-orbit fold among the closed items; this lemma is the per-orbit step of that chain. Cost-algebra $H=J+1$ appears only as ambient naming noise in the dependency graph, not in the argument.
proof idea
Term-mode, two steps. Unfold the full-jet orbit moment to its defining double sum over slots and hinge indices. Rewrite each summand by the upstream slot-coefficient scaling theorem (m2TransportedOrbitSlotCoeffFull_smul), which supplies the factor $c^2$ pointwise, then pull that constant out of both finite sums with ← Finset.mul_sum. No case splits on orbit type or direction are needed at this level.
why it matters
Parent consumer is the all-orbit distinct-hinge full-moment smul theorem in the same module: it unfolds the sum over orbit types and rewrites each summand by this lemma, obtaining global $c^2$ homogeneity of the distinct-hinge aggregate. That aggregate is the continuum-facing m² object whose raw evaluation on axisTTPlus/symbolDir is recorded as $-5/2$ in the sibling M2Eval work, and whose Tendsto limit toward the Einstein–Hilbert continuum is still open.
In the module status ledger this sits under the closed quadratic-homogeneity bullet (blochFoldAll_smul and friends). It does not touch gap-action recovery, nor the residual 3D-style $2/N^4$ cell-sum dictionary still required for EH isotropy. Within Recognition gravity analysis it is bookkeeping infrastructure for the Regge–Bloch symbol, not a forcing-chain (T0–T8) step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.