spacetime_dim_eq_four

formal source

  68def spacetime_dim : ℕ := temporal_dim + spatial_dim
  69
  70/-- **SE-001: Spacetime has exactly 4 dimensions.** -/
  71theorem spacetime_dim_eq_four : spacetime_dim = 4 := by
  72  unfold spacetime_dim temporal_dim spatial_dim D_physical; rfl
  73
  74/-- The 8-tick period matches 2^D for D = 3. -/
  75theorem octave_matches_spatial : eight_tick = 2 ^ spatial_dim := rfl
  76
  77/-! ## §2  The Spatial Metric from J-Cost Curvature -/
  78
  79/-- **The exact J-cost quadratic form near identity.**
  80    J(1+ε) = ε² / (2(1+ε)) for any ε with 1+ε > 0. -/
  81theorem Jcost_near_identity (ε : ℝ) (hε : -1 < ε) :
  82    Jcost (1 + ε) = ε ^ 2 / (2 * (1 + ε)) := by
  83  have h_ne : (1 + ε : ℝ) ≠ 0 := ne_of_gt (by linarith)
  84  rw [Jcost_eq_sq h_ne]; congr 1 <;> ring
  85
  86/-- The spatial cost is strictly positive for any non-zero displacement. -/
  87theorem spatial_cost_positive (ε : ℝ) (hε : -1 < ε) (hε_ne : ε ≠ 0) :
  88    0 < Jcost (1 + ε) := by
  89  rw [Jcost_near_identity ε hε]
  90  exact div_pos (sq_pos_of_ne_zero hε_ne) (mul_pos (by norm_num : (0:ℝ) < 2) (by linarith))
  91
  92/-- **The spatial metric coefficient** at the identity is 1/2,
  93    giving J''(1) = 2 · (1/2) = 1. -/
  94theorem spatial_metric_at_identity :
  95    (1 : ℝ) / (2 * (1 + 0)) = 1 / 2 := by norm_num
  96
  97/-! ## §3  The Minkowski Metric (Forced, Not Postulated) -/
  98
  99/-- The **Minkowski metric** on RS spacetime.
 100    Index 0 = temporal (octave advance), indices 1,2,3 = spatial (Q₃ axes). -/
 101def η (i j : Fin 4) : ℝ :=