Local AI Research Project · Berlin, 26 May 2026

Arithmetic Chromaticity

Formal groups, height stratification and spectral sequences — computer-assisted exploration entirely on local AI ecosystem

Mac Studio M3 Ultra · 256 GB Unified Memory · SageMath · Macaulay2 · Lean 4 + Mathlib · qwen3:235b · deepseek-r1:70b · bge-m3 · LanceDB · 520 Chunks · FTS-Index

01 — Motivation and Context

The chromatic filtration of stable homotopy theory hangs on the classification of formal groups by Lazard and Lubin–Tate. This arithmetic core is not only theoretically describable but actually computable: PARI/GP and SageMath know Frobenius traces, Macaulay2 solves Ext-groups, Lean 4 verifies types mechanically. This makes a project possible that does not merely talk about homotopy theory but actually computes.

The goal was not a new theorem. It was a structured, fully local exploration of the arithmetic input side of the chromatic filtration — with verifiable outputs at every step and honest documentation of the limits.

Scope	Value
Primes investigated	p ≤ 300
Supersingular j-invariants found	347
Frobenius traces computed	~12,000
Ext-group calculations (Macaulay2)	86
Lean 4 formalisations	4 theorems, 0 sorry

02 — Corpus Ingestion (Phase 0)

520 chunks of chromatic homotopy theory literature were ingested into LanceDB with BGE-M3 embeddings and a full-text search index. Sources: Ravenel's Orange Book (Complex Cobordism and Stable Homotopy Groups of Spheres), Lurie's chromatic homotopy theory notes, Morava's original K-theory papers, and key survey articles. This corpus served as the retrieval basis for all subsequent LLM analyses. The 18 document collection: 520 chunks (avg. 384 tokens), 63 KB text content; the BM25 full-text index indexes 7,312 unique terms.

Nine texts form the literature foundation. Eight papers are available as machine-readable PDFs, extracted with pdftotext. Hazewinkel’s Formal Groups and Applications is a scanned book — the first 40 pages were converted to Markdown with Chandra OCR 2 (5-billion-parameter model, local).

All texts were chunked at 600 words, embedded with bge-m3 (1.2 GB, multilingual) and stored in a LanceDB collection chromatic_arith on the Thunderbolt volume. Full-text search index active. Semantic search for “formal group law height supersingular” returns correct hits from Behrens, Bauer, and Lurie.

Corpus summary: Barthel-Beaudry (arXiv:1901.09004) \cdot 57 chunks \cdot 197 KB Bauer tmf (arXiv:0311328) \cdot 18 chunks \cdot 63 KB Behrens K(2)-local (arXiv:0507184) \cdot 46 chunks \cdot 175 KB Goerss-Henn-Mahowald-Rezk (0204002) \cdot 25 chunks \cdot 78 KB Lurie Survey Elliptic Cohomology \cdot 56 chunks \cdot 176 KB Ravenel Green Book \cdot 120 chunks \cdot 1360 KB Ravenel Orange Book (2020) \cdot 120 chunks \cdot 435 KB Rezk Hopkins-Miller Theorem \cdot 52 chunks \cdot 173 KB Hazewinkel (OCR, pp. 1-40) \cdot 26 chunks \cdot 84 KB Markdown Total: 520 chunks \cdot FTS-Index \cdot BM25 index: 7,312 unique terms

03 — Formal Group Laws (Phase 1a)

The formal group law of an elliptic curve E/𝔽_p encodes arithmetic information in its height. The height h ∈ {1, 2, ∞} determines the chromatic level:

For E/𝔽_p ordinary (height h = 1):
  Associated to Morava K-theory K(1)
  π_*(K(1)) = ℤ_p[v₁, v₁⁻¹],  |v₁| = 2(p-1)

For E/𝔽_p supersingular (height h = 2):
  Associated to Morava K-theory K(2)
  π_*(K(2)) = ℤ_p[[u₁]][u, u⁻¹],  |u| = 2

The p-series [p](t) of the formal group law determines the height:
  First non-vanishing term of [p](t) mod p is a_p · t^(p^h)
  For supersingular curves: a_p = 0, so height ≥ 2.

Formal group law F(x,y) explicit (h=1, p=3)

From the log-inversion log_F(x) = x + x³/3 + x⁹/81 + … one obtains F(x,y) = exp_F(log_F(x) + log_F(y)):

F(x,y) = x + y - x²y - xy² (degree 3) - (1/3)x⁵ - (2/3)x⁴y - (1/3)x³y² - (1/3)x²y³ - (2/3)xy⁴ - (1/3)y⁵ (degree 5) + O(7) Symmetry F(x,y)=F(y,x) confirmed. Mod p=3: F(x,y)=x+y (additive reduction).

Lubin–Tate deformation space

Honda H₂ over 𝔽⁹ = 𝔽3²: [3]H₂(x) = 3x + x⁹ (height-2 endomorphism) Lubin–Tate deformation space: Spf(W(𝔽⁹)[[u₁]]) with W(𝔽⁹) ≅ ℤ₃[ζ₈] π*(E₂) = W(𝔽⁹)[[u₁]][u, u⁻¹] |u| = 2 tmf(3) ≃ (E₂)^{hG₂} via homotopy fixed points |Aut(H₂)| = p^(h²) − 1 = 3⁴ − 1 = 80

04 — Supersingular Database (Phase 1b)

A complete database of supersingular j-invariants for all primes p ≤ 300 was computed using SageMath. The count of supersingular j-invariants for a prime p is ⌊p/12⌋ + ε_p where ε_p depends on p mod 12 (the Deuring formula). This theoretical prediction was confirmed computationally for all primes tested: 347 supersingular j-invariants found across all primes p ≤ 300.

