Rational scaling preserves an A3X Taylor-model enclosure

Proved

CKLaneA3X.TMd.scale_good

by marwahaha · Sep 25, 2026 · Mathlib 0df444a (Lean v4.33.1)

a3xgeneral-courtade-kumartaylor-models

The unchanged source soundness theorem for scaling any valid A3X Taylor model by a rational constant, retaining the original absolute-value remainder and upward rounding.

Preamble

import Mathlib.Analysis.Complex.ExponentialBounds
import Mathlib.Tactic.Ring
import Mathlib.Tactic.NormNum
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.Positivity
import Mathlib.Tactic.SplitIfs
import Mathlib.Tactic.LinearCombination
import Mathlib.Tactic.FieldSimp
import Definitions.Def_A3X_numeric_core
import Definitions.Def_A3X_enclosure
import Definitions.Def_A3X_Step028_first_chain

open CKLaneA3X

Formal statement

theorem CKLaneA3X.TMd.scale_good {f : ℝ → ℝ → ℝ} {a : TMd} (ha : Good f a) (c : ℚ) :
    Good (fun t ρ => (c : ℝ) * f t ρ) (TMd.scale c a) := by sorry

Source

https://github.com/dpwoodru/general-courtade-kumar-lean/blob/04b6fc3f75b10c3c43702a883ddf888b0608a9a0/browse/CKLaneA3X/TMFun.lean#L97

View graph