linking_selection_principle

formal source

 286def LinkingSelectionPrincipleHypothesis (D : ℕ) : Prop :=
 287  LinkingInvariantHypothesis D → D = 3
 288
 289theorem linking_selection_principle (D : ℕ)
 290    (h : LinkingSelectionPrincipleHypothesis D) (hLink : LinkingInvariantHypothesis D) :
 291    D = 3 :=
 292  h hLink
 293
 294/-- Paper main theorem (forward direction): if (T), (K), (S) hold then `D=3`.
 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