DiscreteContinuumBridge
plain-language theorem explainer
The DiscreteContinuumBridge structure packages the flat spacetime chain from J-cost lattices through Minkowski geometry to vanishing Einstein tensor, together with the coupling 8 phi^5, four-dimensional spacetime, torsion-free Levi-Civita connection on Minkowski, and the external Regge convergence hypothesis. A researcher tracing the Recognition Science lattice to continuum GR limit would cite this certificate when closing the derivation of the Einstein field equations. It is assembled as a single Prop by direct conjunction of the tiered fields
Claim. The structure asserts the conjunction of: the flat spacetime chain (J-cost expansion to Minkowski metric with vanishing Christoffel, Riemann, Ricci, scalar, and Einstein tensors), positivity of the coupling constant $8 phi^5$, spacetime dimension four, torsion-freeness of the Christoffel symbols for the Minkowski metric tensor, existence and uniqueness of the Levi-Civita connection on the Minkowski tensor, and the Regge convergence hypothesis that simplicial Regge actions converge to the Einstein-Hilbert action as mesh size tends to zero.
background
The module establishes the discrete-to-continuum bridge by the chain J-cost lattice sites with defects to quadratic metric perturbations, lattice Laplacian, Ricci scalar, Einstein tensor, and finally the Einstein field equations in the coarse-graining limit. FlatChain is the structure recording that the Minkowski metric yields identically zero Christoffel symbols, Riemann tensor, Ricci tensor, scalar curvature, and Einstein tensor. ReggeConvergenceHypothesis is the external statement that, for invertible metric tensors, the Regge action on a sequence of simplicial manifolds with mesh tending to zero converges to the Einstein-Hilbert action (Cheeger-Muller-Schrader 1984). Upstream results include the Christoffel definition from the Euler-Lagrange action and the flat-chain construction from ContinuumManifoldEmergence.
proof idea
This is a structure definition that directly packages the six named fields; the first three are drawn from the proved flat-chain and coupling lemmas in the same module, the next three from the curvature and Levi-Civita results in the imported Curvature and LeviCivitaTheorem modules, and the final field is the explicit Regge hypothesis.
why it matters
It supplies the central certificate used by bridge_certificate (which inhabits the structure once the Regge hypothesis is assumed) and by EndToEndChain (which traces the full path from the Recognition Composition Law through J-uniqueness, phi fixed point, D=3, eight-tick octave, Minkowski geometry, curvature tensors, and coupling kappa = 8 phi^5 to the Einstein equations). The declaration therefore closes the discrete lattice to continuum GR link inside the Recognition framework while isolating the single external mathematical hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.