adjugate02
plain-language theorem explainer
The (0,2) entry of the 3×3 adjugate equals the corresponding 2×2 minor determinant E₀₁E₁₂ − E₀₂E₁₁. Gravity analysts cite it when expanding the C8 kernel xᵀ adj(E) x into scalars. Proof is a one-line rewrite via Mathlib’s fin-three adjugate formula plus reflexivity.
Claim. For every real $3\times 3$ array $E$, the $(0,2)$ entry of $\mathrm{adj}(E)$ equals $E_{01}E_{12}-E_{02}E_{11}$.
background
This module is the Regge TT algebraic closer in the QG full-theory campaign (Paper C / Pillar 1, stage C-DAG3). Its headline target is the C8 closed form: the continuum-limit bucket moment equals $(1/2),x^{\mathsf T},\mathrm{adj}(E),x$ for symmetric polarization matrices $E$, with Mathlib’s matrix adjugate.
The adjugate of a $3\times 3$ matrix is the transpose of the cofactor matrix. Entry $(i,j)$ is $(\pm)$ the determinant of the complementary $2\times 2$ minor. The present lemma isolates the single scalar $\mathrm{adj}(E)_{02}$.
Sibling lemmas adjugate00, adjugate01, adjugate10, … supply the remaining eight entries so that the quadratic form can be written without matrix notation.
proof idea
One-line wrapper. Rewrite with Mathlib’s Matrix.adjugate_fin_three, which expands every entry of the $3\times 3$ adjugate as an explicit minor formula; the $(0,2)$ component matches the right-hand side definitionally, so rfl finishes.
why it matters
Feeds adjugateQuadraticForm_explicit, which expands $x^{\mathsf T},\mathrm{adj}(E),x$ into nine scalar monomials; the $(0,2)$ term appears as the coefficient of $x_0 x_2$. That explicit form is the bridge from the abstract C8 kernel equation continuumMoment_eq_half_adjugate to the TT isotropy evaluation adjugateQuadraticForm_tt and ultimately P1.1b (reggeTTMoment_tt_value), the continuum coefficient $-1/4$.
In the production DAG this module is the sole importer of the committed algebraic certificate spike. Without the nine cofactor identities the linear-combination certificates over the TT generators cannot discharge the eigenvalue identity $\mathrm{adj}(E)x=\lambda_1\lambda_2 x$ on the transverse-traceless variety.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.