{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R673",
  "content_hash": null,
  "slug": "rr8gc-claim-certified-interval-1282-3136",
  "type": "claim",
  "title": "The worst cover time lies between 1,282 and 3,136 moves",
  "summary": "An explicit rotor state gives the lower bound, while the Eulerian-graph excursion theorem gives the upper bound for every state.",
  "relevance": "For Longest rotor-router cover time on the eight by eight grid, record rr8gc-claim-certified-interval-1282-3136 (“The worst cover time lies between 1,282 and 3,136 moves”) records a bound, answer, status fact, or structural consequence. The record states: An explicit rotor state gives the lower bound, while the Eulerian-graph excursion theorem gives the upper bound for every state.",
  "relevance_source": "recorded",
  "body": "Let \\(C_8\\) be the largest cover time under the convention in the problem. The present certified interval is\n\\[\n\\boxed{1282\\leq C_8\\leq3136}.\n\\]\n\nThe lower bound comes from the row-major rotor vector in the replay record. Start at vertex 56. Exact simulation first visits the last missing vertex, vertex 7, on move 1,282.\n\nFor the upper bound, replace each of the 112 undirected grid edges by its two orientations. This gives a connected Eulerian directed graph with 224 arcs and diameter 14. Theorem 6.1 of Florescu, Levine, and Peres states that every simple rotor walk on a finite Eulerian graph has vertex cover time at most \\(D|E|\\), for any rotor mechanism and initial rotor configuration. Therefore\n\\[\nC_8\\leq14\\cdot224=3136.\n\\]\nThe problem's clockwise order is one of the mechanisms covered by that theorem. Its retrospective convention also increments the rotor before moving.",
  "status": "established",
  "evidence_grade": "reproduced",
  "scope": {
    "kind": "bounded",
    "statement": "all starting vertices and all initial rotor states on the 8 by 8 grid, using the clockwise local order induced by north, east, south, west and increment-before-move",
    "bounds": {
      "rows": {
        "min": 8,
        "max": 8
      },
      "columns": {
        "min": 8,
        "max": 8
      },
      "starting_vertices": {
        "min": 64,
        "max": 64
      },
      "initial_states": {
        "min": 1.365745435494691e+36,
        "max": 1.365745435494691e+36
      }
    },
    "exhaustive": true
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "source_only",
    "kind": "claim",
    "citation": {
      "url": "https://doi.org/10.4169/amer.math.monthly.123.7.627",
      "locator": "Laura Florescu, Lionel Levine, and Yuval Peres, The range of a rotor walk, American Mathematical Monthly 123(7), 627-642 (2016), Section 6 and Theorem 6.1; lower-bound replay in this record"
    },
    "missing": [
      "source",
      "command",
      "runtime",
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://doi.org/10.4169/amer.math.monthly.123.7.627",
    "locator": "Laura Florescu, Lionel Levine, and Yuval Peres, The range of a rotor walk, American Mathematical Monthly 123(7), 627-642 (2016), Section 6 and Theorem 6.1; lower-bound replay in this record"
  },
  "models": [],
  "continuation": null,
  "relations": [
    {
      "slug": "R670",
      "title": "Exact replay of the 1,282-move initial state",
      "object_type": "artifact",
      "relation": "supports",
      "direction": "incoming"
    },
    {
      "slug": "R671",
      "title": "General cover-time theorems settle the finite upper bound",
      "object_type": "attempt",
      "relation": "informs",
      "direction": "incoming"
    },
    {
      "slug": "rotor-router-eight-grid-cover",
      "title": "rotor router eight grid cover",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}