{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R841",
  "content_hash": null,
  "slug": "z101-four-ap-free-artifact-witness-and-design-bound",
  "type": "artifact",
  "title": "Exact witness and incidence verifier",
  "summary": "Standard-library Python verifies the 30-set and every vertex and pair incidence used in the upper-bound proof.",
  "relevance": "For Largest four-term-progression-free subset of Z_101, record z101-four-ap-free-artifact-witness-and-design-bound (“Exact witness and incidence verifier”) supplies evidence or a replay used to check the packet. The record states: Standard-library Python verifies the 30-set and every vertex and pair incidence used in the upper-bound proof.",
  "relevance_source": "recorded",
  "body": "The verifier generates progressions using every \\(a\\in\\mathbb Z/101\\mathbb Z\\) and every nonzero \\(d\\), then removes the reversal duplication by storing each progression as a sorted tuple. It obtains 5,050 edges. It checks all 20,200 vertex-edge incidences and all 30,300 pair-edge incidences, establishing degrees 200 and pair codegrees six. It then checks the displayed set against every edge and evaluates the final inequality at 68, the first excluded cardinality.\n\nThe canonical report digest is `6edf6fac68fe92ce3563d0f3573215ee33c474019800b84a1dc15a57076f3a43`.",
  "status": "available",
  "evidence_grade": "executable",
  "scope": {
    "kind": "bounded",
    "statement": "the complete four-term progression hypergraph on Z/101Z and the displayed 30-element independent set",
    "bounds": {
      "vertices": {
        "min": 101,
        "max": 101
      },
      "distinct_progressions": {
        "min": 5050,
        "max": 5050
      },
      "witness_size": {
        "min": 30,
        "max": 30
      },
      "pair_incidences_checked": {
        "min": 30300,
        "max": 30300
      }
    },
    "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.4171/EM/16",
      "locator": "Independent exact computation, 2026-07-25"
    },
    "inline_source": [
      "from collections import Counter",
      "from hashlib import sha256",
      "from itertools import combinations",
      "from json import dumps",
      "from math import comb",
      "p=101",
      "witness=(0,10,18,23,27,29,35,37,39,40,45,47,48,49,56,61,65,68,69,70,72,76,78,79,84,85,87,91,93,95)",
      "assert len(witness)==30 and len(set(witness))==30 and all(0<=x<p for x in witness)",
      "edges=sorted({tuple(sorted((a+i*d)%p for i in range(4))) for a in range(p) for d in range(1,p)})",
      "assert len(edges)==5050 and all(len(set(edge))==4 for edge in edges)",
      "vertex_degree=Counter(v for edge in edges for v in edge)",
      "pair_degree=Counter(pair for edge in edges for pair in combinations(edge,2))",
      "assert len(vertex_degree)==101 and set(vertex_degree.values())=={200}",
      "assert len(pair_degree)==comb(101,2)==5050 and set(pair_degree.values())=={6}",
      "chosen=set(witness)",
      "violations=[edge for edge in edges if set(edge)<=chosen]",
      "assert violations==[]",
      "first_excluded=68",
      "pair_side=6*comb(first_excluded,2)",
      "vertex_side=200*first_excluded",
      "assert pair_side>vertex_side",
      "canonical=','.join(map(str,witness))+'\\n'",
      "witness_sha=sha256(canonical.encode()).hexdigest()",
      "report={'modulus':p,'edges':len(edges),'vertex_edge_incidences':sum(vertex_degree.values()),'vertex_degree':min(vertex_degree.values()),'pair_edge_incidences':sum(pair_degree.values()),'pair_codegree':min(pair_degree.values()),'witness_size':len(witness),'violations':len(violations),'certified_upper_bound':67,'first_excluded_size':first_excluded,'pair_side_at_68':pair_side,'vertex_side_at_68':vertex_side,'witness_sha256':witness_sha}",
      "payload=dumps(report,sort_keys=True,separators=(',',':'))",
      "assert sha256(payload.encode()).hexdigest()=='6edf6fac68fe92ce3563d0f3573215ee33c474019800b84a1dc15a57076f3a43'",
      "print(payload)"
    ],
    "missing": [
      "command",
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://doi.org/10.4171/EM/16",
    "locator": "Independent exact computation, 2026-07-25"
  },
  "models": [],
  "relations": [
    {
      "slug": "R843",
      "title": "The certified interval is 30 through 67",
      "object_type": "claim",
      "relation": "supports",
      "direction": "outgoing"
    },
    {
      "slug": "z101-four-ap-free",
      "title": "z101 four ap free",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}