transportedSlotTerm
plain-language theorem explainer
Per-slot contribution to the finite-momentum (1,1) Bloch fold on a Kuhn cell: product of phased area and deficit class dots when the hinge is type (1,1), else zero. Gravity analysts cite it as the atomic summand of the 72-slot transported fold. The body is a one-line conditional product of two plane-wave class pairings at the hinge base.
Claim. For a class matrix $H\in\mathrm{Mat}_4$, wave vector $m\in\mathbb{R}^4$, and oriented slot $(s,t)\in\{0,\ldots,23\}\times\{0,\ldots,9\}$, the transported slot term equals $\langle A_{s,t},\,H,m,x_{s,t}\rangle_{\mathrm{ph}}\cdot\langle K_{s,t},\,H,m,x_{s,t}\rangle_{\mathrm{ph}}$ if the hinge orbit type is $(1,1)$, and equals $0$ otherwise. Here $A_{s,t}$ is the slot area-covariance mask, $K_{s,t}$ the slot deficit kernel, $x_{s,t}$ the hinge base, and $\langle v,H,m,x\rangle_{\mathrm{ph}}=\sum_d v_d\,(\text{plane-wave class perturbation of }H\text{ at }m,x)_d$.
background
Module setting: exact phase-decorated fold of the committed true-weight flat Hessian for type-(1,1) triangle hinges in one Kuhn cell, under the midpoint plane-wave convention of the 4D Regge edge stencil. Scope is the (1,1) orbit only (72 oriented slots per cell). This lane does not yet match the $m^2$ Taylor coefficient to the Einstein–Hilbert / TT continuum symbol.
A hinge base $x_{s,t}$ is the coordinate mask of the first triangle-vertex mask of slot $(s,t)$. The predicate “type (1,1)” is decidable equality of the hinge orbit type with .t11. The phased class dot pairs a 15-component class vector $v$ against the plane-wave class perturbation of $H$ at momentum $m$ and base $x$. Slot area covariance puts weight $1/4$ on the two difference masks of the slot and zero elsewhere; the slot deficit kernel is the matching deficit support for that hinge.
Upstream cost algebra supplies the shifted cost $H(x)=J(x)+1=\frac12(x+x^{-1})$ (d’Alembert form of the Recognition Composition Law), but here $H$ is overloaded as the $4\times4$ class matrix argument of the fold, not the scalar cost.
proof idea
Definition by cases, not a proved theorem. If the hinge is type (1,1), return the product of two phased class dots at the same hinge base: one against the slot area-covariance mask, one against the slot deficit kernel. Otherwise return 0. No lemmas are applied; the body is pure arithmetic assembly of already-defined masks and the phased pairing.
why it matters
Atomic summand of the honest transported finite-momentum (1,1) Bloch fold: blochFold11 is exactly the double sum of this term over all 24×10 slots. Downstream bilinearity (blochFold11_eq_bilinear) unfolds through it. Structural vanishing for difference masks (1,2) and (2,1) on axis-TT loads is stated per slot via this term. Certificate algebra at the special wave vector $m^\star=(\pi/2,\pi/2,\pi/2,0)$ evaluates each slot to $(N_1+N_2\sqrt{2})/8$, then matches geometric values to Nat-kind tables (transportedSlotTerm_axis_waveStar, transportedSlotTerm_gauge_waveStar), closing the fold values $-3$ (axis) and $-4+4\sqrt{2}$ (gauge). In the QG campaign this is the per-hinge brick for the (1,1) orbit fold; it does not itself flip gap-action recovery or prove continuum EH convergence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.