constantSingularOneSimplex_free_boundary
plain-language theorem explainer
The constant singular 1-simplex at a point of S¹ is the free-module boundary of the constant singular 2-simplex at that same point. Cite this for the degenerate base of the prism null-homotopy and for free-chain boundary computations on the circle. The proof expands the free boundary as the alternating face sum, identifies all three faces with the same constant 1-simplex, and cancels by abelian arithmetic.
Claim. For every point $p$ on $S^1$, the free-module boundary of the free generator of the constant singular $2$-simplex at $p$ equals the free generator of the constant singular $1$-simplex at $p$.
background
This module lifts path-level winding 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;\mathbb{Z})$. The free chain complex is an explicit $\mathbb{Z}$-module presentation of singular chains: free generators are actual continuous maps $\Delta^n\to S^1$, and the free $2$-boundary is the alternating sum of the three face maps $\delta_0-\delta_1+\delta_2$.
The constant singular $1$-simplex (resp. $2$-simplex) at $p$ is the continuous map sending all of $\Delta^1$ (resp. $\Delta^2$) to $p$. An upstream face lemma records that every face of the constant $2$-simplex is again the constant $1$-simplex at $p$. The free boundary map is defined by free descent of that alternating face combination.
The local goal is the degenerate base case of the null-homotopy prism: a constant edge should bound a constant triangle in free chains, before non-constant geodesic and prism constructions are built.
proof idea
Term-mode rewrite proof. First apply the free-generator evaluation of the free $2$-boundary, which expands the left-hand side to the alternating sum of free generators of the three faces. Then rewrite each face via the constant-face lemma: $\delta_i$ of the constant $2$-simplex at $p$ is the constant $1$-simplex at $p$ for $i=0,1,2$. The resulting expression is freeMk(c) − freeMk(c) + freeMk(c); abel finishes the cancellation in the free abelian group.
why it matters
This is the degenerate base of the null-homotopy prism construction on free singular chains of $S^1$. Downstream it feeds the raw-chain form of the same identity (constant $2$-simplex boundary in Mathlib's singular complex), the statement that a degenerate geodesic (equal endpoints) bounds a constant $2$-simplex, the oriented singular-edge apparatus, and the transport lemma that free-boundary equalities push to raw Mathlib boundaries.
In the module's larger program, winding on $1$-cycles is a left inverse to the fundamental class (split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$). Constant simplices are the zero-displacement base against which geodesic edges and prism subdivisions are measured; without this free-boundary identity the degenerate geodesic would not be known to be a boundary. No Recognition forcing-chain step (T0–T8) is invoked here; the result is pure singular-homology scaffolding for the circle winding invariant.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.