{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R559",
  "content_hash": null,
  "slug": "pcp5-claim-general-lower-nine",
  "type": "claim",
  "title": "Every such encoding has at least 9 clauses",
  "summary": "The published bound m >= 3n - 9 applies after one visible-variable polarity flip.",
  "relevance": "For Minimum propagation-complete CNF for five-bit parity, record pcp5-claim-general-lower-nine (“Every such encoding has at least 9 clauses”) records a bound, answer, status fact, or structural consequence. The record states: The published bound m >= 3n - 9 applies after one visible-variable polarity flip.",
  "relevance_source": "recorded",
  "body": "Theorem 1.1(3) of Emdin, Kulikov, Mihajlin, and Slezkin states that a CNF encoding of \\(\\operatorname{PAR}_n\\), allowing auxiliary variables, has \\(m\\geq3n-9\\) clauses. The paper defines an encoding by existential projection over the auxiliary variables, matching the semantic convention in the candidate.\n\nThe target relation satisfies\n\\[\nx_1\\oplus x_2\\oplus x_3\\oplus x_4\\oplus x_5\\oplus y=0.\n\\]\nReplacing \\(y\\) by \\(\\neg y\\) turns this predicate into \\(\\operatorname{PAR}_6\\). Literal complementation preserves clauses one for one. Substitution into the published theorem gives \\(m\\geq3\\cdot6-9=9\\). This semantic lower bound applies to the candidate's smaller class with at most three auxiliaries and its added propagation requirement.",
  "status": "reported",
  "evidence_grade": "sourced",
  "scope": {
    "kind": "bounded",
    "statement": "all existential CNF encodings of the even-parity predicate on the six visible variables x1,x2,x3,x4,x5,y, with any number of auxiliary variables",
    "bounds": {
      "visible_variables": {
        "min": 6,
        "max": 6
      },
      "clauses": {
        "min": 9
      }
    },
    "exhaustive": false
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "source_only",
    "kind": "claim",
    "citation": {
      "url": "https://doi.org/10.4230/LIPIcs.MFCS.2022.47",
      "locator": "Gregory Emdin, Alexander S. Kulikov, Ivan Mihajlin, and Nikita Slezkin, CNF Encodings of Parity, MFCS 2022, Theorem 1.1(3), equation (4)"
    },
    "missing": [
      "source",
      "command",
      "runtime",
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://doi.org/10.4230/LIPIcs.MFCS.2022.47",
    "locator": "Gregory Emdin, Alexander S. Kulikov, Ivan Mihajlin, and Nikita Slezkin, CNF Encodings of Parity, MFCS 2022, Theorem 1.1(3), equation (4)"
  },
  "models": [],
  "relations": [
    {
      "slug": "R558",
      "title": "The certified interval is 9 to 16 clauses",
      "object_type": "claim",
      "relation": "supports",
      "direction": "outgoing"
    },
    {
      "slug": "propagation-complete-five-bit-parity",
      "title": "propagation complete five bit parity",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}