{
  "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"
    },
    "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",
      "expected_output"
    ]
  },
  "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"
  },
  "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"
    }
  ]
}