Encyclopedia Gravity Gravity Analysis Regge Ttalgebraic Closer Adjugate Quadratic Form Explicit

ARTICLE 5 claims 5 theorems

Gravity Analysis Regge Ttalgebraic Closer Adjugate Quadratic Form Explicit

A machine-checked proof rewrites a complicated sum over a 3 by 3 matrix into a compact form, a step toward showing gravity's discrete structure becomes isotropic at large scales.

Verify this page

The adjugate identity

In linear algebra, the adjugate of a 3 by 3 matrix is a second matrix built from its nine cofactors; multiplying the adjugate by a vector on both sides produces a quadratic form, a single number that depends quadratically on the vector's three components. The declaration adjugateQuadraticForm_explicit in the framework's machine-checked library of formal theorems proves that this number, written as a sum over all nine entries of the adjugate, expands into a specific polynomial with eighteen explicit terms. Each term is a product of two vector components and one 2 by 2 minor of the original matrix, such as x0 times (E11*E22 - E12*E21) times x0. The theorem is a definitional expansion: it takes the compact sum and writes it out in full, so that any later proof can use the expanded form without re-deriving it.

The expansion matters because it sits inside a longer argument about gravity. The framework models spacetime as a discrete structure built from tetrahedra, and it studies how a polarization matrix E, which describes a gravitational wave's two independent directions of strain, behaves as the lattice spacing shrinks to zero. A key quantity is the continuum-limit moment, a sum over the lattice's cells that depends on E and a direction vector x. The library proves that this moment equals one half of the adjugate quadratic form, and the explicit expansion is the algebraic bridge that makes the equality checkable term by term. From there, a separate theorem shows that when E is symmetric, traceless, and transverse to x, the adjugate form collapses to a strikingly simple value: -(1/2) times the squared length of x times the sum of squares of all entries of E. This is the isotropy result: after normalizing both E and x to unit size, the moment becomes exactly -(1/4), independent of the direction x or the specific polarization E.

The theorem itself makes no claim about physics. It is pure finite algebra over the real numbers, a statement about 3 by 3 matrices and vectors, proved by unfolding definitions and checking each of the nine cofactor formulas. The library's documentation states that the proof uses no sorry, no admit, and no new axioms; the expected axiom footprint is the standard trio of the ambient type theory. The expansion's scope is also explicit: it holds for every real 3 by 3 matrix E and every real vector x, with no symmetry or transversality assumptions. Those extra conditions appear only in the later theorems that use the expansion, not in the expansion itself.

What the declaration does not claim is equally precise. It does not assert that the adjugate quadratic form equals the continuum moment; that is a separate theorem, continuumMoment_eq_half_adjugate, which requires E to be symmetric. It does not claim the isotropy value -(1/4) for arbitrary E and x; that result needs the full set of TT conditions. It does not say anything about the physical interpretation of the moment, only that a certain algebraic expression equals another. The expansion is a tool, not a result about gravity by itself.

THEOREM adjugateQuadraticForm_explicit · IndisputableMonolith/Gravity/Analysis/ReggeTTAlgebraicCloser.lean
adjugateQuadraticForm_explicit · IndisputableMonolith/Gravity/Analysis/ReggeTTAlgebraicCloser.lean:197 
/-- Fully explicit scalar form of the adjugate quadratic form. -/
theorem adjugateQuadraticForm_explicit (E : Fin 3 → Fin 3 → ℝ)
    (x : Fin 3 → ℝ) :
    adjugateQuadraticForm E x =
      x 0 * (E 1 1 * E 2 2 - E 1 2 * E 2 1) * x 0 +
        x 0 * (-(E 0 1 * E 2 2) + E 0 2 * E 2 1) * x 1 +
        x 0 * (E 0 1 * E 1 2 - E 0 2 * E 1 1) * x 2 +
        (x 1 * (-(E 1 0 * E 2 2) + E 1 2 * E 2 0) * x 0 +
          x 1 * (E 0 0 * E 2 2 - E 0 2 * E 2 0) * x 1 +
          x 1 * (-(E 0 0 * E 1 2) + E 0 2 * E 1 0) * x 2) +
        (x 2 * (E 1 0 * E 2 1 - E 1 1 * E 2 0) * x 0 +
          x 2 * (-(E 0 0 * E 2 1) + E 0 1 * E 2 0) * x 1 +
          x 2 * (E 0 0 * E 1 1 - E 0 1 * E 1 0) * x 2) := by
  unfold adjugateQuadraticForm
  simp only [Fin.sum_univ_three]
  rw [adjugate00, adjugate01, adjugate02, adjugate10, adjugate11,
    adjugate12, adjugate20, adjugate21, adjugate22]
