Negating the A3X Jw times UsUs product preserves its certificate
ProvedCKLaneA3X.S_mJwUsUsa3xgeneral-courtade-kumartaylor-models
The exact original conditional source theorem: assuming the Jw times UsUs product enclosure, its negative has the original stored certificate D_mJwUsUs. The source scaling proof and both kernel-decided numerical conditions are 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_mJwUsUs (G_JwUsUs : Good F_JwUsUs D_JwUsUs) : Good F_mJwUsUs D_mJwUsUs := by sorry
Source