quadContr_eq_quadContr_symmetrize4
plain-language theorem explainer
For any real 4×4 matrix A and covector k, the quadratic contraction A_μν k^μ k^ν equals that of the componentwise symmetrization of A. Null-cone rigidity arguments cite this to discard antisymmetric junk before reconstructing matrices modulo η. The proof unfolds both contractions over Fin 4 and cancels by ring.
Claim. For every real $4\times 4$ matrix $A$ and every $k\in\mathbb{R}^4$, the quadratic contraction satisfies $A_{\mu\nu}k^\mu k^\nu=\bigl((A_{\mu\nu}+A_{\nu\mu})/2\bigr)k^\mu k^\nu$.
background
This module is the Phase 5 algebraic prerequisite: finite-dimensional real linear algebra showing that values of a symmetric quadratic form on all Minkowski-null covectors determine the symmetric matrix modulo a scalar multiple of the Minkowski metric η = diag(−1,1,1,1). It is not geometric curvature, Ricci, or the Einstein equation; Tier A stays open until an independent symmetric G is built from Recognition area/focusing ancestry.
The quadratic contraction is the scalar A_μν k^μ k^ν (double sum over Fin 4). Componentwise symmetrization sends A to (A_ij + A_ji)/2. A private Fin-4 sum expansion rewrites ∑_i f(i) as the four-term sum f(0)+f(1)+f(2)+f(3), so both sides become explicit multilinear polynomials in the entries of A and k.
proof idea
One short tactic proof. Unfold the quadratic contraction and the componentwise symmetrization, expand both Fin-4 double sums via the four-term sum lemma, then apply ring. The cross terms A_ij k_i k_j and A_ji k_i k_j average to the same bilinear form, so the antisymmetric remainder cancels identically for every k (null or not).
why it matters
This is the algebraic fact that antisymmetric parts are invisible to null-cone quadratic data. It is wired into the module certificate as the antisym_invisible field, and it underwrites the general reconstruction theorem: null-cone equality of quadratic contractions holds iff the symmetrizations differ by a scalar multiple of η. A sibling uses it to prove that the pure antisymmetrization contracts to zero.
In the Recognition gravity stack this is pure Tier-A algebra supporting later Clausius–Einstein bridge work. It does not construct horizons, Unruh temperature, or close the field equation; the module doc keeps those OPEN and forbids identifying any matrix here with Ricci or stress-energy.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.