m2TransportedOrbitSlotCoeff_smul
plain-language theorem explainer
The canonical transported m² slot coefficient is homogeneous of degree two in the 4×4 metric perturbation: scaling H by c multiplies the coefficient by c². Gravity analysts working the all-orbit Bloch fold cite this when lifting slotwise quadratic scaling to orbit moments. The proof is a one-line wrapper through the truncated-form identity, since the canonical coefficient is defined as that truncation.
Claim. For every hinge-orbit type $\mathrm{ty}$, scalar $c\in\mathbb{R}$, metric perturbation $H\in M_4(\mathbb{R})$, direction $\mathrm{dir}:\{0,1,2,3\}\to\mathbb{R}$, slot $s\in\{0,\ldots,23\}$ and orbit index $t\in\{0,\ldots,9\}$, the canonical transported $m^2$ slot coefficient satisfies $$m^2_{\mathrm{slot}}(\mathrm{ty},\,cH,\mathrm{dir},s,t)=c^2\,m^2_{\mathrm{slot}}(\mathrm{ty},\,H,\mathrm{dir},s,t).$$
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 six lattice orbit types under coordinate permutation are the inductive HingeOrbitType values $(1,1)$, $(1,2)$, $(2,1)$, $(1,3)$, $(3,1)$, and $(2,2)$.
The object here is the canonical transported $m^2$ slot coefficient, defined as the truncated $A_0 K_2$ form used by the integer certificates. The honest product two-jet is $A_0 K_2+A_2 K_0$; on TT plus/cross the two agree slotwise because $K_0=0$. Matrices are plain $4\times 4$ real matrices (Mat4).
Upstream, the truncated coefficient already satisfies the same $c\mapsto c^2$ scaling identity. The cost-algebra $H$ symbols appearing in the dependency graph are ambient Recognition cost reparametrizations ($H=J+1$), not the metric argument of this theorem.
proof idea
One-line wrapper. The canonical coefficient is definitionally the truncated coefficient, so the claim reduces immediately to m2TransportedOrbitSlotCoeffTrunc_smul, which unfolds the truncation, cases on whether the slot-orbit pair is live for the given orbit type, and obtains $c^2$ homogeneity from the bilinearity of the underlying area/kernel pairing.
why it matters
Quadratic homogeneity of the slot coefficient is the atomic step that lifts to orbit-moment scaling: the sole downstream consumer m2TransportedOrbitMoment_smul unfolds the moment as a finite sum of slot coefficients and rewrites via this identity plus Finset.mul_sum.
In the module status ledger this sits under the proved quadratic-homogeneity package (alongside blochFoldAll_smul). It supports the raw all-orbit $m^2$ evaluations (e.g. $-5/2$ on axisTTPlus/symbolDir) without touching the still-open all-orbit $m^2$ Tendsto or continuum Einstein-Hilbert isotropy questions. It does not flip gap_action_recovery. Within RS gravity this is lattice-analytic scaffolding for the Regge-Bloch continuum limit, not a forcing-chain (T0-T8) landmark.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.