TheoremDB

Problem packetResearch packetR751

R751Executable evidence

Exact generator, Pfaffian, and determinant verifier

View replayOpen source ↗
Link to a section

Authored summary

Standard-library Python reconstructs the published circulant blocks and checks every claimed identity with exact arithmetic.

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

Recorded status: available

Recorded scope: the Goethals-Seidel order-36 block construction and its principal submatrix on indices 2 through 35

Complete recorded scope and conditions
{
  "kind": "bounded",
  "statement": "the Goethals-Seidel order-36 block construction and its principal submatrix on indices 2 through 35",
  "bounds": {
    "source_order": {
      "min": 36,
      "max": 36
    },
    "result_order": {
      "min": 34,
      "max": 34
    }
  },
  "exhaustive": true
}

Originating problem: Maximum determinant of a skew Seidel matrix of order 34

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

Recorded relationships: An explicit order-34 matrix has determinant 35^16

Authored record and scope
Authored title
Exact generator, Pfaffian, and determinant verifier
Record type
artifact
Stored status
available
Evidence grade
executable
Recorded scope data
{ "kind": "bounded", "statement": "the Goethals-Seidel order-36 block construction and its principal submatrix on indices 2 through 35", "bounds": { "source_order": { "min": 36, "max": 36 }, "result_order": { "min": 34, "max": 34 } }, "exhaustive": true }
Linked research record IDs
R753

2Authored explanation

The program fixes the circulant convention by setting entry \((i,j)\) to first-row entry \((j-i)\bmod9\). It builds the Goethals-Seidel array, checks all 1,296 entries of \(H+H^T=2I\) and \(HH^T=36I\), then checks the skew Seidel conditions after deletion.

The compact matrix certificate is the SHA-256 digest of its upper-triangle signs in row-major order, writing `+` for 1 and `-` for -1. The order-34 digest is `c081b626a079cca244e06357bacacad2a406f7512557c554a5dc78e0477bcd35`. Exact rational Pfaffian elimination and integer Bareiss elimination independently agree through \(\det S=\operatorname{pf}(S)^2\). The stable output digest is recorded with the program.

Files and source

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

  • R751.txt4,111 bytes · No SHA-256 recorded
    Preview R751.txt
    from fractions import Fraction
import hashlib
from math import isqrt

def circulant(first):
    n = len(first)
    return [[first[(j - i) % n] for j in range(n)] for i in range(n)]

def transpose(a):
    return [list(row) for row in zip(*a)]

def multiply(a, b):
    bt = transpose(b)
    return [[sum(x * y for x, y in zip(row, col)) for col in bt] for row in a]

def negate(a):
    return [[-x for x in row] for row in a]

def blocks(block_rows):
    size = len(block_rows[0][0])
    return [sum((block[i] for block in block_row), [])
            for block_row in block_rows for i in range(size)]

def bareiss(a):
    a = [row[:] for row in a]
    n = len(a)
    sign = 1
    previous = 1
    for k in range(n - 1):
        pivot_row = next((i for i in range(k, n) if a[i][k]), None)
        if pivot_row is None:
            return 0
        if pivot_row != k:
            a[k], a[pivot_row] = a[pivot_row], a[k]
            sign = -sign
        pivot = a[k][k]
        for i in range(k + 1, n):
            for j in range(k + 1, n):
                numerator = a[i][j] * pivot - a[i][k] * a[k][j]
                assert numerator % previous == 0
                a[i][j] = numerator // previous
            a[i][k] = 0
        previous = pivot
    return sign * a[-1][-1]

def pfaffian(a):
    a = [[Fraction(x) for x in row] for row in a]
    result = Fraction(1)
    sign = 1
    while a:
        n = len(a)
        partner = next(j for j in range(1, n) if a[0][j])
        if partner != 1:
            for row in a:
                row[1], row[partner] = row[partner], row[1]
            a[1], a[partner] = a[partner], a[1]
            sign = -sign
        pivot = a[0][1]
        result *= pivot
        a = [[a[i][j] - (a[0][i] * a[1][j] - a[0][j] * a[1][i]) / pivot
              for j in range(2, n)] for i in range(2, n)]
    assert result.denominator == 1
    return sign * result.numerator

def sign_digest(a):
    signs = ''.join('+' if a[i][j] == 1 else '-'
                    for i in range(len(a)) for j in range(i + 1, len(a)))
    return hashlib.sha256(signs.encode('ascii')).hexdigest()

A = circulant([0, 1, 1, -1, 1, -1, 1, -1, -1])
B = circulant([1, -1, 1, 1, -1, -1, 1, 1, -1])
C = circulant([-1, -1, 1, 1, 1, 1, 1, 1, -1])
D = circulant([1, 1, 1, -1, 1, 1, -1, 1, 1])
R = [[int(i + j == 8) for j in range(9)] for i in range(9)]
I9 = [[int(i == j) for j in range(9)] for i in range(9)]
Z = [[A[i][j] + I9[i][j] for j in range(9)] for i in range(9)]
BR, CR, DR = multiply(B, R), multiply(C, R), multiply(D, R)
H = blocks([[Z, BR, CR, DR],
            [negate(BR), Z, negate(DR), CR],
            [negate(CR), DR, Z, negate(BR)],
            [negate(DR), negate(CR), BR, Z]])
assert all(H[i][j] in (-1, 1) for i in range(36) for j in range(36))
assert all(H[i][j] + H[j][i] == 2 * int(i == j)
           for i in range(36) for j in range(36))
HHt = multiply(H, transpose(H))
assert all(HHt[i][j] == 36 * int(i == j)
           for i in range(36) for j in range(36))
K = [[H[i][j] - int(i == j) for j in range(36)] for i in range(36)]
KKt = multiply(K, transpose(K))
assert all(K[i][j] == -K[j][i] for i in range(36) for j in range(36))
assert all(KKt[i][j] == 35 * int(i == j)
           for i in range(36) for j in range(36))
S = [row[2:] for row in K[2:]]
assert all(S[i][i] == 0 for i in range(34))
assert all(S[i][j] in (-1, 1) and S[i][j] == -S[j][i]
           for i in range(34) for j in range(34) if i != j)
digest36 = sign_digest(K)
digest34 = sign_digest(S)
assert digest36 == '2ecf1e091ff9dc48b9a2ce0ea265eb8d7ebead2019915369839d259f4542539f'
assert digest34 == 'c081b626a079cca244e06357bacacad2a406f7512557c554a5dc78e0477bcd35'
pf = pfaffian(S)
det = bareiss(S)
assert pf == -(35 ** 8)
assert det == 35 ** 16 == pf * pf
raw_bound = 65 * 31 ** 16
upper_pf = isqrt(raw_bound)
assert upper_pf == 6876227375063 and upper_pf % 2 == 1
assert (upper_pf + 2) ** 2 > raw_bound
print(f'conference_digest={digest36}')
print(f'principal_digest={digest34}')
print(f'pfaffian={pf}')
print(f'determinant={det}')
print(f'upper_pfaffian={upper_pf}')
print(f'upper_determinant={upper_pf ** 2}')
    File identity
    Recorded filename
    R751.txt
    Download SHA-256
    6515ae8c61051768269be3c9ee7e061593cf2b48ed5f5b90ba2b14bbe57683bb
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 LF characters and execute the resulting Python program
Runtime
Python 3.10 or newer, standard library

Verification source: doi.org ↗, Inline Python 3 standard-library replay of Goethals and Seidel, executed on 2026-07-25

Expected output

conference_digest=2ecf1e091ff9dc48b9a2ce0ea265eb8d7ebead2019915369839d259f4542539f
principal_digest=c081b626a079cca244e06357bacacad2a406f7512557c554a5dc78e0477bcd35
pfaffian=-2251875390625
determinant=5070942774902496337890625
upper_pfaffian=6876227375063
upper_determinant=47282502913565795274253969

Missing for a complete replay: command.

Recorded artifact fields
Kind
inline_python_exact_computation
Entry point
Join source_lines with LF characters and execute the resulting Python program
Environment
Python 3.10 or newer, standard library

5What it produced

