Symmetric4
plain-language theorem explainer
Componentwise symmetry for real 4×4 matrices, read as covariant 2-tensors on Minkowski space. Every Clausius–Einstein bridge lemma that treats stress-like or Ricci-like tensors assumes this predicate. The body is the standard identity A_ij = A_ji on Fin 4 indices; no proof content.
Claim. A real $4\times 4$ matrix $A$ is symmetric when $A_{ij}=A_{ji}$ for all indices $i,j\in\{0,1,2,3\}$.
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 fixes their difference only up to a scalar multiple of the metric, so an all-null local Clausius balance has the algebraic shape of Einstein's equation with a free metric term.
In that setting one works with real matrices indexed by Fin 4, standing for components of covariant 2-tensors in a fixed Lorentz frame. The companion objects are the standard (−,+,+,+) Minkowski matrix, the quadratic contraction of a matrix against a covector, and the null-cone predicate on those covectors. Symmetry of the matrix is the minimal algebraic hypothesis that makes those contractions well-defined as quadratic forms and that lets the null-rigidity lemmas apply.
proof idea
Pure definition: the proposition is the universal quantification that every pair of entries equals its transpose partner. No lemmas, no tactics.
why it matters
This predicate is the standing hypothesis on every stress-like and Ricci-like matrix in the bridge. Downstream, einstein_equation_shaped_of_local_clausius assumes it on both tensors before concluding an Einstein-shaped identity with free scalar metric term. The null-cone rigidity theorems (null_quadratic_zero_eq_scalar_eta, null_quadratic_eq_of_diff_scalar_eta) and the counterexample that null-cut equality is weaker than pointwise equality all take it as input. The algebraic null-quadratic class in NullConeQuadraticTensorClass packages the same symmetry into its representative condition. The module deliberately stops short of horizons, heat–flux identification, continuum focusing, or fixing the free scalar by conservation; symmetry is only the linear-algebra gate those later steps would need.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.