pith. machine review for the scientific record. sign in
theorem proved term proof

Q3_unique_linking_dimension

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 121theorem Q3_unique_linking_dimension :
 122    ∀ D : ℕ, D ≥ 2 → (linkingNumber D ≠ 0 ↔ D = 3) := by

proof body

Term-mode proof.

 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) -/

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (6)

Lean names referenced from this declaration's body.