pathLiftStart_spec
plain-language theorem explainer
For any continuous path γ on the unit circle, the chosen real starting angle maps under the trigonometric covering back to γ(0). Anyone building the canonical path lift or the displacement invariant cites this. The proof is the choose-spec of surjectivity of the covering at the initial point.
Claim. Let $\gamma : I \to S^1$ be continuous, where $S^1$ is the carrier of $\mathrm{TopCat.sphere}\,1$. If $\theta_0 \in \mathbb{R}$ is the chosen real lift of the initial point $\gamma(0)$, then $\mathrm{trigCirclePoint}(\theta_0) = \gamma(0)$.
background
This module builds the local winding (displacement) invariant for paths in the exact TopCat.sphere 1 object. Paths are lifted through the covering map given by the once-around trigonometric parametrization trigCirclePoint : ℝ → S¹, and displacement is the net travel of the lift in ℝ.
SphereOne is just the carrier of that sphere object. Surjectivity of trigCirclePoint supplies, for every point of the circle, some real angle mapping to it. The definition pathLiftStart γ is exactly that choice applied at γ(0): a real number whose image under the covering is the path's start.
The covering is the standard exponential-type map (cos, sin) into the sphere; deck transformations are translations by 2πℤ. Later results need a fixed basepoint in the fiber so Mathlib's path-lifting API can produce a continuous lift of the whole path.
proof idea
One-line term proof. pathLiftStart γ is defined as (trigCirclePoint_surjective (γ 0)).choose. Applying choose_spec to that same existential witness yields exactly trigCirclePoint (pathLiftStart γ) = γ 0. No further lemmas or tactics.
why it matters
This is the fiber-matching hypothesis required by the covering's path-lift constructor. It is fed directly into pathLift (the canonical continuous lift starting at that angle), into pathLift_lifts (the lift really covers γ), and into pathLift_zero (the lift begins at the chosen start).
Downstream, pathDisplacement_homotopic uses the same identity to align basepoints of homotopic paths so that lift uniqueness applies; that homotopy invariance is what makes displacement kill boundaries of singular 2-simplices. In the Recognition foundation stack this is pure covering-space bookkeeping for the circle winding invariant, not a forcing-chain step (T0–T8), but it underwrites any later topological counting on S¹ that the framework needs without custom circle models or axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.