module module high

`IndisputableMonolith.Foundation.CircleWinding`

Path-level winding on the unit circle: every continuous path on $S^1$ lifts through the standard covering $\mathbb{R}\to S^1$, and the endpoint difference of the lift is the real displacement ($2\pi$ times winding). Supplies the pathDisplacement invariant that the singular-simplex winding theory imports. Built from Mathlib covering-space path lifting plus the circle covering fixed upstream.

claimLet $S^1$ be the carrier of $\mathrm{TopCat.sphere}\,1$. Through the covering map $\mathbb{R}\to S^1$ (trigonometric circle point), every continuous path $\gamma:[0,1]\to S^1$ admits a lift $\tilde{\gamma}$ with prescribed start height. The path displacement is $\tilde{\gamma}(1)-\tilde{\gamma}(0)$; it is invariant under integer period shifts of the lift and equals $2\pi$ times the winding number of $\gamma$.

background

Recognition Science builds a winding/degree invariant on singular $1$-chains of the topological circle. The covering map is the standard trigonometric projection $\mathbb{R}\to S^1$ (already shown to be a covering in the circle-covering layer). Upstream, CircleLifting records the two prerequisites: contractibility of simplex realizations, and the covering-map lifting infrastructure imported from Mathlib homotopy theory.

This module works one level below singular chains: continuous paths on $S^1$. SphereOne is the carrier type of the exact TopCat.sphere 1 object. Surjectivity of the trigonometric covering and its equivariance under integer multiples of the period fix uniqueness of lifts up to the choice of starting height. Path lifts are then the unique continuous real lifts with a chosen start, and path displacement is the real difference of endpoints.

proof idea

Definition-and-construction module, not a single theorem. SphereOne aliases the circle carrier. Surjectivity and period-equivariance of the trigonometric covering are recorded first. Path lifts are obtained by applying Mathlib covering-space path lifting (from the homotopy lifting import) to that covering, with a start-height specification lemma. Displacement is defined as endpoint difference of the lift; equality and self-path lemmas follow by uniqueness of lifts. An interval-reversal helper supports orientation bookkeeping used downstream.

why it matters in Recognition Science

Parent consumer is CircleWindingChain, which "lifts the path-level winding/displacement invariant of CircleWinding to the level of singular simplices of TopCat.sphere 1" and proves the kills-boundaries identity that makes displacement a homology invariant. Without a well-defined real path displacement (unique up to start height, period-stable), the simplex-level assignment simplexDisplacement has nothing to reparameterize. In the broader foundation stack this is the analytic core of the circle degree used when Recognition arguments need topological winding rather than purely algebraic J-cost identities.

scope and limits

Does not define winding on singular simplices or chains; that is CircleWindingChain.
Does not prove the kills-boundaries / homology-invariance identity.
Does not treat higher spheres or higher-dimensional covering degrees.
Does not compute numerical winding for concrete paths beyond the abstract lift difference.
Does not re-prove that the trigonometric map is a covering; that is upstream.

used by (1)

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

IndisputableMonolith.Foundation.CircleWindingChain module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Foundation.CircleLifting module_import

declarations in this module (30)

abbrev SphereOne L34
theorem trigCirclePoint_surjective L38
theorem trigCirclePoint_add_intMul_period L49
def pathLiftStart L55
theorem pathLiftStart_spec L58
def pathLift L63
theorem pathLift_lifts L66
theorem pathLift_zero L70
def pathDisplacement L75
theorem pathDisplacement_eq L82
theorem pathDisplacement_self L114
def intervalReverse L118
def reversePath L121
theorem reversePath_apply L123
theorem pathDisplacement_reverse L129
theorem homotopicRel_apply_zero L143
theorem pathDisplacement_homotopic L154
theorem pathDisplacement_trans L178
def pathWinding L220
theorem pathDisplacement_loop_intMul L224
theorem pathWinding_loop_integral L236
def fundamentalLoop L245
def fundamentalLift L251
theorem fundamentalLift_lifts L255
theorem pathDisplacement_fundamentalLoop L261
theorem pathWinding_fundamentalLoop L270
theorem pathLift_endpoint_eq_of_winding_zero L278
theorem pathLift_exists_norm_bound L292
theorem pathLift_shifted_exists_norm_bound L304
theorem pathHomotopicRel_const_of_loop_winding_zero L317