codeEquiv
plain-language theorem explainer
For each size bound B, bounded combinatorial complexes are definitionally equivalent to an explicitly finite code type (sizes in Fin(B+1) plus incidence maps). Anyone proving finiteness of the path-sum configuration class cites this. Both directions and both inverse laws are pure structure eta / proof irrelevance (rfl).
Claim. For every natural number $B$, the type of bounded combinatorial complexes (at most $B$ vertices, edges, and tetrahedra, with abstract edge and tetrahedron incidence) is equivalent to the finite code type $\Sigma_{v,e,t\le B}\,(\mathrm{Fin}\,e\to\mathrm{Fin}\,v\times\mathrm{Fin}\,v)\times(\mathrm{Fin}\,t\to\mathrm{Fin}\,4\to\mathrm{Fin}\,v)$. Both inverse maps are definitional.
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 data.
BoundedComplex B packages that class: counts $nV,nE,nT\le B$ plus maps edgeVerts and tetVerts. It mirrors the incidence shape of Regge 3D triangulations with the metric field dropped and an explicit size cap. It contains all bounded triangulations and also non-simplicial incidence data.
CodeType B is the same data reindexed as a nested sigma type over Fin (B+1), so Mathlib's automatic Fintype instances on sigma, pi, and prod apply. Encoding and decoding (toCode, ofCode) are the two legs of the equivalence.
proof idea
One-line structure equivalence: forward map is the encoder into the finite code type, inverse is the decoder. Left and right inverse laws are both rfl, using structure eta for the record fields and proof irrelevance on the inequality witnesses $nV,nE,nT\le B$. No algebraic lemmas are invoked.
why it matters
This equivalence is the bridge that turns an abstract incidence structure into a type Mathlib already knows is finite. The sole downstream consumer is instFintypeBoundedComplex, which builds Fintype (BoundedComplex B) via Fintype.ofEquiv (CodeType B) (codeEquiv B).symm.
That instance is the proved count-finiteness theorem for the scoped class: a finite cardinal where PathSumUVBound.AdmissibleTriangulationFamily had only postulated a growthBase bound. Finiteness of the superclass yields finiteness of every subclass (including genuine triangulations), and unlocks the finite path sum $Z B w=\sum_K \mu(K),w(K)$, the modulus bounds, and the unitary $Z_{\mathrm{RS}}$ well-definedness statement.
Sharper exponential-growth semantics for exact simplicial classes remain open; this step only discharges the finiteness content.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.