TheoremDB

Problem packetResearch packetR674

R674Executable evidence

Bareiss regression and exact order-ten bound verifier

View replayOpen source ↗
Link to a section

Authored summary

A standard-library program enumerates all binary matrices through order four and checks every large-integer bound calculation.

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

Recorded status: available

Recorded scope: the exact structural bound arithmetic at order ten and exhaustive determinant enumeration for every binary square matrix of orders one through four

Complete recorded scope and conditions
{
  "kind": "bounded",
  "statement": "the exact structural bound arithmetic at order ten and exhaustive determinant enumeration for every binary square matrix of orders one through four",
  "bounds": {
    "bound_order": {
      "min": 10,
      "max": 10
    },
    "regression_order": {
      "min": 1,
      "max": 4
    },
    "largest_regression_space": {
      "min": 65536,
      "max": 65536
    }
  },
  "exhaustive": true
}

Originating problem: Number of singular ten by ten binary matrices over the reals

Recorded relationships: The singular count is between 126,174,821,830,345,268,667,240,568,576 and 901,210,462,928,281,273,073,900,978,176

Authored record and scope
Authored title
Bareiss regression and exact order-ten bound verifier
Record type
artifact
Stored status
available
Evidence grade
executable
Recorded scope data
{ "kind": "bounded", "statement": "the exact structural bound arithmetic at order ten and exhaustive determinant enumeration for every binary square matrix of orders one through four", "bounds": { "bound_order": { "min": 10, "max": 10 }, "regression_order": { "min": 1, "max": 4 }, "largest_regression_space": { "min": 65536, "max": 65536 } }, "exhaustive": true }
Linked research record IDs
R677

2Authored explanation

The verifier enumerates 2^(n^2) labeled matrices for n=1,2,3,4 and evaluates each determinant with fraction-free Bareiss elimination. It reproduces the singular counts 1, 10, 338, and 42,976. At order four it checks the full determinant histogram \[ -3:60,\ -2:1200,\ -1:10020,\ 0:42976,\ 1:10020,\ 2:1200,\ 3:60. \] The canonical count line has SHA-256 digest cb8f2c764fb76fd45e8557a6cb27b6c670e3526d60721dfdc093293f64825ae0. The histogram line has digest ab7118ff1c833f08b01258733186ebe654157be07d1705ae3c387000c14888a3.

The same program evaluates the falling-factorial Bonferroni expression, the order of GL(10,2), and both reduced probability fractions. The order-ten part certifies arithmetic and the combinatorial formulas stated in the claim. It does not enumerate 2^100 matrices.

