{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R787",
  "content_hash": null,
  "slug": "tlef15-artifact-construction-and-upper-bound",
  "type": "artifact",
  "title": "Executable construction and parity upper-bound certificate",
  "summary": "A standard-library program verifies the 33-point witness and proves alpha(T_7)=12 by exhaustive hypergraph branching.",
  "relevance": "For Largest equilateral-triangle-free subset of the fifteen-row triangular lattice, record tlef15-artifact-construction-and-upper-bound (“Executable construction and parity upper-bound certificate”) supplies evidence or a replay used to check the packet. The record states: A standard-library program verifies the 33-point witness and proves alpha(T_7)=12 by exhaustive hypergraph branching.",
  "relevance_source": "recorded",
  "body": "The search represents a candidate vertex set by a bit mask. If it contains a triangle, every independent subset must omit at least one vertex of that triangle, so the search branches on its three deletions. A branch with fewer than 13 candidates fails. A triangle-free candidate mask would certify a 13-point set, while memoization merges identical masks. The complete search visits 409,531 calls and 136,510 distinct masks and finds no such set. A checked 12-point witness establishes \\(\\alpha(T_7)=12\\).\n\nThe same program verifies the 33-point \\(T_{15}\\) construction, checks the triangle totals, and confirms the four parity-class sizes used in the upper bound.",
  "status": "available",
  "evidence_grade": "executable",
  "scope": {
    "kind": "bounded",
    "statement": "exact enumeration on T_15, exact verification of the 33-point witness, and exhaustive exclusion of a 13-point triangle-free subset of T_7",
    "bounds": {
      "t15_vertices": {
        "min": 120,
        "max": 120
      },
      "t15_triangles": {
        "min": 2380,
        "max": 2380
      },
      "t7_search_states": {
        "min": 136510,
        "max": 136510
      }
    },
    "exhaustive": true
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "partial",
    "kind": "inline_python_exact_computation",
    "entrypoint": "Join source_lines with LF characters and execute the resulting Python program",
    "runtime": "Python 3.10 or newer, standard library",
    "citation": {
      "url": "https://arxiv.org/abs/2405.12321",
      "locator": "Python 3.10 standard-library computation executed by TheoremDB entry research on 2026-07-25"
    },
    "inline_source": [
      "import itertools",
      "",
      "def lattice(n):",
      "    return tuple((i, j) for i in range(n) for j in range(n - i))",
      "",
      "def triangles(points):",
      "    index = {p: k for k, p in enumerate(points)}",
      "    result = set()",
      "    for a, b in itertools.combinations(points, 2):",
      "        d = (b[0] - a[0], b[1] - a[1])",
      "        for r in ((-d[1], d[0] + d[1]), (d[0] + d[1], -d[0])):",
      "            c = (a[0] + r[0], a[1] + r[1])",
      "            if c in index:",
      "                result.add(sum(1 << index[p] for p in (a, b, c)))",
      "    return tuple(sorted(result))",
      "",
      "def verify_independent(points, edges, witness):",
      "    index = {p: k for k, p in enumerate(points)}",
      "    mask = sum(1 << index[p] for p in witness)",
      "    return len(witness) == len(set(witness)) and all(edge & mask != edge for edge in edges)",
      "",
      "witness15 = ((0,4),(0,6),(0,7),(0,10),(0,11),(0,14),(1,4),(1,5),(1,7),(1,9),(1,11),(1,13),(2,7),(2,8),(2,11),(2,12),(3,2),(3,3),(4,1),(5,0),(6,0),(7,0),(7,1),(7,2),(8,2),(9,1),(10,0),(11,0),(11,1),(11,2),(12,2),(13,1),(14,0))",
      "witness7 = ((0,0),(0,1),(0,2),(0,3),(0,5),(1,3),(1,5),(2,2),(3,1),(4,0),(5,1),(6,0))",
      "p15 = lattice(15)",
      "e15 = triangles(p15)",
      "p7 = lattice(7)",
      "e7 = triangles(p7)",
      "assert (len(p15), len(e15)) == (120, 2380)",
      "assert (len(p7), len(e7)) == (28, 126)",
      "assert verify_independent(p15, e15, witness15)",
      "assert verify_independent(p7, e7, witness7)",
      "",
      "seen = set()",
      "nodes = 0",
      "def independent_13_exists(candidates):",
      "    global nodes",
      "    nodes += 1",
      "    if candidates.bit_count() < 13:",
      "        return False",
      "    if candidates in seen:",
      "        return False",
      "    seen.add(candidates)",
      "    edge = next((edge for edge in e7 if edge & candidates == edge), None)",
      "    if edge is None:",
      "        return True",
      "    return any(independent_13_exists(candidates & ~(1 << v)) for v in range(28) if edge >> v & 1)",
      "",
      "assert not independent_13_exists((1 << 28) - 1)",
      "assert (nodes, len(seen)) == (409531, 136510)",
      "classes = {(a, b): [] for a in range(2) for b in range(2)}",
      "for p in p15:",
      "    classes[(p[0] % 2, p[1] % 2)].append(p)",
      "class_sizes = tuple(len(classes[r]) for r in ((0,0),(0,1),(1,0),(1,1)))",
      "assert class_sizes == (36, 28, 28, 28)",
      "upper = 20 + 3 * 12",
      "out = f'T15 vertices=120 triangles=2380 witness=33; T7 vertices=28 triangles=126 witness=12 independent13=0 nodes={nodes} states={len(seen)}; parity_sizes={class_sizes} upper={upper}'",
      "print(out)"
    ],
    "missing": [
      "command",
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://arxiv.org/abs/2405.12321",
    "locator": "Python 3.10 standard-library computation executed by TheoremDB entry research on 2026-07-25"
  },
  "models": [],
  "relations": [
    {
      "slug": "R790",
      "title": "A 33-point equilateral-triangle-free set",
      "object_type": "claim",
      "relation": "reproduces",
      "direction": "outgoing"
    },
    {
      "slug": "R789",
      "title": "The current certified interval is 33 through 56",
      "object_type": "claim",
      "relation": "supports",
      "direction": "outgoing"
    },
    {
      "slug": "triangular-lattice-15-equilateral-free",
      "title": "triangular lattice 15 equilateral free",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}