Adversarial synchronization: the reset bound m(n-2)+1 is attained at m=3

The bound m(n-2)+1 of arXiv:2601.18362 Proposition 3.9 is ATTAINED at m = 3 for n = 3,...,9: an n-state 3/omega-automaton with reset threshold exactly 3n-5

Question 3 of arXiv:2601.18362 is FALSE – not every 3/omega-automaton with n states has a reset word of length 3n-6; counterexample at n = 3,...,9 in Lean and n = 10 in C

The same answer stated about the GAME and about WORDS rather than about a solver: Alice has a winning strategy in the 3/omega-game (inductive definition), and no word over the alphabet of length at most 3n-6 resets the automaton

The source's own printed values recomputed from its definitions: rt(Fₙ) = 2n-3 with Alice winning its 2/omega-game; rt(Cₙ) = (n-1)² with mlev(Cₙ) = binom(n,2); rt(Lᵏₘ) in both closed forms with Lᵏₘ in Aₖ minus Aₖ₊₁; Eₙ in Aₙ₋₁ minus Aₙ; and both Remarks after Theorem 3.6

The Cerny function of 3-state m/omega-automata over alphabets of at most 3 letters: f₃(3,m) = 2, 3, 4, 4, 4 for m = 1..5, so Proposition 3.9 is tight at m = 1, 2, 3 and not at m >= 4

Negative controls: a non-synchronizing automaton on which Bob wins every m/omega-game; a synchronizing automaton that is not a 3/omega-automaton; reset-length claims refuted one too high and one too low; the m = 1 case matching the source's C_(Aₒmega)(n) = n-1; and a falsifiability control on the certificate machinery

The reset threshold of each tight witness stated entirely about WORDS: an explicit reset word of length exactly 3n−5 for n = 3,…,9, plus (cited, not re-proved) that no shorter word resets

The reset words all have the block shape Proposition 3.9's proof predicts: the unique non-permutation letter has deficiency 1 and occurs exactly n−1 times, at positions 0,3,…,3(n−2)

The bound m(n−2)+1 of arXiv:2601.18362 Prop. 3.9 is NOT attained at m = 4 when n = 4, over every alphabet GIVEN the classification of the reset-threshold-9 classes (the classification is the nineList hypothesis, discharged externally; see as-13 for the conditional theorem stated correctly): f(4,4) = 8 < 9. Every one of the 24 isomorphism classes of 4-state automata of reset threshold 9 loses the 4/ω-game (and the 5/ω-game), and there is a 4-state 4/ω-automaton of reset threshold 8

f(n,4) ≥ 4(n−2) for n = 4,5,6,7 — an n-state automaton on which Alice wins the 4/ω-game, Bob wins the 3/ω-game, and whose reset threshold is exactly 4(n−2), one below Proposition 3.9's 4(n−2)+1

Complete Černý-function sweeps for m/ω-automata that the source never computed: f₃(5,m) = 4,6,9,12,13,15,15,15,16,16 for m = 1..10; f₄(5,4) = 12 < 13, complete over all alphabets of n−1 = 4 letters — the size at which the m = 3 bound *does* become attainable; and f₂(4,m) = 3,4,6,6,8,9 re-derived inside Lean over all 32 896 two-letter alphabets

Bob's side of the game, certified: a checked *trap* — a set of positions containing the start, containing no singleton, and closed under "Alice moves, Bob replies" — implies ¬ AliceWinsFrom A m A.full, the converse direction of Game.lean's bridge

The landed m = 3 witnesses are letter-minimal: no letter of W₅, W₆, W₇, W₈ can be deleted — every proper sub-alphabet fails to be a 3/ω-automaton, certified on Bob's side at n = 6. Same for the m = 4 witnesses E₆, E₇ at m = 4

