geodesicFreeChain_step
plain-language theorem explainer
Shifting a geodesic's terminal lift by m full turns changes the free singular 1-chain by exactly m copies of the fundamental loop, up to an explicit free 2-boundary. Anyone assembling terminal-return corrections for oriented cyclic families on S¹ cites this step. The proof is integer induction, gluing one lift-affine 2-simplex per turn via the geodesic composition law.
Claim. For every real $y$ and integer $m$, there exists a free singular $2$-chain $K$ on $S^1$ whose free boundary equals $\mathrm{geo}(0,\, y + 2\pi m) - \mathrm{geo}(0,\, y) - m\,\mathrm{geo}(0,\, 2\pi)$, where $\mathrm{geo}(a,b)$ is the free $C_1$ generator of the lift-linear geodesic edge from lift $a$ to lift $b$.
background
This module lifts the path-level winding/displacement invariant of CircleWinding to singular simplices on $S^1$ and proves that displacement kills boundaries, giving the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
A free geodesic 1-chain $\mathrm{geo}(a,b)$ is the free $C_1$ generator of the singular edge carried by the lift-linear geodesic from real lifts $a$ to $b$. The lift-affine singular 2-simplex on triple $(p,q,r)$ has free boundary $\mathrm{geo}(q,r)-\mathrm{geo}(p,r)+\mathrm{geo}(p,q)$ (the geodesic composition law). The free boundary operator is the ModuleCat morphism singularTwoBoundaryFree.
The local goal is to compare geodesics that differ by integer multiples of a full turn $2\pi$, so that winding corrections can be absorbed into free 2-chains rather than left as residual 1-cycles.
proof idea
Integer induction on $m$ via Int.induction_on.
Base $m=0$: take the zero 2-chain; both sides vanish by simp.
Successor: from the inductive chain $K$ for $i$, subtract the free generator of the lift-affine 2-simplex on $(0,,2\pi,, y+i\cdot 2\pi+2\pi)$. Apply map_sub, the inductive hypothesis, and singularTwoBoundaryFree_linear_step at the intermediate basepoint; rewrite the endpoint by ring and cancel with add_smul/one_smul and abel.
Predecessor: symmetrically add the free generator of the lift-affine simplex that steps one turn backward, again using the linear-step boundary identity, then rearrange coefficients with neg_one_smul and abel.
why it matters
This is the per-edge winding-step brick used by orientedCyclicFamilies_terminalSideCorrection_generate_holds, which shows the terminal-side correction target is closed unconditionally. That parent assembles three families of 2-chains (lift-affine cones, these winding-step chains $K_{\mathrm{step}},i$, and constant-apex simplices) so that telescoping leaves exactly terminal-return side minus constant-apex side plus $n$ times the fundamental cycle, with $n=\sum m_i$ the total winding forced by cyclic connectivity.
In the module's larger program, this supports the generation half of the integer comparison map on $H_1(S^1)$: every relevant 1-cycle is homologous to an integer multiple of the fundamental loop. It does not itself invoke the RS forcing chain (T0–T8) or the Recognition Composition Law; it is pure singular-chain bookkeeping on the circle that underwrites the winding homomorphism used elsewhere in the foundation stack.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.