EndToEndChain
plain-language theorem explainer
EndToEndChain packages the DiscreteContinuumBridge certificate with the conditional statement that curvature axioms hold for the Minkowski metric once the lowered Riemann tensor matches its explicit form and the trace vanishes. Researchers tracing the Recognition Science path from the composition law through the forcing chain to the Einstein equations cite this packaging to keep proved and hypothesized steps separate. The declaration is a structure definition that assembles existing fields without invoking any derivation steps.
Claim. Let $B$ be the discrete-to-continuum bridge certificate. EndToEndChain asserts that for every $x : Fin 4 → ℝ$, if the lowered Riemann tensor equals its explicit second-derivative form and the trace over the first index vanishes, then the curvature axioms (pair-exchange symmetry of the Riemann tensor and symmetry of the Ricci tensor) hold for the Minkowski metric tensor.
background
The module connects the J-cost lattice theory of Recognition Science to continuum general relativity by showing how defect-sourced metric perturbations on an $N → ∞$ lattice produce the Einstein field equations in the coarse-graining limit. DiscreteContinuumBridge packages the flat chain from J-cost to the Einstein tensor, positivity of the coupling $8φ^5$, the dimension identity $1+3=4$, torsion-freeness of the Christoffel symbols, and existence plus uniqueness of the Levi-Civita connection for the Minkowski metric.
proof idea
EndToEndChain is a structure definition that directly assembles the DiscreteContinuumBridge field with a lambda expression supplying the curvature axioms under the two explicit hypotheses riemann_lowered_eq_explicit_hypothesis and riemann_trace_vanishes_hypothesis. No lemmas or tactics are applied inside the declaration.
why it matters
This structure supplies the top-level packaging consumed by the end_to_end theorem that instantiates the full chain from the Recognition Composition Law through J-uniqueness, the phi fixed point, the eight-tick octave, D=3, the Minkowski metric, Christoffel symbols, Riemann and Ricci tensors, to the Einstein equations with coupling $κ=8φ^5$. It makes the five external hypotheses (Regge convergence, Schwarz theorem, Jacobi formula, Palatini boundary terms, MP stationarity) visible while keeping them outside the Recognition Science core.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.