Encyclopedia Gravity Gravity Analysis Regge Ttcontinuum Certificate Spike Tet Block2 Eq

ARTICLE 4 claims 4 theorems

Gravity Analysis Regge Ttcontinuum Certificate Spike Tet Block2 Eq

A machine-checked theorem rewrites one piece of a gravity calculation into a simpler polynomial form, and nothing more.

Verify this page

A polynomial identity

In the framework's machine-checked library of formal theorems, tetBlock2_eq is a statement about a specific algebraic expression called tetBlock2. This expression is one of six building blocks in a larger calculation about gravitational waves. The theorem says that this block, which is defined as a sum of 36 terms, is equal to a particular polynomial in the variables E00, E01, ..., x0, x1, x2. The proof is a direct expansion: it unfolds the definition and applies the algebraic simplification rule called ring, which verifies that the two sides are identical for all real number inputs.

The larger context is a certificate for a continuum limit in a discrete model of gravity. The certificate aims to show that a sum over six such blocks, under certain symmetry and trace conditions, equals a simple expression: negative one quarter times the squared norm of the vector x times the squared Frobenius norm of the matrix E. Each block theorem, including tetBlock2_eq, is a lemma in this proof. The block theorems themselves do not impose any conditions; they are unconditional identities. The conditions, such as symmetry and tracelessness, appear in the final certificate theorem, not in the individual block lemmas.

What tetBlock2_eq does not claim is just as important. It does not state anything about the physical meaning of the variables, the validity of the continuum limit, or the behavior of gravitational waves. It is a purely algebraic fact about a defined expression. It does not assert that this block is zero, nor that any particular value is achieved. It only provides a rewritten form of the expression, which is useful for the subsequent proof. The theorem's strength is its certainty: it is checked by a computer kernel, so the identity holds for all real numbers, with no hidden assumptions.

