dimensional_rigidity_main

formal source

 295
 296In the current repo, (S) and (K) are fully formalized at the arithmetic/algebraic level;
 297(T) is recorded but not used in the proof here. -/
 298theorem dimensional_rigidity_main (D : ℕ)
 299    (_hT : LinkingInvariantHypothesis D)
 300    (hK : ConstraintK D)
 301    (_hS : ConstraintS D) :
 302    D = 3 :=
 303  (kepler_selection_principle D).1 hK
 304
 305/-- Paper combined theorem (full statement): forward direction plus a partial converse.
 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