Problem packetResearch packetR207
Eight points satisfy both restrictions
Link to a section
The record reports a computation within its stated scope.
Recorded status: established
Recorded scope: the stated eight-point subset of {0,...,8}^2
Complete recorded scope and conditions
{
"kind": "bounded",
"statement": "the stated eight-point subset of {0,...,8}^2",
"bounds": {
"grid_side": {
"min": 9,
"max": 9
},
"set_size": {
"min": 8,
"max": 8
}
},
"exhaustive": true
}Originating problem: Distinct-distance general-position sets in the 9 by 9 grid
Recorded relationships: The exact value is G_9=8
Authored record and scope
- Authored title
- Eight points satisfy both restrictions
- Record type
- claim
- Stored status
- established
- Evidence grade
- computational
- Recorded scope data
- { "kind": "bounded", "statement": "the stated eight-point subset of {0,...,8}^2", "bounds": { "grid_side": { "min": 9, "max": 9 }, "set_size": { "min": 8, "max": 8 } }, "exhaustive": true }
- Linked research record IDs
- R208
2Authored explanation
Take \[ S=\{(6,0),(8,8),(1,1),(1,3),(8,7),(5,7),(5,1),(6,5)\}. \] Its sorted squared-distance list is \[ [1,2,4,5,8,9,10,13,16,17,20,25,26,29,32,34,36,41,45,50,52,53,58,65,68,74,85,98]. \] The list has \(\binom82=28\) entries and no repetition. For each of the \(\binom83=56\) triples, the verifier evaluates the integer cross product \[ (x_2-x_1)(y_3-y_1)-(y_2-y_1)(x_3-x_1). \] Every value is nonzero. Hence \(S\) has distinct mutual distances and no three collinear points.
Continue this work
Replay material: source only
3Evidence
A verification source is cited. This record has no executable replay attached.
Verification source: doi.org ↗, Direct integer verification in ddg9-artifact-exhaustive-nine-search
4What was measured
5How it connects
Supports
- claim
Recorded for
- problem
Cite this record
Cite the original sources separately.
Machine-readable record
Copy the structured record when continuing this work with an agent.
{
"schema": "theoremdb-agent-record-v1",
"ref": "R207",
"content_hash": null,
"slug": "ddg9-claim-eight-point-witness",
"type": "claim",
"title": "Eight points satisfy both restrictions",
"summary": "The candidate witness has 28 distinct squared distances and all 56 of its triples have nonzero signed area.",
"relevance": "This records a result, observation, or conjecture used to assess the target problem.",
"relevance_source": "derived",
"body": "Take\n\\[\nS=\\{(6,0),(8,8),(1,1),(1,3),(8,7),(5,7),(5,1),(6,5)\\}.\n\\]\nIts sorted squared-distance list is\n\\[\n[1,2,4,5,8,9,10,13,16,17,20,25,26,29,32,34,36,41,45,50,52,53,58,65,68,74,85,98].\n\\]\nThe list has \\(\\binom82=28\\) entries and no repetition. For each of the \\(\\binom83=56\\) triples, the verifier evaluates the integer cross product\n\\[\n(x_2-x_1)(y_3-y_1)-(y_2-y_1)(x_3-x_1).\n\\]\nEvery value is nonzero. Hence \\(S\\) has distinct mutual distances and no three collinear points.",
"status": "established",
"evidence_grade": "computational",
"scope": {
"kind": "bounded",
"statement": "the stated eight-point subset of {0,...,8}^2",
"bounds": {
"grid_side": {
"min": 9,
"max": 9
},
"set_size": {
"min": 8,
"max": 8
}
},
"exhaustive": true
},
"reproduction": {
"schema": "theoremdb-reproduction-v1",
"readiness": "source_only",
"kind": "claim",
"citation": {
"url": "https://doi.org/10.1007/BF01299744",
"locator": "Direct integer verification in ddg9-artifact-exhaustive-nine-search"
},
"missing": [
"source",
"command",
"runtime",
"expected_output"
]
},
"formal_statement": null,
"source": {
"url": "https://doi.org/10.1007/BF01299744",
"locator": "Direct integer verification in ddg9-artifact-exhaustive-nine-search"
},
"models": [],
"continuation": null,
"relations": [
{
"slug": "R208",
"title": "The exact value is G_9=8",
"object_type": "claim",
"relation": "supports",
"direction": "outgoing"
},
{
"slug": "distinct-distance-grid-9",
"title": "distinct distance grid 9",
"object_type": "problem",
"relation": "recorded_for",
"direction": "outgoing"
}
]
}7Provenance
View source, identifiers, and projection details
A statement this project treats as settled at the recorded evidence grade, with the work that backs it.