Norton's Generalized Moonshine

### What is the conjecture

Norton's Generalized Moonshine conjecture extends the Monstrous Moonshine correspondence to pairs of commuting Monster group elements. It asserts that for each commuting pair $(g, h)$ in the Monster group $M$, there exists a holomorphic function $Z(g, h, \tau)$ defined on the upper half-plane satisfying the following properties:

1. **Conjugacy Invariance**: $Z(g, h, \tau)$ is invariant under simultaneous conjugation of $g$ and $h$ in $M$ (up to scalar factors).

2. **Modular Type**: Each function $Z(g, h, \tau)$ is either a genus zero modular function (a Hauptmodul) or a constant.

3. **Representation Characters**: For each commuting pair $(g, h)$, the function $Z(g, h, \tau)$ has a Fourier expansion whose coefficients are graded traces of representations of the centralizer $C_M(g)$ of $g$ in $M$, lifted to actions on a graded vector space $V(g)$.

4. **Modular Transformations**: The functions transform under the action of $\text{SL}_2(\mathbb{Z})$ in a consistent manner, specifically: $Z(g^a h^c, g^b h^d; z) = \alpha \cdot Z(g, h; (az+b)/(cz+d))$ for $\begin{pmatrix} a & b \\ c & d \end{pmatrix} \in \text{SL}_2(\mathbb{Z})$, where $\alpha$ is a scalar phase factor.

5. **Normalization**: $Z(\text{id}, \text{id}, \tau) = j(\tau) - 744$, where $j$ is the modular j-invariant.

The conjecture was formulated by S.P. Norton in 1987 and generalizes the classical Monstrous Moonshine conjecture (which deals only with the identity element). Only special cases have been proven so far.

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

**Sources:**
- https://en.wikipedia.org/wiki/Monstrous_moonshine#Generalized_moonshine, https://sbseminar.wordpress.com/2009/01/08/generalized-moonshine-i-genus-zero-functions/, https://arxiv.org/abs/1902.03118, https://math.berkeley.edu/~reb/papers/monster/monster.pdf, https://encyclopediaofmath.org/wiki/Moonshine_conjectures

### Prerequisites needed

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

Building blocks (2):
- `Monoid.Centralizer`: centralizer structure for group elements
- `UpperHalfPlane`: the complex upper half-plane for holomorphic functions

Missing pieces (2):
- Monster group definition and its irreducible representations with grading
- Modular form infrastructure including genus zero modular functions (Hauptmodule), SL₂(ℤ) action, and modular transformation properties

Rating justification: Stating this conjecture requires formalizing the Monster group structure, vertex operator algebras with graded representations, and a complete theory of modular forms with genus zero properties. While basic group theory and complex analysis exist in Mathlib, the specialized infrastructure for moonshine (Monster representations, modular forms, and their interaction) requires significant new development.

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

* ams-20
* ams-30

### 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.

See more information here: [link](https://leanprover.zulipchat.com/#narrow/channel/524981-Formal-conjectures/topic/Custom.20Agent.20for.20Issue.20Generation/with/569221879)

Feedback on mistakes/hallucinations: [link](https://leanprover.zulipchat.com/#narrow/channel/524981-Formal-conjectures/topic/Issue.20Agent.20Feedback.20Topic/with/569223911)