Main.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Unconditional smooth simple Lebesgue spectrum theorem with real L2 cyclic generator.

theorem OAI.ThreeTorus.simple_lebesgue_spectrum line 17
Source documentation
The unconditional main theorem. The generator and its entire basis are produced by the physical smooth diagonal, then transported by the fixed measure-preserving coordinate equivalence.
Distinct definitions of this name: ComparatorChallenges/ThreeTorus.lean:82 (same statement text; different proof or body). Qualify references as OAI.ThreeTorus.simple_lebesgue_spectrum@path.
```
theorem simple_lebesgue_spectrum : MainConclusion := by
…
```
Mentions: OAI.ThreeTorus.MainConclusion