TheoremDB

Problem packetResearch packetR366

R366Executable evidence

Replayable exact transfer sweep through strip length 3000

View replayOpen source ↗
Link to a section

Authored summary

Standard-library Python regenerates every coefficient with integers, tests every adjacent triple, and hashes eight checkpoint rows.

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

Recorded status: available

Recorded scope: all independence-polynomial coefficients and all internal log-concavity inequalities for 1 <= n <= 3000, with a full seven-mask transfer cross-check for 1 <= n <= 20

Complete recorded scope and conditions
{
  "kind": "bounded",
  "statement": "all independence-polynomial coefficients and all internal log-concavity inequalities for 1 <= n <= 3000, with a full seven-mask transfer cross-check for 1 <= n <= 20",
  "bounds": {
    "strip_length": {
      "min": 1,
      "max": 3000
    },
    "seven_state_crosscheck_length": {
      "min": 1,
      "max": 20
    },
    "inequalities_checked": {
      "min": 9000000,
      "max": 9000000
    }
  },
  "exhaustive": true
}

Originating problem: Hard-core coefficient log-concavity on the first ten thousand four-cycle strips

Authored record and scope
Authored title
Replayable exact transfer sweep through strip length 3000
Record type
artifact
Stored status
available
Evidence grade
executable
Recorded scope data
{ "kind": "bounded", "statement": "all independence-polynomial coefficients and all internal log-concavity inequalities for 1 <= n <= 3000, with a full seven-mask transfer cross-check for 1 <= n <= 20", "bounds": { "strip_length": { "min": 1, "max": 3000 }, "seven_state_crosscheck_length": { "min": 1, "max": 20 }, "inequalities_checked": { "min": 9000000, "max": 9000000 } }, "exhaustive": true }

2Authored explanation

The program implements the three-state transfer displayed in the claim. A separate seven-state calculation uses the masks \([0,1,2,4,5,8,10]\), admits consecutive masks exactly when their bitwise intersection is zero, and matches every reduced-transfer row through \(n=20\).

For each length, the program computes every integer margin before advancing the transfer. It records the least margin and verifies the observed closed form for that minimum. The SHA-256 summary covers one line per length containing \(n\), the minimizing index, the margin, and its adjacent coefficient triple. Eight complete coefficient rows are serialized with fixed-width length prefixes and hashed separately.

The reproduced run took 131.73 seconds on the entry-research host. Raising `LAST_N` continues the same exact calculation. Runtime grows steeply because both the number and bit length of the coefficients increase. A run through 10000 should use checkpointing or a faster big-integer backend.

