Recorded, Not Proved Here

Results this library states but does not prove, because the track that would prove them is not yet developed. Every item in this category is marked ‡ not proved here, and so is every result elsewhere that depends on one. They are included so the library can refer to them honestly, with a citation, instead of leaving a silent gap. Nothing recorded here may be used as a step in a proof.

These are the subjects the rule has held back. Lebesgue measure and the Lebesgue integral, with the convergence theorems, the sharp fundamental theorem of calculus for absolutely continuous functions, Egorov, Lusin, the Lebesgue spaces and the non-measurable sets. Functional analysis, with Hahn-Banach, the open mapping and closed graph theorems, Banach-Alaoglu, the Riesz representation theorems, weak topologies, spectral theory and the counterexamples that make its definitions necessary. Algebraic topology, with covering spaces, the general Jordan curve theorem, invariance of domain and homology. Set theory beyond choice, with forcing, the independence of the continuum hypothesis, Solovay's model and the consistency results that fix the choice strength of theorems proved elsewhere. Open problems are recorded separately, and no track will discharge them.

What rests on this category is every result across the library whose own proof reaches a statement recorded here, which is why an entry is aliased and retired rather than deleted. Each is replaced by a real proof as the track that owns its subject is built, and the measure theory and functional analysis scaffolds have already disposed of their entries row by row.