homotopicRel_apply_zero
plain-language theorem explainer
Paths on the circle that are homotopic relative to their endpoints share the same starting point. Anyone proving homotopy invariance of the local winding (displacement) cites this to align the two lifts at a common base angle. The argument unpacks the relative homotopy and evaluates the fixed-endpoint identities at time zero.
Claim. Let $\gamma,\delta:I\to S^1$ be continuous paths. If $\gamma$ and $\delta$ are homotopic relative to the endpoint set $\{0,1\}$, then $\gamma(0)=\delta(0)$.
background
This module builds the local winding, or displacement, of a path in the exact topological circle $S^1$ (written as the carrier of TopCat.sphere 1). Displacement is read off by lifting the path through the trigonometric covering $\mathbb{R}\to S^1$ and measuring how far the lift travels in $\mathbb{R}$. The module's central fact is that any continuous lift yields the same endpoint difference, so the invariant is independent of lift choice.
A relative homotopy between paths $\gamma$ and $\delta$ is a continuous homotopy that keeps the restricted set ${0,1}\subset I$ fixed throughout. In particular the two paths are forced to agree at both endpoints; the present lemma isolates the start-point half of that agreement.
The lemma sits upstream of the homotopy-invariance statement for displacement: once start points match, the covering's unique-lift machinery can compare the two lifted paths from a common initial angle.
proof idea
Unpack the relative-homotopy witness $H$ from the hypothesis. Record that $0\in{0,1}$. Rewrite $\gamma(0)$ via the relative-homotopy identity that equates the two ends of $H$ on the fixed set (evaluated at parameter $1$), then apply the identity that the time-$1$ slice of $H$ recovers the second path, evaluated at $0$. The result is $\gamma(0)=\delta(0)$. Purely the fixed-set evaluation rules for a relative homotopy; no covering or lift is used.
why it matters
This is the first step inside the homotopy-invariance theorem for path displacement: that theorem opens by invoking the present result to obtain $\gamma(0)=\delta(0)$, then feeds the common start point into the covering lift so both paths lift from the same real angle. The downstream doc-comment states the payoff: "This is the core mechanism by which the winding invariant kills boundaries: the boundary loop of a singular $2$-simplex is null-homotopic in the contractible standard simplex, so its displacement vanishes."
In the broader Recognition foundation, a well-defined, homotopy-invariant displacement on $S^1$ is the local model for the eight-tick / octave winding that later forces discrete temporal structure (T7). Without start-point agreement under relative homotopy, the lift comparison would not even type-check, and the boundary-killing argument would fail.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.