{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R423",
  "content_hash": null,
  "slug": "iso7-claim-exact-maximum-ten",
  "type": "claim",
  "title": "The exact maximum is I_7=10",
  "summary": "A ten-point set has no repeated pair of distances in any triple, and exhaustive search excludes eleven points.",
  "relevance": "This records a result, observation, or conjecture used to assess the target problem.",
  "relevance_source": "derived",
  "body": "The set\n\\[\n\\{(0,0),(0,1),(0,3),(0,4),(1,6),(2,6),(5,5),(5,6),(6,3),(6,4)\\}\n\\]\nhas ten points. Checking its \\(\\binom{10}{3}=120\\) triples shows that the three squared distances in each triple are different. This proves \\(I_7\\geq10\\).\n\nForm a 3-uniform hypergraph on the 49 grid points. An unordered triple is a hyperedge exactly when two of its three squared distances agree. This definition includes equally spaced collinear triples. Direct enumeration gives 2,488 hyperedges, and valid point sets are precisely the independent sets of this hypergraph.\n\nThe executable certificate enumerates every increasing eleven-element candidate. A branch is rejected when its new point completes a hyperedge with two selected points. The search reaches no depth-eleven leaf. Since the condition passes to subsets, every valid set with at least eleven points would contain an independent eleven-set. Hence \\(I_7\\leq10\\), and\n\\[\nI_7=10.\n\\]\n\nPatternBoost reports the same value \\(f(7)=10\\) under its explicitly stated possibly-flat convention. Its authors used SAT solvers to prove optimality for small grids. The independent certificate here reproduces the seven-by-seven case.",
  "status": "established",
  "evidence_grade": "reproduced",
  "scope": {
    "kind": "bounded",
    "statement": "all subsets of {0,...,6}^2, with collinear equally spaced triples included among the forbidden isosceles triples",
    "bounds": {
      "coordinate_minimum": {
        "min": 0,
        "max": 0
      },
      "coordinate_maximum": {
        "min": 6,
        "max": 6
      },
      "grid_points": {
        "min": 49,
        "max": 49
      },
      "set_size": {
        "min": 10,
        "max": 11
      }
    },
    "exhaustive": true
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "source_only",
    "kind": "claim",
    "citation": {
      "url": "https://arxiv.org/abs/2411.00566",
      "locator": "François Charton, Jordan S. Ellenberg, Adam Zsolt Wagner, and Geordie Williamson, PatternBoost: Constructions in Mathematics with a Little Help from AI, arXiv:2411.00566, section 4.1 and Figure 11; independent artifact iso7-artifact-complete-eleven-search"
    },
    "missing": [
      "source",
      "command",
      "runtime",
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://arxiv.org/abs/2411.00566",
    "locator": "François Charton, Jordan S. Ellenberg, Adam Zsolt Wagner, and Geordie Williamson, PatternBoost: Constructions in Mathematics with a Little Help from AI, arXiv:2411.00566, section 4.1 and Figure 11; independent artifact iso7-artifact-complete-eleven-search"
  },
  "models": [],
  "continuation": null,
  "relations": [
    {
      "slug": "R421",
      "title": "Complete eleven-point independent-set certificate",
      "object_type": "artifact",
      "relation": "evidences",
      "direction": "incoming"
    },
    {
      "slug": "R422",
      "title": "PatternBoost already gives the exact seven-grid value",
      "object_type": "attempt",
      "relation": "supports",
      "direction": "incoming"
    },
    {
      "slug": "no-isosceles-grid-7",
      "title": "no isosceles grid 7",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}