The A3X J plus Jw sum has its stored enclosure
ProvedCKLaneA3X.S_JJwa3xgeneral-courtade-kumartaylor-models
The exact original conditional source theorem: assuming Good F_J D_J and Good F_Jw D_Jw, their sum has the original stored D_JJw certificate. All source assumptions and arithmetic are retained.
Preamble
import Definitions.Def_A3X_numeric_core import Definitions.Def_A3X_Step027_data_functions import Definitions.Def_A3X_enclosure import Definitions.Def_A3X_Step028_second_chain set_option maxHeartbeats 0 set_option maxRecDepth 100000 open CKLaneA3X
Formal statement
theorem CKLaneA3X.S_JJw (G_J : Good F_J D_J) (G_Jw : Good F_Jw D_Jw) : Good F_JJw D_JJw := by sorry
Source