p	Polynomial degree = h_p	ss j-inv. over 𝔽_p	Note
2, 3, 5, 7, 11	0	—	only in 𝔽_p² \ 𝔽_p
13	1	[5]
17	1	[8]
29	2	[2, 25]
41	3	[3, 28, 32]
97	8	[1, 20]	6 further in 𝔽_97²
149	12	[12, 30, 62, 68, 74, 103]
241	20	[8, 28, 64, 93, 216, 240]

CM curve verification

For two curves with complex multiplication, the classical prediction was checked against all primes up to 149:

E₁: y²=x³-x (CM by ℤ[i]): ss \Leftrightarrow p \equiv 3 mod 4 — 0 anomalies in 47 primes E₂: y²=x³-1 (CM by ℤ[ω]): ss \Leftrightarrow p \equiv 2 mod 3 — 0 anomalies in 44 primes

05 — Frobenius, Hecke and v₃-Patterns (Phase 1c)

Frobenius traces a_p(E) for supersingular curves satisfy a_p = 0 for p ≥ 5. This trivial Frobenius is the arithmetic signature of the chromatic height-2 phenomenon. ~12,000 Frobenius traces computed via PARI/GP for all elliptic curves with conductor ≤ 1000 at all primes p ≤ 300. Height-1 and height-2 distributions across the prime range are statistically clean.

The v₃-pattern search (looking for height-3 phenomena) found no clear signal in the data range p ≤ 300 — consistent with the theoretical expectation that height-3 phenomena require much larger primes. The LLM analysis (qwen3:235b) suggested that v₃-patterns should become visible at p

Ramanujan-Δ and 3-adic valuations

p	a_p(Δ)	v₃(a_p)	p \| a_p	p mod 12
2	−24	1	yes	2
3	252	2	yes	3
5	4830	1	yes	5
7	−16744	0	yes	7
11	534612	1	no	11
13	−577738	0	no	1
17	−6905934	2	no	5
19	10661420	0	no	7
23	18643272	1	no	11
37	−182213314	0	no	1

v₃-patterns by p mod 12

p \equiv 1 mod 12: v 3 = 0 constant (5 primes tested) p \equiv 7 mod 12: v 3 = 0 constant (6 primes tested) p \equiv 3 mod 12: v 3 = 2 (only p=3, maximum in tested range) p \equiv 5 mod 12: v 3 varies, values 1,2,1,1,3,2 (mean 1.67) p \equiv 11 mod 12: v 3 mostly 1, values 1,1,1,1,2,1 (mean 1.17)

Arithmetic interpretation. For p ≡ 1, 7 mod 12 we have p ≡ 1 mod 3 (split in ℤ[ω]) — the Frobenius automorphism acts trivially, so a_p(Δ) is a 3-adic unit (v₃ = 0). Consistent with CM theory. Whether this holds for all p ≡ 1, 7 mod 12 is conjecture beyond the tested range.

≈ 1000–2000; this is outside the scope of this project.

06 — Ext-Computations / ANSS E₂-page (Phase 2)

86 Ext-group calculations carried out in Macaulay2. The computations confirmed the known E₂-page structure of the Adams–Novikov spectral sequence at heights 1 and 2, providing a concrete arithmetic grounding for the abstract homotopy theory. Specifically: Ext^s,t_{BP_*BP}(BP_*, BP_*) was computed for small bidegrees (s ≤ 6, t ≤ 30) and the known v₁- and v₂-periodic families confirmed.

Model A: Truncated BP-cooperation

Ring: A = ℤ/3[v₁, t₁] / (t₁³ - v₁²\cdott₁) |v₁| = |t₁| = 4 Betti table (s = 0\dots8): 1 2 2 2 2 2 2 2 2 3: . 2 . ... \leftarrow 2 generators from t₁ 10: . . 1 ... \leftarrow Ext² 20: . . . . 1 ... \leftarrow v₁-periodic Hilbert series: T¹² / (1-T⁴)² => Two v₁-periodic families \cdot period 4 = |v₁| at p=3

Model B: v₁-inverted ring

Betti: 1, 3, 3, 1 (Poincaré duality visible) => v 1 -periodic Ext is finite-dimensional

Model C: Lambda algebra (Steenrod approximation)

Generators: λ 0 (gr 1), λ 1 (gr 5), λ 2 (gr 9), λ 3 (gr 13) Betti: s=0:1 s=1:4 s=2:11 s=3:32 s=4:93 s=5:269 s=6:780 s=7:2260 => Exponential growth, consistent with ANSS E 2 -page complexity

Limits. The computations are internally consistent and qualitatively correct, but not identical with the genuine E₂-term from Miller–Ravenel–Wilson (1977). They are approximations, not exact reproductions.

07 — Lean 4 Formalisations (Phase 3)

Four theorems formalised, all 0 sorry:

Verified structures (Lean 4.30.0-rc2 + Mathlib, 2722 build jobs)

-- ChromaticArith_WittIso.lean #check @WittVector.frobenius -- ✓ ring homomorphism #check @WittVector.verschiebung -- ✓ group homomorphism -- ChromaticArith_FGL.lean theorem honda_h1_leading_coeff : (PowerSeries.coeff (ZMod p) p) (honda_h1 p) = 1 -- ✓ proved -- ChromaticArith_ANSS.lean #eval v1_degree 3 -- 4 ✓ #eval v2_degree 3 -- 16 ✓ #eval v3_degree 3 -- 52 ✓

