{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R810",
  "content_hash": null,
  "slug": "twnfa-artifact-fixed-alphabet-exact-replay",
  "type": "artifact",
  "title": "Exact fixed-alphabet one-way-liveness replay",
  "summary": "A deterministic standard-library Python program checks singleton matrix contexts and interprets both the 3h-state four-symbol NFA and its at-most-9h-state binary decoder.",
  "relevance": "For Polynomial determinization of two-way finite automata, record twnfa-artifact-fixed-alphabet-exact-replay (“Exact fixed-alphabet one-way-liveness replay”) supplies evidence or a replay used to check the packet. The record states: A deterministic standard-library Python program checks singleton matrix contexts and interprets both the 3h-state four-symbol NFA and its at-most-9h-state binary decoder.",
  "relevance_source": "recorded",
  "body": "The program represents every Boolean matrix as a row-major integer. It compares a dense Boolean product, an integer-row-mask product, and direct cell extraction for the separator identity. Separate transition interpreters read the canonical four-symbol encoding and its uniform binary image, then compare both answers with the matrix-product oracle.\n\nThe default command enumerates all dimensions and word lengths stated in the bounded computation claim. It uses exact integer and Boolean operations, one process, no pseudorandom choices, no network, and no external service. A successful run prints one stable JSON document ending with `all_exact_checks_passed`.",
  "status": "available",
  "evidence_grade": "executable",
  "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": "partial",
    "kind": "python_exact_boolean_matrix_and_nfa_replay",
    "command": "python3 tools/two_way_nfa_fixed_alphabet_replay.py",
    "entrypoint": "tools/two_way_nfa_fixed_alphabet_replay.py",
    "runtime": "CPython 3.9.6, standard library only",
    "citation": {
      "locator": "Repository file tools/two_way_nfa_fixed_alphabet_replay.py, source SHA-256 c27470826ecc9ad0af3fab2b4da557e8fbb65458026fe6cb03d04236f39b5467"
    },
    "dependencies": [
      {
        "name": "CPython standard library",
        "license": "Python-2.0"
      }
    ],
    "outputs": {
      "stdout_sha256": "6e54a03586dbf06927bfe7024c35332b0fefe34d26089e9ebf7cec5d6e1fefc2",
      "case_checksum_sha256": "5ba55e6f801be821d62ac69d290ef19aeaef384e59a9e896ab3b237a7ded5327",
      "separator_matrix_cell_cases": 1053250,
      "encoded_matrix_words": 332574,
      "binary_decoded_matrix_words": 332574,
      "three_block_matrix_words": 4104,
      "total_exact_cases": 1385824,
      "result": "all_exact_checks_passed"
    },
    "runtime_seconds": 179.75,
    "missing": [
      "source"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": null,
    "locator": "Repository file tools/two_way_nfa_fixed_alphabet_replay.py, source SHA-256 c27470826ecc9ad0af3fab2b4da557e8fbb65458026fe6cb03d04236f39b5467"
  },
  "models": [],
  "relations": [
    {
      "slug": "R814",
      "title": "The separator and encoded NFAs pass 1,385,824 unique finite inputs",
      "object_type": "claim",
      "relation": "evidences",
      "direction": "outgoing"
    },
    {
      "slug": "two-way-nfa-polynomial-determinization",
      "title": "two way nfa polynomial determinization",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}