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

ARTICLE 4 claims 4 theorems

Gravity Analysis Regge Ttalgebraic Closer Bridge Moment Eq Half Adjugate

A machine-checked theorem reduces a complicated gravitational wave calculation to half of a simple matrix expression, with the exact conditions under which it holds.

Verify this page

The bridge moment identity

In the Recognition Science framework's analysis of gravitational waves, a central object is the moment, a weighted sum that measures how a wave's amplitude pattern responds to a chosen direction. The declaration bridgeMoment_eq_half_adjugate proves that, for a symmetric 3x3 matrix E and a real direction vector x, this moment equals exactly (1/2) · xᵀ · adj(E) · x, where adj(E) is the classical adjugate matrix (the transpose of the cofactor matrix). The theorem is verified in the framework's machine-checked library of formal theorems, with no unproved assumptions beyond the standard logical axioms.

The identity holds under three symmetry conditions on E: its off-diagonal entries must be equal (E01 = E10, E02 = E20, E12 = E21). This is not a trivial algebraic accident. The proof proceeds by identifying the production chain's moment with a bridge fold, then collapsing a committed spike expression through block data, and finally applying a linear combination certificate over the three symmetry generators. The result is a clean closed form where a complicated sum over tetrahedral blocks reduces to a single quadratic form.

The theorem does not claim the identity holds for arbitrary non-symmetric matrices. The free-entry difference is exactly the rotational square -(1/8)·(E01·x2 - E02·x1 - E10·x2 + E12·x0 + E20·x1 - E21·x0)², which vanishes precisely on symmetric E. It also does not claim the finite assembly identity holds at aliased side lengths, where N divides 2·mᵢ for some mode component; those cases are disclosed as unrepaired and the production chain consumes the identity only through the eventual-filter form that the continuum limit requires.

In the framework's broader campaign, this closed form feeds the isotropy result: for transverse-traceless polarizations, the moment at the normalized direction equals exactly -(1/4), independent of the mode. The bridge moment identity is the algebraic closer that makes that isotropy value a proved theorem rather than a numerical observation.

THEOREM bridgeMoment_eq_half_adjugate · IndisputableMonolith/Gravity/Analysis/ReggeTTAlgebraicCloser.lean
bridgeMoment_eq_half_adjugate · IndisputableMonolith/Gravity/Analysis/ReggeTTAlgebraicCloser.lean:272 
/-- The Gate B bridge moment fold equals the closed form for symmetric
polarizations. -/
theorem bridgeMoment_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 ReggeTTGateBBridge.rawMomentSupport
        (ReggeTTGateBBridge.rawPhaseQuadratic x)
        (ReggeTTGateBBridge.rawBucketAmplitude E) =
      (1 / 2) * adjugateQuadraticForm E x := by
  rw [ReggeTTGateBBridge.rawMoment_eq_committedSpikeLHS,
    committedSpikeLHS_eq_half_adjugate E x hsym01 hsym02 hsym12]
THEOREM bridgeMoment_eq_half_adjugate · IndisputableMonolith/Gravity/Analysis/ReggeTTAlgebraicCloser.lean
bridgeMoment_eq_half_adjugate · IndisputableMonolith/Gravity/Analysis/ReggeTTAlgebraicCloser.lean:272 
/-- The Gate B bridge moment fold equals the closed form for symmetric
polarizations. -/
theorem bridgeMoment_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 ReggeTTGateBBridge.rawMomentSupport
        (ReggeTTGateBBridge.rawPhaseQuadratic x)
        (ReggeTTGateBBridge.rawBucketAmplitude E) =
      (1 / 2) * adjugateQuadraticForm E x := by
  rw [ReggeTTGateBBridge.rawMoment_eq_committedSpikeLHS,
    committedSpikeLHS_eq_half_adjugate E x hsym01 hsym02 hsym12]
