`D3_admits_circle_linking`

proved

show as: view math explainer →

module: IndisputableMonolith.Foundation.AlexanderDuality
domain: Foundation
line: 154 · github
papers citing: 8 papers (below)

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.AlexanderDuality on GitHub at line 154.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

 151/-! ## Derived Facts -/
 152
 153/-- D = 3 admits circle linking (forward direction). -/
 154theorem D3_admits_circle_linking : SphereAdmitsCircleLinking 3 :=
 155  (alexander_duality_circle_linking 3).mpr rfl
 156
 157/-- Circle linking forces D = 3 (reverse direction). -/
 158theorem circle_linking_forces_D3 (D : ℕ) :
 159    SphereAdmitsCircleLinking D → D = 3 :=
 160  (alexander_duality_circle_linking D).mp
 161
 162/-- No circle linking in D ≤ 2.
 163Proof: H̃^{D-2}(S¹) = 0 for D - 2 ≤ 0, since S¹ has no nontrivial
 164reduced cohomology in non-positive degrees. -/
 165theorem no_circle_linking_low_dim (D : ℕ) (hD : D ≤ 2) :
 166    ¬SphereAdmitsCircleLinking D := by
 167  intro h
 168  have := circle_linking_forces_D3 D h
 169  omega
 170
 171/-- No circle linking in D ≥ 4.
 172Proof: H̃^{D-2}(S¹) = 0 for D - 2 ≥ 2, since S¹ has no nontrivial
 173reduced cohomology above degree 1. -/
 174theorem no_circle_linking_high_dim (D : ℕ) (hD : D ≥ 4) :
 175    ¬SphereAdmitsCircleLinking D := by
 176  intro h
 177  have := circle_linking_forces_D3 D h
 178  omega
 179
 180end AlexanderDuality
 181end Foundation
 182end IndisputableMonolith

papers checked against this theorem (showing 8 of 8)

Fast-slow recurrence stabilizes long-sequence models
echoes · 2604.01577

"reasoning process proceeds T times faster than the observation process … X(t+1) = Π(X(t) + γ F(X(t),C(t);θ)) … never reset until the episode ends"
Spherical arrays deliver 3D coverage and resolution for 6G
echoes · 2604.02701

"Spherical antenna arrays (SAAs), with elements uniformly distributed on a spherical surface, provide an effective solution for three-dimensional (3D) full-space coverage"
Graph pooling extracts functional protein substructures from ESM-2 features
echoes · 2605.10985

"3D CoordinatesC∈RN×3 Radius Graphε= 8Å ... GINEConvBackbone ... Gumbel-Softmax Assignment"
Every 3D convex body has volume product at least 64/9
unclear · 2605.09334

"Lemma 5.1... dim A_θ(P) ≥ F(P) - V(P) + Δ(P) + 1... using Euler’s formula V + F - E = 2."
Matrix model supersymmetry selects four-dimensional Euclidean spacetime
contradicts · 2605.03611

"In any dimension D≠4, the stringent constraints of the non-renormalization theorem cannot be bypassed"
Suspensions of K6-minor graphs force linked cycles in R^4
unclear · 2605.06851

"Theorem 1.1. The suspension of any graph containing K6 as a minor is an intrinsically linked 2-complex in R4."
Pyramid design isolates cosmological gravitational wave chirality
echoes · 2604.08471

"A necessary condition for sensitivity to the circular polarization (Stokes-V) component of an isotropic SGWB is that the detector network be genuinely three dimensional"
Integer twists on edges turn meshes into linked knot structures
echoes · 2604.12023

"Theoretically, we show that these integer-twisted meshes correspond to knotted surfaces in four dimensions, with LK structures arising as their immersions into R^3"