orbitMeanLocalKernel
plain-language theorem explainer
For each hinge orbit type, the mean-local deficit kernel is the full-star seed kernel scaled by the inverse geometric star size r_τ. Gravity analysts cite it as the vacuous Path-B local-incidence kernel K_local = K_star / r_τ on the 15-class space. The body is a one-line pointwise scalar multiple of the orbit seed kernel.
Claim. For each lattice hinge orbit type $\tau$, define the mean-local deficit kernel $K_{\mathrm{local}}(\tau):\{0,\ldots,14\}\to\mathbb{R}$ by $K_{\mathrm{local}}(\tau)(d)=r_\tau^{-1}\,K_{\mathrm{star}}(\tau)(d)$, where $r_\tau$ is the geometric star size of $\tau$ and $K_{\mathrm{star}}(\tau)$ is the seed full-star class kernel of $\tau$.
background
This module develops Path B for 4D continuum Regge–Bloch gravity: 3D-style local-incidence kernels meant to close a missing-factor blocker. Layer 1 is mean-local and intentionally vacuous: at each slot one sets $K_{\mathrm{local}}=K_{\mathrm{star}}/r_\tau$. By linearity of class-dot and pushforward this equals the Path A distinct-hinge construction. Layer 2 is the non-vacuous position-resolved expansion of the star over cube-translate bases.
Hinge orbit types are the six lattice classes under coordinate permutation (here the inductive cases t11, t12, t21, t13, t31). The geometric star size $r_\tau$ is the paper-table count of star members: 6 for (1,1), (1,3), (3,1) and 4 for (1,2), (2,1). The seed kernel is the assembly commitment of the full-star class kernel for that orbit (t11 uses the standard full-star class kernel, other types their specialized kernels).
The codomain is a real 15-vector of class components, the same Fin-15 class space used throughout the Regge hinge star modules.
proof idea
Pure definition: pointwise, invert the orbit star size and multiply the orbit seed kernel. No lemmas, no tactics. Downstream equalities (e.g. multiplying back by $r_\tau$ recovers the seed) are proved separately by unfolding and field simplification with the nonzero star-size fact.
why it matters
This is the Layer-1 mean-local kernel that Path B hangs on. Downstream it specializes at t11 to $(1/6)$ times the full-star class kernel, equates that to the assembled mean, and supplies the smul identity $r_\tau,K_{\mathrm{local}}=K_{\mathrm{star}}$. It is pushforwarded to transported orbit mean-local kernels, then to slot-level mean-local kernels, which scale the slot orbit deficit kernels by $r_\tau^{-1}$. Those feed the Bloch-fold orbit-mean-local constructions in the same module.
In the broader RS gravity stack this is analysis scaffolding for 4D Regge–Bloch continuum matching, not a forcing-chain (T0–T8) step. Python receipts report position-resolved t11 agreeing with distinct-hinge on tested TT rays, while t12 breaks symbolDir plus/cross agreement and misses the EH $-1/4$ target; no gap_action_recovery flip. The definition itself is the shared scale factor those comparisons rest on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.