quadContr_smul_eta
plain-language theorem explainer
Scaling the Minkowski metric by a real factor λ multiplies its quadratic form by λ. Anyone in the null-cone rigidity package cites this to reduce contractions against λη to the standard Minkowski quadratic form. The proof is a two-rewrite wrapper: homogeneity of the quadratic contraction, then the known evaluation of η.
Claim. For every real scalar $\lambda$ and every covector $k \in \mathbb{R}^4$, the quadratic contraction of $\lambda\eta$ against $k$ equals $\lambda$ times the Minkowski quadratic form: $(\lambda\eta)_{\mu\nu} k^\mu k^\nu = \lambda\bigl(-(k^0)^2+(k^1)^2+(k^2)^2+(k^3)^2\bigr)$, where $\eta=\mathrm{diag}(-1,1,1,1)$.
background
This module develops a finite-dimensional rigidity fact: the values of a symmetric quadratic form on all Minkowski-null covectors determine the symmetric matrix only up to a scalar multiple of the Minkowski metric $\eta=\mathrm{diag}(-1,1,1,1)$. It is an algebraic prerequisite for Phase 5 gravity work, not a geometric identification with Ricci or stress-energy.
The quadratic contraction is $A_{\mu\nu}k^\mu k^\nu$, written as a double sum over $\mathrm{Fin},4$. The matrix $\eta$ is the standard $(-,+,+,+)$ Minkowski metric in the coordinate basis. Upstream, the evaluation theorem records that contracting $\eta$ itself recovers $-(k^0)^2+(k^1)^2+(k^2)^2+(k^3)^2$. A companion homogeneity lemma states that scaling the matrix argument scales the contraction: $\mathrm{quadContr}(c\cdot A,k)=c,\mathrm{quadContr}(A,k)$.
proof idea
One-line wrapper. Rewrite first by the homogeneity lemma for quadratic contraction under real scalar multiplication of the matrix, then by the evaluation of the contraction of bare $\eta$. The two rewrites compose to the claimed formula; no further algebra is needed.
why it matters
Immediate parent is the null specialization: on any Minkowski-null covector the same scaled contraction vanishes, because the Minkowski quadratic form itself is zero on the null cone. That fact is the basic vanishing ingredient in the null-cone quadratic tensor class: matrices of the form $\lambda\eta$ are invisible to null quadratic data, so reconstruction of a symmetric matrix from its null-cone values can only be unique modulo multiples of $\eta$.
Within Recognition Science gravity, this sits in the Phase 5 algebraic prerequisite package. The module is explicit that Tier A remains open until a symmetric $G$ is built from Recognition area/focusing ancestry independently of a fixed stress tensor; this lemma does not close the Einstein field equation, construct horizons, or rename finite responses into Ricci.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.