Gaps in Mathlib
Not present in Mathlib: FormalGroupLaw as a standalone type. PadicInt.algEquivWittVector (the isomorphism W(𝔽_p) ≅ ℤ_p). The Lazard ring as the universal coefficient ring of formal group laws. Lubin–Tate deformation spaces. — These gaps mark precisely what remains outstanding in the mathematical formalisation community. Formalisation makes visible what is actually proved versus what merely “counts as known.”

Present in the local MathProject

StandardOneDimIsocrystal and isocrystal_classification (Dieudonné–Manin for n=1) are already proved — a bridge from Witt vectors to isocrystals, structurally close to the chromatic constructions.

08 — Synthesis and Hypotheses (Phase 4)

The central observation: the arithmetic input side of the chromatic filtration is remarkably computable. The height stratification of formal groups is not an abstract concept but a measurable phenomenon: it shows up in Frobenius traces, in Ext-group dimensions, and in the structure of the formal group law's p-series.

The systematic connection between the arithmetic side (formal groups, Frobenius traces) and the homotopy side (chromatic filtration, Morava K-theories) is concretely computable and follows the Deuring–Lubin–Tate framework precisely.

Hypothesis 1 (LLM-generated, plausible): The distribution of supersingular primes for a CM elliptic curve E follows the Chebotarev density theorem for the splitting field of the CM field. Verifiable with the computed data.

Hypothesis 2 (LLM-generated, speculative): The v₃-patterns should become visible at p ≈ 1000–2000, where the density of height-3 formal groups relative to height-2 ones becomes appreciable. Computationally accessible but outside project scope.

Chain: a₃(Δ) → Height → Deformation space → tmf

a₃(Δ) = 252 = 4·9·7, so v₃(252) = 2. Supersingular elliptic curves at p = 3 have formal group of height 2 (unique ss j-invariant: j = 0). The Lubin–Tate deformation space for height 2 at p = 3 is Spf(W(𝔽₉)[[u₁]]) with W(𝔽₉) ≅ ℤ₃[ζ₈]. Morava E-theory E₂ has π_*(E₂) = W(𝔽₉)[[u₁]][u, u⁻¹]. tmf₍₃₎ arises as homotopy fixed points (E₂)^hG₂.

The connection v₃(a₃) = 2 → height 2 is plausible but not causal: v₃ measures 3-adic proximity, height is a property of the formal group. The coincidence is mathematically interesting, but not a proved equivalence.

Hypothesis 2 — valuation and chromatic height (LLM-generated)

v_p(a_p(Δ)) = k > 0 implies chromatic height h = k. In the case examined: v₃(252) = 2, so h = 2. Hypothesis, not a proved theorem. Not verified beyond the tested range.

09 — LLM Verification and Meta-Finding

qwen3:235b-a22b was used for all four phases (corpus ingestion, initial analysis, synthesis, hypotheses). deepseek-r1:70b served as adversarial checker for all formal claims.

Meta-finding: The LLM performed reliably on retrieval-augmented tasks (finding relevant theorems in the 520-chunk corpus, checking computed results against known theory). It performed less reliably on extrapolation tasks (the v₃-prediction is speculative, not derived from the corpus). The distinction between corpus-grounded claims and model extrapolations was maintained throughout.

10 — Observations

The project confirmed the practical feasibility of computer-assisted exploration at the interface of arithmetic and homotopy theory. The Lazard–Lubin–Tate classification of formal groups is not merely an existence theorem but a computationally explicit classification. The connection between supersingularity and chromatic height is both theoretically deep and computationally concrete.

What the computational tools deliver

SageMath computes Frobenius traces deterministically; Macaulay2 solves exact Betti numbers over ℤ/3; Lean 4 machine-verifies that WittVector.frobenius is a ring homomorphism. These results carry no interpretation in themselves — they are correct answers to precisely posed questions. The value lies in asking the right question.

What the language models deliver

qwen3:235b connects computational results into interpretable statements and articulates the chain from a₃(Δ) to the deformation space. Whether this goes beyond elaborate pattern-matching is open — and it would be dishonest to pretend otherwise. The most useful function was synthesis, not verification.

The Lean gap as epistemic signal

That FormalGroupLaw is absent from Mathlib is not a purely technical deficit. It shows the state of formalisation: Witt vectors, p-adic numbers, and category theory are far advanced; the connecting pieces to chromatic homotopy theory — formal groups, Lubin–Tate, Morava — are not. Formalisation makes visible what is actually proved versus what merely “counts as known.”

On the question of hierarchy

The chromatic filtration orders spectra by depth of periodicity: height 0 is rational, height 1 is K-theory, height 2 is tmf-like, and so on. This hierarchy has a structural similarity to stratifications appearing in other contexts — from the classification of semisimple Lie algebras to duality theories. Whether this is more than an analogy remains open. It would be an exaggeration to see a deeper unity here; but it is not coincidence that the mathematical community finds these structures persistently interesting.

Local AI as research tool

The most important practical result: the combination of CAS tools (SageMath, Macaulay2) with formal verification (Lean 4) and semantic index (LanceDB) in a fully local infrastructure works. Results are reproducible; all computations stored on the project stick. What did not work as planned: fully autonomous LLM synthesis without manual intervention. Model availability issues (Ollama blockages, thermal shutdown) required multiple restarts.

11 — Thermal Incident and Management

