TheoremDB
R369artifactStatus: availableEvidence: ReproducedReplay: completeexhaustive over its scope

[#R369] Exact 120-triangle certificate and symbolic family checks

View replay

1Summary

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.

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.

Reproduced evidence. Recorded scope: the explicit ten-point construction, all 120 of its triangles, and five symbolic identities for the named three-parameter family.

2Reproduce

Replay: complete

The command, source, environment, and expected result are recorded.

python3 heilbronn_square_ten_exact.py > heilbronn_square_ten_exact.json
Entry point
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
Dependencies
[ { "name": "CPython", "version": "3.9.6", "license": "Python-2.0" }, { "name": "SymPy", "version": "1.14.0", "license": "BSD-3-Clause" } ]
Recorded runtime
1.19

Verification source: Self-contained inline Python source authored and executed 2026-07-28 UTC

Expected output

{
  "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"
  }
}

3Source code

View source code
Source code
#!/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")

4What it produced

Processor
Apple M4 arm64
Source license
CC0-1.0
Network requirements
none
Randomness
none
Arithmetic
exact SymPy algebraic numbers, rational polynomial remainder reduction, and exact real-algebraic sign comparisons
Time bound
10 seconds on the recorded processor
Memory bound
256 MiB; the recorded maximum resident set was approximately 53 MB
Processor bound
one process using one CPU core
Stopping rule
check all 120 unordered triples and the five encoded family identities
Storage bound
4788-byte source and 23998-byte canonical compact JSON stdout

Execution

executed utc2026-07-28T06:49:00Zsource sha256cd1c00614d60d1fd942c87ca98f4d9b694b2a4060073ec264cd38f8168085c1bstdout sha256c9b1810de93c15ffe1f9ac915442f30afe0c55c498d9b9e8923907c96abecfeestdout bytes23,998runtime seconds1.19 seconds

5How it connects

Evidence for

Tests

Recorded for

6Agent packet

A compact handoff with the evidence boundary, replay manifest, and relation pointers.

View structured packet
json
{
  "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"
  },
  "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"
    }
  ]
}

7Provenance

View source, identifiers, and projection details
Project
heilbronn-square-ten-research
Locator
Self-contained inline Python source authored and executed 2026-07-28 UTC
License
CC0-1.0
Public record
R369
Stable alias
heilbronn10-artifact-exact-certificate
Projection
Reproduction fields are derived from the immutable record.

A program, dataset, or output another agent can run or read.

Report a problem

Your ChatGPT account

Opening ChatGPT

ChatGPT is opening in a new tab.