An improved lower bound for the 3x+1 problem: certificate package (Krasikov-Lagarias exponent 0.9145 at level k=20)

Certificate package for the paper "An improved lower bound for the 3x+1 problem: πa(x) ≥ x0.9145". Krasikov and Lagarias (Acta Arith. 109 (2003) 237–258) proved πa(x) ≥ x0.84 from a feasible solution of the linear program LNTk(λ) at level k=11. This package certifies feasibility at level k=20 with λ = 377/200, giving the exponent log2(377/200) = 0.91456..., via a single explicit positive vector v of 319 = 1,162,261,467 IEEE double-precision entries satisfying Fλ(v) ≥ v row by row with certified rational lower-bound coefficients and an explicit rounding margin. Contents: the 9.3 GB certificate (v_k20_conv.bin), the hardened verifier (kl_verify.cpp, hard-coded interval-certified coefficients, full input and floating-point environment validation), an independent NumPy verifier, the interval certification of the coefficient bounds (kl_exact.py), the search programs, control certificates at k=11 (reproducing the Krasikov–Lagarias level in certified form) and k=12, all verification logs, and a SHA-256 manifest. Verifying the main certificate takes under a minute on a 6-core desktop; see README.txt.