reggeAction
plain-language theorem explainer
Defines the classical Regge action on a path-sum weight as the sum over hinges of area times deficit angle. Gravity and discrete-geometry workers cite it as the linear baseline against the sinh-weighted recognition action. The body is a direct Finset sum; no lemmas are needed.
Claim. Given a path-sum weight $w$ with hinge areas $A_\sigma>0$ and deficit angles $\delta_\sigma$, the Regge action is $S_{\mathrm{Regge}}(w)=\sum_\sigma A_\sigma\,\delta_\sigma$.
background
The module studies UV finiteness of the recognition path sum on a compact 4-manifold: a sum over admissible triangulations with mesh bounded below by the substrate length $\ell_{\mathrm{sub}}$. Continuum Einstein–Hilbert divergences are treated as artifacts of sending the mesh to zero at fixed metric; the recognition substrate never takes that limit.
A path-sum weight packages the discrete curvature data at a triangulation: a finite hinge index set, deficit angles $\delta_\sigma$ at each hinge, and positive hinge areas $A_\sigma$. Upstream geometry defines the deficit as $2\pi-\sum\theta$ (dihedral angles around the hinge), matching the classical Regge curvature measure.
The recognition action replaces the linear factor $\delta$ by $\sinh\delta$ at each hinge. This definition supplies the linear Regge counterpart used for magnitude comparison and for sinh-suppression arguments when deficits are large.
proof idea
Pure definition: unfold to the finite sum $\sum_\sigma A_\sigma,\delta_\sigma$ over the hinge index type of the weight. No tactics, no lemmas, no noncomputable choice beyond the ambient real arithmetic.
why it matters
This is the linear baseline in the UV-finiteness argument. The sibling comparison that recognition magnitude dominates Regge magnitude (when deficits are nonnegative) uses exactly this sum against the sinh-weighted recognition action; large local curvature is then exponentially more suppressed in the recognition path sum than in Regge.
Downstream, concrete 3D Regge action data, second-order Taylor remainders, and Hessian packages in the geometry layer reuse the same area–deficit product shape. The forcing-chain bridge from T5 (J-cost uniqueness, $J(x)=(x+x^{-1})/2-1$) toward a nonlinear Regge curvature action also cites this linear form as the comparison object. In short, it anchors the claim that continuum EH non-renormalizability is an artifact of the zero-mesh limit the recognition substrate refuses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.