IndisputableMonolith.Gravity.PathSumUVBound
Defines the admissible triangulation family for the Recognition Science path sum, with mesh lower bounds and simplex-count volume caps. Supplies the comparison that the recognition action dominates the Regge action via hyperbolic growth, and records a structural UV-finiteness statement. Gravity and path-sum measure developments import it as the configuration class for discrete sums. The argument is definitional scaffolding plus elementary sinh-versus-linear comparisons.
claimAn admissible triangulation family $\mathcal{T}$ for the recognition path sum consists of triangulations whose mesh is bounded below by $\ell_{\mathrm{sub}}$ and whose simplex count is bounded above by a volume constraint $N(\mathrm{Vol})$. On such families one compares the recognition action $S_{\mathrm{rec}}$ to the Regge action $S_{\mathrm{Regge}}$, using $\sinh$ growth to dominate linear edge contributions, and obtains a structural ultraviolet finiteness bound on the path-sum weight.
background
Recognition Science gravity works with discrete path sums over triangulations rather than continuum metrics. Ultraviolet control requires restricting the sum to an admissible family: mesh cannot collapse below a fixed sub-Planck length $\ell_{\mathrm{sub}}$, and the number of simplices cannot exceed a volume-derived bound. That family is the central object of this module.
The module also introduces the path-sum weight, the recognition action, and the classical Regge action on those triangulations. The comparison lemmas rest on elementary real analysis: $\sinh$ grows at least linearly (and eventually strictly faster), so recognition weights that involve hyperbolic factors dominate Regge-type linear edge terms. Constants are taken from the RS-native package (time quantum $\tau_0 = 1$ tick).
Downstream, the admissible family is the carrier for an explicit RS admissibility predicate and for the finite configuration class used in the proved path-sum measure for $Z_{\mathrm{RS}}$.
proof idea
This is primarily a definition module with supporting comparison lemmas, not a single deep theorem. It packages AdmissibleTriangulationFamily (mesh $\ge \ell_{\mathrm{sub}}$, simplex count $\le$ volume bound) and the associated count bound with positivity and non-vanishing facts.
Analytic content is the chain sinh_dominates_linear / sinh_weakly_dominates / monotone ratio statements: standard inequalities showing hyperbolic growth beats linear growth on the positive reals. Those feed recognition_dominates_regge, comparing recognition and Regge actions termwise on admissible triangulations, and the structural claim uv_finiteness_structural that the path-sum weight stays finite under the volume and mesh cuts.
No heavy geometric measure theory; the UV bound is combinatorial once admissibility is imposed.
why it matters in Recognition Science
Without an explicit admissible class, the recognition path sum is not a well-posed discrete object. This module answers that gap and is imported by AdmissibleTriangulationProcedure, which turns admissibility into a machine-checkable predicate IsRSAdmissible over the family defined here (addressing the feedback that RS lacked a stated triangulation procedure).
It is also imported by SevenGaps.PathSumMeasure (Lane 2 toward a proved path-sum measure for $Z_{\mathrm{RS}}$), where bounded complexes and finiteness of the configuration class rest on volume and mesh cuts of this kind. In the broader RS gravity program, structural UV finiteness is the discrete counterpart of controlling short-distance degrees of freedom before continuum or effective-field limits are discussed. The recognition-versus-Regge comparison ties the RS action to a familiar simplicial gravity baseline.
scope and limits
- Does not construct a continuum limit or prove convergence of the path sum to a smooth metric theory.
- Does not derive $\ell_{\mathrm{sub}}$ or the volume bound from the T0–T8 forcing chain inside this module.
- Does not evaluate numerical values of $Z_{\mathrm{RS}}$ or fix the full measure normalization.
- Does not claim dynamical stability or uniqueness of the admissible family under refinement.
- Does not replace a full Regge calculus existence theorem; domination is structural on the cut family.
used by (2)
depends on (1)
declarations in this module (15)
-
structure
AdmissibleTriangulationFamily -
def
triangulationCountBound -
theorem
triangulationCountBound_pos -
theorem
triangulationCountBound_ne_zero -
theorem
sinh_dominates_linear -
theorem
sinh_weakly_dominates -
theorem
sinh_over_linear_monotone_statement -
structure
PathSumWeight -
def
recognitionAction -
def
reggeAction -
theorem
recognition_dominates_regge -
theorem
uv_finiteness_structural -
structure
PathSumUVBoundCert -
def
pathSumUVBoundCert -
theorem
pathSumUVBoundCert_inhabited