Formalize Dade's conjecture (character counts in p-blocks)

### What is the conjecture

Let $G$ be a finite group, $p$ a prime, and $B$ a $p$-block of $G$ (in the sense of Brauer). The $p$-block $B$ is characterized by a defect group $D$ up to conjugacy.

Dade's conjecture asserts that the number of ordinary irreducible characters of $B$ with a given height (relative to the defect group $D$) equals an alternating sum of the numbers of ordinary irreducible characters of $p$-blocks of certain $p$-local subgroups, taken with signs depending on the structure of these subgroups.

More precisely, for each height $h \geq 0$, Dade's ordinary conjecture predicts a formula:
$$k_h(B) = \sum_{H \leq G} (-1)^{|G|/|H| - 1} k_h(b_H)$$
where the sum is over a specific family of subgroups $H$ of $G$, $k_h(B)$ denotes the number of irreducible characters of $B$ with height $h$, and $b_H$ are related blocks of these subgroups.

Dade formulated several versions of this conjecture, including the ordinary conjecture (for heights of ordinary characters) and the projective conjecture (for heights of Brauer characters).

(This description may contain subtle errors especially on more complex problems; for exact details, refer to the sources.)

**Sources:**
- https://en.wikipedia.org/wiki/Dade_conjecture, https://www.cambridge.org/core/journals/canadian-journal-of-mathematics/article/dades-conjecture-for-chevalley-groups-g2q-in-non-defining-characteristics/EB2887E7CBA74344D1B1080D9167A690, https://openaccess.city.ac.uk/id/eprint/20446/7/Kessar-Linckelmann2018_Article_DadeSOrdinaryConjectureImplies.pdf, https://www.cambridge.org/core/journals/lms-journal-of-computation-and-mathematics/article/alperin-weight-conjecture-and-dades-conjecture-for-the-simple-group-fi24/148DA911F2161A759217812D83E87F95

### Prerequisites needed

**Formalizability Rating:** 3/5 (0 is best) (as of 2026-03-14)

Building blocks (from Mathlib/FormalConjectures):
- Finite group theory (`Fintype`, `Group`, `IsCyclic`)
- Character theory (group homomorphisms to multiplicative groups of fields, irreducibility)
- Basic prime and modular arithmetic

Missing pieces (require new development):
- Brauer blocks and block decompositions of the group algebra
- Defect groups of blocks and conjugacy classifications
- Character heights relative to defect groups
- The alternating sum formula with appropriate p-local subgroups and signs

### [AMS categories](https://github.com/google-deepmind/formal-conjectures/labels?q=ams-)

* ams-00

### Choose either option

- [ ] I plan on adding this conjecture to the repository
- [x] This issue is up for grabs: I would like to see this conjecture added by somebody else

---
This issue was generated by an AI agent and reviewed by me.

If you have feedback on mistakes / hallucinations, feel free to just write it in the issue. See more information here: [link](https://leanprover.zulipchat.com/#narrow/channel/524981-Formal-conjectures/topic/Custom.20Agent.20for.20Issue.20Generation/with/569221879)