geodesicFreeChain_zero_twoPi_eq_fundamental
plain-language theorem explainer
The free singular 1-chain of the geodesic edge from 0 to 2π equals the free generator on the once-around fundamental singular 1-simplex of S¹. Anyone identifying free C₁ generators with the geometric fundamental class of the circle cites this. The proof unfolds the free-chain constructor and rewrites by the already-proved simplex-level geodesic identification.
Claim. The free $C_1$ generator of the geodesic singular edge from $0$ to $2\pi$ equals the free module generator on the once-around fundamental singular $1$-simplex of $S^1$.
background
This module lifts the path-level winding/displacement invariant of the circle to singular simplices of $S^1$ and proves that displacement kills boundaries, giving the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
A geodesic free chain geodesicFreeChain a b is the free $C_1$ generator on the singular $1$-simplex obtained from the lift-linear geodesic edge from $a$ to $b$ on the circle. The fundamental singular $1$-simplex is the once-around geometric generator candidate: the image of the standard fundamental circle path under the singular set functor on $S^1$.
Upstream, the simplex-level fact already holds: the singular simplex of the geodesic $0\to 2\pi$ equals that fundamental singular $1$-simplex. The free-chain layer is just ModuleCat.freeMk applied to that simplex.
proof idea
One-line style reduction. Unfold the definition of the geodesic free chain (free generator on the singular simplex of the geodesic edge). Rewrite with the upstream theorem that the singular simplex of the geodesic $0\to 2\pi$ is exactly the fundamental singular $1$-simplex. Equality of free generators follows immediately.
why it matters
Pins the free-coordinate geometric generator: the free chain of the full-turn geodesic is the fundamental free generator. Downstream, fundamentalCycleFreeChain_eq_zsmul uses this to show that the free-coordinate image of $n$ times the fundamental cycle is $n$ copies of the geodesic $0\to 2\pi$.
In the module's program this is the free $C_1$ half of the identification that makes winding a left inverse to the fundamental class (the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$). The generation/surjectivity half still needs a simplicial prism or subdivision operator that Mathlib singular homology does not yet supply. No RS forcing-chain step (T0–T8) is claimed here; the result is pure circle homology scaffolding for later Recognition geometry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.