`Q3_unique_linking_dimension`

proved

show as: view math explainer →

module: IndisputableMonolith.Meta.LedgerUniqueness
domain: Meta
line: 121 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Meta.LedgerUniqueness on GitHub at line 121.

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

used by

formal source

 118  ∀ D : ℕ, D ≥ 2 → (linkingNumber D ≠ 0 ↔ D = 3)
 119
 120/-- D=3 is the unique dimension with irreducible linking. -/
 121theorem Q3_unique_linking_dimension :
 122    ∀ D : ℕ, D ≥ 2 → (linkingNumber D ≠ 0 ↔ D = 3) := by
 123  intro D hD
 124  constructor
 125  · intro hLink
 126    unfold linkingNumber at hLink
 127    split_ifs at hLink with h
 128    · exact h
 129    · simp at hLink
 130  · intro hD3
 131    unfold linkingNumber
 132    simp [hD3]
 133
 134/-- The cube Q₃ is the unique linking-compatible polytope.
 135    (Reformulated: Linking structure implies D=3) -/
 136theorem cube_uniqueness :
 137    ∀ D : ℕ, (linkingNumber D ≠ 0) ↔ D = 3 := by
 138  intro D
 139  constructor
 140  · intro h
 141    unfold linkingNumber at h
 142    split_ifs at h with hD
 143    · exact hD
 144    · contradiction
 145  · intro h
 146    rw [h]
 147    unfold linkingNumber
 148    simp
 149
 150/-! ## 8-Tick Uniqueness -/
 151

papers checked against this theorem

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