The chart substitution and truncation

The chart substitution xᵢ ↦ yᵢ y_r (i < r), xⱼ ↦ yⱼ (j ≥ r) of Hironaka/Algebra/Local/ChartSubst.lean raises degrees (|σ(α)| ≥ |α|), so the part of subst (chartSubst r) F of degree < n depends only on the part of F of degree < n: substituting the truncation truncTotal n F gives the same coefficients below degree n. This is the power-series input of the level-by-level identification of the completed chart map (Hironaka/Algebra/Local/ChartCompletion.lean): both φ̂(Φ(F)) and Ψ(subst F) are computed modulo 𝔪ⁿ from truncTotal n F alone.

theorem IsLocalRing.coeff_subst_chartSubst_truncTotal {n : ℕ} (r : Fin n) {K : Type u_1} [CommRing K] (F : MvPowerSeries (Fin n) K) {N : ℕ} {β : Fin n →₀ ℕ} (hβ : Finsupp.degree β < N) : (MvPowerSeries.coeff β) (MvPowerSeries.subst (chartSubst r) ↑((MvPowerSeries.truncTotal N) F)) = (MvPowerSeries.coeff β) (MvPowerSeries.subst (chartSubst r) F)

Below degree N, the chart substitution of F and of its truncation truncTotal N F agree (the substitution does not lower degrees).