natAbs_sub_sign_unit
plain-language theorem explainer
For any nonzero integer a, subtracting its sign unit (±1) drops |a| by exactly one. Singular-chain ℓ¹ arguments that peel an oriented directed cycle cite this per-edge identity. The proof is a two-way case split on the sign of a, finished by omega.
Claim. Let $a \in \mathbb{Z}$ with $a \neq 0$, and let $s = +1$ if $a > 0$ and $s = -1$ if $a < 0$. Then $|a| = |a - s| + 1$.
background
The ambient module lifts path-level winding on $S^1$ to singular $1$-simplices and proves that simplex displacement kills boundaries, giving the split-injective half of $H_1(S^1;\mathbb{Z}) \cong \mathbb{Z}$. Chains are free $\mathbb{Z}$-linear combinations of singular $1$-simplices; the $\ell^1$ size of a chain is the sum of absolute values of its coefficients.
An oriented cyclic peel subtracts, from a balanced flow, a closed directed walk supported on $k$ distinct edges, each taken with the sign of the flow coefficient. On each such edge the coefficient loses one unit of magnitude, so the global $\ell^1$ drop equals $k$. The present lemma is the scalar arithmetic behind that one-edge drop: the sign unit of a nonzero integer is $\pm 1$, and subtracting it reduces absolute value by one.
proof idea
Case-split on whether $0 < a$. In the positive branch the conditional is $+1$; rewrite and finish with omega. In the complementary branch, $a \neq 0$ forces $a < 0$, the conditional is $-1$, and omega again closes the absolute-value identity. No external lemmas are required beyond integer arithmetic.
why it matters
Feeds chainL1_sub_orientedCyclic, which states that subtracting an oriented closed walk through $k$ distinct supported edges from a balanced singular $1$-chain lowers the $\ell^1$ size by exactly $k$. That peel identity is the quantitative engine for reducing supported cycles in the CircleWindingChain development.
In the broader module story, winding on singular $1$-simplices is already a homology invariant (displacement kills boundaries) and sends the fundamental loop to $1$. Controlling $\ell^1$ under cycle peels is the bookkeeping step toward comparing arbitrary $1$-cycles with integer multiples of the fundamental class. The generation half of $H_1(S^1;\mathbb{Z}) \cong \mathbb{Z}$ still needs a simplicial prism or subdivision operator that Mathlib singular homology does not yet supply; this lemma is pure coefficient arithmetic and does not close that gap.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.