{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R780",
  "content_hash": null,
  "slug": "tfs-claim-exact-incumbent",
  "type": "claim",
  "title": "The best published construction has an exact algebraic separation",
  "summary": "A 15-point code exists with minimum angle arccos(alpha), where alpha is the isolated root 0.5926059029250737... of a degree-five polynomial.",
  "relevance": "For Tammes separation for fifteen points on the sphere, record tfs-claim-exact-incumbent (“The best published construction has an exact algebraic separation”) records a bound, answer, status fact, or structural consequence. The record states: A 15-point code exists with minimum angle arccos(alpha), where alpha is the isolated root 0.5926059029250737...",
  "relevance_source": "recorded",
  "body": "Let \\(\\alpha\\) be the unique root in\n\\[\n0.5926059029250737<\\alpha<0.5926059029250738\n\\]\nof\n\\[\n13x^5-x^4+6x^3+2x^2-3x-1=0.\n\\]\nHenry Cohn's spherical-code table gives a 15-point code in \\(\\mathbb R^3\\) whose largest pairwise inner product is exactly \\(\\alpha\\). The table explains that a listed minimal polynomial means an exact code attaining that value has been checked to exist. Hence\n\\[\n\\theta_{15}\\geq\\arccos(\\alpha)\n=53.65785012993268\\ldots^\\circ.\n\\]\nThe corresponding minimum chordal distance is\n\\[\n\\sqrt{2-2\\alpha}=0.9026561882299664\\ldots.\n\\]\nThe polynomial signs at the two rational endpoints have opposite signs. Its derivative is positive throughout \\([0.59,0.60]\\), which isolates the stated root. The accompanying artifact checks these facts with exact rational arithmetic.",
  "status": "established",
  "evidence_grade": "sourced",
  "scope": {
    "kind": "bounded",
    "statement": "a spherical code of exactly 15 points on the unit sphere in R^3",
    "bounds": {
      "ambient_dimension": {
        "min": 3,
        "max": 3
      },
      "points": {
        "min": 15,
        "max": 15
      }
    },
    "exhaustive": false
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "source_only",
    "kind": "claim",
    "citation": {
      "url": "https://www.spherical-codes.org/",
      "locator": "Dimension 3, 15 points. The entry gives cosine 0.592605902926 without an optimality asterisk and links coordinates. The table introduction states that a listed minimal polynomial certifies existence of an exact code. The plain-text polynomial table gives 13x^5-x^4+6x^3+2x^2-3x-1."
    },
    "missing": [
      "source",
      "command",
      "runtime",
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://www.spherical-codes.org/",
    "locator": "Dimension 3, 15 points. The entry gives cosine 0.592605902926 without an optimality asterisk and links coordinates. The table introduction states that a listed minimal polynomial certifies existence of an exact code. The plain-text polynomial table gives 13x^5-x^4+6x^3+2x^2-3x-1."
  },
  "models": [],
  "relations": [
    {
      "slug": "R781",
      "title": "Global optimality for fifteen points remains open",
      "object_type": "claim",
      "relation": "bounds",
      "direction": "outgoing"
    },
    {
      "slug": "R779",
      "title": "Explicit coordinates and a rational separation certificate",
      "object_type": "artifact",
      "relation": "evidences",
      "direction": "incoming"
    },
    {
      "slug": "tammes-fifteen-separation",
      "title": "tammes fifteen separation",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}