{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R44",
  "content_hash": null,
  "slug": "b2z100-artifact-verifier-and-ilp",
  "type": "artifact",
  "title": "Exact difference verifier and complete size-14 feasibility model",
  "summary": "Standard-library Python checks the construction and emits a canonical 0-1 linear model for the remaining case.",
  "relevance": "For Existence of a fourteen-point two-fold difference packing modulo 100, record b2z100-artifact-verifier-and-ilp (“Exact difference verifier and complete size-14 feasibility model”) supplies evidence or a replay used to check the packet. The record states: Standard-library Python checks the construction and emits a canonical 0-1 linear model for the remaining case.",
  "relevance_source": "recorded",
  "body": "The first part computes all 156 ordered differences of the 13-set. It checks the full 99-entry multiplicity vector, the special self-inverse residue 50, and every possible one-point extension. The second part builds a complete binary linear model for a 14-set.\n\nThe model uses membership variables \\(x_i\\) and pair variables \\(y_{ij}\\) for \\(0\\leq i<j<100\\). Three inequalities impose \\(y_{ij}=x_ix_j\\). For each circular distance \\(d=1,\\ldots,49\\), the sum of the corresponding pair variables is at most two. At distance 50 it is at most one, since one antipodal unordered pair contributes both ordered representations of residue 50. The constraints \\(\\sum_i x_i=14\\) and \\(x_0=1\\) complete the formulation. Fixing zero loses no solution because any nonempty set can be translated.\n\nThe generated LP has 5,050 binary variables, 14,850 linearization constraints, and 50 distance constraints. Its SHA-256 digest is `d0f0125ef4b783aaec55d868884c1ef99e7434bc667b544623389db15ac000a5`. The model has not been solved in this record. A feasible solution supplies the desired 14-set. An infeasibility result needs a retained, independently checked proof trace before it can lower the upper bound.",
  "status": "available",
  "evidence_grade": "executable",
  "scope": {
    "kind": "bounded",
    "statement": "all ordered differences of the displayed 13-set, all 87 one-point extensions, and an exact binary feasibility formulation for size 14 in Z/100Z",
    "bounds": {
      "modulus": {
        "min": 100,
        "max": 100
      },
      "checked_extensions": {
        "min": 87,
        "max": 87
      },
      "ilp_binary_variables": {
        "min": 5050,
        "max": 5050
      }
    },
    "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.9 or later, standard library only",
    "citation": {
      "url": "https://doi.org/10.1109/18.30982",
      "locator": "Self-contained CPython standard-library computation executed on 2026-07-25"
    },
    "outputs": "{\"construction\":[8,13,18,28,29,47,68,71,82,83,91,95,99],\"construction_size\":13,\"counting_upper_bound\":14,\"difference_histogram\":[[0,12],[1,18],[2,69]],\"difference_vector_sha256\":\"806d81adaba5cfa5622d11aa717613aabcbfc21de625fc83447d61ca12a0cb7d\",\"ilp_binary_variables\":5050,\"ilp_distance_constraints\":50,\"ilp_linearization_constraints\":14850,\"ilp_sha256\":\"d0f0125ef4b783aaec55d868884c1ef99e7434bc667b544623389db15ac000a5\",\"inclusion_maximal\":true,\"near_miss_overloads\":[[19,3],[81,3]]}\nreport_sha256=771e7bf607fcfd3ca972c21c661541c741f95c673a921c66291cb40a2e44a8e8\n",
    "inline_source": [
      "from collections import Counter",
      "from hashlib import sha256",
      "from itertools import combinations",
      "from json import dumps",
      "",
      "N = 100",
      "construction = [8,13,18,28,29,47,68,71,82,83,91,95,99]",
      "near_miss = [0,5,7,31,43,58,61,62,63,72,80,84,91,97]",
      "",
      "def ordered_counts(points):",
      "    return Counter((a-b) % N for a in points for b in points if a != b)",
      "",
      "def count_vector(points):",
      "    counts = ordered_counts(points)",
      "    return [counts[d] for d in range(1,N)]",
      "",
      "counts = count_vector(construction)",
      "assert len(construction) == len(set(construction)) == 13",
      "assert sum(counts) == 13*12",
      "assert max(counts) == 2",
      "assert counts[49] in (0,2)",
      "assert all(ordered_counts(construction)[d] == ordered_counts(construction)[N-d] for d in range(1,N))",
      "assert all(max(count_vector(construction+[x])) > 2 for x in range(N) if x not in construction)",
      "",
      "near_counts = count_vector(near_miss)",
      "assert len(near_miss) == 14",
      "assert sum(near_counts) == 14*13",
      "assert [(d+1,c) for d,c in enumerate(near_counts) if c > 2] == [(19,3),(81,3)]",
      "",
      "lines = [\"Minimize\",\" obj: 0\",\"Subject To\",\" cardinality: \"+\" + \".join(f\"x_{i}\" for i in range(N))+\" = 14\",\" fix_translation: x_0 = 1\"]",
      "for i,j in combinations(range(N),2):",
      "    y=f\"y_{i}_{j}\"",
      "    lines.extend([",
      "        f\" lin_u1_{i}_{j}: {y} - x_{i} <= 0\",",
      "        f\" lin_u2_{i}_{j}: {y} - x_{j} <= 0\",",
      "        f\" lin_l_{i}_{j}: {y} - x_{i} - x_{j} >= -1\",",
      "    ])",
      "for d in range(1,51):",
      "    pairs=[f\"y_{i}_{j}\" for i,j in combinations(range(N),2) if min((j-i)%N,(i-j)%N)==d]",
      "    cap=1 if d==50 else 2",
      "    lines.append(f\" distance_{d}: \"+\" + \".join(pairs)+f\" <= {cap}\")",
      "lines.append(\"Binary\")",
      "lines.extend(\" \"+f\"x_{i}\" for i in range(N))",
      "lines.extend(\" \"+f\"y_{i}_{j}\" for i,j in combinations(range(N),2))",
      "lines.append(\"End\")",
      "lp=\"\\n\".join(lines)+\"\\n\"",
      "",
      "vector_sha=sha256((\"\\n\".join(map(str,counts))+\"\\n\").encode()).hexdigest()",
      "lp_sha=sha256(lp.encode()).hexdigest()",
      "report={",
      "    \"construction\":construction,",
      "    \"construction_size\":len(construction),",
      "    \"difference_histogram\":sorted(Counter(counts).items()),",
      "    \"difference_vector_sha256\":vector_sha,",
      "    \"inclusion_maximal\":True,",
      "    \"near_miss_overloads\":[[d+1,c] for d,c in enumerate(near_counts) if c>2],",
      "    \"counting_upper_bound\":14,",
      "    \"ilp_binary_variables\":100+100*99//2,",
      "    \"ilp_linearization_constraints\":3*(100*99//2),",
      "    \"ilp_distance_constraints\":50,",
      "    \"ilp_sha256\":lp_sha,",
      "}",
      "payload=dumps(report,sort_keys=True,separators=(\",\",\":\"))",
      "print(payload)",
      "print(\"report_sha256=\"+sha256(payload.encode()).hexdigest())"
    ],
    "missing": [
      "command"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://doi.org/10.1109/18.30982",
    "locator": "Self-contained CPython standard-library computation executed on 2026-07-25"
  },
  "models": [],
  "relations": [
    {
      "slug": "R47",
      "title": "The certified maximum lies between 13 and 14",
      "object_type": "claim",
      "relation": "verifies",
      "direction": "outgoing"
    },
    {
      "slug": "R45",
      "title": "Bounded local searches reached one circular-distance violation",
      "object_type": "attempt",
      "relation": "uses",
      "direction": "incoming"
    },
    {
      "slug": "b2-two-set-z100",
      "title": "b2 two set z100",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}