hinge4DFlatKernelStatus_flags
plain-language theorem explainer
Status board for the 4D Regge hinge flat-kernel increment: Freudenthal 24-simplex enumeration and seed-hinge incidence are closed; true per-hinge deficit kernels remain open; neither EH 4D convergence nor gap-action recovery is claimed. Gravity auditors cite it as the honest gate record for deliverable B after the 15-class edge stencil. Proof is a one-line decidability check on the status structure.
Claim. The 4D hinge flat-kernel status record asserts: Freudenthal/Kuhn 24-simplex enumeration is complete; seed-hinge incidence is closed; the true per-hinge deficit kernels remain open; convergence of the Regge action to the 4D Einstein–Hilbert action is not established; and gap-action recovery is not established.
background
This module is the next kernel-checked increment in the QG full-theory campaign after the 15-class Regge edge stencil in 4D. It treats the Freudenthal/Kuhn triangulation of the 4-cube: 24 monotone 4-simplices (axis permutations), each with five nested vertices and ten edge-class masks drawn from the imported 15-class stencil.
The seed hinge is the triangle on vertices $0$, $e_0$, $e_0+e_1$ (masks $0,1,3$). Exactly two of the 24 simplices contain it. Incidence multiplicities over the 15 edge classes are computed combinatorially: three classes are absent (decoys); the three hinge-boundary classes each have multiplicity 2. The flat-Hessian assembly formula is MODEL only: it contracts open per-hinge area weights against open per-hinge deficit kernels and forces vanishing off the incidence support.
The upstream status definition hard-codes the five boolean gates that this theorem reifies: enumeration and incidence closed; true deficit kernels open; EH4d convergence and gap-action recovery both false.
proof idea
One-line wrapper: decide on the five concrete Boolean fields of the status structure. No algebraic lemmas are invoked; the values are definitional literals in the upstream status record, so decidable equality closes the conjunction immediately.
why it matters
In the Recognition gravity stack this is the honest gateboard for deliverable B (combinatorial support of the 4D hinge flat kernel). The module doc binds the tier tags: THEOREM for named combinatorial facts, MODEL for the assembly skeleton, OPEN for the true dihedral/Cayley–Menger deficit kernels. It explicitly does not complete the flat Hessian of the 4D Regge action, does not prove $S_{\mathrm{RS}}$ converges to EH in 4D, and does not flip gap-action recovery.
No downstream consumers are wired yet (used_by empty). The record exists so later kernel-checked increments can flip flags only when the corresponding OPEN items (true deficit kernels, EH4d limit, gap-action recovery) are discharged, preventing silent overclaim in the QG campaign.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.