The A3X coefficient sum has its stored enclosure
ProvedCKLaneA3X.S_coefa3xgeneral-courtade-kumartaylor-models
The exact original conditional source theorem: assuming the mInner and negative-product enclosures, their sum has the original stored coefficient certificate D_coef. The source addition proof and its numerical conditions are unchanged.
Preamble
import Definitions.Def_A3X_numeric_core import Definitions.Def_A3X_Step026_data import Definitions.Def_A3X_Step027_data_functions import Definitions.Def_A3X_enclosure import Definitions.Def_A3X_Step028_first_chain set_option maxHeartbeats 0 set_option maxRecDepth 100000 open CKLaneA3X
Formal statement
theorem CKLaneA3X.S_coef (G_mInner : Good F_mInner D_mInner) (G_mJwUsUs : Good F_mJwUsUs D_mJwUsUs) : Good F_coef D_coef := by sorry
Source