intNatAbs_mul_signUnit_eq_self
plain-language theorem explainer
For every integer a, the product of its absolute value with the two-valued sign unit (1 if a>0, else -1) equals a itself, including at zero. Chain-level bookkeeping on singular 1-cycles cites this when reconstructing oriented coefficients from absolute multiplicities. The proof is a positivity case split discharged by omega.
Claim. For every $a \in \mathbb{Z}$, $\lvert a \rvert \cdot s(a) = a$, where $s(a) = 1$ if $a > 0$ and $s(a) = -1$ otherwise (so $s(0) = -1$ and the identity still holds).
background
The ambient module lifts path winding on $S^1$ to singular 1-simplices and proves that simplex displacement kills boundaries: the alternating face sum of any singular 2-simplex vanishes. That identity, with the generator sending the once-around loop to winding 1, supplies the split-injective half of $H_1(S^1;\mathbb{Z}) \cong \mathbb{Z}$.
Integer free chains on singular 1-simplices carry coefficients in $\mathbb{Z}$. Oriented cyclic peels scale a closed walk by a positive integer multiplicity and subtract; recovering a signed coefficient from its absolute value and a discrete sign choice is elementary $\mathbb{Z}$-arithmetic used in the support-cardinality decrease.
The sign unit here is the piecewise constant ${+1,-1}$-valued selector on positivity, not the classical $\mathrm{sgn}$ with $\mathrm{sgn}(0)=0$. Absolute value is the usual $\mathrm{natAbs}$ cast back to $\mathbb{Z}$.
proof idea
Case split on the proposition $0 < a$. On the positive branch, rewrite the conditional to $+1$ and finish with omega (which knows $\lvert a \rvert = a$ when $a > 0$). On the complementary branch, rewrite to $-1$ and again apply omega (covering both $a < 0$, where $\lvert a \rvert \cdot (-1) = a$, and $a = 0$). No external lemmas are required.
why it matters
Parent use is edgeSupportCard_sub_scaled_orientedCyclic_lt: scaling a sign-selected oriented closed walk by the minimum absolute coefficient strictly shrinks edge-support cardinality, the bookkeeping for an exact cyclic peel (minimum-coefficient edge cancelled, no new edges introduced). Reconstructing the original integer coefficient from absolute value times sign unit is the algebraic step that makes the scaled subtraction well-defined on free $\mathbb{Z}$-chains.
In the broader CircleWindingChain story this supports the generation/peeling half of the integer comparison map on $H_1(S^1)$, complementary to the already-proved kills-boundaries identity. It is pure coefficient arithmetic, not a topological landmark (T0–T8, RCL, $\varphi$), but it is load-bearing for the support-induction that closes the peel.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.