rawBucketAmplitude
plain-language theorem explainer
Bucket-fiber amplitude for the Regge TT Gate B bridge: given a polarization matrix E and bucket b, sum the signed raw triple stencil weights over every triple whose bucket key equals b. Gravity analysts closing the continuum moment fold use it as the amplitude argument to the interface moment. The body is a plain filtered Finset sum of the raw triple weight; no algebraic identity is proved here.
Claim. For a real $3\times 3$ matrix $E$ and a bucket $b$, the raw bucket amplitude is $A_E(b):=\sum_{\kappa(p)=b} w_E(p)$, summing the signed raw triple weight $w_E(p)$ over all raw stencil triples $p=(t,f,g)$ whose bucket key $\kappa(p)$ equals $b$. Each weight is the signed product of the Jacobian coefficient of the slot pair with the two polarization edge coefficients of $E$.
background
Gate B (Paper C / Pillar 1, Lane C) asks that the interface moment fold reggeTTMoment, when fed support, phase quadratic, and amplitude built only from the raw cell stencil, equal the committed six-block spike LHS under the seven TT hypotheses. This module instantiates those three inputs from the raw stencil rather than from the spike.
A raw triple is a tetrahedron type with an ordered slot pair among the 216 stencil cells. The bucket key map sends each triple to a bucket $(f,g,u)$ whose integer phase key $u$ is the doubled midpoint displacement of the slot pair (grounded against periodic geometry by the midpoint-phase lemma). The raw triple weight is the signed stencil contribution $-(J_{fg}/(2\sqrt{a^*f})),c{d(t,f)},c_{d(t,g)}$, with the minus sign inherited from the raw cell stencil itself.
The amplitude at a bucket is the honest fiber sum of those weights: every triple landing in the bucket is counted once, with no collision dropped or double-counted. Sibling definitions supply the support (image of all 216 triples under the key map) and the squared midpoint-displacement phase quadratic used by the frozen cosine two-jet convention.
proof idea
Definition only: filter the universe of raw triples to those with bucket key equal to $b$, then sum the raw triple weight of $E$ on that fiber. No lemmas are applied; the equality of this fold to the plain 216-term triple sum is deferred to the next section (Finset.sum_image' on the key map).
why it matters
This is the amplitude leg of the Gate B bridge instantiation. Downstream, the algebraic closer proves the two module copies of the amplitude coincide, that the production continuum moment fold equals the Gate B bridge moment, and that both equal $\tfrac12 x^T\mathrm{adj}(E)x$ for symmetric polarizations (the C8 closed form). Under full TT data the same fold evaluates to the continuum coefficient $-1/4$ (P1.1b headline).
It also feeds the Bloch-assembly identities that identify the canonical finite Hamiltonian with the raw cosine Bloch fold. Without a fiber-honest amplitude built from the actual raw stencil objects (Jacobian, pol-edge coeffs, grounded displacement classes), the Gate B convention target cannot be stated, let alone discharged.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.