hinge4DStarKernel13Status
plain-language theorem explainer
Status record for the type-(1,3) 4D Regge hinge star-deficit kernel on the periodic Freudenthal lattice. It marks star enumeration, the flatness gate, and the full-star class kernel as closed, leaves type-(3,1) transport and flat Hessian assembly open, and records that neither Einstein–Hilbert 4D convergence nor gap-action recovery is claimed. Downstream flag lemmas cite it as the single source of truth for campaign progress. The body is a pure structure literal of booleans.
Claim. The type-$(1,3)$ star-kernel status table asserts: star enumeration closed, flatness gate closed, full-star class kernel closed; type-$(3,1)$ transport open, flat Hessian assembly open; $S_{\mathrm{RS}}\to\mathrm{EH}_{4d}$ convergence false; gap-action recovery false.
background
This module is the next kernel-checked increment in the 4D Regge QG campaign after the type-$(1,1)$ seed orbit and the orbit-classification layer. The hinge under study is the type-$(1,3)$ triangle with absolute masks ${0,e_0,e_0+e_1+e_2+e_3}={0,1,15}$ (difference masks $(1,14)$, local flat squared lengths $(1,3,4)$) and its full periodic Freudenthal star.
The status structure packages seven boolean campaign flags: three closed deliverables (star enumeration of the six Kuhn simplices, flat cosine multiset giving angle sum $2\pi$, and the full-star deficit class kernel on classes $(1,3,5,7,9,11,13)$), two explicitly open items (transport to the complementary type-$(3,1)$ by mask complement, and flat Hessian assembly over all hinges), and two non-claims (convergence of the RS action to Einstein–Hilbert in 4D, and gap-action recovery).
Upstream imports supply the dihedral and flat kernels plus the 15-class edge stencil; this definition never redefines those APIs.
proof idea
Pure definition: a structure literal that assigns the seven boolean fields of Hinge4DStarKernel13Status to the constants true/false listed in the body. No tactics, no lemmas, no computation. The companion theorem hinge4DStarKernel13Status_flags simply unfolds these field projections and conjoins them.
why it matters
Gives a single machine-checked dashboard for the type-$(1,3)$ star-kernel deliverable inside the Gravity analysis stack. Downstream, hinge4DStarKernel13Status_flags re-exports the closed/open split so later modules can gate on the three closed items without re-auditing the kernel proofs.
In the campaign narrative this sits after the type-$(1,1)$ star kernel and the orbit classification: it records that the six-simplex star, the $6\cdot\arccos(1/2)=2\pi$ flatness gate, and the signed $\pm\sqrt{3}$ class kernel on seven stencil classes are done, while type-$(3,1)$ transport, full flat Hessian assembly, $S_{\mathrm{RS}}\to\mathrm{EH}_{4d}$, and gap-action recovery remain out of scope. It does not itself advance the forcing chain (T0–T8) or the Recognition Composition Law; it is bookkeeping for the discrete-gravity side of the RS program.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.