{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R814",
  "content_hash": null,
  "slug": "twnfa-claim-bounded-fixed-alphabet-replay",
  "type": "claim",
  "title": "The separator and encoded NFAs pass 1,385,824 unique finite inputs",
  "summary": "Exact enumeration checks 1,053,250 matrix-cell separator inputs and 332,574 canonical matrix words. Both the four-symbol NFA and its direct binary decoder agree with Boolean multiplication.",
  "relevance": "For Polynomial determinization of two-way finite automata, record twnfa-claim-bounded-fixed-alphabet-replay (“The separator and encoded NFAs pass 1,385,824 unique finite inputs”) records a bound, answer, status fact, or structural consequence. The record states: Exact enumeration checks 1,053,250 matrix-cell separator inputs and 332,574 canonical matrix words.",
  "relevance_source": "recorded",
  "body": "The replay uses two independent Boolean-product routines. One evaluates the three nested loops in the definition. The other composes integer row masks. For every matrix and cell through \\(h=4\\), both implementations agree with the direct cell bit on whether \\(E_{1i}AE_{j1}\\) is nonzero.\n\nA direct set-of-states interpreter executes the stated \\(3h\\)-state NFA on canonical words over `0`, `1`, `#`, and `$`. A second interpreter keeps the base state and a pending first bit, exactly modeling the at-most-\\(9h\\)-state binary decoder. Both answers are compared with Boolean matrix multiplication. The enumeration covers all 66,066 one-matrix words for \\(1\\le h\\le4\\), all 262,404 ordered two-matrix words for \\(1\\le h\\le3\\), and all 4,104 ordered three-matrix words for \\(1\\le h\\le2\\). Every comparison passes. The stable output digest is recorded in the artifact.\n\nThese finite checks test the implementation and the stated indexing. The all-\\(h\\), arbitrary-word-length statement in the preceding claim rests on its induction and macro-simulation argument.",
  "status": "supported",
  "evidence_grade": "computational",
  "scope": {
    "kind": "bounded",
    "statement": "all separator cases through h=4, one-block encodings through h=4, two-block encodings through h=3, and three-block encodings through h=2",
    "bounds": {
      "separator_h": {
        "min": 1,
        "max": 4
      },
      "one_block_h": {
        "min": 1,
        "max": 4
      },
      "two_block_h": {
        "min": 1,
        "max": 3
      },
      "three_block_h": {
        "min": 1,
        "max": 2
      }
    },
    "exhaustive": true
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "source_only",
    "kind": "claim",
    "citation": {
      "locator": "Exact 2026-07-28 run of tools/two_way_nfa_fixed_alphabet_replay.py, with source and stdout hashes in the linked artifact record"
    },
    "missing": [
      "source",
      "command",
      "runtime",
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": null,
    "locator": "Exact 2026-07-28 run of tools/two_way_nfa_fixed_alphabet_replay.py, with source and stdout hashes in the linked artifact record"
  },
  "models": [],
  "relations": [
    {
      "slug": "R810",
      "title": "Exact fixed-alphabet one-way-liveness replay",
      "object_type": "artifact",
      "relation": "evidences",
      "direction": "incoming"
    },
    {
      "slug": "R816",
      "title": "The one-way-liveness bound transfers to a fixed binary alphabet",
      "object_type": "claim",
      "relation": "tests",
      "direction": "outgoing"
    },
    {
      "slug": "R817",
      "title": "Two singleton contexts isolate any Boolean-matrix entry",
      "object_type": "claim",
      "relation": "tests",
      "direction": "outgoing"
    },
    {
      "slug": "two-way-nfa-polynomial-determinization",
      "title": "two way nfa polynomial determinization",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}