sinh_weakly_dominates
plain-language theorem explainer
For every positive real deficit angle δ, hyperbolic sine weakly dominates the linear term: δ ≤ sinh(δ). Gravity path-sum arguments cite this to justify that the recognition hinge weight is at least the Regge weight. The proof is a one-line Mathlib application of the self-le-sinh characterization after weakening strict positivity to a nonstrict bound.
Claim. For every real number $\delta > 0$, one has $\delta \le \sinh\delta$.
background
The module treats UV finiteness of the recognition path sum on a compact 4-manifold. The sum runs over admissible triangulations whose mesh is bounded below by the substrate length $\ell_{\mathrm{sub}}$, with weights $\mu(T)\exp(i S_{\mathrm{RS}}(T)/\hbar_{\mathrm{RS}})$. Continuum Einstein-Hilbert loop divergences are framed as artifacts of sending the mesh to zero at fixed metric; the recognition substrate never takes that limit.
At each hinge the geometric deficit is $\delta = 2\pi - \sum\theta$. Classical Regge calculus inserts the linear deficit into the action. Recognition calculus replaces that linear term by $\sinh\delta$. For large curvature the hyperbolic sine grows much faster than the identity, so highly curved configurations are exponentially more suppressed than in the Regge sum.
The present lemma supplies the elementary comparison $\delta\le\sinh\delta$ on the positive ray that underwrites that suppression. A sibling records the strict gap coming from the cubic and higher terms of the power series; another sibling packages monotonicity of the ratio $\sinh\delta/\delta$.
proof idea
One-line term proof. Mathlib already proves the biconditional $x\le\sinh x\leftrightarrow 0\le x$. The argument applies the reverse direction of that characterization to the nonstrict inequality obtained from the hypothesis $0<\delta$ by le_of_lt. No series expansion or calculus is unfolded here.
why it matters
Sinh suppression is the third pillar of the module's UV-finiteness claim, alongside the Tutte-type bound on triangulation count and the hard mesh floor $\ell_{\mathrm{sub}}$. The weak comparison proved here is the minimal analytic input needed before one can assert that the recognition action dominates the Regge action hingewise (sibling recognition_dominates_regge) and before the structural finiteness theorem for the path sum.
In the broader Recognition framework this is geometry-side support for the claim that continuum non-renormalizability of Einstein-Hilbert gravity is an artifact of an illicit continuum limit, not a feature of the discrete recognition dynamics. The forcing chain (T5 J-cost, T7 eight-tick, T8 $D=3$) is upstream infrastructure; this lemma sits downstream in the gravity layer and does not reopen those steps. The graph currently lists no direct dependents, but the sibling cluster makes the intended use site unambiguous.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.