teInter2
plain-language theorem explainer
The vertex sets of the left and right two-edge subcomplexes intersect definitionally as the literal Finsets {0,1} and {2,3} on Fin 4. Kernel-debugging exhibit from the C15 J-diamond lattice scratchpad; nothing load-bearing imports it. Proof is pure reflexivity after unfolding the two subcomplex definitions.
Claim. The vertex set of the left two-edge subcomplex of the two-edge complex, intersected with the vertex set of the right two-edge subcomplex, equals $\{0,1\}\cap\{2,3\}$ as finite subsets of $\mathrm{Fin}\,4$.
background
Module Gap2JDiamondScratch is a non-load-bearing scratchpad from debugging Lean kernel reduction on Fin numeral goals in the C15 J-diamond lattice work. The four small witnesses here only exhibit a compiling pattern; the lesson is banked as L-qg-fin-literal-show-first.
teLeft and teRight are the two SC4 subcomplexes of twoEdgeComplex: left has vertices ${0,1}$ and edge ${0}$; right has vertices ${2,3}$ and edge ${1}$. The theorem records that their vertex-set intersection is definitionally the same as intersecting those two literal Finsets on Fin 4.
The surrounding finding is that decide and OfNat simprocs fail on non-literal Fin bounds (projections such as K.nV), while writing the definitionally equal literal form first lets ext/fin_cases/simp close.
proof idea
One-line reflexivity. Unfolding teLeft.verts and teRight.verts yields exactly ({0,1} : Finset (Fin 4)) and ({2,3} : Finset (Fin 4)), so the two sides of the equality are definitionally identical and rfl closes.
why it matters
Compiling kernel witness only. The module doc states no load-bearing theorems live here and nothing imports these exhibits; the real payload is the debugging lesson that literal Fin forms must be shown before case-split tactics. Downstream use count is zero. It sits beside sibling witnesses (teInterEmpty, inter4literal, fin4decide) that pin the same Fin-numeral reduction pattern for the J-diamond lattice work, not a step of the T0–T8 forcing chain or a gravity mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.