recognitionAction
plain-language theorem explainer
Defines the recognition action on a triangulation weight as the sum over hinges of area times sinh of the deficit angle. Gravity and path-sum workers cite it as the discrete RS action that replaces the linear Regge action. The body is a direct Finset sum; no proof content beyond the formula.
Claim. Given a path-sum weight $w$ (hinge count, deficit angles $\delta_\sigma$, and positive hinge areas $A_\sigma$), the recognition action is $S_{\mathrm{RS}}(w) = \sum_\sigma A_\sigma \, \sinh(\delta_\sigma)$.
background
This module treats UV finiteness of the recognition path sum on a compact 4-manifold: $Z = \sum_{T:,\mathrm{mesh}(T)\ge\ell_{\mathrm{sub}}} \mu(T),\exp(i S_{\mathrm{RS}}(T)/\hbar_{\mathrm{RS}})$. The continuum EH path integral is never taken; mesh is bounded below by the substrate length $\ell_{\mathrm{sub}}$.
A path-sum weight packages the discrete geometric data at one triangulation: finitely many hinges, deficit angles $\delta_\sigma$ at each hinge, and positive hinge areas $A_\sigma$. Upstream geometry defines the hinge deficit as $2\pi - \sum\theta$ (dihedral and Schläfli packages). The classical Regge action is linear in those deficits; recognition replaces the linear factor by $\sinh$.
The module argument is structural: finite Tutte-type triangulation count at fixed volume and mesh floor, plus sinh suppression of large local curvature relative to Regge.
proof idea
Definitional one-liner. Unfold the weight fields and form the Finset sum $\sum_\sigma A_\sigma\sinh(\delta_\sigma)$. No lemmas are applied; noncomputable only because Real.sinh is.
why it matters
This is the discrete action $S_{\mathrm{RS}}$ inside the recognition path sum. It feeds recognition_dominates_regge, which states that for nonnegative deficits the recognition action is at least the Regge action, and it is the action side of the UV-finiteness certificate (finite triangulation count, positive min mesh, and $\delta\le\sinh\delta$ for $\delta\ge 0$).
In the module narrative, continuum perturbative non-renormalizability of EH gravity is an artifact of sending mesh to zero at fixed metric. Recognition never takes that limit: physical mesh is $\ell_{\mathrm{sub}}$, and EH is an approximation to this sinh-weighted discrete action. Downstream path-sum measure work also treats weights built from this action when descending $Z$ to triangulation classes.
Framework contact is the gravity sector of the discrete recognition ledger, not the T0–T8 forcing chain directly; the eight-tick and $\phi$ landmarks enter only through the ambient RS units and substrate cutoff assumed by the path sum.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.