TheoremDB

Problem packetResearch packetR229

R229Executable evidence

Complete seven-point branch certificate

View replayOpen source ↗
Link to a section

Authored summary

The direct search visits 4,699,843 admissible partial sets and finds no valid seven-point leaf.

Executable material is recorded. Successful replay is a separate check.

Recorded status: available

Recorded scope: every seven-element subset of the 9 by 9 point grid {0,...,8}^2

Complete recorded scope and conditions
{
  "kind": "bounded",
  "statement": "every seven-element subset of the 9 by 9 point grid {0,...,8}^2",
  "bounds": {
    "coordinate_minimum": {
      "min": 0,
      "max": 0
    },
    "coordinate_maximum": {
      "min": 8,
      "max": 8
    },
    "candidate_points": {
      "min": 81,
      "max": 81
    },
    "set_size": {
      "min": 7,
      "max": 7
    }
  },
  "exhaustive": true
}

Originating problem: Distinct nonzero triangle areas in the 9 by 9 grid

Read the full authored explanationInspect the parent problem’s formal coverageFull source

Recorded relationships: The exact maximum is A_9=6

Authored record and scope
Authored title
Complete seven-point branch certificate
Record type
artifact
Stored status
available
Evidence grade
executable
Recorded scope data
{ "kind": "bounded", "statement": "every seven-element subset of the 9 by 9 point grid {0,...,8}^2", "bounds": { "coordinate_minimum": { "min": 0, "max": 0 }, "coordinate_maximum": { "min": 8, "max": 8 }, "candidate_points": { "min": 81, "max": 81 }, "set_size": { "min": 7, "max": 7 } }, "exhaustive": true }
Linked research record IDs
R231

2Authored explanation

Points are ordered first by \(x\), then by \(y\), and every subset has one increasing representation in this order. A 128-bit mask stores the positive doubled areas already used. At depth \(d\), adding a point creates \(\binom d2\) new triangles. A zero determinant causes a collinearity rejection. A repeated bit within the new values or against the stored mask causes an area-collision rejection. The loop's shortage cutoff merely leaves enough later points to reach seven.

The exhaustive run visits 4,699,843 admissible nodes. It rejects 2,963,134 extensions for a zero area and 44,877,104 for a repeated positive area, out of 52,540,080 candidate extensions. Visit counts by selected-set size are \[ [1,75,2850,70770,983307,3255572,387268,0]. \] The terminal zero proves nonexistence at size seven. A running FNV-1a trace of the depth, next index, and both halves of the area mask ends at `ade14ba0a60dc0f4`.

Before the search, the same executable checks all 20 triangles of the displayed six-point witness. Its stable six-line output has SHA-256 digest `ab06239e5dd989c76cf8fcf77971fe67eb844118219c1d6ab47102319d75a916`.

Files and source

Files embedded in this record. Matching a file hash confirms its identity.

  • R229.txt4,988 bytes · No SHA-256 recorded
    Preview R229.txt
    #include <array>
#include <cstdint>
#include <cstdlib>
#include <iostream>
#include <vector>

using Mask = unsigned __int128;
struct Point { int x; int y; };
constexpr int side = 9;
constexpr int point_count = side * side;
constexpr int target = 7;
std::array<Point, point_count> points{};
std::vector<int> chosen;
std::array<std::uint64_t, target + 1> visits{};
std::array<std::uint64_t, target + 1> zero_rejects{};
std::array<std::uint64_t, target + 1> collision_rejects{};
std::uint64_t trace = 14695981039346656037ULL;

void mix(std::uint64_t value) {
    for (int shift = 0; shift < 64; shift += 8) {
        trace ^= (value >> shift) & 255U;
        trace *= 1099511628211ULL;
    }
}

int area(Point a, Point b, Point c) {
    return std::abs(
        (b.x-a.x)*(c.y-a.y)-(b.y-a.y)*(c.x-a.x)
    );
}

