provedFamily_growthBase_derived
plain-language theorem explainer
The growth base of the proved admissible triangulation family at bound B equals the real cardinality of bounded combinatorial complexes of size at most B. Anyone connecting the path-sum UV-bound interface to the concrete finite configuration model cites this. The equality is definitional: the family is built with that cardinal in the growth-base field, so the proof is reflexivity.
Claim. For every $B \in \mathbb{N}$, the growth base of the proved admissible triangulation family at lattice bound $B$ equals the cardinality of the finite class of bounded combinatorial complexes with at most $B$ vertices, edges, and tetrahedra, viewed as a real number.
background
Seven Gaps Lane 2 builds an honest path-sum measure for $Z_{RS}$ on a scoped class of bounded combinatorial triangulations at fixed lattice scale. The recognition substrate fixes edge length at the minimum mesh, so configurations are combinatorial and equilateral (CDT-style). A bounded complex of size at most $B$ stores incidence data for $\le B$ vertices, edges, and tetrahedra (edge and tet vertex maps), mirroring a 3D Regge triangulation with the metric field dropped.
The upstream UV-bound package expects an admissible triangulation family whose growth-base field supplies a finite count. This module already proves the bounded-complex class is a Fintype via an explicit coding equivalence, so a concrete natural cardinal is available. The proved family plugs that cardinal (as a real) into the growth-base slot, discharging the count-finiteness content the interface had only postulated.
Scope honesty from the module: the superclass contains all bounded triangulations but also non-simplicial incidence data; finiteness of the superclass still yields finiteness of every subclass.
proof idea
One-line term proof by reflexivity. The proved family is constructed so its growth-base field is definitionally the real cast of the Fintype cardinality of bounded complexes at bound $B$; no algebraic rewriting or external lemma is required.
why it matters
Bridge result for the path-sum UV bound: the proved count sits inside the structural triangulation-count bound for the proved family, so the assumed-count interface is satisfiable with derived data rather than a free parameter. That closes the finiteness half of the growth-base obligation behind the honest scoped $Z_{RS}$ statement (finite path sum with modulus bounds by the symmetry-factor sum and by the complex cardinal, unitary weights of modulus one).
It does not settle the sharper exponential-growth reading of growth base for exact simplicial classes; the module status leaves that open. No downstream uses are recorded yet; the declaration is infrastructure for the gravity Seven Gaps lane and the CDT-style measure class.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.