stencilOnlyConstantWitnessResidual
plain-language theorem explainer
Records the explicit real residual −π(√2+4)/8 of the stencil-only constant block at the reported TT witness. Gravity analysts cite it as the kernel-locked nonzero obstruction that the hinge/edge-diagonal O(1) term must cancel. Pure numeric definition: no derivation, just the diagnostic value pinned for later equalities.
Claim. The stencil-only constant-block residual at the reported transverse-traceless witness is the real number $-\pi(\sqrt{2}+4)/8$.
background
This module is the panel-locked C11 Regge TT Bloch interface audit (attempt 2). It keeps the first gate non-tautological: rawCellStencil is a literal triple sum over tetrahedra and ordered slot pairs, and the A2 reduced second variation is identified with that sum by distributing a finite inner sum (sign matching the live A2 Schlaefli-reduced contraction). Full rational bucket aggregation and assembled zero-mode cancellation are deliberately not claimed here.
A same-day sympy diagnostic found that the stencil-only constant block does not vanish. The ContinuumLimit path is expected to use the cosine two-jet route only after the hinge/diagonal constant block is formally connected. Gates A2-full, A3 (hinge-aware zero-mode), and B remain open in this file; no ContinuumLimit or spike certificate is imported.
Downstream, the hinge-aware module treats this constant as the kernel-recorded witness residual against which the assembled hinge/edge-diagonal block is compared.
proof idea
Definitional constant, not a proof. The body is the single real expression $-\pi(\sqrt{2}+4)/8$, matching the sympy diagnostic residual for the stencil-only constant block at the reported TT witness. No lemmas are applied.
why it matters
Pins the nonzero stencil-only obstruction that Gate C-A3 must cancel. Downstream, hinge_cancels_recorded_residual proves the hinge/edge-diagonal block at the TT witness equals this residual; assembledConstantBlock_eq_zero is the headline that the assembled constant block vanishes for every polarization; and assembled_witness_split locks the sign convention
assembled = hinge − residual
at the witness. Without this named constant, those equalities could silently drift from the diagnostic. It does not close Gate A3 by itself: it is the recorded obstruction the hinge term is shown to cancel. Framework role is local to the Regge TT second-variation / continuum interface, not a T0–T8 forcing step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.