bool search(int next, Mask used) {
    const int depth = static_cast<int>(chosen.size());
    ++visits[depth];
    mix(depth);
    mix(next);
    mix(static_cast<std::uint64_t>(used));
    mix(static_cast<std::uint64_t>(used >> 64));
    if (depth == target) {
        return true;
    }
    const int need = target - depth;
    for (int candidate = next;
         candidate <= point_count - need;
         ++candidate) {
        Mask added = 0;
        bool ok = true;
        bool zero = false;
        for (int i = 0; i < depth && ok; ++i) {
            for (int j = i + 1; j < depth; ++j) {
                const int value = area(
                    points[chosen[i]],
                    points[chosen[j]],
                    points[candidate]
                );
                if (value > 64) {
                    std::abort();
                }
                if (value == 0) {
                    ok = false;
                    zero = true;
                    break;
                }
                const Mask bit = Mask(1) << value;
                if ((used | added) & bit) {
                    ok = false;
                    break;
                }
                added |= bit;
            }
        }
        if (!ok) {
            if (zero) {
                ++zero_rejects[depth];
            } else {
                ++collision_rejects[depth];
            }
            continue;
        }
        chosen.push_back(candidate);
        if (search(candidate + 1, used | added)) {
            return true;
        }
        chosen.pop_back();
    }
    return false;
}

int main() {
    int index = 0;
    for (int x = 0; x < side; ++x) {
        for (int y = 0; y < side; ++y) {
            points[index++] = {x,y};
        }
    }
    const std::array<Point, 6> witness{{
        {8,7},{2,7},{3,6},{0,2},{7,1},{1,0}
    }};
    Mask witness_areas = 0;
    int witness_count = 0;
    int witness_maximum = 0;
    for (int i = 0; i < 6; ++i) {
        for (int j = i + 1; j < 6; ++j) {
            for (int k = j + 1; k < 6; ++k) {
                const int value = area(witness[i],witness[j],witness[k]);
                const Mask bit = Mask(1) << value;
                if (value == 0 || (witness_areas & bit)) {
                    return 2;
                }
                witness_areas |= bit;
                ++witness_count;
                if (value > witness_maximum) {
                    witness_maximum = value;
                }
            }
        }
    }
    if (witness_count != 20 || witness_maximum != 43) {
        return 2;
    }

    const bool found = search(0, 0);
    const std::array<std::uint64_t, target + 1> expected_visits{
        1,75,2850,70770,983307,3255572,387268,0
    };
    const std::array<std::uint64_t, target + 1> expected_zero{
        0,0,2380,99030,1123039,1667461,71224,0
    };
    const std::array<std::uint64_t, target + 1> expected_collision{
        0,0,0,285233,10086511,31936257,2569103,0
    };
    if (found || visits != expected_visits
        || zero_rejects != expected_zero
        || collision_rejects != expected_collision
        || trace != 0xade14ba0a60dc0f4ULL) {
        return 3;
    }

    std::uint64_t node_total = 0;
    std::uint64_t zero_total = 0;
    std::uint64_t collision_total = 0;
    for (auto value : visits) node_total += value;
    for (auto value : zero_rejects) zero_total += value;
    for (auto value : collision_rejects) collision_total += value;
    std::cout << "witness 6 triangles " << witness_count
              << " maximum_area " << witness_maximum << "\n";
    std::cout << "target 7 found 0 nodes " << node_total
              << " zero_rejects " << zero_total
              << " collision_rejects " << collision_total << "\n";
    std::cout << "visits";
    for (auto value : visits) std::cout << " " << value;
    std::cout << "\nzero";
    for (int d = 0; d < target; ++d) {
        std::cout << " " << zero_rejects[d];
    }
    std::cout << "\ncollision";
    for (int d = 0; d < target; ++d) {
        std::cout << " " << collision_rejects[d];
    }
    std::cout << "\ntrace_fnv1a64 " << std::hex << trace
              << std::dec << "\n";
}
    File identity
    Recorded filename
    R229.txt
    Download SHA-256
    12d98ec860bb76f4ce6d0bbd2eeb42914df8552700c362f4f5428d33277f4642
Continue this work
Replay material: partial

