Repository Guide for "Lean-Verified Multi-Agent Discovery of Exact Nonadditive Quantum Codes"

The earlier SSLP background paper cited by the manuscript is stored separately in:

• paper/background-2504.20847/

The numerical search pipeline and certified catalogue for the distance-2 results live in:

• search/distance2_catalogue/

This directory contains:

• the search scripts,
• the independent audit scripts,
• the summary CSV data,
• the full detailed ZIP archives.

At the paper level, this directory is the main repository home for the catalogue and global statistics discussed in the Results section.

The post-processing and analytic-family extraction materials are in:

• search/general_solutions/

This directory includes:

• General_solutions_of_SSLP.tex,
• the affine post-processing scripts,
• the affine verification and summary scripts.

These materials connect the raw distance-2 catalogue to the analytical structures discussed later in the paper.

The reusable Lean library is in:

• SS/

This directory contains the shared formal machinery for:

• subset-sum support conditions,
• diagonal action,
• Z-type Knill-Laflamme constraints,
• distance-3 verification support,
• analytical family formalization.

The example-specific Lean certificates are in:

• Examples/D2/
• Examples/D3/

Roughly:

• Examples/D2/ contains representative distance-2 examples corresponding to the catalogue side of the paper,
• Examples/D3/ contains exact BD16 distance-3 examples and no-go formalizations.

Supporting derivations and explanatory notes are grouped in:

• notes/

In particular:

• notes/distance3_bd16/ contains the BD16 working note,
• notes/lambda_families/ contains the lambda-family and LP derivation notes,
• notes/wolfram_audit/ contains the Wolfram cross-check materials,
• notes/lean_explanations/ contains an explanatory Lean note.

Presentation files are in:

• slides/

Older or superseded materials retained only for provenance are in:

• archive/

The archive/aristotle/ subdirectory specifically contains Aristotle-generated internal artifacts that are not part of the maintained formalization; the maintained no-go results live under Examples/D3/NoGo/.

.
├── paper/
├── search/
├── SS/
├── Examples/
├── notes/
├── slides/
└── archive/

If you want the shortest route from the paper to the repository contents:

1. Use search/distance2_catalogue/ for the distance-2 search and certified catalogue.
2. Use search/general_solutions/ for analytical extraction from catalogue hits.
3. Use SS/ and Examples/ for the Lean formalization.
4. Use notes/ only for supporting derivations and cross-checks.

To check the Lean development:

lake build

On a fresh machine, the first build downloads mathlib into .lake/.