On the Corral–Rodrigues question: independence of infinite fin-intersecting MAD families

We answer Corral and Rodrigues's Question 3.7 (Filomat 38 (2024), 2563–2578): assuming ZFC is consistent, the existence of an infinite fin-intersecting maximal almost disjoint family is independent of ZFC. Thus ZFC proves neither existence nor nonexistence under this consistency assumption. The new obstruction is that, under s < ap, every almost disjoint family of size at least s fails to be fin-intersecting. In particular, no infinite FI MAD family exists. Together with the known small-family bound this gives an exact cardinal cutoff. The proof uses weak separation and finite-trace coding to realize prescribed subsets of omega modulo finite error as traces of one sequence of disjoint nonempty finite blocks. A consistency theorem of Banakh, Machura and Zdomskyy supplies the negative model, while the positive results of Corral and Rodrigues, including the CH case, supply the other direction. The cited negative model nevertheless contains a MAD family with pseudocompact Vietoris hyperspace. Version 1.2 revises the title, abstract, introduction and selected theorem statements to foreground the answer to the Corral–Rodrigues question. It makes the obstruction quantifiers and verification scopes explicit, clarifies model references and attributions, and distinguishes nonprovability of existence from provable nonexistence. The core arbitrary-label finite-trace coding section is unchanged. No Lean source code is changed in this version. The companion Lean development verifies the combinatorial results on standard sets and gives a relative-independence metatheorem for the original first-order ZFC derivation relation. Internal constructions and forcing assertions have object-theory derivation endpoints; the final relative-consistency and nonderivability statements are metatheorems about that kernel. The formal negative construction does not claim the full BMZ cardinal configuration. Hyperspace and Cohen-model consequences retain their cited-input and paper-proof scopes. Files: revised 13-page article PDF; standalone LaTeX source archive; the unchanged, checksummed FI_MAD_formalization_v1.1.zip from version 1.1. The formal archive retains its original version label, dependency pins and verification evidence. The main package was rechecked during this exposition revision; the isolated model package was not rerun because its sources were unchanged. AI disclosure: generative AI, including GPT-6 Astra and OpenAI Codex, assisted mathematical arguments, formalization, checking and English drafting. The author supplied the problem and coordinated the work. Neither these checks nor kernel verification constitutes independent expert review of the entire manuscript. The author is unaffiliated and received no specific funding.