assembledConstantBlock
plain-language theorem explainer
Defines the assembled constant block of the Regge TT symbol: the k=0 value of the raw cell stencil after Schlaefli reduction, combining hinge and per-tet Hessian contributions with the report's relative-minus convention. Input is a 3×3 polarization matrix E; output is a real scalar built from edge-class coefficients. Downstream zero-mode and continuum-limit theorems cite this object. The body is a triple sum over six tetrahedron types and face pairs, not a proved identity.
Claim. For a real $3\times 3$ polarization matrix $E$, the assembled constant block is $$A(E)=-\sum_{t,f,g=0}^{5} J_{fg}\,c_{d(t,f)}(E)\,c_{d(t,g)}(E),$$ where $J_{fg}$ is the raw Jacobian coefficient table, $d(t,f)$ is the displacement class of face $f$ in tetrahedron type $t$, and $c_d(E)$ is the edge-class coefficient of $E$ in class $d$. This is the $k=0$ value of the Schlaefli-reduced raw cell stencil (hinge plus Hessian, assembled as hinge minus stencil residual).
background
Gate C-A3 sits in the QG full-theory campaign (Paper C / Pillar 1). The module closes the hinge-aware zero mode for the Regge TT symbol: the stencil-only constant block does not vanish under TT (kernel residual $-\pi(\sqrt{2}+4)/8$ at the witness $E=\mathrm{diag}(1,-1,0)/\sqrt{2}$), but the assembled object does.
By the proved Gate A2 Schlaefli reduction, the $k=0$ raw cell stencil already folds the hinge/edge-diagonal $2\pi L''$ block together with the per-tet Hessian; no separate $\theta''$ term survives. The sympy report fixes the relative sign as assembled $=$ hinge $-$ $\Sigma_{Gcc}$. Edge-class coefficients $c_d=\mathrm{polEdgeCoeff}(E,d)$ are the same seven-class coordinates used by the hinge block.
The definition contracts the raw Jacobian table over six tetrahedron types and face pairs against those coefficients. A sibling algebraic identity records that the free-coefficient contraction is the perfect square $(c_0+c_1+c_2-c_3-c_4-c_5+c_6)^2/2$, which vanishes exactly on the alternating-sum hyperplane inhabited by geometric edge-class vectors.
proof idea
Definitional, not a proof. The body is a single negated triple sum: over tetrahedron type $t\in\mathrm{Fin},6$ and face indices $f,g\in\mathrm{Fin},6$, multiply the raw Jacobian entry $J_{fg}$ by the two edge-class coefficients of $E$ at the displacement classes of faces $f$ and $g$ in type $t$. No lemmas are applied; downstream theorems unfold this def and invoke the free-coefficient zero-mode identity plus the alternating-sum property of $\mathrm{polEdgeCoeff}$.
why it matters
This is the named scalar whose vanishing is the Gate C-A3 headline. assembledConstantBlock_eq_zero proves $A(E)=0$ for every polarization $E$ (hinge-aware zero mode: stencil-only fails, assembled succeeds). assembled_witness_split pins the report convention $A(E_w)=\mathrm{hinge}(E_w)-\mathrm{stencilOnlyResidual}$ at the TT witness. rawCellStencil_zeroMomentum identifies the $k=0$ raw cell stencil with $2A(E)$. Continuum-limit work consumes it via rawCosineFoldAtScale_zero: the scale-zero raw cosine fold is exactly this block and hence vanishes.
In the finishing charter this closes Lane C of Pillar 1 for the Regge TT symbol: without a named assembled constant block, the hinge-aware cancellation and the continuum $k\to 0$ limit have no kernel object to cite. It does not itself invoke T0–T8 or the RCL; it is pure discrete-gravity linear algebra feeding the continuum bridge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.