Encyclopedia Gravity Gravity Analysis Regge Ttalgebraic Closer Committed Spike Lhs Eq Half Adjugate

ARTICLE 3 claims 3 theorems

Gravity Analysis Regge Ttalgebraic Closer Committed Spike Lhs Eq Half Adjugate

A machine-checked theorem reduces a complicated gravitational calculation to a simple algebraic formula, but only under strict symmetry conditions.

Verify this page

The half-adjugate identity

In the Recognition Science framework's study of gravity, a key calculation involves a quantity called the continuum-limit bucket moment. This object, built from a polarization matrix E and a direction vector x, encodes how a certain discrete geometric structure behaves in the limit of fine detail. The theorem committedSpikeLHS_eq_half_adjugate proves that this complicated moment equals a much simpler expression: one half of the quadratic form xᵀ·adj(E)·x, where adj(E) is the classical adjugate matrix (the transpose of the cofactor matrix). In plain language, it shows that a sum over geometric buckets collapses to a clean algebraic formula.

The identity holds for every symmetric 3×3 matrix E and every real vector x. Symmetry here means the matrix equals its own transpose: the entry in row i, column j equals the entry in row j, column i. The proof works by identifying the production chain's moment with a bridge fold, then using a committed spike block collapse, and finally verifying the result with a linear combination certificate over three symmetry generators. The theorem is a THEOREM in the framework's machine-checked library, meaning it has been verified by a computer proof assistant with no gaps or missing axioms.

The identity does not hold for arbitrary non-symmetric matrices. If the symmetry conditions fail, the difference between the two sides is an exact rotational square, a term that vanishes precisely when the matrix is symmetric. This is a deliberate scope restriction: the closed form is not claimed to be valid in all nine free entries of a general 3×3 matrix. The theorem's utility lies in the symmetric case, which is the case relevant to the framework's gravitational analysis.

This result is a stepping stone. From it, the framework derives a further theorem: for symmetric, traceless, and x-transverse matrices E, the adjugate quadratic form simplifies to -(1/2)·|x|²·⟨E,E⟩, where ⟨E,E⟩ is the Frobenius inner product. This leads to the isotropy value of -(1/4) for the continuum moment, a constant that appears in the framework's gravitational theory. The half-adjugate identity is thus not an isolated algebraic curiosity; it is the algebraic core that makes the later physical results possible.

What the theorem does not claim is equally important. It does not assert that the identity holds for non-symmetric matrices. It does not claim to repair aliasing issues at certain small side lengths; those cases are explicitly disclosed as unrepaired. And it does not invoke the spike's own TT certificate, relying instead on block data and the Mathlib adjugate definition. The theorem is a precise, conditional statement about symmetric matrices, and its power comes from that precision.

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 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 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

What this page does not claim

The identity does not hold for non-symmetric matrices. The theorem does not repair aliasing issues at finitely many small side lengths. The result does not invoke the spike's own TT certificate, relying on block data instead.

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