flatHessianOrbitForm
plain-language theorem explainer
Defines the flat second-variation class form on one 4D hinge orbit: a double sum over the 15 edge classes of area weight times deficit kernel times edge variations. Anyone assembling the 4D Regge flat Hessian from open per-hinge kernels cites this skeleton. The body is a pure definition, the bilinear contraction itself.
Claim. Given area/hinge-volume weights $A:\{0,\ldots,14\}\to\mathbb{R}$, a deficit-gradient kernel $K$ on pairs of the fifteen edge classes, and an edge-length variation $c$, the flat Hessian orbit form is $\sum_{e,f} A_e\, K_{ef}\, c_e\, c_f$.
background
This module is the next kernel-checked increment after the 15-class 4D edge stencil. It enumerates the Freudenthal/Kuhn triangulation of the 4-cube (24 monotone 4-simplices), isolates a seed hinge orbit (triangle on masks 0,1,3), and records combinatorial incidence multiplicities of each edge class in the two seed simplices that contain that hinge.
The form here is the MODEL layer of that campaign: the 4D skeleton of the 3D Schläfli-reduced contraction $-\sum_\tau\sum_f L'\cdot\theta'$. The map $A$ stands in for area (hinge-volume) first derivatives; $K$ stands in for the outer product of deficit gradients. Both are left OPEN; only the contraction shape is fixed.
The fifteen indices are the edge classes of the imported stencil, never redefined here. Off-support classes are handled downstream by incidence cutoffs, not inside this bare sum.
proof idea
Pure definition: the value is the double finite sum $\sum_e\sum_f A_e K_{ef} c_e c_f$ over Fin 15. No lemmas, no tactics, no reduction.
why it matters
Parent of the cell-local seed-orbit assembly, which multiplies $A$ by the combinatorial incidence multiplicities before calling this form, hard-wiring that off-support classes cannot contribute. That assembly is what the decoy-area annihilation theorem and the support-projection theorem quantify: a bump on a decoy class is killed, and the form depends on $c$ only through supported classes.
In the QG full-theory campaign this is deliverable B's assembly skeleton. It does not evaluate dihedral or Cayley–Menger kernels, does not finish the flat Hessian of the 4D Regge action, and does not touch $S_{\mathrm{RS}}\to\mathrm{EH}_{4d}$ or gap-action recovery. It only freezes the bilinear shape so incidence theorems can talk about support cleanly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.