ConstraintK

formal source

 208  3 ≤ D ∧ ∀ D', 3 ≤ D' → syncPeriod D ≤ syncPeriod D'
 209
 210/-- Paper-style (K) constraint, reduced to the closed-form apsidal-angle condition. -/
 211def ConstraintK (D : ℕ) : Prop :=
 212  apsidalAngle D = 2 * Real.pi
 213
 214/-! The (S) constraint is fully formalized here (arithmetic only). -/
 215
 216theorem constraintS_forces_D3 {D : ℕ} (hS : ConstraintS D) : D = 3 := by
 217  have hD : 3 ≤ D := hS.1
 218  have hle : syncPeriod D ≤ syncPeriod 3 := hS.2 3 (le_rfl)
 219  have hge : syncPeriod 3 ≤ syncPeriod D := (synchronization_selection_principle (D := D) hD).1
 220  have heq : syncPeriod D = syncPeriod 3 := le_antisymm hle hge
 221  exact (synchronization_selection_principle (D := D) hD).2 heq
 222
 223theorem constraintS_iff_D3 (D : ℕ) : ConstraintS D ↔ D = 3 := by
 224  constructor
 225  · intro hS; exact constraintS_forces_D3 hS
 226  · intro hD
 227    subst hD
 228    refine ⟨le_rfl, ?_⟩
 229    intro D' hD'
 230    exact (synchronization_selection_principle (D := D') hD').1
 231
 232/-!
 233Paper-style (T) constraint and Alexander duality are now formalized in
 234`IndisputableMonolith.Foundation.AlexanderDuality`. The Alexander duality
 235hypothesis interface below delegates to the cohomology-based predicate
 236`SphereAdmitsCircleLinking`, which is proved equivalent to D = 3 from
 237the reduced cohomology axiom for S¹.
 238-/
 239
 240open IndisputableMonolith.Foundation.AlexanderDuality
 241