incidenceCoeff
plain-language theorem explainer
The incidence coefficient of a directed singular edge on S¹ at a singular vertex is +1 at the terminal endpoint, −1 at the initial endpoint, and their algebraic sum when the edge is a loop. Anyone assembling the singular boundary operator or a finite free edge-flow on the circle cites it. The body is a one-line difference of two equality indicators on the face maps.
Claim. Let $e$ be a singular $1$-simplex on $S^1$ and $v$ a singular $0$-simplex. Write $t(e)$ and $s(e)$ for the terminal and initial vertices of $e$ (the images under the two face maps $\delta_0$ and $\delta_1$). The incidence coefficient is $I(e,v)=\mathbf{1}_{t(e)=v}-\mathbf{1}_{s(e)=v}\in\mathbb{Z}$. In particular $I(e,t(e))=+1$, $I(e,s(e))=-1$ when the endpoints are distinct, and $I(e,v)=0$ when $v$ is neither endpoint; if $s(e)=t(e)=v$ then $I(e,v)=0$.
background
The module lifts the path-level winding/displacement invariant of CircleWinding to singular simplices of $\mathrm{TopCat.sphere},1$, and proves that displacement kills boundaries: for every singular $2$-simplex the alternating face sum of displacements vanishes. That identity, together with the once-around generator mapping to $1$, supplies 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 of $S^1$. The initial vertex of a directed singular edge $e$ is the face $\delta_1 e$; the terminal vertex is $\delta_0 e$. These match the negative and positive terms in the classical singular boundary $\partial_1 e=t(e)-s(e)$.
The incidence coefficient packages that signed endpoint test as an integer-valued function of the pair $(e,v)$, ready for finite free sums over edge supports.
proof idea
Pure definition: evaluate two decidable equalities and subtract. The first indicator is $1$ precisely when $v$ equals the terminal face $\delta_0 e$; the second is $1$ when $v$ equals the initial face $\delta_1 e$. No lemmas are applied.
why it matters
This is the local building block for every finite-support boundary computation in the module. Downstream, boundaryIncidenceSum sums $n\cdot I(e,v)$ over a free edge-chain; edgeContribution isolates one edge's share; positivity and sign-selection lemmas (edgeContribution_pos_at_oriented_terminal, initial_eq_of_negative_edgeContribution) use it to force compensating outgoing edges in a balanced flow. The equality vertexBoundaryCoeff_eq_incidenceSum_holds identifies the abstract boundary coefficient with this incidence sum, which is the finite-support algebra needed for the support-decreasing graph argument toward the generation half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
In the broader Recognition chain the winding homomorphism on $1$-cycles is the topological half of the eight-tick / circle story (T7); the incidence data is the chain-level bookkeeping that makes the kills-boundaries identity usable on free chains rather than single simplices.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.