THEOREM committedSpikeLHS_eq_half_adjugate · IndisputableMonolith/Gravity/Analysis/ReggeTTAlgebraicCloser.lean
committedSpikeLHS_eq_half_adjugate · IndisputableMonolith/Gravity/Analysis/ReggeTTAlgebraicCloser.lean:243 
/-- **STEP (i) OF THE C8 CLOSED FORM (THEOREM): the committed spike block
sum equals `(1/2)·xᵀ·adj(E)·x` for every symmetric `E` and every `x`.**
The three symmetry hypotheses are consumed through an explicit rotational
cofactor certificate (the free-entry difference is
`-(1/8)·(E₀₁x₂ − E₀₂x₁ − E₁₀x₂ + E₁₂x₀ + E₂₀x₁ − E₂₁x₀)²`, disclosed in
the module docstring).  Only the spike block DATA (`tetBlock*_eq`) is
used; the spike's own TT certificate is never invoked. -/
theorem committedSpikeLHS_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) :
    ReggeTTBlochConventionAudit.committedSpikeLHS
        (ReggeTTBlochConventionAudit.spikeInput E x) =
      (1 / 2) * adjugateQuadraticForm E x := by
  rw [committedSpikeLHS_spikeInput_expand, adjugateQuadraticForm_explicit]
  rw [ReggeTTContinuumCertificateSpike.tetBlock0_eq,
    ReggeTTContinuumCertificateSpike.tetBlock1_eq,
    ReggeTTContinuumCertificateSpike.tetBlock2_eq,
    ReggeTTContinuumCertificateSpike.tetBlock3_eq,
    ReggeTTContinuumCertificateSpike.tetBlock4_eq,
    ReggeTTContinuumCertificateSpike.tetBlock5_eq]
  linear_combination
    (-(1 / 8) * (E 0 1 * x 2 - E 0 2 * x 1 - E 1 0 * x 2 + E 1 2 * x 0 +
        E 2 0 * x 1 - E 2 1 * x 0) * x 2) * hsym01 +
      ((1 / 8) * (E 0 1 * x 2 - E 0 2 * x 1 - E 1 0 * x 2 + E 1 2 * x 0 +
        E 2 0 * x 1 - E 2 1 * x 0) * x 1) * hsym02 +
      (-(1 / 8) * (E 0 1 * x 2 - E 0 2 * x 1 - E 1 0 * x 2 + E 1 2 * x 0 +
        E 2 0 * x 1 - E 2 1 * x 0) * x 0) * hsym12
THEOREM continuumMoment_eq_bridgeMoment · IndisputableMonolith/Gravity/Analysis/ReggeTTAlgebraicCloser.lean
continuumMoment_eq_bridgeMoment · IndisputableMonolith/Gravity/Analysis/ReggeTTAlgebraicCloser.lean:141 
/-- The production continuum moment fold IS the Gate B bridge moment fold. -/
theorem continuumMoment_eq_bridgeMoment (E : Fin 3 → Fin 3 → ℝ)
    (x : Fin 3 → ℝ) :
    reggeTTMoment ReggeTTBlochAssembly.rawCosineSupport
        (ReggeTTContinuumLimit.rawPhaseQuadratic x)
        (ReggeTTBlochAssembly.rawBucketAmplitude E) =
      reggeTTMoment ReggeTTGateBBridge.rawMomentSupport
        (ReggeTTGateBBridge.rawPhaseQuadratic x)
        (ReggeTTGateBBridge.rawBucketAmplitude E) := by
  rw [rawCosineSupport_eq_rawMomentSupport, rawBucketAmplitude_eq,
    rawPhaseQuadratic_eq]

What this page does not claim

The identity does not hold for non-symmetric matrices, where a rotational square term appears. The theorem does not address aliased finite side lengths where N divides 2·mᵢ. The result does not itself derive the isotropy value -(1/4); that requires the additional adjugate quadratic form theorem.

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