Encyclopedia Gravity Gravity Analysis Regge Ttcontinuum Certificate Spike Tet Block3 Eq

ARTICLE 3 claims 3 theorems

Gravity Analysis Regge Ttcontinuum Certificate Spike Tet Block3 Eq

A single algebraic identity, verified by a machine, is one of six pieces that together show how a certain sum over triangles collapses into a simple expression.

Verify this page

A block in a larger proof

In the study of gravity, one sometimes writes down a sum over the triangles of a discretized space, a kind of discrete analogue of an integral. The declaration tetBlock3_eq is a machine-checked theorem stating that one such block of that sum, called tetBlock3, equals a specific polynomial in its variables. The variables are real numbers representing components of a matrix and a vector; the theorem says that the block, which is defined as a literal transcription of a sum over 36 terms, can be rewritten as that polynomial. The proof is a direct expansion and simplification, which the machine checks step by step.

This identity is not a claim about physics by itself. It is a piece of algebra. Its role is to help establish a larger result, the TT continuum certificate, which says that the entire 216-term sum over six such blocks collapses to a simple expression, namely minus one quarter times the squared length of the vector times the squared Frobenius norm of the matrix, provided certain conditions hold. Those conditions are that the matrix is symmetric, has zero trace, and is orthogonal to the vector in a specific sense. The certificate is a theorem in the framework's machine-checked library of formal theorems.

What tetBlock3_eq does not claim is just as important. It does not say that the sum over triangles represents any physical quantity, nor that the conditions of the certificate hold for any particular physical situation. It does not assert that the block is zero, or that it has any particular sign. It only states the equality between the block and the polynomial, given the definitions. The physical interpretation, if any, belongs to the larger certificate and to the framework's broader account of gravity, not to this single algebraic step.

In the framework's account, this identity is a building block. The machine checks it, and the machine checks the certificate that uses it. The reader who wants to see the whole picture should look at the certificate, not at this block alone. The block is a lemma, a tool, and the certificate is the result that gives it meaning.

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

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

set_option maxHeartbeats 1600000 in
THEOREM tt_continuum_certificate · IndisputableMonolith/Gravity/Analysis/ReggeTTContinuumCertificateSpike.lean
tt_continuum_certificate · IndisputableMonolith/Gravity/Analysis/ReggeTTContinuumCertificateSpike.lean:365 
/-- TT continuum certificate: the literal 216-term per-tet sum (s2, s3, p
COMPLETELY FREE, standing for sqrt 2, sqrt 3, pi) equals
-(1/4) * |x|^2 * ||E||_F^2 on the TT constraints.  Proof: collapse each
per-tet block by `tetBlock*_eq` (kernel re-verifies the s2/s3/p
cancellation), then discharge the pure-QQ identity with the explicit offline
cofactor certificate via `linear_combination`. -/
theorem tt_continuum_certificate (E00 E01 E02 E10 E11 E12 E20 E21 E22 x0 x1 x2 s2 s3 p : ℝ)
    (hsym01 : E01 = E10) (hsym02 : E02 = E20) (hsym12 : E12 = E21)
    (htr : E00 + E11 + E22 = 0)
    (htrans0 : x0 * E00 + x1 * E10 + x2 * E20 = 0)
    (htrans1 : x0 * E01 + x1 * E11 + x2 * E21 = 0)
    (htrans2 : x0 * E02 + x1 * E12 + x2 * E22 = 0) :
    ((tetBlock0 E00 E01 E02 E10 E11 E12 E20 E21 E22 x0 x1 x2 s2 s3 p)
      + (tetBlock1 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)
      + (tetBlock3 E00 E01 E02 E10 E11 E12 E20 E21 E22 x0 x1 x2 s2 s3 p)
      + (tetBlock4 E00 E01 E02 E10 E11 E12 E20 E21 E22 x0 x1 x2 s2 s3 p)
      + (tetBlock5 E00 E01 E02 E10 E11 E12 E20 E21 E22 x0 x1 x2 s2 s3 p))
    =
    -((1 : ℝ)/4) * (x0^2 + x1^2 + x2^2) * (E00^2 + E01^2 + E02^2 + E10^2 + E11^2 + E12^2 + E20^2 + E21^2 + E22^2) := by
  rw [tetBlock0_eq, tetBlock1_eq, tetBlock2_eq, tetBlock3_eq,
      tetBlock4_eq, tetBlock5_eq]
  linear_combination
      (E00*x0*x1/2 - E01*x0^2/4 + E01*x1^2/4 + E01*x2^2/8 + E02*x1*x2/4 - E10*x0^2/4 - E10*x1^2/4 - E10*x2^2/8 - E12*x0*x2/4 - E20*x1*x2/4 - E21*x0*x2/4 + E22*x0*x1/2) * hsym01
      + (E00*x0*x2/2 - E02*x0^2/4 + E02*x1^2/8 + E02*x2^2/4 + E11*x0*x2/2 - E12*x0*x1/4 - E20*x0^2/4 - E20*x1^2/8 - E20*x2^2/4 - E21*x0*x1/4) * hsym02
      + (E00*x1*x2/2 - E02*x0*x1/2 + E11*x1*x2/2 + E12*x0^2/8 - E12*x1^2/4 + E12*x2^2/4 - E21*x0^2/8 - E21*x1^2/4 - E21*x2^2/4) * hsym12
      + (-E00*x0^2/4 + E00*x1^2/4 + E00*x2^2/4 - E01*x0*x1 - E02*x0*x2/2 + E11*x0^2/4 - E11*x1^2/4 + E11*x2^2/4 - E12*x1*x2/2 + E22*x0^2/4 + E22*x1^2/4 + E22*x2^2/4) * htr
      + (E00*x0/2 + E01*x1/2 + E02*x2/2) * htrans0
      + (E01*x0/2 + E11*x1/2 + E12*x2/2) * htrans1
      + (-E00*x2/2 + E02*x0/2 - E11*x2/2 + E12*x1/2) * htrans2

What this page does not claim

tetBlock3_eq does not assert that the block is zero or has any particular sign. tetBlock3_eq does not claim that the sum over triangles represents any physical quantity. The conditions of the TT continuum certificate are not claimed to hold for any particular physical situation.

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