quadContr_neg
plain-language theorem explainer
Quadratic contraction of a real 4×4 matrix against a covector is even under sign flip of that covector. Anyone reconstructing a symmetric matrix from null-cone values cites this when extending future-directed data to the full light cone. The proof unfolds the double sum and cancels the two minus signs by elementary ring arithmetic.
Claim. For any real $4\times 4$ matrix $A$ and any covector $k\in\mathbb{R}^4$, the quadratic contraction satisfies $A_{\mu\nu}(-k)^\mu(-k)^\nu = A_{\mu\nu} k^\mu k^\nu$.
background
The ambient module is a finite-dimensional linear-algebra package: values of a symmetric quadratic form on Minkowski-null covectors determine the symmetric matrix modulo a scalar multiple of $\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 the bilinear pairing $A_{\mu\nu}k^\mu k^\nu$, written as a double sum over $\mathrm{Fin},4$. Minkowski nullness uses the standard $(-,+,+,+)$ signature. The module imports only the Clausius–Einstein bridge definitions; it does not construct horizons, Unruh temperature, or close the Einstein equation.
Evenness under $k\mapsto -k$ is the elementary algebraic fact needed to pass from future-directed null data to the full null cone.
proof idea
Unfold the double-sum definition of the quadratic contraction. Apply sum congruence in each index, replace each component of $-k$ by its negation, and finish with ring: the product of two minus signs restores $k_i k_j$. No external lemmas beyond the definition are required.
why it matters
The immediate parent is the theorem that agreement of two quadratic contractions on every future nonzero Minkowski-null vector extends to the whole null cone. That parent explicitly cites quadratic evenness to handle negative-time null vectors (and notes that a null vector with vanishing time component is zero).
In the Recognition gravity stack this is Tier-A algebra inside the null-cone quadratic tensor class: it supports reconstruction of symmetric matrices modulo $\eta$ without claiming geometric curvature, continuum Ricci, or EFE closure. Phase 5 still needs an independently constructed symmetric $G$ with Recognition area/focusing ancestry; this lemma only clears the sign-flip step on the null cone.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.