Encyclopedia Gravity Gravity Analysis Regge Ttcertificate Scratch Certificate Block Pertet

ARTICLE 3 claims 3 theorems

Gravity Analysis Regge Ttcertificate Scratch Certificate Block Pertet

A machine-checked proof that a long gravitational sum collapses to a compact identity, without claiming any physical law.

Verify this page

The certificate's scope

In the framework's machine-checked library of formal theorems, certificate_block_pertet is a proof that a specific, very long algebraic expression equals a much shorter one. The long expression is a sum of many terms, each involving squares of quantities labeled m0, m1, m2 and combinations of quantities labeled E00 through E22. The short expression on the other side is a compact combination of the same quantities. The theorem states that these two expressions are equal for any real numbers assigned to those labels, under the assumptions that two auxiliary numbers s2 and s3 satisfy s2² = 2 and s3² = 3.

This is a purely algebraic identity. It does not assert anything about gravity, spacetime, or physics. The quantities m0, m1, m2 and E00 through E22 are just real numbers in the statement; the theorem does not assign them any physical meaning. The proof works by expanding and simplifying both sides using the rules of arithmetic, a method the framework calls ring. The auxiliary conditions on s2 and s3 are needed because the long expression contains square roots, and the proof uses these conditions to eliminate them.

The declaration sits in a file named ReggeTTCertificateScratch, suggesting it is a preliminary step in a larger project about Regge calculus, a discrete approach to general relativity. The docstring calls it a 'pre-cancellation certificate block', meaning it verifies an algebraic identity that appears before some cancellation step in a computation. The theorem itself, however, makes no reference to Regge calculus, general relativity, or any physical theory. It is a standalone statement about real numbers.

What the declaration does not claim is as important as what it does. It does not claim that the quantities m0, m1, m2 represent masses or that E00 through E22 represent components of a metric tensor. It does not claim that the identity has any physical consequence. It does not claim that the framework derives general relativity or any part of it. The theorem is a piece of formal algebra, verified by a computer, and its significance, if any, for physics would come from how it is used elsewhere, not from the statement itself.

