coneCirclePoint_simplexEdge_zero_of_lift_endpoint_eq
plain-language theorem explainer
On a path γ : I → S¹ whose continuous lift closes (pathLift γ 1 = pathLift γ 0), the pointwise cone map is constantly equal to the basepoint γ(0) along the entire δ₀ edge of the standard 2-simplex. Anyone building the cone homotopy that witnesses zero-winding closed loops as boundaries cites this. The proof is a three-line term reduction: unfold the cone, apply the lifted-angle constancy lemma, then project by the covering equation.
Claim. Let $\gamma : I \to S^1$ be continuous and suppose its canonical real lift satisfies $\widetilde{\gamma}(1) = \widetilde{\gamma}(0)$. Then for every $t \in I$, the pointwise cone value on the $\delta_0$ edge equals the path basepoint: $\mathrm{cone}(\gamma)(\mathrm{edge}_0(t)) = \gamma(0)$.
background
The module lifts the path-level winding/displacement invariant of CircleWinding to singular simplices on $S^1$, aiming at the chain-level identity that displacement kills boundaries: for every singular 2-simplex $F$, $\mathrm{disp}(\delta_0 F) - \mathrm{disp}(\delta_1 F) + \mathrm{disp}(\delta_2 F) = 0$. That identity, together with the generator evaluation, supplies the split-injective half of $H_1(S^1;\mathbb{Z}) \cong \mathbb{Z}$.
A path $\gamma : I \to S^1$ has a canonical continuous lift $\widetilde{\gamma} = \mathrm{pathLift},\gamma : I \to \mathbb{R}$ through the trigonometric covering $\mathbb{R} \to S^1$. The equality $\widetilde{\gamma}(1) = \widetilde{\gamma}(0)$ is exactly the zero-winding condition in lifted form. The pointwise cone $\mathrm{coneCirclePoint},\gamma$ is obtained by projecting a lifted cone angle on the standard 2-simplex $\Delta^2$ back down to $S^1$. The three edges of $\Delta^2$ are the face maps $\delta_0,\delta_1,\delta_2$; this lemma concerns the $\delta_0$ side.
Upstream, coneLiftAngle_simplexEdge_zero_of_lift_endpoint_eq already shows the lifted cone angle is constant (equal to $\widetilde{\gamma}(0)$) on that edge under the same hypothesis. The covering identity $\mathrm{trigCirclePoint}\circ\widetilde{\gamma} = \gamma$ then recovers the basepoint on $S^1$.
proof idea
Term-mode, three steps. Unfold coneCirclePoint, which is defined as $\mathrm{trigCirclePoint}$ of the lifted cone angle. Rewrite the angle on $\mathrm{simplexEdge},0$ by the sibling lemma coneLiftAngle_simplexEdge_zero_of_lift_endpoint_eq, which under $\widetilde{\gamma}(1)=\widetilde{\gamma}(0)$ yields the constant value $\widetilde{\gamma}(0)$. Finish with congrFun (pathLift_lifts γ) 0, i.e. the covering equation $\mathrm{trigCirclePoint}\circ\widetilde{\gamma}=\gamma$ evaluated at the left endpoint, giving $\gamma(0)$.
why it matters
This is the $S^1$-level companion of the lifted-angle constancy on $\delta_0$. Together they pin down the cone on the zero-winding closed side: the cone is constant equal to the basepoint along that entire edge. In the module's programme, such cone control is the geometric input for showing that a zero-winding loop bounds a singular 2-chain (the cone itself, once continuity at the apex is secured).
The module doc frames the target as the kills-boundaries identity simplexDisplacement_boundary and, ultimately, the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. No downstream consumers are wired yet (used_by_count = 0); the immediate next frontier noted in the cone definition is continuity of the pointwise cone at the apex. Within Recognition Science this sits in the Foundation layer that underwrites topological invariants used later in the forcing chain, not a direct T0–T8 step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.