natAbs_sign_unit
plain-language theorem explainer
For every integer, the edge sign-unit (1 if positive, else −1) has natural absolute value exactly 1. Downstream ℓ¹ identities for oriented cyclic singular 1-chains cite this to convert signed support into cardinality. The proof is a two-branch case split on positivity, each closed by decide.
Claim. For every integer $a\in\mathbb{Z}$, if one sets $s(a)=1$ when $a>0$ and $s(a)=-1$ otherwise, then $|s(a)|=1$ (as a natural number).
background
The 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; orientation relative to a flow is recorded by a $\pm 1$ coefficient on each supported edge.
That coefficient is exactly the piecewise choice in the statement: $+1$ when the integer coefficient of the edge is positive, $-1$ otherwise (including zero). The $\ell^1$ size of a chain is the sum of absolute values of coefficients on the edge support, so one needs $|\pm 1|=1$ as a natural number before counting edges in an oriented cyclic walk.
No Recognition-calculus primitives are used; the lemma is pure integer arithmetic supporting the chain-level bookkeeping.
proof idea
Tactic proof by cases on the decidable predicate $0<a$. On the positive branch, rewrite the conditional with if_pos to $1$ and close by decide. On the complementary branch, rewrite with if_neg to $-1$ and again decide. No external lemmas are required.
why it matters
Feeds chainL1_orientedCyclicChain (the $\ell^1$ size of an oriented closed walk through $k$ injective edges equals $k$) and chainL1_sub_orientedCyclic (peeling one such walk from a balanced flow drops $\ell^1$ by exactly $k$). Those identities are the quantitative engine for cycle-peeling arguments on singular 1-chains once winding is known to vanish on boundaries.
In the module narrative this sits under the homology-invariant winding map that left-inverts the fundamental class of $S^1$. It does not itself touch the forcing chain (T0–T8), RCL, or $\varphi$; it is pure foundation for the circle computation that later interfaces with Recognition geometry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.