Hinge4DStarKernelStatus
plain-language theorem explainer
Status record for the 4D Regge seed-hinge star kernel campaign: seven booleans marking which subgoals are closed versus still open. Gravity and discrete-QG workers cite it as the single source of truth for campaign progress after the dihedral kernel. It is a plain structure definition; the concrete assignment lives in the companion value `hinge4DStarKernelStatus`.
Claim. A record type with seven boolean fields: whether star enumeration is closed; whether the flatness gate (star angle sum $= 2\pi$) is closed; whether the full-star deficit class kernel on classes $(2,3,6,7,10,11,14)$ is closed; whether other hinge orbits remain open; whether flat Hessian assembly remains open; whether $S_{\mathrm{RS}}$ convergence to Einstein–Hilbert in 4D is claimed; and whether gap-action recovery is claimed.
background
The ambient module is the next kernel-checked increment in the 4D Regge full-theory campaign, after the two-simplex dihedral cosine kernel. It works on 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. The Freudenthal incidence layer, the 15-class edge stencil, and the seed dihedral cosine calculus are imported, never redefined.
Deliverable A of the module proves: exact six-pair star enumeration; the flat cosine multiset (four simplices at $1/\sqrt{2}$, two at $0$); the flatness gate (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.
This structure does not itself prove those facts. It only packages the closed/open flags that the campaign uses to report which of those gates, and which larger open goals (other orbits, Hessian assembly, EH convergence, gap-action recovery), have been discharged.
proof idea
No proof: this is a structure declaration with seven Bool fields and no constructors beyond the default. Semantic content is supplied by the companion definition that instantiates every field. Downstream code pattern-matches or projects the booleans rather than re-deriving status.
why it matters
In the Recognition Science gravity stack this record is the campaign dashboard for the 4D Regge star kernel. The module doc binds the tier tags: THEOREM-grade kernel checks only, no sorry, no new axioms, expected footprint [propext, Classical.choice, Quot.sound]. The companion value sets star enumeration, flatness gate, and full-star class kernel to closed, and leaves other hinge orbits, flat Hessian assembly, EH4d convergence, and gap-action recovery open, matching the explicit non-claims in the module header.
Parent use is the single definition that materializes the status. That status is what later assembly lemmas and paper-facing summaries read when they assert that the seed-hinge star is kernel-checked while the global Hessian and $S_{\mathrm{RS}}\to\mathrm{EH}_{4d}$ steps remain future work. It does not reverse-engineer continuum weights from Einstein–Hilbert; it only records which discrete gates have closed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.