sinh_over_linear_monotone_statement
plain-language theorem explainer
For every real deficit angle δ ≥ 0, the linear bound is dominated by the hyperbolic sine: δ ≤ sinh(δ). Gravity path-sum arguments cite this to justify that recognition hinge weights (built from sinh of deficit) sit above the corresponding Regge weights. The proof is a one-line term application of Mathlib's self_le_sinh_iff.
Claim. For every real number $\delta$ with $\delta \ge 0$, one has $\delta \le \sinh\delta$.
background
The module treats UV finiteness of the recognition path sum on a compact 4-manifold: a sum over admissible triangulations whose mesh is bounded below by the substrate length $\ell_{\mathrm{sub}}$. The continuum Einstein–Hilbert path integral is replaced by a discrete sum whose action uses hyperbolic sine of hinge deficits rather than the deficits themselves.
A hinge deficit is the usual angular defect $2\pi - \sum\theta$ (DihedralAngle / Schläfli). The Regge action is linear in those deficits; the recognition action replaces each factor $\delta$ by $\sinh\delta$. The elementary comparison $\delta\le\sinh\delta$ on the nonnegative reals is the analytic seed of that replacement.
Mathlib already records the classical inequality as Real.self_le_sinh_iff; the present declaration simply packages the nonnegative direction for the gravity development.
proof idea
Term-mode one-liner. The proof is the function
fun δ hδ => Real.self_le_sinh_iff.mpr hδ,
i.e. it applies the Mathlib biconditional that characterises $\delta\le\sinh\delta$ precisely by nonnegativity of $\delta$, and discharges the hypothesis with the given $0\le\delta$.
why it matters
Sinh suppression is the third pillar of the module's UV-finiteness argument (alongside the Tutte-type triangulation count bound and the hard mesh cutoff $\ell_{\mathrm{sub}}$). Because $\sinh\delta\ge\delta$ for $\delta\ge 0$, and grows much faster for large curvature, configurations with large local deficit are exponentially more suppressed in the recognition path sum than in the ordinary Regge sum.
Sibling declarations (sinh_dominates_linear, sinh_weakly_dominates, recognition_dominates_regge, uv_finiteness_structural) build the full comparison of actions and the structural finiteness theorem on top of this inequality. The doc-comment also sketches the stronger claim that the ratio $\sinh\delta/\delta$ is monotone for $\delta>0$ (via $\tanh\delta\le\delta$); that derivative argument is not formalised here and is flagged as deferred. No downstream used_by edges are recorded yet, so the lemma presently serves the in-module path-sum development.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.