rawMomentSupport
plain-language theorem explainer
Defines the finite support of the raw Regge TT moment fold as the image of all 216 tetrahedron/slot triples under the geometry-derived bucket key. Anyone citing the Gate B convention bridge or comparing continuum and bridge moment folds uses this set. The body is a one-line Finset image of the universal triple product.
Claim. Let every raw stencil triple be a triple $(t,f,g)\in\{0,\ldots,5\}^3$. The raw moment support is the finite set of buckets obtained by sending each triple to the bucket whose left/right slots are $(f,g)$ and whose integer phase key is the doubled midpoint displacement $u=2(\mathrm{mid}_g-\mathrm{mid}_f)$. Equivalently, it is the image of the full $6^3=216$-element triple set under that bucket-key map.
background
This module closes Gate B of the Regge TT Bloch convention audit (Paper C / Pillar 1): the interface moment fold, built only from the raw cell stencil, must match the committed spike left-hand side under the seven TT hypotheses.
A bucket is a triple $(f,g,u)$ with slot indices $f,g\in\mathrm{Fin},6$ and an integer phase vector $u$ (the intended external convention identifies $(f,g,u)\sim(g,f,-u)$ but does not yet quotient). The local map bucketKeyOf sends a raw triple $(t,f,g)$ to the bucket with slots $(f,g)$ and $u_i=\mathrm{slotMidTwice}(t,g,i)-\mathrm{slotMidTwice}(t,f,i)$, i.e. the doubled midpoint displacement of the ordered slot pair, grounded against the actual periodic geometry of localEdgeOf.
The raw cell stencil comprises all $6\times6\times6=216$ triples. The support used by the moment fold is exactly the set of buckets hit by those triples; no external spike support is injected.
proof idea
One-line definition: take the universal Finset on $\mathrm{Fin},6\times\mathrm{Fin},6\times\mathrm{Fin},6$ and push it forward under the bucket-key map. No lemmas are applied; the image construction is the entire body. Downstream equalities (e.g. production cosine support equals this set) unfold both sides and rewrite by key-map agreement.
why it matters
This is the support argument of every Gate B bridge identity in the module. The headline gateB_convention_bridge instantiates the locked target on this support together with the midpoint-displacement phase quadratic and the fiber-aggregated amplitude. The unconditional bridge rawMoment_eq_committedSpikeLHS and the fold-to-triple identity reggeTTMoment_eq_rawTripleSum both quantify over it, using Finset.sum_image' so colliding keys are neither dropped nor double-counted.
Algebraic closer theorems identify the production continuum moment with the bridge moment and prove the bridge moment equals the half-adjugate closed form for symmetric polarizations; those proofs pass this support (or prove it equal to the production cosine support) as the first argument of reggeTTMoment. In the QG campaign it pins the claim that the moment support is the raw stencil's own bucket set, not a spike-side artifact.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.