{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R369",
  "content_hash": null,
  "slug": "heilbronn10-artifact-exact-certificate",
  "type": "artifact",
  "title": "Exact 120-triangle certificate and symbolic family checks",
  "summary": "A self-contained SymPy replay reconstructs the algebraic point set, reduces every triangle area modulo the cubic, and checks the identities and sign brackets used by the family argument.",
  "relevance": "For Exact ten-point Heilbronn number in the unit square, record heilbronn10-artifact-exact-certificate (“Exact 120-triangle certificate and symbolic family checks”) supplies evidence or a replay used to check the packet. The record states: A self-contained SymPy replay reconstructs the algebraic point set, reduces every triangle area modulo the cubic, and checks the identities and sign brackets used by the family argument.",
  "relevance_source": "recorded",
  "body": "The script defines \\(z\\) as the isolated real root of the cubic, constructs the ten exact points, and checks coordinate containment and distinctness. It computes every triangle determinant, reduces it in \\(\\mathbb Q[z]/(f)\\), proves all 120 areas are at least \\(A\\), and prints every exact row. It also checks five symbolic identities or inequalities used in the family upper-bound argument. The artifact checks the algebra behind the proposed family theorem. A human proof review remains appropriate.",
  "status": "available",
  "evidence_grade": "executable",
  "scope": {
    "kind": "bounded",
    "statement": "the explicit ten-point construction, all 120 of its triangles, and five symbolic identities for the named three-parameter family",
    "bounds": {
      "n": {
        "min": 10,
        "max": 10
      },
      "triangle_count": {
        "min": 120,
        "max": 120
      },
      "symbolic_identity_count": {
        "min": 5,
        "max": 5
      }
    },
    "exhaustive": true
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "complete",
    "kind": "inline_python_exact_algebra_certificate",
    "command": "python3 heilbronn_square_ten_exact.py > heilbronn_square_ten_exact.json",
    "entrypoint": "Join source_lines with LF, append a terminal LF, and save as heilbronn_square_ten_exact.py",
    "runtime": "CPython 3.9.6 with SymPy 1.14.0, macOS 26.2 arm64",
    "citation": {
      "locator": "Self-contained inline Python source authored and executed 2026-07-28 UTC"
    },
    "dependencies": [
      {
        "name": "CPython",
        "version": "3.9.6",
        "license": "Python-2.0"
      },
      {
        "name": "SymPy",
        "version": "1.14.0",
        "license": "BSD-3-Clause"
      }
    ],
    "outputs": {
      "format": "one canonical compact JSON object followed by LF",
      "source_bytes": 4788,
      "source_lines": 153,
      "source_sha256": "cd1c00614d60d1fd942c87ca98f4d9b694b2a4060073ec264cd38f8168085c1b",
      "stdout_bytes": 23998,
      "stdout_sha256": "c9b1810de93c15ffe1f9ac915442f30afe0c55c498d9b9e8923907c96abecfee",
      "expected": {
        "triangle_count": 120,
        "equality_triangle_count": 16,
        "strict_triangle_count": 104,
        "distinct_area_form_count": 23,
        "minimum_area_decimal_40": "0.04653741958254177256161176810014551328871"
      }
    },
    "runtime_seconds": 1.19,
    "inline_source": [
      "#!/usr/bin/env python3",
      "import itertools",
      "import json",
      "import platform",
      "import sys",
      "",
      "import sympy as sp",
      "",
      "",
      "u = sp.symbols(\"u\")",
      "f = 12 * u**3 - 27 * u**2 + 20 * u - 4",
      "z = sp.CRootOf(f, 0)",
      "x = z / 2",
      "y = (1 - z) * (1 - 2 * z)",
      "A = 5 * z**2 / 8 - z**3 / 2",
      "",
      "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),",
      "]",
      "",
      "",
      "def reduce_in_u(expr):",
      "    substituted = sp.together(sp.sympify(expr).xreplace({z: u}))",
      "    numerator, denominator = sp.fraction(substituted)",
      "    reduced = sp.rem(sp.Poly(numerator, u), sp.Poly(f, u)).as_expr()",
      "    return sp.factor(reduced / denominator)",
      "",
      "",
      "def exact_area(i, j, k):",
      "    p, q, r = points[i], points[j], points[k]",
      "    determinant = sp.expand(",
      "        p[0] * (q[1] - r[1])",
      "        + q[0] * (r[1] - p[1])",
      "        + r[0] * (p[1] - q[1])",
      "    )",
      "    sign = sp.sign(determinant)",
      "    assert sign in (-1, 1)",
      "    return reduce_in_u(sign * determinant / 2)",
      "",
      "",
      "assert sp.count_roots(f, sp.Rational(3, 10), sp.Rational(1, 3)) == 1",
      "assert sp.discriminant(f, u) == -2976",
      "for px, py in points:",
      "    assert 0 <= px <= 1 and 0 <= py <= 1",
      "assert len(set(points)) == 10",
      "",
      "target = reduce_in_u(A)",
      "rows = []",
      "for triple in itertools.combinations(range(10), 3):",
      "    area = exact_area(*triple)",
      "    difference = reduce_in_u(area - A)",
      "    difference_at_root = difference.xreplace({u: z})",
      "    assert difference_at_root >= 0",
      "    rows.append(",
      "        {",
      "            \"triple\": list(triple),",
      "            \"area_in_Q_u_mod_f\": str(area),",
      "            \"difference_from_A_in_Q_u_mod_f\": str(difference),",
      "            \"area_decimal_30\": str(sp.N(area.xreplace({u: z}), 30)),",
      "            \"equals_A\": bool(difference == 0),",
      "        }",
      "    )",
      "",
      "strict_rows = [row for row in rows if not row[\"equals_A\"]]",
      "second_value = min(",
      "    sp.sympify(row[\"area_in_Q_u_mod_f\"]).xreplace({u: z}) for row in strict_rows",
      ")",
      "second_rows = [",
      "    row",
      "    for row in strict_rows",
      "    if sp.sympify(row[\"area_in_Q_u_mod_f\"]).xreplace({u: z}) == second_value",
      "]",
      "",
      "X, Y, Z, T = sp.symbols(\"X Y Z T\")",
      "P = X * (1 - X - Y)",
      "Q = Y * (1 - 2 * Z)",
      "R = Z * (1 - X + Y) - Y",
      "L = T / (1 - 2 * Z)",
      "U = 1 - (T + (1 - Z) * L) / Z",
      "vertex = (1 - L) / 2",
      "h = (2 * Z**3 - 5 * Z**2 + 2 * Z) / (4 - 6 * Z)",
      "N = T * (4 - 7 * Z) + 2 * Z**2 - Z",
      "H = (6 * Z - 4) * T + 2 * Z**3 - 5 * Z**2 + 2 * Z",
      "assert sp.factor(vertex - U - N / (2 * Z * (1 - 2 * Z))) == 0",
      "assert sp.factor(U * (1 - U - L) - T - T * H / (Z**2 * (1 - 2 * Z))) == 0",
      "assert sp.factor(sp.diff(h, Z) + f.xreplace({u: Z}) / (2 * (3 * Z - 2) ** 2)) == 0",
      "assert sp.Rational(31, 100) < z < sp.Rational(8, 25)",
      "t0 = 2 * A",
      "assert sp.Rational(9, 100) < t0 < sp.Rational(1, 10)",
      "stress_discriminant = 49 * t0**2 - 18 * t0 + 1",
      "assert stress_discriminant < 0",
      "assert reduce_in_u(h.xreplace({Z: z}) - t0) == 0",
      "",
      "certificate = {",
      "    \"schema\": \"heilbronn-square-ten-exact-certificate-v1\",",
      "    \"runtime\": {",
      "        \"python\": platform.python_version(),",
      "        \"sympy\": sp.__version__,",
      "        \"platform\": platform.platform(),",
      "    },",
      "    \"minimal_polynomial\": str(f),",
      "    \"isolating_interval\": [\"3/10\", \"1/3\"],",
      "    \"root_decimal_40\": str(sp.N(z, 40)),",
      "    \"coordinates\": [",
      "        [str(reduce_in_u(px)), str(reduce_in_u(py))] for px, py in points",
      "    ],",
      "    \"minimum_area_in_Q_u_mod_f\": str(target),",
      "    \"minimum_area_decimal_40\": str(sp.N(A, 40)),",
      "    \"triangle_count\": len(rows),",
      "    \"equality_triangle_count\": sum(row[\"equals_A\"] for row in rows),",
      "    \"strict_triangle_count\": len(strict_rows),",
      "    \"distinct_area_form_count\": len({row[\"area_in_Q_u_mod_f\"] for row in rows}),",
      "    \"equality_triples\": [row[\"triple\"] for row in rows if row[\"equals_A\"]],",
      "    \"second_smallest_area_decimal_40\": str(sp.N(second_value, 40)),",
      "    \"second_smallest_triples\": [row[\"triple\"] for row in second_rows],",
      "    \"second_smallest_gap_in_Q_u_mod_f\": str(",
      "        reduce_in_u(",
      "            sp.sympify(second_rows[0][\"area_in_Q_u_mod_f\"]).xreplace({u: z}) - A",
      "        )",
      "    ),",
      "    \"family_upper_algebra\": {",
      "        \"three_double_areas\": [str(P), str(Q), str(R)],",
      "        \"fixed_z_envelope\": str(sp.factor(h)),",
      "        \"envelope_derivative\": str(sp.factor(sp.diff(h, Z))),",
      "        \"root_sign_bracket\": [\"31/100\", \"8/25\"],",
      "        \"f_at_root_bracket_endpoints\": [",
      "            str(f.subs(u, sp.Rational(31, 100))),",
      "            str(f.subs(u, sp.Rational(8, 25))),",
      "        ],",
      "        \"t0_sign_bracket\": [\"9/100\", \"1/10\"],",
      "        \"vertex_gap_numerator\": str(N),",
      "        \"vertex_gap_discriminant_in_Q_u_mod_f\": str(",
      "            reduce_in_u(stress_discriminant)",
      "        ),",
      "        \"vertex_gap_discriminant_at_t0_decimal_30\": str(",
      "            sp.N(stress_discriminant, 30)",
      "        ),",
      "        \"identities_checked\": 5,",
      "    },",
      "    \"triangles\": rows,",
      "}",
      "",
      "payload = json.dumps(certificate, sort_keys=True, separators=(\",\", \":\"))",
      "sys.stdout.write(payload + \"\\n\")"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": null,
    "locator": "Self-contained inline Python source authored and executed 2026-07-28 UTC"
  },
  "models": [],
  "continuation": null,
  "relations": [
    {
      "slug": "R374",
      "title": "The exact Comellas–Yebra construction has minimum area 0.0465374195825...",
      "object_type": "claim",
      "relation": "evidences",
      "direction": "outgoing"
    },
    {
      "slug": "R376",
      "title": "The Comellas–Yebra three-parameter family has exact maximum 0.0465374195825...",
      "object_type": "claim",
      "relation": "tests",
      "direction": "outgoing"
    },
    {
      "slug": "heilbronn-square-ten",
      "title": "heilbronn square ten",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}