Pith. sign in
module module high

IndisputableMonolith.Foundation.CircleParam

show as:
view Lean formalization →

Fixes the ambient Euclidean plane and trigonometric parametrization of Mathlib's unit circle TopCat.sphere 1. Defines the carrier, basepoint, and continuous map θ ↦ (cos θ, sin θ) with endpoint identities at 0 and 2π. Covering-space and singular-homology modules that build H₁(S¹; ℤ) ≅ ℤ import these carriers. Structure is definitional setup plus membership and continuity lemmas.

claimIdentify the ambient space $\mathbb{R}^2$ carrying Mathlib's topological circle $S^1=\{x:\|x\|=1\}$, fix a basepoint on $S^1$, and define the continuous trigonometric parametrization $f(\theta)=(\cos\theta,\sin\theta)$ into $S^1$ with $f(0)=f(2\pi)$ equal to that basepoint.

background

Mathlib presents the circle as TopCat.sphere 1, the unit sphere in a Euclidean inner-product space of dimension 2. This module pins that ambient space explicitly and equips it with the standard trigonometric chart used throughout algebraic topology.

The sibling definitions introduce the ambient Euclidean plane, the carrier set of unit vectors, a concrete base vector and basepoint on the sphere, and the map sending a real angle to $(\cos\theta,\sin\theta)$. Continuity of that map, membership in the sphere, and the identities at $0$ and $2\pi$ are recorded as lemmas.

The local setting is pure foundation for singular homology of the circle: Mathlib's singular-homology library stops short of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$, so every by-hand route needs a fixed geometric model of $S^1$ before covering maps or fundamental simplices can be written.

proof idea

This is a definition module, not a theorem package. It declares the ambient Euclidean space for TopCat.sphere 1, the carrier and basepoint, and the trigonometric parametrization, then records elementary membership, continuity, and endpoint facts (values at 0 and $2\pi$). No deep argument is required; the content is type-level setup plus short analytic checks against Mathlib trigonometry and the sphere predicate.

why it matters in Recognition Science

Every later step toward a by-hand computation of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ imports this model. CircleCovering uses the trigonometric parametrization as the covering map of TopCat.sphere 1 that lifts singular simplices and defines winding. CircleFundamentalSimplex builds the once-around singular 1-simplex in TopCat.toSSet.obj (TopCat.sphere 1) on this carrier and checks that its faces meet at the basepoint. CircleH1Computation is the workbench for the missing isomorphism and treats this geometry as the concrete circle on which finite chain models sit.

In the Recognition Science stack the circle homology computation is infrastructure for the T8 spatial-dimension forcing bridge; the module itself does not touch T8, but without a pinned $S^1$ model the covering and $H_1$ layers cannot start.

scope and limits

used by (3)

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

declarations in this module (17)