Encyclopedia Gravity Gravity Analysis Regge Ttcertificate Scratch

ARTICLE 2 claims 2 theorems

Gravity Analysis Regge Ttcertificate Scratch

A machine-checked proof that a complicated gravity sum can be reorganized into a simpler form, with no approximation.

Verify this page

The certificate block

In the framework's study of gravity, the ledger (a discrete record of events) gives rise to sums over small units called tetrahedra. The module named ReggeTTCertificateScratch contains a proof about one such sum. The sum involves two sets of numbers: E values that describe the geometry of a tetrahedron, and m values that describe something like masses or momenta at its corners. The proof shows that a large, sprawling expression built from these values can be rewritten as a much shorter and more structured expression. The long form has over a hundred terms; the short form has four main pieces.

The proof works in two stages, and the name of the module hints at why. The first stage, called the pre-cancellation certificate block, keeps two square roots (of 2 and 3) as opaque symbols. It shows that a particular sum, with those roots left unevaluated, is exactly equal to the target expression. The second stage, the post-cancellation rational identity, removes those roots entirely. After the radicals cancel, the remaining identity is a purely rational statement, and the proof closes it with a routine algebraic check. Each stage is a theorem in the framework's machine-checked library of formal theorems, meaning a computer verified every step.

What does this establish in plain language? It is a certificate, a formal guarantee, that the messy per-tetrahedron sum can be compressed into the clean form without losing anything. The proof does not approximate, and it does not assume the square roots cancel; it demonstrates the cancellation. This matters because the clean form is what later steps in the framework's gravity analysis can use. A reader who wants to see the structure of the sum, or to build further results on it, can rely on this certificate as a verified foundation.

The module is a scratch module, which in this context means it is a working area where a proof is developed and checked before being integrated into the main library. The certificate block is the core result, and it is complete: both theorems are proved with no gaps. The practical consequence is that the framework has a verified algebraic identity at its disposal, ready for the next stage of the gravity analysis.

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

This module does not prove any physical law or derive a gravitational equation. The certificate does not explain why the sum has this form or what it means physically. The scratch status does not imply the proof is incomplete; both theorems are fully proved.

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