THEOREM tetBlock2 · IndisputableMonolith/Gravity/Analysis/ReggeTTContinuumCertificateSpike.lean
tetBlock2 · IndisputableMonolith/Gravity/Analysis/ReggeTTContinuumCertificateSpike.lean:165 
/-- Tet 2: LITERAL transcription of the 36 (f,g) terms of
(1/2) * G_fg * c_(d(tau,f)) * c_(d(tau,g)) * (x.(m_g - m_f))^2. -/
noncomputable def tetBlock2 (E00 E01 E02 E10 E11 E12 E20 E21 E22 x0 x1 x2 s2 s3 p : ℝ) : ℝ :=
    (((1 : ℝ)/2) * (((-1 : ℝ)/16) * p) * (E11) * (E11) * (0 : ℝ)^2
      + ((1 : ℝ)/2) * (0 : ℝ) * (E11) * (E00 + E01 + E10 + E11) * (x0/2)^2
      + ((1 : ℝ)/2) * (0 : ℝ) * (E11) * (E00 + E01 + E02 + E10 + E11 + E12 + E20 + E21 + E22) * (x0/2 + x2/2)^2
      + ((1 : ℝ)/2) * (0 : ℝ) * (E11) * (E00) * (x0/2 + x1/2)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E11) * (E00 + E02 + E20 + E22) * (x0/2 + x1/2 + x2/2)^2
      + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E11) * (E22) * (x0 + x1/2 + x2/2)^2
      + ((1 : ℝ)/2) * (0 : ℝ) * (E00 + E01 + E10 + E11) * (E11) * (-x0/2)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/32) * s2 * p + ((1 : ℝ)/8)) * (E00 + E01 + E10 + E11) * (E00 + E01 + E10 + E11) * (0 : ℝ)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + E01 + E10 + E11) * (E00 + E01 + E02 + E10 + E11 + E12 + E20 + E21 + E22) * (x2/2)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/4)) * (E00 + E01 + E10 + E11) * (E00) * (x1/2)^2
      + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E00 + E01 + E10 + E11) * (E00 + E02 + E20 + E22) * (x1/2 + x2/2)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + E01 + E10 + E11) * (E22) * (x0/2 + x1/2 + x2/2)^2
      + ((1 : ℝ)/2) * (0 : ℝ) * (E00 + E01 + E02 + E10 + E11 + E12 + E20 + E21 + E22) * (E11) * (-x0/2 - x2/2)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + E01 + E02 + E10 + E11 + E12 + E20 + E21 + E22) * (E00 + E01 + E10 + E11) * (-x2/2)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/108) * s3 * p + ((1 : ℝ)/12)) * (E00 + E01 + E02 + E10 + E11 + E12 + E20 + E21 + E22) * (E00 + E01 + E02 + E10 + E11 + E12 + E20 + E21 + E22) * (0 : ℝ)^2
      + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E00 + E01 + E02 + E10 + E11 + E12 + E20 + E21 + E22) * (E00) * (x1/2 - x2/2)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + E01 + E02 + E10 + E11 + E12 + E20 + E21 + E22) * (E00 + E02 + E20 + E22) * (x1/2)^2
      + ((1 : ℝ)/2) * (0 : ℝ) * (E00 + E01 + E02 + E10 + E11 + E12 + E20 + E21 + E22) * (E22) * (x0/2 + x1/2)^2
      + ((1 : ℝ)/2) * (0 : ℝ) * (E00) * (E11) * (-x0/2 - x1/2)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/4)) * (E00) * (E00 + E01 + E10 + E11) * (-x1/2)^2
      + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E00) * (E00 + E01 + E02 + E10 + E11 + E12 + E20 + E21 + E22) * (-x1/2 + x2/2)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/8) * p + ((1 : ℝ)/4)) * (E00) * (E00) * (0 : ℝ)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/4)) * (E00) * (E00 + E02 + E20 + E22) * (x2/2)^2
      + ((1 : ℝ)/2) * (0 : ℝ) * (E00) * (E22) * (x0/2 + x2/2)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + E02 + E20 + E22) * (E11) * (-x0/2 - x1/2 - x2/2)^2
      + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E00 + E02 + E20 + E22) * (E00 + E01 + E10 + E11) * (-x1/2 - x2/2)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E00 + E02 + E20 + E22) * (E00 + E01 + E02 + E10 + E11 + E12 + E20 + E21 + E22) * (-x1/2)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/4)) * (E00 + E02 + E20 + E22) * (E00) * (-x2/2)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/32) * s2 * p + ((1 : ℝ)/8)) * (E00 + E02 + E20 + E22) * (E00 + E02 + E20 + E22) * (0 : ℝ)^2
      + ((1 : ℝ)/2) * (0 : ℝ) * (E00 + E02 + E20 + E22) * (E22) * (x0/2)^2
      + ((1 : ℝ)/2) * (((1 : ℝ)/4)) * (E22) * (E11) * (-x0 - x1/2 - x2/2)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/8)) * (E22) * (E00 + E01 + E10 + E11) * (-x0/2 - x1/2 - x2/2)^2
      + ((1 : ℝ)/2) * (0 : ℝ) * (E22) * (E00 + E01 + E02 + E10 + E11 + E12 + E20 + E21 + E22) * (-x0/2 - x1/2)^2
      + ((1 : ℝ)/2) * (0 : ℝ) * (E22) * (E00) * (-x0/2 - x2/2)^2
      + ((1 : ℝ)/2) * (0 : ℝ) * (E22) * (E00 + E02 + E20 + E22) * (-x0/2)^2
      + ((1 : ℝ)/2) * (((-1 : ℝ)/16) * p) * (E22) * (E22) * (0 : ℝ)^2)
