transportedOrbitSlotTerm_smul
plain-language theorem explainer
The transported orbit slot term is homogeneous of degree two in the 4×4 metric perturbation: scaling H by a real constant c multiplies the slot contribution by c². Gravity analysts checking polarization scaling of the multi-orbit Bloch fold cite this. Proof cases on orbit membership, applies linearity of the phased class-dot twice, and rings the product.
Claim. For every hinge orbit type $\mathrm{ty}$, scalar $c\in\mathbb{R}$, matrix $H\in M_4(\mathbb{R})$, momentum $m:\mathrm{Fin}\,4\to\mathbb{R}$, and slot indices $s\in\mathrm{Fin}\,24$, $t\in\mathrm{Fin}\,10$, the transported orbit slot term at $cH$ equals $c^2$ times the same term at $H$.
background
This module builds the continuum-facing multi-orbit 4D Bloch fold: each hinge slot 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 values (t11, t12, t21, t13, t31, and the remaining type in the classification).
The slot term itself is the product, when the slot belongs to the given orbit type, of two phased class-dots (area covector against H, and deficit kernel against H) evaluated at the hinge base; otherwise zero. A phased class-dot is linear in the matrix argument: scaling the matrix by c scales the dot by c (upstream phasedClassDot_smul).
Section §4b of the module collects quadratic homogeneity (polarization scaling) facts needed before comparing the transported fold to committed assembly quadratics. The zero-momentum true-weight match for general H remains an open Prop in the same file.
proof idea
Unfold the slot-term definition. Case on whether the slot lies in the named orbit type.
On the true branch, the term is a product of two phased class-dots. Rewrite each factor by the upstream linearity lemma phasedClassDot_smul, obtaining a factor of c from each, then ring to collect c².
On the false branch both sides are zero by definition; a single simp closes.
why it matters
Parent consumer is blochFoldOrbit_smul, which lifts slot-level c² scaling to the full single-orbit Bloch fold by summing over slots and pulling the constant out of the finite sum. That orbit-level fact is the natural stepping stone toward all-orbit homogeneity (blochFoldAll_smul is already listed among the module's proved status items).
In the Recognition gravity stack this is bookkeeping for the Regge–Bloch continuum symbol: the fold must transform as a quadratic form in the metric perturbation so that polarization identities and m² evaluations remain consistent under rescaling. It does not close the open zero-momentum true-weight match (reindex equals the unpushed class-dot only under class-coeff invariance along the covering perm), nor the residual continuum EH isotropy / Tendsto obligations flagged in the module status. It also does not touch gap_action_recovery.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.