geodesicFreeChain_self_bounds
plain-language theorem explainer
A geodesic free 1-chain with equal endpoints equals the free boundary of the constant singular 2-simplex at that circle point. Anyone assembling null-homotopies or terminal-side corrections for cyclic families on S¹ cites this degenerate base case. The proof unfolds the free geodesic chain, collapses the equal-endpoint geodesic to a constant edge, and applies the constant-simplex free-boundary identity.
Claim. For every real $a$, the image of the free generator on the constant singular $2$-simplex at the trigonometric circle point of $a$ under the free singular boundary $C_2\to C_1$ equals the free $1$-chain of the geodesic from $a$ to $a$.
background
This module lifts path-level winding and displacement on $S^1$ to singular simplices and proves that displacement kills boundaries, the chain-level fact needed for a winding homomorphism on $H_1(S^1)$. Singular $1$- and $2$-simplices are continuous maps from the standard simplices into $\mathrm{TopCat.sphere},1$; free chains are the free modules on those simplices, and singularTwoBoundaryFree is the explicit free boundary operator.
A geodesic free chain is the free $C_1$ generator of a lift-linear singular edge between two real lifts. The trigonometric circle point sends a real parameter to the corresponding point of the exact sphere object. When the two lifts coincide, the geodesic edge is constant: equal-endpoint geodesics reduce to the constant singular $1$-simplex at that projected point.
Upstream, the constant singular $1$-simplex is already known to bound the constant singular $2$-simplex in the free complex ("the degenerate base case of the null-homotopy prism construction").
proof idea
Term-mode, three steps. Unfold the definition of the geodesic free chain so the goal is about free generators of singular edges. Rewrite with the equal-endpoint geodesic identity (geodesic $a\to a$ is the constant edge at the trigonometric point) and the identification of that constant edge with the constant singular $1$-simplex under the map-to-simplex constructor. Finish by the constant free-boundary theorem: the free boundary of the constant $2$-simplex at that point is exactly the free generator of the constant $1$-simplex.
why it matters
Degenerate geodesics must be boundaries if free geodesic edges are to serve as a workable basis for cycle corrections on the circle. Downstream, the terminal-side correction generator for oriented cyclic families uses this identity when lift endpoints agree (modulo full turns the connectivity forces). That parent theorem closes the terminal-return sides of a cyclic family by assembling lift-affine cones, winding steps, and these constant-simplex bounds into an explicit free $2$-chain.
In the module's larger program this is the base case of the prism/null-homotopy toolkit that supports the "winding kills boundaries" identity and the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. It does not itself touch the forcing chain T0–T8 or the Recognition Composition Law; it is pure singular-chain bookkeeping on the circle that the foundation layer needs before homology comparisons can feed higher Recognition structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.