FlatChain
plain-language theorem explainer
FlatChain packages the five vanishing conditions for Christoffel symbols, Riemann tensor, Ricci tensor, scalar curvature, and Einstein tensor on the Minkowski metric. Researchers tracing the J-cost lattice to Einstein equations cite it to fix the flat background. The declaration is a structure that simply aggregates the zero identities already shown for the flat metric in the curvature library.
Claim. The Minkowski metric satisfies $Γ^ρ_{μν}=0$, $R^ρ_{σμν}=0$, $R_{μν}=0$, $R=0$, and $G_{μν}=0$ identically at every point.
background
The module connects the Recognition Science J-cost lattice to continuum general relativity through three tiers. Tier 1 covers the Minkowski flat limit and spatial metric emergence from quadratic defects; Tier 2 assembles the curvature tensors; Tier 3 isolates the external Regge convergence hypothesis. FlatChain belongs to Tier 2 and records the complete vanishing of curvature quantities once the metric is Minkowski. The tensors themselves are defined in Curvature.lean and Gravity.RicciTensor: christoffel extracts symbols from the metric, riemann_tensor forms the curvature from their derivatives and products, ricci_tensor contracts the Riemann tensor, ricci_scalar traces it, and einstein_tensor subtracts half the scalar times the metric.
proof idea
The declaration is a structure definition with no body. It simply names five fields, each an independent universal quantification that the corresponding tensor vanishes on the Minkowski metric. The actual zero identities are supplied later by flat_chain_holds, which fills the fields with lemmas already proved in Curvature.lean.
why it matters
FlatChain supplies the flat-spacetime anchor required by DiscreteContinuumBridge, the top-level certificate that J-cost lattices produce the Einstein field equations after coarse graining. The module doc explicitly traces the chain J(1+ε) quadratic defect to spatial metric to Minkowski to vanishing Einstein tensor. This step confirms the flat background before curvature perturbations and aligns with the Recognition Science forcing chain through T8 (D=3) and the eight-tick octave. It leaves the nonlinear Regge convergence hypothesis untouched.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.