pathLiftStart
plain-language theorem explainer
Chooses a real angle whose image under the trigonometric covering is the initial point of a continuous path on S¹. Anyone constructing the canonical path lift or the local winding/displacement invariant cites this choice. The body is a single Classical.choose from covering surjectivity.
Claim. For a continuous path $\gamma : I \to S^1$, there is a chosen real number $\theta$ such that the trigonometric covering map sends $\theta$ to the initial point $\gamma(0)$.
background
The module builds a local winding (displacement) invariant for paths in the exact TopCat.sphere 1 object. Paths are lifted through the trigonometric covering $\mathbb{R} \to S^1$, and displacement is the net travel of the lift in $\mathbb{R}$.
SphereOne is the carrier of that exact sphere object. The covering map (trigonometric point map) is surjective: every point of $S^1$ is the image of some real angle. That surjectivity theorem supplies the existential witness used here.
The module's central claim is that displacement from the canonical choice-based lift agrees with the endpoint difference of any continuous lift (deck-transformation uniqueness). Fixing a real start angle for each path is the first step of that construction.
proof idea
One-line definition: apply the surjectivity theorem of the trigonometric covering at $\gamma(0)$, then take Classical.choose of the resulting existential. No further tactics. The companion specification lemma records that the covering of this chosen real recovers $\gamma(0)$.
why it matters
This is the seed of the canonical lift. Downstream, the continuous lift of a path is the covering-space path-lift starting at this chosen real; the lift-lifts and lift-at-zero lemmas pin that construction. Displacement (net travel of the lift) and its homotopy invariance both thread through this start angle: homotopy invariance reuses the same start fiber when endpoints match, which is how winding kills boundaries of singular 2-simplices.
In the Recognition foundation stack this is pure covering-space infrastructure for the circle, not yet a physics constant. It supports the local winding invariant without project-local $S^1$ replacements, axioms, or sorry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.