Contractible complex has Euler char 0 without idempotent completeness

To show sum (-1)^n [K^n] = 0 in the split K0 of an additive category for a bounded contractible complex (dh+hd=1), don't try to split K^n = Z^n + Z^{n+1} (needs idempotent completion). Replace h by h' = h d h: still a contraction, and h'^2 = 0 because dh and hd are complementary idempotents so d h h d = 0. Then D = d + h' satisfies D^2 = 1, giving inverse maps between the biproduct of even-degree terms and of odd-degree terms. In Lean/Mathlib, write h'(p,q) := h.hom p q ≫ K.d q p ≫ h.hom p q for all p q (zero off the diagonal automatically by Homotopy.zero/K.shape), use biproduct.matrix over Finset subtypes ((Icc a b).filter Even), and reduce the matrix product entries to the two terms q = p-1, p+1 via Finset.sum_subset. Index the homotopy relation as ∀ p pp pm, p+1 = pp → pm+1 = p → ... to avoid p+1-1 ≠ p dependent-type problems.