meanLocalSlotTerm
plain-language theorem explainer
Per-slot contribution to the Path B mean-local Bloch fold for a fixed hinge-orbit type: the product of two phased class-dots (orbit area-covariance times mean-local kernel) at the hinge base, or zero off-orbit. Gravity analysts cite it when assembling the vacuous mean-local fold that should match distinct-hinge by linearity. Construction is a pure case split on orbit membership.
Claim. Fix a hinge-orbit type $\tau$, a $4\times 4$ real matrix $H$, a mode $m:\mathbb{R}^4$, a slot $s\in\{0,\ldots,23\}$ and a triangle index $t\in\{0,\ldots,9\}$. The mean-local slot term equals the product of the phased class-dot of the slot-orbit area covariance with the phased class-dot of the slot-orbit mean-local kernel, both evaluated at the hinge base, when $(s,t)$ belongs to orbit $\tau$; otherwise it is $0$.
background
This module develops Path B local-incidence kernels for the 4D continuum Regge–Bloch analysis. Layer 1 is the vacuous mean-local construction: at each slot one takes $K_{\mathrm{local}}=K_\star/r_\tau$, which by linearity of class-dot and pushforward should reproduce the Path A distinct-hinge fold. Layer 2 (position-resolved) is non-vacuous and is not what this definition encodes.
A hinge base is the coordinate mask of the first triangle-vertex mask at $(s,t)$. The phased class-dot contracts a 15-component symbol vector against plane-wave class perturbations of $H$ at mode $m$ and base point $x$. Orbit membership isOrbit is equality of the classified hinge-orbit type with $\tau$. The slot-orbit mean-local kernel is the transported orbit-mean local kernel at the covering permutation for $(s,t)$; the area covariance is the companion transported area symbol.
The ambient cost algebra uses the shifted cost $H(x)=J(x)+1=\tfrac12(x+x^{-1})$, under which the Recognition Composition Law becomes the d'Alembert identity, but that structure is only ambient here: the definition is purely kinematic on the 4D hinge lattice.
proof idea
Definition by cases, not a proof. If $(s,t)$ lies in orbit type $\tau$, return the product of two phasedClassDot evaluations at hingeBase s t: one against slotOrbitAreaCov ty s t, one against slotOrbitMeanLocalKer ty s t. Otherwise return $0$. No lemmas are applied; the body is the construction itself.
why it matters
This is the atomic summand of the Path B vacuous mean-local fold. Downstream, blochFoldOrbitMeanLocal sums it over all $24\times 10$ slot–triangle pairs to produce the orbit-level mean-local Bloch fold. The companion identity meanLocalSlotTerm_eq_scaled rewrites it as $(\mathrm{orbitStarSize},\tau)^{-1}$ times the transported orbit slot term, which is the algebraic content of "$K_{\mathrm{local}}=K_\star/r_\tau$".
In the missing-factor blocker program this closes the definitional half of Path B layer 1. Measured Python receipts already report that position-resolved t11 agrees with distinct-hinge on tested TT rays, while t12 breaks symbolDir agreement and misses the EH $-1/4$ target. The definition itself does not touch T0–T8 or the mass ladder; it sits inside the 4D Regge gravity analysis that must eventually feed continuum curvature matching.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.