THEOREM adjugateQuadraticForm_explicit · IndisputableMonolith/Gravity/Analysis/ReggeTTAlgebraicCloser.lean
adjugateQuadraticForm_explicit · IndisputableMonolith/Gravity/Analysis/ReggeTTAlgebraicCloser.lean:197 
/-- Fully explicit scalar form of the adjugate quadratic form. -/
theorem adjugateQuadraticForm_explicit (E : Fin 3 → Fin 3 → ℝ)
    (x : Fin 3 → ℝ) :
    adjugateQuadraticForm E x =
      x 0 * (E 1 1 * E 2 2 - E 1 2 * E 2 1) * x 0 +
        x 0 * (-(E 0 1 * E 2 2) + E 0 2 * E 2 1) * x 1 +
        x 0 * (E 0 1 * E 1 2 - E 0 2 * E 1 1) * x 2 +
        (x 1 * (-(E 1 0 * E 2 2) + E 1 2 * E 2 0) * x 0 +
          x 1 * (E 0 0 * E 2 2 - E 0 2 * E 2 0) * x 1 +
          x 1 * (-(E 0 0 * E 1 2) + E 0 2 * E 1 0) * x 2) +
        (x 2 * (E 1 0 * E 2 1 - E 1 1 * E 2 0) * x 0 +
          x 2 * (-(E 0 0 * E 2 1) + E 0 1 * E 2 0) * x 1 +
          x 2 * (E 0 0 * E 1 1 - E 0 1 * E 1 0) * x 2) := by
  unfold adjugateQuadraticForm
  simp only [Fin.sum_univ_three]
  rw [adjugate00, adjugate01, adjugate02, adjugate10, adjugate11,
    adjugate12, adjugate20, adjugate21, adjugate22]
THEOREM continuumMoment_eq_half_adjugate · IndisputableMonolith/Gravity/Analysis/ReggeTTAlgebraicCloser.lean
continuumMoment_eq_half_adjugate · IndisputableMonolith/Gravity/Analysis/ReggeTTAlgebraicCloser.lean:285 
/-- **THE C8 CLOSED FORM, PRODUCTION HEADLINE (THEOREM): the continuum
bucket moment fold of the P1.1a limit equals `(1/2)·xᵀ·adj(E)·x` for every
symmetric polarization matrix and every real direction.** -/
theorem continuumMoment_eq_half_adjugate (E : Fin 3 → Fin 3 → ℝ)
    (x : Fin 3 → ℝ)
    (hsym01 : E 0 1 = E 1 0) (hsym02 : E 0 2 = E 2 0)
    (hsym12 : E 1 2 = E 2 1) :
    reggeTTMoment ReggeTTBlochAssembly.rawCosineSupport
        (ReggeTTContinuumLimit.rawPhaseQuadratic x)
        (ReggeTTBlochAssembly.rawBucketAmplitude E) =
      (1 / 2) * adjugateQuadraticForm E x := by
  rw [continuumMoment_eq_bridgeMoment]
  exact bridgeMoment_eq_half_adjugate E x hsym01 hsym02 hsym12
