{
  "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"
    },
    "outputs": "formula_enumeration_crosscheck=1..6 passed matrices=2131018\nrange=1..50 rows=50 coefficients=1325\ninequalities=1225 violations=0 equalities=0\nminimum_margin=5 at=2:1 triple=1,3,4\ncoefficient_stream_sha256=298e2b5d779b4b3c344d57e3d9c47bd7d35dfe27d42cbc4229be2ffd86519470\nrow_sha256[1]=dcb3840f9848eda5d5001913bc57b75f63c5a786409af260085e1cf6d3e31e4b\nrow_sha256[2]=9f5904b8939cc6425e769da9a2a42526cc78d437a14c1978f17124f0e6d461fe\nrow_sha256[3]=08201ac9266776163081c231ef717d8bd956bf840d54ebd8549c1ef3f7cd91eb\nrow_sha256[4]=c843e211d28f70e6418f90b8851407ef59d0b01b74e8a420963b2c18f749e154\nrow_sha256[5]=cf20d4f51253659ad03e416d45530064e8c110d9b8723713b1881ff7e05d5bec\nrow_sha256[6]=d48bf9bea8467519f0dd9f73d2284326baad586889df83d5f584e31f33874e08\nrow_sha256[10]=96d323835859c903f90f30f67c13180f2876a970b1f70310fff0fabd867694ea\nrow_sha256[25]=da2f64da065b1f57c6845f9d346dabfbaa0ed0802241e798aeb089339e75b32f\nrow_sha256[50]=40cb8ec72ea76ea6f0f626176f2581551145ab85efc6e1a4fea77c0a5c667c4e\n",
    "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"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://arxiv.org/abs/1011.4539",
    "locator": "Inline Python 3 exact computation executed on 2026-07-25"
  },
  "models": [],
  "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"
    }
  ]
}