The A3X d times R product has its stored enclosure
ProvedCKLaneA3X.S_dRa3xgeneral-courtade-kumartaylor-models
The exact original conditional source theorem: assuming Good F_d D_d and Good F_R D_R, the stored D_dR certificate encloses their product. The original analytic composition and seven kernel-decided conditions are unchanged.
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_dR (G_d : Good F_d D_d) (G_R : Good F_R D_R) : Good F_dR D_dR := by sorry
Source