Replacement, traces and extensions in non-fin-intersecting almost disjoint families

We prove in ZFC that s ≤ a implies the existence of a non-fin-intersecting maximal almost disjoint family of size exactly a, answering Corral–Rodrigues Question 4.10; the additional assumption a < c is unnecessary. Here s is the splitting number, a is the almost disjointness number, and c is the continuum. The construction codes a minimum-size MAD family by predecessor graphs on a triangular countable set. Relative maximal families of sets finite in each column complete these graphs without increasing their cardinality. A fixed splitting assignment then divides the graphs into two pieces, preserving maximality and producing one fin-sequence witnessing failure on every infinite set of indices. We also retain a uniform continuum-size construction for Question 4.6, exact trace realizations, and the cardinal spectrum [s,c] for infinite non-fin-intersecting almost disjoint families. The lower-endpoint equality was independently recovered here but was obtained earlier, unpublished, by Rodrigues, to whom priority for that observation belongs. The common framework is local replacement: maximal refinements preserve the orthogonal class and all admissible extension remainders. It yields local-to-global bounds, a countable-incidence extension theorem, and a trace-splitting criterion. The accompanying fixed Lean 4 development covers the earlier results with their stated hypotheses. The new predecessor completion and the answer to Question 4.10 (Section 8) are supplied here as mathematical proofs and are not yet included in that formalization. Version v3 clarifies that the author manually checked all proofs except the new proof of Question 4.10 in Section 8, and removes references to an unused exploratory route. The mathematical statements and proofs are unchanged from v2. The article discloses AI assistance. The author is unaffiliated, and the research received no specific funding. Files contain the revised article PDF and its standalone LaTeX source. Earlier results only: Lean 4 verification record · Fixed formalization source · Statement-by-statement correspondence