Files and source

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

  • R366.txt4,246 bytes · No SHA-256 recorded
    Preview R366.txt
    from hashlib import sha256
    from json import dumps
    from struct import pack
    
    LAST_N = 3000
    ANCHORS = {1, 2, 40, 100, 500, 1000, 2000, 3000}
    MASKS = [m for m in range(16) if not (m & ((m << 1) | (m >> 3)))]
    assert MASKS == [0, 1, 2, 4, 5, 8, 10]
    
    def add_rows(rows):
        size = max(map(len, rows))
        return [sum(row[k] if k < len(row) else 0 for row in rows) for k in range(size)]
    
    def shift(row, amount):
        return [0] * amount + row
    
    def weight(mask):
        return bin(mask).count('1')
    
    def seven_state_rows(last_n):
        states = {mask: shift([1], weight(mask)) for mask in MASKS}
        answer = {}
        for n in range(1, last_n + 1):
            answer[n] = add_rows(list(states.values()))
            if n == last_n:
                break
            states = {
                target: shift(
                    add_rows([states[source] for source in MASKS if not (source & target)]),
                    weight(target),
                )
                for target in MASKS
            }
        return answer
    
    def row_hash(n, row):
        digest = sha256(pack('>II', n, len(row)))
        for value in row:
            raw = value.to_bytes(max(1, (value.bit_length() + 7) // 8), 'big')
            digest.update(pack('>I', len(raw)))
            digest.update(raw)
        return digest.hexdigest()
    
    reference = seven_state_rows(20)
    a = [1, 0, 0]
    b = [0, 1, 0]
    c = [0, 0, 1]
    minimum_summary = sha256()
    anchor_hashes = {}
    global_minimum = None
    equalities = []
    
    for n in range(1, LAST_N + 1):
        row = [x + 4 * y + 2 * z for x, y, z in zip(a, b, c)]
        if n <= 20:
            assert row == reference[n]
        minimum_at_n = None
        for k, (left, center, right) in enumerate(zip(row, row[1:], row[2:]), 1):
            margin = center * center - left * right
            if margin < 0:
                raise RuntimeError(f'violation n={n} k={k} margin={margin}')
            if margin == 0:
                equalities.append((n, k))
            candidate = (margin, k, left, center, right)
            if minimum_at_n is None or candidate < minimum_at_n:
                minimum_at_n = candidate
        margin, k, left, center, right = minimum_at_n
        expected = 14 if n == 1 else 8 * n * n - 8 * n + 16
        assert (k, margin) == (2 * n - 1, expected)
        minimum_summary.update(f'{n}:{k}:{margin}:{left}:{center}:{right}\n'.encode())
        candidate = (margin, n, k, left, center, right)
        if global_minimum is None or candidate < global_minimum:
            global_minimum = candidate
        if n in ANCHORS:
            anchor_hashes[str(n)] = row_hash(n, row)
        if n < LAST_N:
            new_a = row + [0, 0]
            new_b = [0] + [x + 3 * y + z for x, y, z in zip(a, b, c)] + [0]
            new_c = [0, 0] + [x + 2 * y + z for x, y, z in zip(a, b, c)]
            a, b, c = new_a, new_b, new_c
    
    assert not equalities
    assert global_minimum == (14, 1, 1, 1, 4, 2)
    assert minimum_summary.hexdigest() == 'd13e59c2f9e7385f6d5db1b6bee26ff5cc4c0880aee1edf617d2d5295acd77e0'
    expected_hashes = {
        '1': '5d32edff3981b53b3a92e3be0c3fe55e2250acd5c7b3ac0b9436ded0a7ca0048',
        '2': 'c69f169208f73d96f924baafe4a8fbf7e84fedbb6e4ae0d78eaa94daeb118de3',
        '40': '3c559dfe4a76133b2e204cff06098dae2a3635fecdf46399a20b3b28c848cd7d',
        '100': '7c4aca4c5cac77bb8a7e27f27ac87d2479cbb2e6d4882338b96e8e6d5f63bf80',
        '500': 'a6381905f5ce6178dfa27a58567b0c8e1ff7a2a2ad6c529dd777276cb8c6a670',
        '1000': 'cdecf594c4865f9874ad339f901e9a55e4e205ad386e9b9b8648369a674054b0',
        '2000': '6560d068e0604a99a34c2601f14f294347aa269949ef03802813b9c0f26fc2b7',
        '3000': '1fc1629b478fd338c27ebec85fbb2f8ea5cd5c6f9929c95fc2cb2dc7c7b25c87',
    }
    assert anchor_hashes == expected_hashes
    report = {
        'range': [1, LAST_N],
        'lengths': LAST_N,
        'inequalities': LAST_N * LAST_N,
        'violations': 0,
        'equalities': 0,
        'global_minimum': {'margin': 14, 'n': 1, 'k': 1, 'triple': [1, 4, 2]},
        'per_length_minimum': {
            'n_1': 'k=1, margin=14, triple=(1,4,2)',
            'n_2_through_3000': 'k=2n-1, margin=8n^2-8n+16, triple=(4(n^2+n-2),4n,2)',
        },
        'minimum_summary_sha256': minimum_summary.hexdigest(),
        'row_sha256': anchor_hashes,
        'seven_state_crosscheck': [1, 20],
    }
    payload = dumps(report, sort_keys=True, separators=(',', ':'))
    assert sha256(payload.encode()).hexdigest() == '2b010348b9f84eaff3960474512f76a7fa23ad73169940de74dbd12f26ad8b19'
    print(payload)
    File identity
    Recorded filename
    R366.txt
    Download SHA-256
    de5dee818f79243a4c4c703c19e99ecc1ff0af808b21c384922042102482b12f
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.

Verification source: doi.org ↗, Inline Python 3 exact computation executed on 2026-07-25

Missing for a complete replay: command, expected output.

Recorded artifact fields

5What it produced

Certificate

lengths checked3,000inequalities checked9,000,000seven state crosscheck last n20minimum summary sha256d13e59c2f9e7385f6d5db1b6bee26ff5cc4c0880aee1edf617d2d5295acd77e0final row sha2561fc1629b478fd338c27ebec85fbb2f8ea5cd5c6f9929c95fc2cb2dc7c7b25c87report sha2562b010348b9f84eaff3960474512f76a7fa23ad73169940de74dbd12f26ad8b19

6How it connects

Recorded for

Machine-readable record

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

json
{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R366",
  "content_hash": null,
  "slug": "hcc4-artifact-exact-transfer-sweep",
  "type": "artifact",
  "title": "Replayable exact transfer sweep through strip length 3000",
  "summary": "Standard-library Python regenerates every coefficient with integers, tests every adjacent triple, and hashes eight checkpoint rows.",
  "relevance": "For Hard-core coefficient log-concavity on the first ten thousand four-cycle strips, record hcc4-artifact-exact-transfer-sweep (“Replayable exact transfer sweep through strip length 3000”) supplies evidence or a replay used to check the packet. The record states: Standard-library Python regenerates every coefficient with integers, tests every adjacent triple, and hashes eight checkpoint rows.",
  "relevance_source": "recorded",
  "body": "The program implements the three-state transfer displayed in the claim. A separate seven-state calculation uses the masks \\([0,1,2,4,5,8,10]\\), admits consecutive masks exactly when their bitwise intersection is zero, and matches every reduced-transfer row through \\(n=20\\).\n\nFor each length, the program computes every integer margin before advancing the transfer. It records the least margin and verifies the observed closed form for that minimum. The SHA-256 summary covers one line per length containing \\(n\\), the minimizing index, the margin, and its adjacent coefficient triple. Eight complete coefficient rows are serialized with fixed-width length prefixes and hashed separately.\n\nThe reproduced run took 131.73 seconds on the entry-research host. Raising `LAST_N` continues the same exact calculation. Runtime grows steeply because both the number and bit length of the coefficients increase. A run through 10000 should use checkpointing or a faster big-integer backend.",
  "status": "available",
  "evidence_grade": "executable",
  "scope": {
    "kind": "bounded",
    "statement": "all independence-polynomial coefficients and all internal log-concavity inequalities for 1 <= n <= 3000, with a full seven-mask transfer cross-check for 1 <= n <= 20",
    "bounds": {
      "strip_length": {
        "min": 1,
        "max": 3000
      },
      "seven_state_crosscheck_length": {
        "min": 1,
        "max": 20
      },
      "inequalities_checked": {
        "min": 9000000,
        "max": 9000000
      }
    },
    "exhaustive": true
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "partial",
    "kind": "inline_python_exact_computation",
    "entrypoint": "Join source_lines with newline characters, save as check.py, and run python3 check.py",
    "runtime": "CPython 3.8 or later, standard library only",
    "citation": {
      "url": "https://doi.org/10.1137/S089548019528993X",
      "locator": "Inline Python 3 exact computation executed on 2026-07-25"
    },
    "inline_source": [
      "from hashlib import sha256",
      "from json import dumps",
      "from struct import pack",
      "",
      "LAST_N = 3000",
      "ANCHORS = {1, 2, 40, 100, 500, 1000, 2000, 3000}",
      "MASKS = [m for m in range(16) if not (m & ((m << 1) | (m >> 3)))]",
      "assert MASKS == [0, 1, 2, 4, 5, 8, 10]",
      "",
      "def add_rows(rows):",
      "    size = max(map(len, rows))",
      "    return [sum(row[k] if k < len(row) else 0 for row in rows) for k in range(size)]",
      "",
      "def shift(row, amount):",
      "    return [0] * amount + row",
      "",
      "def weight(mask):",
      "    return bin(mask).count('1')",
      "",
      "def seven_state_rows(last_n):",
      "    states = {mask: shift([1], weight(mask)) for mask in MASKS}",
      "    answer = {}",
      "    for n in range(1, last_n + 1):",
      "        answer[n] = add_rows(list(states.values()))",
      "        if n == last_n:",
      "            break",
      "        states = {",
      "            target: shift(",
      "                add_rows([states[source] for source in MASKS if not (source & target)]),",
      "                weight(target),",
      "            )",
      "            for target in MASKS",
      "        }",
      "    return answer",
      "",
      "def row_hash(n, row):",
      "    digest = sha256(pack('>II', n, len(row)))",
      "    for value in row:",
      "        raw = value.to_bytes(max(1, (value.bit_length() + 7) // 8), 'big')",
      "        digest.update(pack('>I', len(raw)))",
      "        digest.update(raw)",
      "    return digest.hexdigest()",
      "",
      "reference = seven_state_rows(20)",
      "a = [1, 0, 0]",
      "b = [0, 1, 0]",
      "c = [0, 0, 1]",
      "minimum_summary = sha256()",
      "anchor_hashes = {}",
      "global_minimum = None",
      "equalities = []",
      "",
      "for n in range(1, LAST_N + 1):",
      "    row = [x + 4 * y + 2 * z for x, y, z in zip(a, b, c)]",
      "    if n <= 20:",
      "        assert row == reference[n]",
      "    minimum_at_n = None",
      "    for k, (left, center, right) in enumerate(zip(row, row[1:], row[2:]), 1):",
      "        margin = center * center - left * right",
      "        if margin < 0:",
      "            raise RuntimeError(f'violation n={n} k={k} margin={margin}')",
      "        if margin == 0:",
      "            equalities.append((n, k))",
      "        candidate = (margin, k, left, center, right)",
      "        if minimum_at_n is None or candidate < minimum_at_n:",
      "            minimum_at_n = candidate",
      "    margin, k, left, center, right = minimum_at_n",
      "    expected = 14 if n == 1 else 8 * n * n - 8 * n + 16",
      "    assert (k, margin) == (2 * n - 1, expected)",
      "    minimum_summary.update(f'{n}:{k}:{margin}:{left}:{center}:{right}\\n'.encode())",
      "    candidate = (margin, n, k, left, center, right)",
      "    if global_minimum is None or candidate < global_minimum:",
      "        global_minimum = candidate",
      "    if n in ANCHORS:",
      "        anchor_hashes[str(n)] = row_hash(n, row)",
      "    if n < LAST_N:",
      "        new_a = row + [0, 0]",
      "        new_b = [0] + [x + 3 * y + z for x, y, z in zip(a, b, c)] + [0]",
      "        new_c = [0, 0] + [x + 2 * y + z for x, y, z in zip(a, b, c)]",
      "        a, b, c = new_a, new_b, new_c",
      "",
      "assert not equalities",
      "assert global_minimum == (14, 1, 1, 1, 4, 2)",
      "assert minimum_summary.hexdigest() == 'd13e59c2f9e7385f6d5db1b6bee26ff5cc4c0880aee1edf617d2d5295acd77e0'",
      "expected_hashes = {",
      "    '1': '5d32edff3981b53b3a92e3be0c3fe55e2250acd5c7b3ac0b9436ded0a7ca0048',",
      "    '2': 'c69f169208f73d96f924baafe4a8fbf7e84fedbb6e4ae0d78eaa94daeb118de3',",
      "    '40': '3c559dfe4a76133b2e204cff06098dae2a3635fecdf46399a20b3b28c848cd7d',",
      "    '100': '7c4aca4c5cac77bb8a7e27f27ac87d2479cbb2e6d4882338b96e8e6d5f63bf80',",
      "    '500': 'a6381905f5ce6178dfa27a58567b0c8e1ff7a2a2ad6c529dd777276cb8c6a670',",
      "    '1000': 'cdecf594c4865f9874ad339f901e9a55e4e205ad386e9b9b8648369a674054b0',",
      "    '2000': '6560d068e0604a99a34c2601f14f294347aa269949ef03802813b9c0f26fc2b7',",
      "    '3000': '1fc1629b478fd338c27ebec85fbb2f8ea5cd5c6f9929c95fc2cb2dc7c7b25c87',",
      "}",
      "assert anchor_hashes == expected_hashes",
      "report = {",
      "    'range': [1, LAST_N],",
      "    'lengths': LAST_N,",
      "    'inequalities': LAST_N * LAST_N,",
      "    'violations': 0,",
      "    'equalities': 0,",
      "    'global_minimum': {'margin': 14, 'n': 1, 'k': 1, 'triple': [1, 4, 2]},",
      "    'per_length_minimum': {",
      "        'n_1': 'k=1, margin=14, triple=(1,4,2)',",
      "        'n_2_through_3000': 'k=2n-1, margin=8n^2-8n+16, triple=(4(n^2+n-2),4n,2)',",
      "    },",
      "    'minimum_summary_sha256': minimum_summary.hexdigest(),",
      "    'row_sha256': anchor_hashes,",
      "    'seven_state_crosscheck': [1, 20],",
      "}",
      "payload = dumps(report, sort_keys=True, separators=(',', ':'))",
      "assert sha256(payload.encode()).hexdigest() == '2b010348b9f84eaff3960474512f76a7fa23ad73169940de74dbd12f26ad8b19'",
      "print(payload)"
    ],
    "missing": [
      "command",
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://doi.org/10.1137/S089548019528993X",
    "locator": "Inline Python 3 exact computation executed on 2026-07-25"
  },
  "models": [],
  "relations": [
    {
      "slug": "R368",
      "title": "Every four-cycle strip through length 3000 has a log-concave independence sequence",
      "object_type": "claim",
      "relation": "reproduces",
      "direction": "outgoing"
    },
    {
      "slug": "hard-core-c4-strip-log-concavity",
      "title": "hard core c4 strip log concavity",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}

8Provenance

View source, identifiers, and projection details

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.