hinge4DStarKernelStatus_flags
plain-language theorem explainer
Status snapshot for the 4D Regge full-star hinge kernel: star enumeration, flatness gate, and full-star class kernel are closed; other hinge orbits and flat Hessian assembly remain open; EH4d convergence and gap-action recovery stay false. Gravity/Regge auditors cite it as the machine-checked campaign ledger for this kernel increment. Proof is a single `decide` on the concrete status record.
Claim. The 4D star-hinge kernel status record satisfies: star enumeration closed $=\mathsf{true}$, flatness gate closed $=\mathsf{true}$, full-star class kernel closed $=\mathsf{true}$, other hinge orbits open $=\mathsf{true}$, flat Hessian assembly open $=\mathsf{true}$, converges to Einstein–Hilbert in 4D $=\mathsf{false}$, and gap-action recovery $=\mathsf{false}$.
background
This module is the next kernel-checked increment in the QG full-theory campaign after the dihedral cosine kernel. Scope is the seed triangle hinge ${0,e_0,e_0+e_1}$ and its full periodic Freudenthal star in the integer lattice: four containing unit cubes and six incident 4-simplices. It imports the Freudenthal incidence layer, the 15-class edge stencil, and the seed two-simplex dihedral cosine calculus without redefining their APIs.
Deliverables already proved in-module include exact star enumeration (six cube-translate/Kuhn-simplex pairs), the flat cosine multiset (four simplices at $1/\sqrt{2}$, two at $0$), the flatness gate (star angle sum exactly $2\pi$), and the full-star deficit class kernel on classes $(2,3,6,7,10,11,14)$ with values $(-1,-1,+1,-1,+1,+1,-1)$, plus nonvacuity, swap-$2\leftrightarrow 3$ symmetry, uniform-scaling decoy, and homothety stationarity gates.
The status structure hinge4DStarKernelStatus is the concrete ledger of those closures and of the deliberately open items named in the module tier tags.
proof idea
One-line decidability proof. The status record is a structure of Boolean fields with literal true/false assignments (star enumeration, flatness gate, and full-star class kernel closed; other orbits and flat Hessian assembly open; EH4d convergence and gap-action recovery false). decide discharges the seven-way conjunction by computation on those literals. No lemmas beyond the status definition are required.
why it matters
Campaign bookkeeping, not a geometric theorem. It freezes, in a single proved conjunction, which parts of the 4D Regge star-hinge program are kernel-closed versus intentionally open, matching the module tier tags: other hinge orbits of the lattice remain open; flat Hessian assembly over all hinges is not completed; $S_{\mathrm{RS}}$ convergence to Einstein–Hilbert in 4D is not claimed; gap-action recovery is not flipped; weights are not reverse-engineered from EH.
Downstream use is empty in the graph today; the declaration exists so auditors and later assembly theorems can quote a single named fact rather than re-reading the status record. In the broader Recognition gravity stack it marks progress on the discrete curvature side that must eventually feed continuum matching, without pretending that matching is done.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.