New machine-checked certificate: collar re-summation and indicial parity.
A new sorry-free module GIFT/Foundations/CollarResummationCertificate.lean (namespace GIFT.Foundations.CollarResummation) formalizes two self-contained analytic identities used in the weighted estimates for the collar region of the K3-fibered G₂ metric:
- Absolute re-summation
∑_{k≥0} |C(3/2,k)| = 3(collar_resummation,tsum_abs_C32) — the collar/bulk erosion factor — proved by an elementary telescoping route∑_{k=0}^n (-1)^k C(3/2,k) = (-1)^n C(1/2,n)combined with|C(1/2,n)| ≤ 1/(2n-1), avoiding Abel's theorem. - Alternating value
∑_{k≥0} (-1)^k C(3/2,k) = 0(alternating_binomial_at_neg_one) without any boundary-limit theorem. - Indicial parity
K_ind(-1) = K_ind(+1) = 4/3(K_ind_neg_one_eq).
Axioms: [propext, Classical.choice, Quot.sound] only (no new GIFT axioms). Blueprint section + sync check pass. Full build green (8394 jobs). No change to any prediction or the published axiom count.