blochFold11
plain-language theorem explainer
Defines the honest transported finite-momentum Bloch fold on the type-(1,1) hinge orbit: a double sum of 72 phase-decorated slot bilinears of a 4×4 Hessian against a wave vector. Gravity analysts cite it as the classical (1,1) fold that closing theorems evaluate at the star momentum. The body is a pure double sum of the transported slot term.
Claim. For a $4\times 4$ real matrix $H$ and momentum $m\in\mathbb{R}^4$, the transported $(1,1)$ Bloch fold is $\sum_{s=0}^{23}\sum_{t=0}^{9}$ of the transported slot term of $(H,m)$ at oriented slot $(s,t)$. Each nonzero summand is the product of two midpoint-phased class dots (area covector and deficit kernel) on type-$(1,1)$ hinges; other hinge types contribute zero.
background
This module runs the QG full-theory campaign for the exact phase-decorated fold of the committed true-weight flat Hessian on type-$(1,1)$ triangle hinges inside one Kuhn cell, using the midpoint plane-wave convention of the 4D Regge edge stencil. Scope is the $(1,1)$ orbit only: 72 oriented slots per cell (indexed as $24\times 10$, with a type filter).
The building block is the transported slot term: if the slot is type $(1,1)$, it multiplies two phased class dots of $H$ against $m$ at the hinge base (one on the slot area covector, one on the deficit kernel); otherwise it is zero. Phasing follows the midpoint plane-wave convention, so finite momentum enters only through those phases.
At zero momentum the factorized phased fold is required to match the committed orbit-zero-momentum quadratic on .t11. The present definition is the finite-momentum transported version of that fold.
proof idea
Pure definition: unfold to the double sum $\sum_s\sum_t$ of the transported slot term. No lemmas, no tactics. Non-$(1,1)$ slots vanish inside the summand, leaving the honest 72-instance fold.
why it matters
This is the classical $(1,1)$ fold that the transported algebraic closer identifies with the orbit fold (blochFoldOrbit_t11_eq_blochFold11) and that the area-match package closes against. Downstream closing theorems evaluate it at the star momentum $m^\star=(\pi/2,\pi/2,\pi/2,0)$: on the axis TT polarization it equals $-3$ (nonzero, nonvacuity), and on the pure-gauge decoy it equals $-4+4\sqrt{2}$ (nonzero, so discrete gauge invariance at finite momentum holds only up to the finite-difference identity).
It also feeds bilinearity and the M2-symbol fold-along construction. In the module's binding tier tags it is item 2 of what is proved (transported phased fold over all 72 slots). It does not itself touch continuum EH/TT symbol matching, $S_{\mathrm{RS}}$ convergence, or gap-action recovery; those remain later lanes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.