Idx
plain-language theorem explainer
Idx supplies the four-element index set for labeling spacetime coordinates in the local coordinate treatment of the Levi-Civita connection. It is referenced by every metric-tensor and Christoffel-symbol construction in the Gravity.Connection module. The declaration is a direct abbreviation of the standard four-element finite type.
Claim. Let $Idx := {0,1,2,3}$ be the finite index set for the four spacetime coordinates.
background
The module works in a coordinate patch on four-dimensional spacetime, representing the metric as a smooth matrix-valued function $g: R^4 to R^{4 times 4}$ and supplying partial derivatives explicitly. This bypasses the absence of abstract connections in Mathlib. The upstream Tensor abbreviation specialises a general $(p,q)$-tensor to 4D spacetime by using Fin 4 as the index type.
proof idea
One-line abbreviation that directly aliases the four-element finite set Fin 4.
why it matters
Idx is the index type underlying ChristoffelData, christoffel_from_metric, metric_compatibility, and ConnectionCert. It enables the explicit coordinate-patch construction of the Levi-Civita connection. The choice matches the framework's D = 3 spatial dimensions plus time, producing the standard four-dimensional spacetime used throughout the Recognition Science gravity development.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.