hinge4DStarKernel13Status_flags
plain-language theorem explainer
Status snapshot for the type-(1,3) 4D Regge hinge star deficit class kernel on the periodic Freudenthal lattice. It records three closed gates (star enumeration, flatness, full-star class kernel) and four still-open items (type-(3,1) transport, flat Hessian assembly, EH4d convergence, gap-action recovery). QG campaign auditors cite it as the machine-checked progress ledger for this hinge class. Proof is a pure decidable check of the boolean status record.
Claim. The status record for the type-$(1,3)$ periodic-lattice star deficit class kernel asserts: star enumeration is closed, the flatness gate is closed, and the full-star class kernel is closed; type-$(3,1)$ transport remains open and flat Hessian assembly remains open; both $S_{\mathrm{RS}}\to\mathrm{EH}_{4d}$ convergence and gap-action recovery are false.
background
This module is the next kernel-checked increment in the 4D Regge QG campaign after the type-$(1,1)$ seed-orbit star kernel and the orbit classification layer. It treats the type-$(1,3)$ triangle hinge with absolute masks ${0,1,15}$ (difference masks $(1,14)$, local flat squared lengths $(1,3,4)$) and its full periodic Freudenthal star inside the origin unit cube and its ${-1,0,1}^4$ translates.
Upstream work already supplies the assembled full-star class kernel on the 15 edge-stencil classes, its explicit nonzero values, vanishing off the support, nonvacuity, the uniform-scaling decoy (directional derivative $-1$), and homothety stationarity (directional derivative $0$). The flatness gate is the star angle sum $6\cdot\arccos(1/2)=2\pi$. The complementary type-$(3,1)$ orbit is related by mask complement but is not transported here.
The status record is a boolean ledger of which campaign gates are closed versus deliberately left open; this theorem freezes that ledger in the kernel.
proof idea
One-line decidable proof: decide evaluates the seven boolean fields of the status structure and confirms the conjunction. No algebraic lemmas are invoked at this site; the closed flags are justified by the upstream theorems already proved in this module and in the type-$(1,1)$ star-kernel import (star cardinality and cube containment, flat cosine multiset and $2\pi$ angle sum, full-star class kernel equality/values/zero-off/nonvacuity, uniform-scale decoy, homothety stationarity). The open and false flags are literal constants in the status definition.
why it matters
This is the machine-checked progress certificate for deliverable A of the type-$(1,3)$ star-kernel campaign: six Kuhn simplices contain the hinge, all flat cosines equal $1/2$, the star is flat, and the full-star deficit class kernel on classes $(1,3,5,7,9,11,13)$ with values $(-\sqrt{3},-\sqrt{3},+\sqrt{3},-\sqrt{3},+\sqrt{3},+\sqrt{3},-\sqrt{3})$ is closed together with its gates.
No downstream theorems yet depend on it (used_by is empty); it exists so later Hessian assembly and continuum-limit arguments can quote a single frozen status rather than re-auditing the module. It explicitly does not flip $S_{\mathrm{RS}}\to\mathrm{EH}_{4d}$ convergence or gap-action recovery, and it leaves type-$(3,1)$ transport and full flat Hessian assembly open, matching the module's binding tier tags.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.