369theorem dimension_unique (D : Dimension) : 370 RSCompatibleDimension D → D = 3 := by
proof body
Term-mode proof.
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. -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.