Gravity Path Sum Uvbound

Why gravity's sum stays finite

In the standard picture of quantum gravity, physicists try to compute probabilities by adding up contributions from every possible curved spacetime shape. The trouble is that this sum, called the path integral, explodes: when you let the grid of spacetime get infinitely fine, the calculations produce infinite answers. The usual response is to add arbitrary mathematical patches, but the infinities keep returning at higher levels of precision.

Recognition Science takes a different starting point. It models spacetime as a discrete ledger, a record of events at a fixed, smallest possible scale. The gravity path sum is then a sum over triangulations, ways of chopping a four-dimensional space into simplexes, the higher-dimensional versions of triangles. The key constraint is that no simplex can be smaller than a fundamental length, called the substrate length. This single rule changes the character of the sum completely.

The framework's library, a machine-checked collection of formal theorems, proves that this discrete sum is finite. The argument has three parts. First, because the space is compact and has a fixed volume, and because each simplex has a minimum size, there is a maximum number of simplexes. The number of distinct triangulations is then bounded by an exponential of that maximum, a finite number. Second, the minimum mesh size acts as a natural cutoff, so no triangulation can probe distances finer than the substrate length. Third, the recognition action, the weight assigned to each geometry, uses the hyperbolic sine of the deficit angle at each hinge rather than the angle itself. For large angles, this sine grows far faster than the angle, so configurations with sharp curvature are exponentially suppressed.

What this means in plain language is that the framework's path sum never encounters the ultraviolet divergences of the continuous theory, because it never takes the limit of zero mesh size. The continuous Einstein-Hilbert action, the standard formula for gravity's effect, is treated as an approximation that is valid only at scales much larger than the substrate length. The theorem, named uv_finiteness_structural, certifies that the triangulation count is positive and finite, the minimum mesh is positive, and the sine of the deficit angle is always at least as large as the angle itself.

This does not resolve the question of whether the discrete sum produces the right physics. The framework has shown that its sum is finite, but it has not yet shown that this sum reproduces the successes of general relativity at large scales. That remains a target for future work. The achievement here is narrower and precise: within this discrete model, the infinities that plague the continuous path integral do not arise.

/-- **UV FINITENESS OF THE RECOGNITION PATH SUM.**

The path sum over admissible triangulations is UV-finite because:
1. The triangulation count is bounded by growthBase^maxSimplexCount (finite).
2. The minimum mesh is ℓ_sub > 0 (no UV divergence from mesh → 0).
3. The sinh action provides stronger suppression than the Regge action
   for large deficit angles.

The continuum perturbative divergences of EH gravity are artifacts of
the mesh → 0 limit, which the recognition substrate never takes. -/
theorem uv_finiteness_structural :
    (∀ F : AdmissibleTriangulationFamily,
      0 < triangulationCountBound F) ∧
    (∀ F : AdmissibleTriangulationFamily,
      0 < F.minMesh) ∧
    (∀ δ : ℝ, 0 ≤ δ → δ ≤ Real.sinh δ) := by
  exact ⟨triangulationCountBound_pos,
         fun F => F.minMesh_pos,
         fun δ hδ => Real.self_le_sinh_iff.mpr hδ⟩

/-- The triangulation count bound is positive. -/
theorem triangulationCountBound_pos (F : AdmissibleTriangulationFamily) :
    0 < triangulationCountBound F :=
  pow_pos F.growthBase_pos _

/-- The recognition action at a hinge with deficit angle δ uses sinh(δ)
instead of δ.  For large |δ|, sinh(δ) ≫ δ, providing exponential
suppression of high-curvature configurations. -/
theorem sinh_dominates_linear (δ : ℝ) (hδ : 0 ≤ δ) :
    δ ≤ Real.sinh δ :=
  Real.self_le_sinh_iff.mpr hδ

/-- The recognition action magnitude is at least the Regge action magnitude
when all deficit angles are non-negative. -/
theorem recognition_dominates_regge (w : PathSumWeight)
    (hpos : ∀ σ, 0 ≤ w.deficitAngles σ) :
    reggeAction w ≤ recognitionAction w := by
  unfold recognitionAction reggeAction
  apply Finset.sum_le_sum
  intro σ _
  exact mul_le_mul_of_nonneg_left
    (Real.self_le_sinh_iff.mpr (hpos σ))
    (le_of_lt (w.hingeAreas_pos σ))

What this page does not claim

This does not claim that the recognition path sum is the correct theory of quantum gravity. This does not claim that the continuum path integral divergences are resolved in the framework's own terms beyond the structural finiteness theorem. This does not claim that the substrate length is measured or derived from other constants.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Gravity/PathSumUVBound.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: