SpacetimeIndex

formal source

  47def Spacetime : Manifold := { dim := 4 }
  48
  49/-- Coordinate indices for spacetime. -/
  50abbrev SpacetimeIndex := Fin 4
  51
  52/-- Time coordinate (index 0). -/
  53def timeIndex : SpacetimeIndex := 0
  54
  55/-- Spatial indices (1, 2, 3). -/
  56def spatialIndices : List SpacetimeIndex := [1, 2, 3]
  57
  58/-- Check if an index is spatial. -/
  59def isSpatial (μ : SpacetimeIndex) : Bool := μ ≠ 0
  60
  61/-- Kronecker delta for indices. -/
  62def kronecker {n : ℕ} (μ ν : Fin n) : ℝ := if μ = ν then 1 else 0
  63
  64theorem kronecker_symm {n : ℕ} (μ ν : Fin n) :
  65  kronecker μ ν = kronecker ν μ := by
  66  by_cases h : μ = ν
  67  · simp [kronecker, h]
  68  · have h' : ν ≠ μ := by
  69      intro hνμ
  70      exact h hνμ.symm
  71    simp [kronecker, h, h']
  72
  73theorem kronecker_diag {n : ℕ} (μ : Fin n) :
  74  kronecker μ μ = 1 := by
  75  simp [kronecker]
  76
  77theorem kronecker_off_diag {n : ℕ} (μ ν : Fin n) (h : μ ≠ ν) :
  78  kronecker μ ν = 0 := by
  79  simp [kronecker, h]
  80