THEOREM certificate_block_pertet · IndisputableMonolith/Gravity/Analysis/ReggeTTCertificateScratch.lean
certificate_block_pertet · IndisputableMonolith/Gravity/Analysis/ReggeTTCertificateScratch.lean:43 · truncated 
/-- Pre-cancellation certificate block: 4*M as the literal per-tet sum with
s2, s3 opaque; the offline lift cofactors are 0, so `linear_combination`
with 0-coefficients (= `ring1` on the difference) closes it. -/
theorem certificate_block_pertet
    (E00 E01 E02 E11 E12 E22 m0 m1 m2 s2 s3 : ℝ)
    (hs2 : s2 ^ 2 = 2) (hs3 : s3 ^ 2 = 3) :
    (((1 : ℝ)/2) * ((0 : ℝ)) * (E00) * (E00 + 2*E01 + E11) * (m1)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E00) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (m1 + m2)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E00) * (E11) * (m0 + m1)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00) * (E11 + 2*E12 + E22) * (m0 + m1 + m2)^2
      + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E00) * (E22) * (m0 + 2*m1 + m2)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E00 + 2*E01 + E11) * (E00) * (-m1)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + 2*E01 + E11) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (m2)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/4)) * (E00 + 2*E01 + E11) * (E11) * (m0)^2
      + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E00 + 2*E01 + E11) * (E11 + 2*E12 + E22) * (m0 + m2)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + 2*E01 + E11) * (E22) * (m0 + m1 + m2)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (E00) * (-m1 - m2)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (E00 + 2*E01 + E11) * (-m2)^2
      + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (E11) * (m0 - m2)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (E11 + 2*E12 + E22) * (m0)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (E22) * (m0 + m1)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E11) * (E00) * (-m0 - m1)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/4)) * (E11) * (E00 + 2*E01 + E11) * (-m0)^2
      + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E11) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (-m0 + m2)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/4)) * (E11) * (E11 + 2*E12 + E22) * (m2)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E11) * (E22) * (m1 + m2)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E11 + 2*E12 + E22) * (E00) * (-m0 - m1 - m2)^2
      + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E11 + 2*E12 + E22) * (E00 + 2*E01 + E11) * (-m0 - m2)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E11 + 2*E12 + E22) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (-m0)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/4)) * (E11 + 2*E12 + E22) * (E11) * (-m2)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E11 + 2*E12 + E22) * (E22) * (m1)^2
      + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E22) * (E00) * (-m0 - 2*m1 - m2)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E22) * (E00 + 2*E01 + E11) * (-m0 - m1 - m2)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E22) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (-m0 - m1)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E22) * (E11) * (-m1 - m2)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E22) * (E11 + 2*E12 + E22) * (-m1)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E00) * (E00 + 2*E02 + E22) * (m2)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E00) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (m1 + m2)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E00) * (E22) * (m0 + m2)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00) * (E11 + 2*E12 + E22) * (m0 + m1 + m2)^2
      + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E00) * (E11) * (m0 + m1 + 2*m2)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E00 + 2*E02 + E22) * (E00) * (-m2)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + 2*E02 + E22) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (m1)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/4)) * (E00 + 2*E02 + E22) * (E22) * (m0)^2
      + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E00 + 2*E02 + E22) * (E11 + 2*E12 + E22) * (m0 + m1)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + 2*E02 + E22) * (E11) * (m0 + m1 + m2)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (E00) * (-m1 - m2)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (E00 + 2*E02 + E22) * (-m1)^2
      + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (E22) * (m0 - m1)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (E11 + 2*E12 + E22) * (m0)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (E11) * (m0 + m2)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E22) * (E00) * (-m0 - m2)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/4)) * (E22) * (E00 + 2*E02 + E22) * (-m0)^2
      + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E22) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (-m0 + m1)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/4)) * (E22) * (E11 + 2*E12 + E22) * (m1)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E22) * (E11) * (m1 + m2)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E11 + 2*E12 + E22) * (E00) * (-m0 - m1 - m2)^2
      + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E11 + 2*E12 + E22) * (E00 + 2*E02 + E22) * (-m0 - m1)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E11 + 2*E12 + E22) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (-m0)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/4)) * (E11 + 2*E12 + E22) * (E22) * (-m1)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E11 + 2*E12 + E22) * (E11) * (m2)^2
      + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E11) * (E00) * (-m0 - m1 - 2*m2)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E11) * (E00 + 2*E02 + E22) * (-m0 - m1 - m2)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E11) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (-m0 - m2)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E11) * (E22) * (-m1 - m2)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E11) * (E11 + 2*E12 + E22) * (-m2)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E11) * (E00 + 2*E01 + E11) * (m0)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E11) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (m0 + m2)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E11) * (E00) * (m0 + m1)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E11) * (E00 + 2*E02 + E22) * (m0 + m1 + m2)^2
      + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E11) * (E22) * (2*m0 + m1 + m2)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E00 + 2*E01 + E11) * (E11) * (-m0)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + 2*E01 + E11) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (m2)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/4)) * (E00 + 2*E01 + E11) * (E00) * (m1)^2
      + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E00 + 2*E01 + E11) * (E00 + 2*E02 + E22) * (m1 + m2)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + 2*E01 + E11) * (E22) * (m0 + m1 + m2)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (E11) * (-m0 - m2)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (E00 + 2*E01 + E11) * (-m2)^2
      + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (E00) * (m1 - m2)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (E00 + 2*E02 + E22) * (m1)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (E22) * (m0 + m1)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E00) * (E11) * (-m0 - m1)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/4)) * (E00) * (E00 + 2*E01 + E11) * (-m1)^2
      + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E00) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (-m1 + m2)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/4)) * (E00) * (E00 + 2*E02 + E22) * (m2)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E00) * (E22) * (m0 + m2)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + 2*E02 + E22) * (E11) * (-m0 - m1 - m2)^2
      + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E00 + 2*E02 + E22) * (E00 + 2*E01 + E11) * (-m1 - m2)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + 2*E02 + E22) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (-m1)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/4)) * (E00 + 2*E02 + E22) * (E00) * (-m2)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E00 + 2*E02 + E22) * (E22) * (m0)^2
      + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E22) * (E11) * (-2*m0 - m1 - m2)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E22) * (E00 + 2*E01 + E11) * (-m0 - m1 - m2)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E22) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (-m0 - m1)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E22) * (E00) * (-m0 - m2)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E22) * (E00 + 2*E02 + E22) * (-m0)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E11) * (E11 + 2*E12 + E22) * (m2)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E11) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (m0 + m2)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E11) * (E22) * (m1 + m2)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E11) * (E00 + 2*E02 + E22) * (m0 + m1 + m2)^2
      + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E11) * (E00) * (m0 + m1 + 2*m2)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E11 + 2*E12 + E22) * (E11) * (-m2)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E11 + 2*E12 + E22) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (m0)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/4)) * (E11 + 2*E12 + E22) * (E22) * (m1)^2
      + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E11 + 2*E12 + E22) * (E00 + 2*E02 + E22) * (m0 + m1)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E11 + 2*E12 + E22) * (E00) * (m0 + m1 + m2)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (E11) * (-m0 - m2)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (E11 + 2*E12 + E22) * (-m0)^2
      + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (E22) * (-m0 + m1)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (E00 + 2*E02 + E22) * (m1)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (E00) * (m1 + m2)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E22) * (E11) * (-m1 - m2)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/4)) * (E22) * (E11 + 2*E12 + E22) * (-m1)^2
      + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E22) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (m0 - m1)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/4)) * (E22) * (E00 + 2*E02 + E22) * (m0)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E22) * (E00) * (m0 + m2)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + 2*E02 + E22) * (E11) * (-m0 - m1 - m2)^2
      + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E00 + 2*E02 + E22) * (E11 + 2*E12 + E22) * (-m0 - m1)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + 2*E02 + E22) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (-m1)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/4)) * (E00 + 2*E02 + E22) * (E22) * (-m0)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E00 + 2*E02 + E22) * (E00) * (m2)^2
      + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E00) * (E11) * (-m0 - m1 - 2*m2)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00) * (E11 + 2*E12 + E22) * (-m0 - m1 - m2)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E00) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (-m1 - m2)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E00) * (E22) * (-m0 - m2)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E00) * (E00 + 2*E02 + E22) * (-m2)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E22) * (E00 + 2*E02 + E22) * (m0)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E22) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (m0 + m1)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E22) * (E00) * (m0 + m2)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E22) * (E00 + 2*E01 + E11) * (m0 + m1 + m2)^2
      + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E22) * (E11) * (2*m0 + m1 + m2)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E00 + 2*E02 + E22) * (E22) * (-m0)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + 2*E02 + E22) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (m1)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/4)) * (E00 + 2*E02 + E22) * (E00) * (m2)^2
      + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E00 + 2*E02 + E22) * (E00 + 2*E01 + E11) * (m1 + m2)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + 2*E02 + E22) * (E11) * (m0 + m1 + m2)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (E22) * (-m0 - m1)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (E00 + 2*E02 + E22) * (-m1)^2
      + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (E00) * (-m1 + m2)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (E00 + 2*E01 + E11) * (m2)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (E11) * (m0 + m2)^2
      + ((1 : ℝ)/

-- … truncated for the page; open the module for the rest.
THEOREM certificate_block_pertet · IndisputableMonolith/Gravity/Analysis/ReggeTTCertificateScratch.lean
certificate_block_pertet · IndisputableMonolith/Gravity/Analysis/ReggeTTCertificateScratch.lean:43 · truncated 
/-- Pre-cancellation certificate block: 4*M as the literal per-tet sum with
s2, s3 opaque; the offline lift cofactors are 0, so `linear_combination`
with 0-coefficients (= `ring1` on the difference) closes it. -/
theorem certificate_block_pertet
    (E00 E01 E02 E11 E12 E22 m0 m1 m2 s2 s3 : ℝ)
    (hs2 : s2 ^ 2 = 2) (hs3 : s3 ^ 2 = 3) :
    (((1 : ℝ)/2) * ((0 : ℝ)) * (E00) * (E00 + 2*E01 + E11) * (m1)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E00) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (m1 + m2)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E00) * (E11) * (m0 + m1)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00) * (E11 + 2*E12 + E22) * (m0 + m1 + m2)^2
      + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E00) * (E22) * (m0 + 2*m1 + m2)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E00 + 2*E01 + E11) * (E00) * (-m1)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + 2*E01 + E11) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (m2)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/4)) * (E00 + 2*E01 + E11) * (E11) * (m0)^2
      + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E00 + 2*E01 + E11) * (E11 + 2*E12 + E22) * (m0 + m2)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + 2*E01 + E11) * (E22) * (m0 + m1 + m2)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (E00) * (-m1 - m2)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (E00 + 2*E01 + E11) * (-m2)^2
      + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (E11) * (m0 - m2)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (E11 + 2*E12 + E22) * (m0)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (E22) * (m0 + m1)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E11) * (E00) * (-m0 - m1)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/4)) * (E11) * (E00 + 2*E01 + E11) * (-m0)^2
      + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E11) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (-m0 + m2)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/4)) * (E11) * (E11 + 2*E12 + E22) * (m2)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E11) * (E22) * (m1 + m2)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E11 + 2*E12 + E22) * (E00) * (-m0 - m1 - m2)^2
      + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E11 + 2*E12 + E22) * (E00 + 2*E01 + E11) * (-m0 - m2)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E11 + 2*E12 + E22) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (-m0)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/4)) * (E11 + 2*E12 + E22) * (E11) * (-m2)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E11 + 2*E12 + E22) * (E22) * (m1)^2
      + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E22) * (E00) * (-m0 - 2*m1 - m2)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E22) * (E00 + 2*E01 + E11) * (-m0 - m1 - m2)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E22) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (-m0 - m1)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E22) * (E11) * (-m1 - m2)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E22) * (E11 + 2*E12 + E22) * (-m1)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E00) * (E00 + 2*E02 + E22) * (m2)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E00) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (m1 + m2)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E00) * (E22) * (m0 + m2)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00) * (E11 + 2*E12 + E22) * (m0 + m1 + m2)^2
      + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E00) * (E11) * (m0 + m1 + 2*m2)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E00 + 2*E02 + E22) * (E00) * (-m2)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + 2*E02 + E22) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (m1)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/4)) * (E00 + 2*E02 + E22) * (E22) * (m0)^2
      + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E00 + 2*E02 + E22) * (E11 + 2*E12 + E22) * (m0 + m1)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + 2*E02 + E22) * (E11) * (m0 + m1 + m2)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (E00) * (-m1 - m2)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (E00 + 2*E02 + E22) * (-m1)^2
      + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (E22) * (m0 - m1)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (E11 + 2*E12 + E22) * (m0)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (E11) * (m0 + m2)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E22) * (E00) * (-m0 - m2)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/4)) * (E22) * (E00 + 2*E02 + E22) * (-m0)^2
      + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E22) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (-m0 + m1)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/4)) * (E22) * (E11 + 2*E12 + E22) * (m1)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E22) * (E11) * (m1 + m2)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E11 + 2*E12 + E22) * (E00) * (-m0 - m1 - m2)^2
      + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E11 + 2*E12 + E22) * (E00 + 2*E02 + E22) * (-m0 - m1)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E11 + 2*E12 + E22) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (-m0)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/4)) * (E11 + 2*E12 + E22) * (E22) * (-m1)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E11 + 2*E12 + E22) * (E11) * (m2)^2
      + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E11) * (E00) * (-m0 - m1 - 2*m2)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E11) * (E00 + 2*E02 + E22) * (-m0 - m1 - m2)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E11) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (-m0 - m2)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E11) * (E22) * (-m1 - m2)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E11) * (E11 + 2*E12 + E22) * (-m2)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E11) * (E00 + 2*E01 + E11) * (m0)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E11) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (m0 + m2)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E11) * (E00) * (m0 + m1)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E11) * (E00 + 2*E02 + E22) * (m0 + m1 + m2)^2
      + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E11) * (E22) * (2*m0 + m1 + m2)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E00 + 2*E01 + E11) * (E11) * (-m0)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + 2*E01 + E11) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (m2)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/4)) * (E00 + 2*E01 + E11) * (E00) * (m1)^2
      + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E00 + 2*E01 + E11) * (E00 + 2*E02 + E22) * (m1 + m2)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + 2*E01 + E11) * (E22) * (m0 + m1 + m2)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (E11) * (-m0 - m2)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (E00 + 2*E01 + E11) * (-m2)^2
      + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (E00) * (m1 - m2)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (E00 + 2*E02 + E22) * (m1)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (E22) * (m0 + m1)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E00) * (E11) * (-m0 - m1)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/4)) * (E00) * (E00 + 2*E01 + E11) * (-m1)^2
      + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E00) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (-m1 + m2)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/4)) * (E00) * (E00 + 2*E02 + E22) * (m2)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E00) * (E22) * (m0 + m2)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + 2*E02 + E22) * (E11) * (-m0 - m1 - m2)^2
      + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E00 + 2*E02 + E22) * (E00 + 2*E01 + E11) * (-m1 - m2)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + 2*E02 + E22) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (-m1)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/4)) * (E00 + 2*E02 + E22) * (E00) * (-m2)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E00 + 2*E02 + E22) * (E22) * (m0)^2
      + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E22) * (E11) * (-2*m0 - m1 - m2)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E22) * (E00 + 2*E01 + E11) * (-m0 - m1 - m2)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E22) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (-m0 - m1)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E22) * (E00) * (-m0 - m2)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E22) * (E00 + 2*E02 + E22) * (-m0)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E11) * (E11 + 2*E12 + E22) * (m2)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E11) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (m0 + m2)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E11) * (E22) * (m1 + m2)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E11) * (E00 + 2*E02 + E22) * (m0 + m1 + m2)^2
      + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E11) * (E00) * (m0 + m1 + 2*m2)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E11 + 2*E12 + E22) * (E11) * (-m2)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E11 + 2*E12 + E22) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (m0)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/4)) * (E11 + 2*E12 + E22) * (E22) * (m1)^2
      + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E11 + 2*E12 + E22) * (E00 + 2*E02 + E22) * (m0 + m1)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E11 + 2*E12 + E22) * (E00) * (m0 + m1 + m2)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (E11) * (-m0 - m2)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (E11 + 2*E12 + E22) * (-m0)^2
      + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (E22) * (-m0 + m1)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (E00 + 2*E02 + E22) * (m1)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (E00) * (m1 + m2)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E22) * (E11) * (-m1 - m2)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/4)) * (E22) * (E11 + 2*E12 + E22) * (-m1)^2
      + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E22) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (m0 - m1)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/4)) * (E22) * (E00 + 2*E02 + E22) * (m0)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E22) * (E00) * (m0 + m2)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + 2*E02 + E22) * (E11) * (-m0 - m1 - m2)^2
      + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E00 + 2*E02 + E22) * (E11 + 2*E12 + E22) * (-m0 - m1)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + 2*E02 + E22) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (-m1)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/4)) * (E00 + 2*E02 + E22) * (E22) * (-m0)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E00 + 2*E02 + E22) * (E00) * (m2)^2
      + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E00) * (E11) * (-m0 - m1 - 2*m2)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00) * (E11 + 2*E12 + E22) * (-m0 - m1 - m2)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E00) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (-m1 - m2)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E00) * (E22) * (-m0 - m2)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E00) * (E00 + 2*E02 + E22) * (-m2)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E22) * (E00 + 2*E02 + E22) * (m0)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E22) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (m0 + m1)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E22) * (E00) * (m0 + m2)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E22) * (E00 + 2*E01 + E11) * (m0 + m1 + m2)^2
      + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E22) * (E11) * (2*m0 + m1 + m2)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E00 + 2*E02 + E22) * (E22) * (-m0)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + 2*E02 + E22) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (m1)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/4)) * (E00 + 2*E02 + E22) * (E00) * (m2)^2
      + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E00 + 2*E02 + E22) * (E00 + 2*E01 + E11) * (m1 + m2)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + 2*E02 + E22) * (E11) * (m0 + m1 + m2)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (E22) * (-m0 - m1)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (E00 + 2*E02 + E22) * (-m1)^2
      + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (E00) * (-m1 + m2)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (E00 + 2*E01 + E11) * (m2)^2
      + ((1 : ℝ)/2) * ((0 : ℝ)) * (E00 + 2*E01 + 2*E02 + E11 + 2*E12 + E22) * (E11) * (m0 + m2)^2
      + ((1 : ℝ)/

-- … truncated for the page; open the module for the rest.
THEOREM certificate_block_rational · IndisputableMonolith/Gravity/Analysis/ReggeTTCertificateScratch.lean
certificate_block_rational · IndisputableMonolith/Gravity/Analysis/ReggeTTCertificateScratch.lean:237 
/-- Post-cancellation rational identity (radicals already cancelled),
closed by plain `ring`. -/
theorem certificate_block_rational
    (E00 E01 E02 E11 E12 E22 m0 m1 m2 : ℝ) :
    E00^2*m0^2 + E00^2*m1^2 + E00^2*m2^2 + 2*E00*E11*m2^2 - 4*E00*E12*m1*m2 + 2*E00*E22*m1^2 + 2*E01^2*m0^2 + 2*E01^2*m1^2 + 4*E01*E02*m1*m2 + 4*E01*E12*m0*m2 - 4*E01*E22*m0*m1 + 2*E02^2*m0^2 + 2*E02^2*m2^2 - 4*E02*E11*m0*m2 + 4*E02*E12*m0*m1 + E11^2*m0^2 + E11^2*m1^2 + E11^2*m2^2 + 2*E11*E22*m0^2 + 2*E12^2*m1^2 + 2*E12^2*m2^2 + E22^2*m0^2 + E22^2*m1^2 + E22^2*m2^2
    =
    (-E00*m0^2 + E00*m1^2 + E00*m2^2 - 4*E01*m0*m1 - 2*E02*m0*m2 + E11*m0^2 - E11*m1^2 + E11*m2^2 - 2*E12*m1*m2 + E22*m0^2 + E22*m1^2 + E22*m2^2) * (E00 + E11 + E22)
      + (2*E00*m0 + 2*E01*m1 + 2*E02*m2) * (E00*m0 + E01*m1 + E02*m2)
      + (2*E01*m0 + 2*E11*m1 + 2*E12*m2) * (E01*m0 + E11*m1 + E12*m2)
      + (-2*E00*m2 + 2*E02*m0 - 2*E11*m2 + 2*E12*m1) * (E02*m0 + E12*m1 + E22*m2) := by
  ring

What this page does not claim

The theorem assigns no physical meaning to the quantities m0, m1, m2 or E00 through E22. The theorem does not assert anything about general relativity or Regge calculus. The declaration does not claim that the framework derives any physical law.

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/ReggeTTCertificateScratch.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