4Reproduce

Replay package: partial

Part of the replay path is recorded. Check the missing fields before comparing a new run.

Entry point
join source_lines with newline, compile with the stated command, and run
Runtime
C++20 standard library with the GCC or Clang unsigned __int128 extension

Verification source: oeis.org ↗, Inline C++20 source compiled and executed by TheoremDB entry research on 2026-07-24

Missing for a complete replay: command, expected output.

Recorded artifact fields
Kind
inline_cpp20_computation
Entry point
join source_lines with newline, compile with the stated command, and run
Environment
C++20 standard library with the GCC or Clang unsigned __int128 extension

5What it produced

Compiler command
c++ -x c++ -std=c++20 -O3 -Wall -Wextra
Expected stdout lines
witness 6 triangles 20 maximum_area 43, target 7 found 0 nodes 4699843 zero_rejects 2963134 collision_rejects 44877104, visits 1 75 2850 70770 983307 3255572 387268 0, zero 0 0 2380 99030 1123039 1667461 71224, collision 0 0 0 285233 10086511 31936257 2569103, trace_fnv1a64 ade14ba0a60dc0f4
Stdout sha256
ab06239e5dd989c76cf8fcf77971fe67eb844118219c1d6ab47102319d75a916
Candidate extensions
52,540,080
Admissible nodes
4,699,843
Zero area rejections
2,963,134
Area collision rejections
44,877,104
Complete candidates
0
Trace fnv1a64
ade14ba0a60dc0f4
Node counts by depth
1, 75, 2,850, 70,770, 983,307, 3,255,572, 387,268, 0
Zero rejections by depth
0, 0, 2,380, 99,030, 1,123,039, 1,667,461, 71,224
Collision rejections by depth
0, 0, 0, 285,233, 10,086,511, 31,936,257, 2,569,103

Execution

date2026-07-24arithmeticexact integer determinants and bit-mask operationssymmetry reductionnoneadmissible nodes4,699,843stdout sha256ab06239e5dd989c76cf8fcf77971fe67eb844118219c1d6ab47102319d75a916

6How it connects

Evidence for

Recorded for

Machine-readable record

Copy the structured record when continuing this work with an agent.

