pathLift_zero
plain-language theorem explainer
The canonical continuous lift of a path on the unit circle evaluates at time zero to the chosen real preimage of the path's start point. Anyone normalizing winding or path displacement through the trigonometric covering cites this. The proof is a one-line call to the covering-map path-lift API at the initial time.
Claim. For every continuous path $\gamma : I \to S^1$, the canonical lift $\widetilde{\gamma} : I \to \mathbb{R}$ satisfies $\widetilde{\gamma}(0)$ equal to the chosen real angle whose image under the trigonometric covering is $\gamma(0)$.
background
The module builds a local winding (displacement) invariant for paths in the exact TopCat.sphere 1 carrier by lifting through the trigonometric covering $\mathbb{R} \to S^1$ and reading the net travel of the lift in $\mathbb{R}$.
SphereOne is that carrier. For a path $\gamma$, a start height is chosen by surjectivity of the covering: some real whose image is $\gamma(0)$. The canonical lift is then the unique continuous lift of $\gamma$ that begins at that chosen height, obtained from the Mathlib path-lifting API once the covering is packaged as an IsCoveringMap.
Upstream, isCoveringMap_trig is exactly that packaging of the trigonometric covering, so the standard lift-at-zero identity applies directly.
proof idea
One-line term proof. Apply the covering-map lemma liftPath_zero to isCoveringMap_trig, the path $\gamma$, the chosen start height, and the fact (from the start-height specification, symmetrized) that the covering sends that height to $\gamma(0)$. No extra algebra.
why it matters
Path displacement is defined as how far the canonical lift travels in $\mathbb{R}$. That definition is only well-posed once the lift is pinned at time zero to the chosen fiber representative; this identity records that pin.
The module's central result is that displacement from the canonical lift agrees with the endpoint difference of any continuous lift (deck-transformation uniqueness). The zero-time normalization is the base case that makes the canonical lift a legitimate reference for that comparison.
No downstream dependents are recorded yet. In the Recognition foundation layer this is pure covering geometry for $S^1$, not yet tied to the forcing chain (T0–T8), RCL, or the eight-tick octave; it supplies the topological substrate those later invariants may use when paths on the circle appear.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.