{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R621",
  "content_hash": null,
  "slug": "qafp-artifact-incidence-replay",
  "type": "artifact",
  "title": "Exact enumeration of the 11,811 by 2,667 cover matrix",
  "summary": "A standard-library program enumerates every binary line and plane, verifies all degrees and forced intersection counts, and hashes the ordered incidence rows.",
  "relevance": "For A binary q-analog of the Fano plane, record qafp-artifact-incidence-replay (“Exact enumeration of the 11,811 by 2,667 cover matrix”) supplies evidence or a replay used to check the packet. The record states: A standard-library program enumerates every binary line and plane, verifies all degrees and forced intersection counts, and hashes the ordered incidence rows.",
  "relevance_source": "recorded",
  "body": "Nonzero vectors are represented by the integers 1 through 127. A subspace is represented by a bit mask of its nonzero vectors. The program enumerates lines from independent pairs and planes from independent triples, then forms the seven line indices in every plane.\n\nThe resulting exact-cover matrix has 82,677 ones. Every line column has degree 31. The compact JSON list of the 11,811 ordered rows has SHA-256 digest `f80714bf2a15e8bae29e0a871d2330b7b201b0426e708b066853c304367c704b`. The program also replays the block, point, 5-space, hyperplane, and solid-intersection calculations. Its canonical report has digest `38f17c035e648a2dec9064ec2ed5558ecfe1b3cb9313ee56801dc8ea2fa43db9`.",
  "status": "available",
  "evidence_grade": "executable",
  "scope": {
    "kind": "bounded",
    "statement": "all 2-dimensional and 3-dimensional subspaces of F_2^7 and the complete line-plane incidence matrix",
    "bounds": {
      "nonzero_vectors": {
        "min": 127,
        "max": 127
      },
      "lines": {
        "min": 2667,
        "max": 2667
      },
      "planes": {
        "min": 11811,
        "max": 11811
      }
    },
    "exhaustive": true
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "partial",
    "kind": "inline_python_exact_enumeration",
    "entrypoint": "join source_lines with newline and run with python3",
    "runtime": "CPython 3, standard library only",
    "citation": {
      "url": "https://doi.org/10.15495/EPub_UBT_00008787",
      "locator": "Inline CPython standard-library computation executed by TheoremDB entry research on 2026-07-25"
    },
    "inline_source": [
      "from collections import Counter",
      "from hashlib import sha256",
      "from itertools import combinations",
      "from json import dumps",
      "from math import prod",
      "",
      "def qbinom(n, k, q=2):",
      "    if k < 0 or k > n:",
      "        return 0",
      "    k = min(k, n-k)",
      "    num = prod(q**(n-i)-1 for i in range(k))",
      "    den = prod(q**(k-i)-1 for i in range(k))",
      "    return num // den",
      "",
      "def vector_mask(vectors):",
      "    return sum(1 << v for v in vectors)",
      "",
      "points = tuple(range(1, 128))",
      "lines = set()",
      "for a, b in combinations(points, 2):",
      "    if a != b:",
      "        lines.add(vector_mask((a, b, a ^ b)))",
      "lines = tuple(sorted(lines))",
      "line_index = {line: i for i, line in enumerate(lines)}",
      "",
      "planes = set()",
      "for a, b, c in combinations(points, 3):",
      "    if c == (a ^ b):",
      "        continue",
      "    vectors = {a, b, c, a ^ b, a ^ c, b ^ c, a ^ b ^ c}",
      "    if len(vectors) == 7:",
      "        planes.add(vector_mask(vectors))",
      "planes = tuple(sorted(planes))",
      "",
      "matrix_rows = []",
      "degrees = Counter()",
      "for plane in planes:",
      "    vectors = [v for v in points if plane >> v & 1]",
      "    contained = sorted({line_index[vector_mask((a, b, a ^ b))]",
      "                        for a, b in combinations(vectors, 2)})",
      "    assert len(contained) == 7",
      "    matrix_rows.append(contained)",
      "    degrees.update(contained)",
      "",
      "assert [qbinom(7, k) for k in range(8)] == [1, 127, 2667, 11811, 11811, 2667, 127, 1]",
      "assert len(lines) == 2667 and len(planes) == 11811",
      "assert set(degrees.values()) == {31}",
      "assert sum(degrees.values()) == 82677",
      "blocks = qbinom(7, 2) // qbinom(3, 2)",
      "assert blocks == 381",
      "assert blocks * 7 == len(lines)",
      "per_point = blocks * qbinom(3, 1) // qbinom(7, 1)",
      "per_5space = blocks * qbinom(4, 2) // qbinom(7, 5)",
      "per_hyperplane = blocks * qbinom(4, 3) // qbinom(7, 6)",
      "assert (per_point, per_5space, per_hyperplane) == (21, 5, 45)",
      "intersection_types = {'solid_without_block': [136, 210, 35, 0],",
      "                      'solid_with_block': [128, 224, 28, 1]}",
      "for vector in intersection_types.values():",
      "    assert sum(vector) == blocks",
      "    assert vector[1] + 3*vector[2] + 7*vector[3] == qbinom(4, 1) * per_point",
      "    assert vector[2] + 7*vector[3] == qbinom(4, 2)",
      "solids_with_block = blocks * qbinom(4, 1)",
      "solids_without_block = qbinom(7, 4) - solids_with_block",
      "assert (solids_without_block, solids_with_block) == (6096, 5715)",
      "matrix_payload = dumps(matrix_rows, separators=(',', ':'))",
      "matrix_digest = sha256(matrix_payload.encode()).hexdigest()",
      "report = {",
      "    'blocks_required': blocks,",
      "    'exact_cover_columns': len(lines),",
      "    'exact_cover_ones': sum(degrees.values()),",
      "    'exact_cover_rows': len(planes),",
      "    'gaussian_7': [qbinom(7, k) for k in range(8)],",
      "    'intersection_types': intersection_types,",
      "    'line_column_degree': min(degrees.values()),",
      "    'matrix_rows_sha256': matrix_digest,",
      "    'per_5space': per_5space,",
      "    'per_hyperplane': per_hyperplane,",
      "    'per_point': per_point,",
      "    'solids_by_type': [solids_without_block, solids_with_block],",
      "}",
      "payload = dumps(report, sort_keys=True, separators=(',', ':'))",
      "digest = sha256(payload.encode()).hexdigest()",
      "assert matrix_digest == 'f80714bf2a15e8bae29e0a871d2330b7b201b0426e708b066853c304367c704b'",
      "assert digest == '38f17c035e648a2dec9064ec2ed5558ecfe1b3cb9313ee56801dc8ea2fa43db9'",
      "print(payload)",
      "print('sha256=' + digest)"
    ],
    "missing": [
      "command",
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://doi.org/10.15495/EPub_UBT_00008787",
    "locator": "Inline CPython standard-library computation executed by TheoremDB entry research on 2026-07-25"
  },
  "models": [],
  "relations": [
    {
      "slug": "R624",
      "title": "Every solution has 381 blocks and fixed local incidence counts",
      "object_type": "claim",
      "relation": "verifies",
      "direction": "outgoing"
    },
    {
      "slug": "R626",
      "title": "Any solution has at most one nonidentity automorphism and tightly fixed intersections",
      "object_type": "claim",
      "relation": "supports",
      "direction": "outgoing"
    },
    {
      "slug": "q-analog-fano-plane",
      "title": "q analog fano plane",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}