AdmissibleTriangulationFamily
plain-language theorem explainer
Packages the three numeric parameters that define an admissible triangulation family for the recognition path sum: a positive simplex-count cap, a positive exponential growth base for the Tutte-type count bound, and a positive minimum mesh (the substrate length). Gravity and path-sum UV arguments cite it as the carrier type for finiteness certificates. As a structure definition there is no proof body; positivity side-conditions are part of the data.
Claim. An admissible triangulation family is a triple $(N_{\max}, C, \ell_{\min})$ of a positive integer maximum simplex count $N_{\max}$, a positive real growth base $C$, and a positive real minimum mesh $\ell_{\min}$ (identified with the substrate length $\ell_{\mathrm{sub}}$), so that every member triangulation has mesh at least $\ell_{\min}$ and at most $N_{\max}$ simplices, with the number of combinatorially distinct such triangulations bounded by $C^{N_{\max}}$.
background
The module treats UV finiteness of the recognition path sum on a compact 4-manifold $M$. The sum runs over admissible triangulations $T$ with mesh bounded below by the substrate length $\ell_{\mathrm{sub}}$:
$Z = \sum_{T:,\mathrm{mesh}(T)\ge\ell_{\mathrm{sub}}} \mu(T),\exp(i S_{\mathrm{RS}}(T)/\hbar_{\mathrm{RS}})$.
Finiteness rests on three structural facts: a volume-and-mesh bound on the maximum simplex count $N_{\max}=V/\ell_{\mathrm{sub}}^4$; a Tutte-type exponential bound (at most $C^N$ combinatorially distinct triangulations with $\le N$ simplices); and sinh suppression of large deficit angles in the recognition action relative to Regge. Continuum EH power-counting divergences are read as artifacts of sending the mesh to zero at fixed metric; the recognition substrate never takes that limit.
This structure is the data package for those three parameters. Related notions of admissibility appear upstream in the recognition operator (ledger-state admissibility) and in hinge-aware Regge analysis, but here the fields are purely the numeric bounds needed for the path-sum count.
proof idea
Definitional structure with no proof body. Three fields carry the bounds, each paired with an explicit positivity hypothesis (0 < maxSimplexCount, 0 < growthBase, 0 < minMesh). Downstream code reads the fields directly (e.g. the count bound is growthBase ^ maxSimplexCount) and reuses the positivity proofs via positivity or norm_num when concrete witnesses are supplied.
why it matters
This is the carrier type for the structural UV-finiteness argument in the gravity path-sum module. Downstream, triangulationCountBound is exactly growthBase^maxSimplexCount; positivity and non-vanishing of that bound, and the certificate PathSumUVBoundCert (finite count, positive mesh, sinh dominates linear deficit), all quantify over this family. The admissibility procedure module builds IsRSAdmissible on top of it (re-deriving mesh lower bound, finite simplex cap, and positive growth base), supplies a concrete witness with unit constants, and proves bridge-constant monotonicity for RS-admissible families.
In the broader Recognition framework the structure encodes the discrete UV cutoff that replaces continuum $h\to 0$: mesh $\ge\ell_{\mathrm{sub}}$ and finite $N_{\max}$ make the path sum a finite sum, so perturbative non-renormalizability of Einstein-Hilbert (dimension $-2$ Newton coupling) does not apply. It does not itself invoke the forcing chain (T5–T8) or the mass ladder; it is the gravity-side bookkeeping object those continuum comparisons rest on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.