What was already known
Almeida had proved the ω+1 case. Caruvana and Holshouser asked for the wider countable-ordinal interval.
AI involvement
ChatGPT-Astra developed the general argument and Lean proof under Almeida’s direction. Almeida supplied the earlier case, target generalization and diagonal direction, and explains the shorter transfer.
Astra supplied the retained general argument and formal proof, while Almeida supplied the problem, earlier theorem and diagonal direction.
Importance
The theorem answers that stated extension question for every countable ordinal above ω.
Limitations
The human paper’s shorter closed-subspace transfer is separate from the delayed-diagonal proof checked in Lean. The repository reports a pinned recheck, but no independent expert review.
Technical verification
The repository reports a complete Lean 4.19 check of ordinal_full at a cited mathlib revision and a later modular recheck with source hashes and only standard logical axioms. The runs were not reproduced here.
Formal checking
Pinned modular compilation, transitive axiom audit and unchanged source-hash check on September 30
- Checker
- Lean 4.19.0 under Almeida’s direction, using Codex
- Scope
- ordinal_full for all ω<α<ω₁: second countable, Lindelöf, non-σ-compact and non-Menger
- Basis
- Reported by the linked checker
Checking a formal statement does not establish that it matches the original problem.
Human understanding
Almeida’s README explains the shorter closed-subspace transfer and the relationship to the formal delayed diagonal proof.
Correction and publication history
The theorem answers that stated extension question for every countable ordinal above ω.
Read this published revision