An F-sigma ideal without web closure or uncountable strongly unbounded sets

We construct a proper F-sigma ideal on the countable grid for which web closure fails while every strongly unbounded subfamily is countable. This gives a negative answer to Conjecture 4.14 of Hernandez-Hernandez, Hrusak and Rivas-Gonzalez, The bounded topology. The preprint includes a complete elementary proof and a companion Lean 4 formalization. The general thinning bound is 4C and the row-finite bound is 3C. AI-assisted work under the author’s direction. OpenAI Codex assisted with exploration, formalization, auditing and drafting. Kernel verification is distinguished from independent peer review and historical-priority certification. A limited literature search did not identify an earlier resolution; no exhaustive priority claim is made. Files: English preprint PDF and LaTeX/Lean source archive with pinned dependencies and verification records. This revision adds acknowledgements to the Rethlas development team (Haocheng Ju, Jiedong Jiang, Shurui Liu, Guoxiong Gao, Yuefeng Wang, Zeming Sun, Leheng Chen and Bin Wu; project leaders Liang Xiao and Bin Dong). See https://github.com/frenzymath/Rethlas and https://web.stanford.edu/~srliu/homepage/blog/rethlas-guide/ . Mathematical statements, proofs and formalization scope are unchanged. Version 2.0, 30 September 2026. Rethlas was used during earlier exploratory stages. The final counterexample and Lean formalization were developed in subsequent Codex-assisted work. The acknowledgement does not attribute discovery of the final construction or kernel verification to Rethlas.