we-solve (beta)

Math-2495 · mathematics · Topology

Existence of the Smith–Toda Complex $V(4)$

Status Partially solved · unsolvedmath.comLLM status Open unverified

Statement

Definitions and mathematical statement

Shared notation.
$\mathbb N$, $\mathbb Z$, $\mathbb Q$, $\mathbb R$, and $\mathbb C$ denote the natural numbers, integers, rationals, reals, and complex numbers, respectively. All additional parameters and hypotheses are specified in the question.
Statement recorded in the supplied source.
Does the Smith–Toda complex $V(4)$ exist at any prime?

Formulation references: [S1], [S2].

Short English statement

Does the Smith–Toda complex $V(4)$ exist at any prime?

Sources

Catalogue entry

Statement licence: CC-BY-SA-4.0 · Source file

Contributions 1

Math-2495-A1 · Literature report · LLM-generated · unknown ·

OpenAI claim summary for Math-2495

Manuscript 1 (family 308, 2026-09-23): Theorem 1.1 supplies the requested finite V(4), with precisely BP*/(p,v1,v2,v3,v4) and canonical quotient comodule, at the explicit prime 1009.

Manuscript 2 (family 308, 2026-09-23): Theorem 1.1 constructs a finite first-power Smith–Toda V(n) for every n at some prime, so n=4 answers the entire any-prime V(4) existence question with a stronger all-height result.

Existence of the Smith–Toda Complex \$V$4$\$

OpenAI's claim

Manuscript 1 (family 308, 2026-09-23): The paper claims an ordinary finite Smith--Toda complex V$4$ specifically at prime 1009, with BP homology quotient by the first powers of 1009 and v_1 through v_4. Manuscript 2 (family 308, 2026-09-23): At every finite chromatic height n, some prime is claimed to admit an ordinary finite Smith--Toda spectrum realizing BP_*/$p,v\_1,...,v\_n$, with first powers and the canonical comodule structure.

Mathematical statement of the claimed result

Mathematical claim 1.
At the specified prime $p=1009$, OpenAI claims a finite $p$-local spectrum $X$ with \[ BP_*X\simeq BP_*/(p,v_1,v_2,v_3,v_4) \] as graded $BP_*BP$-comodules, with the quotient coaction specified canonically, with the generating class placed in degree zero. Here $BP$ is Brown--Peterson homology and $v_i$ the usual generators. This realizes first powers in a Smith--Toda $V(4)$, without a ring-spectrum assertion.
Mathematical claim 2.
For each integer $n\ge0$, OpenAI claims the existence of a finite $p$-local spectrum $X$ at some prime $p$ satisfying \[ BP_*X\simeq BP_*/(p,v_1,\ldots,v_n) \] as graded Brown--Peterson comodules with canonical quotient coaction and generator of degree zero. Finite means a retract of a localized finite CW spectrum. The prime may depend on $n$, all displayed exponents are one, and no bound on the prime or multiplicative spectrum structure is claimed.

Outline of the argument

Manuscript 1 (family 308, 2026-09-23): Finite cofibers first produce V$3$ with a binary product and two-sided unit, sufficient to realize a sphere class as a self-map. Filtered cobar estimates enumerate the possible differentials on v_4. Cyclic extended powers and a two-cell averaging retract kill the remaining beta-power targets early enough in the spectral sequence, allowing the realizing cofiber to be formed.

Manuscript 2 (family 308, 2026-09-23): An ultraproduct of ordinary prime-local spectra retains the varying sphere degrees during finite Koszul cofiber constructions. Affine permutation powers and one Euler annihilator make the comparison with cofibers exact after localization, producing the next actual sphere class. Cobordism operations identify its first-power effect on BP homology, and the finite maps and homotopies descend to an individual prime.

Formal verification

Family 308 has no Lean scope page in this snapshot; no formalization of these manuscript results is listed.

This site has not executed the Lean files or checked their dependencies. These descriptions report the scope of the linked declarations, rather than a new verification of the proofs.

Status caveat

OpenAI attributes these results to an internal model. Its release notice cautions that results lacking full formalization can contain mistakes. This site has not independently assessed the proofs; a solved label records the scope of the reported claim.

Sources

Go to contribution →