`D_physical_compatible`

proved

show as: view math explainer →

module: IndisputableMonolith.Foundation.DimensionForcing
domain: Foundation
line: 396 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.DimensionForcing on GitHub at line 396.

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

depends on

formal source

 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
 414    3. **Spin group (CHARACTERIZATION)**: Spin(3) ≅ SU(2) is the simplest
 415       non-abelian compact Lie group (gauge structure for weak interactions).
 416
 417    4. **Bott periodicity (CONSEQUENCE)**: Period 8 = 2³ = 2^D follows
 418       from D = 3, linking Clifford periodicity to dimension.
 419
 420    5. **Gap-45 (CONSEQUENCE)**: lcm(8, 45) = 360 = 2³ × 3² × 5 follows
 421       from the 8-tick = 2^3 derived from D = 3.
 422
 423    The Alexander duality argument is the logically primary route.
 424    Items 2–5 are consequences or characterizations, not premises. -/
 425theorem why_D_equals_3 :
 426    -- Spinor structure requires D = 3

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.