RSCompatibleDimension

formal source

 353    1. Supports non-trivial linking (ledger conservation)
 354    2. 2^D = 8 (eight-tick synchronization)
 355    3. Compatible with gap-45 sync -/
 356structure RSCompatibleDimension (D : Dimension) : Prop where
 357  linking : SupportsNontrivialLinking D
 358  eight_tick : EightTickFromDimension D = eight_tick
 359  gap_sync : 2^D ∣ sync_period
 360
 361/-- D = 3 is RS-compatible. -/
 362theorem D3_compatible : RSCompatibleDimension 3 := {
 363  linking := D3_has_linking
 364  eight_tick := rfl
 365  gap_sync := by rw [sync_period_eq_360]; use 45; rfl
 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