IndisputableMonolith.Gravity.AdmissibleTriangulationProcedure
Defines the RS admissibility predicate for triangulation families entering the recognition path sum on a compact 4-manifold. Packages positive mesh lower bound, finite simplex-count cap, positive growth base, and an assumed bridge from recognition ratios to deficit angles. Gravity workers citing the path-sum UV bound use this interface. Structure is definitional: predicate, witness, existence, and a monotone bridge-constant lemma.
claimA triangulation family is RS-admissible when $\min\mathrm{Mesh}>0$, $\max\mathrm{SimplexCount}>0$, $\mathrm{growthBase}>0$, and the recognition-ratio bridge $\log x_\sigma=\kappa\cdot\mathrm{deficit}+O(\mathrm{mesh}^3)$ holds as a physical hypothesis (not an RS axiom).
background
The recognition path sum runs over admissible triangulations $T$ of a compact 4-manifold $M$ with mesh bounded below by a sub-Planck length $\ell_{\mathrm{sub}}$. Upstream, PathSumUVBound treats UV finiteness of that sum as a structural theorem: once the family of triangulations is admissible, the sum stays finite.
This module isolates what "admissible" means in RS terms. Three conditions are derived bookkeeping: a strictly positive mesh lower bound, a finite positive simplex-count cap, and a positive growth base controlling how counts scale under refinement. The fourth is tagged ASSUMED: a bridge $\log x_\sigma=\kappa\cdot\mathrm{deficit}+O(\mathrm{mesh}^3)$ linking recognition ratios on simplices to deficit angles, with cubic mesh remainder.
Sibling names mark the interface: the predicate itself, a concrete witness, an existence statement, and monotonicity of the bridge constant under the natural order on families.
proof idea
Definition-and-interface module, not a deep proof development. The core object is a Prop packaging the four admissibility clauses. A witness construction supplies concrete parameters satisfying the three derived bounds; existence follows by exhibiting that witness. The bridge clause is carried as an assumed hypothesis rather than discharged from RS axioms. A short monotone lemma compares bridge constants when one family refines another. No heavy tactic scripts: packaging, witness, and order facts.
why it matters in Recognition Science
PathSumUVBound needs a sharp admissibility gate before it can claim UV finiteness of the recognition path sum. This module is that gate: without positive mesh, finite simplex counts, and controlled growth, the sum over triangulations is not even well-posed; without the ratio-to-deficit bridge, geometric curvature data never enter the recognition weights.
The bridge is explicitly not derived from the forcing chain (T0-T8) or the Recognition Composition Law. It is the physical handoff from discrete recognition ratios to continuum deficit angles, with $O(\mathrm{mesh}^3)$ remainder matching standard Regge-calculus error scales. Downstream used_by is empty in the graph snapshot, so the immediate consumer is the imported UV-bound development itself rather than a named child theorem here.
Anyone auditing gravity claims in RS should treat the three derived bounds as closed bookkeeping and the bridge as an open physical hypothesis still sitting outside the axiom core.
scope and limits
- Does not derive the recognition-ratio bridge from RS axioms; it remains ASSUMED.
- Does not prove UV finiteness of the path sum; that lives in PathSumUVBound.
- Does not fix numerical values of mesh, simplex cap, growth base, or bridge constant κ.
- Does not address non-compact manifolds or meshes allowed to approach zero.
- Does not construct the continuum limit or recover Einstein equations from the sum.