A certified lower bound of exponent 0.937 for the 3x+1 problem: the Krasikov–Lagarias systems at depth 25

Let π₁(x) count the integers n ≤ x whose 3x+1 orbit reaches 1. Krasikov and Lagarias (2003) proved π₁(x) ≥ x^0.84 by exhibiting a feasible point of a system of difference inequalities at depth k = 11; the exponent has stood since. We recast their feasibility question as a nonlinear Perron-root condition for an explicit monotone operator whose coefficients are arithmetic functions of the row index — so that no matrix is ever stored — and evaluate it by chunked, index-free GPU kernels to depth k = 25, systems with 2.8 × 10^11 constraints, certifying every level k ≤ 25 in exact rational arithmetic. This yields π₁(x) ≥ 1.591 × 10^-6 · x^0.93756 for all x ≥ 5; both the density constant and the threshold are explicit. The same reformulation settles two questions left open in 2003 — γk is the best exponent the depth-k system can give, and λk is strictly increasing for every k — and sharpens an averaged inequality of Krasikov–Lagarias into an exact identity ρ(F₂⁽ᵏ⁾) = 1/4 + (3/4)·āk/v̄k at the critical parameter λ = 2, so that the Perron root there is determined outright by the equidistribution of a single eigenvector on its fibres. This record contains the paper (PDF), the compact rational certificates and verification logs for k = 2…25, a ready-made k = 17 certificate vector for independent CPU-only verification, and a snapshot of the certification code (development mirror on GitHub).