planeWaveClassPert_smul
plain-language theorem explainer
Plane-wave midpoint loading on a Freudenthal edge class is homogeneous of degree one in the 4×4 metric perturbation. Anyone assembling Bloch-folded class dots or star-edge plane-wave sums in the 4D Regge stencil cites this scalar law. The proof unfolds the loading definition and applies the already-proved scalar law for the class coefficient, then reassociates.
Claim. For every real scalar $c$, every $4\times 4$ real matrix $H$, every wavevector $m$ and base point $x$ in $\mathbb{R}^4$, and every Freudenthal edge class $d$ among the fifteen nonzero $\{0,1\}^4$ displacements, the plane-wave midpoint loading of $cH$ at $(m,x,d)$ equals $c$ times the loading of $H$. Explicitly, $(D^\top (cH) D)\,\cos(m\cdot x+m\cdot D/2)=c\,(D^\top H D)\,\cos(m\cdot x+m\cdot D/2)$.
background
The module packages the 4D Regge edge stencil after ReggeEdgeTTAttachment4D: fifteen Freudenthal-style edge classes, namely the nonzero displacement vectors in ${0,1}^4$, indexed by bit masks. For class $d$ with displacement $D$, the class coefficient is the squared-length load $D^\top H D$ (same convention as 3D polEdgeCoeff / 4D edgeLoad). Plane-wave midpoint loading multiplies that coefficient by the midpoint cosine $\cos(m\cdot x + m\cdot D/2)$.
The local campaign proves algebraic structure of a provisional finite quadratic aggregate with all-ones class weights. True 4D Regge Hessian weights remain OPEN and must not be reverse-engineered from Einstein-Hilbert.
Upstream, the sibling scalar law already states that the class coefficient itself satisfies $\mathrm{classCoeff}(cH,d)=c,\mathrm{classCoeff}(H,d)$ via the edge-load scalar identity.
proof idea
Short tactic proof, not a deep argument. Unfold the plane-wave midpoint loading to the product of class coefficient and midpoint cosine. Rewrite with the upstream scalar law for the class coefficient, which pulls $c$ out of $D^\top (cH) D$. Finish by mul_assoc so the scalar sits in front of the full product. The cosine factor does not depend on $H$, so degree-one homogeneity lifts immediately from the coefficient to the loading.
why it matters
This is the scalar-multiplication leg required when folding or summing plane-wave class contributions. Downstream, the Bloch-fold identity for the phased class dot product rewrites under this law and then factors $c$ out of a finite sum. The star-edge origins development uses it inside a list-sum map when every seed-edge contribution is evaluated on $cH$ rather than $H$.
In the Recognition Science gravity track it sits inside the 4D Regge edge-stencil packaging that prepares finite TT quadratic structure for later Bloch analysis. It does not close the OPEN true Regge weights, does not prove $S_{\mathrm{RS}}$ converges to Einstein-Hilbert in 4D, and does not flip gap-action recovery. Pure algebraic homogeneity scaffolding for the Bloch and star-edge layers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.