R704artifactStatus: availableEvidence: ReproducedReplay: partialexhaustive over its scope

[#R704] Replayable exact rank and log-concavity sweep

1Summary

A standard-library Python program cross-checks the formula against 2,131,018 matrices and verifies every coefficient and inequality through order 50.

The program evaluates the MacWilliams product with exact rational arithmetic and asserts integrality. It checks each rank row against the total number \(2^{n(n+1)/2}\) of symmetric binary matrices. For orders at most six, a separate Gray-code enumeration visits every upper-triangular bit assignment, forms the symmetric matrix, computes its rank over \(\mathbb F_2\), and compares the complete row with the formula.

The program then checks the two adjacent-quotient formulas and all 1,225 strict log-concavity inequalities. The smallest margin is 5 at \((n,r)=(2,1)\), with triple \((1,3,4)\).

Reproduced evidence. Recorded scope: all rank counts and adjacent log-concavity inequalities for 1 <= n <= 50, with exhaustive matrix enumeration for 1 <= n <= 6.

2Reproduce

Replay: partial

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

Entry point: Join source_lines with newline characters, save as check.py, and run python3 check.py
Runtime: Python 3.8 or later, standard library only

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

Missing for a complete replay: command, expected output.

3Overview

For the coefficient digest, each row begins with two-byte big-endian fields for its order and length. Each coefficient is encoded by a two-byte byte-length followed by its minimal unsigned big-endian representation. Concatenating the 50 rows in increasing order gives SHA-256 digest `298e2b5d779b4b3c344d57e3d9c47bd7d35dfe27d42cbc4229be2ffd86519470`.

4Source code

View source code

Source code

from fractions import Fraction
from hashlib import sha256
from struct import pack

FIRST_N = 1
LAST_N = 50
ANCHORS = {1, 2, 3, 4, 5, 6, 10, 25, 50}

def rank_count(n, r):
    value = Fraction(1)
    for i in range(1, r // 2 + 1):
        value *= Fraction(2 ** (2 * i), 2 ** (2 * i) - 1)
    for i in range(r):
        value *= 2 ** (n - i) - 1
    if value.denominator != 1:
        raise RuntimeError(f"nonintegral count at n={n}, r={r}")
    return value.numerator

def rank_row(n):
    return [rank_count(n, r) for r in range(n + 1)]

def gf2_rank(rows):
    work = rows[:]
    answer = 0
    while work:
        pivot = max(work)
        if pivot == 0:
            break
        work.remove(pivot)
        bit = 1 << (pivot.bit_length() - 1)
        work = [row ^ pivot if row & bit else row for row in work]
        answer += 1
    return answer

def enumerated_rank_row(n):
    positions = [(i, j) for i in range(n) for j in range(i, n)]
    rows = [0] * n
    counts = [0] * (n + 1)
    previous_gray = 0
    for serial in range(1 << len(positions)):
        gray = serial ^ (serial >> 1)
        if serial:
            changed = (gray ^ previous_gray).bit_length() - 1
            i, j = positions[changed]
            rows[i] ^= 1 << j
            if i != j:
                rows[j] ^= 1 << i
        counts[gf2_rank(rows)] += 1
        previous_gray = gray
    return counts

def serialize_row(n, row):
    encoded = bytearray(pack(">HH", n, len(row)))
    for value in row:
        raw = value.to_bytes(max(1, (value.bit_length() + 7) // 8), "big")
        encoded += pack(">H", len(raw))
        encoded += raw
    return bytes(encoded)

enumerated_matrices = 0
for n in range(1, 7):
    expected = rank_row(n)
    observed = enumerated_rank_row(n)
    enumerated_matrices += 1 << (n * (n + 1) // 2)
    if observed != expected:
        raise RuntimeError(f"formula/enumeration mismatch at n={n}")

stream_hash = sha256()
anchor_hashes = {}
inequality_count = 0
equalities = 0
minimum = None
for n in range(FIRST_N, LAST_N + 1):
    row = rank_row(n)
    if sum(row) != 2 ** (n * (n + 1) // 2):
        raise RuntimeError(f"row-total mismatch at n={n}")
    encoded = serialize_row(n, row)
    stream_hash.update(encoded)
    if n in ANCHORS:
        anchor_hashes[n] = sha256(encoded).hexdigest()
    for r in range(n):
        quotient = Fraction(row[r + 1], row[r])
        if r % 2 == 0:
            expected = Fraction(2 ** (n - r) - 1)
        else:
            expected = Fraction(2 ** (r + 1) * (2 ** (n - r) - 1), 2 ** (r + 1) - 1)
        if quotient != expected:
            raise RuntimeError(f"quotient mismatch at n={n}, r={r}")
    for r in range(1, n):
        left, center, right = row[r - 1:r + 2]
        margin = center * center - left * right
        inequality_count += 1
        if margin == 0:
            equalities += 1
        if margin <= 0:
            raise RuntimeError(f"strict log-concavity failure at n={n}, r={r}")
        if minimum is None or margin < minimum[0]:
            minimum = (margin, n, r, left, center, right)

print(f"formula_enumeration_crosscheck=1..6 passed matrices={enumerated_matrices}")
print(f"range={FIRST_N}..{LAST_N} rows={LAST_N-FIRST_N+1} coefficients={sum(n + 1 for n in range(FIRST_N, LAST_N + 1))}")
print(f"inequalities={inequality_count} violations=0 equalities={equalities}")
margin, n, r, left, center, right = minimum
print(f"minimum_margin={margin} at={n}:{r} triple={left},{center},{right}")
print("coefficient_stream_sha256=" + stream_hash.hexdigest())
for n in sorted(anchor_hashes):
    print(f"row_sha256[{n}]={anchor_hashes[n]}")

5What it produced

Observed runtime: 5.1 seconds on the entry-research host
Expected stdout: formula_enumeration_crosscheck=1..6 passed matrices=2131018 range=1..50 rows=50 coefficients=1325 inequalities=1225 violations=0 equalities=0 minimum_margin=5 at=2:1 triple=1,3,4 coefficient_stream_sha256=298e2b5d779b4b3c344d57e3d9c47bd7d35dfe27d42cbc4229be2ffd86519470 row_sha256[1]=dcb3840f9848eda5d5001913bc57b75f63c5a786409af260085e1cf6d3e31e4b row_sha256[2]=9f5904b8939cc6425e769da9a2a42526cc78d437a14c1978f17124f0e6d461fe row_sha256[3]=08201ac9266776163081c231ef717d8bd956bf840d54ebd8549c1ef3f7cd91eb row_sha256[4]=c843e211d28f70e6418f90b8851407ef59d0b01b74e8a420963b2c18f749e154 row_sha256[5]=cf20d4f51253659ad03e416d45530064e8c110d9b8723713b1881ff7e05d5bec row_sha256[6]=d48bf9bea8467519f0dd9f73d2284326baad586889df83d5f584e31f33874e08 row_sha256[10]=96d323835859c903f90f30f67c13180f2876a970b1f70310fff0fabd867694ea row_sha256[25]=da2f64da065b1f57c6845f9d346dabfbaa0ed0802241e798aeb089339e75b32f row_sha256[50]=40cb8ec72ea76ea6f0f626176f2581551145ab85efc6e1a4fea77c0a5c667c4e
Coefficient stream sha256: 298e2b5d779b4b3c344d57e3d9c47bd7d35dfe27d42cbc4229be2ffd86519470
Formula: R(n,r)=product_{i=1..floor(r/2)} 2^(2i)/(2^(2i)-1) times product_{i=0..r-1}(2^(n-i)-1)
Orders checked: 50
Coefficients checked: 1,325
Inequalities checked: 1,225
Violations: 0
Equalities: 0
Exhaustive crosscheck max order: 6
Matrices exhaustively enumerated: 2,131,018

Row sha256

1dcb3840f9848eda5d5001913bc57b75f63c5a786409af260085e1cf6d3e31e4b29f5904b8939cc6425e769da9a2a42526cc78d437a14c1978f17124f0e6d461fe308201ac9266776163081c231ef717d8bd956bf840d54ebd8549c1ef3f7cd91eb4c843e211d28f70e6418f90b8851407ef59d0b01b74e8a420963b2c18f749e1545cf20d4f51253659ad03e416d45530064e8c110d9b8723713b1881ff7e05d5bec6d48bf9bea8467519f0dd9f73d2284326baad586889df83d5f584e31f33874e081096d323835859c903f90f30f67c13180f2876a970b1f70310fff0fabd867694ea25da2f64da065b1f57c6845f9d346dabfbaa0ed0802241e798aeb089339e75b32f5040cb8ec72ea76ea6f0f626176f2581551145ab85efc6e1a4fea77c0a5c667c4e

6How it connects

7Agent packet

A compact handoff with the evidence boundary, replay manifest, and relation pointers.

View structured packet

json

{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R704",
  "content_hash": null,
  "slug": "sbmrlc-artifact-exact-sweep",
  "type": "artifact",
  "title": "Replayable exact rank and log-concavity sweep",
  "summary": "A standard-library Python program cross-checks the formula against 2,131,018 matrices and verifies every coefficient and inequality through order 50.",
  "relevance": "For Rank log-concavity for symmetric binary matrices through order fifty, record sbmrlc-artifact-exact-sweep (“Replayable exact rank and log-concavity sweep”) supplies evidence or a replay used to check the packet. The record states: A standard-library Python program cross-checks the formula against 2,131,018 matrices and verifies every coefficient and inequality through order 50.",
  "relevance_source": "recorded",
  "body": "The program evaluates the MacWilliams product with exact rational arithmetic and asserts integrality. It checks each rank row against the total number \\(2^{n(n+1)/2}\\) of symmetric binary matrices. For orders at most six, a separate Gray-code enumeration visits every upper-triangular bit assignment, forms the symmetric matrix, computes its rank over \\(\\mathbb F_2\\), and compares the complete row with the formula.\n\nThe program then checks the two adjacent-quotient formulas and all 1,225 strict log-concavity inequalities. The smallest margin is 5 at \\((n,r)=(2,1)\\), with triple \\((1,3,4)\\).\n\nFor the coefficient digest, each row begins with two-byte big-endian fields for its order and length. Each coefficient is encoded by a two-byte byte-length followed by its minimal unsigned big-endian representation. Concatenating the 50 rows in increasing order gives SHA-256 digest `298e2b5d779b4b3c344d57e3d9c47bd7d35dfe27d42cbc4229be2ffd86519470`.",
  "status": "available",
  "evidence_grade": "executable",
  "scope": {
    "kind": "bounded",
    "statement": "all rank counts and adjacent log-concavity inequalities for 1 <= n <= 50, with exhaustive matrix enumeration for 1 <= n <= 6",
    "bounds": {
      "matrix_order": {
        "min": 1,
        "max": 50
      },
      "formula_enumeration_crosscheck_order": {
        "min": 1,
        "max": 6
      },
      "coefficients_checked": {
        "min": 1325,
        "max": 1325
      },
      "inequalities_checked": {
        "min": 1225,
        "max": 1225
      }
    },
    "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": "Python 3.8 or later, standard library only",
    "citation": {
      "url": "https://arxiv.org/abs/1011.4539",
      "locator": "Inline Python 3 exact computation executed on 2026-07-25"
    },
    "inline_source": [
      "from fractions import Fraction",
      "from hashlib import sha256",
      "from struct import pack",
      "",
      "FIRST_N = 1",
      "LAST_N = 50",
      "ANCHORS = {1, 2, 3, 4, 5, 6, 10, 25, 50}",
      "",
      "def rank_count(n, r):",
      "    value = Fraction(1)",
      "    for i in range(1, r // 2 + 1):",
      "        value *= Fraction(2 ** (2 * i), 2 ** (2 * i) - 1)",
      "    for i in range(r):",
      "        value *= 2 ** (n - i) - 1",
      "    if value.denominator != 1:",
      "        raise RuntimeError(f\"nonintegral count at n={n}, r={r}\")",
      "    return value.numerator",
      "",
      "def rank_row(n):",
      "    return [rank_count(n, r) for r in range(n + 1)]",
      "",
      "def gf2_rank(rows):",
      "    work = rows[:]",
      "    answer = 0",
      "    while work:",
      "        pivot = max(work)",
      "        if pivot == 0:",
      "            break",
      "        work.remove(pivot)",
      "        bit = 1 << (pivot.bit_length() - 1)",
      "        work = [row ^ pivot if row & bit else row for row in work]",
      "        answer += 1",
      "    return answer",
      "",
      "def enumerated_rank_row(n):",
      "    positions = [(i, j) for i in range(n) for j in range(i, n)]",
      "    rows = [0] * n",
      "    counts = [0] * (n + 1)",
      "    previous_gray = 0",
      "    for serial in range(1 << len(positions)):",
      "        gray = serial ^ (serial >> 1)",
      "        if serial:",
      "            changed = (gray ^ previous_gray).bit_length() - 1",
      "            i, j = positions[changed]",
      "            rows[i] ^= 1 << j",
      "            if i != j:",
      "                rows[j] ^= 1 << i",
      "        counts[gf2_rank(rows)] += 1",
      "        previous_gray = gray",
      "    return counts",
      "",
      "def serialize_row(n, row):",
      "    encoded = bytearray(pack(\">HH\", n, len(row)))",
      "    for value in row:",
      "        raw = value.to_bytes(max(1, (value.bit_length() + 7) // 8), \"big\")",
      "        encoded += pack(\">H\", len(raw))",
      "        encoded += raw",
      "    return bytes(encoded)",
      "",
      "enumerated_matrices = 0",
      "for n in range(1, 7):",
      "    expected = rank_row(n)",
      "    observed = enumerated_rank_row(n)",
      "    enumerated_matrices += 1 << (n * (n + 1) // 2)",
      "    if observed != expected:",
      "        raise RuntimeError(f\"formula/enumeration mismatch at n={n}\")",
      "",
      "stream_hash = sha256()",
      "anchor_hashes = {}",
      "inequality_count = 0",
      "equalities = 0",
      "minimum = None",
      "for n in range(FIRST_N, LAST_N + 1):",
      "    row = rank_row(n)",
      "    if sum(row) != 2 ** (n * (n + 1) // 2):",
      "        raise RuntimeError(f\"row-total mismatch at n={n}\")",
      "    encoded = serialize_row(n, row)",
      "    stream_hash.update(encoded)",
      "    if n in ANCHORS:",
      "        anchor_hashes[n] = sha256(encoded).hexdigest()",
      "    for r in range(n):",
      "        quotient = Fraction(row[r + 1], row[r])",
      "        if r % 2 == 0:",
      "            expected = Fraction(2 ** (n - r) - 1)",
      "        else:",
      "            expected = Fraction(2 ** (r + 1) * (2 ** (n - r) - 1), 2 ** (r + 1) - 1)",
      "        if quotient != expected:",
      "            raise RuntimeError(f\"quotient mismatch at n={n}, r={r}\")",
      "    for r in range(1, n):",
      "        left, center, right = row[r - 1:r + 2]",
      "        margin = center * center - left * right",
      "        inequality_count += 1",
      "        if margin == 0:",
      "            equalities += 1",
      "        if margin <= 0:",
      "            raise RuntimeError(f\"strict log-concavity failure at n={n}, r={r}\")",
      "        if minimum is None or margin < minimum[0]:",
      "            minimum = (margin, n, r, left, center, right)",
      "",
      "print(f\"formula_enumeration_crosscheck=1..6 passed matrices={enumerated_matrices}\")",
      "print(f\"range={FIRST_N}..{LAST_N} rows={LAST_N-FIRST_N+1} coefficients={sum(n + 1 for n in range(FIRST_N, LAST_N + 1))}\")",
      "print(f\"inequalities={inequality_count} violations=0 equalities={equalities}\")",
      "margin, n, r, left, center, right = minimum",
      "print(f\"minimum_margin={margin} at={n}:{r} triple={left},{center},{right}\")",
      "print(\"coefficient_stream_sha256=\" + stream_hash.hexdigest())",
      "for n in sorted(anchor_hashes):",
      "    print(f\"row_sha256[{n}]={anchor_hashes[n]}\")"
    ],
    "missing": [
      "command",
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://arxiv.org/abs/1011.4539",
    "locator": "Inline Python 3 exact computation executed on 2026-07-25"
  },
  "relations": [
    {
      "slug": "R707",
      "title": "The symmetric binary rank distribution is strictly log-concave",
      "object_type": "claim",
      "relation": "reproduces",
      "direction": "outgoing"
    },
    {
      "slug": "R706",
      "title": "MacWilliams's product formula gives every rank count",
      "object_type": "claim",
      "relation": "uses",
      "direction": "outgoing"
    },
    {
      "slug": "symmetric-binary-matrix-rank-log-concavity",
      "title": "symmetric binary matrix rank log concavity",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}

8Provenance

View source, identifiers, and projection details

Project: symmetric-binary-matrix-rank-log-concavity
Locator: Inline Python 3 exact computation executed on 2026-07-25
License: CC0-1.0
Contributors: TheoremDB entry research, 2026-07-25
Source: arxiv.org ↗
Public record: R704
Stable alias: sbmrlc-artifact-exact-sweep
Projection: Reproduction fields are derived from the immutable record.

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

Record & provenance

View versioned JSON