eq_sign_unit_of_natAbs_eq_one
plain-language theorem explainer
Any integer of absolute value one equals its sign unit: +1 if positive, −1 otherwise. Cited when unit coefficients appear in free singular 1-chains on the circle, especially support-cardinality arguments for oriented cyclic walks. The proof is a two-branch case split on the sign, discharged by omega.
Claim. If $a \in \mathbb{Z}$ satisfies $|a| = 1$, then $a$ equals its sign unit: $a = 1$ when $a > 0$, and $a = -1$ otherwise.
background
The ambient module lifts path-level winding and displacement from CircleWinding to singular simplices of $S^1$. It defines simplexDisplacement on continuous maps $\Delta^1 \to S^1$ and proves that the alternating face sum of displacements vanishes on every singular 2-simplex, so winding kills boundaries and yields a left inverse to the fundamental class on $H_1(S^1;\mathbb{Z})$.
In the free abelian group of singular 1-chains, edge coefficients are integers. A coefficient of absolute value one is a unit coefficient: it marks an edge that can be peeled off by subtracting a signed oriented cyclic walk without residual multiplicity. The present lemma identifies such a coefficient with the pure sign $\pm 1$ used when building that walk.
No Recognition-Science cost functional or forcing-chain step is involved; the statement is pure integer arithmetic supporting the chain-level bookkeeping.
proof idea
Case-split on whether $0 < a$. In the positive branch, rewrite the conditional to $1$ and finish with omega using $|a|=1$. In the non-positive branch, rewrite to $-1$ and again use omega (the only remaining integer of absolute value one is $-1$). No external lemmas are required.
why it matters
Downstream, edgeSupportCard_sub_orientedCyclic_lt_of_unitCoeff uses this identification: if a sign-selected oriented closed walk hits a unit coefficient of the ambient flow, subtracting that walk strictly shrinks edge-support cardinality. That isolates the support-cardinality half of large-support extraction from the separate encoding of mixed-orientation walks.
In the broader CircleWindingChain story, unit-coefficient peeling is part of reducing 1-cycles toward integer multiples of the fundamental loop, the generation half of $H_1(S^1;\mathbb{Z}) \cong \mathbb{Z}$. The module already has the kills-boundaries identity and the once-around generator; this tiny arithmetic fact keeps the support-reduction step free of residual $\pm 1$ bookkeeping errors.
It does not itself touch T0–T8, RCL, or the phi ladder; it is infrastructure for the singular-homology comparison on the circle.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.