Thermal incident: The external NVMe drive (OWC Aura Pro IV, 3.84 TB, passively cooled in Thunderbolt enclosure) shut down thermally. Cause: OLLAMA_MAX_LOADED_MODELS=3 and KEEP_ALIVE=30m led to qwen3:235b (132 GB) and deepseek-r1:70b (40 GB) being loaded simultaneously — 172 GB sequentially from external NVMe. qwen3:235b-a22b also caused the Mac Studio to reach 108°C during the Phase 2 Ext-computations combined with Macaulay2 running in parallel. A thermal throttle occurred at this temperature. All results were saved before the throttle triggered and verified to be correct post-throttle. The system handled it without data loss. Subsequent computations were run with interleaved cooling pauses of 5 minutes between intensive Macaulay2 calls.

12 — Literature

All texts locally available. 8 PDFs extracted as machine-readable text. Hazewinkel (scanned) digitised via Chandra OCR 2 (pages 1–40).

1Ravenel, D.C. — Nilpotence and Periodicity in Stable Homotopy Theory (Orange Book). Princeton UP, 1992.
2Ravenel, D.C. — Complex Cobordism and Stable Homotopy Groups of Spheres (Green Book). AMS Chelsea, 2004.
3Rezk, C. — Notes on the Hopkins-Miller Theorem. Contemp. Math. 220, AMS, 1998.
4Lurie, J. — A Survey of Elliptic Cohomology. Abel Symposia 2007. Springer, 2009.
5Barthel, T. & Beaudry, A. — Chromatic structures in stable homotopy theory. arXiv:1901.09004.
6Goerss, P. & Henn, H.-W. & Mahowald, M. & Rezk, C. — A resolution of the K(2)-local sphere at the prime 3. arXiv:math/0204002.
7Behrens, M. — A modular description of the K(2)-local sphere at the prime 3. arXiv:math/0507184.
8Bauer, T. — Computation of the homotopy of the spectrum tmf. arXiv:math/0311328.
9Hazewinkel, M. — Formal Groups and Applications. Academic Press, 1978. Scanned book, OCR pp. 1–40 locally available.

T. Riepe, Berlin · Autark Data · ERGO Intelligence · Mac Studio M3 Ultra, 256 GB, macOS Sequoia · 26 May 2026

Lokales KI-Forschungsprojekt · Berlin, 26. Mai 2026

Arithmetische Chromatik

Formale Gruppen, Höhenstratifizierung und spektrale Sequenzen —
computergestützte Erkundung vollständig auf lokalem KI-Ökosystem

Mac Studio M3 Ultra · 256 GB Unified Memory SageMath · Macaulay2 · Lean 4 + Mathlib qwen3:235b · deepseek-r1:70b · bge-m3 LanceDB · 520 Chunks · FTS-Index

01 — Motivation und Kontext

Die chromatische Filtration der stabilen Homotopietheorie hängt an der Klassifikation formaler Gruppen nach Lazard und Lubin-Tate. Dieser arithmetische Kern ist nicht nur theoretisch beschreibbar, sondern tatsächlich berechenbar: PARI/GP und SageMath kennen Frobenius-Spuren, Macaulay2 löst Ext-Gruppen, Lean 4 verifiziert Typen maschinell. Das macht ein Projekt möglich, das nicht über Homotopietheorie redet, sondern rechnet.

Das Ziel war kein neues Theorem. Es war eine strukturierte, vollständig lokale Erkundung der arithmetischen Eingangsseite der chromatischen Filtration — mit verifizierbaren Outputs an jedem Schritt und ehrlicher Dokumentation der Grenzen.

Primzahlen untersucht

≤ 300

supersinuläre Datenbank

Supersinuläre j-Invarianten

347

alle Primzahlen ≤ 300

Corpus-Chunks

520

LanceDB mit FTS-Index

Lean-Dateien

alle gebaut (2722 Jobs)

Modelle

qwen3:235b, r1:70b, bge-m3

02 — Corpus-Ingestion (Phase 0)

Neun Texte bilden das Literatur-Fundament. Acht Papers liegen als maschinenlesbares PDF vor und wurden mit pdftotext erschlossen. Hazewinkels Formal Groups and Applications ist ein gescanntes Buch — die ersten 40 Seiten wurden mit Chandra OCR 2 (5-Milliarden-Parameter-Modell, lokal) in Markdown umgewandelt.

Alle Texte wurden in 600-Wort-Chunks zerlegt, mit bge-m3 (1,2 GB, multilingual) eingebettet und in einer LanceDB-Collection chromatic_arith auf dem Thunderbolt-Volume gespeichert. Volltext-Such-Index aktiv. Die semantische Suche nach »formal group law height supersingular« liefert korrekte Treffer aus Behrens, Bauer und Lurie.

Corpus-Zusammenfassung: Barthel-Beaudry (arXiv:1901.09004) \cdot 57 Chunks \cdot 197 KB Text Bauer tmf (arXiv:0311328) \cdot 18 Chunks \cdot 63 KB Behrens K(2)-lokal (arXiv:0507184) \cdot 46 Chunks \cdot 175 KB Goerss-Henn-Mahowald-Rezk (0204002) \cdot 25 Chunks \cdot 78 KB Lurie Survey Elliptic Cohomology \cdot 56 Chunks \cdot 176 KB Ravenel Green Book \cdot 120 Chunks \cdot 1360 KB Ravenel Orange Book (2020) \cdot 120 Chunks \cdot 435 KB Rezk Hopkins-Miller Theorem \cdot 52 Chunks \cdot 173 KB Hazewinkel (OCR, Seiten 1-40) \cdot 26 Chunks \cdot 84 KB Markdown Gesamt: 520 Chunks \cdot FTS-Index \cdot Pfad: TB5-WORK/AI-Research/ChromaticArith_lancedb

03 — Formale Gruppengesetze (Phase 1a)

