A Multi-Backend Verified Control Theorem Motivated by the Erdős–Turán Conjecture on Arithmetic Progressions

This record contains the public reproducibility package for the manuscript “A Multi-Backend Verified Control Theorem for Global Smoothed Projection Blindness.” The motivating open problem is the Erdős conjecture on arithmetic progressions, also known in this context as the Erdős–Turán reciprocal-sum problem: whether a subset of the natural numbers whose reciprocal sum diverges must contain arbitrarily long arithmetic progressions. This package does not claim to solve that conjecture. It contains a formally verified control theorem showing that a global smoothed projection collapses point distinction and is blind to boundary fields, exception fields, and previous-anchor fields. The archive includes Markdown and LaTeX manuscript sources, a compiled PDF, Coq, Lean, Isabelle/HOL, Agda, Z3, and CVC5 artifacts, audit logs, SHA-256 manifests, and a referee hash-checking script. The claim is limited to the included formal artifacts: GLOBAL_ERDOS_CLAIM=falseCONTROL_MODEL_ONLY=true