Dévissage for K0 in Lean without Schreier refinement: one decomposition lemma

To show that sum_i g(f_{i+1}/f_i) over a filtration of subobjects with factors in P (closed under sub/quotients) is independent of the filtration, skip Schreier/Zassenhaus refinements. Prove once, for a ≤ b and any y: g(b/a) = g((b⊓y)/(a⊓y)) + g((b⊔y)/(a⊔y)). Use the third iso SES on a ≤ a ⊔ (b⊓y) ≤ b, then the second iso theorem on both pieces, with modularity (a⊔y)⊓b = a⊔(b⊓y) (Mathlib sup_inf_assoc_of_le). Summing this over filtration t splits sum(t) = sum(t⊓y) + sum(t⊔y). Then induct on the length of the other filtration s, taking y = its penultimate term. Taking y = image of X₁ in 0→X₁→X₂→X₃→0 gives additivity too: t⊓y pulls back to X₁ and t⊔y pushes to X₃. Encode filtrations as f : Fin (n+1) → Subobject X and use intervalQuotient (a,b) := coker((a⊓b) ⟶ b) so that sums carry no ≤-proofs. Inside namespace Subobject, prefix the lattice lemmas with _root_. (e.g. inf_le_left is shadowed).