SC4
plain-language theorem explainer
SC4 packages a finite subcomplex of a bounded complex K: a vertex set inside Fin K.nV and an edge set inside Fin K.nE. It is a scratch-level carrier used only to stage Fin-literal kernel witnesses (teLeft, teRight) while debugging J-diamond lattice goals. The declaration is pure data; no theorems attach.
Claim. For a bounded complex $K$ (with vertex count $K.nV$ and edge count $K.nE$), an SC4 record is a pair of finite sets: vertices $\subseteq \{0,\ldots,K.nV-1\}$ and edges $\subseteq \{0,\ldots,K.nE-1\}$.
background
The module is an explicit scratchpad for C15 J-diamond lattice work. Nothing load-bearing lives here; the four small kernel witnesses are compiling exhibits only. The lesson banked is that decide and OfNat simprocs refuse non-literal Fin bounds such as projections K.nV and K.nE.
Upstream, nV and nE are the vertex- and edge-count observables on census ensembles. BoundedComplex B supplies those counts as fields, so a subcomplex is just a pair of Finsets over the corresponding finite index types. Related cosmology edges (B, diamond edge lists) motivate the same vertex/edge split but are not required to inhabit SC4.
Local convention: write literal Fin n bounds first (show the definitionally equal numeral form), then ext/fin_cases/simp closes residual equalities that otherwise stall as silent axioms.
proof idea
No proof: SC4 is a structure declaration (two fields, no propositions). Inhabitation is by supplying concrete Finsets, as in the sibling witnesses that fix K = twoEdgeComplex and give literal vertex/edge sets over Fin 4 and Fin 2.
why it matters
SC4 exists only to host the compiling exhibits teLeft and teRight (and related intersection lemmas in the same file) while the team debugged kernel reduction for Fin numeral goals on the J-diamond lattice. The module doc states that nothing imports these witnesses; the real deliverable is the tactic pattern L-qg-fin-literal-show-first.
In the broader SevenGaps gravity line, diamond subcomplexes and census measures (nV, nE) feed gap-counting arguments, but this particular structure is not on the forcing chain (T0–T8) and does not constrain $\varphi$, the eight-tick octave, or $D=3$. It is scaffolding hygiene, not a physics claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.