FlatChain
FlatChain packages the flat-spacetime conditions that close the J-cost to Einstein-tensor chain in the discrete-to-continuum bridge. Researchers assembling the Recognition Science gravity limit cite it when they need the Minkowski anchor for the full bridge certificate. The structure simply collects five independent vanishing statements, each already established by direct substitution into the curvature definitions supplied by the Curvature module.
claimThe flat spacetime chain holds when the Minkowski metric tensor satisfies $Γ^ρ_{μν}(η,x)=0$, $R^ρ_{σμν}(η,x)=0$, $R_{μν}(η,x)=0$, $R(η,x)=0$, and $G_{μν}(η,x)=0$ for all coordinates and index combinations.
background
The DiscreteBridge module connects the J-cost lattice of Recognition Science to continuum GR by routing lattice defects through a quadratic metric perturbation to the Einstein tensor. Tier 1 supplies the Minkowski flat limit and spatial metric from J-cost; Tier 2 derives the curvature tensors; Tier 3 isolates the external Regge convergence hypothesis. The structure FlatChain sits in Tier 2 and records the complete vanishing of curvature for the flat metric η = diag(−1,+1,+1,+1). Upstream definitions in Curvature.lean give the Christoffel symbols via the standard formula involving the inverse metric and partial derivatives of g, the Riemann tensor via the usual commutator of covariant derivatives plus quadratic terms, the Ricci tensor as its single contraction, the scalar as the trace, and the Einstein tensor as R_{μν} − (1/2) R g_{μν}.
proof idea
FlatChain is a structure definition with no body. Its five fields are instantiated in the companion theorem flat_chain_holds by direct appeal to the five zero lemmas minkowski_christoffel_zero_proper, minkowski_riemann_zero, minkowski_ricci_zero, minkowski_ricci_scalar_zero, and minkowski_einstein_zero, each obtained by substituting the constant Minkowski components into the general curvature expressions.
why it matters in Recognition Science
FlatChain supplies the flat anchor required by the parent structure DiscreteContinuumBridge, which certifies that an N→∞ J-cost lattice produces the Einstein field equations after coarse-graining. It completes the Tier 2 segment of the module’s three-tier architecture and aligns with the Recognition Science forcing chain at the point where D=3 spatial dimensions and the eight-tick octave are already fixed. The declaration therefore closes the linear flat limit before the nonlinear Regge hypothesis is invoked.
scope and limits
- Does not prove convergence of the nonlinear Regge lattice to the Einstein-Hilbert action.
- Does not derive the metric perturbation from the underlying J-cost lattice; that step is upstream.
- Does not treat curved backgrounds or weak-field expansions beyond the exact flat case.
- Does not supply numerical lattice simulations or error bounds.
- Does not claim that Minkowski is the unique metric satisfying the listed vanishing conditions.
formal statement (Lean)
80structure FlatChain : Prop where
81 minkowski_christoffel : ∀ x ρ μ ν,
82 christoffel minkowski_tensor x ρ μ ν = 0
83 minkowski_riemann : ∀ x up low,
84 riemann_tensor minkowski_tensor x up low = 0
85 minkowski_ricci : ∀ x up low,
86 ricci_tensor minkowski_tensor x up low = 0
87 minkowski_scalar : ∀ x,
88 ricci_scalar minkowski_tensor x = 0
89 minkowski_einstein : ∀ x up low,
90 einstein_tensor minkowski_tensor x up low = 0
91
92/-- The flat chain holds. All fields proved in `Curvature.lean`. -/