353structure SpacetimeEmergenceCert where 354 dim_eq_four : spacetime_dim = 4 355 temporal_one : temporal_dim = 1 356 spatial_three : spatial_dim = 3 357 signature_lorentzian : 358 (Finset.univ.filter (fun i : Fin 4 => η i i < 0)).card = 1 ∧ 359 (Finset.univ.filter (fun i : Fin 4 => 0 < η i i)).card = 3 360 metric_trace : ∑ i : Fin 4, η i i = 2 361 metric_det : ∏ i : Fin 4, η i i = -1 362 cone_timelike : ∀ v : Displacement, 363 interval v < 0 ↔ spatial_norm_sq v < temporal_sq v 364 cone_lightlike : ∀ v : Displacement, 365 interval v = 0 ↔ spatial_norm_sq v = temporal_sq v 366 mass_gap_positive : 0 < massGap 367 mass_gap_universal : ∀ n : ℤ, n ≠ 0 → massGap ≤ Jcost (PhiLadder n) 368 octave_period : eight_tick = 8 369 sig_unique : temporal_dim = 1 ∧ spatial_dim = 3 370 arrow : ∀ t : ℕ, t < t + 1 371 372/-- **THEOREM**: The Spacetime Emergence Certificate is inhabited. 373 Zero sorry. -/
used by (4)
From the project-wide theorem graph. These declarations reference this one in their body.