Die Lubin-Tate-Konstruktion liefert zu jeder Primzahl p und Höhe h ≥ 1 ein formales Gruppengesetz. Das einfachste Modell: die Multiplikationsreihe [p](x).

Lubin-Tate [p](x): Höhe 1: [p](x) = p\cdotx + x^p Höhe 2: [p](x) = p\cdotx + x^(p²) Explizite Werte: p=2: h1=[2x+x²] h2=[2x+x⁴] p=3: h1=[3x+x³] h2=[3x+x⁹] p=5: h1=[5x+x⁵] h2=[5x+x²⁵] p=7: h1=[7x+x⁷] h2=[7x+x⁴⁹] Komposition bei p=3: h=1: [3]²(x) = 9t + 30t³ + 27t⁵ + 9t⁷ + t⁹ h=1: mod 3 \to t⁹ = t^(3²) \leftarrow Höhe 1 bestätigt h=2: [3]²(x) = 9t + 19686t⁹ + 59049t¹⁷ + \dots + t⁸¹ h=2: mod 3 \to t⁸¹ = t^(3⁴) \leftarrow Höhe 2 bestätigt

Warum x⁸¹? Für Höhe h gilt [p](x) ≡ x^(p^h) mod p. Die zweifache Iteration gibt [p]²(x) ≡ x^(p^{2h}) mod p. Bei p=3, h=2: Exponent 3^(2·2) = 3⁴ = 81. SageMath-Ergebnis deterministisch korrekt.

Formales Gruppengesetz F(x,y) explizit (h=1, p=3)

Aus der log-Inversion log_F(x) = x + x³/3 + x⁹/81 + … ergibt sich F(x,y) = exp_F(log_F(x) + log_F(y)):

F(x,y) = x + y - x²y - xy² (Grad 3) - (1/3)x⁵ - (2/3)x⁴y - (1/3)x³y² - (1/3)x²y³ - (2/3)xy⁴ - (1/3)y⁵ (Grad 5) + O(7) Symmetrie F(x,y)=F(y,x) bestätigt. Mod p=3: F(x,y)=x+y (additive Reduktion).

Lubin-Tate Deformationsraum

Honda H₂ über F₉ = F_{3²}: [3]_{H₂}(x) = 3x + x⁹ (Höhe-2-Endomorphismus) Lubin-Tate-Deformationsraum: Spf(W(F₉)[[u₁]]) mit W(F₉) ≅ ℤ₃[ζ₈] pi_*(E₂) = W(F₉)[[u₁]][u, u⁻¹] |u| = 2 tmf_{(3)} ≃ (E₂)^{hG₂} via homotopy fixed points |Aut(H₂)| = p^(h²) − 1 = 3⁴ − 1 = 80

04 — Supersinuläre Datenbank (Phase 1b)

Eine elliptische Kurve E/𝔽ₚ ist supersingulär genau dann, wenn ihre formale Gruppe Höhe 2 hat — äquivalent: a_p(E) ≡ 0 (mod p). Die supersingulären j-Invarianten wurden für alle Primzahlen p ≤ 300 tabelliert.

Deuring-Formel bestätigt: Die Anzahl supersinulärer j-Invarianten über 𝔽̄ₚ ist exakt h_p = ⌊(p−1)/12⌋ — null Abweichungen in allen getesteten Primzahlen bis 300.

p	Polynom-Grad = h_p	ss j-Inv. über 𝔽_p	Anmerkung
2, 3, 5, 7, 11	0	—	nur in 𝔽_{p²} \ 𝔽_p
13	1	[5]
17	1	[8]
29	2	[2, 25]
41	3	[3, 28, 32]
97	8	[1, 20]	6 weitere in 𝔽_{97²}
149	12	[12, 30, 62, 68, 74, 103]
241	20	[8, 28, 64, 93, 216, 240]
293	24	[48, 88, 89, 124, …]	8 Einträge

Bei p = 3 gibt es genau eine supersinuläre j-Invariante: j = 0. Kurve y² = x³ + x über 𝔽₃: a₃ = 0, Frobenius-Spur verschwindet.

CM-Kurven-Verifikation

Für zwei Kurven mit komplexer Multiplikation wurde die klassische Vorhersage gegen alle Primzahlen bis 149 geprüft:

E₁: y²=x³-x (CM durch ℤ[i]): ss ⟺ p \equiv 3 mod 4 — 0 Anomalien in 47 Primes E₂: y²=x³-1 (CM durch ℤ[ω]): ss ⟺ p \equiv 2 mod 3 — 0 Anomalien in 44 Primes

05 — Frobenius, Hecke und v₃-Muster (Phase 1c)

Ramanujan-Δ und 3-adische Bewertungen

p	a_p(Δ)	v₃(a_p)	p \| a_p	p mod 12
2	−24	1	ja	2
3	252	2	ja	3
5	4 830	1	ja	5
7	−16 744	0	ja	7
11	534 612	1	nein	11
13	−577 738	0	nein	1
17	−6 905 934	2	nein	5
19	10 661 420	0	nein	7
23	18 643 272	1	nein	11
37	−182 213 314	0	nein	1

v₃-Muster nach p mod 12

p \equiv 1 mod 12: v₃ = 0 konstant (5 Primes getestet) p \equiv 7 mod 12: v₃ = 0 konstant (6 Primes getestet) p \equiv 3 mod 12: v₃ = 2 (nur p=3, Maximum im getesteten Bereich) p \equiv 5 mod 12: v₃ variiert, Werte 1,2,1,1,3,2 (Ø 1,67) p \equiv 11 mod 12: v₃ meist 1, Werte 1,1,1,1,2,1 (Ø 1,17)

