ofCode
plain-language theorem explainer
Decodes a finite combinatorial code into a size-capped abstract triangulation: vertex/edge/tet counts and incidence maps are unpacked from a dependent product over Fin(B+1). Anyone proving finiteness of the scoped path-sum class cites this as the inverse half of the code equivalence. Construction is pure field projection plus the Fin-to-≤B bound conversion via lt_succ_iff.
Claim. Given a bound $B\in\mathbb{N}$ and a code $c$ in the finite type of triples $(v,e,t)\in\mathrm{Fin}(B+1)^3$ together with incidence maps $\mathrm{Fin}\,e\to\mathrm{Fin}\,v\times\mathrm{Fin}\,v$ and $\mathrm{Fin}\,t\to\mathrm{Fin}\,4\to\mathrm{Fin}\,v$, return the bounded complex with those counts and maps, taking the size inequalities $v,e,t\le B$ from the $\mathrm{Fin}$ witnesses.
background
Lane 2 of the Seven Gaps program builds a proved path-sum measure $Z_{\mathrm{RS}}$ over a scoped class of combinatorial 3D triangulations. The substrate fixes edge length at the minimum mesh, so configurations are equilateral and CDT-style: all geometry sits in incidence data.
BoundedComplex B is that scoped class: at most $B$ vertices, edges, and tetrahedra, with maps edgeVerts and tetVerts of the same shape as Regge triangulation incidence (metric field dropped). The companion finite code type packages the same data as a $\Sigma$-type over $\mathrm{Fin}(B+1)$ for the three counts, so Mathlib's automatic Fintype instances apply.
This decoder is the structure-level inverse of the encoder that packs a bounded complex into that code. Together they make the scoped class definitionally equivalent to a manifestly finite type.
proof idea
Definitional constructor, not a tactic proof. Project the $\Sigma$-type: first three components become $nV,nE,nT$; the paired incidence functions become edgeVerts and tetVerts. Each size bound $n\le B$ is recovered from the Fin(B+1) witness by Nat.lt_succ_iff.mp on isLt. No lemmas beyond that Nat fact and structure eta.
why it matters
Feeds codeEquiv, the explicit equivalence BoundedComplex B \simeq CodeType B whose both inverses are definitional (structure eta and proof irrelevance). That equivalence is how the module obtains Fintype on the scoped class and thereby discharges the count-finiteness content of the assumed growthBase field in PathSumUVBound.AdmissibleTriangulationFamily.
With a finite labeled class in hand, the module defines the symmetry-factor measure $\mu(K)=1/|\mathrm{Aut},K|$, the path sum $Z B w=\sum_K \mu(K),w(K)$, and the unitary instance $w=e^{iS}$ that yields the honest scoped $Z_{\mathrm{RS}}$ bounds. Sharper exponential-growth semantics for exact simplicial subclasses remain open; this decoder only closes the finite-cardinal half.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.