{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R160",
  "content_hash": null,
  "slug": "cpcrt-claim-odd-reset-upper-bound",
  "type": "claim",
  "title": "Every odd order has a quadratic reset word",
  "summary": "For odd n, an explicit word of length n(n-1)/2 synchronizes the automaton.",
  "relevance": "For Reset threshold of the cyclic pair-compression automaton, record cpcrt-claim-odd-reset-upper-bound (“Every odd order has a quadratic reset word”) records a bound, answer, status fact, or structural consequence. The record states: For odd n, an explicit word of length n(n-1)/2 synchronizes the automaton.",
  "relevance_source": "recorded",
  "body": "Write \\(n=2m+1\\) and define\n\\[\nW_n=b\\left(\\prod_{j=0}^{m-2}a^{2j+1}b\\,a^{n-2j-1}b\\right)ab,\n\\]\nwhere the product is read with increasing \\(j\\). After the first \\(b\\), the active set is \\(\\{0,2,\\ldots,2m\\}\\). After the block \\(a^{2j+1}b\\) in pair \\(j\\), it is \\(\\{2j,2j+2,\\ldots,2m-2\\}\\). After the following block \\(a^{n-2j-1}b\\), it is\n\\[\n\\{0,2,\\ldots,2(m-j-2)\\}\\cup\\{2m\\}.\n\\]\nThe formulas follow by reducing the displayed even states modulo \\(2m+1\\) and applying \\(b\\). The final \\(ab\\) sends \\(\\{0,2m\\}\\) to \\(\\{0\\}\\). The word contains \\(2m=n-1\\) copies of \\(b\\). Its powers of \\(a\\) sum to \\((m-1)n+1=m(2m-1)\\), so its length is \\(m(2m+1)=n(n-1)/2\\).",
  "status": "established",
  "evidence_grade": "reproduced",
  "scope": {
    "kind": "universal",
    "statement": "the automata A_n for every odd integer n at least 3"
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "source_only",
    "kind": "claim",
    "citation": {
      "url": "https://doi.org/10.4213/rm10005e",
      "locator": "Direct active-set calculation in this record; construction checked through odd n=101 in cpcrt-artifact-exact-sweep"
    },
    "missing": [
      "source",
      "command",
      "runtime",
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://doi.org/10.4213/rm10005e",
    "locator": "Direct active-set calculation in this record; construction checked through odd n=101 in cpcrt-artifact-exact-sweep"
  },
  "models": [],
  "relations": [
    {
      "slug": "R159",
      "title": "The candidate odd threshold is n(n-1)/2",
      "object_type": "claim",
      "relation": "supports",
      "direction": "outgoing"
    },
    {
      "slug": "cyclic-pair-compression-reset-threshold",
      "title": "cyclic pair compression reset threshold",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}