we-solve (beta)

Math-2903 · mathematics · Probability

Linear hitting-time variance for random clause size at least four

Status OpenLLM status Open unverified

Statement

Definitions and mathematical statement

Statement recorded in the supplied source.
For each fixed $k\geq 4$, let $H_n$ be the first unsatisfiable time under independent proper uniformly signed k-clauses sampled with replacement. Is $Var(H_n)=Theta_k(n)$? Ask also $Var(min(H_n,floor(Bn)))=Theta_{k,B}(n)$ for $B>\log (2)/(-\log (1-2^{-k}))$.

Short English statement

For each fixed $k\geq 4$, let $H_n$ be the first unsatisfiable time under independent proper uniformly signed k-clauses sampled with replacement. Is $Var(H_n)=Theta_k(n)$? Ask also $Var(min(H_n,floor(Bn)))=Theta_{k,B}(n)$ for $B>\log (2)/(-\log (1-2^{-k}))$.

Sources

Statement licence: CC-BY-4.0 · Source file

Contributions 1

Math-2903-A1 · Literature report · LLM-generated · unknown ·

OpenAI claim summary for Math-2903

The proposed first-unsatisfiable-prefix variance is $\Theta(n)$ for $k\geq4$, and between order $n$ and order $n\log n$ for $k=3$. The question retains these same parameters and conventions. Within these assumptions, this is a claimed affirmative answer to the stated question.

Linear hitting-time variance for random clause size at least four

OpenAI's claim

OpenAI presents a proof in the selected manuscript. The proposed first-unsatisfiable-prefix variance is $\Theta(n)$ for $k\geq4$, and between order $n$ and order $n\log n$ for $k=3$.

Mathematical statement of the claimed result

Result 1.
Sample independent clauses, with replacement, uniformly among the $2^k\binom nk$ signed clauses on $k$ distinct variables. Write $F_m=\bigwedge_{j=1}^mC_j$ and $H_n=\min\{m\ge1:F_m\text{ is unsatisfiable}\}$. For each fixed $k\ge3$, put $\ell_3(n)=\log(en)$, $\ell_k(n)=1$ for $k\ge4$, and $U_k=\log2/[-\log(1-2^{-k})]$. Constants depending only on $k$ satisfy \[ \operatorname{Var}(H_n)\le C_kn\ell_k(n)\quad(n\ge k),\qquad \operatorname{Var}(H_n)\ge c_kn\quad(n\text{ sufficiently large}). \] For fixed $B>0$, $T_{n,B}=\min(H_n,\lfloor Bn\rfloor)$ obeys $\operatorname{Var}(T_{n,B})\le C_{k,B}n\ell_k(n)$. Its matching lower bound $c_kn$ applies when $B>U_k$.

Outline of the argument

Assignment-set survival estimates and clause omission express deletion delays through independent root tests. Occupation and collision moments bound squared delays and hence variance, with matching linear lower bounds from transition-width estimates; clipping preserves the upper bounds.

Formal verification

For family 235, the selected entries establish threshold existence, threshold computability, linear variance for $k\geq4$, and the earlier $O(n\log n)$ bound for $k=3$. The later linear three-clause variance improvement is not selected. The listed Comparator files are FixedClauseThreshold.lean, SATComputability.lean, SATSharpness.lean, SATVariance.lean. The inventory does not supply a named declaration for these Comparator entries. This site has not executed the Lean code. The scope descriptions do not certify the remaining manuscript arguments.

Status caveat

OpenAI attributes these manuscripts to work by an internal model. Its release cautions that arguments without formalization can contain mistakes. This catalogue has not independently checked the proofs; the labels report the mathematical claims attributed to OpenAI.

Sources

Go to contribution →