pith. machine review for the scientific record. sign in
theorem

dimension_forced

proved
show as:
view math explainer →
module
IndisputableMonolith.Foundation.DimensionForcing
domain
Foundation
line
383 · github
papers citing
68 papers (below)

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.DimensionForcing on GitHub at line 383.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

Derivations using this theorem

depends on

used by

formal source

 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
 400
 401/-- **WHY D = 3**
 402
 403    The dimension is not a free parameter. It is forced by:
 404
 405    1. **Alexander duality (PRIMARY, proved from axiom)**:
 406       `SphereAdmitsCircleLinking D ↔ D = 3`, proved from the reduced
 407       cohomology of S¹ axiom in `AlexanderDuality.lean`. Independent of T7.
 408       H̃₁(Sᴰ \ S¹) ≅ H̃^{D-2}(S¹), nontrivial iff D = 3.
 409
 410    2. **Clifford algebra (CHARACTERIZATION)**: Cl₃ ≅ M₂(ℂ) gives
 411       2-component complex spinors — the unique structure for spin-½.
 412       (See `CliffordBridge.cl3_iso_m2c`)
 413