Automatic numerical action of the scalar-linear object twist

The generic scalar-linear twist formulas consume an explicit LinearEvaluationData.IsEulerCopower witness. Over a field, finite bounded H⁰ Hom-spaces and the existence of scalar-linear copowers now construct that witness automatically, so the numerical Seidel--Thomas formula needs no additional presentation data.

Exactness comes from the generic dg-functor theorem, not from Hom-finiteness or formality; no sphericality or autoequivalence is inferred.

theorem CategoryTheory.LinearEvaluationData.TwistConeData.twistK₀Of_eq_twistK₀_ofHomFiniteBounded (k : Type v) [Field k] {C : Type u} [DGCategory C] [IsPretriangulated C] [(X Y : C) → (p : ℤ) → Module k ↑((DGCategoryStruct.dgHom X Y).X p)] [DGLinear k C] [Triangulated.HomFiniteBounded k (H0 C)] [∀ (n : ℤ), Functor.Linear k (shiftFunctor (H0 C) n)] [HasLinearCopowers k C] {E : C} {V : LinearEvaluationData k E} (K : TwistConeData k V) (X : H0 C) : Triangulated.K₀.of (H0 C) (K.twist.h0.obj X) = (Triangulated.SphericalTwist.twistK₀ k (H0 C) (have this := E; this)) (Triangulated.K₀.of (H0 C) X)

When all scalar-linear copowers exist, field formality and HomFiniteBounded automatically identify the evaluation-cone class with the numerical twist class.

theorem CategoryTheory.LinearEvaluationData.TwistConeData.twistK₀Map_eq_twistK₀_ofHomFiniteBounded (k : Type v) [Field k] {C : Type u} [DGCategory C] [IsPretriangulated C] [(X Y : C) → (p : ℤ) → Module k ↑((DGCategoryStruct.dgHom X Y).X p)] [DGLinear k C] [Triangulated.HomFiniteBounded k (H0 C)] [∀ (n : ℤ), Functor.Linear k (shiftFunctor (H0 C) n)] [HasLinearCopowers k C] {E : C} {V : LinearEvaluationData k E} (K : TwistConeData k V) : Triangulated.K₀.map K.twist.h0 = Triangulated.SphericalTwist.twistK₀ k (H0 C) (have this := E; this)

The induced endomorphism is the numerical twist without a separately supplied Euler copower witness.