coreWeight
plain-language theorem explainer
A fixed 6×6 table of rational stencil weights for the Regge TT raw Jacobian on six face slots. Gravity analysts cite it as the leaf-local coefficient data for the Gate C-B spike bridge. The definition is pure case-by-case assignment of fractions in {0, ±1/12, ±1/8, ±1/4}; no proof content.
Claim. Define a weight table $W:\{0,\ldots,5\}^2\to\mathbb{R}$ by the thirty-six explicit rationals $W(0,4)=-1/8$, $W(0,5)=1/4$, $W(1,1)=1/8$, $W(1,2)=-1/8$, $W(1,3)=-1/4$, $W(1,4)=1/4$, $W(1,5)=-1/8$, $W(2,1)=-1/8$, $W(2,2)=1/12$, $W(2,3)=1/4$, $W(2,4)=-1/8$, $W(3,1)=-1/4$, $W(3,2)=1/4$, $W(3,3)=1/4$, $W(3,4)=-1/4$, $W(4,0)=-1/8$, $W(4,1)=1/4$, $W(4,2)=-1/8$, $W(4,3)=-1/4$, $W(4,4)=1/8$, $W(5,0)=1/4$, $W(5,1)=-1/8$, and $W(i,j)=0$ on all remaining pairs.
background
Gate C-B of the Lane C finishing charter bridges a 216-term raw moment sum on six face indices to six tet-blocks of the continuum spike certificate. To keep the heavy polynomial algebra inside a laptop memory guard, this leaf module imports only the committed spike transcription and works entirely with literal tables and scalars.
The weight table here is the raw-coefficient stencil on pairs of face slots. Module documentation states it carries the same thirty-six rationals as the independent rational stencil of Gate C-A2f. The main bridge module later kernel-identifies the table with the actual raw Jacobian coefficient, so the leaf never trusts a hand transcription of geometry.
Companion tables in the same file fix slot displacement classes, doubled midpoints, and seven edge-class linear forms. One signed raw moment term multiplies phase-squared against a product of two weights and two edge coefficients; summing those terms over faces is the core identity of the bridge.
proof idea
No proof: the declaration is a definition by exhaustive pattern match on Fin 6 × Fin 6. Each of the thirty-six pairs is assigned a concrete rational in {0, ±1/12, ±1/8, ±1/4}. Downstream equalities rewrite with this table and discharge the finite cases by norm_num or by matching precomputed tet-block expansions.
why it matters
This table is the coefficient substrate for every core triple term in the leaf algebra. The parent theorem coreWeight_eq_raw in the main Gate B bridge proves it equals the actual raw Jacobian coefficient via Gate C-A2f kernel evaluation ("nothing is transcribed on trust"). The six private block equalities coreBlock0_eq–coreBlock5_eq and coreTripleTerm consume the table to show the 216-term raw moment sum equals tetBlock0+⋯+tetBlock5 identically in free scalars and edge data, without invoking the continuum certificate itself.
In the broader Regge TT program this is bookkeeping that lets the spike-convention bridge stay axiom-light (standard trio only, no sorry). It does not itself touch the forcing chain T0–T8 or the Recognition Composition Law; it is gravity-side discrete calculus supporting the continuum limit certificate path.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.