singularTwoBoundaryFree_linear_step
plain-language theorem explainer
The free singular boundary of the lift-affine 2-simplex on vertices (0, 2π, z+2π) equals geo(0,z) − geo(0,z+2π) + geo(0,2π) in free C₁. Anyone proving the one-turn geodesic winding step cites this identity. The proof applies the general geodesic composition law, then folds the (2π, z+2π) edge onto (0,z) by 2π-shift invariance.
Claim. For every real $z$, the free singular boundary of the lift-affine $2$-simplex with lift vertices $(0,\,2\pi,\,z+2\pi)$ equals $\mathrm{geo}(0,z)-\mathrm{geo}(0,z+2\pi)+\mathrm{geo}(0,2\pi)$ in the free singular $1$-chain module on $S^1$.
background
The module lifts path-level winding on $S^1$ to singular simplices and proves that displacement kills $2$-boundaries, giving the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
A geodesic free chain $\mathrm{geo}(a,b)$ is the free $C_1$ generator of the lift-linear singular edge from lift $a$ to lift $b$. The free $2$-boundary map sends a singular $2$-simplex to the alternating sum of its three $1$-faces. The lift-affine $2$-simplex on real vertices $(p,q,r)$ is the singular $2$-simplex whose faces are the three geodesics among those lifts.
Upstream, the composition law states that $\partial(\mathrm{linear},p,q,r)=\mathrm{geo}(q,r)-\mathrm{geo}(p,r)+\mathrm{geo}(p,q)$. Separately, a simultaneous $2\pi\mathbb{Z}$ shift of both lift endpoints leaves the geodesic free chain unchanged.
proof idea
Rewrite the left-hand side by the general composition law singularTwoBoundaryFree_geodesicFreeChain at $(p,q,r)=(0,2\pi,z+2\pi)$. This produces $\mathrm{geo}(2\pi,z+2\pi)-\mathrm{geo}(0,z+2\pi)+\mathrm{geo}(0,2\pi)$.
The remaining step is the identity $\mathrm{geo}(2\pi,z+2\pi)=\mathrm{geo}(0,z)$, obtained from geodesicFreeChain_shift at base $(0,z)$ with integer shift $m=1$. Substitute and finish.
why it matters
This is the one-turn special case that feeds geodesicFreeChain_step: shifting the terminal lift endpoint by $m$ full turns adds $m$ fundamental loops to the geodesic, modulo an explicit free $2$-boundary. The induction in that parent theorem uses the present identity as the $m=\pm 1$ generator step.
In the module's program, the winding homomorphism on $1$-cycles is already a left inverse to the fundamental class (via simplexDisplacement_boundary and the once-around generator). The geodesic step supplies the explicit chain-level relation that realises integer multiples of the fundamental loop as homologous differences of geodesics, which is the concrete generator needed before any prism/subdivision argument for the surjective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.