# Timed scouts on a known-size ring **For every integer f > 0 and n ≥ 3, 2f + 2 agents suffice under this viewer's message-only fault rules.** This is a sufficient construction, not a claim of optimality. The executable viewer bounds n to 3–40 and f to 1–12 for practical display and replay; the argument below has no such upper bounds. ## Exact model There is one always-active black hole in an oriented synchronous ring. Home is safe, and all agents start there knowing n, f, the team IDs, and the shared round schedule. Number nodes by clockwise distance from home, 0 through n−1. These are relative coordinates; the algorithm does not need marked node IDs. Movement takes one edge per round. A round reads/writes locally, then moves. Entering the hole destroys any agent, including a Byzantine agent. At most f fixed agents are Byzantine. They must obey all movement, waiting, reading, and state-update instructions. At their own prescribed writing opportunity, they may omit their write or replace it with an attributed false claim that their current port-0 or port-1 neighbor is the hole. They cannot forge a completed-trip receipt, impersonate another ID, erase records, write remotely, refuse a trip, or survive the hole. Whiteboards persist. The adversary knows the entire execution and can choose each message adaptively. No assumption of a fixed omission or alternating-ports policy is needed. Ground truth is used only for destruction and validating whether a chosen warning is false, and by the verifier when checking the result. ## Protocol Partition IDs into f + 1 scouts S and f + 1 guards G. All scouts and guards read the same local home board at the scheduled assessment rounds. For d = 1, 2, …, n−1: 1. In increasing scout-ID order, assign each scout a slot of **2d + 1 rounds**. It walks d edges clockwise, d counterclockwise, then writes `RETURN_OK(d)` at home in the last round. Other agents wait at home. A destroyed scout's slot still runs to its public deadline. 2. After **all** slots, spend one separate assessment round at home. Read only authenticated `RETURN_OK(d)` records from this stage's scouts on the **home** board. Departures, warnings, and earlier-depth receipts do not enter this predicate. 3. If at least one such receipt exists, advance to d + 1. If none exists, every guard identifies clockwise coordinate d as the hole. 4. After identification, guards traverse the remaining path forever, reversing when their next edge would enter coordinate d. Knowing n lets each guard track its coordinate and recognize both boundaries. Exactly one scout moves during a mission. Guards learn nothing from the observer's displayed deaths or remote board contents. The successful and failed slots have the same fixed duration. Returned scouts wait through all other slots; no early receipt accelerates the next depth. ## Correctness for every f Let h be the clockwise distance from home to the actual hole. **Induction on safe depths.** Initially all agents are at safe home. Assume depths below d have been completed, with d < h. Every scout's complete trip uses only coordinates 0 through d, so every scout returns alive. The f + 1 scouts include at least one honest agent because there are at most f faults in the entire team. Its receipt is written before the assessment. No allowed Byzantine action can erase that receipt. Thus the assessment declares d safe, and all agents are again at home for the next stage. A safe depth is never declared to be the hole, regardless of any omissions or false warnings. **At depth h.** The induction ensures every scout is alive at home at the start of the stage. Each prescribed clockwise trip enters h, so all f + 1 scouts are destroyed. No scout returns, and no completed-trip receipt for h can be written. In particular, a false neighbor warning cannot masquerade as a receipt. All guards wait for all deadlines and then correctly identify h from their local board and the protocol's guarantee of an honest scout. **Survival.** All f + 1 guards waited at safe home throughout the search. At most f can be Byzantine, so at least one surviving guard is honest. Exactly f + 1 agents are lost, all scouts. Even if every faulty agent is a guard, an honest guard remains. **Perpetual exploration.** Deleting the identified hole leaves one path with n−1 vertices and n−2 edges. Each guard follows its edges, reflecting at the two endpoints. It visits every safe vertex during each period of length 2(n−2), never enters h, and repeats indefinitely. Therefore every safe node is visited infinitely often by at least one honest agent. **Termination and cost.** Identification occurs in exactly ``` T(h) = Σ[d=1..h] ((f + 1)(2d + 1) + 1) = h[(f + 1)(h + 2) + 1] ≤ (n − 1)[(f + 1)(n + 1) + 1] rounds. ``` Search uses exactly (f + 1)h² edge traversals. The deliberately simple design trades quadratic search time for a short proof under the restricted faults. The theorem also tolerates a faulty scout choosing to write its genuine receipt after an actual return; such a receipt can only certify a safe trip. The viewer's adversary alphabet remains the three choices requested above. ## What “every adversary” in the viewer means There are infinitely many adaptive adversary programs, but only finitely many message histories before this terminating search and the displayed patrol periods. The checker uses two explicit reductions, not random samples. **1. Exact message-state reduction for a fixed placement.** The only board records read by this protocol are `RETURN_OK` receipts. Erase all other records and observer-only logs/decision history. This changes no current or future movement, pending writing opportunity, deadline, or inference. The Rust checker executes every legal next action (omit, false port 0, false port 1, excluding a warning that would be true) from each reached reduced state. There is at most one writer per round. It checks that the resulting control states, agent states, and retained receipts are equal, then merges them. By induction, **every adaptive combination** of these choices is covered, including combinations that are never shown by the autoplay tour. The implementation performs the ordinary simulator transitions, not a separate formula-based animation. A failed equality check fails verification. **2. Scout-slot symmetry and inert guards.** For a fixed h, every scout follows the same trips in a different, fixed slot. All slots complete before the receipt predicate is read. For d < h, the predicate is true for *every* nonempty honest-scout subset; at h it is false for every subset. Relabeling which b scouts are faulty changes receipt IDs and times, but neither the assessment predicate nor anyone's route. Each faulty scout has the same number of legal message choices along these time-shifted trips. Guards never have a prescribed write, so their fault flags change neither a board nor a route. Their only relevant bound is that at least one is honest. Consequently it suffices to check b = 0, …, f faulty scouts, taking the first b as a representative and placing f−b faults among guards to check the minimum honest-guard count. The class represents exactly ``` C(f + 1, b) × Σ[g=0..f−b] C(f + 1, g) ``` fault placements, including teams with fewer than f actual faults. Summing classes gives Σ[k=0..f] C(2f + 2, k), exactly all permitted placements. The symmetry argument above is part of the proof; it is not a claim that the computer separately executes every labeled placement. Native tests also check all concrete placements for f ≤ 3 on a small ring to catch indexing errors in this reduction. For the selected n and f the verifier checks all **(n−1)(f+1)** classes. It checks correct identification, exactly f+1 losses, at least one honest survivor, every survivor's safe-node coverage, and identical position/next-move states one full patrol period apart. It checks two patrol periods; the reflection rule proves the infinite continuation. Testing finitely many parameters alone is not a proof for unbounded f; the correctness argument above supplies that proof. The coverage counter counts concrete message **histories**, not adversary programs. For a representative with x binary and y ternary writing choices, the class covers its placement multiplicity times 2^x·3^y histories. Counts use arbitrary-precision integers; large displayed totals are rounded in scientific notation. Exported results retain the exact exponents. Autoplay shows one varying-message representative per class. Frames may batch multiple simulated rounds for large cases, but every round and decision is retained for replay/export. **Stop** leaves an explicitly partial result. Changing n or f requires starting a new verification. Verification runs in a worker so the controls remain responsive. ## Reproduce the checks ``` npm run build npm test node scripts/verify.mjs 10 1 ``` The last command checks the same compiled Wasm as the site and writes `verification/n10-f1.json`. The browser's **Verify & autoplay** button computes fresh results; it does not substitute a precomputed success indicator. This construction does **not** establish the same bound for arbitrary Byzantine movement, forged safety records, erasable boards, asynchronous timing, or an intermittently active gray hole. Those are different models from the rules in this viewer and from the broader research draft.