{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R35",
  "content_hash": null,
  "slug": "asser-attempt-mechanize-three-variable-reduction",
  "type": "attempt",
  "title": "Mechanize the three-variable bipartite reduction",
  "summary": "Build a proof-producing sentence compiler for the affine spectrum encoding, with finite-model replays that expose the exact complement pullback still needed.",
  "relevance": "For Asser's complement problem for first-order spectra, record asser-attempt-mechanize-three-variable-reduction (“Mechanize the three-variable bipartite reduction”) documents a concrete method, search boundary, or failed route. The record states: Build a proof-producing sentence compiler for the affine spectrum encoding, with finite-model replays that expose the exact complement pullback still needed.",
  "relevance_source": "recorded",
  "body": "Implement Theorem 1.1 of Kopczyński and Tan as a syntax-directed compiler. Given a first-order sentence \\(\\Phi\\) using at least three variables over binary relations, the artifact should emit the one-relation sentence \\(\\Phi'\\), the constants \\(p,q\\), and checkable translation data for\n\\[\n\\operatorname{Spec}(\\Phi')=\\{pn+q:n\\in\\operatorname{Spec}(\\Phi)\\}.\n\\]\nFor \\(m\\) normalized source relations, the paper's construction gives \\(p=m+3\\) and \\(q=8m+2\\). The trace should cover self-loop elimination, padding to \\(m\\ge3\\), the definitions \\(F_1,\\ldots,F_5\\), the constraints \\(P_1,\\ldots,P_6\\), and the forward and reverse model maps. It should retain the source variable bound, prove symmetry of the relation, and derive the bipartition of every model.\n\nThe first milestone accepts three-variable sentences over one source relation with quantifier rank at most three. Its test manifest fixes 64 canonical normalized sentences of at most twelve abstract-syntax nodes, chosen to exercise every compiler clause and their main interactions. For each sentence it enumerates every source relation through cardinality four, builds the forward target model, and checks the translated sentence and size equation. Reverse correctness comes from the emitted clause-by-clause proof trace. Generated target models and single-edge mutations supply bounded regression coverage. Self-loop elimination introduces a second relation, then dummy padding brings the normalized count to three, so the affine constants are \\(p=6\\) and \\(q=26\\). Stop after eight active implementation hours or after every compiler clause and size equation has a checked lemma. A successful artifact would reproduce an established reduction. The remaining complement construction would stay visible as a separate obligation.",
  "status": "next_experiment",
  "evidence_grade": "self_reported",
  "scope": {
    "kind": "family",
    "statement": "the source transformation from sentences with at least three variables and binary relations to one-relation sentences whose finite models are undirected bipartite graphs",
    "family": "Kopczyński-Tan affine spectrum encoding"
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "source_only",
    "kind": "attempt",
    "citation": {
      "url": "https://doi.org/10.23638/LMCS-14(2:4)2018",
      "locator": "Theorem 1.1 and construction in Sections 2–3, pp. 2–13"
    },
    "missing": [
      "source",
      "command",
      "runtime",
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://doi.org/10.23638/LMCS-14(2:4)2018",
    "locator": "Theorem 1.1 and construction in Sections 2–3, pp. 2–13"
  },
  "relations": [
    {
      "slug": "R40",
      "title": "Three-variable bipartite graph sentences suffice",
      "object_type": "claim",
      "relation": "uses",
      "direction": "outgoing"
    },
    {
      "slug": "R38",
      "title": "Asser's complement problem remains open",
      "object_type": "claim",
      "relation": "addresses",
      "direction": "outgoing"
    },
    {
      "slug": "first-order-spectra-complement-closure",
      "title": "first order spectra complement closure",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}