Gravity Path Sum Uvbound Recognition Dominates Regge

The suppression inequality

In the discrete approach to gravity known as Regge calculus, spacetime is built from flat triangular pieces glued together, and curvature lives only along the hinges where pieces meet. The Regge action, the quantity whose exponential weights each configuration in a path sum, is linear in the deficit angle at each hinge: a sharper corner costs proportionally more. The Recognition Science framework replaces that linear dependence with a hyperbolic sine, sinh(δ), which for small angles behaves like δ but for large angles grows far faster. The declaration recognition_dominates_regge is the machine-checked theorem that, when all deficit angles are non-negative, the recognition action is always at least as large as the Regge action on the same triangulation.

The proof is a direct comparison. The framework's library of formal theorems verifies that for every non-negative real number δ, the inequality δ ≤ sinh(δ) holds, a classical fact visible from the power series sinh(δ) = δ + δ³/6 + ... . Since hinge areas are positive, multiplying both sides by the area preserves the inequality, and summing over all hinges of a triangulation yields the result. The theorem is tagged STRUCTURAL THEOREM in the library's certification structure, with zero unproved axioms and zero framework-internal axioms; its statement and proof are checked by the machine.

The consequence is that high-curvature configurations, those with large deficit angles, are exponentially more suppressed in the recognition path sum than in the Regge path sum. The recognition path sum is defined as a sum over admissible triangulations of a compact 4-manifold with mesh bounded below by a substrate length ℓ_sub. Because the triangulation count is finite and the mesh never goes to zero, the sum is UV-finite: the continuum perturbative divergences of Einstein-Hilbert gravity, which arise from taking the mesh to zero while holding the metric fixed, are artifacts of a limit the recognition substrate never takes. The framework's library states this as the uv_finiteness_structural theorem, combining the finite triangulation count, the positive minimum mesh, and the sinh dominance.

The theorem does not claim that the recognition action is always strictly larger than the Regge action; for zero deficit angles the two are equal. It does not claim that the recognition path sum converges in the sense of a rigorous functional integral, only that the structural ingredients for UV finiteness hold. It does not establish that the recognition action is the physically correct quantum gravity action, nor that the discrete model reproduces the Einstein-Hilbert action in a continuum limit beyond the approximation stated. The comparison is pointwise on a fixed triangulation with non-negative deficit angles; configurations with negative deficit angles are not covered by this declaration.

/-- 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 σ))

/-- 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δ

/-- **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δ⟩

What this page does not claim

The recognition action is strictly larger than the Regge action for all configurations; they are equal when all deficit angles are zero. The recognition path sum is a rigorously convergent functional integral; only the structural ingredients for UV finiteness are established. The recognition action is the physically correct quantum gravity action, or that it matches any specific experimental prediction.

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: