The A3X d times Jh minus one product has its certificate
ProvedCKLaneA3X.S_dJha3xgeneral-courtade-kumartaylor-models
The exact original conditional source theorem: assuming Good F_d D_d and Good F_Jhm1 D_Jhm1, their product has the original stored D_dJh certificate. The original multiplication 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_third_chain set_option maxHeartbeats 0 set_option maxRecDepth 100000 open CKLaneA3X
Formal statement
theorem CKLaneA3X.S_dJh (G_d : Good F_d D_d) (G_Jhm1 : Good F_Jhm1 D_Jhm1) : Good F_dJh D_dJh := by sorry
Source