arrow_of_time

formal source

 312/-! ## §9  The Arrow of Time from the Octave -/
 313
 314/-- **SE-009: The arrow of time**. Recognition advances monotonically. -/
 315theorem arrow_of_time :
 316    temporal_dim = 1 ∧ eight_tick = 8 ∧ ∀ t : ℕ, t < t + 1 :=
 317  ⟨rfl, rfl, fun _ => Nat.lt_succ_of_le le_rfl⟩
 318
 319/-! ## §10  Exclusion of Alternative Signatures -/
 320
 321theorem not_euclidean : ¬(temporal_dim = 0) := by simp [temporal_dim]
 322theorem not_split_signature : ¬(temporal_dim = 2) := by simp [temporal_dim]
 323theorem not_three_temporal : ¬(temporal_dim = 3) := by simp [temporal_dim]
 324theorem not_1_2_signature : ¬(spatial_dim = 2) := by simp [spatial_dim, D_physical]
 325theorem not_1_4_signature : ¬(spatial_dim = 4) := by simp [spatial_dim, D_physical]
 326
 327/-- **SE-010: The signature (1, 3) is the UNIQUE RS-compatible signature.** -/
 328theorem signature_unique :
 329    temporal_dim = 1 ∧ spatial_dim = 3 ∧
 330    (∀ d_t d_s : ℕ, d_t + d_s = spacetime_dim → d_t = 1 → d_s = 3) := by
 331  refine ⟨rfl, rfl, fun d_t d_s h1 h2 => ?_⟩
 332  rw [h2, spacetime_dim_eq_four] at h1; omega
 333
 334/-! ## §11  The Mass Gap as the Minimum Spacetime Excitation -/
 335
 336/-- The mass gap sets the minimum spatial excitation energy. -/
 337theorem mass_gap_is_spatial_minimum :
 338    ∀ n : ℤ, n ≠ 0 → massGap ≤ Jcost (PhiLadder n) := spectral_gap
 339
 340/-- The mass gap is exactly J(φ). -/
 341theorem mass_gap_from_phi : Jcost phi = massGap := Jcost_phi_eq_massGap
 342
 343/-- **Mass gap numerical bounds**: 0.118 < Δ < 0.119. -/
 344theorem mass_gap_bounds : (0.118 : ℝ) < massGap ∧ massGap < (0.119 : ℝ) :=
 345  massGap_numerical_bound