Function ksat_threshold_first_moment_upper 

pub fn ksat_threshold_first_moment_upper(k: u32) -> f64

The first-moment (counting) upper bound on the random k-SAT satisfiability threshold: α*(k) = ln 2 / ln(2ᵏ / (2ᵏ − 1)). Above this clause density the expected number of satisfying assignments E[X] = 2ⁿ(1 − 2⁻ᵏ)^{αn} = (2·(1 − 2⁻ᵏ)^α)ⁿ has per-variable base < 1, so E[X] → 0 and the instance is UNSAT with high probability (Markov) — a rigorous upper bound on the true threshold, exact and closed-form (no sampling). The sequence climbs as 2ᵏ ln 2 − (ln 2)/2, asymptotically doubling per k: 2.41, 5.19, 10.74, 21.83, 44.02, … for k = 2, 3, 4, 5, 6, …. The true thresholds (≈ 1, 4.27, 9.93, 21.1, …) lie below it; the gap → ½ as k → ∞ (the difference between the first-moment bound 2ᵏln2 − ½ln2 and the sharp value 2ᵏln2 − (1+ln2)/2).