PeriodicFreudenthalRefinementFamily
plain-language theorem explainer
Packages a filter-indexed family of periodic Freudenthal Dirichlet certificates with a uniform error bound and lattice spacing tending to zero. Gravity continuum-limit arguments cite it to obtain pointwise second-order Regge-to-continuum convergence. The companion theorem is a one-line wrapper around the bounded-error vanishing lemma; a second theorem transfers that limit to any fixed continuum action via a squeeze argument.
Claim. A refinement family along a filter $\ell$ on an index type, for an encoded periodic Freudenthal torus $P$ of size $(N_x,N_y,N_z)$, consists of certificates $t\mapsto C_t$ each carrying a lattice spacing $a_t>0$, a continuum comparison action, and an error constant, together with a uniform bound $C_t.\mathrm{error}\le E$ and $a_t\to 0$ along $\ell$. For every vertex potential $\xi$, the second-order Regge action of the canonical Hessian then converges pointwise to $C_t$'s continuum action along $\ell$; if those continuum actions themselves tend to a fixed limit action $L(\xi)$, the Regge action tends to $L(\xi)$.
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 theorem obligations needed to instantiate that model on a periodic torus.
A PeriodicFreudenthalDirichletCertificate is the theorem data identifying an encoded periodic Freudenthal torus with the physical cubic Dirichlet model: a positive lattice spacing, a continuum comparison action on vertex potentials, a nonnegative error constant, and propositional slots for the six-tet cubic decomposition and the canonical-Hessian-is-Dirichlet claim.
The second-order Regge action is evaluated on the canonical Regge Hessian of the torus complex $K$. The dimensionless bridge ratio $K=\varphi^{1/2}$ appears in the ambient constants layer but is not the object of this structure; here the relevant analytic data are the spacing $a_t$ and the uniform error bound.
proof idea
The structure itself is pure data: a certificate map, a uniform error bound, the bound inequality, and spacing tendsto-zero along the filter.
pointwise_converges is a one-line wrapper applying periodicFreudenthalCertificate_error_vanishes_of_bounded_error_and_spacing to the family's certificate map, error bound, bound proof, and spacing hypothesis.
pointwise_converges_to_fixed_limit transfers the spacing-dependent continuum comparison to a fixed continuum action $L$. It rewrites both the Regge-minus-continuum and continuum-minus-$L$ convergences in distance form, adds them, and squeezes $|R-L|\le|R-C_t|+|C_t-L|$ to zero via the triangle inequality and squeeze_zero.
why it matters
This is the abstract refinement interface for Track 1.B continuum comparison on periodic Freudenthal tori. Downstream, canonicalPeriodicEdgeStencilRefinementFamily and canonicalPeriodicEdgeStencilContinuumRefinementFamily construct concrete instances: each spacing gets a canonical periodic edge-stencil certificate with a supplied continuum action and a $C a^2$ estimate; uniform boundedness of the constants is the only analytic hypothesis the wrapper needs.
CanonicalPeriodicFixedContinuumComparisonData packages the remaining fixed-continuum step: future work must supply the fixed continuum action (e.g. Einstein-Hilbert), spacing-dependent comparisons, $C a^2$ estimates, and convergence of the spacing-dependent actions to the fixed one. The transfer theorem here is exactly the glue that turns those data into Regge $\to$ fixed continuum.
In the Recognition gravity stack this sits under the Regge cubic-lattice limit path toward the physical six-tet Dirichlet model, not under the T0-T8 forcing chain directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.