sign_unit_ne_zero
plain-language theorem explainer
For every integer coefficient, the associated sign unit is either +1 or -1, hence never zero. Cited when building edge supports and oriented cyclic chains on singular 1-simplices so coefficients cannot collapse support. Proof is a two-branch case split on positivity, closed by simplification.
Claim. For every $a \in \mathbb{Z}$, the integer equal to $1$ when $0 < a$ and equal to $-1$ otherwise is nonzero.
background
This module lifts the path-level winding and displacement invariant of the circle to singular simplices of $S^1$, and proves that simplex displacement kills boundaries. That identity is the chain-level fact making winding a homology invariant, and (with the generator evaluation) supplies the split-injective half of $H_1(S^1;\mathbb{Z}) \cong \mathbb{Z}$.
Oriented cyclic chains are assembled from an injective family of singular 1-simplices with integer coefficients. Each coefficient contributes a sign unit: $+1$ when the coefficient is positive and $-1$ otherwise. Support membership for the resulting free chain is defined in terms of nonzero edge coefficients, so the sign unit must be shown never to vanish. The claim is pure integer arithmetic and does not depend on the topology of $S^1$.
proof idea
Case-split on the proposition $0 < a$. In the positive branch the conditional simplifies to $1 \neq 0$; in the complementary branch it simplifies to $-1 \neq 0$. Both residual goals close by simp with the case hypothesis in the context. No external lemmas are required.
why it matters
The sole recorded consumer is edgeSupport_orientedCyclicChain, which states that the support of an oriented closed walk equals the image of its edge family. That identity needs the sign unit of each coefficient to be nonzero so that support membership tracks the image of the injective edge map rather than dropping edges under a vanishing coefficient.
In the broader module story, edge-support control is infrastructure for the winding homomorphism on 1-cycles. Together with the evaluation of the once-around generator, this yields the left inverse to the fundamental class (split-injectivity of the integer comparison map for $H_1(S^1;\mathbb{Z})$). Surjectivity, i.e. generation of every 1-cycle by the fundamental cycle, still needs a simplicial prism or subdivision operator that Mathlib singular homology does not yet supply.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.