pathLift_exists_norm_bound
plain-language theorem explainer
Any continuous path on the circle admits a canonical real lift that is uniformly bounded on the unit interval. Analysts building continuous cone fillers over closed edges cite this as the compactness input that keeps the apex formula finite. The proof is a one-shot application of the continuous-image bound on a compact domain.
Claim. For every continuous path $\gamma : I \to S^1$, there exists a constant $C \in \mathbb{R}$ such that $\|\widetilde{\gamma}(t)\| \le C$ for all $t \in I$, where $\widetilde{\gamma}$ is 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 given by the trigonometric parametrization of the circle, and displacement is read off as how far the lift travels in $\mathbb{R}$.
The canonical lift of a path $\gamma$ is the unique continuous lift starting at a fixed choice of preimage of $\gamma(0)$ under that covering. SphereOne is simply the carrier type of the exact sphere object. Because the unit interval $I$ is compact and the lift is continuous as a map $I \to \mathbb{R}$, standard real analysis supplies a uniform bound on its values.
Downstream cone constructions need exactly this bound: the singular-cone formula multiplies a lifted base path by a vanishing factor $(1-x_2)$ near the apex, and a uniform bound on the lift guarantees the product tends to zero continuously.
proof idea
Term-mode proof via compactness. Apply isCompact_univ.exists_bound_of_continuousOn to the continuous map $t \mapsto \mathrm{pathLift},\gamma,t$ on the whole unit interval (which is compact). Continuity of the lift is inherited from the covering-space path-lifting construction. The resulting bound $C$ is returned directly; the universal quantifier over $t \in I$ is discharged by membership of every point in the universe set.
why it matters
Uniform boundedness of the canonical lift is the analytic prerequisite for apex continuity of the singular cone filler used in the circle-winding chain. The module doc and the inline comment both flag this bound as the exact input consumed by the cone formula $L_0 + (1-x_2)\cdot(L(\mathrm{coneBaseParam},x)-L_0)$: without a finite $C$ controlling $L$, the product need not vanish at the apex.
In the broader Recognition foundation, displacement on $S^1$ is the local winding invariant that later feeds discrete period and octave arguments (eight-tick structure, covering uniqueness). This lemma itself is pure analysis, not a forcing-chain step, but it closes a compactness gap that any continuous geometric realization of winding must fill. No downstream theorem currently records a direct used_by edge, so the immediate consumer is the cone-continuity argument described in the doc-comment.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.