The main theorem from the two remaining analytic inputs

All structural ingredients are proved. The only hypotheses of the final deduction are the relative expansion statement and the balanced-combination statement. Thresholds are selected before the decomposition, with the final prime bound taken over its uniformly bounded node radii.

theorem EGZ.eventualCeilZeroSum_of_expansion_balanced (hExpansion : Expansion.RelativeExpansionStatement) (hBalanced : BalancedCombinationLemma) (d : ℕ) (hd : 0 < d) : EventualCeilZeroSum d

The finite target follows from expansion and balanced combinations, using the proved flag decomposition, Helly bound, and centerpoint theorem.

theorem EGZ.mainUpperBound_of_expansion_balanced (hExpansion : Expansion.RelativeExpansionStatement) (hBalanced : BalancedCombinationLemma) (d : ℕ) (hd : 0 < d) : MainUpperBound d

The upper estimate, with exactly the two unproved paper ingredients as explicit hypotheses.

theorem EGZ.mainAsymptotic_of_expansion_balanced (hExpansion : Expansion.RelativeExpansionStatement) (hBalanced : BalancedCombinationLemma) (d : ℕ) (hd : 0 < d) : MainAsymptotic d

Conditional assembly of Theorem 1.2. No additional geometric, rounding, coordinate-change, or uniformity hypotheses are required.