The A3X qT product has its stored enclosure
ProvedCKLaneA3X.S_qTa3xgeneral-courtade-kumartaylor-models
The exact original conditional source theorem: assuming Good F_q D_q and Good F_JJw2dR D_JJw2dR, the stored D_qT certificate encloses their product. The complete original analytic composition and every kernel-decided condition 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_third_chain set_option maxHeartbeats 0 set_option maxRecDepth 100000 open CKLaneA3X
Formal statement
theorem CKLaneA3X.S_qT (G_q : Good F_q D_q) (G_JJw2dR : Good F_JJw2dR D_JJw2dR) : Good F_qT D_qT := by sorry
Source