# Limiting random SAT thresholds, sharp variance and computability

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [A Limiting Satisfiability Threshold for Every Fixed Clause Size](../../preprints/A-Limiting-Satisfiability-Threshold-for-Every-Fixed-Clause-Size-September-25-2026/article.pdf)
- [Variance of the Random $k$-SAT Hitting Time](../../preprints/Variance-of-the-Random-k-SAT-Hitting-Time-September-27-2026/article.pdf)
- [Computing the Random 3-SAT Threshold](../../preprints/Computing-the-Random-3-SAT-Threshold-September-27-2026/article.pdf)

## Scope

The random $k$-SAT threshold problem asks whether satisfiability changes at one limiting clause density. The formalization proves that every fixed integer $k\ge3$ has a finite positive threshold $\alpha_k$: for every fixed density $c<\alpha_k$, the satisfiability probability tends to one as the number of variables grows, while for every $c>\alpha_k$ it tends to zero. Clauses use distinct variables with independent uniform signs and are sampled independently with replacement. The statement makes no assertion at the threshold itself.

Let $H_n$ be the first unsatisfiable prefix length in random $k$-SAT with independent uniformly signed clauses on $k$ distinct variables, sampled with replacement. The formalization proves $\mathrm{Var}(H_n)=\Theta_k(n)$ for every fixed $k\ge4$. For $k=3$, it proves a positive linear lower bound and an $O(n\log n)$ upper bound. The same upper bounds hold after clipping at any fixed positive multiple of $n$, and linear lower bounds hold for sufficiently high clipping levels.

The linked supplements prove sharpness of the separate survival-lifetime and clause-replacement estimates used in the argument. They do not show that the logarithmic factor in the $k=3$ variance bound is necessary.

The formalization proves that the limiting threshold $\alpha$ for uniform random $3$-SAT is a computable positive real. Satisfiability tends to one at every fixed density below $\alpha$ and to zero at every fixed density above it. One deterministic machine produces a rational number $q_r$ for every requested precision $r$ with $|q_r-\alpha|\le2^{-r}$. No computable rate of finite-size convergence is assumed in the statement.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Limiting satisfiability threshold for every fixed $k\ge3$ | [FixedClauseThreshold.lean](../ComparatorChallenges/FixedClauseThreshold.lean) |
| Sharpness of random $k$-SAT lifetime and replacement bounds | [SATSharpness.lean](../ComparatorChallenges/SATSharpness.lean) |
| Variance bounds for the random $k$-SAT hitting time | [SATVariance.lean](../ComparatorChallenges/SATVariance.lean) |
| Computability of the random $3$-SAT threshold | [SATComputability.lean](../ComparatorChallenges/SATComputability.lean) |