Encyclopedia Gravity Gravity Analysis Regge Ttalgebraic Closer Continuum Moment Eq Half Adjugate

ARTICLE 4 claims 4 theorems

Gravity Analysis Regge Ttalgebraic Closer Continuum Moment Eq Half Adjugate

A machine-checked proof shows that a certain continuum limit in a lattice gravity model collapses to half the adjugate quadratic form, but only for symmetric matrices.

Verify this page

The closed form

The declaration continuumMoment_eq_half_adjugate is a proved theorem in the Recognition Science framework's machine-checked library of formal theorems. It states that for every symmetric 3 by 3 real matrix E and every real direction vector x, a certain continuum-limit moment, built from a periodic lattice assembly, equals (1/2) times xᵀ adj(E) x. Here adj(E) is the classical adjugate matrix, whose entries are signed minors of E. The theorem is a closed-form simplification: a complicated sum over lattice buckets collapses into a single quadratic expression.

The proof works by identifying the production chain's continuum limit with a bridge construction that uses the same geometric tables, then verifying a committed algebraic spike certificate. The key step is a linear_combination certificate over three symmetry generators, which checks the identity by pure algebra. The theorem holds only under the three symmetry hypotheses E01=E10, E02=E20, E12=E21. Without symmetry, the difference is an exact rotational square that vanishes precisely on symmetric matrices. The theorem does not claim the identity for arbitrary non-symmetric matrices.

A companion theorem, adjugateQuadraticForm_tt, specializes to the transverse-traceless (TT) case: for symmetric, traceless E with x transverse to E, the adjugate quadratic form equals -(1/2)|x|²⟨E,E⟩. This leads to the isotropy value: for every nonzero integer mode and TT polarization, the continuum moment equals exactly reggeTTContinuumCoefficient = -(1/4). The finite assembly identity that feeds this result holds only at non-aliased side lengths; at finitely many aliased small N, the finite reduced symbol is not identified with the bucket fold, and no repair is attempted. The production chain consumes the identity through the eventual-filter form, which is all the continuum limit needs.

In plain terms, the theorem says that in this lattice model, the continuum limit of a certain moment is not a free function but a fixed quadratic form, and for TT polarizations it becomes a constant. This is a structural result about the model's behavior in the continuum limit, not a statement about physical gravity. The theorem is proved in the framework's library with no sorry, no admit, no new axioms, and the expected axiom footprint is the standard trio [propext, Classical.choice, Quot.sound].

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 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 reggeTTMoment_tt_value · IndisputableMonolith/Gravity/Analysis/ReggeTTAlgebraicCloser.lean
reggeTTMoment_tt_value · IndisputableMonolith/Gravity/Analysis/ReggeTTAlgebraicCloser.lean:369 
/-- **P1.1b HEADLINE (THEOREM): for every nonzero integer mode and every
TT polarization, the P1.1a continuum moment at the normalized real
direction equals exactly `reggeTTContinuumCoefficient = -(1/4)`.** -/
theorem reggeTTMoment_tt_value (m : Fin 3 → ℤ) (E : Fin 3 → Fin 3 → ℝ)
    (hm : ∃ i : Fin 3, m i ≠ 0) (hTT : IsTTPolarization m E) :
    reggeTTMoment ReggeTTBlochAssembly.rawCosineSupport
        (ReggeTTContinuumLimit.rawPhaseQuadratic
          (ReggeTTContinuumLimit.normalizedRealMode m))
        (ReggeTTBlochAssembly.rawBucketAmplitude E) =
      reggeTTContinuumCoefficient := by
  obtain ⟨hsymm, htrace, htrans, hnorm⟩ := hTT
  have hs : 0 < ReggeTTContinuumLimit.realModeNormSq (fun i => (m i : ℝ)) :=
    ReggeTTContinuumLimit.realModeNormSq_intCast_pos m hm
  have hxval : ∀ i : Fin 3,
      ReggeTTContinuumLimit.normalizedRealMode m i =
        (m i : ℝ) /
          Real.sqrt (ReggeTTContinuumLimit.realModeNormSq
            (fun j => (m j : ℝ))) := fun i => rfl
  have htr : E 0 0 + E 1 1 + E 2 2 = 0 := by
    have h := htrace
    rwa [Fin.sum_univ_three] at h
  have hxtrans : ∀ j : Fin 3,
      ReggeTTContinuumLimit.normalizedRealMode m 0 * E 0 j +
          ReggeTTContinuumLimit.normalizedRealMode m 1 * E 1 j +
          ReggeTTContinuumLimit.normalizedRealMode m 2 * E 2 j = 0 := by
    intro j
    have h := htrans j
    rw [Fin.sum_univ_three] at h
    rw [hxval 0, hxval 1, hxval 2, div_mul_eq_mul_div, div_mul_eq_mul_div,
      div_mul_eq_mul_div, div_add_div_same, div_add_div_same, h, zero_div]
  have hxnorm :
      ReggeTTContinuumLimit.normalizedRealMode m 0 ^ 2 +
          ReggeTTContinuumLimit.normalizedRealMode m 1 ^ 2 +
          ReggeTTContinuumLimit.normalizedRealMode m 2 ^ 2 = 1 := by
    have hsum : (m 0 : ℝ) ^ 2 + (m 1 : ℝ) ^ 2 + (m 2 : ℝ) ^ 2 =
        ReggeTTContinuumLimit.realModeNormSq (fun j => (m j : ℝ)) := by
      simp only [ReggeTTContinuumLimit.realModeNormSq, Fin.sum_univ_three]
    rw [hxval 0, hxval 1, hxval 2, div_pow, div_pow, div_pow,
      div_add_div_same, div_add_div_same, Real.sq_sqrt hs.le, hsum,
      div_self hs.ne']
  exact reggeTTMoment_tt_real E (ReggeTTContinuumLimit.normalizedRealMode m)
    (hsymm 0 1) (hsymm 0 2) (hsymm 1 2) htr (hxtrans 0) (hxtrans 1)
    (hxtrans 2) hxnorm hnorm
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

What this page does not claim

The theorem does not claim the identity for non-symmetric matrices. The theorem does not claim that the finite assembly identity holds at aliased side lengths. The theorem does not claim any direct physical interpretation of the constant -(1/4).

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