Gravity Path Sum Uvbound Sinh Dominates Linear

The suppression inequality

The hyperbolic sine function, written sinh, grows faster than its input. For any non-negative number δ, the value of sinh(δ) is at least δ. The formal statement sinh_dominates_linear in the framework's machine-checked library proves exactly this: δ ≤ sinh(δ) whenever 0 ≤ δ. The proof is a direct appeal to a standard real-analysis fact; it is a theorem about ordinary mathematics, not a claim about physics by itself.

The inequality matters in a specific model of quantum gravity. The framework's path sum for gravity is a sum over triangulations, or discrete subdivisions, of a four-dimensional space. Each triangulation has hinges where edges meet, and each hinge carries a deficit angle δ, a measure of how much local curvature is concentrated there. In the classical Regge action, the contribution of a hinge is proportional to δ. In the framework's recognition action, the contribution is proportional to sinh(δ). The theorem shows that the recognition action is at least as large as the Regge action for every hinge with a non-negative deficit angle, and much larger when δ is large.

That gap is the mechanism behind a proposed ultraviolet finiteness result. In the continuum path integral for Einstein-Hilbert gravity, short-distance fluctuations drive divergences. The framework's path sum never takes the mesh to zero: a minimum length ℓ_sub cuts off the triangulations, and the sinh suppression makes high-curvature configurations exponentially rare. The library packages the ingredients, including the sinh inequality, into a structural certificate of finiteness. The statement is a structural theorem: it assembles the pieces, but the physical claim that this discrete sum is the correct theory of gravity is not part of the theorem.

What the inequality does not claim is equally precise. It does not say that sinh(δ) is strictly greater than δ; the proved version is weak, with equality at δ = 0. It does not assert that the suppression ratio sinh(δ)/δ is monotone, a stronger property that the library marks as a statement with the proof deferred. And it does not, by itself, prove that the recognition path sum is finite: the full finiteness argument also needs the finite count of triangulations and the positive minimum mesh, which are separate hypotheses in the certificate.

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

theorem pathSumUVBoundCert_inhabited :
    Nonempty PathSumUVBoundCert :=
  ⟨pathSumUVBoundCert⟩

What this page does not claim

The theorem does not prove that the recognition path sum is physically correct or that it describes actual quantum gravity. It does not establish strict inequality sinh(δ) > δ for positive δ, only the weak version with equality at zero. It does not prove the monotonicity of the suppression ratio sinh(δ)/δ, which remains a deferred statement.

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: