KerrFormalization

KerrFormalization expresses pieces of black-hole geometry in Lean so the definitions, assumptions, and proof boundary can be inspected directly.

The checked core includes an explicit proof that the outer Kerr horizon radius is a root of the Kerr Delta function when the discriminant is nonnegative.

In the Kerr Problems database, I also completed the primary-literature audit that closed K-608 as solved in the literature and advanced K-505 from open to partial without overstating the remaining gap.