hingeEdgeDiagonalBlock
plain-language theorem explainer
The hinge/edge-diagonal O(1) block of the real-space Regge Hessian at flat geometry, contracted with a polarization matrix's edge-class coefficients. Anyone auditing TT zero-mode cancellation in the assembled constant block cites this scalar. It is the explicit seven-class sum of 2π L''(ℓ_d²) c_d(E)², matching the sympy diagnostic hinge term term-for-term. As a closed-form definition there is no proof obligation beyond the formula.
Claim. For a polarization matrix $E\in\mathbb{R}^{3\times 3}$, define the hinge/edge-diagonal block $$H_{\mathrm{hinge}}(E)=\sum_{d=0}^{6} 2\pi\cdot\Bigl(-\frac{1}{4\,\ell_d^{2}\sqrt{\ell_d^{2}}}\Bigr)\,c_d(E)^{2},$$ where $\ell_d^{2}$ is the flat squared length of displacement class $d$ and $c_d(E)=\sum_{i,j}E_{ij}D_d^{i}D_d^{j}$ is the edge-class loading of $E$.
background
Gate C-A3 of the QG full-theory campaign (Paper C / Pillar 1) closes the hinge-aware TT zero mode for the Regge Hessian on the periodic Freudenthal torus. The stencil-only constant block (full per-tet Hessian contracted with edge-class coefficients, no hinge) does not vanish under TT: at the reported witness $E=\mathrm{diag}(1,-1,0)/\sqrt{2}$ with $k=e_z$ its residual is $-\pi(\sqrt{2}+4)/8$. The diagnostic records that the hinge contribution equals that same value, so the assembled block (hinge minus stencil residual) cancels.
The length functional is $L(\ell^{2})=\sqrt{\ell^{2}}$, so the second derivative at flat is $L''(\ell^{2})=-1/(4,\ell^{2}\sqrt{\ell^{2}})$. Flat deficits vanish, leaving the constant $2\pi$ on the hinge diagonal. Squared lengths $\ell_d^{2}$ come from the seven positive displacement classes of the periodic geometry (values 1, 1, 1, 2, 2, …). Edge-class coefficients $c_d(E)$ are the quadratic forms $\sum_{ij}E_{ij}D_d^{i}D_d^{j}$ from the symbol preflight.
proof idea
Pure definition: no tactics. The body is the finite sum over Fin 7 of $2\pi$ times $L''(\ell_d^{2})=-1/(4,\ell_d^{2}\sqrt{\ell_d^{2}})$ (with $\ell_d^{2}$ from periodicDispSqEdge) times the square of the edge-class coefficient polEdgeCoeff E d. It is the kernel transcription of the sympy diagnostic's hinge object, term for term.
why it matters
This scalar is the hinge half of the assembled constant block that Gate C-A3 must show vanishes at the TT witness. Downstream, hinge_cancels_recorded_residual evaluates it at the reported polarization and proves equality with the kernel-recorded stencil-only residual $-\pi(\sqrt{2}+4)/8$. The witness-level split theorem then pins the assembly convention in-kernel: assembled = hinge − stencil residual, with both sides zero, so no silent sign flip is possible. Together with the TT check on the witness and the Schlaefli-reduced zero-mode headline, it closes the hinge-aware zero-mode gate for Lane C of the finishing charter.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.