dimension_unique

formal source

 366}
 367
 368/-- D = 3 is the unique RS-compatible dimension. -/
 369theorem dimension_unique (D : Dimension) :
 370    RSCompatibleDimension D → D = 3 := by
 371  intro ⟨hlink, height, _⟩
 372  exact linking_requires_D3 D hlink
 373
 374/-- **THE DIMENSION FORCING THEOREM**
 375
 376    D = 3 is forced by Alexander duality:
 377    1. Ledger conservation requires non-trivial linking
 378    2. Alexander duality: linking exists ↔ D = 3 (Hatcher Thm 3.44)
 379    3. Consequences: 2^D = 8 (eight-tick) and lcm(8,45) = 360 (gap-45 sync)
 380
 381    There is no free parameter; D is determined.
 382    The 8-tick and gap-45 are now consequences, not premises. -/
 383theorem dimension_forced : ∃! D : Dimension, RSCompatibleDimension D := by
 384  use 3
 385  constructor
 386  · exact D3_compatible
 387  · intro D hD
 388    exact dimension_unique D hD
 389
 390/-! ## Physical Interpretation -/
 391
 392/-- The spatial dimension of the physical world. -/
 393def D_physical : Dimension := 3
 394
 395/-- D_physical is RS-compatible. -/
 396theorem D_physical_compatible : RSCompatibleDimension D_physical := D3_compatible
 397
 398/-- The eight-tick cycle in D = 3 dimensions. -/
 399theorem physical_eight_tick : EightTickFromDimension D_physical = 8 := rfl