Negative controls for the m = 4 layer: a synchronizing automaton that is not a 4/ω-automaton (with Bob's win certified); reset thresholds refuted one too high and one too low; the witnesses shown synchronizing; Proposition 3.9 respected strictly; the m = 3 witnesses shown to be 4/ω-automata but with the smaller reset threshold 3n−5; and the trap machinery shown falsifiable

The lower half of "3 is the level" restated about the game: for n = 3,…,9 Alice has no winning strategy in the 2/ω-game on the tight witness Wₙ, via an explicit checked trap for Bob — so boundₜightₘ3_game says "Alice wins at 3 and loses at 2" with no decision procedure in the statement

Bob's strategy on a tight witness is one letter: his reply table has exactly n-1 nonempty entries, each a single letter, sitting at exactly the n-1 pairs q,z that contain the state z missing from the image of the deficiency-1 letter — so Alice's winning region in the 2/ω-game is the n singletons plus those n-1 pairs, 2n-1 of 2ⁿ positions

Given the classification of the 4-state alphabets of reset threshold ≥ 9 (the 24 classes of nineList, stated as an explicit hypothesis), f(4,4) = 8: every four-state alphabet — any number of letters, any order, repetitions allowed — on which Alice wins the 4/ω-game has reset threshold ≤ 8, and E4 attains 8; same upper half at m = 5. Plus the game isomorphism that makes the quantifier possible: Alice's winning region transports along a relabelling of the states and a reindexing of the letters

Controls for the conditional form: deleting one of the 24 classes makes the classification hypothesis false (witnessed by the deleted alphabet); E4 does not relabel into the list; the Černý automaton 𝒞₄ does; and the review's count of 576 labelled 4-state alphabets of reset threshold 9 is reproduced inside Lean from nineList alone, all 576 with rt = 9, all 576 lost by Alice at m = 4

Zhu's binary family Fₙ (arXiv:2607.19675, Definition Z:2192) has reset threshold exactly 3n−5 for n = 4,…,10, and his other claims about it — wₙ = a^(n−2)b^(n−1)a^(n−2) resets to state 1, one-cluster with m = 2 and ℓ = n−2, strongly connected — hold as stated

Fₙ is not a 3/ω-automaton: Bob wins the 3/ω-game on Zhu's Fₙ for every n = 4,…,10, so attaining Lipin–Volkov's Proposition 3.9 value 3(n−2)+1 = 3n−5 does not imply that it is a 3/ω-automaton

The level of Fₙ in the m/ω-hierarchy is 2n−3: Bob wins at m = 2n−4 and Alice wins at m = 2n−3, for n = 4,…,8; at n = 4, 5, 6 Alice's win is certified as AliceWinsFrom

Controls: the reversed-orientation sibling of Fₙ has reset threshold 2n−3 for odd n (Zhu's Remark Z:2757, Gusev–Pribavkina) and is not synchronizing at all for even n = 4, 6, 8, 10, which the Remark does not say; the trap builder refuses F₄ at m = 5 where Alice wins, and the strategy-certificate builder refuses it at m = 4 where Bob wins; rt(F₆) is neither 12 nor 14; no word of length 3n−6 resets Fₙ for n = 4,…,8

The m = 4 witnesses' reset threshold stated entirely about WORDS: an explicit reset word of length exactly 4(n−2) for n = 4,…,7, plus (cited, not re-proved) that no shorter word resets — so Proposition 3.9's bound 4(n−2)+1 is missed by one, with no decision procedure in the statement

The m = 4 reset words are n−2 blocks of four with NO leading letter — the first block drops the image by two, each later block by exactly one — which is why the length is 4(n−2) and not Proposition 3.9's 4(n−2)+1

Proposition 3.9's bound m(n−2)+1 is ATTAINED at m = 3 for every n ≥ 3: the explicit n-state, (n−1)-letter automaton 𝒰ₙ = (0↦1) + the 3-cycles (0 1 j) is a 3/ω-automaton whose shortest reset word has length exactly 3n−5, proved for all n with no decision procedure in the statement

Question 3 of arXiv:2601.18362 is FALSE for every n ≥ 3: no word of length 3n−6 resets 𝒰ₙ, while 𝒰ₙ is a 3/ω-automaton

The level of 𝒰ₙ in the m/ω-hierarchy is exactly 3 for every n ≥ 3: Bob wins the 2/ω-game, proved by induction on Alice's inductive winning predicate rather than by a per-n trap certificate

Core.lean's independent decision procedures agree with the general theorems at n = 3,…,8: aliceWins (𝒰ₙ) 3 = true, resetThreshold (𝒰ₙ) = 3n−5, hasResetWord (𝒰ₙ) (3n−6) = false, and the transition tables are the ones the definition prints

3 is the least m for which 𝒰ₙ is an m/ω-automaton, by the solver: aliceWins (𝒰ₙ) 2 = false for n = 3,…,8 and mlev (𝒰ₙ) = 3 for n = 4,5,6

Negative controls: one 3-cycle replaced by a transposition gives reset threshold exactly 3n−6 yet is still a 3/ω-automaton; deleting one permutation makes the automaton non-synchronizing; a different admissible permutation choice reproduces 3n−5; the reset length refuted one too high and one too low; the automata are synchronizing

Within the Černý shape (one letter a: 0 ↦ 1 plus permutations — the shape of 𝒞ₙ, of the source's ℱₙ and of 𝒰ₙ), a synchronizing automaton always admits a word of length at most two that puts the mergeable pair back together after the first merge: the second merge is at most three letters after the first, never four

The class of as-U7 is not empty and contains the objects it is about: 𝒰ₙ is Černý-shaped (Uₑqₛhaped, [propext, Quot.sound]) and so is Core.lean's Černý automaton 𝒞ₙ (cernyₑqₛhaped)