decoyClass8
plain-language theorem explainer
Names edge class 8 among the 15 Freudenthal 4-cube edge classes as an explicit combinatorial decoy: a class that never appears as a local edge of either seed simplex containing the seed hinge. Gravity analysts cite it when stating the three-class decoy support of the seed-hinge incidence vector. The body is a Fin-subtype constructor with a decide proof of the bound.
Claim. Let $\mathrm{decoy}_8 := 8 \in \{0,1,\ldots,14\}$ be the named edge-class index used as the second of three combinatorial decoys for the seed-hinge incidence count on the 15-class Regge edge stencil.
background
The module builds the combinatorial skeleton of the flat Hessian for 4D Regge calculus on the Freudenthal (Kuhn) triangulation of the 4-cube. It imports the fixed 15-class edge stencil and never redefines it. Each 4-simplex is a monotone path through the four axes; each of its ten edges lands in one of the fifteen global classes via local edge masks.
The seed hinge is the triangle with vertex masks $0$, $e_0$, $e_0+e_1$ (classes $0,1,3$). Exactly two of the twenty-four simplices contain it. Incidence multiplicity of a class is the number of those two simplices in which the class appears as a local edge. Three classes never appear; they are the combinatorial decoys.
This definition simply pins the middle decoy index to $8$ as an element of $\mathrm{Fin},15$, matching the sibling decoys at $4$ and $12$.
proof idea
Definition only: construct the subtype element $\langle 8,_\rangle : \mathrm{Fin},15$ and discharge $8 < 15$ by decide. No lemmas are applied.
why it matters
Feeds the decoy half of the incidence package. The parent theorem seedHingeIncidence_decoy_zero states that the three named decoys (classes 4, 8, and 12) each have seed-hinge incidence zero, proved by decide on the enumerated support. That non-support is part of deliverable B in the module doc: combinatorial control of which stencil classes can carry nonzero flat-Hessian class weights.
It does not evaluate OPEN per-hinge area or deficit kernels, and it does not complete the flat Hessian or flip gap_action_recovery / S_RS_converges_EH_4d. It only labels one of the three classes forced to vanish in the assembly skeleton so the MODEL contraction is supported exactly on the incidence set.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.