coreBlock4_eq
plain-language theorem explainer
For fixed tet index 4, the double sum of signed raw moment terms over the 6×6 slot pairs equals the committed spike block tetBlock4, identically in the edge matrix E, displacement x, and free scalars s2,s3,p. Gate C-B bridge authors cite it when assembling the 216-term raw sum into six spike blocks. Proof: rewrite by the pure-QQ collapse of tetBlock4, unfold the literal tables, then ring.
Claim. For every real $3\times 3$ matrix $E$, every $x\in\mathbb{R}^3$, and every free scalars $s_2,s_3,p\in\mathbb{R}$, $$\sum_{f=0}^{5}\sum_{g=0}^{5} T_4(E,x;f,g)=B_4(E,x;s_2,s_3,p),$$ where $T_4$ is the signed raw moment term at tet index $4$ (weight $\times$ edge-class forms $\times$ squared midpoint phase) and $B_4$ is the literal 36-term spike transcription of tet block 4.
background
This file is the leaf algebra support for Gate C-B of the Lane C finishing charter. It isolates the heavy polynomial identity that bridges the raw 216-term moment sum to the six committed spike blocks, importing only the spike transcription so a full 216-term ring stays under the build memory guard.
All data here are literal tables: coreWeight is the rational raw-coefficient stencil (36 values); slotDispCore and slotMidTwice encode slot displacement class and doubled midpoint phase; corePolEdgeCoeff gives the seven edge-class linear forms $c_d=\sum_{ij}E_{ij}D_d^i D_d^j$. One coreTripleTerm is the signed raw moment $-(\mathrm{phase}^2)/2\cdot(-(w_{fg}c_f c_g))$.
Upstream, tetBlock4 is the literal transcription of the 36 $(f,g)$ terms of $\tfrac12 G_{fg}c_{d(\tau,f)}c_{d(\tau,g)}(x\cdot(m_g-m_f))^2$ at tet 4. Its companion tetBlock4_eq states that tet 4 collapses to a pure-QQ polynomial: every $s_2/s_3/p$ entry of $G$ carries a literal $(0)^2$ midpoint factor.
proof idea
Term-mode, four steps. First rewrite the right-hand side by tetBlock4_eq, replacing the spike transcription by its pure-QQ expanded polynomial (no free $s_2,s_3,p$ dependence survives). Then simp only expands the left-hand double sum over Fin 6, unfolds coreTripleTerm, coreWeight, corePolEdgeCoeff, slotDispCore, slotMidTwice, and the inner Fin 3 sums that build the edge-class forms and midpoint phases. push_cast clears integer-to-real coercions. A final ring identifies the two multivariate polynomials in the nine $E_{ij}$ and three $x_i$.
why it matters
One of six parallel block identities (coreBlock0_eq through coreBlock5_eq) that feed the parent theorem coreTripleSum_eq_spikeSum: the 216-term raw moment sum equals tetBlock0+...+tetBlock5 for completely free $s_2,s_3,p$, identically in $E$ and $x$. That core identity is the algebraic heart of the Gate C-B bridge; only block data is used, never the spike's TT continuum certificate.
In the broader gravity analysis this closes the raw-to-spike transcription gap on the Regge TT side without trusting hand-copied coefficients: the main module kernel-identifies the literal tables with the geometric rawJacobianCoefficient, periodic slot geometry, and polEdgeCoeff. No new axioms; standard trio footprint. It does not itself touch the forcing chain (T0–T8) or the mass ladder; it is pure continuum-certificate algebra inside Lane C.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.