rationalStencilWeight
plain-language theorem explainer
Independent 6×6 rational stencil table for Regge TT bucket aggregation: each bucket's left/right edge-slot pair maps to a fixed rational in {0, ±1/8, ±1/4, 1/12}. Anyone closing Gate C-A2f cites it as the radical-free right-hand side that the raw Jacobian coefficient must match. Defined by a bare phase-independent match on the 36 slot pairs, not via fiber sums or the radical-bearing coefficient.
Claim. For a bucket with edge-slot indices $f,g\in\{0,\ldots,5\}$, the rational stencil weight is the literal table entry $W_{fg}\in\mathbb{Q}$ given by the fixed 36-branch assignment with values in $\{0,\pm 1/8,\pm 1/4,1/12\}$, independent of the bucket phase key.
background
This module finishes Gate C-A2f of the Regge TT Bloch-interface campaign (Paper C / Pillar 1, Lane C). The raw stencil coefficient is $J_{fg}/(2\sqrt{a^_f})$, where $J$ is the flat-angle Jacobian and $a^$ is the Freudenthal flat squared-edge tuple. That expression carries square-root radicals from the angle derivatives.
A bucket is a triple (left slot, right slot, phase vector) with slots in $\mathrm{Fin},6$. The intended external identification only swaps $(f,g,u)\sim(g,f,-u)$; this table is the phase-free weight on the underlying $6\times 6$ matrix of slot pairs.
Upstream, the Schläfli radical bridge writes $\sqrt{a^_f},(\mathrm{d}\theta_f/\mathrm{d}a_g)=(1/\sqrt{2,\mathrm{cm}_3})\cdot N$, with $N$ the rationalized Schläfli summand norm and $\sqrt{2,\mathrm{cm}_3}=4$ on the flat tuple, so every entry reduces to a pure rational cofactor over $8a^_f$. The interface-audit module only recorded two smoke entries; this definition supplies the full independent table.
proof idea
Definition by exhaustive pattern match on the pair (left, right) of Fin-6 indices. Each of the 36 branches is a literal rational constant; there is no computation, no fiber sum, and no reference to the raw Jacobian coefficient. Phase is ignored by construction. The offline derivation (closed forms of the flat-angle Jacobian and flat edge tuple) is external; the Lean object is only the resulting table.
why it matters
This is the independent right-hand side of the Gate C-A2f headline aggregate_raw_weight_eq_rational: on every bucket, the radical-bearing raw coefficient equals the real cast of this table. Downstream, rawJacobianCoefficient_eval evaluates all 36 entries by kernel rational arithmetic after the Schläfli bridge; rationalStencilWeight_swap shows the matrix is symmetric, so the external bucket quotient is well-defined on table values; and the smoke/worst-radical corollaries recover the two interface-audit kernel facts ($(0,5)=1/4$, $(1,2)=-1/8$).
The proved value set ${0,1/12,\pm 1/8,\pm 1/4}$ is strictly larger than the panel preregistration ${0,\pm 1/4,-1/8}$ (extra diagonal entries $+1/8$, $+1/12$, $+1/8$). Closing this gate removes the last open bucket-fiber aggregation obligation left by the Bloch interface audit and feeds the Gate-B bridge that equates core weights to the raw coefficients.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.