coreTripleTerm
plain-language theorem explainer
Defines one signed raw moment contribution for a triple of slot indices (t,f,g) in the Regge TT Gate B bridge: minus half the squared midpoint-phase difference times the product of the literal weight and the two edge-class linear forms. Gravity analysts cite it when assembling the 216-term raw moment sum that must match the six tet blocks. The body is a pure arithmetic expression over the leaf tables (weights, displacements, doubled midpoints, polynomial edge coeffs).
Claim. For a $3\times 3$ real matrix $E$, a vector $x\in\mathbb{R}^3$, and a triple $q=(t,f,g)\in\{0,\ldots,5\}^3$, the signed raw moment term is $$-\frac{1}{2}\Big(\sum_{i=0}^{2} x_i\cdot\frac{m(t,g,i)-m(t,f,i)}{2}\Big)^2\cdot\Big(-(w_{f g}\,c_{d(t,f)}(E)\,c_{d(t,g)}(E))\Big),$$ where $m$ is the doubled midpoint table, $w$ the rational weight table, $d$ the displacement-class table, and $c_d(E)$ the edge-class linear form of class $d$.
background
This leaf module isolates the heavy polynomial algebra of the Gate C-B spike-convention bridge so that a 216-term ring normalization stays under the laptop memory guard. It imports only the committed spike transcription and basic real arithmetic; every table is a literal scalar or case table, later kernel-identified with geometry in the main bridge module.
The ingredients are: coreWeight, the $6\times 6$ rational raw-coefficient table (same values as Gate C-A2f's rationalStencilWeight); slotDispCore, mapping each slot pair to one of seven edge displacement classes; slotMidTwice, the doubled midpoint coordinate of a local edge slot (twice base offset plus positive displacement bit); and corePolEdgeCoeff, seven linear forms in the entries of $E$ (diagonal and pairwise sums).
The module doc states the target identity: the sum of all 216 raw moment terms equals tetBlock0+...+tetBlock5 identically in free $E$ and $x$, with spike blocks entering only as data.
proof idea
Pure definition, no proof. The body expands the signed product of two factors: (i) minus half the square of the midpoint-phase difference $\sum_i x_i\cdot(m(t,g,i)-m(t,f,i))/2$, built from the doubled-midpoint table; (ii) minus the product of the literal weight $w_{fg}$ with the two edge-class linear forms $c_{d(t,f)}(E)$ and $c_{d(t,g)}(E)$. All four tables are referenced by name; no tactics or lemmas fire.
why it matters
This is the atomic summand of the Gate C-B raw-moment expansion. Downstream, tripleTerm_ident in the main bridge module identifies each geometric signed moment with this literal term pointwise (no case split on the triple). The six private block equalities coreBlock0_eq through coreBlock5_eq sum the term over $(f,g)$ at fixed $t$ and match the corresponding tet block. Those feed coreTripleSum_eq_spikeSum, the core identity that the full 216-term sum equals the six-block spike polynomial identically in $E$ and $x$.
In the Lane C finishing charter this closes the algebraic half of the continuum-certificate bridge without invoking tt_continuum_certificate itself. It sits in the gravity analysis stack that ultimately supports the discrete-to-continuum Regge TT gate, consistent with the $D=3$ spatial forcing (T8) already fixed upstream.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.