{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R226",
  "content_hash": null,
  "slug": "dstg-artifact-witness-direction-check",
  "type": "artifact",
  "title": "Exact witness verifier and size-11 continuation instance",
  "summary": "Standard-library Python checks all slopes, proves the counting bound, and hashes a complete 0-1 pseudo-Boolean instance for the next case.",
  "relevance": "For Most lattice points with all pairwise slopes distinct in a ten by ten grid, record dstg-artifact-witness-direction-check (“Exact witness verifier and size-11 continuation instance”) supplies evidence or a replay used to check the packet. The record states: Standard-library Python checks all slopes, proves the counting bound, and hashes a complete 0-1 pseudo-Boolean instance for the next case.",
  "relevance_source": "recorded",
  "body": "The program represents an undirected slope by a sign-normalized primitive integer pair. It checks every one of the witness's 45 pairs and enumerates the complete set of 112 directions supported by the grid.\n\nIt also constructs a precise continuation for testing size 11. A Boolean variable selects each grid point. For each two point-pairs with the same direction, a three-variable or four-variable inequality forbids selecting their union. The program deduplicates these to 331,537 conflict constraints. It adds the cardinality target \\(\\sum x_i\\geq11\\). Two safe translation constraints require a selected point on the left edge and one on the bottom edge, since any solution can be translated until its minimum coordinates are zero. The resulting canonical pseudo-Boolean text has SHA-256 digest `4f61cab88ff8fbabfc4ee3165bba3bb486f4f874c799cd9a4ebf0fee4d8ec93b`.",
  "status": "available",
  "evidence_grade": "executable",
  "scope": {
    "kind": "bounded",
    "statement": "the displayed 10-point witness, all 45 of its pairs, all 4,950 grid pairs, and a canonical pseudo-Boolean continuation instance",
    "bounds": {
      "grid_points": {
        "min": 100,
        "max": 100
      },
      "witness_points": {
        "min": 10,
        "max": 10
      },
      "witness_pairs": {
        "min": 45,
        "max": 45
      },
      "supported_directions": {
        "min": 112,
        "max": 112
      }
    },
    "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, standard library only",
    "citation": {
      "url": "https://doi.org/10.1016/j.disc.2025.114822",
      "locator": "Inline Python 3 computation executed on 2026-07-25"
    },
    "inline_source": [
      "from hashlib import sha256",
      "from itertools import combinations",
      "from json import dumps",
      "from math import gcd",
      "N=10",
      "WITNESS=[(0,7),(1,2),(2,0),(4,6),(5,3),(6,9),(7,1),(8,1),(9,5),(9,8)]",
      "def direction(a,b):",
      "    dx=b[0]-a[0]",
      "    dy=b[1]-a[1]",
      "    if dx<0 or (dx==0 and dy<0):",
      "        dx,dy=-dx,-dy",
      "    g=gcd(abs(dx),abs(dy))",
      "    return dx//g,dy//g",
      "points=[(x,y) for x in range(N) for y in range(N)]",
      "supported=sorted({direction(a,b) for a,b in combinations(points,2)})",
      "witness_directions=[direction(a,b) for a,b in combinations(WITNESS,2)]",
      "assert len(points)==100 and len(supported)==112",
      "assert len(WITNESS)==len(set(WITNESS))==10",
      "assert all(p in points for p in WITNESS)",
      "assert len(witness_directions)==len(set(witness_directions))==45",
      "assert 15*14//2<=len(supported)<16*15//2",
      "edges_by_direction={d:[] for d in supported}",
      "for i,j in combinations(range(100),2):",
      "    edges_by_direction[direction(points[i],points[j])].append((i,j))",
      "conflicts=set()",
      "for edges in edges_by_direction.values():",
      "    for first,second in combinations(edges,2):",
      "        conflicts.add(tuple(sorted(set(first+second))))",
      "assert all(len(c) in (3,4) for c in conflicts)",
      "h=sha256()",
      "def add(line):",
      "    h.update((line+'\\n').encode())",
      "add('* distinct-slopes-ten-grid, exact 0-1 PB decision instance for a set of size at least 11')",
      "add('* x_i selects points ordered lexicographically as (0,0),(0,1),...,(9,9)')",
      "add(' '.join(f'+1 x{i+1}' for i in range(100))+' >= 11;')",
      "add(' '.join(f'+1 x{i+1}' for i,p in enumerate(points) if p[0]==0)+' >= 1;')",
      "add(' '.join(f'+1 x{i+1}' for i,p in enumerate(points) if p[1]==0)+' >= 1;')",
      "for c in sorted(conflicts):",
      "    add(' '.join(f'+1 x{i+1}' for i in c)+f' <= {len(c)-1};')",
      "report={'grid_points':len(points),'supported_undirected_primitive_directions':len(supported),'all_directions_sha256':sha256(('\\n'.join(f'{a},{b}' for a,b in supported)+'\\n').encode()).hexdigest(),'witness':WITNESS,'witness_size':len(WITNESS),'witness_pairs':len(witness_directions),'witness_unique_directions':len(set(witness_directions)),'witness_directions_sha256':sha256(('\\n'.join(f'{a},{b}' for a,b in sorted(witness_directions))+'\\n').encode()).hexdigest(),'pair_count_upper_bound':15,'pb_target_size':11,'pb_translation_symmetry_constraints':2,'pb_conflict_constraints':len(conflicts),'pb_three_point_constraints':sum(len(c)==3 for c in conflicts),'pb_four_point_constraints':sum(len(c)==4 for c in conflicts),'pb_total_constraints':len(conflicts)+3,'pb_canonical_sha256':h.hexdigest()}",
      "payload=dumps(report,sort_keys=True,separators=(',',':'))",
      "assert sha256(payload.encode()).hexdigest()=='90c106c91f256a3badd69fa104dfee0d762903ba94cbab75c7b8e58377736b5a'",
      "print(payload)"
    ],
    "missing": [
      "command",
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://doi.org/10.1016/j.disc.2025.114822",
    "locator": "Inline Python 3 computation executed on 2026-07-25"
  },
  "relations": [
    {
      "slug": "R228",
      "title": "The maximum lies between 10 and 15",
      "object_type": "claim",
      "relation": "evidences",
      "direction": "outgoing"
    },
    {
      "slug": "distinct-slopes-ten-grid",
      "title": "distinct slopes ten grid",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}