THEOREM adjugateQuadraticForm_tt · IndisputableMonolith/Gravity/Analysis/ReggeTTAlgebraicCloser.lean
adjugateQuadraticForm_tt · IndisputableMonolith/Gravity/Analysis/ReggeTTAlgebraicCloser.lean:302 
/-- **STEP (ii) OF THE C8 CLOSED FORM (THEOREM): on the TT variety the
adjugate quadratic form collapses to `-(1/2)·|x|²·⟨E,E⟩`.**  Kernel form
of the eigenvalue argument (`x` is a null eigenvector of `E`, so
`adj(E)x = λ₁λ₂x` with `λ₁ + λ₂ = 0`), discharged as an explicit cofactor
certificate over the seven TT generators. -/
theorem adjugateQuadraticForm_tt (E : Fin 3 → Fin 3 → ℝ) (x : Fin 3 → ℝ)
    (hsym01 : E 0 1 = E 1 0) (hsym02 : E 0 2 = E 2 0)
    (hsym12 : E 1 2 = E 2 1)
    (htr : E 0 0 + E 1 1 + E 2 2 = 0)
    (htrans0 : x 0 * E 0 0 + x 1 * E 1 0 + x 2 * E 2 0 = 0)
    (htrans1 : x 0 * E 0 1 + x 1 * E 1 1 + x 2 * E 2 1 = 0)
    (htrans2 : x 0 * E 0 2 + x 1 * E 1 2 + x 2 * E 2 2 = 0) :
    adjugateQuadraticForm E x =
      -(1 / 2) * (x 0 ^ 2 + x 1 ^ 2 + x 2 ^ 2) *
        (E 0 0 * E 0 0 + E 0 1 * E 0 1 + E 0 2 * E 0 2 + E 1 0 * E 1 0 +
          E 1 1 * E 1 1 + E 1 2 * E 1 2 + E 2 0 * E 2 0 + E 2 1 * E 2 1 +
          E 2 2 * E 2 2) := by
  rw [adjugateQuadraticForm_explicit]
  linear_combination
    (E 0 0 * x 0 * x 1 - E 0 1 * x 0 ^ 2 / 2 + E 0 1 * x 1 ^ 2 / 2 +
        E 0 1 * x 2 ^ 2 / 2 - E 1 0 * x 0 ^ 2 / 2 - E 1 0 * x 1 ^ 2 / 2 -
        E 1 0 * x 2 ^ 2 / 2 - E 2 1 * x 0 * x 2 + E 2 2 * x 0 * x 1) *
      hsym01 +
    (E 0 0 * x 0 * x 2 - E 0 2 * x 0 ^ 2 / 2 + E 0 2 * x 1 ^ 2 / 2 +
        E 0 2 * x 2 ^ 2 / 2 + E 1 1 * x 0 * x 2 - E 1 2 * x 0 * x 1 -
        E 2 0 * x 0 ^ 2 / 2 - E 2 0 * x 1 ^ 2 / 2 - E 2 0 * x 2 ^ 2 / 2) *
      hsym02 +
    (E 0 0 * x 1 * x 2 - E 0 2 * x 0 * x 1 + E 1 1 * x 1 * x 2 +
        E 1 2 * x 0 ^ 2 / 2 - E 1 2 * x 1 ^ 2 / 2 + E 1 2 * x 2 ^ 2 / 2 -
        E 2 1 * x 0 ^ 2 / 2 - E 2 1 * x 1 ^ 2 / 2 - E 2 1 * x 2 ^ 2 / 2) *
      hsym12 +
    (-(E 0 0 * x 0 ^ 2) / 2 + E 0 0 * x 1 ^ 2 / 2 + E 0 0 * x 2 ^ 2 / 2 -
        2 * E 0 1 * x 0 * x 1 - E 0 2 * x 0 * x 2 + E 1 1 * x 0 ^ 2 / 2 -
        E 1 1 * x 1 ^ 2 / 2 + E 1 1 * x 2 ^ 2 / 2 - E 1 2 * x 1 * x 2 +
        E 2 2 * x 0 ^ 2 / 2 + E 2 2 * x 1 ^ 2 / 2 + E 2 2 * x 2 ^ 2 / 2) *
      htr +
    (E 0 0 * x 0 + E 0 1 * x 1 + E 0 2 * x 2) * htrans0 +
    (E 0 1 * x 0 + E 1 1 * x 1 + E 1 2 * x 2) * htrans1 +
    (-(E 0 0 * x 2) + E 0 2 * x 0 - E 1 1 * x 2 + E 1 2 * x 1) * htrans2
THEOREM reggeTTMoment_tt_real · IndisputableMonolith/Gravity/Analysis/ReggeTTAlgebraicCloser.lean
reggeTTMoment_tt_real · IndisputableMonolith/Gravity/Analysis/ReggeTTAlgebraicCloser.lean:344 
/-- The moment value at unit-normalized real TT data: the fold equals
exactly `reggeTTContinuumCoefficient = -(1/4)`. -/
theorem reggeTTMoment_tt_real (E : Fin 3 → Fin 3 → ℝ) (x : Fin 3 → ℝ)
    (hsym01 : E 0 1 = E 1 0) (hsym02 : E 0 2 = E 2 0)
    (hsym12 : E 1 2 = E 2 1)
    (htr : E 0 0 + E 1 1 + E 2 2 = 0)
    (htrans0 : x 0 * E 0 0 + x 1 * E 1 0 + x 2 * E 2 0 = 0)
    (htrans1 : x 0 * E 0 1 + x 1 * E 1 1 + x 2 * E 2 1 = 0)
    (htrans2 : x 0 * E 0 2 + x 1 * E 1 2 + x 2 * E 2 2 = 0)
    (hxnorm : x 0 ^ 2 + x 1 ^ 2 + x 2 ^ 2 = 1)
    (hEnorm : (∑ i : Fin 3, ∑ j : Fin 3, E i j * E i j) = 1) :
    reggeTTMoment ReggeTTBlochAssembly.rawCosineSupport
        (ReggeTTContinuumLimit.rawPhaseQuadratic x)
        (ReggeTTBlochAssembly.rawBucketAmplitude E) =
      reggeTTContinuumCoefficient := by
  have hEnorm' := hEnorm
  simp only [Fin.sum_univ_three] at hEnorm'
  have hcoeff : reggeTTContinuumCoefficient = -(1 / 4 : ℝ) := rfl
  rw [continuumMoment_eq_half_adjugate E x hsym01 hsym02 hsym12,
    adjugateQuadraticForm_tt E x hsym01 hsym02 hsym12 htr htrans0 htrans1
      htrans2, hcoeff]
  linear_combination
    (-(1 / 4 : ℝ) * (x 0 ^ 2 + x 1 ^ 2 + x 2 ^ 2)) * hEnorm' +
      (-(1 / 4 : ℝ)) * hxnorm

What this page does not claim

The expansion itself does not assert equality with the continuum moment, which requires the symmetry conditions. The theorem does not claim the isotropy value -(1/4) holds for arbitrary matrices and vectors. The declaration makes no statement about the physical meaning of the moment, only about algebraic equality.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Gravity/Analysis/ReggeTTAlgebraicCloser.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND