recognition_dominates_regge
plain-language theorem explainer
When all deficit angles are non-negative, the recognition path-sum action is at least the classical Regge action, hinge by hinge. Discrete-gravity and path-integral workers comparing sinh-weights to Einstein-Hilbert/Regge weights would cite it. The proof is a finite-sum comparison: multiply the elementary inequality $x\le\sinh x$ (for $x\ge 0$) by positive hinge areas.
Claim. Let $w$ assign to each hinge $\sigma$ a positive area $A_\sigma>0$ and a deficit angle $\delta_\sigma\in\mathbb{R}$. If $\delta_\sigma\ge 0$ for every hinge, then the Regge action is at most the recognition action: $\sum_\sigma A_\sigma\,\delta_\sigma \le \sum_\sigma A_\sigma\,\sinh(\delta_\sigma)$.
background
This 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 diverges under mesh $\to 0$; the recognition sum never takes that limit.
A path-sum weight packages the discrete geometric data at one triangulation: finitely many hinges, deficit angles $\delta_\sigma$, and strictly positive hinge areas $A_\sigma$. The classical Regge action is $\sum A_\sigma\delta_\sigma$. The recognition action replaces the linear deficit by a hyperbolic one, $\sum A_\sigma\sinh(\delta_\sigma)$, so large local curvature is more strongly suppressed.
The comparison $x\le\sinh x$ for $x\ge 0$ is the elementary real-analysis input. Combined with $A_\sigma>0$, it lifts termwise to the two actions and feeds the structural UV-finiteness certificate in this file.
proof idea
Unfold both actions to finite sums over hinges. Apply Finset.sum_le_sum and reduce to a per-hinge inequality. For each hinge $\sigma$, use mul_le_mul_of_nonneg_left with the positivity of the hinge area, and discharge the scalar comparison via Real.self_le_sinh_iff applied to the hypothesis $\delta_\sigma\ge 0$. No induction or continuum limit appears; the argument is pure termwise comparison of real sums.
why it matters
This is the action-level half of the sinh-suppression clause in the UV finiteness argument for the recognition path sum. Downstream it is wired into pathSumUVBoundCert as the field recognition_dominates, alongside the finite triangulation-count bound, positive minimum mesh, and the scalar self_le_sinh fact.
In the module narrative, continuum perturbative non-renormalizability of Einstein-Hilbert gravity is an artifact of sending the mesh to zero at fixed metric. The recognition substrate keeps mesh $\ge\ell_{\mathrm{sub}}$ and uses $\sinh\delta$ rather than $\delta$, so configurations with large deficit angles are exponentially more suppressed than in Regge calculus. The inequality proved here is exactly that dominance of recognition over Regge under non-negative deficits, and is cited as item 3 of the UV-finiteness structural theorem in this file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.