teInterEmpty
plain-language theorem explainer
The left and right two-edge subcomplexes on the four-vertex diamond have disjoint vertex sets. Anyone checking the C15 J-diamond lattice scratch witnesses would cite this. The proof is pure finite case analysis: extensionality, then fin_cases over Fin 4 with simp unfolding the two hardcoded Finsets.
Claim. On the two-edge complex with four vertices, the left SC4 subcomplex has vertices $\{0,1\}$ and the right has vertices $\{2,3\}$. Their intersection is empty: $\{0,1\} \cap \{2,3\} = \emptyset$ as subsets of $\mathrm{Fin}\,4$.
background
Module Gap2JDiamondScratch is a non-load-bearing scratchpad from debugging kernel reduction of Fin numeral goals in the C15 J-diamond lattice work. Nothing imports it; the four small witnesses are kept only as compiling exhibits. The banked lesson is that decide and OfNat simprocs fail on non-literal Fin bounds, while show of the literal form first, then ext/fin_cases/simp, closes the goals.
Here SC4 packages a 4-vertex subcomplex of the two-edge complex: a vertex Finset in Fin 4 and an edge Finset in Fin 2. The left witness takes verts ${0,1}$ and edge ${0}$; the right takes verts ${2,3}$ and edge ${1}$. This theorem records that those two vertex sets are disjoint, the elementary set fact needed before any intersection or gluing argument on the diamond.
proof idea
Tactic proof, four lines. Apply set extensionality on the vertex type Fin 4, then fin_cases on the variable. Each of the four residual goals is closed by simp unfolding the definitions of the left and right subcomplexes, which expose the concrete Finsets ${0,1}$ and ${2,3}$. No external lemmas are required; the sibling definitions supply the data.
why it matters
Inside Recognition Science gravity, Gap2 work sits in the SevenGaps stack around the J-diamond lattice (C15), where J is the unique cost from the forcing chain (T5: $J(x)=(x+x^{-1})/2-1$) and lattice combinatorics feed discrete curvature and posting-layer floors. This declaration is not on that critical path: the module doc states no load-bearing theorems live here and nothing imports the witnesses.
Its value is methodological. It freezes a working kernel pattern for empty intersections of literal Finset (Fin n) data when projections would otherwise leave residuals that simp/decide cannot close. Downstream of the scratchpad, that pattern supports cleaner proofs in Gap2JEhrhartSpan and related J-diamond span arguments. No parent theorem lists this as a dependency (used_by is empty).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.