{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R370",
  "content_hash": null,
  "slug": "heilbronn10-artifact-symmetric-family-cover",
  "type": "artifact",
  "title": "Exact rational interval cover for the symmetric family",
  "summary": "A standard-library branch-and-bound closes the whole ordered parameter cube at threshold 0.0465376 using five witness triangles and exact dyadic rational interval arithmetic.",
  "relevance": "For Exact ten-point Heilbronn number in the unit square, record heilbronn10-artifact-symmetric-family-cover (“Exact rational interval cover for the symmetric family”) supplies evidence or a replay used to check the packet. The record states: A standard-library branch-and-bound closes the whole ordered parameter cube at threshold 0.0465376 using five witness triangles and exact dyadic rational interval arithmetic.",
  "relevance_source": "recorded",
  "body": "The script forms all 120 signed determinant polynomials for the ten affine points. For each dyadic box in \\([0,1/2]^3\\), it computes exact termwise rational bounds. A box closes once one of five fixed witness determinants lies throughout \\([-2T,2T]\\), which proves that every configuration in that box has a triangle of area at most \\(T\\). Ordered-infeasible boxes are pruned exactly. At \\(T=14543/312500=0.0465376\\), the run closes the family after 649,645 nodes. The analytic family theorem is sharper; this artifact records an independent computational route and its scaling boundary.",
  "status": "available",
  "evidence_grade": "executable",
  "scope": {
    "kind": "family",
    "statement": "all ordered parameters 0 <= x <= y <= z <= 1/2 in the listed ten-point affine boundary ansatz at threshold 14543/312500",
    "family": "Comellas-Yebra diagonal-reflection and half-turn symmetric three-parameter boundary family"
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "complete",
    "kind": "inline_python_exact_rational_branch_and_bound",
    "command": "python3 heilbronn_square_ten_symmetric_family.py 14543 312500 > heilbronn_square_ten_symmetric_family.json",
    "entrypoint": "Join source_lines with LF, append a terminal LF, and save as heilbronn_square_ten_symmetric_family.py",
    "runtime": "CPython 3.9.6 standard library, macOS 26.2 arm64",
    "citation": {
      "locator": "Self-contained inline Python exact-rational interval program authored and executed 2026-07-28 UTC"
    },
    "dependencies": [
      {
        "name": "CPython standard library",
        "version": "3.9.6",
        "license": "Python-2.0"
      }
    ],
    "outputs": {
      "format": "one canonical compact JSON object followed by LF",
      "source_bytes": 7019,
      "source_lines": 239,
      "source_sha256": "9ea2153e6f2d1d1a113fb189bff5b3f7b11bb9999a5196bb1aa1d48e34043138",
      "stdout_bytes": 2066,
      "stdout_sha256": "a0dac5d917b053526d6ff793e8eff3f9435679d33746affc24c5034e72569eae",
      "expected": {
        "threshold": "14543/312500",
        "nodes": 649645,
        "witness_prunes": 324651,
        "order_infeasible_prunes": 172,
        "maximum_depth": 62,
        "complete_cover": true,
        "open_boxes": 0,
        "terminal_cover_sha256": "6189a6f48b64cdf2801525747c7e51bbce1f952485e6c188e4c6a4fb70877e6d"
      }
    },
    "runtime_seconds": 101.48,
    "inline_source": [
      "#!/usr/bin/env python3",
      "import hashlib",
      "import itertools",
      "import json",
      "import platform",
      "import sys",
      "from collections import Counter",
      "from fractions import Fraction as F",
      "",
      "",
      "ZERO = {}",
      "ONE = {(0, 0, 0): F(1)}",
      "X = {(1, 0, 0): F(1)}",
      "Y = {(0, 1, 0): F(1)}",
      "Z = {(0, 0, 1): F(1)}",
      "",
      "",
      "def add(a, b):",
      "    result = dict(a)",
      "    for monomial, coefficient in b.items():",
      "        result[monomial] = result.get(monomial, F(0)) + coefficient",
      "        if result[monomial] == 0:",
      "            del result[monomial]",
      "    return result",
      "",
      "",
      "def neg(a):",
      "    return {monomial: -coefficient for monomial, coefficient in a.items()}",
      "",
      "",
      "def sub(a, b):",
      "    return add(a, neg(b))",
      "",
      "",
      "def mul(a, b):",
      "    result = {}",
      "    for left_power, left_coefficient in a.items():",
      "        for right_power, right_coefficient in b.items():",
      "            power = tuple(left_power[i] + right_power[i] for i in range(3))",
      "            result[power] = (",
      "                result.get(power, F(0)) + left_coefficient * right_coefficient",
      "            )",
      "    return {power: coefficient for power, coefficient in result.items() if coefficient}",
      "",
      "",
      "def determinant(p, q, r):",
      "    return add(",
      "        add(",
      "            mul(p[0], sub(q[1], r[1])),",
      "            mul(q[0], sub(r[1], p[1])),",
      "        ),",
      "        mul(r[0], sub(p[1], q[1])),",
      "    )",
      "",
      "",
      "def polynomial_text(poly):",
      "    terms = []",
      "    for powers, coefficient in sorted(poly.items(), reverse=True):",
      "        terms.append(",
      "            {",
      "                \"powers_xyz\": list(powers),",
      "                \"coefficient\": str(coefficient),",
      "            }",
      "        )",
      "    return terms",
      "",
      "",
      "def interval(poly, box):",
      "    lower = F(0)",
      "    upper = F(0)",
      "    for powers, coefficient in poly.items():",
      "        monomial_lower = F(1)",
      "        monomial_upper = F(1)",
      "        for axis, power in enumerate(powers):",
      "            monomial_lower *= box[axis][0] ** power",
      "            monomial_upper *= box[axis][1] ** power",
      "        if coefficient >= 0:",
      "            lower += coefficient * monomial_lower",
      "            upper += coefficient * monomial_upper",
      "        else:",
      "            lower += coefficient * monomial_upper",
      "            upper += coefficient * monomial_lower",
      "    return lower, upper",
      "",
      "",
      "def ordered_region_empty(box):",
      "    x_interval, y_interval, z_interval = box",
      "    return (",
      "        x_interval[0] > y_interval[1]",
      "        or y_interval[0] > z_interval[1]",
      "        or max(x_interval[0], y_interval[0]) > min(y_interval[1], z_interval[1])",
      "    )",
      "",
      "",
      "def split_box(box):",
      "    widths = [high - low for low, high in box]",
      "    axis = max(range(3), key=lambda index: (widths[index], -index))",
      "    low, high = box[axis]",
      "    middle = (low + high) / 2",
      "    left = list(box)",
      "    right = list(box)",
      "    left[axis] = (low, middle)",
      "    right[axis] = (middle, high)",
      "    return tuple(left), tuple(right)",
      "",
      "",
      "def terminal_line(kind, witness, depth, box):",
      "    witness_text = \"-\" if witness is None else \",\".join(map(str, witness))",
      "    fields = [kind, witness_text, str(depth)]",
      "    fields.extend(",
      "        f\"{low.numerator}/{low.denominator}:{high.numerator}/{high.denominator}\"",
      "        for low, high in box",
      "    )",
      "    return \"|\".join(fields) + \"\\n\"",
      "",
      "",
      "points = [",
      "    (X, ZERO),",
      "    (sub(ONE, Y), ZERO),",
      "    (ZERO, X),",
      "    (ONE, Y),",
      "    (sub(ONE, Z), Z),",
      "    (Z, sub(ONE, Z)),",
      "    (ZERO, sub(ONE, Y)),",
      "    (ONE, sub(ONE, X)),",
      "    (Y, ONE),",
      "    (sub(ONE, X), ONE),",
      "]",
      "all_determinants = {",
      "    triple: determinant(*(points[index] for index in triple))",
      "    for triple in itertools.combinations(range(10), 3)",
      "}",
      "",
      "# These five triangles covered every terminal box in an exploratory all-120 run.",
      "witnesses = [",
      "    (1, 4, 5),",
      "    (0, 5, 8),",
      "    (0, 1, 2),",
      "    (1, 3, 4),",
      "    (0, 4, 7),",
      "]",
      "if len(sys.argv) not in (1, 3, 4):",
      "    raise SystemExit(",
      "        \"usage: heilbronn_family.py [THRESHOLD_NUM THRESHOLD_DEN [MAX_NODES]]\"",
      "    )",
      "threshold = (",
      "    F(2327, 50000)",
      "    if len(sys.argv) == 1",
      "    else F(int(sys.argv[1]), int(sys.argv[2]))",
      ")",
      "max_nodes = None if len(sys.argv) < 4 else int(sys.argv[3])",
      "twice_threshold = 2 * threshold",
      "initial_box = ((F(0), F(1, 2)),) * 3",
      "stack = [(initial_box, 0)]",
      "nodes = 0",
      "order_prunes = 0",
      "witness_prunes = Counter()",
      "maximum_depth = 0",
      "cover_hasher = hashlib.sha256()",
      "",
      "while stack and (max_nodes is None or nodes < max_nodes):",
      "    box, depth = stack.pop()",
      "    nodes += 1",
      "    maximum_depth = max(maximum_depth, depth)",
      "    if ordered_region_empty(box):",
      "        order_prunes += 1",
      "        cover_hasher.update(terminal_line(\"order\", None, depth, box).encode())",
      "        continue",
      "    found = None",
      "    for triple in witnesses:",
      "        lower, upper = interval(all_determinants[triple], box)",
      "        if max(abs(lower), abs(upper)) <= twice_threshold:",
      "            found = triple",
      "            break",
      "    if found is not None:",
      "        witness_prunes[found] += 1",
      "        cover_hasher.update(terminal_line(\"witness\", found, depth, box).encode())",
      "        continue",
      "    left, right = split_box(box)",
      "    stack.append((right, depth + 1))",
      "    stack.append((left, depth + 1))",
      "",
      "complete = not stack",
      "if complete:",
      "    assert nodes == 2 * (sum(witness_prunes.values()) + order_prunes) - 1",
      "if threshold == F(2327, 50000) and max_nodes is None:",
      "    assert nodes == 153907",
      "    assert sum(witness_prunes.values()) == 76782",
      "    assert order_prunes == 172",
      "if threshold == F(14543, 312500) and max_nodes is None:",
      "    assert nodes == 649645",
      "    assert sum(witness_prunes.values()) == 324651",
      "    assert order_prunes == 172",
      "",
      "result = {",
      "    \"schema\": \"heilbronn-square-ten-symmetric-family-cover-v1\",",
      "    \"runtime\": {",
      "        \"python\": platform.python_version(),",
      "        \"platform\": platform.platform(),",
      "    },",
      "    \"family\": \"0 <= x <= y <= z <= 1/2 with the ten listed affine boundary points\",",
      "    \"points\": [",
      "        [\"x\", \"0\"],",
      "        [\"1-y\", \"0\"],",
      "        [\"0\", \"x\"],",
      "        [\"1\", \"y\"],",
      "        [\"1-z\", \"z\"],",
      "        [\"z\", \"1-z\"],",
      "        [\"0\", \"1-y\"],",
      "        [\"1\", \"1-x\"],",
      "        [\"y\", \"1\"],",
      "        [\"1-x\", \"1\"],",
      "    ],",
      "    \"scope_caveat\": \"The coordinate ansatz and ordering define a three-parameter family. They do not reduce arbitrary ten-point configurations to this family.\",",
      "    \"threshold\": str(threshold),",
      "    \"threshold_decimal\": format(float(threshold), \".12g\"),",
      "    \"arithmetic\": \"fractions.Fraction exact rational arithmetic\",",
      "    \"interval_rule\": \"A box closes when one witness determinant has an interval contained in [-2T,2T].\",",
      "    \"split_rule\": \"Bisect a longest coordinate interval; ties choose x, then y, then z.\",",
      "    \"all_triangle_polynomial_count\": len(all_determinants),",
      "    \"witnesses\": [",
      "        {",
      "            \"triple\": list(triple),",
      "            \"determinant_polynomial\": polynomial_text(all_determinants[triple]),",
      "            \"boxes_closed\": witness_prunes[triple],",
      "        }",
      "        for triple in witnesses",
      "    ],",
      "    \"nodes\": nodes,",
      "    \"witness_prunes\": sum(witness_prunes.values()),",
      "    \"order_infeasible_prunes\": order_prunes,",
      "    \"maximum_depth\": maximum_depth,",
      "    \"terminal_cover_sha256\": cover_hasher.hexdigest(),",
      "    \"complete_cover\": complete,",
      "    \"open_boxes\": len(stack),",
      "    \"node_cap\": max_nodes,",
      "}",
      "json.dump(result, sys.stdout, sort_keys=True, separators=(\",\", \":\"))",
      "sys.stdout.write(\"\\n\")"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": null,
    "locator": "Self-contained inline Python exact-rational interval program authored and executed 2026-07-28 UTC"
  },
  "models": [],
  "continuation": null,
  "relations": [
    {
      "slug": "R376",
      "title": "The Comellas–Yebra three-parameter family has exact maximum 0.0465374195825...",
      "object_type": "claim",
      "relation": "tests",
      "direction": "outgoing"
    },
    {
      "slug": "R372",
      "title": "Cover the symmetric family by exact determinant intervals",
      "object_type": "attempt",
      "relation": "uses",
      "direction": "incoming"
    },
    {
      "slug": "heilbronn-square-ten",
      "title": "heilbronn square ten",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}