quadContr_smul
plain-language theorem explainer
Quadratic contraction of a 4x4 matrix against a covector is homogeneous of degree one in the matrix: scaling the matrix by a real constant scales the contraction by the same factor. Cited by anyone peeling scalar multiples off Einstein-shaped or null-cone identities in the RS gravity stack. Proof unfolds the double sum and factors the constant through both Finset sums.
Claim. For every real scalar $c$, every real $4\times 4$ matrix $A$, and every covector $k\in\mathbb{R}^4$, the quadratic contraction $A_{\mu\nu}k^\mu k^\nu$ is homogeneous in the matrix: $$(cA)_{\mu\nu}k^\mu k^\nu = c\, A_{\mu\nu}k^\mu k^\nu.$$
background
The quadratic contraction of a matrix $A$ against a covector $k$ is the real number $\sum_{i,j} A_{ij} k_i k_j$, written $A_{\mu\nu} k^\mu k^\nu$ in index notation. It is the basic probe of the null-cone package: one evaluates a quadratic form on Minkowski-null directions to recover the matrix modulo multiples of the metric.
This module is a Phase 5 algebraic prerequisite. Finite-dimensional real linear algebra shows that the values of a symmetric quadratic form on all Minkowski-null covectors determine the symmetric matrix modulo a scalar multiple of $\eta=\mathrm{diag}(-1,1,1,1)$. The module does not construct geometric curvature, horizons, or close the Einstein equation; an independently sourced symmetric $G$ remains open.
Homogeneity in the matrix argument is the elementary scalar-factor fact needed before undetermined pure-metric terms can be cancelled on the null cone. An identical statement already lives in the RS null-field equation module; this file re-establishes it in the local null-cone class.
proof idea
Unfold the contraction to a double finite sum over $\mathrm{Fin},4$. Simplify matrix scalar multiplication to ordinary multiplication of entries. A three-line calc then reassociates each summand $c\cdot A_{ij}\cdot k_i\cdot k_j$ by ring, pulls $c$ out of the inner sum via Finset.mul_sum, and pulls $c$ out of the outer sum the same way. No null-cone hypothesis is used; the identity is pure finite-sum algebra.
why it matters
Direct parent uses include the scaled Minkowski contraction (multiple of $\eta$ against any $k$) and the vanishing of every pure metric term on a Minkowski-null probe. Those feed the null reduction of an Einstein-shaped equation: if $c,T=\mathrm{Ric}+f,\eta$, the undetermined scalar metric term drops on every null direction, leaving a pure stress-versus-Ricci null identity.
In the Recognition Science gravity stack this is supporting linear algebra for null-cone rigidity and the RS null-field equation, not a geometric claim. Module honesty tags keep Tier A open: no independent Recognition-ancestry $G$, no continuum Ricci, no closed EFE. The lemma only licenses factoring scalars off matrix arguments inside quadratic probes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.