quadContr_add
plain-language theorem explainer
Quadratic contraction of a real 4×4 matrix against a covector is additive in the matrix argument. Gravity reductions that split Einstein-shaped sources into Ricci plus metric terms cite this identity. The proof unfolds the double sum and distributes addition over products and finite sums.
Claim. For real $4\times 4$ matrices $A,B$ and any $k:\mathbb{R}^4$, the quadratic contraction obeys $(A+B)_{\mu\nu}k^\mu k^\nu = A_{\mu\nu}k^\mu k^\nu + B_{\mu\nu}k^\mu k^\nu$.
background
The ambient module treats an assumed Einstein-shaped matrix equation $\kappa T = \mathrm{Ric} + f,\eta$ and reduces it, by null contraction, to a scalar relation on Minkowski-null directions. Honesty tags mark the matrix algebra as theorem content and the inhabitation of the source hypothesis as external input.
Quadratic contraction is the bilinear form $A_{\mu\nu}k^\mu k^\nu$, written as the double sum $\sum_i\sum_j A_{ij}k_i k_j$ over $\mathrm{Fin},4$. It is the bridge object that turns a matrix field equation into a scalar along a chosen covector $k$.
Additivity in the matrix slot is the first algebraic property needed before one can peel a sum $\mathrm{Ric}+f\eta$ apart under contraction.
proof idea
Term-mode proof: unfold the double-sum definition of quadratic contraction, then simplify with matrix entrywise addition, distributivity of multiplication over addition, and additivity of finite sums. No external lemmas beyond those simp facts are required.
why it matters
Feeds the parent theorem that null-reduces one Einstein-shaped equation: once the source equals Ricci plus a scalar multiple of the Minkowski metric, additivity lets the contraction split, after which the metric term vanishes on null $k$ and one obtains $\mathrm{Ric}(k,k)=\kappa T(k,k)$. That step is the algebraic core of the RS null-scalar reduction; the module does not yet derive the sourced equation from the ledger or construct horizon patches. Within the gravity domain it is pure linear algebra supporting the conditional bridge from matrix sources to null scalars, with RS specialization of the coupling left to later certificates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.