teLeft
plain-language theorem explainer
Names the left edge of the two-edge complex as a four-vertex subcomplex: vertices {0,1} and the single edge index 0. Used only as a compiling witness while debugging Fin-literal kernel goals in the J-diamond lattice scratchpad. The body is a direct structure instance, not a proof.
Claim. Let $K$ be the bounded complex with four vertices and two disjoint edges $0\to 1$ and $2\to 3$. The left subcomplex is the pair of finite sets $V_L=\{0,1\}\subset\mathrm{Fin}\,4$ and $E_L=\{0\}\subset\mathrm{Fin}\,2$.
background
The module is a non-load-bearing scratchpad for C15 J-diamond lattice work. It records kernel witnesses that force Lean to reduce Fin goals against literal bounds rather than projections such as K.nV or K.nE.
twoEdgeComplex is the ambient complex: four vertices, two edges, zero triangles, with the two edges disjoint ($0\to 1$ and $2\to 3$). The local structure SC4 packages any choice of vertex subset and edge subset of a bounded complex as a named pair of finsets.
Upstream, the cosmology interface supplies a diamond edge list (ordered adjacent pairs), but here only the two-edge toy complex is used. The lesson banked from these witnesses is to show the definitionally equal literal form before ext/fin_cases/simp.
proof idea
Definitional instance, not a tactic proof. The structure fields are filled by two finset literals: vertices {0, 1} in Fin 4 and edges {0} in Fin 2, matching the left edge of twoEdgeComplex. No lemmas are applied.
why it matters
Exists only as a compiling exhibit inside Gap2JDiamondScratch. Downstream, teInterEmpty and teInter2 use it (with the matching right subcomplex) to check that the two vertex sets are disjoint and that their intersection reduces definitionally to the literal empty intersection. Nothing in the Recognition forcing chain (T0–T8), RCL, or gravity mass ladder depends on it; the module doc states no other file imports these witnesses. The value is methodological: it freezes the Fin-literal pattern later summarized as L-qg-fin-literal-show-first.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.