coreBlock5_eq
plain-language theorem explainer
The double sum of signed raw moment terms with first multi-index fixed at 5 equals the fifth committed spike-block polynomial, identically in the 3×3 edge matrix E, the vector x, and free scalars s2,s3,p. Anyone assembling the six-block partition of the 216-term Regge TT Gate B core identity cites this. Proof unfolds the block definition, expands the Fin-6/Fin-3 table lookups, and closes by ring.
Claim. For every real $3\times 3$ matrix $E$, every $x\in\mathbb{R}^3$, and every free $s_2,s_3,p\in\mathbb{R}$, $$\sum_{f=0}^{5}\sum_{g=0}^{5} T(E,x;(5,f,g)) = B_5\bigl(E_{ij},x_k;s_2,s_3,p\bigr),$$ where $T$ is the signed raw moment term $-(\mathrm{phase}^2)/2\cdot(-(w_{fg}\,c_f\,c_g))$ built from the literal weight, displacement-class, midpoint, and edge-coefficient tables, and $B_5$ is the fifth committed spike-block polynomial.
background
This leaf module isolates the heavy polynomial algebra of the Regge TT Gate B bridge (Lane C finishing charter, Gate C-B). It imports only the committed spike transcription so that a 216-term ring normalization stays under the build memory guard. Everything is defined over literal tables and free scalars: the rational raw-coefficient table (same 36 values as Gate C-A2f's stencil weights), the slot displacement-class table, the doubled-midpoint table, and the seven edge-class linear forms. The main bridge later kernel-identifies these tables with the geometric objects; this file never trusts a transcription.
A single signed raw moment term is $T = -(\mathrm{phase}^2)/2\cdot(-(w_{fg},c_f,c_g))$. The 216-term sum runs over a triple of Fin-6 indices. It is partitioned into six blocks by fixing the first index $q_0\in{0,\ldots,5}$; this declaration is the $q_0=5$ slice. The free parameters $s_2,s_3,p$ enter only through the committed block polynomials and are never specialized here.
proof idea
Term-mode algebraic identity. Rewrite the right-hand side by the defining equation of the fifth spike block. Then simp only expands both Fin-6 double sums, the raw moment term, and the four literal tables (weights, edge coefficients, slot displacements, doubled midpoints), together with the Fin-3 sums that appear inside those tables. After push_cast clears numeral coercions, ring normalizes both sides to the same multivariate polynomial in the nine entries of $E$, the three components of $x$, and the free scalars $s_2,s_3,p$.
why it matters
One of six block equalities that feed the core identity coreTripleSum_eq_spikeSum: the full 216-term raw moment sum equals the sum of the six committed spike blocks, for completely free $s_2,s_3,p$ and identically in $E$ and $x$. That core identity is the algebraic heart of the Gate B bridge; only block data is used, and the spike's continuum TT conclusion is never invoked. Closing the six blocks therefore discharges the leaf-side half of Gate C-B without touching continuum certificates or the heavier symbol-program import chain. In the broader gravity lane this is pure support algebra: it does not itself force $D=3$ or the eight-tick structure, but it makes the discrete-to-continuum moment matching checkable by ring.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.