{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R816",
  "content_hash": null,
  "slug": "twnfa-claim-fixed-binary-quadratic-transfer",
  "type": "claim",
  "title": "The one-way-liveness bound transfers to a fixed binary alphabet",
  "summary": "There is a family of at most 9h-state 1NFAs over one binary alphabet for which every equivalent 2DFA has at least \\(h(h+1)/8-1\\) states.",
  "relevance": "For Polynomial determinization of two-way finite automata, record twnfa-claim-fixed-binary-quadratic-transfer (“The one-way-liveness bound transfers to a fixed binary alphabet”) records a bound, answer, status fact, or structural consequence. The record states: There is a family of at most 9h-state 1NFAs over one binary alphabet for which every equivalent 2DFA has at least \\(h(h+1)/8-1\\) states.",
  "relevance_source": "recorded",
  "body": "Begin with \\(\\Gamma=\\{0,1,\\#,\\$\\}\\). Encode an \\(h\\) by \\(h\\) Boolean matrix row by row, put `#` between successive rows, and append `$`. Each matrix block has length \\(h^2+h\\).\n\nDefine a 1NFA \\(N_h\\) with one start state, \\(h-1\\) row-skipping states, \\(h\\) column states, and \\(h\\) tail states. The total is \\(3h\\). At the first block it guesses a starting row. In each block it skips to the row stored by the current branch, scans that row, and may choose a `1` in column \\(j\\). The tail state \\(T_j\\) carries \\(j\\) to the next `$`. The start state and the \\(h\\) states representing block boundaries are final. Thus a branch accepts after the last complete block exactly when it selected one edge in every matrix. Let \\(K_h\\) be the language accepted by this automaton, including its explicitly determined behavior away from canonical matrix encodings. On every canonical word\n\\[\nc_h(A_1)c_h(A_2)\\cdots c_h(A_m),\n\\]\nmembership in \\(K_h\\) is equivalent to the Boolean product \\(A_1A_2\\cdots A_m\\) being nonzero. This follows by induction on the blocks: after each `$`, the live branches store exactly the reachable right-column nodes.\n\nNow suppose an \\(s\\)-state 2DFA \\(D_h\\) recognizes \\(K_h\\). Build a 2DFA for \\(\\operatorname{owl}_h\\) whose ordinary states pair a state of \\(D_h\\) with the side from which a matrix block was entered. For each large-alphabet symbol \\(A\\), hardwire the deterministic run of \\(D_h\\) inside the fixed word \\(c_h(A)\\) until it exits that block, halts, or repeats an internal state-position configuration. An exit becomes one move to the adjacent matrix symbol with the corresponding entry side. An accepting halt enters a right-sweeping accept state. A rejecting halt or repeated internal configuration enters a right-sweeping reject state. The two sweep states also put the machine into the right-endmarker acceptance convention used by the source lower bound. Endmarker behavior is copied directly. This macro machine has at most \\(2s+2\\) states and agrees with \\(D_h\\) on every canonical encoding.\n\nUse the uniform two-bit code\n\\[\n0\\mapsto00,\\qquad 1\\mapsto01,\\qquad \\#\\mapsto10,\\qquad \\$\\mapsto11.\n\\]\nA binary decoder for \\(N_h\\) has one boundary copy of each state and two pending-first-bit copies. It therefore uses at most \\(9h\\) states and accepts exactly the two-bit images of words in \\(K_h\\). A 2DFA for this binary language can be macro-simulated directly on each length-\\(2(h^2+h)\\) matrix block, again using two state copies and the two sweep states.\n\nThe sourced one-way-liveness lower bound therefore gives\n\\[\n2s+2\\ge \\frac{h(h+1)}4,\n\\qquad\ns\\ge \\frac{h(h+1)}8-1.\n\\]\nFor the four-symbol intermediate family, \\(n=3h\\) gives \\(s\\ge n^2/72+n/24-1\\). For the binary family, \\(n=9h\\) gives \\(s\\ge n^2/648+n/72-1\\). These bounds are quadratic. Their exponent matches Chrobak's earlier unary fixed-alphabet lower bound, while the explicit binary family transports the 2026 liveness construction. The canonical polynomial-simulation question remains open.",
  "status": "supported",
  "evidence_grade": "self_reported",
  "scope": {
    "kind": "family",
    "statement": "the explicitly defined binary family obtained from K_h by a uniform two-bit code, for every integer h at least 1",
    "family": "at most 9h-state binary one-way NFAs recognizing encoded one-way liveness"
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "source_only",
    "kind": "claim",
    "citation": {
      "url": "https://arxiv.org/abs/2602.24279",
      "locator": "Original fixed-alphabet reduction written and audited 2026-07-28, using Adeogun and Kapoutsis's Theorem 1 as the imported lower bound"
    },
    "missing": [
      "source",
      "command",
      "runtime",
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://arxiv.org/abs/2602.24279",
    "locator": "Original fixed-alphabet reduction written and audited 2026-07-28, using Adeogun and Kapoutsis's Theorem 1 as the imported lower bound"
  },
  "relations": [
    {
      "slug": "R818",
      "title": "One-way liveness forces at least h(h+1)/4 deterministic states",
      "object_type": "claim",
      "relation": "depends_on",
      "direction": "outgoing"
    },
    {
      "slug": "R815",
      "title": "The fixed-alphabet determinization question remains open",
      "object_type": "claim",
      "relation": "supports",
      "direction": "outgoing"
    },
    {
      "slug": "R814",
      "title": "The separator and encoded NFAs pass 1,385,824 unique finite inputs",
      "object_type": "claim",
      "relation": "tests",
      "direction": "incoming"
    },
    {
      "slug": "R812",
      "title": "The fixed-alphabet transfer stops at a quadratic lower bound",
      "object_type": "attempt",
      "relation": "depends_on",
      "direction": "incoming"
    },
    {
      "slug": "two-way-nfa-polynomial-determinization",
      "title": "two way nfa polynomial determinization",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}