Rational Chern twists and the real exponential action

The rational, intersection-ring-valued Numerical.twist is retained for its geometric consumers. Taking weighted degrees and extending scalars to ℝ intertwines it with Wall.Exp.twist. The truncation degree m may be smaller than the geometric dimension n; the comparison requires m ≤ n to combine the powers of the polarisation. The component family is arbitrary, so it may already include a correction class.

theorem AlgebraicGeometry.Numerical.twist_degree_eq_exp {A : Type u_1} [CommRing A] [Algebra ℚ A] {n : ℕ} (R : NumericalRingData n A) (H : A) (β : ℚ) (c : ℕ → A) (m : ℕ) (hmn : m ≤ n) : (fun (i : Fin (m + 1)) => ↑(R.degree (twist H β c ↑i * H ^ (n - ↑i)))) = CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Exp.twist m ↑β fun (i : Fin (m + 1)) => ↑(R.degree (c ↑i * H ^ (n - ↑i)))

Weighted degrees intertwine the rational intersection-ring twist with the real exponential action, at every truncation degree at most the dimension.