quadContr
plain-language theorem explainer
Defines the quadratic contraction of a real 4×4 matrix A against a 4-vector k as ∑_{i,j} A_{ij} k_i k_j. This is the elementary bilinear form used throughout the algebraic Clausius–Einstein hinge: null-cut equality, rigidity of symmetric tensors on the Minkowski null cone, and the Einstein-shaped conclusion all speak in this language. The body is a direct double sum; no proof content.
Claim. For a real $4\times 4$ matrix $A$ and a real 4-vector $k$, the quadratic contraction is $A(k,k) := \sum_{i=0}^{3}\sum_{j=0}^{3} A_{ij}\, k_i k_j$.
background
The module isolates the finite-dimensional linear algebra behind Jacobson's thermodynamic route to the Einstein equation. Equality of two symmetric quadratic forms on every Minkowski-null direction determines their difference only up to a scalar multiple of the metric; an all-null local Clausius balance therefore has the algebraic shape of Einstein's equation, with the metric term free.
The ambient signature is the standard Lorentzian form $\eta=\mathrm{diag}(-1,+1,+1,+1)$ on $\mathbb{R}^4$. A vector $k$ is Minkowski-null when $\eta(k,k)=0$. Symmetric $4\times 4$ matrices are the tensors that appear as stress-like and Ricci-like sides of the local Clausius interface. The quadratic contraction is the evaluation map that turns those matrices into scalar null-cut data.
The module deliberately stays clear of continuum focusing, horizon construction, and any ledger-deficit-to-hinge identification; it only needs this algebraic pairing.
proof idea
Pure definition: the body is the double finite sum $\sum_i\sum_j A_{ij} k_i k_j$ over Fin 4. No lemmas are applied. Downstream lemmas such as quadContr_minkowskiEta4 expand the sum against the explicit Minkowski matrix and simplify by ring arithmetic.
why it matters
Every null-cut statement in the bridge is phrased with this contraction. It feeds pointwise_eq_implies_null_cut_eq, the counterexample null_cut_eq_not_pointwise_eq (metric vs zero agree on null vectors), the rigidity theorem null_quadratic_zero_eq_scalar_eta (vanishing null contractions force a pure metric multiple), and the two-tensor form null_quadratic_eq_of_diff_scalar_eta. Those assemble into einstein_equation_shaped_of_local_clausius: equal null contractions of symmetric stress-like and Ricci-like tensors imply Einstein shape up to a free scalar metric term.
It is also the evaluation map for the null-cone quadratic tensor class used outside this file. In the Recognition gravity stack this is the algebraic hinge that converts an assumed local Clausius balance into Einstein form without fixing the cosmological term by conservation, matching the classical Jacobson step before that fix.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.