m2TransportedAllOrbitMomentDistinctHingeFull_smul
plain-language theorem explainer
The distinct-hinge all-orbit second-moment of the transported 4D Bloch fold is homogeneous of degree two in the metric perturbation: scaling the 4×4 matrix H by a real scalar c multiplies the moment by c². Continuum-face and axis/gauge m² evaluations cite this to pull normalization constants out of the fold. The proof unfolds the orbit sum, applies the per-orbit smul identity, and factors c² through the finite sum.
Claim. For every real scalar $c$, every $4\times 4$ real matrix $H$, and every direction $\mathrm{dir}:\{0,1,2,3\}\to\mathbb{R}$, the distinct-hinge all-orbit transported second moment satisfies $$m_2^{\mathrm{all}}(c\cdot H,\mathrm{dir})=c^2\, m_2^{\mathrm{all}}(H,\mathrm{dir}),$$ where $m_2^{\mathrm{all}}$ sums, over hinge orbit types $\tau$, the full-jet orbit moment weighted by the reciprocal geometric star size $r_\tau^{-1}$.
background
This module builds the continuum-facing multi-orbit 4D Bloch fold: each slot transports its orbit seed area covector and star deficit kernel by the covering permutation of the first $S_4$ cover of the orbit representative. The distinct-hinge all-orbit second moment is the weighted sum $$m_2^{\mathrm{all}}(H,\mathrm{dir})=\sum_\tau r_\tau^{-1}, m_2^{\mathrm{orb}}(\tau,H,\mathrm{dir}),$$ with geometric star sizes $r_\tau\in{4,6}$ fixed by orbit type (paper table: $(1,1)\to 6$, $(1,2)\to 4$, etc.).
Each per-orbit full moment $m_2^{\mathrm{orb}}$ itself sums slot coefficients over the 24 covering slots and 10 hinge indices. The sibling theorem m2TransportedOrbitMomentFull_smul already records that every such orbit moment is quadratic in $H$. The present statement lifts that homogeneity through the $r_\tau^{-1}$ weights to the full distinct-hinge aggregate used by continuum-face evaluations.
Module status marks quadratic homogeneity of the all-orbit fold as a closed theorem item; residual open work is all-orbit $m^2$ Tendsto and continuum Einstein–Hilbert isotropy.
proof idea
Unfold the all-orbit definition to the finite sum over HingeOrbitType of $r_\tau^{-1}\cdot m_2^{\mathrm{orb}}(\tau,\cdot)$. Rewrite each summand by the upstream per-orbit identity
$$m_2^{\mathrm{orb}}(\tau,c\cdot H,\mathrm{dir})=c^2, m_2^{\mathrm{orb}}(\tau,H,\mathrm{dir}).$$
A one-line ring lemma moves $c^2$ past the constant factor $r_\tau^{-1}$. Finally Finset.mul_sum factors $c^2$ out of the whole sum, yielding the claim.
why it matters
Continuum-face normalizations scale the seed matrix (e.g. $(\sqrt{2})^{-1}\cdot\mathrm{axisTTCross}$) before evaluating the fold. Downstream continuumFace_fullTwoJet_normalizedCross_e0Dir rewrites through this smul law to obtain the normalized cross value $-1/16$ on the $e_0$ direction (not the Einstein–Hilbert $-1/4$). Without degree-two homogeneity, those normalizations could not leave the fold.
In the Recognition gravity stack this sits inside the transported all-orbit Bloch analysis that feeds continuum Einstein–Hilbert matching. Module status already lists quadratic homogeneity among closed items; the remaining open questions (all-orbit $m^2$ Tendsto, residual $2/N^4$ cell-sum dictionary for EH isotropy) are independent of this algebraic identity. It does not touch gap_action_recovery.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.