Sendov's Conjecture
Shared via MathBB
Cover page
Introduction
Normalization and the counterexample structure
Four identities
The boundary case: Rubinstein's theorem
Low degrees: n ≤ 5
The polar channel
Three lemmas: Maclaurin, defect, and the J-sum
The origin channel
Combining the channels
The master inequality and conclusion
State of the Lean formalization
Interactive: Sendov's theorem