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

We give a single ZFC construction of a non-fin-intersecting maximal almost disjoint family of size continuum, addressing Corral–Rodrigues Question 4.6 without a division into cardinal cases. The construction completes all binary-tree branches to a maximal almost disjoint family and replaces each branch by its infinite bit-defined pieces; the completion uses a fixed well-order parameter. Its mechanism is local replacement: maximal refinements preserve the orthogonal class and exactly the possible extension remainders. We develop this mechanism into local-to-global bounds for extension costs, an extension theorem at the almost disjointness number under a countable-incidence hypothesis, and a cardinality-preserving trace-splitting criterion. We also obtain exact trace realizations and the full cardinal spectrum from the splitting number to the continuum for infinite non-fin-intersecting almost disjoint families. The minimum-size equality at the lower endpoint was independently recovered here but was obtained earlier, unpublished, by Rodrigues; priority for that observation belongs to him, and it is included as background for the subsequent constructions. The size-control problem in Question 4.10 remains unresolved. An accompanying Lean 4 development verifies the mathematical results, with the conditional hypotheses retained explicitly. This preprint includes disclosure of AI assistance and attribution of earlier work. The author is unaffiliated, and the research received no specific funding. Files comprise the article PDF and its complete LaTeX source. Lean 4 verification record · Fixed formalization source · Statement-by-statement correspondence