temporal_dim

formal source

  59/-! ## §1  Spacetime Dimension = 4 -/
  60
  61/-- The number of temporal dimensions: exactly 1 (the octave advance). -/
  62def temporal_dim : ℕ := 1
  63
  64/-- The number of spatial dimensions: D = 3 (forced by T8). -/
  65def spatial_dim : ℕ := D_physical
  66
  67/-- Total spacetime dimension: temporal + spatial. -/
  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,