m2TransportedOrbitSlotCoeffTrunc_smul
plain-language theorem explainer
The truncated per-slot m² coefficient of the transported all-orbit 4D Bloch fold is homogeneous of degree two in the metric matrix: scaling H by c multiplies the coefficient by c². Gravity analysts assembling the continuum-facing multi-orbit fold cite this for quadratic scaling of the discrete Einstein–Hilbert symbol. The proof unfolds the truncation, splits on orbit membership, and applies the two class-coefficient smul lemmas plus ring.
Claim. For every hinge-orbit type $\mathrm{ty}$, scalar $c\in\mathbb{R}$, matrix $H\in M_4(\mathbb{R})$, direction $\mathrm{dir}:\mathbb{R}^4$, slot $s\in\{0,\ldots,23\}$ and triangle index $t\in\{0,\ldots,9\}$, the truncated transported-orbit slot $m^2$ coefficient satisfies $$m^2_{\mathrm{trunc}}(\mathrm{ty},\,cH,\mathrm{dir},s,t)=c^2\,m^2_{\mathrm{trunc}}(\mathrm{ty},\,H,\mathrm{dir},s,t).$$
background
This module builds the continuum-facing multi-orbit 4D Bloch fold: each of the 24 hinge slots 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 truncated slot coefficient is the building block that vanishes off-orbit and, on-orbit, multiplies the transported area and deficit class sums.
Mat4 is simply $M_4(\mathbb{R})$. Orbit membership isOrbit ty s t means the lattice hinge $(s,t)$ has orbit type ty. The phase factor phaseScaleDir dir x d is the midpoint phase linear in the ray parameter along dir. The two class-sum smul lemmas used below encode that the area-covector and phase-weighted deficit class coefficients each scale by one power of $c$ when $H\mapsto cH$, hence their product (the $m^2$ density) scales by $c^2$.
The module status list already records quadratic homogeneity of the full fold (blochFoldAll_smul) as a proved item; the present lemma is the per-slot truncated engine behind that claim.
proof idea
Term-mode proof by unfolding m2TransportedOrbitSlotCoeffTrunc and casing on isOrbit ty s t.
- On-orbit branch: the
itereduces to the product of the two class sums. Rewrite the area sum bysum_mul_classCoeff_smul c H (slotOrbitAreaCov ty s t)and the phase-weighted deficit sum bysum_mul_classCoeff_phase_smul c H (slotOrbitDeficitKer ty s t) (fun d => (phaseScaleDir dir (hingeBase s t) d)^2). Each sum contributes one factor of $c$;ringfinishes $c\cdot c=c^2$. - Off-orbit branch: both sides are zero (
mul_zero), so equality is immediate.
why it matters
Feeds the untruncated sibling m2TransportedOrbitSlotCoeff_smul, which is literally a one-line application of this lemma. That homogeneity is part of the module's proved package for the transported all-orbit fold: covering-based transport, $(1,1)$ recovery of the classical Bloch fold, and quadratic scaling under metric rescaling.
In the Recognition gravity stack this is discrete-symbol bookkeeping for the Regge–Bloch $m^2$ that should tend to the continuum Einstein–Hilbert symbol. The module still lists as open the all-orbit $m^2$ Tendsto and the residual 3D-style $2/N^4$ cell-sum dictionary needed for EH isotropy; homogeneous scaling is a prerequisite identity for those limits, not a substitute. It does not touch gap_action_recovery or the T0–T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.