kernel21_eq_kernel12
plain-language theorem explainer
On the fifteen edge classes of the 4D Regge hinge, the type-(2,1) star-class deficit kernel equals the committed type-(1,2) kernel pointwise. Hessian assemblers cite this when folding S4 orbit types into the zero-momentum second variation. The proof is definitional reflexivity: the (2,1) kernel is literally defined to be the (1,2) kernel via complement transport.
Claim. For every edge-class index $d \in \{0,\ldots,14\}$, the type-$(2,1)$ star-class kernel at $d$ equals the committed type-$(1,2)$ full star-class kernel at $d$.
background
The module assembles the flat second-variation class quadratic of the 4D Regge action from committed per-orbit star deficit kernels and Heron area gradients, at zero momentum (constant edge-class perturbation). Edge classes live on Fin 15. Six $S_4$ orbit types appear, with orbit counts $72/48/48/24/24/24$.
Vertex complement $m \mapsto m \oplus 15$ preserves difference masks, so edge-class indices are invariant under that transport. Consequently the type-$(2,1)$ star kernel is identified with the already-committed type-$(1,2)$ kernel (and likewise $(3,1)$ with $(1,3)$). The local definition of the type-$(2,1)$ kernel is exactly that committed $(1,2)$ map.
Upstream, ReggeHinge4DStarKernel12.fullStarClassKernel supplies the explicit real values on the fifteen classes (nonzero entries involve $\pm\sqrt{2}/2$ on low indices). Sibling kernels cover the other orbit types.
proof idea
One-line definitional equality. The type-$(2,1)$ kernel is defined by
kernel21 := ReggeHinge4DStarKernel12.fullStarClassKernel,
so pointwise equality on every $d : \mathrm{Fin},15$ is rfl. No algebraic rewriting or case split is required.
why it matters
Fills deliverable A.2 of the Regge flat Hessian assembly: complement transport is the identity on edge classes, so type-$(2,1)$ may reuse the committed $(1,2)$ star kernel without a separate geometric computation. That reuse is a prerequisite for the orbit-count-weighted zero-momentum true-weight Hessian (sum of $(dA\cdot c)(d\delta\cdot c)$ over the six $S_4$ types) and for the later evaluations that kill pure gauge on decoyGauge and related modes.
No downstream consumers are wired yet in the graph. The module explicitly does not claim continuum Einstein–Hilbert recovery, gap-action recovery, or finite-momentum Bloch folding; those remain open. Within Recognition gravity analysis this is bookkeeping that keeps the Hessian assembly on committed geometry rather than reverse-engineered weights.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.