Prove2Me

The A3X summed numerator has its stored enclosure

Proved
CKLaneA3X.S_auN

by marwahaha · Sep 25, 2026 · Mathlib 0df444a (Lean v4.33.1)

a3xgeneral-courtade-kumartaylor-models

The exact original conditional source theorem: given Good F_qT D_qT and Good F_dJh D_dJh, their sum has the stored D_auN certificate. Every source assumption and arithmetic proof is 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_auN (G_qT : Good F_qT D_qT) (G_dJh : Good F_dJh D_dJh) : Good F_auN D_auN := by sorry
Source
https://github.com/dpwoodru/general-courtade-kumar-lean/blob/04b6fc3f75b10c3c43702a883ddf888b0608a9a0/browse/CKLaneA3X/Step028.lean#L47

View graph