CodeType
plain-language theorem explainer
A finite encoding of bounded combinatorial 3-complexes with at most B vertices, edges, and tetrahedra: sizes live in Fin(B+1) and incidence maps are functions on those finite index types. Anyone proving count-finiteness of the scoped triangulation class cites this type. The definition is a dependent sigma of finite products and function spaces, so Mathlib supplies Fintype automatically.
Claim. For each bound $B\in\mathbb{N}$, the code type is the dependent sum $\sum_{v,e,t\,:\,\mathrm{Fin}(B+1)}\bigl(\mathrm{Fin}\,e\to\mathrm{Fin}\,v\times\mathrm{Fin}\,v\bigr)\times\bigl(\mathrm{Fin}\,t\to\mathrm{Fin}\,4\to\mathrm{Fin}\,v\bigr)$. It packages vertex/edge/tetrahedron counts (capped by $B$) together with edge-endpoint and tetrahedron-vertex incidence data on those explicit finite sets.
background
Lane 2 of the Seven Gaps program builds a proved path-sum measure $Z_{\mathrm{RS}}$ over a scoped class of combinatorial triangulations at fixed lattice scale. The substrate fixes edge length at the minimum mesh, so configurations are equilateral and CDT-style: all geometry sits in incidence maps.
The structure BoundedComplex B is that scoped class: natural numbers $n_V,n_E,n_T\le B$ plus maps $\mathrm{edgeVerts}:\mathrm{Fin},n_E\to\mathrm{Fin},n_V\times\mathrm{Fin},n_V$ and $\mathrm{tetVerts}:\mathrm{Fin},n_T\to\mathrm{Fin},4\to\mathrm{Fin},n_V$. It mirrors the incidence shape of the 3D Regge triangulation type with the metric field dropped and an explicit size cap. It contains all bounded triangulations and also non-simplicial configurations; finiteness of the superclass still yields finiteness of every subclass.
To obtain a Fintype instance one needs a type whose finiteness is automatic from sigma, pi, and product instances. That is the role of this code type: replace the inequality-bounded naturals by elements of $\mathrm{Fin}(B+1)$ and keep the incidence functions on the corresponding finite index types.
proof idea
Definitional abbrev, not a proof. Expand the structure fields into a single dependent sum: three size coordinates in $\mathrm{Fin}(B+1)$, then a pair of function spaces for edge endpoints and tetrahedron vertices. Coercions $(\mathrm{Fin},k:\mathbb{N})$ recover the domain cardinalities used by those function types. No lemmas are applied; Mathlib's standard finite-type instances on $\Sigma$, $\times$, and $\to$ do the rest once the encoding is in place.
why it matters
This type is the finite carrier behind the count-finiteness theorem for the scoped class. The encode/decode maps and the equivalence codeEquiv identify BoundedComplex B with the code type definitionally (structure eta and proof irrelevance). The Fintype instance is then Fintype.ofEquiv along that equivalence, discharging the count-finiteness content of the assumed growthBase field on admissible triangulation families: a proved finite cardinal where only a bound was postulated.
Downstream, finiteness feeds the automorphism groups, the symmetry-factor measure $\mu(K)=1/|\mathrm{Aut},K|$, and the path sum $Z(B,w)=\sum_K\mu(K),w(K)$ with the modulus bounds $|Z|\le\sum\mu$ and $|Z|\le|\mathrm{BoundedComplex},B|$. The unitary weights $w(K)=e^{iS(K)}$ then give the honest scoped $Z_{\mathrm{RS}}$ statement. Sharper exponential-growth semantics for exact simplicial subclasses remain open; this definition only underwrites the finite superclass.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.