decoyClass4
plain-language theorem explainer
Names the edge-class index 4 in the 15-class Regge stencil as a combinatorial decoy for the seed hinge. Gravity analysts cite it when stating that three explicit classes lie outside seed-hinge incidence support. The body is a Fin constructor with a decide proof that 4 < 15.
Claim. Let $\mathrm{decoy}_4 := 4 \in \{0,\ldots,14\}$ be the named edge-class index corresponding to mask $5$ among the fifteen Regge edge classes. Together with indices $8$ and $12$ (masks $9$ and $13$), it is one of the three combinatorial decoy classes for the seed hinge.
background
The module builds the combinatorial skeleton of a 4D Freudenthal/Kuhn triangulation of the unit 4-cube and its seed-hinge incidence, as the next kernel-checked increment after the 15-class edge stencil. That stencil partitions local edges of the 24 monotone 4-simplices into fifteen combinatorial classes; it is imported, never redefined.
The seed hinge is the triangle on vertices $0$, $e_0$, $e_0+e_1$ (masks $0,1,3$). Exactly two of the twenty-four simplices contain it. Incidence multiplicities count, for each of the fifteen classes, how many of those seed-simplices carry that class as a local edge. Three classes never appear: the decoys.
Doc-comment pins the decoy masks as $5,9,13$, i.e. class indices $4,8,12$. This definition is the first of those three named indices.
proof idea
Pure definition: the subtype constructor $\langle 4,_\rangle : \mathrm{Fin},15$, with the bound $4 < 15$ discharged by decide. No lemmas are applied.
why it matters
Gives a stable name for the first decoy class so incidence and assembly theorems can cite it without magic numbers. Downstream, seedHingeIncidence_decoy_zero proves the three decoys (indices 4, 8, 12) have zero seed-hinge incidence by decide. Downstream seedOrbitAssembly_decoy_area shows a decoy-only bump in the area weight is annihilated by the incidence cutoff in the flat-Hessian assembly skeleton.
In the module's honest scope this is deliverable-B combinatorics only: it supports nonvacuity/symmetry/decoy statements and forces the MODEL assembly form to vanish off incidence support. It does not evaluate OPEN per-hinge deficit or area kernels, does not complete the flat Hessian of the 4D Regge action, and does not touch S_RS_converges_EH_4d or gap_action_recovery.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.