Normalized eigenforms

The coefficient sequence obeys extra arithmetic rules, with its first coefficient fixed to one.

Start with a concrete example

Start with the pair (1, b). Our toy machine changes (u, v) to (v, 2u + v). For b = 2 it sends (1, 2) to (2, 4): exactly twice the original pair. Try other b.

Move the number or condition

This input is scaled by 2 under the toy machine.

How this example differs from the definition

This two-number machine is not a Hecke operator on modular forms. It illustrates only the “same shape up to a multiple” idea.

A small check: try the idea

Compare the numbers in the question with the diagram you are moving. You can try again.

Our machine sends (1,2) to (2,4). How did the pair change?

Read the answer and reasoning

Both entries were multiplied by 2. Compare 1→2 and 2→4. Both have the same multiplier. Try b=3 to see that this pattern is not automatic for every input.

Build the idea in three steps

An operator acts on functions. An eigenfunction is sent to a scalar multiple of itself by the relevant operators.
For the weight-two cusp forms in this repository, IsNormalizedEigenform records specific coefficient identities that express the required arithmetic.
Normalization fixes the coefficient at one to 1. This rules out the zero form.

A small example

For coprime m and n, the definition requires a(mn) = a(m)a(n). This is a required identity, not a property of every number sequence.

Lean definition · original excerpt

FLT · aa2d8b3 · Def_FLTPrelim_Modularity.lean

28structure IsNormalizedEigenform {N : ℕ} (f : CuspForm (CongruenceSubgroup.Gamma0 N) 2) :29    Prop where30 31  qCoeff_one : qCoeff f 1 = 132 33  qCoeff_mul_of_coprime : ∀ m n : ℕ, m.Coprime n →34    qCoeff f (m * n) = qCoeff f m * qCoeff f n35 36  qCoeff_prime_pow_of_not_dvd : ∀ p r : ℕ, p.Prime → ¬ p ∣ N →37    qCoeff f (p ^ (r + 2)) = qCoeff f p * qCoeff f (p ^ (r + 1)) - p * qCoeff f (p ^ r)38 39  qCoeff_prime_pow_of_dvd : ∀ p r : ℕ, p.Prime → p ∣ N →40    qCoeff f (p ^ (r + 2)) = qCoeff f p * qCoeff f (p ^ (r + 1))

How to read this Lean

qCoeff_one is normalization. The following fields record multiplicativity and recurrences at prime powers, distinguishing primes that divide the level from those that do not.

Original source ↗ · L28–40 Open the complete saved source

Where this idea is used

8. The secret duet 9. Two doors to the concert 10. A three-note audition 11. Borrow a better passport 12. The workshops agree 13. Pip’s impossible quilt 14. The shrinking reservation

Normalized eigenforms

Start with a concrete example

A small check: try the idea

Build the idea in three steps

A small example

Lean definition · original excerpt

How to read this Lean

Where this idea is used

Mika’s help desk

One thing at a time

In simpler words

A small clue