Gleason's Theorem: A Lean 4 Formalization

Initial public release of Gleason's Theorem: A Lean 4 Formalization.

This release formalizes Gleason's representation theorem for nonnegative,
countably additive finite measures on the orthogonal projections of separable
real and complex Hilbert spaces of dimension at least three. The representing
operator is positive, trace class, and unique.

Verification:

• Lean 4.26.0 and Mathlib v4.26.0.
• Complete repository build: 8036 jobs.
• The exact Mathlib-only public statement and proof bridge were accepted by
  Lean Comparator
  at commit 550686caf1d2840f991fb0d751e5d27ea6e75989.
• Reported logical dependencies: propext, Classical.choice, and Quot.sound.
• No sorry, admit, sorryAx, custom axioms, or unsafe declarations.