Standard four-sphere and smooth Poincaré predicates

Definition

SP4Sphere

by ryanshin · Sep 5, 2026 · Mathlib 0df444a (Lean v4.33.1)

The standard four-sphere is the unit sphere in Euclidean five-space. SPC4 says that every compact Hausdorff Type-0 manifold with a given boundaryless smooth real four-dimensional atlas, if homeomorphic to this sphere, is smoothly diffeomorphic to it. SPC4Homotopy replaces homeomorphism by homotopy equivalence. These are propositions, not proofs.

Definition code

-- Derived from frozen local sources; exact source/hash provenance in items.json.
import Mathlib

set_option autoImplicit false

namespace SP4Mission

open scoped Manifold ContDiff

noncomputable section

abbrev S4 : Type := Metric.sphere (0 : EuclideanSpace ℝ (Fin (4 + 1))) 1

def SPC4 : Prop :=
  ∀ (M : Type) [TopologicalSpace M] [T2Space M] [CompactSpace M]
    [ChartedSpace (EuclideanSpace ℝ (Fin 4)) M] [IsManifold (𝓡 4) ∞ M],
    Nonempty (M ≃ₜ S4) →
    Nonempty (M ≃ₘ⟮𝓡 4, 𝓡 4⟯ S4)

def SPC4Homotopy : Prop :=
  ∀ (M : Type) [TopologicalSpace M] [T2Space M] [CompactSpace M]
    [ChartedSpace (EuclideanSpace ℝ (Fin 4)) M] [IsManifold (𝓡 4) ∞ M],
    Nonempty (ContinuousMap.HomotopyEquiv M S4) →
    Nonempty (M ≃ₘ⟮𝓡 4, 𝓡 4⟯ S4)

section Transport

variable {N : Type} [TopologicalSpace N]

end Transport

section Bridge

open Set ChartedSpace

variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] {E : Type*} [NormedAddCommGroup E]
  [NormedSpace 𝕜 E] {H' : Type*} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H'}
  {X : Type*} [TopologicalSpace X] [ChartedSpace H' X]
  {X' : Type*} [TopologicalSpace X'] [ChartedSpace H' X']
  {m : ℕ∞ω} [IsManifold I m X] [IsManifold I m X']

end Bridge

end

end SP4Mission

Source

Unpublished local Lean source SPC4.lean, SHA-256 b17fdb932034e5211d0db8171c08e2b3a182016bceaecdd2deb49c39d6bfd5cc; supported copy and exact oracle provenance in the accompanying local package.

Read-back

What the Lean code literally says, in plain math · Codex; the exact underlying model identifier is not exposed in this session.

Let $S^4=\{x\in\mathbb R^5:\|x\|=1\}$ , with its subspace topology and standard stereographic smooth structure modeled on $\mathbb R^4$ . The proposition $\mathrm{SPC4}$ says that for every type $M$ in the base universe and every choice on $M$ of topology, Hausdorff and compactness structures, and a charted-space structure modeled on $\mathbb R^4$ with $C^\infty$ -compatible transitions, existence of a homeomorphism $M\to S^4$ implies existence of a diffeomorphism $M\to S^4$ , meaning a bijection for which both the forward map and the inverse are $C^\infty$ in the specified manifold charts. The proposition $\mathrm{SPC4Homotopy}$ has exactly the same quantified spaces and structures and the same conclusion, but its premise is existence of a continuous homotopy equivalence between $M$ and $S^4$ , meaning a pair of continuous maps in opposite directions whose two composites are continuously homotopic to the corresponding identity maps. Both propositions require existence, without uniqueness or a prescribed underlying map for the diffeomorphism. No separate nonemptiness hypothesis on $M$ is imposed; an empty $M$ is included in the universal quantifier, and in that case neither a homeomorphism nor a homotopy equivalence to the nonempty sphere exists.

Human review

Endorsed by Shuze Chen · Sep 6, 2026
Endorsed by ryanshin · Sep 6, 2026
Confirmed by the mission captain (proposal self-audit).

View graph