{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R538",
  "content_hash": null,
  "slug": "ms200-artifact-construction-and-lp",
  "type": "artifact",
  "title": "Construction verifier and exact rational LP replay",
  "summary": "Python enumerates every collision, verifies the 71-set, hash-binds the hypergraph, and solves its rational relaxation.",
  "relevance": "For Largest multiplicative Sidon subset of the first 200 integers, record ms200-artifact-construction-and-lp (“Construction verifier and exact rational LP replay”) supplies evidence or a replay used to check the packet. The record states: Python enumerates every collision, verifies the 71-set, hash-binds the hypergraph, and solves its rational relaxation.",
  "relevance_source": "recorded",
  "body": "The program first checks the lower-bound set using integer multiplication. It then groups all \\(20,100\\) ground-set pairs by product. Every pair of distinct representations yields a three- or four-vertex forbidden edge. Sorting and hashing all 20,111 distinct edges fixes the exact hypergraph used by the upper calculation.\n\nThe final block asks Z3's exact rational optimizer to maximize the sum of 200 real variables under the box and hyperedge constraints. It asserts the optimum \\(291/2\\), then emits a canonical JSON report. On the audited installation, Z3 5.0.0 completed this relaxation in about 28 seconds. The report has SHA-256 digest `68e7d07943110a09a301151769f2d3d750b42f35402796bd36204588ddc487a0`.",
  "status": "available",
  "evidence_grade": "executable",
  "scope": {
    "kind": "bounded",
    "statement": "all 20,100 unordered pairs in the ground set 1 through 200, every resulting product collision, and the full 200-variable collision-hypergraph LP",
    "bounds": {
      "ground_set_size": {
        "min": 200,
        "max": 200
      },
      "ground_pairs": {
        "min": 20100,
        "max": 20100
      },
      "collision_hyperedges": {
        "min": 20111,
        "max": 20111
      },
      "lp_variables": {
        "min": 200,
        "max": 200
      }
    },
    "exhaustive": true
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "partial",
    "kind": "inline_python_computation",
    "entrypoint": "join source_lines with newline and run with python3",
    "runtime": "CPython 3 with z3-solver 5.0.0",
    "citation": {
      "url": "https://arxiv.org/abs/1808.06182",
      "locator": "Inline Python exhaustive verifier with Z3 exact rational optimization, executed 2026-07-25"
    },
    "inline_source": [
      "from collections import defaultdict",
      "from hashlib import sha256",
      "from json import dumps",
      "from z3 import Optimize, Real, Sum, sat",
      "A=[1,12,17,31,35,40,41,43,49,52,54,55,58,71,73,81,83,86,89,96,101,103,107,109,113,114,117,118,119,121,125,127,131,133,134,137,138,139,143,145,148,149,151,153,157,158,159,163,164,167,168,170,173,174,176,179,181,182,183,184,185,186,188,191,193,194,195,197,198,199,200]",
      "products=[a*b for i,a in enumerate(A) for b in A[i:]]",
      "assert len(A)==71 and len(products)==len(set(products))==2556",
      "representations=defaultdict(list)",
      "for a in range(1,201):",
      "    for b in range(a,201):",
      "        representations[a*b].append((a,b))",
      "edges=set()",
      "for pairs in representations.values():",
      "    for i in range(len(pairs)):",
      "        for j in range(i):",
      "            edges.add(tuple(sorted(set(pairs[i]+pairs[j]))))",
      "assert len(edges)==20111",
      "assert sum(len(edge)==3 for edge in edges)==248",
      "assert sum(len(edge)==4 for edge in edges)==19863",
      "assert all(not set(edge)<=set(A) for edge in edges)",
      "set_text=' '.join(map(str,A))+'\\n'",
      "product_text='\\n'.join(map(str,sorted(products)))+'\\n'",
      "edge_text='\\n'.join(' '.join(map(str,edge)) for edge in sorted(edges))+'\\n'",
      "set_sha=sha256(set_text.encode()).hexdigest()",
      "products_sha=sha256(product_text.encode()).hexdigest()",
      "edges_sha=sha256(edge_text.encode()).hexdigest()",
      "assert set_sha=='87c37bb973034570880b4c3a868eaf2a20ab69d25872f48a545fe2e9a0716db3'",
      "assert products_sha=='2c893b6f16e7f5b02675d9d78bf06467300d5437d6729334d35473e816cc5c20'",
      "assert edges_sha=='652883fe102d2e111adfc61a2b85e8ced861934bdc089fe9a9204c0d4ee76358'",
      "x=[None]+[Real('x_'+str(i)) for i in range(1,201)]",
      "opt=Optimize()",
      "for i in range(1,201):",
      "    opt.add(x[i]>=0,x[i]<=1)",
      "for edge in edges:",
      "    opt.add(Sum([x[i] for i in edge])<=len(edge)-1)",
      "handle=opt.maximize(Sum(x[1:]))",
      "assert opt.check()==sat",
      "assert str(opt.upper(handle))=='291/2'",
      "report={'n':200,'set_size':len(A),'pair_products':len(products),'distinct_pair_products':len(set(products)),'collision_products':sum(len(value)>1 for value in representations.values()),'collision_hyperedges':len(edges),'triple_edges':sum(len(edge)==3 for edge in edges),'quadruple_edges':sum(len(edge)==4 for edge in edges),'set_sha256':set_sha,'products_sha256':products_sha,'hyperedges_sha256':edges_sha,'lp_relaxation_optimum':'291/2','integer_upper_bound':145}",
      "payload=dumps(report,sort_keys=True,separators=(',',':'))",
      "assert sha256(payload.encode()).hexdigest()=='68e7d07943110a09a301151769f2d3d750b42f35402796bd36204588ddc487a0'",
      "print(payload)"
    ],
    "missing": [
      "command",
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://arxiv.org/abs/1808.06182",
    "locator": "Inline Python exhaustive verifier with Z3 exact rational optimization, executed 2026-07-25"
  },
  "models": [],
  "relations": [
    {
      "slug": "R540",
      "title": "The certified interval is 71 through 145",
      "object_type": "claim",
      "relation": "verifies",
      "direction": "outgoing"
    },
    {
      "slug": "multiplicative-sidon-200",
      "title": "multiplicative sidon 200",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}