m2MeanLocalOrbitSlotCoeff
plain-language theorem explainer
Per-slot coefficient of the mean-local m² moment on a fixed hinge-orbit type in the 4D Regge–Bloch Path B analysis. Nonzero only when the (slot, triangle) pair lies on that orbit; then it is the product of the orbit area-covariance class-dot with a −1/2 phase-weighted mean-local kernel class-dot. Gravity analysts cite it when assembling orbit moments or comparing mean-local Path B to transported Path A. The body is a pure piecewise formula, not a proof.
Claim. For a hinge-orbit type $\mathrm{ty}$, a $4\times 4$ real matrix $H$, a ray direction $\mathrm{dir}\in\mathbb{R}^4$, and indices $(s,t)\in\{0,\ldots,23\}\times\{0,\ldots,9\}$, the mean-local $m^2$ slot coefficient equals zero unless $(s,t)$ belongs to orbit $\mathrm{ty}$. On-orbit it is $\bigl(\sum_{d=0}^{14} A^{\mathrm{cov}}_{\mathrm{ty},s,t}(d)\,c_H(d)\bigr)\cdot\bigl(-\tfrac12\sum_{d=0}^{14} K^{\mathrm{ml}}_{\mathrm{ty},s,t}(d)\,c_H(d)\,\phi_{\mathrm{dir}}(b_{s,t},d)^2\bigr)$, where $A^{\mathrm{cov}}$ is the slot-orbit area covariance, $K^{\mathrm{ml}}$ the mean-local kernel, $c_H$ the edge-class coefficients of $H$, $\phi_{\mathrm{dir}}$ the midpoint phase scale, and $b_{s,t}$ the hinge base point.
background
Module Path B builds 3D-style local-incidence kernels in the 4D continuum as a missing-factor blocker. Layer 1 is vacuous mean-local: at each slot one takes $K_{\mathrm{local}}=K_{\star}/r_\tau$, which equals Path A distinct-hinge by linearity of class-dot and pushforward. Layer 2 is position-resolved and non-vacuous; measured receipts show t11 agreement on TT rays but t12 breaks symbolDir plus/cross and misses EH $-1/4$.
This definition sits in §2 (mean-local $m^2$). Mat4 is just $4\times 4$ real matrices. Membership isOrbit ty s t means the hinge orbit type of slot $s$ and triangle $t$ equals $\mathrm{ty}$. The mean-local kernel slotOrbitMeanLocalKer is the transported orbit-mean local kernel under the orbit covering permutation. phaseScaleDir is the midpoint phase linear in the ray parameter: $\sum_i \mathrm{dir}_i x_i$ plus half the class-displacement term. hingeBase is the masked coordinate of the first triangle-vertex mask.
Upstream area covariance slotOrbitAreaCov and edge-class coefficients classCoeff supply the two class-dots that multiply. The shifted cost $H=J+1$ appears only as ambient CostAlgebra notation, not inside this formula.
proof idea
Definitional, not a proved statement. The body is a single if isOrbit ty s t then ... else 0. On the true branch it multiplies two real sums over the 15 edge classes: the area-covariance class-dot of $H$, times $-1/2$ times the mean-local-kernel class-dot weighted by the squared midpoint phase scale at the hinge base. Off-orbit the coefficient is identically zero. No lemmas are applied; later theorems rewrite this formula by unfolding and scaling.
why it matters
Feeds the orbit-level mean-local $m^2$ moment m2MeanLocalOrbitMoment, which sums the coefficient over all 24 slots and 10 triangles. Also the direct subject of m2MeanLocalOrbitSlotCoeff_eq_scaled, which identifies it with $(\mathrm{orbitStarSize},\mathrm{ty})^{-1}$ times the transported-orbit slot coefficient, closing the vacuous Path B equals distinct-hinge comparison at the $m^2$ layer.
In the broader RS gravity stack this is bookkeeping for the Regge–Bloch continuum symbol on 4D hinges: mean-local Path B is the linearity shortcut that should match Path A before any non-vacuous position-resolved correction is trusted. The module receipt already flags that position-resolved t12 fails EH $-1/4$ and symbolDir agreement, so this mean-local coefficient is the clean baseline against which that failure is measured. It does not itself touch T5–T8 forcing, RCL, or the $\phi$-ladder mass formula; it is continuum-kernel algebra inside the gravity analysis layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.