The A3X Jh minus one sum has its stored enclosure
ProvedCKLaneA3X.S_Jhm1a3xgeneral-courtade-kumartaylor-models
The exact original conditional source theorem: assuming Good F_Jh D_Jh and Good F_mone D_mone, their sum has the original stored D_Jhm1 certificate. The genuine minus-one enclosure hypothesis is retained, together with all original arithmetic.
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_Jhm1 (G_Jh : Good F_Jh D_Jh) (G_mone : Good F_mone D_mone) : Good F_Jhm1 D_Jhm1 := by sorry
Source