provedFamily
plain-language theorem explainer
Packages the finite scoped class of bounded complexes of size at most B into an admissible triangulation family for the recognition path sum. Growth base is the actual Fintype cardinal of that class, not a postulated exponential; mesh is the unit lattice scale. Cited by anyone discharging the PathSumUVBound count interface or building the scoped Z_RS measure. Structure instance: positivity lemmas and a cast of the proved card.
Claim. For each natural number $B$, there is an admissible triangulation family with maximum simplex count $B+1$, growth base equal to the cardinality of the set of bounded combinatorial complexes of size at most $B$ (as a real), and minimum mesh equal to $1$.
background
Lane 2 of the Seven Gaps gravity work builds an honest path-sum measure $Z_{RS}$ on a scoped configuration class. The class BoundedComplex B is a combinatorial triangulation at fixed lattice scale: at most $B$ vertices, edges, and tetrahedra, with abstract incidence maps and no metric field (CDT-style; edge length fixed at the substrate minimum mesh). It is proved finite via an explicit code equivalence, and nonempty (the empty complex).
Upstream, AdmissibleTriangulationFamily is the interface structure for recognition path sums: members must bound simplex count above by a volume constraint, supply a positive growth base for the triangulation count, and keep mesh bounded below by $\ell_{\mathrm{sub}}$. Historically the growth base was an assumed exponential parameter. The module's theorem tier replaces that assumption with a derived finite cardinal of the scoped superclass.
Scope honesty from the module doc: BoundedComplex carries arbitrary bounded incidence data and does not enforce simplicial constraints, so it contains all bounded triangulations and also non-simplicial configurations. Finiteness of the superclass still yields finiteness of every subclass.
proof idea
Definitional structure instance, not a tactic proof. Set maxSimplexCount := B + 1 and discharge positivity by Nat.succ_pos. Set growthBase to the real cast of Fintype.card (BoundedComplex B), with positivity by exact_mod_cast on the upstream theorem boundedComplex_card_pos (card positive because the empty complex inhabits the type). Set minMesh := 1 with one_pos. No further lemmas.
why it matters
This is the bridge object that turns the PathSumUVBound interface from assumed-count data into derived data. Downstream, provedFamily_growthBase_derived records that the growth base equals the Fintype cardinal by definitional equality, and proved_count_le_structural_bound shows that cardinal sits inside triangulationCountBound for this family (the assumed-count interface is satisfiable). Together they discharge the count-finiteness content of the admissible-family growth field for the scoped class.
In the broader Recognition gravity stack this feeds the honest $Z_{RS}$ statement: the path sum over labeled complexes with symmetry factor $\mu(K)=1/|\mathrm{Aut},K|$ is a finite sum with modulus bounds, and the unitary weights $w=e^{iS}$ inherit those bounds. The sharper exponential-growth semantics of the growth-base field for exact simplicial subclasses remains open (module status tier).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.