hinge4DStarKernel22Status_flags
plain-language theorem explainer
The type-(2,2) Regge 4D hinge star-kernel status record is certified: star enumeration, flatness gate, and full-star class kernel are closed; other hinge orbits and flat Hessian assembly stay open; EH4d convergence and gap-action recovery are false. Gravity analysts in the QG full-theory campaign cite this as the machine-checked flag snapshot for the (2,2) orbit. Proof is a single decidability check on the concrete status structure.
Claim. The status record for the type-$(2,2)$ four-dimensional Regge hinge star kernel asserts that star enumeration, the flatness gate, and the full-star class kernel are closed, that other hinge orbits and flat Hessian assembly remain open, and that both Einstein–Hilbert four-dimensional convergence and gap-action recovery evaluate to 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-(2,2) triangle hinge on the periodic Freudenthal lattice, with vertex masks ${0,3,15}$ and difference masks $(3,12)$, together with its full star of incident Kuhn simplices. The API for incidence, the 15-class edge stencil, and Gram-projection cosines is imported, never redefined.
Deliverable A packages five positive gates (star enumeration of exactly four cube-translate/simplex pairs, flat cosine multiset all zero, star angle sum exactly $2\pi$, full-star deficit class kernel on all 15 stencil classes, plus nonvacuity and symmetry gates) and three explicit non-claims (other orbits open, flat Hessian assembly open, no EH4d convergence or gap-action recovery).
The upstream status definition hard-codes those seven booleans. The present theorem only certifies that the record really carries the advertised values.
proof idea
One-line decidability proof. The tactic decide evaluates the seven boolean field equalities against the concrete status structure and discharges the conjunction. No lemmas are invoked beyond the decidable equality instance on Bool.
why it matters
This is the machine-checked flag snapshot that freezes deliverable A of the type-(2,2) star kernel. Downstream consumers (none yet recorded) can pattern-match on the closed gates without re-running the enumeration or flatness arithmetic. In the broader Recognition gravity stack it advances the discrete Regge side of the continuum limit program, while the module doc explicitly keeps three campaign-level questions open: full flat Hessian assembly over all hinge orbits, $S_{\mathrm{RS}}$ convergence to Einstein–Hilbert in 4d, and gap-action recovery. Those remain false or open flags, so the theorem also serves as a non-regression guard against accidental over-claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.