FundamentalTheoremExistence
plain-language theorem explainer
FundamentalTheoremExistence packages the existence half of the Fundamental Theorem of Pseudo-Riemannian Geometry for a metric tensor g. It requires the Christoffel connection to be torsion-free and to satisfy metric compatibility through the Koszul identity. Discrete-to-continuum bridge work in Recognition Science cites this when lifting lattice models to the Einstein equations. The structure directly records the two properties without further derivation steps.
Claim. For a metric tensor $g$, the structure FundamentalTheoremExistence($g$) asserts that the Christoffel connection is torsion-free, i.e., its coefficients satisfy $Γ^ρ_{μν}=Γ^ρ_{νμ}$, and metric-compatible, i.e., the covariant derivative vanishes: $∇_ρ g_{μν}=0$, which follows from the Koszul identity $g_{σν}Γ^σ_{ρμ}+g_{μσ}Γ^σ_{ρν}=∂_ρ g_{μν}$.
background
The module establishes the Fundamental Theorem of Pseudo-Riemannian Geometry on a pseudo-Riemannian manifold (M,g): there exists a unique torsion-free, metric-compatible connection whose coefficients are the Christoffel symbols. MetricTensor supplies the local bilinear form interface. IsTorsionFree states that a connection Γ is torsion-free precisely when Γ^ρ_{μν}=Γ^ρ_{νμ} for all indices. KoszulIdentity encodes metric compatibility by equating the partial derivative of the metric components to the indicated contractions with the connection coefficients.
proof idea
This is a structure definition that directly packages the two required properties. Torsion-freeness is asserted via the IsTorsionFree predicate on the Christoffel connection. Metric compatibility is asserted by requiring that the Koszul identity implies the covariant derivative of the metric vanishes. No lemmas or tactics are invoked inside the structure itself.
why it matters
The structure supplies the existence component of the Fundamental Theorem and is used to build the combined LeviCivitaCertificate together with the uniqueness half. It is invoked by DiscreteContinuumBridge to certify that the continuum limit of the J-cost lattice recovers the Einstein equations. The module anchors the result in Wald Theorem 3.1.1 and do Carmo Theorem 2.3, placing the classical Levi-Civita connection inside the Recognition Science geometry layer that supports the phi-ladder and eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.