The A3X d-q-J product times Si has its stored enclosure
ProvedCKLaneA3X.S_dqJSia3xgeneral-courtade-kumartaylor-models
The exact original conditional source theorem: given Good F_dqJ D_dqJ and Good F_Si D_Si, their product has the stored D_dqJSi certificate. All original hypotheses and kernel-decided 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_fourth_chain set_option maxHeartbeats 0 set_option maxRecDepth 100000 open CKLaneA3X
Formal statement
theorem CKLaneA3X.S_dqJSi (G_dqJ : Good F_dqJ D_dqJ) (G_Si : Good F_Si D_Si) : Good F_dqJSi D_dqJSi := by sorry
Source