dimensional_rigidity_full_forward

formal source

 306
 307Status: the converse direction is recorded in the paper but depends on substantial
 308geometric infrastructure; we record only the forward direction as proved above. -/
 309theorem dimensional_rigidity_full_forward (D : ℕ)
 310    (hT : LinkingInvariantHypothesis D) (hK : ConstraintK D) (hS : ConstraintS D) :
 311    D = 3 :=
 312  dimensional_rigidity_main D hT hK hS
 313
 314/-- Paper corollary: there is no `D > 3` satisfying all three constraints simultaneously.
 315
 316We prove this using the (K)-based forcing `ConstraintK D → D=3`. -/
 317theorem no_higher_dimensional_alternative (D : ℕ) (hD : 3 < D)
 318    (hT : LinkingInvariantHypothesis D) (hK : ConstraintK D) (hS : ConstraintS D) :
 319    False := by
 320  have h3 : D = 3 := dimensional_rigidity_full_forward D hT hK hS
 321  have : D ≤ 3 := by simp [h3]
 322  exact (not_le_of_gt hD) this
 323
 324end DraftV1
 325end Papers
 326end IndisputableMonolith