Sources, scope & reproducibility
The Lean verification
The development formalizes both implications of the real BFPP characterization and the transfinite construction of the domain and maps, with mathlib as its only declared library dependency.
What was checked
The recorded verification compiled all 73 mathematical modules, the aggregate import, and the audit file with the pinned Lean executable and an existing compiled mathlib checkout. The audit passed for 988 declarations in namespace BFPP, including generated declarations.
The allowlist is exactly propext, Classical.choice, and Quot.sound. The audit rejects all other axioms, including sorryAx. The recorded source scan found no sorry, admit, custom axiom, or unsafe declarations.
The full direct-compilation verification completed on 14 September 2026 (UTC). The manuscript’s later editorial revisions preserved the Lean sources. This site presents that existing verification record; preparing the website did not constitute a new Lean build.
A cached Lake configuration check and an offline import smoke check were also completed in an isolated probe. A fresh online lake update followed by a conventional clean lake build was not performed. See the full record for the environment and limits of these checks.
From the paper to the modules
These entry points follow the mathematical construction. Each link opens the complete source file, with stable line anchors. The full correspondence map lists further declarations and proof adaptations.
Some formal proofs take a different route to the same conclusion. For example, centered synthesis is proved contractive directly from positivity; the measure representation and convex-integral calculation are also proved separately. The extremally disconnected implication is developed internally rather than assumed as an external theorem.
Five modules retain the former appendix as supplementary material. They remain in the full development, but are outside the import closures of MainTransfinite and Characterization. They are marked in the source index.
Build the project independently
Extract the Lean project archive. With Lean’s toolchain manager installed, open a terminal in the extracted BFPPFormalization directory. The included toolchain and Lake configuration pin the versions.
lake update
lake exe cache get
lake buildThese are the conventional reproduction commands; the verification reported above used direct compilation against an existing cache. Both the aggregate library and audit are default build targets.
The archive also includes scripts/build-local.ps1 and an offline smoke-check script for Windows. Supply your own -MathlibRoot and -LeanExe paths; their saved defaults belong to the original verification environment. Consult the project README before using them.
Downloads and evidence
- Complete Lean projectSource, pinned configuration, audit, scripts and evidence. Compiled caches are excluded.
- Paper-to-Lean correspondenceMapping of mathematical results and explanations of proof adaptations.
- Verification recordScope, environment, manuscript revisions, axiom checks and build limitations.
- Compilation and audit logThe recorded build covers 75 distinct Lean source files.
- Project source checksumsSHA-256 manifest for source, configuration, scripts, documentation and evidence.
Authorship and acknowledgments
The paper is by Cleon S. Barroso. The Lean development was prepared with OpenAI Codex under the author’s direction. The author is responsible for the mathematical statements and their correspondence with the manuscript.
This companion’s organization is inspired by the Complemented subspaces project website. The site uses its own text, styles and static source browser. Its pages, code, downloads and fonts are available locally; no external service is needed to read them.