THEOREM tetBlock2_eq · IndisputableMonolith/Gravity/Analysis/ReggeTTContinuumCertificateSpike.lean
tetBlock2_eq · IndisputableMonolith/Gravity/Analysis/ReggeTTContinuumCertificateSpike.lean:205 
/-- Tet 2 collapses to a pure-QQ polynomial (every s2/s3/p entry of G
carries a literal (0)^2 midpoint factor). -/
theorem tetBlock2_eq (E00 E01 E02 E10 E11 E12 E20 E21 E22 x0 x1 x2 s2 s3 p : ℝ) :
    tetBlock2 E00 E01 E02 E10 E11 E12 E20 E21 E22 x0 x1 x2 s2 s3 p
    =
    (E00^2*x1^2/32 + E00^2*x2^2/32 + E00*E01*x1^2/32 + E00*E01*x2^2/16 + E00*E02*x1^2/16 + E00*E02*x2^2/32 + E00*E10*x1^2/32 + E00*E10*x2^2/16 - E00*E11*x0^2/32 - E00*E11*x0*x1/16 - E00*E11*x0*x2/16 - E00*E11*x1*x2/16 + E00*E11*x2^2/32 + E00*E12*x1^2/32 - E00*E12*x1*x2/8 + E00*E12*x2^2/32 + E00*E20*x1^2/16 + E00*E20*x2^2/32 + E00*E21*x1^2/32 - E00*E21*x1*x2/8 + E00*E21*x2^2/32 - E00*E22*x0^2/32 - E00*E22*x0*x1/16 - E00*E22*x0*x2/16 + E00*E22*x1^2/32 - E00*E22*x1*x2/16 - E01^2*x2^2/32 + E01*E02*x1^2/32 + E01*E02*x1*x2/8 + E01*E02*x2^2/32 - E01*E10*x2^2/16 - E01*E11*x2^2/16 - E01*E12*x2^2/32 + E01*E20*x1^2/32 + E01*E20*x1*x2/8 + E01*E20*x2^2/32 - E01*E21*x2^2/32 - E01*E22*x0^2/32 - E01*E22*x0*x1/16 - E01*E22*x0*x2/16 + E01*E22*x1*x2/16 - E02^2*x1^2/32 + E02*E10*x1^2/32 + E02*E10*x1*x2/8 + E02*E10*x2^2/32 - E02*E11*x0^2/32 - E02*E11*x0*x1/16 - E02*E11*x0*x2/16 + E02*E11*x1*x2/16 - E02*E12*x1^2/32 - E02*E20*x1^2/16 - E02*E21*x1^2/32 - E02*E22*x1^2/16 - E10^2*x2^2/32 - E10*E11*x2^2/16 - E10*E12*x2^2/32 + E10*E20*x1^2/32 + E10*E20*x1*x2/8 + E10*E20*x2^2/32 - E10*E21*x2^2/32 - E10*E22*x0^2/32 - E10*E22*x0*x1/16 - E10*E22*x0*x2/16 + E10*E22*x1*x2/16 - E11^2*x2^2/32 - E11*E12*x2^2/32 - E11*E20*x0^2/32 - E11*E20*x0*x1/16 - E11*E20*x0*x2/16 + E11*E20*x1*x2/16 - E11*E21*x2^2/32 + 3*E11*E22*x0^2/16 + E11*E22*x0*x1/8 + E11*E22*x0*x2/8 + E11*E22*x1^2/32 + E11*E22*x1*x2/8 + E11*E22*x2^2/32 - E12*E20*x1^2/32 - E12*E22*x1^2/32 - E20^2*x1^2/32 - E20*E21*x1^2/32 - E20*E22*x1^2/16 - E21*E22*x1^2/32 - E22^2*x1^2/32) := by
  unfold tetBlock2
  ring

