Axiom audit for the orthonormalization theorem

What the vendored development proves outright, and what it does not, is the thing to know before citing any of it, and the distinction is invisible in the source: every statement reads like a theorem. This file makes it mechanical. It fails to build if one of the unconditional results acquires an axiom, and equally if one of the four open targets is closed upstream without this repository noticing — in which case the blueprint's thm:orthonormalization and rem:orthonormalization-scope are what need updating.

Unconditional, in order of generality: every von Neumann algebra on a finite-dimensional space; B(H) for arbitrary H; and II₁ factors whose trace and state are of trace-class form. The general case is povm_orthogonalization_of_structure, which is a theorem about the implication only: its hypothesis MvNStructureTheory bundles eight facts of von Neumann algebra structure theory that Mathlib does not have, and no term of that type is constructed anywhere.

Unconditional

Conditional on the structure-theory interface

The implication is proved; its hypothesis is not.

The open targets

Upstream's signed statements: the unconditional general forms, stated so that each tier can be compared against them, and sorry until the interface above is discharged. Nothing proved in the development depends on them.