singularTwoBoundaryFree_freeMk_coneSingularTwoSimplexOfPath
plain-language theorem explainer
For any continuous path γ on the circle, the free singular boundary of the cone 2-simplex over γ equals the free generator of the terminal-return edge, minus the constant apex edge, plus the path itself as a singular 1-simplex. Homology and circle-winding arguments cite this as the single-path prism brick. The proof unfolds the cone, applies the free boundary formula, and rewrites the three faces via the cone face lemmas.
Claim. Let $\gamma:I\to S^1$ be continuous. Write $C(\gamma)$ for the singular $2$-simplex obtained by coning $\gamma$ to its initial point. Then the free singular boundary satisfies $\partial^{\mathrm{free}}_2[C(\gamma)]=[\mathrm{terminal\text{-}return}(\gamma)]-[\mathrm{const}_{\gamma(0)}]+[\gamma]$, where each bracket denotes the free generator of the corresponding singular $1$-simplex.
background
The module CircleWindingChain lifts the path-level winding/displacement invariant of CircleWinding to singular simplices of $S^1=\mathrm{TopCat.sphere},1$, and proves that displacement kills boundaries: for every singular $2$-simplex $F$, $\mathrm{disp}(\delta_0 F)-\mathrm{disp}(\delta_1 F)+\mathrm{disp}(\delta_2 F)=0$. That identity, with the once-around generator sending to $1$, yields the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
A cone over a path $\gamma:I\to S^1$ is the singular $2$-simplex obtained by joining every point of $\gamma$ to the apex $\gamma(0)$. Its three faces are computed by the upstream face lemmas: $\delta_0$ is the terminal-return side, $\delta_1$ is the constant edge at the apex, and $\delta_2$ is the path reparameterized as a singular $1$-simplex. The free boundary operator on free $2$-chains is the alternating sum of those faces after free generators are applied.
This declaration packages that face computation into a single free-module identity, the "path-parametric cone boundary shell" that the doc-comment calls the primitive finite-prism brick.
proof idea
Term/tactic proof by successive rewriting. Unfold the definition of the cone singular $2$-simplex (it is singularTwoSimplexOfMap of the continuous cone map). Apply the free-module boundary formula singularTwoBoundaryFree_freeMk, which turns the free generator of a $2$-simplex into the alternating free sum of its three faces. Expand each face via singularTwoSimplexOfMap_delta three times. Finish by the three cone face identities: coneCircleMapOfContinuous_face_zero (terminal-return), coneCircleMapOfContinuous_face_one (constant apex), and coneCircleMapOfContinuous_face_two_path (base path). No homotopy or displacement arithmetic is needed here; pure face bookkeeping.
why it matters
This is the single-path brick for the finite-prism / subdivision apparatus that the module doc identifies as still missing from Mathlib's singular homology, and that is required for the generation (surjectivity) half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. Downstream, singularTwoBoundaryFree_coneSingularTwoChainOfPathFamily sums the identity over a finite family of paths: the summed cone boundary becomes sum of terminal sides minus sum of constant apex sides plus sum of base edges, "the algebraic target whose side terms must telescope in the multi-edge prism."
In the Recognition Science foundation layer this supports the winding homomorphism on $1$-cycles as a left inverse to the fundamental class, completing the split-injective half already obtained from simplexDisplacement_boundary and pathWinding_fundamentalLoop. The cone shell is the elementary step toward proving every $1$-cycle is homologous to an integer multiple of the fundamental cycle, without axioms or project-local $S^1$ replacements.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.