coreBlock2_eq
plain-language theorem explainer
The double sum of signed raw moment terms at tetrahedron index 2 equals the committed spike block tetBlock2, identically in the edge matrix E, displacement x, and free scalars s2,s3,p. Gravity analysts bridging the 216-term Regge TT moment sum to the six spike blocks cite this leaf identity. The proof rewrites the spike block to its pure quadratic polynomial, expands the literal weight/coeff/midpoint tables, and closes by ring.
Claim. For any real $3\times 3$ matrix $E$, any $x\in\mathbb{R}^3$, and any free scalars $s_2,s_3,p\in\mathbb{R}$, the sum $\sum_{f=0}^{5}\sum_{g=0}^{5}$ of the signed raw moment term at tetrahedron slot $2$ with edge-pair indices $(f,g)$ equals the literal tet-2 spike block polynomial in the nine entries of $E$, the three components of $x$, and $s_2,s_3,p$.
background
This leaf module isolates the heavy polynomial algebra of the Gate C-B spike-convention bridge so that a 216-term ring normalization does not blow the laptop memory guard. Everything is defined over literal tables and free scalars: the rational raw-coefficient table (coreWeight), the slot displacement-class table, the doubled-midpoint table, and seven edge-class linear forms $c_d=\sum_{ij}E_{ij}D_d^i D_d^j$.
One signed raw moment term is $-({\rm phase})^2/2\cdot(-(w_{fg},c_f,c_g))$. The six committed spike blocks (tetBlock0 through tetBlock5) are pure data transcriptions of the 36 $(f,g)$ contributions per tetrahedron of $\tfrac12 G_{fg},c_{d(\tau,f)},c_{d(\tau,g)},(x\cdot(m_g-m_f))^2$. Upstream, tetBlock2_eq collapses tet 2 to a pure quadratic polynomial in the $E_{ij}$ and $x_k$, because every $s_2/s_3/p$ entry of $G$ carries a literal zero midpoint factor.
The local goal is the core identity: the full 216-term raw moment sum equals the sum of the six spike blocks, identically in $E$ and $x$, with $s_2,s_3,p$ completely free. This declaration is the tet-2 slice of that partition.
proof idea
Term-mode tactic script, not a wrapper. First rewrite the right-hand side via tetBlock2_eq, replacing the literal spike transcription by its expanded pure-QQ polynomial (no residual $s_2,s_3,p$ dependence). Then simp-expand the left-hand double sum over Fin 6: unfold the signed moment term, the weight table, the seven edge-class linear forms, the slot displacement table, and the doubled-midpoint table, and evaluate the Fin-3 sums inside. push_cast clears integer-to-real coercions. ring finishes the polynomial identity.
why it matters
Feeds directly into coreTripleSum_eq_spikeSum, the core identity of the Gate C-B bridge: the 216-term raw moment sum equals tetBlock0+...+tetBlock5 for free $s_2,s_3,p$, identically in $E$ and $x$. Only block data is used; the spike continuum certificate itself is never invoked.
That identity is the algebraic heart of ReggeTTGateBBridge (Lane C finishing charter, Gate C-B). Sibling lemmas coreBlock0_eq through coreBlock5_eq partition the triple sum by tetrahedron index; this is the index-2 cell. Closing the bridge lets the continuum TT certificate speak about the actual raw Jacobian stencil without trusting any hand transcription of weights or midpoints (those are kernel-identified in the main module against Gate C-A2f and the periodic geometry).
In the broader RS gravity stack this is pure discrete-to-continuum bookkeeping on the eight-tick / D=3 lattice side, not a new physical law. It removes a scaffolding risk: if any tet block failed to match its 36-term slice, the Gate C-B claim would not assemble.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.