distinctHingeMomentForm_smul
plain-language theorem explainer
Scaling a 4×4 polarization matrix by a real constant multiplies the distinct-hinge transported m² form by the square of that constant. Gravity analysts banking the 4D Regge TT quadratic form cite this homogeneity when reducing ray evaluations and zero cases. The proof is a one-line wrapper of the underlying all-orbit transported-moment scaling lemma.
Claim. For every real scalar $c$, every real $4\times 4$ matrix $E$, and every direction $\mathrm{dir}:\{0,1,2,3\}\to\mathbb{R}$, the distinct-hinge transported $m^2$ quadratic form $Q$ satisfies $Q(c\cdot E,\mathrm{dir})=c^2\,Q(E,\mathrm{dir})$.
background
This module is the 4D counterpart of the 3D Regge TT algebraic closer. It banks the transported distinct-hinge $m^2$ as a quadratic form in a polarization matrix and a direction on the TT variety, with closed ray evaluations available now; full equality to a universal adjugate-style tensor contraction remains open.
Here $\mathrm{Mat}_4$ is the type of real $4\times 4$ matrices. The distinct-hinge moment form is the in-module name for the transported all-orbit distinct-hinge $m^2$ functional of a polarization and a direction: it is defined by direct alias to that upstream moment. The module already records the banked homogeneity statement for that moment under scalar multiplication of the polarization.
Upstream, the scaling identity for the transported all-orbit distinct-hinge moment is proved by unfolding the moment and rewriting with the orbit-moment scalar-multiplication lemma. This declaration simply re-exports that identity under the quadratic-form alias used throughout the closer.
proof idea
One-line wrapper: apply the upstream theorem that scales the transported all-orbit distinct-hinge moment under $c\cdot H$, with the same scalar, matrix, and direction. Because the local form is definitionally that moment, no further rewriting is required.
why it matters
Homogeneity is the first banked theorem of the 4D tensor algebraic closer: every closed ray evaluation of the distinct-hinge form must respect quadratic scaling in the polarization. The immediate parent is the zero-matrix evaluation, which obtains vanishing of the form at $E=0$ by specializing this identity at $c=0$.
That zero fact and the banked plus/cross ray values (symbol and $e_0$ directions, normalized $-1/8$ and $-1/16$) feed the residual arithmetic against the Einstein-Hilbert continuum face. The module keeps open the universal bilinear closed form matching the distinct-hinge moment on all TT data, and the geometric account of the residual factor 4; this lemma does not close those questions and does not flip gap-action recovery. It is the algebraic bookkeeping step that lets later ray lemmas treat the form as genuinely quadratic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.