Recursive Amplification of Monotone Trades in One-Factorizations

This record contains the preprint, Supporting Information, finite verification package, and Lean 4 formalization for the manuscript “Recursive Amplification of Monotone Trades in One-Factorizations”. The paper studies exact trades between labeled one-factorizations that gain perfect factor pairs while preserving every previously perfect pair. For every integer ℓ ≥ 0 and n = 64·2^ℓ, the construction gives a trade on K_n changing exactly three factor labels and gaining exactly 5n/16 perfect pairs without loss. More generally, two signed-doubling successor operations amplify stable finite seeds while preserving setwise monotonicity and giving exact support and gain recurrences. The finite verification package contains the explicit K16 input, the three certified K64 stable seeds, complete perfect-pair and defect data, independent exact verifiers, expected outputs, integrity checks, and reproduction commands. The Lean 4 development formally verifies the core recursive construction, including the F- and D-successor closure theorems, the three certified K64 stable seeds, arbitrary-word amplification, and the headline three-factor infinite family. The formalization is built with Lean 4.31.0 and a pinned Mathlib revision. It verifies the core recursive results of the manuscript; it is not a claim that every auxiliary appendix and expository statement has been formalized. The finite computational verification and Lean formalization provide complementary evidence: the former independently checks the explicit finite certificates and generated instances, while the latter kernel-checks the core recursive mathematical argument.