singularTwoBoundaryFree_geodesicFreeChain
plain-language theorem explainer
On free singular 1-chains of the circle, the boundary of the lift-affine 2-simplex with lift vertices (p,q,r) equals the alternating geodesic sum geo(q,r) − geo(p,r) + geo(p,q). Anyone assembling geodesic 2-chains for H₁(S¹) composition or cyclic terminal-side corrections cites this. The proof is a one-line wrapper renaming the three free generators via geodesicFreeChain.
Claim. For all real lifts $p,q,r$, the free singular boundary of the lift-affine $2$-simplex on $(p,q,r)$ equals $\mathrm{geo}(q,r)-\mathrm{geo}(p,r)+\mathrm{geo}(p,q)$ in the free $C_1$ module, where $\mathrm{geo}(a,b)$ is the free generator of the geodesic (lift-linear) singular edge from $a$ to $b$.
background
This module lifts path-level winding/displacement on $S^1$ to singular simplices and proves that displacement kills boundaries, giving the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
The free boundary map sends a singular $2$-simplex to the alternating sum of its three singular $1$-faces in the free $C_1$ module. The lift-affine $2$-simplex on real endpoints $(p,q,r)$ is the singular $2$-simplex induced by the affine map on lifts, then projected to the circle. A geodesic free chain is the free generator of the corresponding lift-linear singular edge.
Upstream, the geodesic composition law already states that this free boundary equals the three freeMk geodesic edges with signs $+\mathrm{geo}(q,r)-\mathrm{geo}(p,r)+\mathrm{geo}(p,q)$. In particular $\mathrm{geo}(p,q)+\mathrm{geo}(q,r)$ is homologous to $\mathrm{geo}(p,r)$: geodesics compose additively in $H_1$.
proof idea
One-line term wrapper. It applies the already-proved geodesic composition law singularTwoBoundaryFree_freeMk_linearSingularTwoSimplex at $(p,q,r)$, then reads the three freeMk geodesic edges as the definition of geodesicFreeChain. No new face computation or homotopy is performed here.
why it matters
This is the named composition law in free $C_1$ used wherever geodesic edges are packaged as free chains rather than raw singular simplices. Downstream, singularTwoBoundaryFree_linear_step rewrites the one-turn cone boundary $\partial(\mathrm{linear},0,2\pi,(z+2\pi))$ by invoking this identity and folding a shifted side via $2\pi\mathbb{Z}$ invariance. The larger parent orientedCyclicFamilies_terminalSideCorrection_generate_holds builds the bounding $2$-chain for terminal-return sides of oriented cyclic families from lift-affine cones, citing this composition law as the first family of summands.
In the module narrative this is bookkeeping for the kills-boundaries / generation pipeline toward $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$: additive geodesic composition is how integer windings assemble from edgewise lifts. It does not itself touch the forcing chain T0–T8 or the J-cost RCL; it is pure singular-chain infrastructure for the circle.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.