ChristoffelSymbols
plain-language theorem explainer
A structure bundles the connection coefficients as a four-index tensor that defaults to zero on all spacetime points and index combinations. It acts as the base type for connection objects in the relativity geometry placeholders. The definition proceeds by direct initialization to the constant zero function.
Claim. The connection coefficients form a structure where the map from a point in four-dimensional space and three indices to a real number evaluates to zero for all inputs.
background
This module supplies placeholder definitions for Christoffel symbols and covariant derivatives in relativity geometry. The structure holds a map from points in four-dimensional space and three indices to real numbers, defaulting to zero. The module documentation states that this is a scaffold module not part of the verified certificate chain, and that all symbols default to zero with covariant derivatives collapsing to zero. These serve as structural placeholders rather than rigorous differential geometry.
proof idea
The structure is introduced by a direct definition that sets the field to the constant zero function on all arguments.
why it matters
It supplies the type used by the definitions of the metric-derived connection and the symmetry predicate in the same module. As a scaffold, it supports compilation of the relativity geometry layer while the actual theory remains outside the main Recognition Science certificate chain. It relates to the broader effort to embed differential geometry into the framework but highlights the current separation of placeholder code from verified results.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.