row0SmokeBucket
plain-language theorem explainer
Defines the row-0 smoke-test bucket as the pair of tetrahedron slots (0,5) with vanishing Bloch phase. It is the radical-trivial test case for the stencil weight J_05/(2 sqrt a*_0) when freudenthalTetSqEdges 0 = 1. Downstream smoke theorems cite it to check that the rational table returns 1/4. The body is a three-field structure literal.
Claim. The row-0 smoke-test bucket is the triple $(f,g,u)=(0,5,0)$ in the bucket space: left slot $0\in\mathrm{Fin}\,6$, right slot $5\in\mathrm{Fin}\,6$, and zero phase vector. It represents the radical-trivial coefficient $J_{05}/(2\sqrt{a^*_0})$ with $\mathrm{freudenthalTetSqEdges}(0)=1$.
background
This module is the panel-locked C11 Regge TT Bloch interface audit. It keeps the first gate deliberately non-tautological: rawCellStencil is a literal $6\times6\times6$ triple sum, and full rational bucket aggregation plus hinge-aware zero-mode cancellation are not claimed here. Gates A2-full, A3, and B remain open.
A bucket is a representative triple $(f,g,u)$ with left and right slots in $\mathrm{Fin},6$ and a phase vector. The intended external convention only identifies $(f,g,u)$ with $(g,f,-u)$; this attempt does not yet quotient or aggregate all fibers.
The row-0 smoke bucket is the isolated radical-trivial cell used before any full fiber aggregation. Doc-comment: it stands for $J_{05}/(2\sqrt{a^*_0})$ with $\mathrm{freudenthalTetSqEdges},0=1$.
proof idea
Definitional structure literal, not a proof. Instantiates Bucket with left slot $\langle 0\rangle$, right slot $\langle 5\rangle$ (both discharged by decide on Fin 6), and phase the zero function on the phase index. No lemmas are applied.
why it matters
Supplies the fixed smoke-test input for the narrow C11 audit gate. Downstream, row0Smoke_table_value shows the independent rational table agrees with this bucket after casting to reals, equaling $1/4$, and is "intentionally only the isolated smoke-test bucket, not the full aggregate_raw_weight_eq_rational gate." In the aggregation module, table_matches_row0Smoke equates the same rational weight to rawJacobianCoefficient (0,5), again kernel-recorded as $1/4$.
The definition therefore anchors the first non-tautological check that stencil weights match the rational table on a radical-trivial cell, without claiming full A2 aggregation, hinge-aware zero-mode (A3), or the spike convention bridge (B). It sits in the gravity analysis path toward continuum TT second-variation control, not in the T0–T8 forcing chain itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.