coreBlock1_eq
plain-language theorem explainer
The double sum of signed raw moment terms over the six-by-six face pairs at fixed tet index 1 equals the committed spike block tetBlock1, identically in the edge matrix E, the displacement vector x, and free scalars s2, s3, p. Lane-C / Gate C-B algebra cites this as one of six block identities. The proof rewrites the spike block to its pure quadratic polynomial, expands the literal weight and midpoint tables, and finishes 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}$, $$\sum_{f=0}^{5}\sum_{g=0}^{5} T_1(E,x;f,g)=B_1(E,x;s_2,s_3,p),$$ where $T_1$ is the signed raw moment term at tet slot $1$ built from the literal weight table, edge-class linear forms, and doubled midpoints, and $B_1$ is the committed tet-1 spike block (the 36-term transcription of $\tfrac12 G_{fg}\,c_{d(\tau,f)}\,c_{d(\tau,g)}\,(x\cdot(m_g-m_f))^2$).
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 build memory guard. Everything is defined over literal tables and free scalars: coreWeight is the 36-entry rational raw-coefficient table (kernel-identified elsewhere with the true Jacobian coefficients), slotDispCore and slotMidTwice are the literal displacement-class and doubled-midpoint tables, and corePolEdgeCoeff supplies the seven edge-class linear forms $c_d=\sum_{ij}E_{ij}D_d^i D_d^j$.
A single summand coreTripleTerm is the signed raw moment $-(\mathrm{phase})^2/2\cdot(-(w_{fg},c_f,c_g))$. The six committed spike blocks tetBlock0–tetBlock5 are pure data transcriptions of those 36-term faces; tetBlock1 is the tet-1 face, and the upstream identity tetBlock1_eq collapses it to a pure quadratic polynomial in the $E_{ij}$ and $x_k$ (every $s_2/s_3/p$ entry of $G$ multiplies a literal zero midpoint factor).
The local goal is the core identity that the full 216-term raw moment sum equals the sum of the six spike blocks, identically in $E$ and $x$ and for completely free $s_2,s_3,p$. This declaration is the tet-1 slice of that partition.
proof idea
Term-mode wrapper that is really a short tactic script. First rewrite the right-hand side by tetBlock1_eq, replacing the expanded spike transcription by its collapsed pure-QQ polynomial (no residual $s_2,s_3,p$ dependence). Then simp only unfolds the finite sums over Fin 6 and Fin 3 together with the literal tables coreTripleTerm, coreWeight, corePolEdgeCoeff, slotDispCore, and slotMidTwice. A push_cast clears integer-to-real coercions, and ring equates the two multivariate polynomials.
why it matters
Feeds directly into coreTripleSum_eq_spikeSum, the core Gate C-B identity: the 216-term raw moment sum equals tetBlock0+…+tetBlock5 for free $s_2,s_3,p$, identically in $E$ and $x$. That identity is the algebraic heart of the Regge TT Gate B bridge (Lane C finishing charter): it shows the spike blocks are not an external continuum claim but a faithful regrouping of the discrete moment sum, without ever invoking tt_continuum_certificate.
In the broader Recognition gravity stack this closes a leaf of the continuum-certificate bridge between the discrete Regge/TT stencil and the committed spike transcription. Sibling theorems coreBlock0_eq–coreBlock5_eq cover the other five tet faces; together they discharge the heavy ring work in a memory-safe import context. No new axioms; expected footprint is the standard trio.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.