Bucket
plain-language theorem explainer
A bucket is a triple of left slot index, right slot index (each in a six-slot cell), and an integer phase displacement in three dimensions. It is the discrete key used to group raw Regge TT stencil triples before cosine folding. Downstream assembly and Gate B convention work cite it as the support type for amplitudes and phase evaluators. As a structure with decidable equality, it needs no proof beyond field packing.
Claim. A bucket is a triple $(f,g,u)$ with slot indices $f,g \in \{0,\ldots,5\}$ and integer phase key $u:\{0,1,2\}\to\mathbb{Z}$. The external identification intended later is only $(f,g,u)\sim(g,f,-u)$; this type does not quotient by that relation or aggregate fibers.
background
This module is the panel-locked C11 Regge TT Bloch interface audit (attempt 2). It keeps the first gate non-tautological: the raw cell stencil is a literal $6\times 6\times 6$ triple sum over tetrahedra and ordered slot pairs, not definitionally wired to the rational bucket table it is meant to audit.
A phase vector is an integer displacement key $u:\mathrm{Fin},3\to\mathbb{Z}$ used to label plane-wave phase buckets on the lattice. Upstream continuum TT work defines a continuous plane-wave phase $k\cdot x$ on four-vectors; here the discrete analogue is the integer key carried by each bucket.
The eight-tick foundation supplies continuous phases $k\pi/4$, but this structure is purely combinatorial: it packages two of six ordered slots with a three-component integer phase for later cosine evaluation and fiber sums.
proof idea
Definitional structure only: three fields (left, right in Fin 6, phase a PhaseVector), with derived DecidableEq and Repr. No lemmas, tactics, or equalities are proved. The doc-comment records that the intended external symmetry $(f,g,u)\leftrightarrow(g,f,-u)$ is not yet imposed as a quotient.
why it matters
Buckets are the discrete support type for the Regge TT Bloch assembly path. Downstream, bucketKeyOf maps each raw tetrahedron/slot triple to a bucket whose phase is the doubled midpoint displacement between slots; rawBucketAmplitude honestly sums signed stencil weights over that fiber; rawCosineEvaluator and rawCosineSupport fold cosines over the finite image of all 216 triples.
Gate B convention audit takes a Finset Bucket together with phase-quadratic and amplitude maps as the open target for matching the spike LHS under the seven TT equations, without importing continuum certificates. Module status keeps Gate A2-full (aggregate raw weight equals rational over all buckets), Gate A3 (hinge-aware zero-mode), and Gate B open. The type therefore anchors the non-tautological audit surface between raw stencil geometry and eventual continuum limit cosine two-jet work.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.