toCode
plain-language theorem explainer
Packs a size-capped combinatorial triangulation (at most B vertices, edges, tetrahedra, with incidence maps) into an explicitly finite code type whose components live in Fin(B+1) and function spaces over Fin. Anyone proving finiteness of the scoped path-sum class cites this encoding. The body is a pure structure packing: bound inequalities become Fin memberships via Nat.lt_succ_of_le, and the incidence maps are carried unchanged.
Claim. Given a natural number bound $B$ and a bounded complex $K$ (counts $n_V,n_E,n_T\le B$ together with edge and tetrahedron incidence maps), produce the corresponding code: the triple of sizes as elements of $\mathrm{Fin}(B+1)$, paired with the same incidence data as maps between the corresponding finite index types.
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 at fixed lattice scale. The substrate fixes edge length at the minimum mesh, so configurations are equilateral and combinatorial (CDT-style); geometry is carried only by incidence.
BoundedComplex B is that scoped class: natural counts $n_V,n_E,n_T$ each at most $B$, plus edgeVerts : Fin nE → Fin nV × Fin nV and tetVerts : Fin nT → Fin 4 → Fin nV. It mirrors the incidence shape of Regge triangulation without a metric field, and deliberately does not enforce simplicial constraints.
CodeType B is the matching finite type: a dependent sum over sizes in $\mathrm{Fin}(B+1)$ of the product of the two incidence function spaces. Fintype instances for sigma, pi, and prod then make the code type finite automatically.
proof idea
Definitional packing, not a tactic proof. For each count $n\le B$, form the Fin element $\langle n,\mathrm{Nat.lt_succ_of_le},h\rangle$ so the size lives in $\mathrm{Fin}(B+1)$. Bundle the three Fin sizes with the pair $(K.\mathrm{edgeVerts},K.\mathrm{tetVerts})$ into the sigma/product shape of the code type. No lemmas beyond the standard inequality-to-Fin coercion are used.
why it matters
This encoder is one half of codeEquiv, the explicit equivalence BoundedComplex B ≃ CodeType B whose both inverses are definitional (structure eta and proof irrelevance). That equivalence supplies the Fintype instance on the scoped class, which discharges the count-finiteness content of the assumed growthBase field of PathSumUVBound.AdmissibleTriangulationFamily: a proved finite cardinal where a bound was only postulated.
Downstream, finiteness of labeled complexes yields a finite automorphism group, the symmetry-factor measure $\mu(K)=1/|\mathrm{Aut},K|$, and the finite path sum $Z B w=\sum_K \mu(K),w(K)$ with norm bounds and relabeling invariance. The unitary weights $w=\exp(iS)$ then give the honest scoped $Z_{\mathrm{RS}}$ statement. Sharper exponential-growth semantics for exact simplicial subclasses remain open; this definition only enables the superclass finiteness argument.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.