Files and source

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

  • R674.txt2,624 bytes · No SHA-256 recorded
    Preview R674.txt
    from collections import Counter
    from fractions import Fraction
    from hashlib import sha256
    from math import comb, prod
    
    def determinant(rows):
        a=[row[:] for row in rows]
        n=len(a)
        if n==1:
            return a[0][0]
        sign=1
        previous=1
        for k in range(n-1):
            pivot_row=next((r for r in range(k,n) if a[r][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):
                    a[i][j]=(a[i][j]*pivot-a[i][k]*a[k][j])//previous
            for i in range(k+1,n):
                a[i][k]=0
            previous=pivot
        return sign*a[-1][-1]
    
    def histogram(n):
        out=Counter()
        for bits in range(1<<(n*n)):
            rows=[[(bits>>(r*n+c))&1 for c in range(n)] for r in range(n)]
            out[determinant(rows)]+=1
        return out
    
    expected_counts={1:1,2:10,3:338,4:42976}
    histograms={n:histogram(n) for n in range(1,5)}
    assert {n:histograms[n][0] for n in histograms}==expected_counts
    expected_hist4=Counter({-3:60,-2:1200,-1:10020,0:42976,1:10020,2:1200,3:60})
    assert histograms[4]==expected_hist4
    
    counts_text=','.join(f'{n}:{expected_counts[n]}' for n in sorted(expected_counts))
    hist4_text=','.join(f'{d}:{expected_hist4[d]}' for d in sorted(expected_hist4))
    assert sha256((counts_text+'\n').encode()).hexdigest()=='cb8f2c764fb76fd45e8557a6cb27b6c670e3526d60721dfdc093293f64825ae0'
    assert sha256((hist4_text+'\n').encode()).hexdigest()=='ab7118ff1c833f08b01258733186ebe654157be07d1705ae3c387000c14888a3'
    
    def falling(a,k):
        return prod(a-i for i in range(k))
    
    n=10
    total=1<<(n*n)
    row_bad=total-falling((1<<n)-1,n)
    column_extra=55*falling((1<<(n-1))-1,n)-comb(55,2)*falling((1<<(n-2))-1,n)
    lower=row_bad+column_extra
    gl2=prod((1<<n)-(1<<i) for i in range(n))
    upper=total-gl2
    assert total==1267650600228229401496703205376
    assert row_bad==66512166928711781758210744576
    assert column_extra==59662654901633486909029824000
    assert lower==126174821830345268667240568576
    assert gl2==366440137299948128422802227200
    assert upper==901210462928281273073900978176
    lower_fraction=Fraction(lower,total)
    upper_fraction=Fraction(upper,total)
    assert lower_fraction==Fraction(492870397774786205731408471,4951760157141521099596496896)
    assert upper_fraction==Fraction(25613941912987493,36028797018963968)
    
    report=f'n=10 total={total} lower={lower} upper={upper} lower_fraction={lower_fraction} upper_fraction={upper_fraction} regression={counts_text} histogram4={hist4_text}'
    print(report)
    print(sha256((report+'\n').encode()).hexdigest())
    File identity
    Recorded filename
    R674.txt
    Download SHA-256
    de3b3b25315f13513b861d9bf152da56e834a5e0c7606dbc638085cfa3ad5179
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 deterministic verifier prepared on 2026-07-25

Expected output

n=10 total=1267650600228229401496703205376 lower=126174821830345268667240568576 upper=901210462928281273073900978176 lower_fraction=492870397774786205731408471/4951760157141521099596496896 upper_fraction=25613941912987493/36028797018963968 regression=1:1,2:10,3:338,4:42976 histogram4=-3:60,-2:1200,-1:10020,0:42976,1:10020,2:1200,3:60
bf867a96b0c91ca818fe7c1d8767bba0653af2df133be55d7b1d25ad36817989

Missing for a complete replay: command.

Recorded artifact fields

5What it produced

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": "R674",
  "content_hash": null,
  "slug": "rsbm10-artifact-bounds-and-regression",
  "type": "artifact",
  "title": "Bareiss regression and exact order-ten bound verifier",
  "summary": "A standard-library program enumerates all binary matrices through order four and checks every large-integer bound calculation.",
  "relevance": "For Number of singular ten by ten binary matrices over the reals, record rsbm10-artifact-bounds-and-regression (“Bareiss regression and exact order-ten bound verifier”) supplies evidence or a replay used to check the packet. The record states: A standard-library program enumerates all binary matrices through order four and checks every large-integer bound calculation.",
  "relevance_source": "recorded",
  "body": "The verifier enumerates 2^(n^2) labeled matrices for n=1,2,3,4 and evaluates each determinant with fraction-free Bareiss elimination. It reproduces the singular counts 1, 10, 338, and 42,976. At order four it checks the full determinant histogram\n\\[\n-3:60,\\ -2:1200,\\ -1:10020,\\ 0:42976,\\ 1:10020,\\ 2:1200,\\ 3:60.\n\\]\nThe canonical count line has SHA-256 digest cb8f2c764fb76fd45e8557a6cb27b6c670e3526d60721dfdc093293f64825ae0. The histogram line has digest ab7118ff1c833f08b01258733186ebe654157be07d1705ae3c387000c14888a3.\n\nThe same program evaluates the falling-factorial Bonferroni expression, the order of GL(10,2), and both reduced probability fractions. The order-ten part certifies arithmetic and the combinatorial formulas stated in the claim. It does not enumerate 2^100 matrices.",
  "status": "available",
  "evidence_grade": "executable",
  "scope": {
    "kind": "bounded",
    "statement": "the exact structural bound arithmetic at order ten and exhaustive determinant enumeration for every binary square matrix of orders one through four",
    "bounds": {
      "bound_order": {
        "min": 10,
        "max": 10
      },
      "regression_order": {
        "min": 1,
        "max": 4
      },
      "largest_regression_space": {
        "min": 65536,
        "max": 65536
      }
    },
    "exhaustive": true
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "partial",
    "kind": "inline_python_deterministic_verifier",
    "entrypoint": "Join source_lines with LF characters and execute the resulting Python program",
    "runtime": "Python 3.10 or later, standard library only",
    "citation": {
      "url": "https://doi.org/10.1016/S0021-9800(67)80006-1",
      "locator": "Inline Python 3 deterministic verifier prepared on 2026-07-25"
    },
    "outputs": "n=10 total=1267650600228229401496703205376 lower=126174821830345268667240568576 upper=901210462928281273073900978176 lower_fraction=492870397774786205731408471/4951760157141521099596496896 upper_fraction=25613941912987493/36028797018963968 regression=1:1,2:10,3:338,4:42976 histogram4=-3:60,-2:1200,-1:10020,0:42976,1:10020,2:1200,3:60\nbf867a96b0c91ca818fe7c1d8767bba0653af2df133be55d7b1d25ad36817989\n",
    "inline_source": [
      "from collections import Counter",
      "from fractions import Fraction",
      "from hashlib import sha256",
      "from math import comb, prod",
      "",
      "def determinant(rows):",
      "    a=[row[:] for row in rows]",
      "    n=len(a)",
      "    if n==1:",
      "        return a[0][0]",
      "    sign=1",
      "    previous=1",
      "    for k in range(n-1):",
      "        pivot_row=next((r for r in range(k,n) if a[r][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):",
      "                a[i][j]=(a[i][j]*pivot-a[i][k]*a[k][j])//previous",
      "        for i in range(k+1,n):",
      "            a[i][k]=0",
      "        previous=pivot",
      "    return sign*a[-1][-1]",
      "",
      "def histogram(n):",
      "    out=Counter()",
      "    for bits in range(1<<(n*n)):",
      "        rows=[[(bits>>(r*n+c))&1 for c in range(n)] for r in range(n)]",
      "        out[determinant(rows)]+=1",
      "    return out",
      "",
      "expected_counts={1:1,2:10,3:338,4:42976}",
      "histograms={n:histogram(n) for n in range(1,5)}",
      "assert {n:histograms[n][0] for n in histograms}==expected_counts",
      "expected_hist4=Counter({-3:60,-2:1200,-1:10020,0:42976,1:10020,2:1200,3:60})",
      "assert histograms[4]==expected_hist4",
      "",
      "counts_text=','.join(f'{n}:{expected_counts[n]}' for n in sorted(expected_counts))",
      "hist4_text=','.join(f'{d}:{expected_hist4[d]}' for d in sorted(expected_hist4))",
      "assert sha256((counts_text+'\\n').encode()).hexdigest()=='cb8f2c764fb76fd45e8557a6cb27b6c670e3526d60721dfdc093293f64825ae0'",
      "assert sha256((hist4_text+'\\n').encode()).hexdigest()=='ab7118ff1c833f08b01258733186ebe654157be07d1705ae3c387000c14888a3'",
      "",
      "def falling(a,k):",
      "    return prod(a-i for i in range(k))",
      "",
      "n=10",
      "total=1<<(n*n)",
      "row_bad=total-falling((1<<n)-1,n)",
      "column_extra=55*falling((1<<(n-1))-1,n)-comb(55,2)*falling((1<<(n-2))-1,n)",
      "lower=row_bad+column_extra",
      "gl2=prod((1<<n)-(1<<i) for i in range(n))",
      "upper=total-gl2",
      "assert total==1267650600228229401496703205376",
      "assert row_bad==66512166928711781758210744576",
      "assert column_extra==59662654901633486909029824000",
      "assert lower==126174821830345268667240568576",
      "assert gl2==366440137299948128422802227200",
      "assert upper==901210462928281273073900978176",
      "lower_fraction=Fraction(lower,total)",
      "upper_fraction=Fraction(upper,total)",
      "assert lower_fraction==Fraction(492870397774786205731408471,4951760157141521099596496896)",
      "assert upper_fraction==Fraction(25613941912987493,36028797018963968)",
      "",
      "report=f'n=10 total={total} lower={lower} upper={upper} lower_fraction={lower_fraction} upper_fraction={upper_fraction} regression={counts_text} histogram4={hist4_text}'",
      "print(report)",
      "print(sha256((report+'\\n').encode()).hexdigest())"
    ],
    "missing": [
      "command"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://doi.org/10.1016/S0021-9800(67)80006-1",
    "locator": "Inline Python 3 deterministic verifier prepared on 2026-07-25"
  },
  "models": [],
  "continuation": null,
  "relations": [
    {
      "slug": "R677",
      "title": "The singular count is between 126,174,821,830,345,268,667,240,568,576 and 901,210,462,928,281,273,073,900,978,176",
      "object_type": "claim",
      "relation": "supports",
      "direction": "outgoing"
    },
    {
      "slug": "R678",
      "title": "The current exact table ends at order nine",
      "object_type": "claim",
      "relation": "tests",
      "direction": "outgoing"
    },
    {
      "slug": "real-singular-binary-matrices-ten",
      "title": "real singular binary matrices ten",
      "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.