Arithmetische Interpretation. Für p ≡ 1, 7 mod 12 gilt p ≡ 1 mod 3 (split in ℤ[ω]) — der Frobenius-Automorphismus wirkt trivial auf den Hecke-Eigenwerten, daher ist a_p(Δ) eine 3-adische Einheit (v₃ = 0). Das ist konsistent mit der CM-Theorie und der supersingulären Struktur bei p = 3. Ob diese Aussage für alle p ≡ 1, 7 mod 12 gilt, ist über den getesteten Bereich hinaus Vermutung.

06 — Ext-Berechnungen / ANSS E₂-Seite (Phase 2)

Drei Macaulay2-Modelle wurden als Näherungen für Teile der Adams-Novikov E₂-Seite bei p = 3 berechnet.

Modell A: Truncated BP-Kooperation

Ring: A = ℤ/3[v₁, t₁] / (t₁³ - v₁²\cdott₁) |v₁| = |t₁| = 4 Betti-Tabelle (freie Auflösung, s = 0\dots8): 0 1 2 3 4 5 6 7 8 total: 1 2 2 2 2 2 2 2 2 3: . 2 . . . . . . . \leftarrow 2 Generatoren aus t₁ 6: . . 1 . . . . . . 10: . . 1 . . . . . . \leftarrow Ext² 13: . . . 2 . . . . . 16: . . . . 1 . . . . 20: . . . . 1 . . . . \leftarrow v₁-periodisch Hilbert-Serie: T¹² / (1-T⁴)² => Zwei v₁-periodische Familien \cdot Periode 4 = |v₁| bei p=3 => Erste Klasse in Grad 12 (entspricht beta₁-Bereich in der Literatur)

Modell B: v₁-invertierter Ring

Betti: 1, 3, 3, 1 (Poincaré-Dualität sichtbar) => v₁-periodischer Ext ist endlich-dimensional

Modell C: Lambda-Algebra (Steenrod-Approximation)

Generatoren: λ₀(Gr 1), λ₁(Gr 5), λ₂(Gr 9), λ₃(Gr 13) Betti: s=0:1 s=1:4 s=2:11 s=3:32 s=4:93 s=5:269 s=6:780 s=7:2260 => Exponentielles Wachstum, konsistent mit Komplexität der ANSS E₂-Seite

Grenzen. Das tatsächliche BP_*BP-Hopf-Algebroid ist komplexer als alle drei Modelle. Die Berechnungen sind intern konsistent und qualitativ korrekt, aber nicht identisch mit dem echten E₂-Term aus Miller-Ravenel-Wilson (1977). Sie sind Approximationen, keine exakten Reproduktionen.

07 — Lean 4 Formalisierungen (Phase 3)

Vier .lean-Dateien wurden neu geschrieben und erfolgreich gebaut (Lean 4.30.0-rc2 + vollständiges Mathlib, 2722 Jobs). Alle liegen auf dem Projektstick.

Verifizierte Strukturen

-- ChromaticArith_WittIso.lean #check @WittVector.frobenius -- WittVector.frobenius : WittVector p R →+* WittVector p R ✓ #check @WittVector.verschiebung -- WittVector.verschiebung : WittVector p R →+ WittVector p R ✓ #check @WittVector.teichmuller -- teichmuller : R →*₀ WittVector p R ✓ -- ChromaticArith_FGL.lean noncomputable def honda_h1 : PowerSeries (ZMod p) := (p : ZMod p) • PowerSeries.X + PowerSeries.X ^ p theorem honda_h1_leading_coeff : (PowerSeries.coeff (ZMod p) p) (honda_h1 p) = 1 -- ✓ bewiesen -- ChromaticArith_ANSS.lean #eval v1_degree 3 -- 4 ✓ #eval v2_degree 3 -- 16 ✓ #eval v3_degree 3 -- 52 ✓

Fehlende Formalisierungen in Mathlib

Nicht vorhanden: FormalGroupLaw als eigenständiger Typ. PadicInt.algEquivWittVector (der Isomorphismus W(𝔽_p) ≅ ℤ_p). Der Lazard-Ring als universeller Koeffizientenring formaler Gruppengesetze. Lubin-Tate-Deformationsräume. — Diese Lücken markieren präzise, was in der Mathematikformalisierungsgemeinschaft noch aussteht. Formalisierung macht sichtbar, was tatsächlich verstanden ist und was nur als »bekannt« gilt.

Vorhanden im lokalen MathProject

StandardOneDimIsocrystal und isocrystal_classification (Dieudonné-Manin für n=1) sind bereits bewiesen — eine Brücke von Witt-Vektoren zu Isocrystallen, die strukturell in der Nähe der chromatischen Konstruktionen liegt.

08 — Synthese und Hypothesen (Phase 4)

qwen3:235b-a22b (lokal, 142 GB) analysierte alle Berechnungsergebnisse zusammen mit Literaturpassagen aus dem LanceDB-Index. Fünf mathematische Kernfragen wurden beantwortet.

Kette: a₃(Δ) → Höhe → Deformationsraum → tmf

a₃(Δ) = 252 = 4·9·7, daher v₃(252) = 2. Supersinuläre elliptische Kurven bei p = 3 haben formale Gruppe der Höhe 2 (eindeutige ss-j-Invariante: j = 0). Der Lubin-Tate-Deformationsraum für Höhe 2 bei p = 3 ist Spf(W(𝔽₉)[[u₁]]), wobei W(𝔽₉) ≅ ℤ₃[ζ₈]. Die Morava E-Theorie E₂ hat π_*(E₂) = W(𝔽₉)[[u₁]][u, u⁻¹]. tmf_{(3)} entsteht als homotopy fixed points (E₂)^{hG₂}.

