Doubling the A3X dR product preserves its certificate
ProvedCKLaneA3X.S_tdRa3xgeneral-courtade-kumartaylor-models
The exact original conditional source theorem: assuming the dR product enclosure, twice that function has the original stored D_tdR certificate. The source rational scaling by 2 and both numerical conditions are unchanged.
Preamble
import Definitions.Def_A3X_numeric_core import Definitions.Def_A3X_Step027_data_functions import Definitions.Def_A3X_enclosure import Definitions.Def_A3X_Step028_second_chain set_option maxHeartbeats 0 set_option maxRecDepth 100000 open CKLaneA3X
Formal statement
theorem CKLaneA3X.S_tdR (G_dR : Good F_dR D_dR) : Good F_tdR D_tdR := by sorry
Source