A conditional analytic framework for rank-one branched Kovalev-Lefschetz adiabatic limits dataset

Conditional analytic framework for a special case of Donaldson's Conjecture 1 (2017) on adiabatic limits of coassociative Kovalev-Lefschetz fibrations with K3 fibres. For branched rank-one admissible data (fibrations whose monodromy on H^2(K3;R) acts through a single root direction, whose period section is collar-affine, and whose discriminant is a geometrically split unlink), the paper obtains: (i) an unconditional weighted edge Fredholm theory of the maximal-submanifold Jacobi operator in the Pacard-Mazzeo beta=-1 window, with a cokernel-inversion certificate; (ii) a conditional lifting scheme producing closed positive 3-forms of G_2-type in the class [phi_0]+R[B] for every R above a finite threshold, under three quantitative admissibility conditions; (iii) a conditional torsion-free upgrade under an anisotropic three-scale perturbation hypothesis (J). For a normalised datum D_0 from a K_7 -> S^3 construction with N=77 branch components, the source-side discharge constants are certified with structural provenance and the threshold R_0(D_0) <= 4.9 x 10^3 is enclosed by outward-rounded interval arithmetic. The main paper (68 pp) is accompanied by a supplement (25 pp) collecting the edge-calculus toolbox, Lean 4 verification statements, K_7 -> S^3 construction with Betti-number computation, interval-arithmetic enclosures, structural derivations of the D_0 constants, and numerical verification of the discharge conditions. A structured dataset (constants_D0.json) and four Python + mpmath.iv reproducibility scripts (interval-arithmetic verification of the L1.6 recollement K_Sch <= 16/3 and the L2 assembled adiabatic-reconstruction contraction) accompany the paper. The Lean 4 formal verification of the combinatorial identity sum |C(3/2,k)| = 3 used in Section 6.4 lives in the public repository gift-framework/core (tag v3.4.29). Part of the Arithmon research programme (arithmon.com).