Proved
Positive-level one-cluster theorem reported ↗
Synchronizing, unique a-cycle, least level ℓ ≥ 1.
Source dated Jul 22, 2026 · Observed Oct 14, 2026
Theorem · version 1
Relative extending words on the unique cycle
Statement
Under the positive-level one-cluster hypotheses, for every nonempty proper S ⊂ C there is a word w with |w| ≤ n such that .
Assumptions
- Letters act on the right; (wa^ℓ)⁻¹ denotes a set preimage, not an inverse transition function. The empty and whole-cycle subsets are excluded.
Evidence
Source reports
Connections
In this problem · publication v2 · Selected context
Černý synchronization conjecture →
Supporting result · Proved
Relationship not independently reviewed. This concerns its use in this problem.
In this problem · publication v4
Černý synchronization conjecture →
Supporting result · Proved
Relationship not independently reviewed. This concerns its use in this problem.
Sources
The Černý Conjecture for One-Cluster Automata via Annular Spectral Descent →
- Main theorem and relative-extending-word result → · Original passage ↗
Recorded wording
For a synchronizing one-cluster automaton with n states, cycle length m and least level ℓ ≥ 1, the source proves the bound (m−1)(n−1)+mℓ ≤ (n−1)² and the stated relative-extension property.
paraphrase · Linked proof prose is not republished. Any copied graph data is CC0, as specified by its archive.
Yinfeng Zhu · Preprint · Publication date Jul 22, 2026
Source-reported results and external checks are separate from independent OpenMath assessment.
Revision & attribution
Source revision: v1. Observed Oct 14, 2026.
Zhu reports obtaining the proof through interaction with OpenAI Codex using GPT-5.6 Sol in ultra mode and verifying the argument himself.
History
Statement versions
Statement versions and problem publication versions are separate. A new publication can update context or sources while retaining the same statement.
Assessment history · 1
Assessments retained in these publication records. Earlier statement versions retain their own source histories.
Proved
Positive-level one-cluster theorem reported ↗
Synchronizing, unique a-cycle, least level ℓ ≥ 1.
Source dated Jul 22, 2026 · Observed Oct 14, 2026 · Source passage →
Record details
- Claim ID
- claim-cerny-relative-extension
- Statement version
- 1
- SHA-256
- ca45862df06c945a445a4c4f81aae27a3ef8d09add0311e9a61eb200b91d7957