{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R782",
  "content_hash": null,
  "slug": "threshold-six-three-artifact-five-and-verifier",
  "type": "artifact",
  "title": "Exhaustive verifier for the five-AND circuit",
  "summary": "The standard-library program checks every input, the truth-table word, and the degree-three plus degree-four algebraic normal form.",
  "relevance": "For Multiplicative complexity of the six-bit threshold-at-least-three function, record threshold-six-three-artifact-five-and-verifier (“Exhaustive verifier for the five-AND circuit”) supplies evidence or a replay used to check the packet. The record states: The standard-library program checks every input, the truth-table word, and the degree-three plus degree-four algebraic normal form.",
  "relevance_source": "recorded",
  "body": "The program evaluates the five products in the straight-line program on every six-bit input. It compares each output with the direct predicate `sum(x) >= 3`, packs the outputs into a 64-bit word, and applies the Boolean Möbius transform. The expected output certifies 64 matching rows, five counted products, truth-table word `fffefee8fee8e880`, and 35 algebraic-normal-form terms whose degrees are exactly 3 and 4.",
  "status": "available",
  "evidence_grade": "executable",
  "scope": {
    "kind": "bounded",
    "statement": "all 64 Boolean assignments to x1 through x6 for the displayed five-AND circuit and its algebraic normal form",
    "bounds": {
      "assignments": {
        "min": 64,
        "max": 64
      },
      "and_gates": {
        "min": 5,
        "max": 5
      },
      "anf_terms": {
        "min": 35,
        "max": 35
      }
    },
    "exhaustive": true
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "partial",
    "kind": "inline_python_exhaustive_verifier",
    "entrypoint": "Join source_lines with LF characters and execute the resulting Python program",
    "runtime": "Python 3 standard library",
    "citation": {
      "url": "https://doi.org/10.1016/j.tcs.2008.01.030",
      "locator": "Python 3 standard-library verifier executed by TheoremDB entry research on 2026-07-25"
    },
    "outputs": "rows=64 ands=5 truth_table=fffefee8fee8e880 anf_terms=35 anf_degrees=[3, 4]\n",
    "inline_source": [
      "def circuit(x):",
      "    x1, x2, x3, x4, x5, x6 = x",
      "    s0 = x1 ^ x2 ^ x3",
      "    a0 = ((x1 ^ x2) & (x1 ^ x3)) ^ x1",
      "    s1 = x4 ^ x5 ^ x6",
      "    a1 = ((x4 ^ x5) & (x4 ^ x6)) ^ x4",
      "    a2 = s0 & s1",
      "    a3 = ((a0 ^ a1) & (a0 ^ a2)) ^ a0",
      "    a4 = (s0 ^ s1) & (a0 ^ a1 ^ a2)",
      "    return a3 ^ a4",
      "",
      "truth = 0",
      "values = []",
      "for word in range(64):",
      "    x = tuple((word >> i) & 1 for i in range(6))",
      "    got = circuit(x)",
      "    want = int(sum(x) >= 3)",
      "    assert got == want, (word, x, got, want)",
      "    values.append(got)",
      "    truth |= got << word",
      "assert truth == 0xfffefee8fee8e880",
      "",
      "anf = values[:]",
      "for bit in range(6):",
      "    for mask in range(64):",
      "        if mask & (1 << bit):",
      "            anf[mask] ^= anf[mask ^ (1 << bit)]",
      "terms = [mask for mask, coefficient in enumerate(anf) if coefficient]",
      "degrees = sorted({mask.bit_count() for mask in terms})",
      "assert len(terms) == 35",
      "assert degrees == [3, 4]",
      "assert sum(mask.bit_count() == 3 for mask in terms) == 20",
      "assert sum(mask.bit_count() == 4 for mask in terms) == 15",
      "print(f'rows=64 ands=5 truth_table={truth:016x} '",
      "      f'anf_terms={len(terms)} anf_degrees={degrees}')"
    ],
    "missing": [
      "command"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://doi.org/10.1016/j.tcs.2008.01.030",
    "locator": "Python 3 standard-library verifier executed by TheoremDB entry research on 2026-07-25"
  },
  "models": [],
  "relations": [
    {
      "slug": "R786",
      "title": "Five AND gates suffice",
      "object_type": "claim",
      "relation": "supports",
      "direction": "outgoing"
    },
    {
      "slug": "R785",
      "title": "Algebraic degree forces at least three AND gates",
      "object_type": "claim",
      "relation": "supports",
      "direction": "outgoing"
    },
    {
      "slug": "threshold-at-least-three-six-multiplicative-complexity",
      "title": "threshold at least three six multiplicative complexity",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}