continuum_action
plain-language theorem explainer
Defines the continuum target of the RS cubic lattice action as half the integrated strain: S_cont = ε_int/2. Gravity and Regge-convergence arguments cite it as the weak-field Einstein–Hilbert quadratic limit that the discrete J-cost converges to. The body is a one-line abbreviation, not a proof.
Claim. The continuum action associated to an integrated strain $\varepsilon_{\mathrm{int}}$ is $S_{\mathrm{cont}}(\varepsilon_{\mathrm{int}}) := \varepsilon_{\mathrm{int}}/2$.
background
The module develops Regge convergence on the RS cubic lattice $\mathbb{Z}^3$ without the full Cheeger–Müller–Schrader regularity package. Cubes are identical (shape quality $\sigma=1$), the eight-tick UV cutoff fixes the mesh $a=\ell_0$, and strict convexity of the J-cost supplies energy estimates.
In the weak-field regime the local J-cost admits the expansion $J(e^\varepsilon)=\varepsilon^2/2+O(\varepsilon^4)$, with the quartic remainder bounded by $|\varepsilon|^4/24$. The quadratic piece $\varepsilon^2/2$ is the continuum (Einstein–Hilbert / Laplacian) action density that lattice field theory is expected to recover under Lax-type convergence.
This definition simply packages that continuum target: given an already-integrated strain scalar $\varepsilon_{\mathrm{int}}$, the continuum action is half of it. Sibling material (lattice action, quartic error control, weak-field convergence) uses the same normalization.
proof idea
There is no proof. The declaration is a one-line definition equating the continuum action to half the supplied integrated strain. The factor $1/2$ matches the leading term in the J-cost expansion $J(e^\varepsilon)\approx\varepsilon^2/2$ used throughout the module's weak-field error estimates.
why it matters
It names the continuum limit object that the RS cubic Regge program aims at: the quadratic action recovered once lattice spacing $a\to 0$ in the weak-field regime. The module strategy is (a) treat the J-cost Laplacian on $\mathbb{Z}^3$ as a standard lattice action, (b) invoke second-order Lax convergence, (c) control quartic and higher J-errors by $|J(e^\varepsilon)-\varepsilon^2/2|\le|\varepsilon|^4/24$, and (d) conclude unconditional $O(a^2)$ convergence for $|\varepsilon|<\varepsilon_{\max}$.
Framework landmarks in play are T5 J-uniqueness (the cost whose continuum limit this is), the eight-tick UV cutoff (T7), and $D=3$ spatial structure (T8) that makes the cubic lattice natural. No downstream theorems currently depend on the name; siblings such as weak-field error estimates and RS cubic convergence conditions are the intended consumers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.