Encyclopedia Gravity Gravity Analysis Regge Ttalgebraic Closer Committed Spike Lhs Spike Input Expand

ARTICLE 3 claims 3 theorems

Gravity Analysis Regge Ttalgebraic Closer Committed Spike Lhs Spike Input Expand

A machine-checked proof that a complicated gravitational sum collapses into a simple quadratic form, with the exact limits of that collapse spelled out.

Verify this page

The algebraic closer

The declaration committedSpikeLHS_spikeInput_expand is a theorem in the machine-checked library of formal theorems. It states that a certain large expression, built from a 3 by 3 matrix E and a three-dimensional vector x, can be rewritten as a sum of six simpler pieces. Those pieces come from a separate certificate file, and each one is a polynomial in the entries of E and x, with the constants √2, √3, and π appearing as fixed parameters.

The theorem is a rewriting step, not a new physical claim. It says the left-hand side, which is the continuum-limit moment of a gravitational assembly, equals the sum of those six polynomial blocks. This is the algebraic backbone that later theorems use to show the whole moment equals (1/2)·xᵀ·adj(E)·x, where adj(E) is the adjugate matrix. That closed form is what makes the subsequent isotropy result, the value -(1/4), computable in one line.

The proof is finite algebra. It expands the left-hand side by definition, then matches it against the six blocks. No sorry, no admit, no new axioms; the expected axiom footprint is the standard trio [propext, Classical.choice, Quot.sound]. The theorem is tagged THEOREM in the framework's accounting.

What the theorem does not claim is just as important. It does not assert that the six-block expansion is valid for all matrices. The closed form (1/2)·xᵀ·adj(E)·x holds only under the three symmetry hypotheses on E, meaning E must be symmetric. For a general nine-entry matrix, the difference is an exact rotational square, which vanishes precisely when E is symmetric. The theorem also does not repair aliasing: the finite assembly identity holds only at non-aliased side lengths, and at the finitely many aliased small N no repair is attempted. The production chain consumes the identity through the eventual-filter form, which is all the continuum limit needs. Unrepaired and disclosed.

In Recognition Science, this declaration is the algebraic closer. It takes the raw output of the geometric assembly and reduces it to a form that the rest of the chain can evaluate. The payoff is that the isotropy value -(1/4) is not a fitted constant but a proved consequence of the geometry. That is the step that turns a pile of bucket tables into a single number.

THEOREM committedSpikeLHS_spikeInput_expand · IndisputableMonolith/Gravity/Analysis/ReggeTTAlgebraicCloser.lean
committedSpikeLHS_spikeInput_expand · IndisputableMonolith/Gravity/Analysis/ReggeTTAlgebraicCloser.lean:217 
/-- Definitional expansion of the committed spike LHS at a marshalled
matrix/direction pair (structure-projection reduction only). -/
theorem committedSpikeLHS_spikeInput_expand (E : Fin 3 → Fin 3 → ℝ)
    (x : Fin 3 → ℝ) :
    ReggeTTBlochConventionAudit.committedSpikeLHS
        (ReggeTTBlochConventionAudit.spikeInput E x) =
      ReggeTTContinuumCertificateSpike.tetBlock0 (E 0 0) (E 0 1) (E 0 2)
          (E 1 0) (E 1 1) (E 1 2) (E 2 0) (E 2 1) (E 2 2) (x 0) (x 1) (x 2)
          (Real.sqrt 2) (Real.sqrt 3) Real.pi +
        ReggeTTContinuumCertificateSpike.tetBlock1 (E 0 0) (E 0 1) (E 0 2)
          (E 1 0) (E 1 1) (E 1 2) (E 2 0) (E 2 1) (E 2 2) (x 0) (x 1) (x 2)
          (Real.sqrt 2) (Real.sqrt 3) Real.pi +
        ReggeTTContinuumCertificateSpike.tetBlock2 (E 0 0) (E 0 1) (E 0 2)
          (E 1 0) (E 1 1) (E 1 2) (E 2 0) (E 2 1) (E 2 2) (x 0) (x 1) (x 2)
          (Real.sqrt 2) (Real.sqrt 3) Real.pi +
        ReggeTTContinuumCertificateSpike.tetBlock3 (E 0 0) (E 0 1) (E 0 2)
          (E 1 0) (E 1 1) (E 1 2) (E 2 0) (E 2 1) (E 2 2) (x 0) (x 1) (x 2)
          (Real.sqrt 2) (Real.sqrt 3) Real.pi +
        ReggeTTContinuumCertificateSpike.tetBlock4 (E 0 0) (E 0 1) (E 0 2)
          (E 1 0) (E 1 1) (E 1 2) (E 2 0) (E 2 1) (E 2 2) (x 0) (x 1) (x 2)
          (Real.sqrt 2) (Real.sqrt 3) Real.pi +
        ReggeTTContinuumCertificateSpike.tetBlock5 (E 0 0) (E 0 1) (E 0 2)
          (E 1 0) (E 1 1) (E 1 2) (E 2 0) (E 2 1) (E 2 2) (x 0) (x 1) (x 2)
          (Real.sqrt 2) (Real.sqrt 3) Real.pi := rfl

set_option maxHeartbeats 3200000 in
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

What this page does not claim

The theorem does not prove the closed form for non-symmetric matrices E. The theorem does not repair the aliasing failure at small side lengths. The theorem does not itself establish the isotropy value -(1/4); that is a separate 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