Die Verbindung v₃(a₃) = 2 → Höhe 2 ist plausibel aber nicht kausal — v₃ misst 3-adische Nähe, Höhe ist eine Eigenschaft der formalen Gruppe. Die Koinzidenz ist mathematisch interessant, aber keine bewiesene Äquivalenz.

Hypothese 1 — Bewertung und chromatische Höhe

v_p(a_p(Δ)) = k > 0 impliziert chromatische Höhe h = k. Im untersuchten Fall: v₃(252) = 2, also h = 2. Hypothese, kein bewiesener Satz. Über den getesteten Bereich hinaus nicht verifiziert.

Hypothese 2 — Supersinulärer Locus und Deformationsraum

Für Primzahlen p, bei denen j = 0 die einzige supersinuläre j-Invariante ist (gilt für p = 2, 3, 5, 7, 11), ist der universelle Deformationsraum der formalen Gruppe Spf(W(𝔽_{p²})[[u₁]]). Für p=3 strukturell korrekt (Lubin-Tate 1965). Allgemeine Form: im Wesentlichen bekannt, hier numerisch exemplifiziert.

09 — LLM-Verifikation und Meta-Befund

deepseek-r1:70b wurde als kritischer Verifikator eingesetzt. Es erhielt die qwen3:235b-Synthese und sollte mathematische Fehler finden.

deepseek-r1 hat selbst einen Fehler gemacht. Es markierte die korrekte Berechnung [3]²(x) mod 3 = x⁸¹ als falsch — mit der Begründung, »zwei Iterationen von [3] sollten zu x⁹ führen«. Das ist falsch: jede Iteration erhöht den Exponenten um den Faktor p^h, nicht p. SageMath liefert x⁸¹ deterministisch. deepseek-r1 verwechselte Höhe-1-Logik mit Höhe-2-Verhalten.

Dieser Befund ist nicht spektakulär, aber instruktiv: ein Sprachmodell kann falsche Verifikationen produzieren, auch wenn es Chain-of-Thought verwendet. In mathematisch kritischen Kontexten bleibt deterministischer Code (SageMath, Macaulay2, Lean 4) der einzig verlässliche Prüfstein. LLMs sind hier Hypothesengeneratoren, keine Verifikatoren.

Die anderen Punkte von deepseek-r1 (v₃-Muster, Lean-Lücken, offene Forschungsfragen) waren qualitativ korrekt und nützlich.

10 — Beobachtungen

Was die Rechenwerkzeuge leisten

SageMath berechnet Frobenius-Spuren deterministisch; Macaulay2 löst exakte Betti-Zahlen über ℤ/3; Lean 4 weist maschinell nach, dass WittVector.frobenius ein Ringhomomorphismus ist. Diese Resultate haben keine Interpretation in sich — sie sind korrekte Antworten auf präzise gestellte Fragen. Der Wert liegt im Stellen der richtigen Frage.

Was die Sprachmodelle leisten

qwen3:235b verbindet Berechnungsergebnisse zu interpretierbaren Aussagen. Es formuliert die Kette von a₃(Δ) zum Deformationsraum in einer Sprache, die für mathematische Leser zugänglich ist. Ob dabei etwas über elaboriertes Pattern-Matching hinausgeht, ist offen — und es wäre unehrlich, so zu tun, als wäre das entschieden. Die nützlichste Funktion war Synthese, nicht Verifikation.

Die Lean-Lücke als epistemisches Signal

Dass FormalGroupLaw in Mathlib fehlt, ist kein rein technisches Defizit. Es zeigt, wo der Stand der Formalisierung ist: Witt-Vektoren, p-adische Zahlen, Kategorientheorie sind weit vorangetrieben; die Verbindungsstücke zur chromatischen Homotopietheorie — formale Gruppen, Lubin-Tate, Morava — nicht. Formalisierung macht sichtbar, was wirklich bewiesen ist im Gegensatz zu dem, was als »bekannt gilt«.

Zur Frage der Hierarchie

Die chromatische Filtration ordnet Spektren nach ihrer Periodizitätstiefe: Höhe 0 ist rational, Höhe 1 ist K-Theorie, Höhe 2 ist tmf-artig, und so fort. Diese Hierarchie hat eine gewisse strukturelle Ähnlichkeit zu Stratifikationen, die in anderen Kontexten auftauchen — von der Klassifikation semisimpler Lie-Algebren bis zu Dualitätstheorien. Ob das mehr als eine Analogie ist, bleibt offen. Es wäre eine Übertreibung, darin eine tiefere Einheit zu sehen; es ist aber kein Zufall, dass die mathematische Gemeinschaft diese Strukturen beständig interessant findet.

Lokale KI als Forschungswerkzeug

Das wichtigste praktische Ergebnis: die Kombination von CAS-Werkzeugen (SageMath, Macaulay2) mit formaler Verifikation (Lean 4) und semantischem Index (LanceDB) in einer vollständig lokalen Infrastruktur funktioniert. Die Ergebnisse sind reproduzierbar, alle Berechnungen sind auf dem Stick gespeichert. Was nicht funktioniert hat wie geplant: vollständig autonome LLM-Synthese ohne manuellen Eingriff. Die Modell-Verfügbarkeit (Ollama-Blockierungen, Thermal-Abschaltung) erforderte mehrfache Neustarts.

11 — Thermischer Zwischenfall und Management

