CanonicalPeriodicFixedContinuumComparisonData
plain-language theorem explainer
Packages the data needed for fixed-continuum comparison of second-order Regge action against a spacing-dependent continuum action on the canonical encoded periodic Freudenthal torus (Nx,Ny,Nz > 2). Gravity workers in Track 1.B cite it to supply C a² estimates, a uniform error bound, and filter convergence of continuum actions to a fixed limit. The structure is pure data; conversion to a refinement family is a one-line field projection.
Claim. A data package over a filter $l$ on index type $\alpha$, for lattice sizes $N_x,N_y,N_z>2$, consisting of: positive mesh spacings $a(t)\to 0$ along $l$; spacing-dependent continuum actions $S_t$ on vertex potentials of the canonical encoded periodic Freudenthal torus; nonnegative error constants $C(t)\le C_\ast$; the estimate $|S_{\mathrm{Regge}}^{(2)}(\xi)-S_t(\xi)|\le C(t)\,a(t)^2$ for every potential $\xi$; a fixed limit action $S_\infty$; and $S_t(\xi)\to S_\infty(\xi)$ along $l$.
background
The module links the encoded periodic Freudenthal torus scaffold to the physical six-tet cubic Dirichlet model. It does not assert the physical Dirichlet equality for free; it packages the exact obligations needed to instantiate that model on a periodic Freudenthal torus.
The second-order Regge action is evaluated with the canonical Regge Hessian on the torus graph $K$. Vertex potentials are real assignments on the vertices of that graph. Mesh refinement is indexed by a filter $l$: spacings tend to zero, and continuum comparison actions are allowed to depend on the refinement parameter.
Upstream, a refinement family is "a refinement-indexed family of physical periodic-Freudenthal certificates with exactly the hypotheses needed for pointwise second-order convergence." The present structure is the fixed-continuum specialization of that package: continuum actions converge to one fixed limit rather than merely forming a Cauchy net.
proof idea
No proof: this is a structure bundling fields (spacing, continuum action, error constants, $C a^2$ estimate, limit action, and continuum convergence).
The companion conversion toRefinementFamily is a one-line wrapper that feeds those fields into canonicalPeriodicEdgeStencilContinuumRefinementFamily. Pointwise Regge-to-limit convergence then applies the corresponding refinement-family convergence lemma with the packaged continuum-tendsto hypothesis. Finite-probe and weighted finite-probe aggregate theorems are tendsto_finset_sum lifts of the pointwise result.
why it matters
This is the remaining fixed-continuum comparison step in Track 1.B. Instantiating Einstein-Hilbert on the periodic Freudenthal torus requires exactly these fields: fixed continuum action, spacing-dependent comparisons, $C a^2$ estimates, bounded constants, and convergence of the spacing-dependent actions to the fixed one.
The finite-probe aggregate is the finite-dimensional precursor to the later pointwise-to-integral lift in Track 1.B; the weighted version supplies the Riemann-sum shape for integral approximations. Together they close the discrete-to-continuum bridge from second-order Regge action on the six-tet cubic lattice toward the physical Dirichlet target, without yet claiming the Einstein-Hilbert identification.
No downstream consumers are wired yet; the structure is the obligation surface future EH instantiations must hit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.