TheoremDB
R1artifactStatus: availableEvidence: ReproducedReplay: completeexhaustive over its scope

[#R1] Exact affine-matrix prefilter for image lengths 8 through 12

View replay

1Summary

A standard-library Python program reduces the proposed morphism range to nine length patterns and 1,130 complement-conjugacy orbits of expanding length-sum matrices.

For a morphism on letters \(x=0,1,2,3\), affineness requires image lengths \(L_x=a+bx\) and image sums \(S_x=c+dx\). Requiring every \(L_x\) to lie in \([8,12]\) leaves nine length vectors. A sum is feasible precisely when \(0\le S_x\le3L_x\), since every integer in that interval is the sum of an \(L_x\)-letter word over \(\{0,1,2,3\}\).

For \(M=[[a,b],[c,d]]\), write \(T=a+d\) and \(D=ad-bc\). The program checks the expanding-eigenvalue condition with exact integer arithmetic by applying the quadratic Schur criterion to the reciprocal eigenvalues. Its three inequalities are \((D-T+1)D>0\), \((D+T+1)D>0\), and \((D-1)D>0\), with \(D\ne0\).

Reproduced evidence. Recorded scope: every affine integer length-sum matrix whose four image lengths lie between 8 and 12 and whose image sums are feasible over {0,1,2,3}.

2Reproduce

Replay: complete

The command, source, environment, and expected result are recorded.

python3 affine_matrix_prefilter.py
Entry point
Join source_lines with LF characters and append one terminal LF as affine_matrix_prefilter.py; source_sha256 includes that terminal LF
Runtime
Python 3.9.6, standard library only
Dependencies
[ { "name": "CPython", "version": "3.9.6", "license": "PSF-2.0" }, { "name": "Python standard library", "version": "3.9.6", "license": "PSF-2.0" } ]
Recorded runtime
0.06

Verification source: Inline Python 3 prefilter prepared and executed on 2026-07-28; expansion conditions follow Andrade and Mol, Theorem 2.4

Expected output

{
  "source_sha256": "2147f9a1e0a2d154db7fdbdcef945659a1ae16938a829057f08a11d8806b1214",
  "payload_sha256_including_final_lf": "49f895c7213dcda80907260baa61bbc59b512ea3aab65a07d44e5d495692a368",
  "stdout_sha256": "adac34c2add54bb7b89faa2c828c105873828241921871725b67ced7cf5c8573",
  "length_patterns": [
    [
      8,
      8,
      8,
      8
    ],
    [
      8,
      9,
      10,
      11
    ],
    [
      9,
      9,
      9,
      9
    ],
    [
      9,
      10,
      11,
      12
    ],
    [
      10,
      10,
      10,
      10
    ],
    [
      11,
      10,
      9,
      8
    ],
    [
      11,
      11,
      11,
      11
    ],
    [
      12,
      11,
      10,
      9
    ],
    [
      12,
      12,
      12,
      12
    ]
  ],
  "feasible_sum_matrices": 2895,
  "nonsingular_matrices": 2724,
  "expanding_matrices": 2212,
  "complement_fixed_matrices": 48,
  "complement_matrix_orbits": 1130,
  "maximum_resident_bytes": 11649024
}

3Overview

The exhaustive matrix-level pass finds 2,895 feasible length-sum matrices, of which 2,724 are nonsingular and 2,212 meet the expanding condition. Complement conjugation sends \((a,b,c,d)\) to \((a+3b,-b,3a+9b-c-3d,d-3b)\). It is an involution on the expanding set, with 48 fixed matrices and 1,130 orbits. Prolongability and additive-cube avoidance remain word-level stages in the recommended experiment.

4Source code

View source code
Source code
from hashlib import sha256
import json


def expanding_matrix(a, b, c, d):
    determinant = a * d - b * c
    trace = a + d
    if determinant == 0:
        return False
    return (
        (determinant - trace + 1) * determinant > 0
        and (determinant + trace + 1) * determinant > 0
        and (determinant - 1) * determinant > 0
    )


def complement_conjugate(matrix):
    a, b, c, d = matrix
    return a + 3 * b, -b, 3 * a + 9 * b - c - 3 * d, d - 3 * b


rows = []
expanding_set = set()
for a in range(8, 13):
    for b in range(-4, 5):
        lengths = [a + b * x for x in range(4)]
        if any(length < 8 or length > 12 for length in lengths):
            continue
        feasible = 0
        nonsingular = 0
        expanding = 0
        for c in range(3 * lengths[0] + 1):
            for d in range(-36, 37):
                sums = [c + d * x for x in range(4)]
                if any(total < 0 or total > 3 * lengths[x]
                       for x, total in enumerate(sums)):
                    continue
                feasible += 1
                nonsingular += a * d - b * c != 0
                is_expanding = expanding_matrix(a, b, c, d)
                expanding += is_expanding
                if is_expanding:
                    expanding_set.add((a, b, c, d))
        rows.append({
            "lengths": lengths,
            "feasible_sum_matrices": feasible,
            "nonsingular_matrices": nonsingular,
            "expanding_matrices": expanding,
        })

assert all(complement_conjugate(matrix) in expanding_set
           for matrix in expanding_set)
fixed_matrices = sum(complement_conjugate(matrix) == matrix
                     for matrix in expanding_set)
complement_orbits = {
    min(matrix, complement_conjugate(matrix))
    for matrix in expanding_set
}

report = {
    "complement_conjugacy": {
        "fixed_matrices": fixed_matrices,
        "matrix_orbits": len(complement_orbits),
    },
    "image_length_interval": [8, 12],
    "length_patterns": rows,
    "number_of_length_patterns": len(rows),
    "totals": {
        "feasible_sum_matrices": sum(row["feasible_sum_matrices"] for row in rows),
        "nonsingular_matrices": sum(row["nonsingular_matrices"] for row in rows),
        "expanding_matrices": sum(row["expanding_matrices"] for row in rows),
    },
}
payload = json.dumps(report, sort_keys=True, separators=(",", ":"))
print(payload)
print(sha256((payload + "\n").encode()).hexdigest())

5What it produced

Processor
Apple M4, arm64
Time bound
10 seconds wall clock
Memory bound
128 MiB resident memory
Processor bound
one CPython process with no worker threads
Network requirements
none
Artifact license
CC0-1.0
Arithmetic
exact integer
Randomness
none
Network during execution
none
Matrix level exhaustive
yes
Word level exhaustive
no

Storage bound

working storage bound bytes10,000measured replay files bytes3,720included files2,472-byte source and 1,248-byte captured stdout

6How it connects

Depended on by

Recorded for

7Agent packet

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

View structured packet
json
{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R1",
  "content_hash": null,
  "slug": "ac0123-artifact-affine-matrix-prefilter",
  "type": "artifact",
  "title": "Exact affine-matrix prefilter for image lengths 8 through 12",
  "summary": "A standard-library Python program reduces the proposed morphism range to nine length patterns and 1,130 complement-conjugacy orbits of expanding length-sum matrices.",
  "relevance": "For Additive-cube avoidance on the alphabet zero through three, record ac0123-artifact-affine-matrix-prefilter (“Exact affine-matrix prefilter for image lengths 8 through 12”) supplies evidence or a replay used to check the packet. The record states: A standard-library Python program reduces the proposed morphism range to nine length patterns and 1,130 complement-conjugacy orbits of expanding length-sum matrices.",
  "relevance_source": "recorded",
  "body": "For a morphism on letters \\(x=0,1,2,3\\), affineness requires image lengths \\(L_x=a+bx\\) and image sums \\(S_x=c+dx\\). Requiring every \\(L_x\\) to lie in \\([8,12]\\) leaves nine length vectors. A sum is feasible precisely when \\(0\\le S_x\\le3L_x\\), since every integer in that interval is the sum of an \\(L_x\\)-letter word over \\(\\{0,1,2,3\\}\\).\n\nFor \\(M=[[a,b],[c,d]]\\), write \\(T=a+d\\) and \\(D=ad-bc\\). The program checks the expanding-eigenvalue condition with exact integer arithmetic by applying the quadratic Schur criterion to the reciprocal eigenvalues. Its three inequalities are \\((D-T+1)D>0\\), \\((D+T+1)D>0\\), and \\((D-1)D>0\\), with \\(D\\ne0\\).\n\nThe exhaustive matrix-level pass finds 2,895 feasible length-sum matrices, of which 2,724 are nonsingular and 2,212 meet the expanding condition. Complement conjugation sends \\((a,b,c,d)\\) to \\((a+3b,-b,3a+9b-c-3d,d-3b)\\). It is an involution on the expanding set, with 48 fixed matrices and 1,130 orbits. Prolongability and additive-cube avoidance remain word-level stages in the recommended experiment.",
  "status": "available",
  "evidence_grade": "executable",
  "scope": {
    "kind": "bounded",
    "statement": "every affine integer length-sum matrix whose four image lengths lie between 8 and 12 and whose image sums are feasible over {0,1,2,3}",
    "bounds": {
      "image_length": {
        "min": 8,
        "max": 12
      },
      "alphabet_size": {
        "min": 4,
        "max": 4
      }
    },
    "exhaustive": true
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "complete",
    "kind": "inline_python3_exact_affine_matrix_prefilter",
    "command": "python3 affine_matrix_prefilter.py",
    "entrypoint": "Join source_lines with LF characters and append one terminal LF as affine_matrix_prefilter.py; source_sha256 includes that terminal LF",
    "runtime": "Python 3.9.6, standard library only",
    "citation": {
      "locator": "Inline Python 3 prefilter prepared and executed on 2026-07-28; expansion conditions follow Andrade and Mol, Theorem 2.4"
    },
    "dependencies": [
      {
        "name": "CPython",
        "version": "3.9.6",
        "license": "PSF-2.0"
      },
      {
        "name": "Python standard library",
        "version": "3.9.6",
        "license": "PSF-2.0"
      }
    ],
    "outputs": {
      "source_sha256": "2147f9a1e0a2d154db7fdbdcef945659a1ae16938a829057f08a11d8806b1214",
      "payload_sha256_including_final_lf": "49f895c7213dcda80907260baa61bbc59b512ea3aab65a07d44e5d495692a368",
      "stdout_sha256": "adac34c2add54bb7b89faa2c828c105873828241921871725b67ced7cf5c8573",
      "length_patterns": [
        [
          8,
          8,
          8,
          8
        ],
        [
          8,
          9,
          10,
          11
        ],
        [
          9,
          9,
          9,
          9
        ],
        [
          9,
          10,
          11,
          12
        ],
        [
          10,
          10,
          10,
          10
        ],
        [
          11,
          10,
          9,
          8
        ],
        [
          11,
          11,
          11,
          11
        ],
        [
          12,
          11,
          10,
          9
        ],
        [
          12,
          12,
          12,
          12
        ]
      ],
      "feasible_sum_matrices": 2895,
      "nonsingular_matrices": 2724,
      "expanding_matrices": 2212,
      "complement_fixed_matrices": 48,
      "complement_matrix_orbits": 1130,
      "maximum_resident_bytes": 11649024
    },
    "runtime_seconds": 0.06,
    "inline_source": [
      "from hashlib import sha256",
      "import json",
      "",
      "",
      "def expanding_matrix(a, b, c, d):",
      "    determinant = a * d - b * c",
      "    trace = a + d",
      "    if determinant == 0:",
      "        return False",
      "    return (",
      "        (determinant - trace + 1) * determinant > 0",
      "        and (determinant + trace + 1) * determinant > 0",
      "        and (determinant - 1) * determinant > 0",
      "    )",
      "",
      "",
      "def complement_conjugate(matrix):",
      "    a, b, c, d = matrix",
      "    return a + 3 * b, -b, 3 * a + 9 * b - c - 3 * d, d - 3 * b",
      "",
      "",
      "rows = []",
      "expanding_set = set()",
      "for a in range(8, 13):",
      "    for b in range(-4, 5):",
      "        lengths = [a + b * x for x in range(4)]",
      "        if any(length < 8 or length > 12 for length in lengths):",
      "            continue",
      "        feasible = 0",
      "        nonsingular = 0",
      "        expanding = 0",
      "        for c in range(3 * lengths[0] + 1):",
      "            for d in range(-36, 37):",
      "                sums = [c + d * x for x in range(4)]",
      "                if any(total < 0 or total > 3 * lengths[x]",
      "                       for x, total in enumerate(sums)):",
      "                    continue",
      "                feasible += 1",
      "                nonsingular += a * d - b * c != 0",
      "                is_expanding = expanding_matrix(a, b, c, d)",
      "                expanding += is_expanding",
      "                if is_expanding:",
      "                    expanding_set.add((a, b, c, d))",
      "        rows.append({",
      "            \"lengths\": lengths,",
      "            \"feasible_sum_matrices\": feasible,",
      "            \"nonsingular_matrices\": nonsingular,",
      "            \"expanding_matrices\": expanding,",
      "        })",
      "",
      "assert all(complement_conjugate(matrix) in expanding_set",
      "           for matrix in expanding_set)",
      "fixed_matrices = sum(complement_conjugate(matrix) == matrix",
      "                     for matrix in expanding_set)",
      "complement_orbits = {",
      "    min(matrix, complement_conjugate(matrix))",
      "    for matrix in expanding_set",
      "}",
      "",
      "report = {",
      "    \"complement_conjugacy\": {",
      "        \"fixed_matrices\": fixed_matrices,",
      "        \"matrix_orbits\": len(complement_orbits),",
      "    },",
      "    \"image_length_interval\": [8, 12],",
      "    \"length_patterns\": rows,",
      "    \"number_of_length_patterns\": len(rows),",
      "    \"totals\": {",
      "        \"feasible_sum_matrices\": sum(row[\"feasible_sum_matrices\"] for row in rows),",
      "        \"nonsingular_matrices\": sum(row[\"nonsingular_matrices\"] for row in rows),",
      "        \"expanding_matrices\": sum(row[\"expanding_matrices\"] for row in rows),",
      "    },",
      "}",
      "payload = json.dumps(report, sort_keys=True, separators=(\",\", \":\"))",
      "print(payload)",
      "print(sha256((payload + \"\\n\").encode()).hexdigest())"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": null,
    "locator": "Inline Python 3 prefilter prepared and executed on 2026-07-28; expansion conditions follow Andrade and Mol, Theorem 2.4"
  },
  "relations": [
    {
      "slug": "R6",
      "title": "Search beyond image length seven with a decision certificate",
      "object_type": "attempt",
      "relation": "uses",
      "direction": "incoming"
    },
    {
      "slug": "R2",
      "title": "Exact additive-cube-free image pools through length 12",
      "object_type": "artifact",
      "relation": "depends_on",
      "direction": "incoming"
    },
    {
      "slug": "additive-cube-four-term-progression-alphabet",
      "title": "additive cube four term progression alphabet",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}

8Provenance

View source, identifiers, and projection details
Project
additive-cube-four-term-progression-alphabet-research
Locator
Inline Python 3 prefilter prepared and executed on 2026-07-28; expansion conditions follow Andrade and Mol, Theorem 2.4
License
CC0-1.0
Public record
R1
Stable alias
ac0123-artifact-affine-matrix-prefilter
Projection
Reproduction fields are derived from the immutable record.

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

Report a problem

Your ChatGPT account

Opening ChatGPT

ChatGPT is opening in a new tab.