{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R482",
  "content_hash": null,
  "slug": "lyndon8-claim-certified-interval-49-94",
  "type": "claim",
  "title": "The certified interval is 49 to 94",
  "summary": "A Boolean satisfiability computation rules out length 48, while a replayable 94-bit word covers all 30 targets.",
  "relevance": "For Shortest superstring of the binary Lyndon words of length eight, record lyndon8-claim-certified-interval-49-94 (“The certified interval is 49 to 94”) records a bound, answer, status fact, or structural consequence. The record states: A Boolean satisfiability computation rules out length 48, while a replayable 94-bit word covers all 30 targets.",
  "relevance_source": "recorded",
  "body": "Let \\(L_8\\) be the set of the 30 binary Lyndon words of length eight, and let \\(m\\) be the minimum length of a word containing every member of \\(L_8\\). The current certificates give\n\\[\n49\\leq m\\leq94.\n\\]\n\nFor the lower endpoint, fix a proposed length \\(N\\). Introduce one Boolean variable for each position of the proposed superstring. For every \\(w\\in L_8\\), assert a disjunction over its \\(N-7\\) possible starting positions, with eight bit equalities in each disjunct. This formula is satisfiable exactly when a length-\\(N\\) common superstring exists. Z3 5.0.0 returns `unsat` at \\(N=48\\), which also rules out every shorter length because a shorter superstring can be padded to length 48.\n\nFor the upper endpoint, view each required word as an edge in the order-seven binary de Bruijn graph. The 30 required edges form 11 weak components, each a directed path. Spelling those paths gives blocks of lengths\n\\[\n14,12,10,11,10,8,9,8,9,8,8.\n\\]\nAn exact Held-Karp computation over these 11 blocks finds a shortest block-preserving merge of length 94. One such word is\n\\[\n\\texttt{0000000111111100000101111100001001111010000110111100010101110001100100101101100011101100110101}.\n\\]\nThe artifact regenerates all targets and checks every containment directly. The interval remains open. In particular, the 94-bit construction is optimal only within the stated block-preserving family.",
  "status": "established",
  "evidence_grade": "reproduced",
  "scope": {
    "kind": "bounded",
    "statement": "binary words containing every binary Lyndon word of length 8 as a contiguous factor",
    "bounds": {
      "alphabet_size": {
        "min": 2,
        "max": 2
      },
      "required_word_length": {
        "min": 8,
        "max": 8
      },
      "required_words": {
        "min": 30,
        "max": 30
      },
      "certified_superstring_length": {
        "min": 49,
        "max": 94
      }
    },
    "exhaustive": false
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "source_only",
    "kind": "claim",
    "citation": {
      "url": "https://doi.org/10.1016/0012-365X(78)90002-X",
      "locator": "Lower endpoint reproduced by lyndon8-artifact-unsat-at-48; upper endpoint reproduced by lyndon8-artifact-component-superstring"
    },
    "missing": [
      "source",
      "command",
      "runtime",
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://doi.org/10.1016/0012-365X(78)90002-X",
    "locator": "Lower endpoint reproduced by lyndon8-artifact-unsat-at-48; upper endpoint reproduced by lyndon8-artifact-component-superstring"
  },
  "models": [],
  "relations": [
    {
      "slug": "R480",
      "title": "Boolean unsatisfiability certificate at length 48",
      "object_type": "artifact",
      "relation": "evidences",
      "direction": "incoming"
    },
    {
      "slug": "R479",
      "title": "Exact 11-block Held-Karp construction",
      "object_type": "artifact",
      "relation": "evidences",
      "direction": "incoming"
    },
    {
      "slug": "R481",
      "title": "The FKM construction addresses a larger target family",
      "object_type": "attempt",
      "relation": "informs",
      "direction": "incoming"
    },
    {
      "slug": "length-eight-lyndon-superstring",
      "title": "length eight lyndon superstring",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}