set_option maxHeartbeats 1600000 in
THEOREM tetBlock2_eq · IndisputableMonolith/Gravity/Analysis/ReggeTTContinuumCertificateSpike.lean
tetBlock2_eq · IndisputableMonolith/Gravity/Analysis/ReggeTTContinuumCertificateSpike.lean:205 
/-- Tet 2 collapses to a pure-QQ polynomial (every s2/s3/p entry of G
carries a literal (0)^2 midpoint factor). -/
theorem tetBlock2_eq (E00 E01 E02 E10 E11 E12 E20 E21 E22 x0 x1 x2 s2 s3 p : ℝ) :
    tetBlock2 E00 E01 E02 E10 E11 E12 E20 E21 E22 x0 x1 x2 s2 s3 p
    =
    (E00^2*x1^2/32 + E00^2*x2^2/32 + E00*E01*x1^2/32 + E00*E01*x2^2/16 + E00*E02*x1^2/16 + E00*E02*x2^2/32 + E00*E10*x1^2/32 + E00*E10*x2^2/16 - E00*E11*x0^2/32 - E00*E11*x0*x1/16 - E00*E11*x0*x2/16 - E00*E11*x1*x2/16 + E00*E11*x2^2/32 + E00*E12*x1^2/32 - E00*E12*x1*x2/8 + E00*E12*x2^2/32 + E00*E20*x1^2/16 + E00*E20*x2^2/32 + E00*E21*x1^2/32 - E00*E21*x1*x2/8 + E00*E21*x2^2/32 - E00*E22*x0^2/32 - E00*E22*x0*x1/16 - E00*E22*x0*x2/16 + E00*E22*x1^2/32 - E00*E22*x1*x2/16 - E01^2*x2^2/32 + E01*E02*x1^2/32 + E01*E02*x1*x2/8 + E01*E02*x2^2/32 - E01*E10*x2^2/16 - E01*E11*x2^2/16 - E01*E12*x2^2/32 + E01*E20*x1^2/32 + E01*E20*x1*x2/8 + E01*E20*x2^2/32 - E01*E21*x2^2/32 - E01*E22*x0^2/32 - E01*E22*x0*x1/16 - E01*E22*x0*x2/16 + E01*E22*x1*x2/16 - E02^2*x1^2/32 + E02*E10*x1^2/32 + E02*E10*x1*x2/8 + E02*E10*x2^2/32 - E02*E11*x0^2/32 - E02*E11*x0*x1/16 - E02*E11*x0*x2/16 + E02*E11*x1*x2/16 - E02*E12*x1^2/32 - E02*E20*x1^2/16 - E02*E21*x1^2/32 - E02*E22*x1^2/16 - E10^2*x2^2/32 - E10*E11*x2^2/16 - E10*E12*x2^2/32 + E10*E20*x1^2/32 + E10*E20*x1*x2/8 + E10*E20*x2^2/32 - E10*E21*x2^2/32 - E10*E22*x0^2/32 - E10*E22*x0*x1/16 - E10*E22*x0*x2/16 + E10*E22*x1*x2/16 - E11^2*x2^2/32 - E11*E12*x2^2/32 - E11*E20*x0^2/32 - E11*E20*x0*x1/16 - E11*E20*x0*x2/16 + E11*E20*x1*x2/16 - E11*E21*x2^2/32 + 3*E11*E22*x0^2/16 + E11*E22*x0*x1/8 + E11*E22*x0*x2/8 + E11*E22*x1^2/32 + E11*E22*x1*x2/8 + E11*E22*x2^2/32 - E12*E20*x1^2/32 - E12*E22*x1^2/32 - E20^2*x1^2/32 - E20*E21*x1^2/32 - E20*E22*x1^2/16 - E21*E22*x1^2/32 - E22^2*x1^2/32) := by
  unfold tetBlock2
  ring

