christoffel_from_metric
plain-language theorem explainer
The declaration supplies a placeholder for Christoffel symbols tied to an input metric tensor, returning the zero structure in the current build. It is referenced by geodesic uniqueness results and gravity connection theorems that assume a connection. The definition is a direct one-line return of the default zero bundle without any derivative computation.
Claim. For a metric tensor $g$, the associated Christoffel symbols are defined by setting every component identically to zero: $Γ^ρ_{μν}(x) = 0$ for all indices and points $x$.
background
The module supplies structural placeholders for differential geometry objects. MetricTensor is the local non-sealed bilinear form interface whose components default to zero. ChristoffelSymbols is the stub bundle whose $Γ$ entries are identically zero, as defined by its structure with the constant function returning 0.
proof idea
The definition is a one-line wrapper that ignores the input metric and returns the default zero ChristoffelSymbols structure.
why it matters
This placeholder feeds Gravity.Connection.christoffel_from_metric, the symmetry theorem, ConnectionCert, flat_christoffel_vanish, and NullGeodesic constructions. It occupies the connection slot in relativity geometry before a full differential geometry layer exists. The module is explicitly excluded from the certificate chain, leaving open the question of a rigorous embedding of Riemannian geometry into the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.