AI Proof WatchKeep up with AI contributions

Sharp reset thresholds for bounded-response synchronization games with a sink

Ben Keene

For n≥2 and k≥1 with k=1 or n≤k+3, the largest shortest-reset-word length among n-state A_k automata with a fixed sink is M(n,k)=∑_{i=1}^{n−1}⌈i/k⌉. Alice chooses one letter per round and Bob replies with fewer than k letters, including the empty word; A_k means Alice can force a reset. In particular M(k+2,k)=k+2 and M(k+3,k)=k+4 for k≥2, and M(5,2)=6.

Sources for this record

What was already known

Lipin and Volkov studied the game and gave endpoint bounds and ceiling-sum lower-bound constructions. Their conjecture specifies the divisible case k∣n−1; it does not assert the ceiling-sum extension for all pairs.

AI involvement AI-led

Ben Keene designed and ran the research pipeline and approved its scope. Claude Opus wrote the proof of record and most formal proofs; GPT-6 Astra supplied independent proofs and adversarial reviews. Keene re-entered some model proofs with explicit binders. The documented human direction supports AI-led work rather than task-only autonomy.

Importance Modest

Adds sharp bounds for a limited parameter range of the sink-game problem, with the wider conjecture unresolved. The endpoint bounds and lower-bound framework retain their earlier human credit.

Limitations

The result concerns automata with a sink and the stated bounded-response game. It does not settle the general reset-threshold conjecture beyond k=1 or n≤k+3. The formal target uses an inductive winning-position predicate; its equivalence to a history-dependent winning strategy is explained in prose. The later CiE conference chapter was not available in full text, so novelty is assessed against the January preprint and the scoped searches. Human approval of the pipeline is not an independent mathematical review.

Technical verification Formal (Lean)

The exact-commit Palomar preflight completed on 29 October. The package records Lean builds, axiom audits, kernel replay and statement comparison for the upper and lower bounds, including the five-state case. Only propext, Classical.choice and Quot.sound are permitted. These are source-reported checks of the formal game statements; the prose bridge from the inductive predicate to explicit strategies remains separate.

Formal checking

The exact-commit Palomar preflight completed on 29 October. The package records Lean builds, axiom audits, kernel replay and statement comparison for the upper and lower bounds, including the five-state case. Only propext, Classical.choice and Quot.sound are permitted. These are source-reported checks of the formal game statements; the prose bridge from the inductive predicate to explicit strategies remains separate.

Checker
Palomar mechanical verifier
Scope
For n≥2 and k≥1 with k=1 or n≤k+3, the largest shortest-reset-word length among n-state A_k automata with a fixed sink is M(n,k)=∑_{i=1}^{n−1}⌈i/k⌉. Alice chooses one letter per round and Bob replies with fewer than k letters, including the empty word; A_k means Alice can force a reset. In particular M(k+2,k)=k+2 and M(k+3,k)=k+4 for k≥2, and M(5,2)=6.
Basis
Reported by the linked checker
Evidence source

Checking a formal statement does not establish that it matches the original problem.

Human understanding Few

Few is the default when evidence for a higher level is insufficient. The source records Keene’s scope and correspondence review, but does not document a completed human explanation of the central bound argument. Model reviews alone do not establish human understanding.

Correction and publication history