singularTwoBoundaryFree_freeMk_pathBacktrack
plain-language theorem explainer
The free singular boundary of the triangular path-backtrack 2-simplex on a continuous path γ in S¹ equals the free 1-chain reverse(γ) − constant(γ(0)) + γ. Anyone computing oriented edge boundaries or prism corrections in the circle winding chain cites this identity. The proof unfolds the backtrack simplex, applies the free boundary formula, and matches the three faces to reverse path, constant initial edge, and original path.
Claim. For every continuous path $\gamma : I \to S^1$, the image of the free generator on the path-backtrack singular $2$-simplex under the free singular boundary map equals $\mathrm{free}(\mathrm{rev}(\gamma)) - \mathrm{free}(\mathrm{const}_{\gamma(0)}) + \mathrm{free}(\gamma)$ as a free singular $1$-chain.
background
The module lifts the path-level winding/displacement invariant of CircleWinding to singular simplices of $S^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 fundamental loop winding to $1$, gives the split-injective half of $H_1(S^1;\mathbb{Z}) \cong \mathbb{Z}$.
Here $S^1$ is the exact TopCat.sphere 1 carrier. Paths are continuous maps $I \to S^1$; reversePath reparameterizes by $t \mapsto 1-t$. Singular $1$-simplices arise from maps on the standard $1$-simplex (or from paths via reparameterization); the constant singular $1$-simplex sits at a fixed point. The free module functor turns these into generators of free chains, and singularTwoBoundaryFree is the induced free boundary on free $2$-chains.
The path-backtrack $2$-simplex is the triangular prism that runs $\gamma$ out and back, used to cancel oriented edge pairs in chain-level corrections.
proof idea
Term/tactic hybrid, purely equational. Unfold the definition of the path-backtrack singular $2$-simplex. Rewrite by the free-boundary evaluation lemma on free generators. Expand the three face operators of the underlying map-simplex via the delta identities. Match faces zero, one, and two of the backtrack map to reverse path, constant initial edge, and original path respectively. Finish by identifying the constant face with the constant singular $1$-simplex. No homotopy or winding arithmetic is invoked; only face bookkeeping.
why it matters
Feeds the oriented singular edge apparatus in the same module: oriented edges need a clean free-boundary formula for the backtrack prism so that reverse-plus-forward pairs cancel against the constant initial edge in free chains. That cancellation is part of the prism/subdivision toolkit the module doc flags as needed for the generation (surjectivity) half of $H_1(S^1;\mathbb{Z}) \cong \mathbb{Z}$, beyond the already-proved kills-boundaries identity for displacement.
In the Recognition foundation layer this sits under the circle winding chain that supports the eight-tick octave and discrete period structure (T7), by making singular homology of $S^1$ computable without axioms or project-local sphere replacements. It does not itself mention $\varphi$ or the J-cost; it is pure topological scaffolding for those later identifications.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.