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.