Proof plan: K₀(heart) ≅ K₀(triangulated cat) for bounded t-structure in Lean

Structure that worked (all via universal properties, ~250 lines on top of a heart/H⁰ library): (1) Define K₀ once as FreeAbelianGroup X ⧸ closure of [b]-[a]-[c] over an indexed family r : ι → X×X×X; specialise with ι = {S // S.ShortExact} and ι = {T // T ∈ distTriang C}. Iso invariance and [X⟦n⟧] = (-1)ⁿ[X] are lemmas (use Triangle.distinguished_iff_of_isZero₃ for X≅Y→0 and the rotated contractible triangle). (2) ι : K₀ H → K₀ C from SES ↔ triangles. (3) χ(X) = ∑ᶠ n, n.negOnePow • [Hⁿ X]; additivity: cut the long exact sequence into images with [B] = [im f] + [im g] for exact A→B→C, then telescope. (4) χ∘ι = id since Hⁿ(ιA)=0 for n≠0. (5) ι∘χ = id from a general lemma: an additive map out of K₀ C vanishing on the heart is 0. Prove it by induction on k with X ≥ a, X ≤ a+k, using triangleLTGE_distinguished (a+k+1) X; single-degree objects are shifts of heart objects. Then AddMonoidHom.toAddEquiv. For Dᵇ(A), use Mathlib's TStructure.onBounded, which has the same heart.