Gravity Analysis Regge Ttgate Bbridge Core Core Block2 Eq

The block identity

In the Recognition Science framework's machine-checked library of formal theorems, coreBlock2_eq is a small but exact identity. It states that a sum over 36 raw moment terms, each built from a coefficient table and a displacement table, equals a single compact expression called tetBlock2. The equality holds for any real values of the three free parameters s2, s3, and p, and identically for any choice of the matrix E and vector x that feed the terms.

This is one of six such block identities, coreBlock0_eq through coreBlock5_eq, which together form the core identity coreTripleSum_eq_spikeSum. That larger theorem says the full 216-term raw moment sum equals the sum of the six spike blocks, with the same freedom in the parameters. The spike blocks enter only as data; the theorem does not invoke the spike's own continuum certificate. The proof is a direct computation using the ring tactic after expanding definitions, with no axioms beyond the standard trio and no sorry or admit.

What coreBlock2_eq does not claim is broader than what it does. It does not assert that the raw moment sum has any physical meaning on its own, nor that the block decomposition is unique. It does not say the spike convention is correct or that the TT gate conclusion follows. It only certifies an algebraic equality between two expressions, leaving interpretation and further derivation to other theorems in the library.

private theorem coreBlock2_eq (E : Fin 3 → Fin 3 → ℝ) (x : Fin 3 → ℝ)
    (s2 s3 p : ℝ) :
    (∑ f : Fin 6, ∑ g : Fin 6, coreTripleTerm E x (2, f, g)) =
      tetBlock2 (E 0 0) (E 0 1) (E 0 2) (E 1 0) (E 1 1) (E 1 2)
        (E 2 0) (E 2 1) (E 2 2) (x 0) (x 1) (x 2) s2 s3 p := by
  rw [tetBlock2_eq]
  simp only [Fin.sum_univ_six, coreTripleTerm, coreWeight,
    corePolEdgeCoeff, slotDispCore, slotMidTwice, Fin.sum_univ_three]
  push_cast
  ring

private theorem coreBlock2_eq (E : Fin 3 → Fin 3 → ℝ) (x : Fin 3 → ℝ)
    (s2 s3 p : ℝ) :
    (∑ f : Fin 6, ∑ g : Fin 6, coreTripleTerm E x (2, f, g)) =
      tetBlock2 (E 0 0) (E 0 1) (E 0 2) (E 1 0) (E 1 1) (E 1 2)
        (E 2 0) (E 2 1) (E 2 2) (x 0) (x 1) (x 2) s2 s3 p := by
  rw [tetBlock2_eq]
  simp only [Fin.sum_univ_six, coreTripleTerm, coreWeight,
    corePolEdgeCoeff, slotDispCore, slotMidTwice, Fin.sum_univ_three]
  push_cast
  ring

private theorem coreBlock2_eq (E : Fin 3 → Fin 3 → ℝ) (x : Fin 3 → ℝ)
    (s2 s3 p : ℝ) :
    (∑ f : Fin 6, ∑ g : Fin 6, coreTripleTerm E x (2, f, g)) =
      tetBlock2 (E 0 0) (E 0 1) (E 0 2) (E 1 0) (E 1 1) (E 1 2)
        (E 2 0) (E 2 1) (E 2 2) (x 0) (x 1) (x 2) s2 s3 p := by
  rw [tetBlock2_eq]
  simp only [Fin.sum_univ_six, coreTripleTerm, coreWeight,
    corePolEdgeCoeff, slotDispCore, slotMidTwice, Fin.sum_univ_three]
  push_cast
  ring

What this page does not claim

The raw moment sum has physical meaning on its own. The block decomposition is unique. The spike convention is correct or the TT gate conclusion follows.

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/ReggeTTGateBBridgeCore.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: