{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R779",
  "content_hash": null,
  "slug": "tfs-artifact-coordinates-and-contact-graph",
  "type": "artifact",
  "title": "Explicit coordinates and a rational separation certificate",
  "summary": "Exact integer comparisons certify all 105 normalized dot products and recover the 30-edge contact graph.",
  "relevance": "For Tammes separation for fifteen points on the sphere, record tfs-artifact-coordinates-and-contact-graph (“Explicit coordinates and a rational separation certificate”) supplies evidence or a replay used to check the packet. The record states: Exact integer comparisons certify all 105 normalized dot products and recover the 30-edge contact graph.",
  "relevance_source": "recorded",
  "body": "Download the cited 15-point coordinate file lawfully from the Hardin-Sloane-Smith library and pass its local path to the checker. Number its vectors in file order and put \\(u_i=v_i/\\lVert v_i\\rVert\\). Every decimal token is treated as an exact rational number. The checker verifies the source-file and normalized-token hashes before using the coordinates. The source coordinates are not stored in this packet.\n\nExact squared comparisons prove\n\\[\nu_i\\mathbin{\\cdot}u_j<0.5926059032\n\\quad(i\\ne j).\n\\]\nThus these published decimals alone certify a minimum angle greater than \\(\\arccos(0.5926059032)=53.6578501103\\ldots^\\circ\\). This is a rigorous lower bound for the normalized decimal realization. The exact algebraic construction in the first claim has the slightly larger endpoint \\(\\arccos(\\alpha)\\).\n\nThe 30 pairs with normalized inner product above 0.5926059008 are\n```\n1-4 1-9 1-10 1-13 2-3 2-7 2-11 2-12 3-8 3-9\n3-10 4-5 4-9 4-11 5-6 5-7 5-15 6-7 6-12 6-14\n6-15 7-11 7-12 8-10 8-14 9-10 10-13 12-14 13-14 13-15\n```\nEvery other normalized inner product is below 0.424696, leaving a gap larger than 0.1679 between contacts and noncontacts. This gap makes the contact graph insensitive to the source's rounding. The largest decimal-model inner product belongs to pair 13-14.",
  "status": "available",
  "evidence_grade": "executable",
  "scope": {
    "kind": "bounded",
    "statement": "the 45 decimal coordinate tokens in the Hardin-Sloane-Smith 15-point file, treated as exact rationals and normalized point by point",
    "bounds": {
      "points": {
        "min": 15,
        "max": 15
      },
      "pairs": {
        "min": 105,
        "max": 105
      },
      "near_contact_pairs": {
        "min": 30,
        "max": 30
      }
    },
    "exhaustive": true
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "partial",
    "kind": "inline_python_exact_rational_certificate",
    "entrypoint": "Join source_lines with LF characters, save as check.py, download pack.3.15.txt from source_url, then run python3 check.py /local/path/pack.3.15.txt",
    "runtime": "CPython 3.10 or newer, standard library only",
    "citation": {
      "url": "https://neilsloane.com/packings/dim3/pack.3.15.txt",
      "locator": "Hardin-Sloane-Smith dimension-three packing library, 15 consecutive vectors. Source-file SHA-256 recorded by the candidate audit: d1a1d120faf0a7a69441fb8a42ea741da2209b5bd2c45819d16648a49fe0b10f."
    },
    "outputs": "source_tokens_sha256=21ae48600f58f33bc0450daccd1c7acc6e44fd98ece86be825356a057cc2209f\npoints=15 pairs=105 contact_edges=30\ncosine_certificate=max_dot<0.5926059032 noncontact_max<0.424696\nclosest_pair_decimal_model=13-14 angle_degrees=53.657850116162\npolynomial_root_interval=[0.5926059029250737,0.5926059029250738]\nincumbent_angle_degrees=53.657850129933\narea_upper_bound_degrees=59.852869733228\n",
    "inline_source": [
      "from fractions import Fraction as F",
      "from hashlib import sha256",
      "from itertools import combinations",
      "from math import acos, degrees, sqrt",
      "from pathlib import Path",
      "from sys import argv",
      "",
      "if len(argv) != 2:",
      "    raise SystemExit('usage: python3 check.py /local/path/pack.3.15.txt')",
      "blob = Path(argv[1]).read_bytes()",
      "assert sha256(blob).hexdigest() == 'd1a1d120faf0a7a69441fb8a42ea741da2209b5bd2c45819d16648a49fe0b10f'",
      "tokens = blob.decode('ascii').split()",
      "assert len(tokens) == 45",
      "canonical_tokens = ' '.join(tokens)",
      "assert sha256(canonical_tokens.encode()).hexdigest() == '21ae48600f58f33bc0450daccd1c7acc6e44fd98ece86be825356a057cc2209f'",
      "values = [F(token) for token in tokens]",
      "points = [values[i:i+3] for i in range(0, 45, 3)]",
      "norm2 = [sum(x*x for x in point) for point in points]",
      "assert all(F('0.9999999999999999') < n < F('1.0000000000000003') for n in norm2)",
      "",
      "expected_edges = {(1,4),(1,9),(1,10),(1,13),(2,3),(2,7),(2,11),(2,12),",
      "                  (3,8),(3,9),(3,10),(4,5),(4,9),(4,11),(5,6),(5,7),",
      "                  (5,15),(6,7),(6,12),(6,14),(6,15),(7,11),(7,12),",
      "                  (8,10),(8,14),(9,10),(10,13),(12,14),(13,14),(13,15)}",
      "contact_floor = F('0.5926059008')",
      "all_pair_ceiling = F('0.5926059032')",
      "noncontact_ceiling = F('0.424696')",
      "edges = set()",
      "decimal_dots = []",
      "for i, j in combinations(range(15), 2):",
      "    dot = sum(points[i][k]*points[j][k] for k in range(3))",
      "    product = norm2[i]*norm2[j]",
      "    if dot > 0 and dot*dot > contact_floor*contact_floor*product:",
      "        edges.add((i+1, j+1))",
      "    if dot > 0:",
      "        assert dot*dot < all_pair_ceiling*all_pair_ceiling*product",
      "    decimal_dots.append((float(dot)/sqrt(float(product)), i+1, j+1))",
      "assert edges == expected_edges",
      "for i, j in combinations(range(15), 2):",
      "    if (i+1, j+1) in edges:",
      "        continue",
      "    dot = sum(points[i][k]*points[j][k] for k in range(3))",
      "    if dot > 0:",
      "        assert dot*dot < noncontact_ceiling*noncontact_ceiling*norm2[i]*norm2[j]",
      "",
      "p = lambda x: 13*x**5-x**4+6*x**3+2*x**2-3*x-1",
      "dp = lambda x: 65*x**4-4*x**3+18*x**2+4*x-3",
      "lo = F(5926059029250737, 10**16)",
      "hi = F(5926059029250738, 10**16)",
      "a, b = F(59,100), F(3,5)",
      "assert p(lo) < 0 < p(hi)",
      "assert dp(a) > 0",
      "assert 260*a**3-12*b**2+36*a+4 > 0",
      "",
      "maximum = max(decimal_dots)",
      "print('source_tokens_sha256=21ae48600f58f33bc0450daccd1c7acc6e44fd98ece86be825356a057cc2209f')",
      "print(f'points={len(points)} pairs={len(decimal_dots)} contact_edges={len(edges)}')",
      "print('cosine_certificate=max_dot<0.5926059032 noncontact_max<0.424696')",
      "print(f'closest_pair_decimal_model={maximum[1]}-{maximum[2]} angle_degrees={degrees(acos(maximum[0])):.12f}')",
      "print('polynomial_root_interval=[0.5926059029250737,0.5926059029250738]')",
      "print(f'incumbent_angle_degrees={degrees(acos((float(lo)+float(hi))/2)):.12f}')",
      "print(f'area_upper_bound_degrees={2*degrees(acos(13/15)):.12f}')"
    ],
    "missing": [
      "command"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://neilsloane.com/packings/dim3/pack.3.15.txt",
    "locator": "Hardin-Sloane-Smith dimension-three packing library, 15 consecutive vectors. Source-file SHA-256 recorded by the candidate audit: d1a1d120faf0a7a69441fb8a42ea741da2209b5bd2c45819d16648a49fe0b10f."
  },
  "models": [],
  "relations": [
    {
      "slug": "R780",
      "title": "The best published construction has an exact algebraic separation",
      "object_type": "claim",
      "relation": "evidences",
      "direction": "outgoing"
    },
    {
      "slug": "tammes-fifteen-separation",
      "title": "tammes fifteen separation",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}