blochFoldOrbitMeanLocal
plain-language theorem explainer
Defines the Bloch fold of the mean-local Path B kernel on one hinge-orbit class: sum of local slot terms over the 24×10 discrete slot lattice. Gravity analysts cite it when comparing vacuous mean-local incidence to the distinct-hinge fold. The body is a plain double sum of the per-slot mean-local product.
Claim. For a hinge-orbit type $\mathrm{ty}$, a $4\times 4$ real matrix $H$, and a mass/momentum weight $m:\{0,1,2,3\}\to\mathbb{R}$, the mean-local Bloch fold on that orbit is $$\sum_{s=0}^{23}\sum_{t=0}^{9} \tau_{\mathrm{ty}}(H,m;s,t),$$ where $\tau_{\mathrm{ty}}$ is the mean-local slot term (phased class-dot of area covector times mean-local kernel when $(s,t)$ lies in the orbit, else zero).
background
Module Path B builds 3D-style local-incidence kernels in a 4D continuum Regge–Bloch setting. Layer 1 is the vacuous mean-local construction: at each slot one takes $K_{\mathrm{local}}=K_{\star}/r_\tau$, so the fold equals the distinct-hinge Path A object by linearity of class-dot and pushforward. Layer 2 (position-resolved) is non-vacuous and is not this definition.
HingeOrbitType indexes the six lattice orbits under coordinate permutation (t11, t12, t21, t13, t31, …). Mat4 is the space of real $4\times 4$ matrices. The summand meanLocalSlotTerm returns the product of two phased class-dots—one on the slot orbit area covector, one on the mean-local kernel—when the discrete indices $(s,t)\in\mathrm{Fin},24\times\mathrm{Fin},10$ belong to the orbit, and zero otherwise.
Upstream cost algebra supplies the shifted cost $H(x)=J(x)+1=\tfrac12(x+x^{-1})$ (d'Alembert form of the Recognition Composition Law); here the symbol $H$ is instead the matrix argument of the Bloch fold, not that scalar cost.
proof idea
Definitional, not a proof. The body is the double finite sum $\sum_s\sum_t$ of meanLocalSlotTerm ty H m s t over $s:\mathrm{Fin},24$ and $t:\mathrm{Fin},10$. No lemmas are applied at the definition site; scaling identities are proved downstream by unfolding and rewriting with meanLocalSlotTerm_eq_scaled.
why it matters
This is the per-orbit building block of vacuous Path B. Downstream, blochFoldAllMeanLocal sums it over all HingeOrbitType values and is documented as the full vacuous Path B fold (equal to distinct-hinge). The companion theorem blochFoldOrbitMeanLocal_eq_scaled identifies the definition with $(\mathrm{orbitStarSize},\mathrm{ty})^{-1}$ times the ordinary orbit Bloch fold, closing the mean-local versus full-star comparison on one orbit.
In the missing-factor blocker program, Path B tests whether local-incidence kernels recover Einstein–Hilbert structure on TT rays. Measured receipts show position-resolved t11 agrees with distinct-hinge on tested rays, while t12 breaks symbolDir plus/cross agreement and misses EH $-1/4$; this mean-local fold is the linear baseline those probes compare against. It does not itself touch T5–T8 forcing or the mass ladder; it is gravity-analysis scaffolding inside the 4D Regge–Bloch hinge calculus.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.