ReggeConvergenceHypothesis
plain-language theorem explainer
The declaration encodes the external hypothesis that Regge action on simplicial manifolds with mesh tending to zero converges to the Einstein-Hilbert action for smooth metrics. Lattice-to-continuum researchers in discrete gravity would cite it to close the Recognition Science bridge from J-cost defects to Einstein equations. The definition asserts existence of a positive rate under pointwise metric invertibility, with the explicit error bound left as a placeholder.
Claim. For every metric tensor $g$ invertible at each point there exists a positive real rate such that the Regge action $S_ {Regge}[T_N]$ on simplicial manifolds $T_N$ with mesh size to zero converges to the Einstein-Hilbert action $S_{EH}[g]$ at that rate.
background
The Discrete-to-Continuum Bridge module links J-cost lattices to continuum curvature. J-cost is the cost induced by multiplicative recognizers and equals the defect functional for positive arguments; defects source quadratic metric perturbations. MetricTensor supplies a local non-sealed bilinear form on four-dimensional spacetime, while the invertibility predicate ensures non-degeneracy at each point. Upstream results include the defect definition from LawOfExistence (equals J with zero at unity) and cost predicates from ObserverForcing and MultiplicativeRecognizerL4. The module separates proved tiers (flat chain, curvature tensors via LeviCivitaTheorem) from this Tier 3 external hypothesis on Regge convergence, citing Cheeger-Muller-Schrader 1984 on piecewise flat curvature.
proof idea
The declaration is a direct definition of the Prop. It quantifies over MetricTensor, applies the pointwise invertibility condition, and asserts existence of a positive rate with the convergence inequality replaced by True as placeholder. No lemmas or tactics are invoked beyond the structural assumptions imported from Hamiltonian and Gravity modules.
why it matters
This hypothesis supplies the Tier 3 nonlinear convergence step required by the bridge_certificate theorem and the end_to_end chain. It allows J-cost lattice sites with defect perturbations to recover the Einstein field equations in the coarse-graining limit, consistent with D=3 and coupling 8 phi^5. The framework treats it as external mathematics (Cheeger-Muller-Schrader 1984), analogous to smoothness packages elsewhere, and leaves open the question of discharging it via future Mathlib formalization of Regge calculus.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.