The XAG and AIG gaps at five inputs: ladders, witnesses, logs and checks

Data and code behind the note The XAG and AIG gaps at five inputs: where the XAG gap reaches 2, and where parity stands (doi:10.5281/zenodo.23920692, all versions), which cites this record as [D]. Model: circuits and formulas over XAG (two-input AND and XOR gates) and AIG (two-input AND gates), with free inputs, constants and inverters; opt is the least number of gates of a circuit, tree of a formula, and gap = tree − opt. Contents. The log of the exhaustive enumeration of XAG circuit shapes with at most six gates on five inputs; the exhaustive formula dynamic program for the five separators of opt_XAG 6, rerun when the record was assembled; the log of the disjoint-decomposition tests over the five-input classes; the formula runs on the three decomposable separators; the CSVs of the SAT ladders for 0x1669e996, 0x16686997 and 0x16696997 at five inputs and for 0x16e9 and 0x1669 at four, each UNSAT leg with its drat-trim verdict and formula hash; the witness circuits, among them a 13-gate circuit for 0x1669e996 and the constructions of 17 and 24 gates, with a script that simulates them; the outputs of the one-step gate-elimination bounds and of the checks of Lemma S on small inputs; byte-identical copies of seven files of the earlier record 10.5281/zenodo.23328820, so that the checks run from this record alone; the scripts that produced these files, except the runners of kissat and drat-trim and the script that built the constructions from third-party formulas; and the output of twelve checks run from this package when it was assembled, one of which checks every row of the note's table "Provenance by number" against these files. Since version 1.1, also a Lean project (Lean 4 core) with the proofs of Lemma S and of the formula half of the substitution law, their statement files and configurations for the comparator of the Lean FRO, and the output of a thirteenth check that builds them, prints their axioms, runs the comparator and confirms that it rejects 18 planted changes. What is not included. Formulas and proofs: the formulas of the UNSAT and TIMEOUT legs regenerate from the encoder included here, which one of the checks confirms leg by leg, and the proofs were deleted after checking because of their size. Third-party sources (optimal5, Lflib5, the Boolean Oracle table) are not included. The per-class values at four inputs are in the atlas dataset 10.5281/zenodo.23353481. The proofs of the theorems are in the note; two of them are also in the Lean project. The circuit half of the substitution law is not formalised. Limits. DRAT certifies the formulas, not that they encode the intended question. Solver results without proofs, enumerations and gate-elimination bounds are computation, not certified proofs; the note gives each statement its status. Text and data under CC BY 4.0; code under MIT.