pathLift_shifted_exists_norm_bound
plain-language theorem explainer
Any continuous path on the circle has a canonical real lift whose deviation from the starting height is uniformly bounded on the unit interval. Analysts building cone homotopies or winding contractions cite this bound. The argument is a one-shot compactness extraction: the continuous shifted lift on the compact interval I attains a finite supremum norm.
Claim. For every continuous path $\gamma : I \to S^1$, there exists a constant $C \in \mathbb{R}$ such that for all $t \in I$, $\|L_\gamma(t) - L_\gamma(0)\| \le C$, where $L_\gamma$ denotes the canonical continuous lift of $\gamma$ through the trigonometric covering $\mathbb{R} \to S^1$.
background
The module constructs the local winding (displacement) invariant of paths in the exact TopCat.sphere 1 object. Paths are lifted through the covering map trigCirclePoint : ℝ → S¹, and displacement is the net travel of the lift in ℝ. The canonical lift pathLift γ is the continuous lift of γ that starts at a fixed choice of fiber point over γ(0).
Because the covering is a local homeomorphism with deck group 2πℤ, any two continuous lifts of the same path that agree at one endpoint differ by a constant integer multiple of 2π. The central comparison theorem of the module records that the displacement read from the canonical lift therefore agrees with the endpoint difference of every continuous lift.
The present statement isolates a purely analytic consequence of that construction: after subtracting the initial height, the lifted path remains a continuous real-valued function on the compact interval I, hence is bounded.
proof idea
Term-mode proof via Mathlib compactness. Apply isCompact_univ.exists_bound_of_continuousOn to the continuous map $t \mapsto \mathrm{pathLift},\gamma,t - \mathrm{pathLift},\gamma,0$ on the universe of I. Continuity of the difference follows from continuity of the canonical lift minus a constant. The extracted bound C is then returned, and the universal quantification over t is discharged by the bound hypothesis on the whole of I.
why it matters
Downstream, coneLiftAngle_tendsto_apex consumes this bound as its first step: compactness supplies C, and the barycentric factor $(1-x_2)$ then squeezes the shifted lift to zero at the cone apex. The doc-comment of that parent theorem calls the pair "the analytic heart of the cone construction."
The cone itself is the device that contracts a zero-winding closed path on S¹ down to a constant, by lifting, linearly shrinking the real lift, and projecting back. That contraction is the topological engine behind the local winding invariant used throughout the Foundation layer. Without a uniform bound on the shifted lift, the squeeze argument at the apex would not close.
No forcing-chain landmark (T5–T8) is touched directly; the result is pure covering-space analysis feeding the circle-winding chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.