abstract_regge_action
plain-language theorem explainer
On the flat substrate the abstract Regge action is the zero function of lattice spacing. Track 1.B cites it as the canonical witness that Regge and Einstein-Hilbert actions agree before any residual bound is proved. The definition is constant zero by design; the spacing argument is deliberately unused.
Claim. The abstract Regge action $S_{\mathrm{Regge}}(a)$ is defined by $S_{\mathrm{Regge}}(a) := 0$ for every lattice spacing $a \in \mathbb{R}$.
background
Track 1.B/1.C of the gravity master theorem packages two structural inputs: discrete-to-continuum convergence of the Regge action to the Einstein-Hilbert (EH) action, and the contracted second Bianchi identity on the Regge substrate. Both are shipped under named geometric hypotheses, with a flat-substrate canonical witness supplying non-vacuous inhabitation.
Regge calculus replaces the continuum curvature integral by a sum of deficit angles times hinge areas on a simplicial lattice. On a flat triangulation every deficit vanishes, so the Regge action is identically zero at every spacing. The companion abstract EH action is likewise zero on flat space. Lattice spacing itself is the usual refinement quantity $L/N$ from the unified lattice-manifold correspondence; here it is only a formal parameter.
The structural continuum Prop then asks only that the two abstract actions agree for every spacing. On the flat witness that equality is $0=0$.
proof idea
Pure definition: the body is the constant real $0$. The spacing parameter is bound and ignored, matching the doc-comment that the flat substrate has vanishing Regge action for any spacing. No lemmas are applied.
why it matters
This definition is the Regge half of the flat canonical witness for Track 1.B. Downstream, regge_eh_continuum_structural_prop is the Prop $\forall a,, S_{\mathrm{Regge}}(a)=S_{\mathrm{EH}}(a)$, and regge_eh_continuum_canonical_witness proves it by unfolding both abstract actions to $0$ and closing by reflexivity. That witness inhabits the master-theorem hypothesis RegEHContinuumAndBianchi together with the discrete Bianchi structural piece.
In the Recognition gravity program this is kinematic scaffolding, not the physical residual bound $|S_{\mathrm{Regge}}-S_{\mathrm{EH}}|\le C\cdot a$. Unconditional Track 1.B still needs the geometric residual proof on a genuine physical triangulation. The flat zero-action witness only shows the structural Prop is inhabited and the continuum statement is well-typed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.