hinge4DStarKernel12Status_flags
plain-language theorem explainer
The type-(1,2) Regge 4D star-kernel status record reports three gates closed (star enumeration, flatness, full-star class kernel), three scopes still open (type-(2,1) complement, other hinge orbits, flat Hessian assembly), and both EH4d convergence and gap-action recovery false. Gravity auditors cite it as the machine-checked ledger of what this kernel increment actually finished. Proof is a single `decide` on concrete Boolean fields.
Claim. The status record for the 4D Regge type-$(1,2)$ periodic-lattice star kernel satisfies: star enumeration closed, flatness gate closed, and full-star class kernel closed all equal $\mathrm{true}$; type-$(2,1)$ complement orbit open, other hinge orbits open, and flat Hessian assembly open all equal $\mathrm{true}$; Einstein–Hilbert 4D convergence and gap-action recovery both equal $\mathrm{false}$.
background
This module is the next kernel-checked increment in the QG full-theory campaign after the type-$(1,1)$ seed orbit. It treats the type-$(1,2)$ triangle hinge ${0,e_0,e_0+e_1+e_2}$ (masks $0,1,7$; difference masks $(1,6)$) and its full periodic Freudenthal star in the integer lattice: two containing unit cubes and four incident 4-simplices. It imports the Freudenthal incidence layer, the 15-class edge stencil, and the committed Gram-projection / cleared-denominator cosine calculus without redefining their API.
Deliverables already proved in the module include exact star enumeration (four cube-translate / Kuhn-simplex pairs), a flat cosine multiset of all zeros recomputed from each orbit's Gram vector, the flatness gate (star angle sum $4\cdot\arccos 0=2\pi$), and the full-star deficit class kernel on all 15 stencil classes with values $\pm\sqrt{2}/2$. The status structure packages which of those gates are closed versus deliberately left open.
The upstream definition hinge4DStarKernel12Status is the concrete record value whose Boolean fields this theorem inspects.
proof idea
One-line decidability proof. The status is a concrete structure literal with Boolean fields; decide discharges the eight-way conjunction of field equalities by computation. No lemmas beyond the definition of the status record are required.
why it matters
In the Recognition Science gravity stack this is the audited ledger for the type-$(1,2)$ full-star deficit class kernel: it freezes, in a proved theorem, exactly which gates the module closed and which campaign goals remain open. Downstream consumers (none yet wired in the graph) can pattern-match on these flags rather than re-reading the module narrative.
The module doc binds the open flags to the campaign roadmap: the complement-related type-$(2,1)$ orbit is not transported here; other hinge orbits stay open; flat Hessian assembly over all hinges is unfinished; $S_{\mathrm{RS}}$ convergence to Einstein–Hilbert in 4D is not claimed; and gap-action recovery is not flipped. The theorem makes those non-claims machine-checkable rather than prose-only.
It sits inside the Regge discretization path toward continuum gravity, after the type-$(1,1)$ kernel and before full Hessian assembly. No forcing-chain landmark (T0–T8) is directly touched; the link is the broader discrete-to-continuum gravity program.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.