norm_coneLiftAngle_sub_start_le
plain-language theorem explainer
Uniform apex estimate: if a path's real lift stays within distance C of its start value, the cone-lifted angle at any barycentric point x of the 2-simplex lies within (1-x₂)C of the apex lift. Used by the apex-continuity argument for the zero-winding cone filler on S¹. Proof rewrites via the shifted cone-angle identity, drops absolute value by nonnegativity of 1-x₂, and multiplies the given bound.
Claim. Let $\gamma:I\to S^1$ be continuous and $C\in\mathbb{R}$ such that $\|\widetilde{\gamma}(t)-\widetilde{\gamma}(0)\|\le C$ for all $t\in I$, where $\widetilde{\gamma}$ is the canonical continuous real lift of $\gamma$. Then for every $x$ in the standard $2$-simplex $\Delta^2$, the radially contracted cone lift $\theta(\gamma,x)$ satisfies $\|\theta(\gamma,x)-\widetilde{\gamma}(0)\|\le(1-x_2)C$.
background
This module lifts the path-level winding/displacement invariant of the circle covering to singular simplices on $S^1$, and proves that displacement kills boundaries: the alternating face sum of any singular $2$-simplex vanishes. That chain-level identity, together with the generator evaluation on the once-around loop, supplies the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
The cone construction fills a closed zero-winding edge by contracting radially toward an apex. The lifted cone angle is defined by $\theta(\gamma,x)=(1-x_2)\widetilde{\gamma}(b(x))+x_2\widetilde{\gamma}(0)$, where $b(x)$ is the barycentric base parameter (normalized coordinate along the base edge away from the apex, set to $0$ at the apex). The shifted identity isolates the vanishing factor: $\theta(\gamma,x)-\widetilde{\gamma}(0)=(1-x_2)(\widetilde{\gamma}(b(x))-\widetilde{\gamma}(0))$.
Continuity of $\theta$ at the apex is nontrivial because $b$ itself jumps; the squeeze comes from bounding the shifted lift and letting $1-x_2\to 0$.
proof idea
One short tactic block. Rewrite the left-hand side by the shifted cone-angle identity, so the difference becomes $(1-x_2)$ times a shifted lift value. From membership of $x$ in the standard simplex, $x_2\le 1$, hence $1-x_2\ge 0$. Pass the norm through the product, replace $|1-x_2|$ by $1-x_2$, and apply the given uniform bound at the base parameter $b(x)$, multiplying on the left by the nonnegative factor $1-x_2$.
why it matters
This is the quantitative squeeze estimate that the apex-continuity theorem consumes directly: that parent result obtains a uniform bound $C$ on the shifted path lift by compactness, invokes this lemma to get $|\theta(\gamma,x)-\widetilde{\gamma}(0)|\le(1-x_2)C$ for every $x$, and concludes $\theta(\gamma,x)\to\widetilde{\gamma}(0)$ as $x$ approaches the apex vertex. The doc-comment on the parent calls this "the analytic heart of the cone construction."
The cone filler is the geometric device that makes the $2$-simplex telescoping work for zero-winding closed edges, which is the remaining analytic step in the kills-boundaries identity for singular displacement. That identity is the chain-level half of the winding homomorphism being a left inverse to the fundamental class on $H_1(S^1)$. No Recognition-Science forcing-chain landmark (T5–T8, RCL, $\varphi$) is invoked here; the result is pure covering-space analysis inside the foundation layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.