coreBlock0_eq
plain-language theorem explainer
The double sum of signed raw moment terms over the six-by-six slot pairs at tet index 0 equals the committed spike block for tet 0, identically in the edge matrix E, the displacement vector x, and free scalars s2, s3, p. Gravity analysts assembling the Gate C-B continuum bridge cite this leaf identity. The proof rewrites the spike block to its pure polynomial form, unfolds the literal coefficient tables, and closes by ring normalization.
Claim. For any real $3\times 3$ matrix $E$, any $x\in\mathbb{R}^3$, and free scalars $s_2,s_3,p\in\mathbb{R}$, $$\sum_{f=0}^{5}\sum_{g=0}^{5} T(E,x;(0,f,g)) = B_0(E_{ij},x_k;s_2,s_3,p),$$ where $T$ is the signed raw moment term $-({\rm phase})^2/2\cdot(-(w_{fg}\,c_f\,c_g))$ built from the literal weight table, edge-class linear forms, and doubled midpoint phases, and $B_0$ is the tet-0 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: the rational raw-coefficient table (36 weights), 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 $T=-({\rm phase})^2/2\cdot(-(w_{fg},c_f,c_g))$. The spike side contributes six committed blocks; tet block 0 is the literal 36-term transcription of $\tfrac12 G_{fg} c_{d(\tau,f)} c_{d(\tau,g)}(x\cdot(m_g-m_f))^2$. Upstream, that block collapses 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), which is the content of the tet-0 equality lemma used here.
The ambient setting is Lane C finishing: the main bridge later kernel-identifies these literal tables with the geometric rawJacobianCoefficient, periodic slot geometry, and polEdgeCoeff, so no transcription is trusted on faith.
proof idea
One short tactic script. First rewrite the right-hand side by the upstream tet-0 collapse lemma, replacing the spike transcription by its pure-QQ polynomial. Then simp only unfolds the finite sums over Fin 6 and Fin 3 together with the local definitions of the triple term, weight table, edge-class linear forms, slot displacement, and doubled midpoints. After push_cast clears integer-to-real coercions, ring normalizes both sides to the same multivariate polynomial.
why it matters
This is the tet-0 slice of the core Gate C-B identity. Downstream, the parent theorem sums the six block equalities (tet 0 through tet 5) to conclude that 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$. Only block data is used; the continuum certificate's TT conclusion is never invoked.
In the Lane C charter this leaf algebra is what lets the main bridge module stay thin: the heavy ring work lives here, while the parent file only assembles and grounds the tables against geometry. It does not itself touch the forcing chain (T0–T8) or the Recognition Composition Law; it is infrastructure for the Regge TT continuum gate that feeds the gravity side of the monolith.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.