exists_next_orientedEdge_from_terminal
plain-language theorem explainer
In a free singular 1-chain on S¹ with vanishing boundary, every supported non-loop oriented edge admits a supported successor whose sign-selected orientation begins at that edge's terminal vertex. Cycle-extraction and homology-generation arguments on balanced edge-flows cite this local step. The proof obtains a negative boundary contribution at the terminal, then reads off the initial vertex of the contributing edge.
Claim. Let $c$ be a finitely supported free singular $1$-chain on $S^1$ with $\partial c = 0$. If $e$ lies in the support of $c$ and the sign-selected orientation of $e$ is not a loop (initial vertex $\neq$ terminal vertex), then there exists $e'$ in the support of $c$ whose sign-selected orientation starts at the terminal vertex of the orientation of $e$.
background
The module lifts path-level winding on the circle to singular simplices of $\mathrm{TopCat.sphere},1$ and proves that simplex displacement kills boundaries, giving the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. Singular $0$- and $1$-simplices are the actual objects of the singular simplicial set; free $1$-chains are finite-support $\mathbb{Z}$-linear combinations of those $1$-simplices.
A chain is balanced when its image under the free singular boundary map is zero. The edge support is the finite set of $1$-simplices with nonzero coefficient. Each supported edge carries a sign-selected orientation (orientedEdgeOfCoeff) whose initial and terminal vertices are the endpoints after that sign choice. Edge contribution at a vertex is the signed incidence of that oriented edge in the boundary coefficient.
Upstream, exists_negative_edgeContribution_at_oriented_terminal states that in a balanced flow a positive contribution at a vertex forces some negative contribution at the same vertex; applied to a sign-selected supported edge this is the algebraic core of the next-edge step. initial_eq_of_negative_edgeContribution then converts a negative contribution at $v$ into the equality that the oriented initial of that edge is $v$.
proof idea
Short tactic proof, two steps. First apply exists_negative_edgeContribution_at_oriented_terminal to the balanced hypothesis, the membership of $e$ in the edge support, and the non-loop assumption; this yields a supported edge $e'$ together with a negative edge-contribution of $e'$ at the oriented terminal of $e$. Then package the witness with initial_eq_of_negative_edgeContribution, which turns that negative contribution into the equality that the oriented initial of $e'$ equals the oriented terminal of $e$. No further case analysis or boundary rewriting is needed at this layer.
why it matters
This is the local successor step for oriented closed-walk extraction on balanced free edge-flows. The sole downstream consumer is exists_orientedCyclicFamily_of_balanced_nonzero, which asserts that every nonzero balanced free edge-flow admits a positive-length family of distinct supported edges whose sign-selected orientations connect terminal-to-initial cyclically.
That extraction is the combinatorial engine behind the generation half of the integer comparison map on $H_1(S^1;\mathbb{Z})$: once every balanced nonzero chain contains an oriented cycle, winding (via simplexDisplacement and the kills-boundaries identity) can peel off fundamental-class multiples. The module doc frames the remaining open piece as surjectivity of the comparison map, which still needs a simplicial prism or subdivision operator that Mathlib's singular homology does not yet supply. Within Recognition Science this sits in the Foundation layer that makes the circle's first homology an explicit $\mathbb{Z}$, feeding later geometric and forcing arguments that rely on a rigorously identified generator.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.