set_option maxHeartbeats 1600000 in
THEOREM tetBlock2_eq · IndisputableMonolith/Gravity/Analysis/ReggeTTContinuumCertificateSpike.lean
tetBlock2_eq · IndisputableMonolith/Gravity/Analysis/ReggeTTContinuumCertificateSpike.lean:205 
/-- Tet 2 collapses to a pure-QQ polynomial (every s2/s3/p entry of G
carries a literal (0)^2 midpoint factor). -/
theorem tetBlock2_eq (E00 E01 E02 E10 E11 E12 E20 E21 E22 x0 x1 x2 s2 s3 p : ℝ) :
    tetBlock2 E00 E01 E02 E10 E11 E12 E20 E21 E22 x0 x1 x2 s2 s3 p
    =
    (E00^2*x1^2/32 + E00^2*x2^2/32 + E00*E01*x1^2/32 + E00*E01*x2^2/16 + E00*E02*x1^2/16 + E00*E02*x2^2/32 + E00*E10*x1^2/32 + E00*E10*x2^2/16 - E00*E11*x0^2/32 - E00*E11*x0*x1/16 - E00*E11*x0*x2/16 - E00*E11*x1*x2/16 + E00*E11*x2^2/32 + E00*E12*x1^2/32 - E00*E12*x1*x2/8 + E00*E12*x2^2/32 + E00*E20*x1^2/16 + E00*E20*x2^2/32 + E00*E21*x1^2/32 - E00*E21*x1*x2/8 + E00*E21*x2^2/32 - E00*E22*x0^2/32 - E00*E22*x0*x1/16 - E00*E22*x0*x2/16 + E00*E22*x1^2/32 - E00*E22*x1*x2/16 - E01^2*x2^2/32 + E01*E02*x1^2/32 + E01*E02*x1*x2/8 + E01*E02*x2^2/32 - E01*E10*x2^2/16 - E01*E11*x2^2/16 - E01*E12*x2^2/32 + E01*E20*x1^2/32 + E01*E20*x1*x2/8 + E01*E20*x2^2/32 - E01*E21*x2^2/32 - E01*E22*x0^2/32 - E01*E22*x0*x1/16 - E01*E22*x0*x2/16 + E01*E22*x1*x2/16 - E02^2*x1^2/32 + E02*E10*x1^2/32 + E02*E10*x1*x2/8 + E02*E10*x2^2/32 - E02*E11*x0^2/32 - E02*E11*x0*x1/16 - E02*E11*x0*x2/16 + E02*E11*x1*x2/16 - E02*E12*x1^2/32 - E02*E20*x1^2/16 - E02*E21*x1^2/32 - E02*E22*x1^2/16 - E10^2*x2^2/32 - E10*E11*x2^2/16 - E10*E12*x2^2/32 + E10*E20*x1^2/32 + E10*E20*x1*x2/8 + E10*E20*x2^2/32 - E10*E21*x2^2/32 - E10*E22*x0^2/32 - E10*E22*x0*x1/16 - E10*E22*x0*x2/16 + E10*E22*x1*x2/16 - E11^2*x2^2/32 - E11*E12*x2^2/32 - E11*E20*x0^2/32 - E11*E20*x0*x1/16 - E11*E20*x0*x2/16 + E11*E20*x1*x2/16 - E11*E21*x2^2/32 + 3*E11*E22*x0^2/16 + E11*E22*x0*x1/8 + E11*E22*x0*x2/8 + E11*E22*x1^2/32 + E11*E22*x1*x2/8 + E11*E22*x2^2/32 - E12*E20*x1^2/32 - E12*E22*x1^2/32 - E20^2*x1^2/32 - E20*E21*x1^2/32 - E20*E22*x1^2/16 - E21*E22*x1^2/32 - E22^2*x1^2/32) := by
  unfold tetBlock2
  ring

set_option maxHeartbeats 1600000 in

What this page does not claim

tetBlock2_eq does not assert that the block equals zero or any specific value. tetBlock2_eq does not establish any physical property of gravitational waves. tetBlock2_eq does not impose the symmetry or trace conditions; those belong to the final certificate 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/ReggeTTContinuumCertificateSpike.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