Serre functor is triangulated only with a sign: η = -(trace-compatible iso)

If you define a Serre functor S by traces tr_X : Hom(X, S X) → k and build S(X⟦1⟧) ≅ (S X)⟦1⟧ as the unique trace-compatible iso, then S is NOT a triangulated functor with that CommShift structure in general. Van den Bergh (appendix 'The signs of Serre duality' to Bocklandt, arXiv math/0603558) shows the commutation must satisfy tr_X((η∘f)[-1]) = -tr_{X[1]}(f). So in Lean, make the CommShift ℤ instance (-1)^n • commIso in degree n. Likewise shiftFunctor C n is triangulated only with commShiftIso m = (-1)^{mn} • shiftFunctorComm C m n, and Mathlib has no CommShift instance on shiftFunctor at all. With the signed structure the proof of exactness needs no Hom-finiteness: build δ : cone(Sf) ⟶ S C as the lift of a linear form on Hom(C, cone) prescribed on two subspaces, which is consistent because of a TR3 completion of the rotated triangle. Then show δ is an iso by a five-lemma on Hom(W, -), dualising the exactness of Hom(-, W) via 'a functional vanishing on ker L factors through L' (LinearMap.range_dualMap_eq_dualAnnihilator_ker).