The A3X Jw times UsUs product has its stored enclosure
ProvedCKLaneA3X.S_JwUsUsa3xgeneral-courtade-kumartaylor-models
The exact original conditional source theorem: assuming Good F_Jw D_Jw and Good F_UsUs D_UsUs, the stored D_JwUsUs certificate encloses F_JwUsUs. The original analytic composition and all seven kernel-decided numerical conditions are preserved unchanged.
Preamble
import Definitions.Def_A3X_numeric_core import Definitions.Def_A3X_Step026_data import Definitions.Def_A3X_Step027_data_functions import Definitions.Def_A3X_enclosure import Definitions.Def_A3X_Step028_first_chain set_option maxHeartbeats 0 set_option maxRecDepth 100000 open CKLaneA3X
Formal statement
theorem CKLaneA3X.S_JwUsUs (G_Jw : Good F_Jw D_Jw) (G_UsUs : Good F_UsUs D_UsUs) : Good F_JwUsUs D_JwUsUs := by sorry
Source