PathSumWeight
plain-language theorem explainer
Packages the discrete geometric data of a triangulation for the recognition path sum: a finite list of hinges, each with a deficit angle and a positive area. Gravity and discrete-geometry workers cite it as the carrier type for both the sinh-weighted recognition action and the linear Regge comparison. It is a plain structure with a positivity side-condition; no proof content.
Claim. A path-sum weight consists of a natural number $N$ of hinges, deficit angles $\delta_\sigma \in \mathbb{R}$ for $\sigma \in \{0,\ldots,N-1\}$, and hinge areas $A_\sigma \in \mathbb{R}$ with $A_\sigma > 0$ for every hinge.
background
The module treats UV finiteness of the recognition path sum over admissible triangulations of a compact 4-manifold. The sum is
$$Z = \sum_{T:,\mathrm{mesh}(T)\ge \ell_{\mathrm{sub}}} \mu(T),\exp\bigl(i S_{\mathrm{RS}}(T)/\hbar_{\mathrm{RS}}\bigr),$$
with mesh bounded below by the substrate length $\ell_{\mathrm{sub}}$. Continuum EH divergences are framed as artifacts of sending mesh to zero at fixed metric; the recognition substrate never takes that limit.
In the simplicial ledger, curvature lives on codimension-2 hinges (edges in a 3-simplicial ledger). The geometric deficit at a hinge is $2\pi - \sum \theta$, the usual angular defect. The present structure packages one triangulation's hinge data: count, deficits, and positive areas. Downstream, the recognition action replaces the linear Regge weight $\delta$ by $\sinh\delta$ at each hinge, which is the source of the stronger large-curvature suppression used in the UV argument.
proof idea
No proof: this is a structure definition. Fields are the hinge count, the deficit-angle map, the area map, and the positivity hypothesis on areas. Downstream definitions unfold those fields into finite sums; the positivity field is available whenever a comparison needs $A_\sigma > 0$.
why it matters
This is the carrier type for the discrete action comparison that underwrites UV finiteness of the recognition path sum. recognitionAction and reggeAction are defined by summing $A_\sigma\sinh\delta_\sigma$ and $A_\sigma\delta_\sigma$ over its hinges; recognition_dominates_regge then shows the sinh action dominates the linear Regge action for nonnegative deficits. That domination is one of the three pillars of PathSumUVBoundCert (finite triangulation count, positive min mesh, sinh dominates linear). In the module's framing, continuum perturbative non-renormalizability of EH gravity assumes a mesh-to-zero limit the recognition substrate never takes; the packaged hinge data make the discrete comparison precise.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.