Confluence of a Saturation Procedure for Rooted Phylogenetic Triples

Ebert, Lindeberg, and Hellmuth introduced a saturation procedure for required and forbidden rooted triples and asked whether its returned relation depends on the legal choices made during a run. We prove that it does not: arbitrary completed runs, even with different lengths and different choices, return literally the same final relation. The proof isolates a deactivation lemma yielding a strong diamond property for the exact saturation transition system. The accompanying Lean 4 development formalizes the definitions and confluence theorem. It also formalizes and proves all four clauses of the source paper’s Lemma 5.12, including its realizability statement through a canonical quotient-poset DAG construction. The proof-and-replay archive contains the manuscript and its LaTeX source, the Lean formalization, theorem-interface and axiom checks, an independently written Python semantics, bounded cross-checks and mutation tests, source-version records, and a SHA-256 manifest. From a clean extraction, run: python verify.py The formal declarations use only the standard axioms propext, Classical.choice, and Quot.sound. The confluence theorem itself requires neither finiteness nor non-emptiness of the leaf type; the realizability portion of Lemma 5.12 uses the source paper’s finite, non-empty leaf-set assumptions. This work was conducted within the conjecture-prover and autoformalization project of the Stanford Lean Club, led by Donald D. Poindexter, Jr. OpenAI GPT-5.6 Sol Ultra assisted with problem analysis, proof discovery, and proof development. Claude Code using Claude Opus 5 constructed and iteratively hardened the Lean formalization under adversarial audit. Version 0.1 file correction, 5 August 2026: the deposited files were replaced solely to correct the manuscript’s typesetting and PDF metadata. The mathematical statements, proofs, Lean sources, and claimed results are unchanged. Files and SHA-256 checksums: phylogenetic_saturation_confluence_v0.1.pdfa20c1cb46c4f59788c2132d7c16e81183ead944f01bda5daacc2dfd9c724b032 phylogenetic_saturation_confluence_v0.1_proof_replay.zip3b82c21199c5c048c84b7451ae992cf9c4b3585770f06d2220446d6e9c9c125b DOI: https://doi.org/10.5281/zenodo.21802298 The manuscript and documentation are licensed under CC BY 4.0. Lean and Python source code are licensed under the MIT License.