bucketKeyOf
plain-language theorem explainer
Maps each raw stencil triple (tetrahedron index, left slot, right slot) to a bucket whose phase vector is the doubled midpoint displacement from left to right. Downstream Bloch-fold and fiber-amplitude constructions cite it as the geometry-derived key. The body is a pure structure constructor from slotMidTwice differences.
Claim. For a raw stencil triple $(t,f,g)\in\{0,\ldots,5\}^3$, the bucket key is the representative with left slot $f$, right slot $g$, and phase vector $u$ given componentwise by $u_i=m_i(t,g)-m_i(t,f)$, where $m_i(t,s)$ is the geometry-derived doubled midpoint coordinate of local edge slot $s$ on tetrahedron $t$.
background
This module is the C-DAG1 finite-cell assembly stage for Regge TT: the cosine evaluator is defined from a bucket's integer phase key, independently of any quadratic moment evaluator. The target type is Bucket: a triple of left slot, right slot (each in a 6-element edge-slot index), 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 phase is built from the doubled midpoint coordinate of a local edge slot: twice its base offset plus its positive displacement bit. For each coordinate $i$, that midpoint is evaluated on the right slot and on the left slot of the same tetrahedron, then subtracted. The raw domain is all $6^3=216$ tetrahedron/slot triples; the image of this key is the finite support of the raw cosine fold.
proof idea
Definition by structure construction, not a proof. Unpack the input triple as $(t,f,g)$; set left $=f$, right $=g$, and phase $=i\mapsto$ (doubled midpoint of $(t,g)$ in coordinate $i$) minus (doubled midpoint of $(t,f)$ in coordinate $i$). No lemmas are applied; the body is the Bucket constructor applied to those three fields.
why it matters
Central geometry-to-key map for the finite Bloch assembly. It defines the support of the raw cosine fold (image of all 216 triples) and the fiber filter inside the honest bucket-fiber amplitude. The evaluator identity states that the bucket cosine of a raw triple equals the cosine of the difference of its two cell-independent slot phases. The fold-expansion theorem rewrites the Bloch fold as a plain sum over all 216 triples with collisions retained through the fiber amplitude. Those pieces feed the finite-assembly headline: under exact doubled-frequency non-aliasing, the Schlaefli-reduced raw stencil equals the raw bucket cosine fold. An algebraic-closer lemma records equality with the bridge copy of the same key map, so production and bridge assemblies share one keying convention. Local to the Regge TT discrete gravity analysis; not a T0–T8 forcing step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.