CanonicalPeriodicFiniteEHDirichletLimitWeightRefinementData
plain-language theorem explainer
Packages mesh refinement data for the periodic Freudenthal torus so that finite EH/Dirichlet aggregates are identified with a continuum Einstein–Hilbert integral at the limiting weights. Gravity workers cite it when they prefer to prove weight convergence first, then equality of the limiting aggregate to the continuum value. The structure is pure data: spacing schedule, probes, weights, and the limit-weight integral target.
Claim. A refinement package over a filter $l$ on index type $\alpha$, for lattice sizes $N_x,N_y,N_z>2$, consists of: a finite probe family of vertex potentials on the canonical encoded periodic Freudenthal torus; mesh weights $w_t$ and limiting weights $w_\infty$; a spacing schedule $h(t)\to 0$ with $h(t)\neq 0$ eventually; a supplied continuum EH integral $I$; and the requirement that the finite EH/Dirichlet aggregate of the probes at $w_\infty$ equals $I$.
background
This module wires 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 torus.
The continuum target is deliberately a bare real: CanonicalPeriodicContinuumEHIntegral is just $\mathbb{R}$, with the analytic content living in the Riemann-sum (or limiting-aggregate) hypothesis that identifies finite EH/Dirichlet aggregates with that value. The finite aggregate itself is the weighted sum of the Dirichlet/EH stencil over a fixed probe family.
The stronger identification used here, CanonicalPeriodicFiniteEHDirichletLimitWeightIntegralTarget, says that after mesh weights converge, equality of the limiting finite aggregate to the continuum integral is enough to feed the finite-to-integral bridge. Lattice sizes satisfy $N_x,N_y,N_z>2$ so the periodic edge stencil is well-defined; spatial dimension $D=3$ is the ambient RS setting (T8/T9).
proof idea
No proof: this is a structure bundling fields. Downstream, toIntegralRefinementData converts it into the explicit Riemann-sum package by applying canonicalPeriodicFiniteEHDirichletToContinuumIntegralTarget_of_limitWeightIntegralTarget (mesh-weight convergence plus the limiting-aggregate equality yield the full finite-to-integral target). The companion theorem fullRegge_tendsto_continuumIntegral is then a one-line wrapper through that conversion into the integral-refinement bridge, which itself adds the residual vanishing of full nonlinear Regge versus finite EH/Dirichlet to the aggregate convergence.
why it matters
Track 1.B finite-to-integral layer for gravity on the canonical periodic Freudenthal torus. The usable theorem shape is: prove weights tend to limits, prove the limiting finite EH/Dirichlet aggregate equals the continuum integral, then obtain full nonlinear Regge convergence (normalized by $|h|^2$) to the same integral, conditional on local edge-stencil correspondence.
It feeds CanonicalPeriodicFiniteEHDirichletQuadratureRefinementData, which specializes further to a named quadrature rule whose fixed weights supply the finite integral proxy. That path is how the module closes obligations toward PhysicalSixTetCubicDirichletModel without claiming the final manifold EH theorem. Framework landmarks in view: $D=3$ spatial dimensions and the Regge–continuum correspondence on the eight-tick / cubic lattice geometry; the package is scaffolding for the continuum limit, not a mass or $\alpha$ derivation step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.