corePolEdgeCoeff
plain-language theorem explainer
Seven literal edge-class linear forms on a free 3×3 real matrix E: the three diagonal entries, the three 2×2 principal-block sums, and the full nine-entry sum. They stand in for c_d = ∑_{ij} E_{ij} D_d^i D_d^j in the leaf algebra of the Regge TT Gate B bridge. Downstream proofs identify them with the true polEdgeCoeff and feed them into the 216-term triple-moment sum. Pure pattern-match definition; no proof obligation.
Claim. For a free matrix $E:\{0,1,2\}^2\to\mathbb{R}$, define seven real coefficients $c_0,\ldots,c_6$ by $c_0=E_{00}$, $c_1=E_{11}$, $c_2=E_{22}$, $c_3=E_{00}+E_{01}+E_{10}+E_{11}$, $c_4=E_{00}+E_{02}+E_{20}+E_{22}$, $c_5=E_{11}+E_{12}+E_{21}+E_{22}$, and $c_6=\sum_{i,j=0}^{2}E_{ij}$. These are the edge-class linear forms $c_d=\sum_{ij}E_{ij}D_d^i D_d^j$ written out on the nose.
background
Gate C-B of the Lane C finishing charter bridges the Regge TT continuum certificate to a spike-convention transcription. The present module is a leaf import file: it holds only literal tables and scalar algebra so that a 216-term ring normalization does not blow the laptop memory guard when the full symbol-program chain is loaded.
The seven forms here are the edge-class contractions $c_d=\sum_{ij}E_{ij}D_d^i D_d^j$. Indices $0,1,2$ pick the pure diagonal classes; $3,4,5$ pick the three coordinate-plane $2\times 2$ blocks; index $6$ is the full sum. The matrix $E$ is free (no symmetry or positivity assumed at this layer). Sibling literals supply the rational raw-coefficient table, the slot displacement-class table, and the doubled-midpoint phase table; the main bridge module later kernel-identifies each table with its geometric source.
Upstream geometry (Freudenthal two-cube strip, eight-tick phases, lattice-ball edges) motivates the seven classes but is not imported here; only basic real arithmetic is in scope.
proof idea
No proof: this is a pure definition by exhaustive pattern match on Fin 7. Each clause writes the corresponding linear form in the nine free entries of $E$ by hand. Identification with the geometric polEdgeCoeff is deferred to the one-line fin_cases/ring theorem in the parent bridge module.
why it matters
These seven scalars are the only channel through which the free matrix $E$ enters the leaf triple-moment algebra. Every coreTripleTerm multiplies a weight by a product of two such coefficients, and the six block equalities coreBlock0_eq–coreBlock5_eq rewrite the resulting $6\times 6$ double sums into the committed spike blocks tetBlock0–tetBlock5. The parent theorem corePolEdgeCoeff_eq then asserts that the literals equal the true geometric polEdgeCoeff, so the core identity coreTripleSum_eq_spikeSum (216 raw moments equal the six tet blocks, identically in free $E,x,s_2,s_3,p$) transfers to the actual continuum certificate without ever invoking tt_continuum_certificate inside the leaf. In the broader RS gravity stack this is bookkeeping for the discrete-to-continuum TT gate, not a new physical claim; it keeps Gate C-B axiom-light (standard trio only, no sorry).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.