{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R40",
  "content_hash": null,
  "slug": "asser-claim-three-variable-bipartite-reduction",
  "type": "claim",
  "title": "Three-variable bipartite graph sentences suffice",
  "summary": "Closure of all first-order spectra under complement is equivalent to closure for three-variable sentences whose finite models are undirected bipartite graphs.",
  "relevance": "For Asser's complement problem for first-order spectra, record asser-claim-three-variable-bipartite-reduction (“Three-variable bipartite graph sentences suffice”) records a bound, answer, status fact, or structural consequence. The record states: Closure of all first-order spectra under complement is equivalent to closure for three-variable sentences whose finite models are undirected bipartite graphs.",
  "relevance_source": "recorded",
  "body": "Kopczyński and Tan first reduce the complement question to three-variable sentences over binary relations. Their later graph encoding replaces any collection of binary relations by one symmetric binary relation. For a source sentence \\(\\Phi\\), the construction gives constants \\(p,q\\) and a sentence \\(\\Phi'\\) with\n\\[\n\\operatorname{Spec}(\\Phi')=\\{pn+q:n\\in\\operatorname{Spec}(\\Phi)\\}.\n\\]\nEvery model of \\(\\Phi'\\) is an undirected bipartite graph, and the transformation preserves the number of variables when at least three are available. The proof of Corollary 1.2 combines this encoding with the spectrum-machine characterization and a padding argument to obtain the stated equivalence.",
  "status": "reported",
  "evidence_grade": "sourced",
  "scope": {
    "kind": "family",
    "statement": "equivalence between complement closure for all first-order spectra and closure for three-variable sentences over one symmetric binary relation whose finite models are bipartite",
    "family": "all first-order spectra and the three-variable one-relation bipartite normal form"
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "source_only",
    "kind": "claim",
    "citation": {
      "url": "https://doi.org/10.23638/LMCS-14(2:4)2018",
      "locator": "Corollary 1.2, pp. 2 and 13–14"
    },
    "missing": [
      "source",
      "command",
      "runtime",
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://doi.org/10.23638/LMCS-14(2:4)2018",
    "locator": "Corollary 1.2, pp. 2 and 13–14"
  },
  "relations": [
    {
      "slug": "R38",
      "title": "Asser's complement problem remains open",
      "object_type": "claim",
      "relation": "supports",
      "direction": "outgoing"
    },
    {
      "slug": "R34",
      "title": "Dated source and duplicate audit",
      "object_type": "attempt",
      "relation": "informs",
      "direction": "incoming"
    },
    {
      "slug": "R35",
      "title": "Mechanize the three-variable bipartite reduction",
      "object_type": "attempt",
      "relation": "uses",
      "direction": "incoming"
    },
    {
      "slug": "first-order-spectra-complement-closure",
      "title": "first order spectra complement closure",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}