Addition preserves A3X Taylor-model enclosures

Proved

CKLaneA3X.TMd.add_good

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

a3xgeneral-courtade-kumartaylor-models

The unchanged source soundness theorem for adding two valid A3X Taylor models, lowering their orders to the same minimum and retaining the exact original rounded remainder.

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.add_good {f g : ℝ → ℝ → ℝ} {a b : TMd} (ha : Good f a) (hb : Good g b) :
    Good (fun t ρ => f t ρ + g t ρ) (TMd.add a b) := by sorry

Source

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

View graph