kernel31_eq_kernel13
plain-language theorem explainer
Pointwise, the type-(3,1) star-class deficit kernel on the 15 edge classes equals the committed type-(1,3) kernel. Hessian assemblers cite this to reuse the (1,3) table for the complementary S4 orbit under vertex complement. The proof is definitional reflexivity: the (3,1) kernel is defined as that committed map.
Claim. For every edge-class index $d \in \{0,\ldots,14\}$, the type-$(3,1)$ star-class kernel evaluated at $d$ equals the committed type-$(1,3)$ full-star-class kernel at $d$.
background
This module assembles the zero-momentum per-cell Hessian of the 4D Regge action from committed per-orbit star deficit kernels and Heron area gradients, replacing the provisional weight-1 aggregate. Edge classes live on Fin 15 (nonzero difference masks of the 4-cube vertex set). Each S4 orbit type has a committed full-star-class kernel: a sparse map Fin 15 → ℝ recording deficit response on those classes.
Vertex complement $m \mapsto m \oplus 15$ preserves difference masks, so edge-class indices are invariant. The module therefore treats type $(3,1)$ as identity-transported from the committed type-$(1,3)$ kernel (and likewise $(2,1)$ from $(1,2)$). The local definition of the $(3,1)$ kernel is exactly that committed $(1,3)$ map; the present theorem records the equality on every class index.
Upstream, ReggeHinge4DStarKernel13.fullStarClassKernel supplies the concrete values (nonzero only on a few classes, with coefficients $\pm\sqrt{3}$).
proof idea
One-line definitional equality. The local kernel31 is defined by := ReggeHinge4DStarKernel13.fullStarClassKernel, so kernel31 d = fullStarClassKernel d holds by rfl for every d : Fin 15. No algebraic rewriting or case split is required.
why it matters
Fills item 2 of deliverable A in the module campaign: complement transport is identity on edge classes, so type-$(3,1)$ may reuse the committed $(1,3)$ star kernel. That reuse is required before the orbit-count-weighted sum (counts $72/48/48/24/24/24$) that builds the zero-momentum true-weight Hessian quadratic and its polarization.
No downstream theorems yet cite this lemma directly (used_by is empty), but it is part of the scaffolding that lets true weights kill pure gauge on decoyGauge and decoyTrace at zero momentum (provisional weight-1 did not). Framework scope stays local to Regge discrete gravity analysis: it does not touch the T0–T8 forcing chain, RCL, or continuum EH recovery. Finite-momentum Bloch folding and S_RS_converges_EH_4d remain open per the module contract.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.