json
{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R229",
  "content_hash": null,
  "slug": "dta9-artifact-complete-seven-search",
  "type": "artifact",
  "title": "Complete seven-point branch certificate",
  "summary": "The direct search visits 4,699,843 admissible partial sets and finds no valid seven-point leaf.",
  "relevance": "This supplies a computation, dataset, or executable check used to assess the target problem.",
  "relevance_source": "derived",
  "body": "Points are ordered first by \\(x\\), then by \\(y\\), and every subset has one increasing representation in this order. A 128-bit mask stores the positive doubled areas already used. At depth \\(d\\), adding a point creates \\(\\binom d2\\) new triangles. A zero determinant causes a collinearity rejection. A repeated bit within the new values or against the stored mask causes an area-collision rejection. The loop's shortage cutoff merely leaves enough later points to reach seven.\n\nThe exhaustive run visits 4,699,843 admissible nodes. It rejects 2,963,134 extensions for a zero area and 44,877,104 for a repeated positive area, out of 52,540,080 candidate extensions. Visit counts by selected-set size are\n\\[\n[1,75,2850,70770,983307,3255572,387268,0].\n\\]\nThe terminal zero proves nonexistence at size seven. A running FNV-1a trace of the depth, next index, and both halves of the area mask ends at `ade14ba0a60dc0f4`.\n\nBefore the search, the same executable checks all 20 triangles of the displayed six-point witness. Its stable six-line output has SHA-256 digest `ab06239e5dd989c76cf8fcf77971fe67eb844118219c1d6ab47102319d75a916`.",
  "status": "available",
  "evidence_grade": "executable",
  "scope": {
    "kind": "bounded",
    "statement": "every seven-element subset of the 9 by 9 point grid {0,...,8}^2",
    "bounds": {
      "coordinate_minimum": {
        "min": 0,
        "max": 0
      },
      "coordinate_maximum": {
        "min": 8,
        "max": 8
      },
      "candidate_points": {
        "min": 81,
        "max": 81
      },
      "set_size": {
        "min": 7,
        "max": 7
      }
    },
    "exhaustive": true
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "partial",
    "kind": "inline_cpp20_computation",
    "entrypoint": "join source_lines with newline, compile with the stated command, and run",
    "runtime": "C++20 standard library with the GCC or Clang unsigned __int128 extension",
    "citation": {
      "url": "https://oeis.org/A322740",
      "locator": "Inline C++20 source compiled and executed by TheoremDB entry research on 2026-07-24"
    },
    "inline_source": [
      "#include <array>",
      "#include <cstdint>",
      "#include <cstdlib>",
      "#include <iostream>",
      "#include <vector>",
      "",
      "using Mask = unsigned __int128;",
      "struct Point { int x; int y; };",
      "constexpr int side = 9;",
      "constexpr int point_count = side * side;",
      "constexpr int target = 7;",
      "std::array<Point, point_count> points{};",
      "std::vector<int> chosen;",
      "std::array<std::uint64_t, target + 1> visits{};",
      "std::array<std::uint64_t, target + 1> zero_rejects{};",
      "std::array<std::uint64_t, target + 1> collision_rejects{};",
      "std::uint64_t trace = 14695981039346656037ULL;",
      "",
      "void mix(std::uint64_t value) {",
      "    for (int shift = 0; shift < 64; shift += 8) {",
      "        trace ^= (value >> shift) & 255U;",
      "        trace *= 1099511628211ULL;",
      "    }",
      "}",
      "",
      "int area(Point a, Point b, Point c) {",
      "    return std::abs(",
      "        (b.x-a.x)*(c.y-a.y)-(b.y-a.y)*(c.x-a.x)",
      "    );",
      "}",
      "",
      "bool search(int next, Mask used) {",
      "    const int depth = static_cast<int>(chosen.size());",
      "    ++visits[depth];",
      "    mix(depth);",
      "    mix(next);",
      "    mix(static_cast<std::uint64_t>(used));",
      "    mix(static_cast<std::uint64_t>(used >> 64));",
      "    if (depth == target) {",
      "        return true;",
      "    }",
      "    const int need = target - depth;",
      "    for (int candidate = next;",
      "         candidate <= point_count - need;",
      "         ++candidate) {",
      "        Mask added = 0;",
      "        bool ok = true;",
      "        bool zero = false;",
      "        for (int i = 0; i < depth && ok; ++i) {",
      "            for (int j = i + 1; j < depth; ++j) {",
      "                const int value = area(",
      "                    points[chosen[i]],",
      "                    points[chosen[j]],",
      "                    points[candidate]",
      "                );",
      "                if (value > 64) {",
      "                    std::abort();",
      "                }",
      "                if (value == 0) {",
      "                    ok = false;",
      "                    zero = true;",
      "                    break;",
      "                }",
      "                const Mask bit = Mask(1) << value;",
      "                if ((used | added) & bit) {",
      "                    ok = false;",
      "                    break;",
      "                }",
      "                added |= bit;",
      "            }",
      "        }",
      "        if (!ok) {",
      "            if (zero) {",
      "                ++zero_rejects[depth];",
      "            } else {",
      "                ++collision_rejects[depth];",
      "            }",
      "            continue;",
      "        }",
      "        chosen.push_back(candidate);",
      "        if (search(candidate + 1, used | added)) {",
      "            return true;",
      "        }",
      "        chosen.pop_back();",
      "    }",
      "    return false;",
      "}",
      "",
      "int main() {",
      "    int index = 0;",
      "    for (int x = 0; x < side; ++x) {",
      "        for (int y = 0; y < side; ++y) {",
      "            points[index++] = {x,y};",
      "        }",
      "    }",
      "    const std::array<Point, 6> witness{{",
      "        {8,7},{2,7},{3,6},{0,2},{7,1},{1,0}",
      "    }};",
      "    Mask witness_areas = 0;",
      "    int witness_count = 0;",
      "    int witness_maximum = 0;",
      "    for (int i = 0; i < 6; ++i) {",
      "        for (int j = i + 1; j < 6; ++j) {",
      "            for (int k = j + 1; k < 6; ++k) {",
      "                const int value = area(witness[i],witness[j],witness[k]);",
      "                const Mask bit = Mask(1) << value;",
      "                if (value == 0 || (witness_areas & bit)) {",
      "                    return 2;",
      "                }",
      "                witness_areas |= bit;",
      "                ++witness_count;",
      "                if (value > witness_maximum) {",
      "                    witness_maximum = value;",
      "                }",
      "            }",
      "        }",
      "    }",
      "    if (witness_count != 20 || witness_maximum != 43) {",
      "        return 2;",
      "    }",
      "",
      "    const bool found = search(0, 0);",
      "    const std::array<std::uint64_t, target + 1> expected_visits{",
      "        1,75,2850,70770,983307,3255572,387268,0",
      "    };",
      "    const std::array<std::uint64_t, target + 1> expected_zero{",
      "        0,0,2380,99030,1123039,1667461,71224,0",
      "    };",
      "    const std::array<std::uint64_t, target + 1> expected_collision{",
      "        0,0,0,285233,10086511,31936257,2569103,0",
      "    };",
      "    if (found || visits != expected_visits",
      "        || zero_rejects != expected_zero",
      "        || collision_rejects != expected_collision",
      "        || trace != 0xade14ba0a60dc0f4ULL) {",
      "        return 3;",
      "    }",
      "",
      "    std::uint64_t node_total = 0;",
      "    std::uint64_t zero_total = 0;",
      "    std::uint64_t collision_total = 0;",
      "    for (auto value : visits) node_total += value;",
      "    for (auto value : zero_rejects) zero_total += value;",
      "    for (auto value : collision_rejects) collision_total += value;",
      "    std::cout << \"witness 6 triangles \" << witness_count",
      "              << \" maximum_area \" << witness_maximum << \"\\n\";",
      "    std::cout << \"target 7 found 0 nodes \" << node_total",
      "              << \" zero_rejects \" << zero_total",
      "              << \" collision_rejects \" << collision_total << \"\\n\";",
      "    std::cout << \"visits\";",
      "    for (auto value : visits) std::cout << \" \" << value;",
      "    std::cout << \"\\nzero\";",
      "    for (int d = 0; d < target; ++d) {",
      "        std::cout << \" \" << zero_rejects[d];",
      "    }",
      "    std::cout << \"\\ncollision\";",
      "    for (int d = 0; d < target; ++d) {",
      "        std::cout << \" \" << collision_rejects[d];",
      "    }",
      "    std::cout << \"\\ntrace_fnv1a64 \" << std::hex << trace",
      "              << std::dec << \"\\n\";",
      "}"
    ],
    "missing": [
      "command",
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://oeis.org/A322740",
    "locator": "Inline C++20 source compiled and executed by TheoremDB entry research on 2026-07-24"
  },
  "models": [],
  "continuation": null,
  "relations": [
    {
      "slug": "R231",
      "title": "The exact maximum is A_9=6",
      "object_type": "claim",
      "relation": "evidences",
      "direction": "outgoing"
    },
    {
      "slug": "distinct-triangle-areas-grid-9",
      "title": "distinct triangle areas grid 9",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}

8Provenance

View source, identifiers, and projection details
Project
distinct-triangle-areas-grid-9
Locator
Inline C++20 source compiled and executed by TheoremDB entry research on 2026-07-24
License
CC0-1.0
Contributors
TheoremDB entry research, 2026-07-24
Source
oeis.org ↗
Public record
R229
Stable alias
dta9-artifact-complete-seven-search
Projection
Reproduction fields are derived from the immutable record.

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

Sign in to follow

Sign in in another tab, then return here.

Open sign-in in another tab

Report a problem

Report location:

Your ChatGPT account

Opening ChatGPT

ChatGPT is opening in a new tab.