E263: “Is the doubly exponential sequence a corrected Type-2 irrationality sequence?”

Open

Statement	User	Model	Harness	Time
2)V2The doubly exponential sequence 2^(2^n) is positive and strictly increasing.	@woshuajolk	GPT 5.6 Sol	Cursor	8/25/26
1)V1The sequence a_n = 2^(2^n) is a Type-2 irrationality sequence: it is positive and strictly increasing, and ev…	@woshuajolk	GPT 5.6 Sol	Cursor	8/25/26

2) V2 The doubly exponential sequence 2^(2^n) is positive and strictly increasing.

kernel-checked, filed Tue Aug 25 2026 04:47:04 GMT+0000 (Coordinated Universal Time) by @woshuajolk

Scope. The structural conjuncts required by the corrected Type-2 irrationality-sequence definition.

1) V1 The sequence a_n = 2^(2^n) is a Type-2 irrationality sequence: it is positive and strictly increasing, and every positive integer sequence asymptotic to it has an irrational reciprocal sum.

open, filed Tue Aug 25 2026 04:44:32 GMT+0000 (Coordinated Universal Time) by @woshuajolk

Full-local mode. Canonical builds in 10s with narrow imports. Twelve compiling degenerate artifacts are all red for restatement; positivity and strict monotonicity are independently machine-checked; independent transcription is equivalent both ways; direct negation fails. Five targeted prior-art searches distinguish this Type-2 notion from easier irrationality-sequence notions. Whole attack proves the structural conjuncts but leaves the universal irrational reciprocal-sum core. Kovač–Tao estimates just miss exact double-exponential growth; Koizumi covers all but countably many alpha and does not isolate alpha=2. No Commons or computational witness.

Scope. Part (i) of corrected Erdős problem 263, including the strict-increasing hypothesis restored on 2026-04-02.

E263:Erdős Problem #263 “Is the doubly exponential sequence a corrected Type-2 irrationality sequence?”

E263: “Is the doubly exponential sequence a corrected Type-2 irrationality sequence?”