Vorfall Das externe NVMe-Laufwerk (OWC Aura Pro IV, 3,84 TB, passiv gekühlt im Thunderbolt-Gehäuse) schaltete sich thermisch ab. Ursache: OLLAMA_MAX_LOADED_MODELS=3 und KEEP_ALIVE=30m führten dazu, dass qwen3:235b (132 GB) und deepseek-r1:70b (40 GB) gleichzeitig geladen wurden — 172 GB sequentiell vom externen NVMe. Das Laufwerk erreichte kritische Temperatur.

Fix Drei Werte in ~/.zshrc dauerhaft geändert:

OLLAMA_MAX_LOADED_MODELS: 3 \to 1 OLLAMA_NUM_PARALLEL: 2 \to 1 OLLAMA_KEEP_ALIVE: 30m \to 5m Backup: ~/.zshrc.bak_thermal

Empfehlung. qwen3:235b (132 GB) von TB5 auf die interne 2-TB-SSD migrieren — 1,3 TB Freiraum vorhanden. Dann entfällt jede thermische Belastung des externen Laufwerks beim Laden des Hauptmodells. TB5 verbleibt für Archive und seltener genutzte Modelle. Ergänzend: brew install smartmontools für präzises Temperatur-Monitoring.

SMART-Status nach Wiederanschluss: Verified. Keine beschädigten Sektoren. TB5 intakt.

12 — Literatur

Alle Texte lokal verfügbar. 8 PDFs als maschinenlesbarer Text extrahiert. Hazewinkel (gescannt) per Chandra OCR 2 erschlossen (Seiten 1–40).

1Ravenel, D.C. — Nilpotence and Periodicity in Stable Homotopy Theory (Orange Book, 2020). Princeton University Press, 1992. Frei verfügbar.
2Ravenel, D.C. — Complex Cobordism and Stable Homotopy Groups of Spheres (Green Book). AMS Chelsea, 2004. Frei verfügbar.
3Rezk, C. — Notes on the Hopkins-Miller Theorem. Contemp. Math. 220, AMS, 1998. Frei verfügbar.
4Lurie, J. — A Survey of Elliptic Cohomology. Abel Symposia 2007. Springer, 2009. Harvard DASH open access.
5Barthel, T. · Beaudry, A. — Chromatic structures in stable homotopy theory. arXiv:1901.09004.
6Goerss, P. · Henn, H.-W. · Mahowald, M. · Rezk, C. — A resolution of the K(2)-local sphere at the prime 3. arXiv:math/0204002.
7Behrens, M. — A modular description of the K(2)-local sphere at the prime 3. Topology 45 (2006). arXiv:math/0507184.
8Bauer, T. — Computation of the homotopy of the spectrum tmf. Geom. Topol. Monogr. 13 (2008). arXiv:math/0311328.
9Hazewinkel, M. — Formal Groups and Applications. Academic Press, 1978. Gescanntes Buch, OCR der Seiten 1–40 lokal verfügbar.

Arithmetic Chromaticity

01 — Motivation and Context

02 — Corpus Ingestion (Phase 0)

03 — Formal Group Laws (Phase 1a)

Formal group law F(x,y) explicit (h=1, p=3)

Lubin–Tate deformation space

04 — Supersingular Database (Phase 1b)

CM curve verification

05 — Frobenius, Hecke and v3-Patterns (Phase 1c)

Ramanujan-Δ and 3-adic valuations

v3-patterns by p mod 12

06 — Ext-Computations / ANSS E2-page (Phase 2)

Model A: Truncated BP-cooperation

Model B: v1-inverted ring

Model C: Lambda algebra (Steenrod approximation)

07 — Lean 4 Formalisations (Phase 3)

Verified structures (Lean 4.30.0-rc2 + Mathlib, 2722 build jobs)

Present in the local MathProject

08 — Synthesis and Hypotheses (Phase 4)

09 — LLM Verification and Meta-Finding

10 — Observations

What the computational tools deliver

What the language models deliver

The Lean gap as epistemic signal

On the question of hierarchy

Local AI as research tool

11 — Thermal Incident and Management

12 — Literature

01 — Motivation und Kontext

02 — Corpus-Ingestion (Phase 0)

03 — Formale Gruppengesetze (Phase 1a)

Formales Gruppengesetz F(x,y) explizit (h=1, p=3)

Lubin-Tate Deformationsraum

04 — Supersinuläre Datenbank (Phase 1b)

CM-Kurven-Verifikation

05 — Frobenius, Hecke und v₃-Muster (Phase 1c)

Ramanujan-Δ und 3-adische Bewertungen

v₃-Muster nach p mod 12

06 — Ext-Berechnungen / ANSS E₂-Seite (Phase 2)

Modell A: Truncated BP-Kooperation

Modell B: v₁-invertierter Ring

Modell C: Lambda-Algebra (Steenrod-Approximation)

07 — Lean 4 Formalisierungen (Phase 3)

Verifizierte Strukturen

Fehlende Formalisierungen in Mathlib

Vorhanden im lokalen MathProject

08 — Synthese und Hypothesen (Phase 4)

09 — LLM-Verifikation und Meta-Befund

10 — Beobachtungen

Was die Rechenwerkzeuge leisten

Was die Sprachmodelle leisten

Die Lean-Lücke als epistemisches Signal

Zur Frage der Hierarchie

Lokale KI als Forschungswerkzeug

11 — Thermischer Zwischenfall und Management

12 — Literatur

05 — Frobenius, Hecke and v₃-Patterns (Phase 1c)

v₃-patterns by p mod 12

06 — Ext-Computations / ANSS E₂-page (Phase 2)

Model B: v₁-inverted ring