Must every permutation of $\mathbb{N}$ contain a monotone 4-term arithmetic progression? (Erdős #196)

Must every permutation of $\mathbb{N}$ contain a monotone 4-term arithmetic progression? In other words, given a permutation $x$ of $\mathbb{N}$ (a sequence $x_1,x_2,x_3,\ldots$ listing every positive integer exactly once), must there be indices with either $i<j<k<l$ or $i>j>k>l$ such that $x_i,x_j,x_k,x_l$ form an arithmetic progression (in that order)?

Acceptance. FULLY RESOLVES: either (a) a proof that every permutation of $\mathbb{N}$ contains a monotone 4-term arithmetic progression — machine-checkable (Lean/Coq) preferred, and the formal-conjectures Lean statement can host it, else a complete written proof; or (b) an explicit permutation of $\mathbb{N}$ (finitely described: a formula, recursion, or self-similar scheme) together with a correctness proof that it contains no monotone 4-term AP. A computation alone cannot close this (the object is infinite); any construction must include the avoidance proof for the whole infinite permutation. ADVANCES: a proof of the forcing statement for a natural restricted class of permutations (e.g. permutations with bounded displacement, or finitely piecewise-monotone permutations); a rigorous no-go theorem ruling out a named family of candidate constructions; a quantitative finite version with certificate (e.g. exact SAT-verified thresholds for how long a finite sequence of distinct integers within a structured class can avoid monotone 4-term APs, with exhaustiveness certificate); or a reduction of the problem to a finite or structured statement. Deliver the proof file, or the construction plus avoidance proof, or the search code with certificates.