coreTripleSum_eq_spikeSum
plain-language theorem explainer
The 216-term raw-moment triple sum over six-by-six-by-six slot indices equals the sum of the six committed tetrahedral spike blocks, identically in the edge matrix E and the displacement vector x, for completely free scalars s2, s3, p. Gravity analysts bridging the Regge TT stencil to the continuum spike certificate cite this leaf identity. The proof splits the product sum into six Fin-6 blocks and rewrites each by the corresponding core-block equality.
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_{q\in\{0,\ldots,5\}^3}\mathrm{coreTripleTerm}(E,x,q)=\sum_{k=0}^{5}\mathrm{tetBlock}_k(E,x,s_2,s_3,p),$$ where each $\mathrm{tetBlock}_k$ 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$ on tetrahedron $k$, and $\mathrm{coreTripleTerm}$ is one signed raw-moment summand $-(\mathrm{phase}^2)/2\cdot(-(w_{fg}c_fc_g))$.
background
This leaf module isolates the heavy polynomial algebra of the Gate C-B spike-convention bridge so that a 216-term normalization does not blow the build-memory guard. Everything is defined over literal tables and scalars: coreWeight is the rational raw-coefficient table (36 values matching Gate C-A2f's stencil weights); slotDispCore and slotMidTwice are the slot displacement-class and doubled-midpoint tables; corePolEdgeCoeff holds the seven edge-class linear forms. One summand coreTripleTerm is the signed raw moment $-(phase^2)/2\cdot(-(w_{fg}c_f c_g))$.
Upstream, the six tetBlock0..tetBlock5 definitions are literal transcriptions 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$ on each tetrahedron. They enter here as pure data: the continuum certificate and its $-1/4$ conclusion are never invoked. Sibling lemmas coreBlock0_eq..coreBlock5_eq identify each Fin-6 fiber sum of triple terms with the matching tet block.
proof idea
Short tactic proof. First simp only [Fintype.sum_prod_type] flattens the sum over Fin 6 × Fin 6 × Fin 6 into an iterated sum. Then Fin.sum_univ_six expands the outer index into six concrete summands. Each summand is rewritten by the matching sibling equality coreBlockk_eq E x s2 s3 p ($k=0..5$), which already equates that fiber to tetBlockk evaluated on the nine entries of $E$, the three components of $x$, and the free scalars $s_2,s_3,p$. No ring normalization or continuum certificate is needed at this layer.
why it matters
This is the core algebraic identity of the Gate C-B bridge in the Lane C finishing charter. Downstream, rawMoment_eq_committedSpikeLHS chains fiber aggregation, pointwise identification, and this 216-term identity at the committed instantiation $s_2=\sqrt{2}$, $s_3=\sqrt{3}$, $p=\pi$, proving the raw-stencil moment fold equals the committed spike LHS identically in $(E,x)$. Only block data is used; the spike's TT continuum certificate and its $-1/4$ conclusion stay out of scope.
In the broader Recognition gravity stack this closes the leaf half of the Regge TT stencil-to-spike bridge: the continuum side can later quote the spike blocks without re-deriving the 216-term polynomial match. The module is deliberately import-thin (committed spike transcription only) so the heavy algebra stays buildable. Expected axiom footprint is the standard trio; no sorry, admit, or native_decide.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.