bucketKeyOf
plain-language theorem explainer
Maps each raw Regge TT stencil triple (tetrahedron type t, ordered edge slots f,g) to a bucket whose left/right slots are (f,g) and whose integer phase vector is the doubled midpoint displacement mid_g − mid_f. Gravity analysts cite it when assembling the raw cell stencil into a Bloch cosine fold. The body is a one-line structure constructor from the grounded slotMidTwice table.
Claim. For a raw stencil triple $p=(t,f,g)\in\mathrm{Fin}\,6\times\mathrm{Fin}\,6\times\mathrm{Fin}\,6$, the bucket key is the triple $(f,g,u)$ with phase vector $u_i=\mathrm{slotMidTwice}(t,g,i)-\mathrm{slotMidTwice}(t,f,i)$ for each spatial coordinate $i\in\{0,1,2\}$. Equivalently, $u=2(\mathrm{mid}_g-\mathrm{mid}_f)$ in doubled midpoint coordinates.
background
Gate B of the Regge TT campaign equates the interface moment fold reggeTTMoment (support, phase quadratic, amplitude) built from the actual raw cell stencil with the committed spike LHS under the seven TT hypotheses. The raw stencil is indexed by 216 triples $(t,f,g)$: tetrahedron type and an ordered pair of local edge slots.
A Bucket is a representative $(f,g,u)$ with left/right slots in $\mathrm{Fin},6$ and an integer phase vector $u:\mathrm{Fin},3\to\mathbb{Z}$. The intended external convention only identifies $(f,g,u)\sim(g,f,-u)$; this map does not yet quotient fibers. The doubled midpoint table slotMidTwice t f i is geometry-derived: twice the base offset of slot $f$ on tetrahedron $t$ plus the positive displacement bit in coordinate $i$. The bridge core also carries a literal table of the same values, kernel-identified with the assembly version.
Upstream, the assembly module already defines the same constructor; the bridge re-exports it so that support, phase quadratic, and bucket amplitudes can be built entirely from the raw stencil rather than from the spike convention.
proof idea
Pure definitional constructor. Unpack the triple $p=(t,f,g)$ and form the Bucket structure with left := f, right := g, and phase := fun i => slotMidTwice t g i - slotMidTwice t f i. No lemmas or tactics; the phase is exactly the doubled midpoint displacement from the left slot to the right slot, matching the assembly-side definition line-for-line.
why it matters
This is the geometry-to-bucket dictionary for Gate B (Paper C / Pillar 1, Lane C). Every raw-stencil object in the bridge is keyed through it: rawMomentSupport is its image on all 216 triples; rawBucketAmplitude sums signed triple weights over the fiber of a fixed bucket; rawPhaseQuadratic evaluates the squared midpoint-displacement phase on that bucket.
Downstream, the algebraic closer proves production and bridge keys coincide (bucketKeyOf_eq). Assembly theorems then expand the raw cosine Bloch fold to a plain 216-term sum (rawCosineFold_eq_rawTripleSum), identify the bucket cosine with the difference of cell-independent slot phases (rawCosineEvaluator_bucketKeyOf), and close the finite-assembly headline that the Schlaefli-reduced raw stencil equals the raw bucket cosine fold under doubled-frequency non-aliasing (rawCellStencil_eq_rawCosineBlochFold). Without a grounded key, the spike-convention bridge cannot claim that support and amplitude come from the actual stencil rather than from the committed LHS.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.