down_prev_one_eq_two
plain-language theorem explainer
In the downward ℕ-indexed chain-complex shape, the predecessor of degree 1 is degree 2. Anyone specializing singular-homology exactness or boundary-lifting at H₁ of the circle cites this degree bookkeeping fact. The proof unfolds ComplexShape.prev and closes both branches of the existential split via the down-relation 2 Rel 1.
Claim. For the downward chain-complex shape on $\mathbb{N}$, $\mathrm{prev}(1)=2$. Equivalently, the unique degree $n$ with a differential $C_n\to C_1$ in that shape is $n=2$.
background
Mathlib indexes chain complexes by a ComplexShape on the degree type. The downward shape ComplexShape.down ℕ has relation $n\mathrel{R}m$ iff $n=m+1$, so differentials run $C_{m+1}\to C_m$. The operation prev i is the unique predecessor of degree $i$ when it exists (an existential choice under that relation).
This module lifts path-level winding on $S^1$ to singular 1-simplices and proves that displacement kills boundaries of 2-simplices. That identity is the chain-level half of the winding homomorphism on $H_1(S^1;\mathbb{Z})$. When one writes an element-level exactness statement at degree 1 ("a 1-cycle homologous to zero is a 2-boundary"), the ambient shape must supply prev 1 = 2 so that the boundary operator lands in the correct degree.
No Recognition-Science constants or forcing-chain steps are involved; the lemma is pure degree arithmetic for the singular chain complex of the circle.
proof idea
Tactic proof. Unfold ComplexShape.prev, which is defined by a dite on existence of a related degree. In the positive branch, apply prev_eq to the chosen witness and rewrite the relation via ComplexShape.down_Rel, then close with norm_num (the witness is 2). In the negative branch, derive a contradiction by exhibiting the explicit pair $\langle 2,, 2\mathrel{R}1\rangle$, again via down_Rel and norm_num. No external project lemmas are used.
why it matters
Feeds cycle_eq_boundary_of_homologyπ_eq_zero in the same module: that theorem states a degree-1 cycle whose homology class vanishes is explicitly a degree-2 boundary (element-level exactness of the homology cokernel on the circle singular complex). Without prev 1 = 2, the boundary operator's source degree is not identified, and the cokernel statement cannot even be typed at the right place.
In the module narrative this is scaffolding for the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ via the winding invariant (simplexDisplacement / pathWinding_fundamentalLoop). The converse generation half still needs a simplicial prism or subdivision operator that Mathlib singular homology does not yet supply. The lemma itself is not a Recognition forcing step (T0–T8); it is local homological bookkeeping that lets the winding story sit on Mathlib's chain complexes cleanly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.