# Verification report — OWR-782-001, duplicate OWR-782-002 (extremal modular forms modulo p)

Verification date: 2026-10-01.

**Verdict.** Conjecture 4 of Bannai, Koike, Shinohara and Tagami is true, with Case (2) read as in the journal
abstract. Let f_k be the extremal modular form of weight k and p a prime in Case (2), i.e. f_k mod p is a nonconstant
power series in q^p. Then:
- f_k(τ) ≡ f_{k'}(pτ) (mod p), where k' = w(f_k mod p)/p is even, 4 ≤ k' ≤ k/p and k' ≡ k (mod p − 1);
- this holds for every even k ≥ 4, not only for k = 12μ;
- so part (ii) of the conjecture holds with r = 1;
- iterating, it also holds for the largest possible r, and the last extremal form of the chain is in Case (3);
- for r ≥ 1, (ii) holds exactly for r = 1, …, R, with g unique modulo p (neither g nor its weight is unique: f_22 ≡ f_12
  (mod 11), and both serve for (252, 11)).

The result is a corollary of the classical theory of modular forms modulo p. The key input is w(h^p) = p·w(h), which
follows from Swinnerton-Dyer's structure theorem and the fact that the Hasse polynomial à has no repeated factor
(Serre uses it in Sém. Bourbaki 416, §2.2); it is the mechanism behind the Serre–Katz theorem on the kernel of θ. The
note is unrefereed and claims no novelty beyond "not found in print". Two independent AI-assisted verification runs
(2026-09-30 and 2026-10-01) found no error, and their separate programs reproduce all computations (see below).

## Statement checked
- **Primary source.** E. Bannai (joint work with M. Koike, M. Shinohara, M. Tagami), "Spherical designs, extremal
  lattices and the Fourier coefficients modulo p of the extremal modular forms", Oberwolfach Reports 2 (2005), no. 1,
  pp. 12–15, in Report 1/2005 "Gitter und Anwendungen" (organisers C. Bachoc, E. Bayer-Fluckiger, G. Nebe),
  doi:10.4171/OWR/2005/01.
  - The extended abstract occupies pp. 12–15; its reference list is on p. 15.
  - The three cases are defined on p. 13; Theorems 2 and 3 and Conjecture 4 are on p. 14.
  - Pages 13 and 14 were read in a rendering of the EMS PDF.
- **Second printing.** E. Bannai, RIMS Kôkyûroku 1440 (2005), pp. 1–4, hdl:2433/47528 (KURENAI, open access). A
  Japanese preface is followed by the same English extended abstract. Case (2) is on p. 3 and Conjecture 4 on p. 4.
  Both pages were read in a rendering of the PDF.
- **Misprint in both printings.** The first condition of Case (2) is printed "p ∤ a_i" (OWR p. 13, RIMS p. 3).
  - Read literally, Case (2) is empty for k = 12μ, since a_1 = 0, and the conjecture would be vacuous.
  - The journal abstract (below) has "p | a_i". This is also the only reading under which exactly one of the three
    "(exclusive)" cases holds for every pair (k, p).
  - The note uses the corrected reading and does not exploit the misprint. It records the misprint in both printings.
- **Journal version.** E. Bannai, M. Koike, M. Shinohara, M. Tagami, Moscow Math. J. 6 (2006), no. 2, 225–264,
  doi:10.17323/1609-4514-2006-6-2-225-264, Zbl 1121.11046, MR 2270613.
  - Only the abstract was read (Math-Net.Ru, mmj245). It says the paper ends by proposing a conjecture that may
    characterize Case (2), so the question was still open there.
  - The full text is behind a paywall (the DOI resolves to an AMS login page). Its wording of the conjecture and any
    further partial results could not be compared. If possible, someone with library access should glance at it.
- **Corpus records.** ulamai/UnsolvedMath 1.6.0:
  - OWR-782-001: Conjecture 4 as printed; status `partially_solved`.
  - OWR-782-002: the same conjecture, paraphrased, asking for an extremal g already in (i); status
    `partially_solved`. It is a duplicate of OWR-782-001, and the note answers both.

## Readings
| Reading | Answer | Where in the note |
|---|---|---|
| Case (2) as in the journal abstract ("p \| a_i for p ∤ i, and some a_j ≢ 0") | conjecture true | Thm 1.2, Cor 1.3 |
| Case (2) literally as printed in OWR/RIMS ("p ∤ a_i") | Case (2) empty for k = 12μ; conjecture vacuous | §1 |
| (i): g any modular form of smaller weight | yes, g = f_{k'}, weight k' ≤ k/p | Thm 1.2 |
| (ii) with some natural number r | yes, r = 1 | Cor 1.3 |
| (ii) with the largest possible r | yes; the chain k > k_1 > … > k_R ends at an extremal form in Case (3) | Cor 1.3(a)–(c) |
| (ii) for which r ≥ 1? | exactly r = 1, …, R; g is unique modulo p, g ≡ f_{k_r} (mod p), but neither g nor its weight is unique | Cor 1.3(c), §4 |
| OWR-782-002 wording (g extremal already in (i)) | yes | Thm 1.2 |
| all even weights k ≥ 4 instead of k = 12μ | yes (needed for the chain, e.g. 504 > 44 > 4) | Thm 1.2, Table 1 |

## Results in the paper
- **Theorem 1.2.** If p is in Case (2) for f_k (k ≥ 4 even), then p ≥ 5, (p−1) ∤ k, w(f_k mod p) = p·k' with k' even,
  4 ≤ k' ≤ k/p, k' ≡ k (mod p−1), and f_k(τ) ≡ f_{k'}(pτ) (mod p).
  - Proof: G := T_p f_k mod p lies in weight k and f_k mod p = G(q^p) = G^p.
  - w(G^p) = p·w(G) (Lemma 2.3(d)) gives k' := w(G) ≤ k/p; weights agree mod p−1 (Serre, Th. 2).
  - G = 1 + O(q^{⌊(d−1)/p⌋+1}) and dim M_{k'} ≤ ⌊(d−1)/p⌋ + 1 (Step 5, with a separate argument for k ≡ 2 mod 12).
  - The integral Miller basis then forces G ≡ f_{k'}.
- **Corollary 1.3.** The chain k_{i+1} = w(f_{k_i} mod p)/p gives f_k(τ) ≡ f_{k_i}(p^i τ). It ends at a form in Case (3),
  and (ii) holds exactly for r = 1, …, R, with g unique modulo p. Hence Conjecture 4 holds in both readings.
- **Corollary 1.4.**
  - (a) Case (1) ⟺ (p−1) | k. This is the source's own result; a proof is included.
  - (b) A finite test for Case (2): some even k' ≤ k/p with k' ≡ k (mod p−1) and f_{k'} ≡ 1 + O(q^{⌊(d−1)/p⌋+1}).
    The least such k' is w/p.
  - (c) In Case (2), p ≤ k/4. For k = 12μ this gives 11 ≤ p ≤ 3μ and p ≠ 13.
- **Lemma 2.1** (integral Miller basis), **Theorem 2.2** (Swinnerton-Dyer, as stated by Serre), **Lemma 2.3**
  (injectivity on graded pieces, representatives, filtration test, w(h^p) = p·w(h)), **Lemma 3.1** (Case (1)),
  **Lemma 3.2** (sufficient criterion via f_{k'}^p E_{p−1}^m).
- **Table 1 and §4.** Examples: f_84 ≡ E4(q^11) mod 11 and ≡ E4(q^17) mod 17; f_252 ≡ Θ_Leech(q^11) mod 11;
  f_504 ≡ f_44(q^11) ≡ E4(q^121) mod 11 (R = 2); f_5544 ≡ E4(q^1331) mod 11 (R = 3, chain 5544 > 484 > 44 > 4).
  - R ≥ 3 needs k ≥ 4·11^3 when 12 | k; the first case is (5364, 11).
  - For k = 12μ ≤ 7200 the chain lengths are R = 1, 2, 3 for 3306, 703 and 31 pairs.
  - Only the reduction of g is determined. For (252, 11) the weights 12 and 22 both pass the test of Corollary 1.4(b)
    (f_22 ≡ f_12 mod 11), and for (5544, 11) the weights 484, 494 and 504 do.
- **Remark 4.1** (explicitly about the OWR/RIMS text).
  - Theorem 2 of the extended abstract is the dimension-forced special case of Lemma 3.2. Under the natural reading
    r2 ≥ k2 ⟺ k ≥ p·k2, it misses 240 of the 1631 Case-(2) pairs with μ ≤ 300; the first is (252, 11).
  - Theorem 3 as printed fails for Case-(1) primes, e.g. (k, p) = (12, 13). With (p−1) ∤ k added it agrees with the
    computations for μ ≤ 600 (μ ≤ 300 in the primary run). The journal version may contain this hypothesis.

## Computations (exact; scripts and outputs in reproducibility/)
- **Primary** (`primary/`, standard library only).
  - `bkst_verify.py 300 1200` (about 4 min). f_k is computed by the j-polynomial method and cross-checked.
  - Every prime is certified for every weight k = 12μ ≤ 3600 and every even k ≤ 1200.
  - Result: 1631 + 2191 = 3822 Case-(2) pairs, 0 unresolved, 0 filtration mismatches.
  - It also produces the counts on the source's Theorems 2 and 3.
  - `spot_check.py`, `sd_check.py 900` and `tabulate.py` give further checks and statistics.
- **Independent verification run** (`independent/`, AI-assisted, separately written).
  - `indep_verify.py` computes f_k by the t = Δ/E4³ hypergeometric expansion and detects Case (2) by the θ criterion
    with the level-one bound. It does not use the note's results for the detection.
  - It then tests every conclusion, with filtrations computed by a separate implementation modulo p.
  - μ ≤ 300 and k ≤ 1200: the same 3822 pairs with the same (k', R) as the primary run (`compare.py`).
  - μ ≤ 600 and even k ≤ 2400: 4040 + 5393 = 9433 pairs, no failure.
  - `spot_r3.py`: f_5544 ≡ E4(q^1331) mod 11 for n < 2700.
  - That run's re-runs of the primary programs are in `independent/rerun_of_primary/`.
- **Final re-runs** (`final/`, 2026-10-01). All programs were re-run: `bkst_verify.py 300 1200`, `indep_verify.py`
  (300 1200 and 600 2400), `spot_check.py`, `sd_check.py 900`, `tabulate.py`, `spot_r3.py` and `compare.py`.
  - The results are identical to the recorded outputs apart from timing lines.
  - `paper_numbers.py` extracts every number quoted in the note from the recorded outputs.
- **Second independent verification run** (`independent_run_2/`, AI-assisted, 2026-10-01, separately written).
  - f_k is computed by exact elimination in the basis of Lemma 2.1, with Δ from Jacobi's identity, and separately modulo p.
  - Case (2) is decided by the θ test and a gcd for every prime.
  - Filtrations are computed from extremal forms alone: f_k mod p lies in M~_w iff f_w ≡ 1 + O(q^{d_k}) mod p.
  - Range: all k = 12μ ≤ 7200, all even k ≤ 2400, all primes. Result: 9433 Case-(2) pairs, with no failure of Theorem 1.2
    (including w(f_k mod p) = p·w(f_{k'} mod p)), of Corollary 1.3 or of Corollary 1.4.
  - (k, p, k', R) agrees pair by pair with the primary run (3822 pairs) and with the first independent run (9433 pairs).
  - Table 1 is confirmed with long-range congruences.
  - R = 3 for p = 11 exactly at the 31 weights 12μ with 447 ≤ μ ≤ 597 and μ ≡ 2 (mod 5).
  - Theorem 2.2(iii) holds for 5 ≤ p ≤ 1000.
  - Its reruns of all programs above, from an extracted copy of the released source archive, are in
    `independent_run_2/rerun_of_package/`. They are identical to the recorded outputs apart from timing lines.

## Independent verification runs
### First independent verification run (2026-09-30, AI-assisted)
This run checked the argument, the sources and the computations:
- Classification: paper candidate (a short note).
- Correct: yes. Every step was checked (Lemma A of the draft = Lemma 2.3, the dimension bound including k ≡ 2 mod 12,
  the Miller-basis uniqueness, the corollaries and the chain).
- Fidelity: the corrected Case (2) is the intended one. r = 1 is a legitimate witness, and the maximal-r reading also
  holds.
- Novelty: no proof found in print. The key lemma is classical, so a specialist may view the result as a short
  exercise; it is not "clearly folklore", since the conjecture's authors left it open in three printings.

The six required fixes and how they were applied:
1. **Classical input credited up front.** The abstract and §1 present the result as a corollary of classical mod-p
   theory, crediting w(h^p) = p·w(h) and the Serre/Katz kernel-of-θ theorem. The equality is cited as used in
   Serre's Bourbaki exposé 416, §2.2. Swinnerton-Dyer (LNM 350), Serre (exposé 416 and LNM 350) and Katz (LNM 601) are
   credited.
   - Theorem numbers were checked in Serre's Bourbaki exposé 416 (open-access Numdam PDF, pages rendered and read):
     Th. 1 (ker ρ = (Ã − 1), attributed to Swinnerton-Dyer) and Th. 2 (weights ≡ mod p−1) on pp. 321–322.
   - Also checked there: Th. 3 (Deligne: Ã is the Hasse invariant) and its Cor. 1 (Ã has no multiple factors), p. 323.
   - Also checked: Th. 5 (attributed to Swinnerton-Dyer) with Cor. 1 (Ã, B̃ coprime; Ã squarefree), p. 325, and
     Cor. 2 (M̃ stable by θ, θM̃_k ⊂ M̃_{k+p+1}) with Cor. 3 (w(θf) ≤ w(f)+p+1, equality iff p ∤ w(f)), p. 326.
   - Also checked: the definition of the filtration (§1.4) and w(φ^p) = p·w(φ) in the proof of the Lemma of §2.2
     (p. 329).
   - Swinnerton-Dyer's own paper (LNM 350), Serre's LNM 350 paper and Katz (LNM 601) were not accessible. The note says
     so and cites them for attribution only, following Serre's exposé and Böcherer–Kikuta–Takemori (§1; read in
     arXiv:1606.06390v1).
2. **Misprint documented in both printings** (OWR p. 13, RIMS p. 3; the journal abstract has "p | a_i"). RIMS
   Kôkyûroku 1440 was added to the sources and the bibliography.
3. **Maximal-r reading stated explicitly.** Corollary 1.3 says the chain ends in a Case-(3) extremal form and that
   (ii) holds exactly for r = 1, …, R.
4. **Prior-art limitation stated.** The Scope paragraph says the journal full text was not read (paywall). It gives
   the citation-index counts: zbMATH 14, Math-Net.Ru 16 and Semantic Scholar 26 citing works, none relevant among those
   read. It notes that Koike (2009) treats only congruences modulo powers of 2 and 3.
5. **Theorem-3 remark qualified.** Remark 4.1 begins "This refers to the text of the extended abstract" and ends with
   "The journal version, which we have not seen, may contain this hypothesis".
6. **Both records cited.** The note cites OWR-782-001 and OWR-782-002 (duplicate) in §1, in the Scope paragraph, in
   the bibliography entry for the dataset and in the PDF keywords. Any HF notice should cite both records.

### Second independent verification run (2026-10-01, AI-assisted)
This run checked the argument, the cited statements and the sources, and did the computations with its own programs
(`reproducibility/independent_run_2/`).

**Sources**, fetched anonymously and read in page renderings:
- OWR 1/2005, pp. 12–15. The TIB open-access copy of the EMS PDF; the Crossref record gives vol. 2, no. 1, pp. 5–67.
- RIMS Kôkyûroku 1440, pp. 1–4 (KURENAI). The English extended abstract there is headed by all four authors.
- The MMJ abstract (Math-Net.Ru). It prints "p | a_i" and reports 16 citing papers.

**Statement and fidelity.**
- The misprint "p ∤ a_i" is on OWR p. 13 and RIMS p. 3.
- Conjecture 4 is on OWR p. 14 and RIMS p. 4.
- The paraphrase in the note, the page ranges and the readings are all correct.

**Proofs.** Every lemma and step was checked line by line. This includes:
- the hypotheses of Lemma 2.3(d) (p ≥ 5, Th. 1 of Serre's exposé, Ã squarefree);
- the passage to f_{k'} through the Miller basis;
- Step 5 for k ≡ 2 (mod 12);
- the chain and the uniqueness modulo p in Corollary 1.3;
- the bounds of Corollary 1.4(c).

No error was found.

**Cited results.** These were checked in Serre's exposé (Numdam):
- §1.2 (the monomial basis of M̃_k, p. 321);
- Th. 1 [18] (p. 321) and Th. 2 (p. 322);
- Th. 3 (Deligne) with Cor. 1 (p. 323);
- Th. 5 [18] with Cor. 1 (p. 325);
- Cor. 2, Cor. 3 and the filtration of §1.4 (p. 326);
- the argument "A ne divise pas Φ^p ; la filtration de φ^p est donc ph" in §2.2 (p. 329).

Serre's [18] is Swinnerton-Dyer's unpublished 1971 manuscript. BKT18 §1 credits Serre (LNM 350) for level one and Katz
for general level. All nine DOIs were rechecked via Crossref.

**Computations.**
- Own programs: 9433 Case-(2) pairs for all 12μ ≤ 7200, all even k ≤ 2400 and all primes, with no failure.
- They agree pair by pair with both earlier runs.
- Table 1 and the counts of Remark 4.1 are confirmed. So is the first R = 3 weight 5364, with 31 R = 3 weights for μ ≤ 600.
- Ã is squarefree for 5 ≤ p ≤ 1000.
- All released programs were rerun from an extracted copy of the source archive. The outputs are identical apart from
  timing lines.

**Literature.** Anonymous requests only:
- the arXiv API;
- Crossref;
- zbMATH: 14 citing documents, none on Conjecture 4, and Nakaya's arXiv text cites BKST06 only for the definition;
- the OpenAlex work lookup (the citing-works query was rate-limited);
- Math-Net.Ru;
- one web search.

No proof or statement of the result was found.

The required fixes and how they were applied:
1. **Verification item 1.** "E*_{k0}Δ^s P(j)" had an undefined s. It now reads Δ^μ, with P a polynomial of degree at
   most μ.
2. **Corollary 1.3.** It now says that g is unique modulo p, namely g ≡ f_{k_r} (mod p). §4 adds that neither g nor its
   weight is unique: f_22 ≡ f_12 (mod 11) for (252, 11), and the weights 484, 494, 504 for (5544, 11).
3. **Records.** The run is recorded in the note (Verification, item 3), in this report and in
   reproducibility/README.md. Its code and outputs are in `reproducibility/independent_run_2/` with a README.
4. **Docstring.** `final/paper_numbers.py` now refers to Remark 4.1; its output is unchanged.
5. **Release rebuilt.** The PDF, source archive, Zenodo copies and checksums were rebuilt.

Also applied:
- Serre's source for Th. 1 and Th. 5 is named (an unpublished 1971 manuscript of Swinnerton-Dyer).
- The RIMS bibliography entry says that the English extended abstract is headed by all four authors.
- Remark 4.1 now states the Theorem-3 agreement for μ ≤ 600.

## References checked (all anonymous requests, logged in ../queries.log)
| Reference | Checked via | Result |
|---|---|---|
| Bannai et al., OWR 2 (2005) no. 1 | Crossref 10.4171/OWR/2005/01 | report "Gitter und Anwendungen", pp. 5–67, organisers as cited; abstract pp. 12–15 in the PDF |
| Bannai, RIMS Kôkyûroku 1440 (2005) 1–4 | KURENAI record hdl:2433/47528 and CiNii | vol. 1440, pp. 1–4, July 2005, open access |
| Bannai–Koike–Shinohara–Tagami, Moscow Math. J. 6 (2006) | Crossref, zbMATH 1121.11046, Math-Net.Ru | 6(2):225–264 |
| Böcherer–Kikuta–Takemori, Canad. J. Math. 70 (2018) | Crossref 10.4153/CJM-2017-014-0 | 70(2):241–264 |
| Katz, LNM 601 (1977) | Crossref 10.1007/BFb0063944, zbMATH 0392.10026 | pp. 53–61 |
| Koike, Kyushu J. Math. 63 (2009) | Crossref 10.2206/kyushujm.63.123 | 63(1):123–132 |
| Serre, Sém. Bourbaki 416, LNM 317 (1973) | Crossref 10.1007/BFb0069289, zbMATH 0276.14013, Numdam | pp. 319–338 |
| Serre, LNM 350 (1973) | Crossref 10.1007/978-3-540-37802-0_4, zbMATH 0277.12014 | pp. 191–268 |
| Serre, A Course in Arithmetic, GTM 7 (1973) | Crossref 10.1007/978-1-4684-9884-4 (Ch. VII "Modular Forms", pp. 77–111) | cited at chapter level only |
| Swinnerton-Dyer, LNM 350 (1973) | Crossref 10.1007/978-3-540-37802-0_1, zbMATH 0267.10032 | pp. 1–55 |
| ulamai/UnsolvedMath 1.6.0 | local corpus snapshot | records OWR-782-001, OWR-782-002 |

## Relation to the literature, novelty and scope
- **Searches** (September–October 2026; anonymous):
  - arXiv API (about 20 metadata queries on extremal modular forms with congruences, mod p, θ-operator, filtration,
    lattices);
  - Crossref bibliographic queries, and zbMATH (including the 14 documents citing the journal version);
  - OpenAlex (20 citing works, from an earlier fetch), Semantic Scholar (26 citing works), Math-Net.Ru (16) and
    CiNii Research;
  - three web searches (one each by the author and by the two verification runs).
- **Findings.** Nothing proves or disproves Conjecture 4.
  - The citing works concern spherical designs, codes and Assmus–Mattson type theorems, Lehmer's conjecture and
    related topics.
  - Those read do not address the conjecture: Koike 2009, and the arXiv texts of Bannai–Miezaki and of Nakaya.
  - The Bannai–Bannai survey (Europ. J. Combin. 2009) was not read.
- **Caveats.** The journal full text was not read. Swinnerton-Dyer (1973), Serre (LNM 350) and Katz (1977) were not
  consulted directly. This negative search is not a proof of priority.
- **Novelty.** The argument uses only classical results. Experts may regard it as an exercise, and the note says so.
  What the note adds:
  - the observation and a written proof;
  - the sharp form (r = 1, k' = w/p) and the description of all admissible r;
  - the extension to all even weights and the finite test for Case (2);
  - the side remarks on the source's Theorems 2 and 3.

## Public release and license
This paper, its source files, and this verification report are licensed under the Creative Commons Attribution
4.0 International License (CC BY 4.0): https://creativecommons.org/licenses/by/4.0/