sinh_dominates_linear
plain-language theorem explainer
For every nonnegative real deficit angle, the linear weight is at most the hyperbolic sine. Path-sum and Regge-comparison arguments in recognition gravity cite this elementary bound to justify sinh hinge weights. The proof is a one-line reverse application of Mathlib's self-le-sinh biconditional.
Claim. For every real number $\delta\ge 0$, one has $\delta\le\sinh\delta$.
background
The recognition path sum on a compact 4-manifold sums over admissible triangulations with mesh bounded below by the substrate length $\ell_{\mathrm{sub}}$:
$$Z=\sum_{T:,\mathrm{mesh}(T)\ge\ell_{\mathrm{sub}}}\mu(T),\exp\bigl(i S_{\mathrm{RS}}(T)/\hbar_{\mathrm{RS}}\bigr).$$
UV finiteness in this module rests on three pillars: a Tutte-type exponential bound on triangulation count at fixed simplex budget, the hard mesh floor, and sinh suppression at hinges. Classically the Regge action is linear in the deficit angle $\delta$. The recognition action replaces $\delta$ by $\sinh\delta$ at each hinge. For small curvature $\sinh\delta\sim\delta$, so the continuum limit is unchanged; for large $|\delta|$, $\sinh\delta\gg\delta$, so high-curvature configurations are exponentially more suppressed than in Regge gravity. The present lemma is the elementary comparison $\delta\le\sinh\delta$ on the nonnegative ray that underwrites that replacement.
proof idea
One-line term proof. Mathlib supplies the biconditional Real.self_le_sinh_iff, which states $0\le x\leftrightarrow x\le\sinh x$. Applying the reverse direction (.mpr) to the hypothesis $0\le\delta$ yields $\delta\le\sinh\delta$ at once. No series expansion or calculus is unfolded here.
why it matters
This is the base comparison behind the module's third UV-finiteness pillar (sinh suppression of large local curvature). Sibling lemmas strengthen it: a weak dominance form, a monotone ratio $\sinh\delta/\delta$, and the hingewise claim that the recognition action dominates the Regge action. Those feed the structural UV-finiteness theorem for the recognition path sum. In the broader framework the point is that continuum Einstein-Hilbert non-renormalizability assumes sending the mesh to zero at fixed metric; the recognition substrate never takes that limit, keeps mesh $\ge\ell_{\mathrm{sub}}$, and damps large deficits by $\sinh$ rather than by the linear Regge weight. No external used_by edges are recorded yet; the natural consumers sit in the same module (recognition_dominates_regge, uv_finiteness_structural).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.