The A3X J plus Jw plus twice dR sum has its certificate
ProvedCKLaneA3X.S_JJw2dRa3xgeneral-courtade-kumartaylor-models
The exact original conditional source theorem: assuming the J plus Jw and twice dR enclosures, their sum has the original D_JJw2dR certificate. The original addition proof and all numerical conditions 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_JJw2dR (G_JJw : Good F_JJw D_JJw) (G_tdR : Good F_tdR D_tdR) : Good F_JJw2dR D_JJw2dR := by sorry
Source