Pith. sign in
module module moderate

IndisputableMonolith.Foundation.SingularSphereGeometry

show as:
view Lean formalization →

Sets up the ambient Euclidean space and standard two-chart atlas for the unit sphere S^n used throughout the singular-sphere foundation. Defines poles, radial north vector, and complementary open covers U and V whose union is the whole sphere. Downstream linking-vanishing arguments in high dimension import this geometry as the ambient manifold. Pure definitional scaffolding: no nontrivial proofs beyond openness and covering identities.

claimFix ambient Euclidean space $E = \mathbb{R}^{n+1}$ and the unit sphere $S^n \subset E$. Let $N,S\in S^n$ be the north and south poles (distinct), and let $U = S^n\setminus\{S\}$, $V = S^n\setminus\{N\}$ be the complementary open charts. Then $U\cup V = S^n$ and both sets are open in the subspace topology.

background

Recognition Science foundation work on singular spheres needs a concrete model of $S^n$ inside Euclidean space before any linking or vanishing statements can be stated. This module supplies that model: ambient space $E$, the embedded sphere, a distinguished unit north vector, and the two poles obtained by normalizing $\pm$ that vector.

The two-chart cover is the classical stereographic atlas: remove south pole for $U$, remove north pole for $V$. Openness of each chart and the covering identity $U\cup V=S^n$ are recorded as elementary facts so later modules can quote them without re-proving basic topology.

The module sits directly on top of SingularSphere (the abstract singular-sphere interface) and Mathlib radial-equivalence utilities for balls. It does not yet discuss metrics, curvature, or linking numbers; those appear downstream.

proof idea

Definition module. The bulk of the file introduces named abbreviations for ambient space, sphere, poles, and charts. The few lemmas are one-line: openness of each chart follows from openness of the complement of a closed singleton in the subspace topology; the covering identity is immediate set algebra once poles are known distinct. No tactic-heavy arguments and no appeal to deeper differential geometry.

why it matters in Recognition Science

Supplies the concrete geometric stage on which high-dimensional linking-vanishing is proved. The sole recorded consumer is Foundation.LinkingVanishingHighDim, which imports the poles and two-chart cover to reduce linking questions on singular spheres to calculations inside Euclidean charts. Within the broader RS forcing chain the module is pure infrastructure: it does not itself force dimension, cost functional, or tick structure, but any later geometric identity that needs an explicit $S^n$ model routes through these definitions.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (66)