hinge4DStarKernel22Status
plain-language theorem explainer
Status record for the type-(2,2) 4D Regge triangle-hinge star kernel on the periodic Freudenthal lattice. It marks star enumeration, flatness gate, and full-star class kernel as closed, while leaving other hinge orbits, flat Hessian assembly, Einstein–Hilbert 4D convergence, and gap-action recovery open or false. Downstream flag lemmas cite it as the single source of campaign progress bits. The body is a pure structure literal with no proof work.
Claim. Define the campaign status object for the type-$(2,2)$ hinge star kernel by setting: star enumeration closed $=\mathrm{true}$, flatness gate closed $=\mathrm{true}$, full-star class kernel closed $=\mathrm{true}$, other hinge orbits open $=\mathrm{true}$, flat Hessian assembly open $=\mathrm{true}$, converges to Einstein–Hilbert in 4D $=\mathrm{false}$, gap-action recovery $=\mathrm{false}$.
background
This module is the next kernel-checked increment in the QG full-theory Regge campaign after the type-$(1,1)$ seed orbit. Scope is the type-$(2,2)$ triangle hinge ${0, e_0+e_1, e_0+e_1+e_2+e_3}$ (masks ${0,3,15}$, difference masks $(3,12)$) and its full periodic Freudenthal star. The module imports the Freudenthal incidence layer, the 15-class edge stencil, and the Gram-projection cosine calculus without redefining their APIs.
The status structure packages seven boolean campaign flags: three closed deliverables (star enumeration of the four incident simplices, flat cosine multiset with angle sum $2\pi$, and the full-star deficit class kernel on all 15 stencil classes), two deliberately open items (other hinge orbits; flat Hessian assembly over all hinges), and two false convergence claims (RS action converges to EH in 4D; gap-action recovery). Expected axiom footprint is only propext, Classical.choice, and Quot.sound.
proof idea
Pure definitional structure literal. Each field of the status record is assigned a concrete Bool constant (true or false) matching the module's tier tags: the three proved deliverables are marked closed, the two out-of-scope items remain open, and the two non-claims stay false. No tactics, no lemmas, no computation.
why it matters
Serves as the single machine-readable progress dashboard for the type-$(2,2)$ star-kernel increment. The immediate consumer is the flag conjunction theorem, which re-exports the seven bits as a proved equality chain so downstream assembly code can pattern-match on closed vs open gates without re-reading the module doc. In the broader Recognition gravity stack this sits inside the Regge discrete curvature pipeline that must eventually feed flat Hessian assembly and the still-open claim that the RS action converges to Einstein–Hilbert in four dimensions; the status object makes those open obligations explicit rather than silent. It does not itself advance the forcing chain (T0–T8) or the Recognition Composition Law; it only tracks local kernel closure on one hinge orbit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.