IndisputableMonolith.Foundation.CircleLifting
Supplies the homotopy-lifting toolkit for the trigonometric covering of the circle: contractibility and simple connectedness of the standard simplex, and the covering-map status of the trig parametrization. Anyone building a by-hand winding or degree invariant for H₁(S¹; ℤ) cites it. The argument is mostly Mathlib convexity plus the covering map already constructed in CircleCovering.
claimThe standard topological $n$-simplex $\Delta^n$ is contractible (hence simply connected). The trigonometric map $\mathbb{R}\to S^1$ is a covering map, and two real lifts represent the same point of $S^1$ precisely when they differ by an integer multiple of $2\pi$ (equivalently, when their complex exponentials agree).
background
Recognition Science builds $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ by hand because Mathlib's singular homology stops at the totally disconnected case. The route is classical covering-space theory: singular simplices into $S^1$ are lifted through a covering map, and the real displacement of the lift becomes the winding number.
The covering map itself lives in CircleCovering: the trigonometric parametrization of TopCat.sphere 1. Lifting a map $f:X\to S^1$ through that cover requires $X$ to be connected and, for uniqueness up to homotopy, simply connected. The domain of a singular simplex is the standard simplex $\Delta^n$, a nonempty compact convex subset of $\mathbb{R}^{n+1}$. Convex sets in real vector spaces are contractible, so $\Delta^n$ is simply connected and the homotopy lifting property applies.
This module therefore sits between the covering construction and the path-level displacement invariant: it records that $\Delta^n$ is contractible/simply connected and packages the covering and fibre-equality facts needed to lift uniquely.
proof idea
Contractibility of the standard simplex is a one-line appeal to Mathlib: a nonempty convex set in a real topological vector space is contractible, and $\Delta^n$ is such a set. Simple connectedness follows from contractibility.
The covering-map statement for the trigonometric parametrization is imported or re-exported from CircleCovering (isCoveringMap_trig). Equality of trig points is reduced to equality of complex exponentials, then to integer multiples of $2\pi$, via the standard exponential covering $\mathbb{R}\to S^1$. No deep new topology is proved here; the module assembles Mathlib convexity and the existing circle cover into the lemmas the winding modules call.
why it matters in Recognition Science
Without unique lifts of singular simplices, there is no well-defined displacement, and the by-hand proof that $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ cannot start. CircleWinding imports this module to define path displacement by lifting through isCoveringMap_trigCirclePoint and measuring travel in $\mathbb{R}$. CircleWindingChain then lifts that path invariant to singular $1$-simplices and proves the kills-boundaries identity that makes displacement a homology invariant.
In the broader Foundation layer this is pure topological scaffolding for the circle's first homology, not a Recognition-Science forcing step (T0–T8). It is the bridge from the covering map to the winding number that later feeds discrete octave and phase arguments.
scope and limits
- Does not compute $H_1(S^1;\mathbb{Z})$ or define the winding number itself.
- Does not treat coverings of spheres $S^n$ for $n\neq 1$.
- Does not prove existence of lifts for arbitrary domains, only records simplex contractibility and the trig cover.
- Does not address higher homotopy groups or the long exact sequence of the fibration.