pith. machine review for the scientific record. sign in
abbrev definition def or abbrev high

Idx

show as:
view Lean formalization →

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.

claimLet $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 in Recognition Science

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.

scope and limits

formal statement (Lean)

  33abbrev Idx := Fin 4

proof body

Definition body.

  34
  35/-! ## Metric Tensor in Coordinates -/
  36
  37/-- A metric tensor in local coordinates: a symmetric 4x4 matrix
  38    at each spacetime point (here abstracted as just the components). -/

used by (30)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (7)

Lean names referenced from this declaration's body.