The pretriangulated H⁰ of a dg category

The intrinsic triangulated theory of H⁰ C for a pretriangulated dg category C: the zero object, the shift, the distinguished triangles built from dg cones, the functorial cone diagrams, and the exactness of the functors and natural transformations DGFunctor.h0 produces.

Every statement below is about C alone. No ordinary category has been chosen, no comparison equivalence appears, and nothing here imports an enhancement consumer, a scheme realization or a stability module. Comparing this structure with a specified triangulated category is CategoryTheory/Triangulated/DGEnhancement/; realizing it on Mathlib's homotopy category is Algebra/Homology/HomotopyCategory/DGEnhancement/.

The Grothendieck-group readings of these triangles -- Euler forms, K₀ classes of twists and cones -- consume CategoryTheory/Triangulated/GrothendieckGroup/ and stay with it, below DGEnhancement/H0/. They are downstream of this root, not part of it.