coreBlock3_eq
plain-language theorem explainer
For fixed tet index 3, the 36-term double sum of signed raw moment contributions equals the committed spike block tetBlock3, identically in the 3×3 matrix E, the vector x, and free scalars s2, s3, p. Gate C-B bridge authors cite it when assembling the 216-term raw moment sum into six spike blocks. The proof rewrites the spike block to its pure polynomial form, unfolds the literal coefficient tables, and closes by 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}$, the double sum $\sum_{f=0}^{5}\sum_{g=0}^{5}$ of the signed raw moment term at triple index $(3,f,g)$ equals the literal tet-3 spike block evaluated on 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 for Regge TT continuum work. It imports only the committed spike transcription so that a 216-term ring normalization stays inside the laptop memory guard. All tables are literal: coreWeight is the 36-entry rational raw-coefficient stencil; slotDispCore and slotMidTwice are the displacement-class and doubled-midpoint tables; corePolEdgeCoeff supplies the seven edge-class linear forms $c_d=\sum_{ij}E_{ij}D_d^i D_d^j$; coreTripleTerm is one signed raw moment $-({\rm phase})^2/2\cdot(-(w_{fg}c_f c_g))$.
Upstream, tetBlock3 is the literal 36-term transcription of $(1/2)G_{fg}c_{d(\tau,f)}c_{d(\tau,g)}(x\cdot(m_g-m_f))^2$ for tet index 3, and tetBlock3_eq collapses that block to a pure quadratic polynomial in the $E_{ij}$ and $x_k$ (every $s_2/s_3/p$ entry of $G$ multiplies a literal $(0)^2$ midpoint factor). The present identity matches the raw double sum at fixed first index 3 against that committed block, with $s_2,s_3,p$ completely free.
proof idea
One short tactic script. First rewrite the right-hand side by tetBlock3_eq, replacing the spike block by its expanded pure-QQ polynomial. Then simp only unfolds Fin.sum_univ_six, coreTripleTerm, coreWeight, corePolEdgeCoeff, slotDispCore, slotMidTwice, and Fin.sum_univ_three, exposing the concrete rational coefficients and midpoint displacements. push_cast clears residual coercions. ring finishes the polynomial identity.
why it matters
This is one of six parallel block equalities (indices 0 through 5) that feed the core identity coreTripleSum_eq_spikeSum: the full 216-term raw moment sum equals tetBlock0+...+tetBlock5 for free $s_2,s_3,p$, identically in $E$ and $x$. That core identity is the algebraic heart of the Gate C-B bridge in the Lane C finishing charter; only block data is used, never the continuum certificate conclusion itself. In the broader Recognition gravity stack the bridge lets the discrete Regge TT stencil talk to the continuum spike transcription without trusting hand-copied coefficients, because the main module kernel-identifies the literal tables with the geometric rawJacobianCoefficient, polEdgeCoeff, and edgeMidpointPhase. No forcing-chain landmark (T5–T8) is invoked here; the work is pure finite polynomial algebra supporting the gravity analysis layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.