CanonicalPeriodicFixedPhysicalActionComparisonData
plain-language theorem explainer
Data package for the fixed-action Track 1.B step: lattice spacing a(t)→0, a fixed continuum action S_∞ on the canonical periodic Freudenthal torus, and uniform O(a²) bounds between the second-order Regge action and S_∞. Anyone closing the physical six-tet cubic Dirichlet/EH continuum limit cites this interface. Pure structure definition; analytic content is the estimate field, not a proof.
Claim. A comparison-data package on a filter base $\alpha$ for lattice sizes $N_x,N_y,N_z>2$: a positive spacing $a(t)\to 0$, a fixed continuum action $S_\infty$ on vertex potentials of the canonical encoded periodic Freudenthal torus, a nonnegative error factor $C(t)$ bounded by a uniform constant, and the pointwise estimate $|S_{\mathrm{Regge}}^{(2)}(\xi)-S_\infty(\xi)|\le C(t)\,a(t)^2$ for every vertex potential $\xi$.
background
The module links the encoded periodic Freudenthal torus scaffold to the physical six-tet cubic Dirichlet model. It does not give the physical Dirichlet equality for free; it packages the exact obligations needed to instantiate that model on a periodic Freudenthal lattice with $N_x,N_y,N_z>2$.
The fixed continuum action type is just a real functional on vertex potentials of the canonical encoded torus; the analytic burden sits in comparison-data structures. The more general Track 1.B package allows a spacing-dependent continuum action plus convergence to a limit action. The present structure specializes that package to a single fixed physical Dirichlet/EH candidate $S_\infty$, so only spacing-dependent $C a^2$ estimates remain.
Second-order Regge action is evaluated with the canonical Regge Hessian on that torus. Spacing positivity and $a(t)\to 0$ are the continuum-limit bookkeeping shared with the general comparison data.
proof idea
Definitional structure: six field groups (spacing with positivity and filter limit, fixed action, error constant with nonnegativity and uniform bound, and the $O(a^2)$ estimate). No proof body.
The companion coercion fills the general fixed-continuum comparison package by setting both the spacing-dependent continuum action and the limit action equal to the fixed action, then discharges continuum convergence by constant-net tendsto. Downstream pointwise and finite-probe residual theorems are one-line wrappers through that coercion into the general Track 1.B residual lemmas.
why it matters
This is the interface for the physical Dirichlet/Einstein-Hilbert step of Track 1.B once $S_\infty$ is chosen and only mesh-dependent $C a^2$ estimates remain. It specializes the general fixed-continuum comparison package to the physical six-tet cubic Dirichlet instance on the canonical periodic Freudenthal torus.
Methods on the package give pointwise Regge convergence to the fixed action and fixed- or variable-weight finite-probe residual convergence to zero (the direct Riemann-sum hook). Those are the continuum-limit obligations the module was built to expose, not free theorems.
In the broader RS gravity chain this sits under the $D=3$ spatial lattice and the Regge-to-continuum correspondence imports. No graph dependents yet; the open work is supplying concrete spacing families and proving the estimate field for a genuine EH/Dirichlet $S_\infty$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.