{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R558",
  "content_hash": null,
  "slug": "pcp5-claim-certified-nine-to-sixteen",
  "type": "claim",
  "title": "The certified interval is 9 to 16 clauses",
  "summary": "A general parity-encoding theorem gives the lower endpoint, while an exhaustive verifier certifies the standard 16-clause chain.",
  "relevance": "For Minimum propagation-complete CNF for five-bit parity, record pcp5-claim-certified-nine-to-sixteen (“The certified interval is 9 to 16 clauses”) records a bound, answer, status fact, or structural consequence. The record states: A general parity-encoding theorem gives the lower endpoint, while an exhaustive verifier certifies the standard 16-clause chain.",
  "relevance_source": "recorded",
  "body": "Let \\(M\\) be the minimum in the candidate question. Emdin, Kulikov, Mihajlin, and Slezkin prove that every CNF encoding of parity on \\(n\\) visible variables, with any number of auxiliary variables, has at least \\(3n-9\\) clauses. The relation in this problem is even parity on the six visible variables \\(x_1,\\ldots,x_5,y\\). Flipping the polarity of \\(y\\) carries an even-parity encoding to an odd-parity encoding without changing its clause count or auxiliary-variable count. Their theorem therefore gives \\(M\\geq 3\\cdot6-9=9\\).\n\nFor the other endpoint, introduce \\(z_1,z_2,z_3\\) and impose\n\\[\nz_1=x_1\\oplus x_2,\\qquad z_2=z_1\\oplus x_3,\\qquad z_3=z_2\\oplus x_4,\\qquad y=z_3\\oplus x_5.\n\\]\nEach binary XOR equivalence uses its four prime implicates, giving 16 clauses. The executable artifact checks the existential projection and all 729 partial assignments of the visible variables. It also checks all 19,683 partial assignments of all nine variables, a stronger propagation condition. Hence\n\\[\n9\\leq M\\leq16.\n\\]\nThe available evidence leaves clause counts 9 through 15 open. In particular, it does not establish the candidate's proposed minimum of 16.",
  "status": "established",
  "evidence_grade": "reproduced",
  "scope": {
    "kind": "bounded",
    "statement": "the minimum clause count among CNF encodings of y=x1 xor x2 xor x3 xor x4 xor x5 that use at most three auxiliary variables and satisfy the candidate's visible-variable propagation criterion",
    "bounds": {
      "visible_variables": {
        "min": 6,
        "max": 6
      },
      "auxiliary_variables": {
        "min": 0,
        "max": 3
      },
      "certified_clause_lower_bound": {
        "min": 9,
        "max": 9
      },
      "certified_clause_upper_bound": {
        "min": 16,
        "max": 16
      }
    },
    "exhaustive": false
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "source_only",
    "kind": "claim",
    "citation": {
      "url": "https://doi.org/10.4230/LIPIcs.MFCS.2022.47",
      "locator": "The lower endpoint applies Theorem 1.1(3) of Emdin et al.; the upper endpoint is reproduced by pcp5-artifact-chain-verifier"
    },
    "missing": [
      "source",
      "command",
      "runtime",
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://doi.org/10.4230/LIPIcs.MFCS.2022.47",
    "locator": "The lower endpoint applies Theorem 1.1(3) of Emdin et al.; the upper endpoint is reproduced by pcp5-artifact-chain-verifier"
  },
  "models": [],
  "relations": [
    {
      "slug": "R556",
      "title": "Exhaustive verifier for the 16-clause XOR chain",
      "object_type": "artifact",
      "relation": "evidences",
      "direction": "incoming"
    },
    {
      "slug": "R559",
      "title": "Every such encoding has at least 9 clauses",
      "object_type": "claim",
      "relation": "supports",
      "direction": "incoming"
    },
    {
      "slug": "R557",
      "title": "The checked literature leaves the exact clause count open",
      "object_type": "attempt",
      "relation": "informs",
      "direction": "incoming"
    },
    {
      "slug": "propagation-complete-five-bit-parity",
      "title": "propagation complete five bit parity",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}