end_to_end
plain-language theorem explainer
The theorem constructs the complete end-to-end chain from the discrete J-cost lattice through the Einstein field equations, conditional on the Regge convergence hypothesis. Researchers modeling lattice gravity or emergent continuum spacetime would cite it to close the discrete-to-continuum link. The proof is a direct term construction that applies the bridge certificate theorem and invokes the curvature axioms theorem on the Minkowski tensor.
Claim. Assume the Regge convergence hypothesis: on simplicial manifolds with mesh tending to zero, the Regge action converges to the Einstein-Hilbert action. Then the end-to-end chain exists, consisting of the discrete-to-continuum bridge together with the curvature axioms holding for the Minkowski metric tensor.
background
The module connects the Recognition Science discrete lattice to continuum general relativity via the path J-cost lattice to quadratic defect to lattice Laplacian to Ricci scalar to Einstein tensor to the Einstein field equations. The local setting distinguishes three tiers: proved Minkowski flat limit and curvature chain, plus the external Regge convergence hypothesis packaged explicitly rather than as an axiom.
proof idea
The proof is a term-mode construction of the EndToEndChain structure. It populates the bridge field by applying the bridge_certificate theorem to the supplied Regge hypothesis. The curvature_axioms field is a lambda that calls the curvature_axioms_hold theorem on the Minkowski tensor, using the explicit-form and trace-vanishing hypotheses.
why it matters
This declaration assembles the top-level end-to-end chain in the Recognition framework, closing the path from the Recognition Composition Law through forced constants (phi, D=3, eight-tick octave) and the curvature chain to the Einstein field equations with coupling 8 phi^5. It incorporates the proved tiers documented in the module and leaves the nonlinear Regge convergence as the explicit external hypothesis from Cheeger-Muller-Schrader 1984. The parent structure is EndToEndChain itself, which records the zero-sorry accounting of the full chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.