hinge4DOrbitClassificationStatus_flags
plain-language theorem explainer
Status ledger for the Regge 4D triangle-hinge orbit classification: the module's status list has exactly six entries and explicitly records the open item on per-orbit star kernels for the five non-seed S4 orbits. Anyone tracking combinatorial prerequisites for the flat Hessian would cite it. Proof is a single decide on a concrete finite list.
Claim. The hinge-orbit classification status list has length $6$, and it contains the open-status marker for per-orbit star kernels on the five non-seed $S_4$ orbits.
background
This module is the combinatorial prerequisite for assembling the flat Hessian of the 4D Regge action from per-orbit star kernels on a unit 4-cube Kuhn triangulation (Freudenthal cell). Scope is combinatorics only: triangle hinges up to lattice translation (difference masks) and triangulation-preserving symmetry. It imports the 24 Kuhn simplices / vertex-mask API and the 15-class edge-stencil mask utilities; it does not redefine them.
Deliverable A classifies every index-triple triangle as a monotone mask chain with disjoint nonzero difference masks $(a,b)$, typed by the popcount pair $(|a|,|b|)\in{(1,1),(1,2),(2,1),(1,3),(3,1),(2,2)}$. Cell enumeration gives $24\cdot C(5,3)=240$ oriented slots with per-type counts $(72,48,48,24,24,24)$. The $S_4$ action on bit positions is transitive on each type (six lattice orbits); adjoining bitwise complement merges $(1,2)\sim(2,1)$ and $(1,3)\sim(3,1)$ to four orbits under $S_4\rtimes{id,\mathrm{complement}}$.
The status definition is a fixed List String of theorem and open markers for this campaign slice. The present theorem only audits that list.
proof idea
One-line decidable proof: decide discharges both conjuncts on the concrete finite list hinge4DOrbitClassificationStatus (length equality and list membership of the quoted OPEN string). No lemmas about hinges, masks, or $S_4$ orbits are invoked.
why it matters
Bookkeeping for the QG full-theory campaign: it freezes an honest status snapshot of what the orbit-classification module has closed versus what remains open. The OPEN entry it pins is the missing per-orbit star kernels for the five non-seed $S_4$ orbits (the seed hinge ${0,e_0,e_0+e_1}$ of type $(1,1)$ is already committed elsewhere). A sibling OPEN flags flat Hessian assembly over all hinge orbits.
Module tier tags bind that this slice does not evaluate those kernels, does not complete the flat Hessian, does not prove $S_{RS}$ converges to Einstein-Hilbert in 4D, and does not flip gap-action recovery. No downstream consumers are wired yet (used_by empty); the flag exists so later Hessian/star-kernel work can cite a machine-checked ledger rather than prose alone.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.