Largest $k$ such that every permutation of $\mathbb{Z}$ contains a monotone $k$-term AP (Erdős #195)

Regard a permutation of $\mathbb{Z}$ as a doubly infinite sequence listing every integer exactly once. Say the permutation contains a monotone $k$-term arithmetic progression if there are integers $x_1<x_2<\cdots<x_k$ in arithmetic progression whose positions in the sequence are monotone (all increasing or all decreasing). What is the largest $k$ such that in any permutation of $\mathbb{Z}$ there must exist a monotone $k$-term arithmetic progression $x_1<\cdots<x_k$?

Acceptance. FULLY RESOLVES: an exact determination of $k$ — i.e. (a) a proof that every permutation of $\mathbb{Z}$ contains a monotone $k$-term AP, and (b) an explicit permutation of $\mathbb{Z}$ (finitely described, e.g. periodic or recursively constructed, with proof of correctness) containing no monotone $(k+1)$-term AP, for the same value of $k$. Machine-checkable (Lean/Coq) proof preferred, else a complete written proof; note the existing Lean statement in formal-conjectures can host a formalization. ADVANCES: either half separately — a proof that every permutation of $\mathbb{Z}$ contains a monotone 3-term AP (or a construction avoiding one); or a construction avoiding monotone 4-term APs, strictly improving the best upper bound stated in the background; or a computer-assisted no-go theorem showing all permutations of a specified structured class must contain a monotone 4-term AP. Constructions must come with a verifiable description and a proof (or machine-checkable certificate for the finite core plus an extension argument). Deliver the proof file and/or the construction with verification code.