complement_orbit_deficit_kernels
plain-language theorem explainer
Complement hinge-orbit pairs share identical deficit kernels: type (2,1) equals (1,2) and type (3,1) equals (1,3), pointwise on all 15 edge slots. Cited when collapsing the six S4 hinge types to the four S4+complement orbits in the factorized Regge–Bloch fold. Proof is pure definitional equality (two reflexivity steps).
Claim. For every edge-slot index $d\in\{0,\ldots,14\}$, the orbit deficit kernel of hinge type $(2,1)$ equals that of type $(1,2)$, and the orbit deficit kernel of type $(3,1)$ equals that of type $(1,3)$.
background
This module builds the generic orbit-indexed Regge 4D Bloch fold over the six S4 hinge types $(1,1)$, $(1,2)$, $(2,1)$, $(1,3)$, $(3,1)$, $(2,2)$. Under the S4+complement action those six collapse to four orbits, so kernels on complement pairs must agree.
The assembly layer defines an orbit-indexed deficit kernel map sending each hinge orbit type to a function $\mathrm{Fin},15\to\mathbb{R}$ (one real per edge slot of the star). Types $(2,1)$ and $(3,1)$ are wired by identity transport to the committed $(1,2)$ and $(1,3)$ star-class kernels respectively; the assembly already records the pointwise equalities as reflexivity lemmas.
The fold consumes those kernels together with committed Heron area covectors. Scope is factorized (orbit-constant) kernels only; it does not replace the transported $(1,1)$ fold elsewhere in the stack.
proof idea
Split the conjunction with constructor. Each conjunct is intro d; rfl: after unfolding the orbit-indexed deficit-kernel map, the $(2,1)$ branch is definitionally the $(1,2)$ star-class kernel, and the $(3,1)$ branch is definitionally the $(1,3)$ star-class kernel (identity transport in the assembly). No algebraic rewriting is required.
why it matters
The module header lists complement kernel identities among the binding THEOREM tags for the all-orbit factorized Bloch fold and $m^2$ moment. Without pointwise agreement on complement pairs, the six hinge types cannot be merged into the four S4+complement orbits that index the factorized fold and the cosine two-jet formal coefficient.
No downstream consumer is wired yet in the graph; sibling factorized-fold definitions are the natural landing site. The result stays inside discrete Regge calculus on the committed star kernels. It does not touch continuum Einstein–Hilbert recovery, does not flip gap_action_recovery, and does not address the still-open arbitrary-direction cosine two-jet Tendsto goals flagged in the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.