{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R795",
  "content_hash": null,
  "slug": "tptgms-artifact-exact-square-verifier",
  "type": "artifact",
  "title": "Exact four-subset square verifier",
  "summary": "Standard-library Python checks all 3,921,225 grid quadruples, finds 825 squares, and confirms that exactly 32 lie in the witness.",
  "relevance": "For Most squares spanned by twenty points of the ten grid, record tptgms-artifact-exact-square-verifier (“Exact four-subset square verifier”) supplies evidence or a replay used to check the packet. The record states: Standard-library Python checks all 3,921,225 grid quadruples, finds 825 squares, and confirms that exactly 32 lie in the witness.",
  "relevance_source": "recorded",
  "body": "A quadruple is accepted precisely when its six squared pair distances consist of four copies of a positive integer \\(d\\) and two copies of \\(2d\\). This distance test is invariant under orientation and counts each unordered vertex set once.\n\nThe program applies the test to every four-subset of the ten grid. It finds 825 squares. It then filters those squares by containment in the displayed witness and independently tests all 4,845 witness quadruples. Both routes return the same ordered list of 32 squares. The canonical list has SHA-256 digest `6c44a24e1b8a7a1cfb59815218f4f1a9af988ad41c3e114f05772ec5094c682c`.\n\nThe final four integers replay the deletion-averaging arithmetic. The starting value 22 is the external mathematical input supplied by Kurz's Theorem 51. The canonical report has SHA-256 digest `05b18b55243fed5de2d6417dc98e7e385f0249cde1cd2bf472d1769c6b975e22`.",
  "status": "available",
  "evidence_grade": "executable",
  "scope": {
    "kind": "bounded",
    "statement": "all four-subsets of the 100 points in {0,1,...,9}^2 and all four-subsets of the displayed 20-point witness",
    "bounds": {
      "grid_points": {
        "min": 100,
        "max": 100
      },
      "grid_four_subsets": {
        "min": 3921225,
        "max": 3921225
      },
      "witness_points": {
        "min": 20,
        "max": 20
      },
      "witness_four_subsets": {
        "min": 4845,
        "max": 4845
      }
    },
    "exhaustive": true
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "partial",
    "kind": "inline_python_computation",
    "entrypoint": "Join source_lines with LF characters and execute the resulting Python program",
    "runtime": "CPython 3, standard library only",
    "citation": {
      "url": "https://arxiv.org/abs/2112.12716",
      "locator": "Self-contained Python standard-library computation executed on 2026-07-25"
    },
    "inline_source": [
      "from collections import Counter",
      "from hashlib import sha256",
      "from itertools import combinations",
      "from json import dumps",
      "",
      "N=10",
      "grid=tuple((x,y) for x in range(N) for y in range(N))",
      "witness=frozenset(((2,2),(2,3),(2,4),(3,2),(3,3),(3,4),(3,5),",
      "                   (4,1),(4,2),(4,3),(4,4),(4,5),",
      "                   (5,1),(5,2),(5,3),(5,4),(5,5),(6,2),(6,3),(6,4)))",
      "",
      "def is_square(vertices):",
      "    distances=sorted((a[0]-b[0])**2+(a[1]-b[1])**2",
      "                     for a,b in combinations(vertices,2))",
      "    return (distances[0]>0 and distances[:4]==[distances[0]]*4",
      "            and distances[4:]==[2*distances[0]]*2)",
      "",
      "grid_squares=tuple(q for q in combinations(grid,4) if is_square(q))",
      "witness_squares=tuple(q for q in grid_squares if set(q)<=witness)",
      "independent_check=tuple(q for q in combinations(sorted(witness),4)",
      "                        if is_square(q))",
      "assert len(grid)==100 and len(grid_squares)==825",
      "assert len(witness)==20 and witness_squares==independent_check",
      "assert len(witness_squares)==32",
      "",
      "side_histogram=Counter(",
      "    min((a[0]-b[0])**2+(a[1]-b[1])**2 for a,b in combinations(q,2))",
      "    for q in witness_squares)",
      "assert sorted(side_histogram.items())==[(1,11),(2,8),(4,4),(5,7),(8,1),(10,1)]",
      "",
      "upper_bounds={17:22}",
      "for n in (18,19,20):",
      "    upper_bounds[n]=(n*upper_bounds[n-1])//(n-4)",
      "assert upper_bounds=={17:22,18:28,19:35,20:43}",
      "",
      "point_text='\\n'.join(f'{x},{y}' for x,y in sorted(witness))+'\\n'",
      "square_text='\\n'.join(';'.join(f'{x},{y}' for x,y in q)",
      "                          for q in witness_squares)+'\\n'",
      "report={",
      "    'grid_points':len(grid),",
      "    'grid_side_points':N,",
      "    'grid_squares':len(grid_squares),",
      "    'side_squared_histogram':sorted(side_histogram.items()),",
      "    'upper_bounds_from_S17':sorted(upper_bounds.items()),",
      "    'witness_point_sha256':sha256(point_text.encode()).hexdigest(),",
      "    'witness_points':len(witness),",
      "    'witness_square_sha256':sha256(square_text.encode()).hexdigest(),",
      "    'witness_squares':len(witness_squares),",
      "}",
      "assert report['witness_point_sha256']=='abf6c3e7bde7d49fd54c2ce2e3ee7503a469797aa200ad62ab09bc1594a5bd77'",
      "assert report['witness_square_sha256']=='6c44a24e1b8a7a1cfb59815218f4f1a9af988ad41c3e114f05772ec5094c682c'",
      "payload=dumps(report,sort_keys=True,separators=(',',':'))",
      "assert sha256(payload.encode()).hexdigest()=='05b18b55243fed5de2d6417dc98e7e385f0249cde1cd2bf472d1769c6b975e22'",
      "print(payload)"
    ],
    "missing": [
      "command",
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://arxiv.org/abs/2112.12716",
    "locator": "Self-contained Python standard-library computation executed on 2026-07-25"
  },
  "models": [],
  "relations": [
    {
      "slug": "R797",
      "title": "The maximum lies between 32 and 43",
      "object_type": "claim",
      "relation": "supports",
      "direction": "outgoing"
    },
    {
      "slug": "twenty-points-ten-grid-max-squares",
      "title": "twenty points ten grid max squares",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}