Lean project
The Lean 4 project that proves the formalised statements of the paper; the formalisation page maps each statement to its declarations and says how to check the project.
Download: everything needed for checking (the Lean project and the ancillary files, with instructions) or the Lean project alone.
Project files
Modules
Each module page shows the source with the declarations that the paper links to. The table lists the top-level modules; the proofs of the RSC reduction are in the modules under MaxLeafFormal/RSC/, which these import, and the RSC data modules are generated (ancillary/README.md).
Scripts
scripts/ holds the axiom checks of each part and the programs that wrote the data modules from the ancillary certificates: AxiomsAntinorm3.lean, AxiomsAntinorm8.lean, AxiomsBudget.lean, AxiomsCCGibbs.lean, AxiomsCCT.lean, AxiomsCDS.lean, AxiomsCertificates.lean, AxiomsDSTGraph.lean, AxiomsLobsterGraph.lean, AxiomsMLS.lean, AxiomsPDGraph.lean, AxiomsRSCCert.lean, AxiomsRSCCheck.lean, AxiomsRSCCheckExtras.lean, AxiomsRSCCompose.lean, AxiomsRSCFinal.lean, AxiomsRSCFinalExtras.lean, AxiomsRSCHeadline.lean, AxiomsRSCSteiner.lean, AxiomsRSCTree.lean, AxiomsRSRateAB.lean, RSCReductionChecks.lean, StatementsDSTGraph.lean, StatementsDstRec.lean, StatementsPDGraph.lean, StatementsRSC.lean, StatementsRSCExtras.lean, StatementsRSRate.lean, StatementsRSRateAB.lean, export_cc_cert.py, export_dst_cert.py, export_lobster_cells.py, export_rs_cover.py, export_rsc_cert.py, export_rsc_extras.py, export_rstheta_cert.py, rsc_data_audit.py, rsc_extras_audit.py. The docstring of export_rsc_cert.py predates the switch of the RSC data check to native_decide; the file is unchanged because the generated data modules pin its checksum.