Open formalization work

These theorem statements are preserved as structured TODO comments in Statlib rather than compiled declarations. Each item links to its exact source location and is a concrete starting point for contributors.