Weak separation and finite-trace coding: independence of infinite fin-intersecting MAD families

We prove that, under s < ap, an almost disjoint family is fin-intersecting exactly when its cardinality is less than s. A uniform finite-trace coding lemma and complementary splitting labels exclude every sufficiently large candidate, including every infinite MAD family. Together with the published Banakh, Machura and Zdomskyy consistency theorem and the positive results of Corral and Rodrigues, this yields relative independence over ZFC of infinite fin-intersecting MAD existence. The article reconstructs the known CH construction, distinguishes FI existence from pseudocompact hyperspace existence, and includes a Cohen-model comparison. Version 1.1 adds a complete Lean relative-independence proof in the original YesMetaZFC first-order Project kernel. The original Con(ZFC) hypothesis is consumed by Henkin model existence, followed by countable elementary reduction and genuine positive and negative generic extensions. Internal CH construction, finite-support Dow preservation, exhaustive set-coded bookkeeping, paired family localization, small-family separation and negative forcing have original ZFC derivation endpoints. The final relative-consistency and nonderivability statements are metatheorems about that same kernel. The formal negative model is sufficient for FI-MAD independence. The full prescribed BMZ cardinal configuration, including continuum = aleph_2, is not claimed for this construction. Hyperspace and Cohen-model consequences retain their cited-input and paper-proof scopes; separate Boolean truth-value adapters remain conditional. The deposit includes an English article PDF, standalone LaTeX source archive and exact checksummed Lean source archive for both pinned packages. The new source snapshot extends public commit 72b0ac8; the completed proof is in the accompanying archive, not in that historical commit. Both packages have passed full builds and transitive axiom audits with only propext, Classical.choice and Quot.sound. Their manifests fix source hashes and dependency revisions. 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.