Expected stdout
conference_digest=2ecf1e091ff9dc48b9a2ce0ea265eb8d7ebead2019915369839d259f4542539f principal_digest=c081b626a079cca244e06357bacacad2a406f7512557c554a5dc78e0477bcd35 pfaffian=-2251875390625 determinant=5070942774902496337890625 upper_pfaffian=6876227375063 upper_determinant=47282502913565795274253969
Expected stdout sha256
21e729674c2d1986900c0b634f42992e63e3ce770441d9a3d385e9283280bbbe

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": "R751",
  "content_hash": null,
  "slug": "ssm34-artifact-gs36-principal-minor",
  "type": "artifact",
  "title": "Exact generator, Pfaffian, and determinant verifier",
  "summary": "Standard-library Python reconstructs the published circulant blocks and checks every claimed identity with exact arithmetic.",
  "relevance": "For Maximum determinant of a skew Seidel matrix of order 34, record ssm34-artifact-gs36-principal-minor (“Exact generator, Pfaffian, and determinant verifier”) supplies evidence or a replay used to check the packet. The record states: Standard-library Python reconstructs the published circulant blocks and checks every claimed identity with exact arithmetic.",
  "relevance_source": "recorded",
  "body": "The program fixes the circulant convention by setting entry \\((i,j)\\) to first-row entry \\((j-i)\\bmod9\\). It builds the Goethals-Seidel array, checks all 1,296 entries of \\(H+H^T=2I\\) and \\(HH^T=36I\\), then checks the skew Seidel conditions after deletion.\n\nThe compact matrix certificate is the SHA-256 digest of its upper-triangle signs in row-major order, writing `+` for 1 and `-` for -1. The order-34 digest is `c081b626a079cca244e06357bacacad2a406f7512557c554a5dc78e0477bcd35`. Exact rational Pfaffian elimination and integer Bareiss elimination independently agree through \\(\\det S=\\operatorname{pf}(S)^2\\). The stable output digest is recorded with the program.",
  "status": "available",
  "evidence_grade": "executable",
  "scope": {
    "kind": "bounded",
    "statement": "the Goethals-Seidel order-36 block construction and its principal submatrix on indices 2 through 35",
    "bounds": {
      "source_order": {
        "min": 36,
        "max": 36
      },
      "result_order": {
        "min": 34,
        "max": 34
      }
    },
    "exhaustive": true
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "partial",
    "kind": "inline_python_exact_computation",
    "entrypoint": "Join source_lines with LF characters and execute the resulting Python program",
    "runtime": "Python 3.10 or newer, standard library",
    "citation": {
      "url": "https://doi.org/10.1017/S144678870000673X",
      "locator": "Inline Python 3 standard-library replay of Goethals and Seidel, executed on 2026-07-25"
    },
    "outputs": "conference_digest=2ecf1e091ff9dc48b9a2ce0ea265eb8d7ebead2019915369839d259f4542539f\nprincipal_digest=c081b626a079cca244e06357bacacad2a406f7512557c554a5dc78e0477bcd35\npfaffian=-2251875390625\ndeterminant=5070942774902496337890625\nupper_pfaffian=6876227375063\nupper_determinant=47282502913565795274253969\n",
    "inline_source": [
      "from fractions import Fraction",
      "import hashlib",
      "from math import isqrt",
      "",
      "def circulant(first):",
      "    n = len(first)",
      "    return [[first[(j - i) % n] for j in range(n)] for i in range(n)]",
      "",
      "def transpose(a):",
      "    return [list(row) for row in zip(*a)]",
      "",
      "def multiply(a, b):",
      "    bt = transpose(b)",
      "    return [[sum(x * y for x, y in zip(row, col)) for col in bt] for row in a]",
      "",
      "def negate(a):",
      "    return [[-x for x in row] for row in a]",
      "",
      "def blocks(block_rows):",
      "    size = len(block_rows[0][0])",
      "    return [sum((block[i] for block in block_row), [])",
      "            for block_row in block_rows for i in range(size)]",
      "",
      "def bareiss(a):",
      "    a = [row[:] for row in a]",
      "    n = len(a)",
      "    sign = 1",
      "    previous = 1",
      "    for k in range(n - 1):",
      "        pivot_row = next((i for i in range(k, n) if a[i][k]), None)",
      "        if pivot_row is None:",
      "            return 0",
      "        if pivot_row != k:",
      "            a[k], a[pivot_row] = a[pivot_row], a[k]",
      "            sign = -sign",
      "        pivot = a[k][k]",
      "        for i in range(k + 1, n):",
      "            for j in range(k + 1, n):",
      "                numerator = a[i][j] * pivot - a[i][k] * a[k][j]",
      "                assert numerator % previous == 0",
      "                a[i][j] = numerator // previous",
      "            a[i][k] = 0",
      "        previous = pivot",
      "    return sign * a[-1][-1]",
      "",
      "def pfaffian(a):",
      "    a = [[Fraction(x) for x in row] for row in a]",
      "    result = Fraction(1)",
      "    sign = 1",
      "    while a:",
      "        n = len(a)",
      "        partner = next(j for j in range(1, n) if a[0][j])",
      "        if partner != 1:",
      "            for row in a:",
      "                row[1], row[partner] = row[partner], row[1]",
      "            a[1], a[partner] = a[partner], a[1]",
      "            sign = -sign",
      "        pivot = a[0][1]",
      "        result *= pivot",
      "        a = [[a[i][j] - (a[0][i] * a[1][j] - a[0][j] * a[1][i]) / pivot",
      "              for j in range(2, n)] for i in range(2, n)]",
      "    assert result.denominator == 1",
      "    return sign * result.numerator",
      "",
      "def sign_digest(a):",
      "    signs = ''.join('+' if a[i][j] == 1 else '-'",
      "                    for i in range(len(a)) for j in range(i + 1, len(a)))",
      "    return hashlib.sha256(signs.encode('ascii')).hexdigest()",
      "",
      "A = circulant([0, 1, 1, -1, 1, -1, 1, -1, -1])",
      "B = circulant([1, -1, 1, 1, -1, -1, 1, 1, -1])",
      "C = circulant([-1, -1, 1, 1, 1, 1, 1, 1, -1])",
      "D = circulant([1, 1, 1, -1, 1, 1, -1, 1, 1])",
      "R = [[int(i + j == 8) for j in range(9)] for i in range(9)]",
      "I9 = [[int(i == j) for j in range(9)] for i in range(9)]",
      "Z = [[A[i][j] + I9[i][j] for j in range(9)] for i in range(9)]",
      "BR, CR, DR = multiply(B, R), multiply(C, R), multiply(D, R)",
      "H = blocks([[Z, BR, CR, DR],",
      "            [negate(BR), Z, negate(DR), CR],",
      "            [negate(CR), DR, Z, negate(BR)],",
      "            [negate(DR), negate(CR), BR, Z]])",
      "assert all(H[i][j] in (-1, 1) for i in range(36) for j in range(36))",
      "assert all(H[i][j] + H[j][i] == 2 * int(i == j)",
      "           for i in range(36) for j in range(36))",
      "HHt = multiply(H, transpose(H))",
      "assert all(HHt[i][j] == 36 * int(i == j)",
      "           for i in range(36) for j in range(36))",
      "K = [[H[i][j] - int(i == j) for j in range(36)] for i in range(36)]",
      "KKt = multiply(K, transpose(K))",
      "assert all(K[i][j] == -K[j][i] for i in range(36) for j in range(36))",
      "assert all(KKt[i][j] == 35 * int(i == j)",
      "           for i in range(36) for j in range(36))",
      "S = [row[2:] for row in K[2:]]",
      "assert all(S[i][i] == 0 for i in range(34))",
      "assert all(S[i][j] in (-1, 1) and S[i][j] == -S[j][i]",
      "           for i in range(34) for j in range(34) if i != j)",
      "digest36 = sign_digest(K)",
      "digest34 = sign_digest(S)",
      "assert digest36 == '2ecf1e091ff9dc48b9a2ce0ea265eb8d7ebead2019915369839d259f4542539f'",
      "assert digest34 == 'c081b626a079cca244e06357bacacad2a406f7512557c554a5dc78e0477bcd35'",
      "pf = pfaffian(S)",
      "det = bareiss(S)",
      "assert pf == -(35 ** 8)",
      "assert det == 35 ** 16 == pf * pf",
      "raw_bound = 65 * 31 ** 16",
      "upper_pf = isqrt(raw_bound)",
      "assert upper_pf == 6876227375063 and upper_pf % 2 == 1",
      "assert (upper_pf + 2) ** 2 > raw_bound",
      "print(f'conference_digest={digest36}')",
      "print(f'principal_digest={digest34}')",
      "print(f'pfaffian={pf}')",
      "print(f'determinant={det}')",
      "print(f'upper_pfaffian={upper_pf}')",
      "print(f'upper_determinant={upper_pf ** 2}')"
    ],
    "missing": [
      "command"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://doi.org/10.1017/S144678870000673X",
    "locator": "Inline Python 3 standard-library replay of Goethals and Seidel, executed on 2026-07-25"
  },
  "models": [],
  "continuation": null,
  "relations": [
    {
      "slug": "R753",
      "title": "An explicit order-34 matrix has determinant 35^16",
      "object_type": "claim",
      "relation": "evidences",
      "direction": "outgoing"
    },
    {
      "slug": "skew-seidel-maxdet-34",
      "title": "skew seidel maxdet 34",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}

8Provenance

View source, identifiers, and projection details
Project
skew-seidel-maxdet-34
Locator
Inline Python 3 standard-library replay of Goethals and Seidel, executed on 2026-07-25
License
CC0-1.0
Contributors
TheoremDB entry research, 2026-07-25
Source
doi.org ↗
Public record
R751
Stable alias
ssm34-artifact-gs36-principal-minor
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.