# Relative bicentralizers and modular spectral recovery

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [Bounded recovery for modular spectral averages](../../preprints/Bounded-recovery-for-modular-spectral-averages-September-23-2026/Bounded-recovery-for-modular-spectral-averages-September-23-2026.pdf)

## Scope

For a faithful normal state with scalar centralizer in the stated standard-space representation, the formalized result converts positive modular spectral averages into uniformly bounded algebra elements. Given unit vectors in shrinking spectral bands around a real number $s$ and a positive limiting symmetric average for a bounded operator $T$, it finds a subsequence of bounded algebra elements whose images under $T$ stay uniformly nonzero and whose spectral bands have four times the original widths. The absolute bicentralizer conjecture is not included.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Bounded recovery from modular spectral averages | [BoundedRecovery.lean](../ComparatorChallenges/BoundedRecovery.lean) |