TheoremDB
R381artifactStatus: availableEvidence: ReproducedReplay: completeexhaustive over its scope

[#R381] Exact deletion-contraction f-vectors for n=6 and n=7

View replay

1Summary

A standard-library Python replay computes every face count of VR(Q_6;4) and VR(Q_7;4), checks the n=6 graph isomorphism, and obtains reduced Euler characteristics -253 and -3937.

For each \(n\in\{6,7\}\), the program builds the graph whose edges join binary words at Hamming distance greater than four. Rips faces are independent sets of this graph. It computes the independence polynomial by \[ P_G(x)=P_{G-v}(x)+xP_{G-N[v]}(x), \] with exact integer coefficients, connected-component factorization, a maximum-induced-degree pivot, and memoization by the surviving vertex mask.

For \(n=6\), the 23 counts by face cardinality are `1, 64, 1792, 29120, 307440, 2239552, 11682944, 44769920, 128380880, 279211520, 464621248, 593908224, 582529360, 435648640, 245610720, 102886976, 31658620, 7189056, 1239840, 165760, 17584, 1408, 64`. They sum to 2,932,100,733 including the empty face. The maximum face cardinality is 22 and \(\widetilde\chi=-253\).

Reproduced evidence. Recorded scope: every face of VR(Q_n;4) for n=6 and n=7, counted exactly by cardinality.

2Reproduce

Replay: complete

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

python3 hypercube_rips_fvectors.py
Entry point
Join source_lines with LF characters, append one terminal LF, and save as hypercube_rips_fvectors.py
Runtime
CPython 3.12.13, standard library only, macOS arm64
Dependencies
[ { "name": "CPython standard library", "version": "3.12.13", "license": "Python-2.0" } ]
Recorded runtime
18

Verification source: Inline deterministic computation authored and executed on 2026-07-28 UTC

Expected output

{
  "source_sha256_including_terminal_lf": "eaa48f2d7152ad8e56393e6e02b67ef6146f73c719f6d1bd58797a8142e9ab31",
  "stdout_sha256": "e3cfcb2b5e4c667e435b2b6920acf56caccef5dce5f64c5ad7b40354e2270b8d",
  "replay_count": 2,
  "replays_byte_identical": true,
  "report_sha256_without_digest": "8643f0411d7db0b3e8692da568447b194be2ac8722b0bdd3197d3cdd8897b46d",
  "n6_edge_list_sha256": "b7ba57c50deb226143fef7af9bf1eeeda98ba2e6ffffab330a077d9216338dac",
  "n7_edge_list_sha256": "4ad9f235f4a4b00904bf8af3c1a8baf0ecbfb5f5b9e64209830ea7c12724a081",
  "n6_coordinate_map_sha256": "54fedb34e89ba1f791cdf47f4ba718d6964be4e60ea8614f6cbc5e17595815ce",
  "n6_counts_sha256": "fac3217af540f10fe5d1e69561d0b8706b10f468138c601b2e550d385e670dce",
  "n7_counts_sha256": "c9ccfc4896a2be8f7606af6e5c59768602662f05a6780f60947b7c20121a485a",
  "n6_total_faces_including_empty": 2932100733,
  "n7_total_faces_including_empty": 209570782049,
  "n6_reduced_euler_characteristic": -253,
  "n7_reduced_euler_characteristic": -3937
}

3Overview

For \(n=7\), the 30 counts are `1, 128, 6272, 159488, 2409792, 23483264, 156322432, 742564352, 2605928992, 6949231744, 14412507648, 23711476992, 31506817664, 34424345984, 31535692288, 24757907456, 17050663168, 10523630208, 5903704576, 3018193920, 1393044352, 570251648, 202612992, 61051648, 15211392, 3040128, 467712, 51968, 3712, 128`. They sum to 209,570,782,049 including the empty face. The maximum face cardinality is 29 and \(\widetilde\chi=-3937\).

Two fresh-process replays produced byte-identical standard output.

4Source code

View source code
Source code
#!/usr/bin/env python3
"""Exact f-vectors of VR(Q_6;4) and VR(Q_7;4)."""

import hashlib
import json
from functools import lru_cache

EXPECTED = {
    6: (
        1, 64, 1792, 29120, 307440, 2239552, 11682944, 44769920,
        128380880, 279211520, 464621248, 593908224, 582529360,
        435648640, 245610720, 102886976, 31658620, 7189056,
        1239840, 165760, 17584, 1408, 64,
    ),
    7: (
        1, 128, 6272, 159488, 2409792, 23483264, 156322432, 742564352,
        2605928992, 6949231744, 14412507648, 23711476992, 31506817664,
        34424345984, 31535692288, 24757907456, 17050663168,
        10523630208, 5903704576, 3018193920, 1393044352, 570251648,
        202612992, 61051648, 15211392, 3040128, 467712, 51968, 3712, 128,
    ),
}


def popcount(value):
    return bin(value).count("1")


def add(a, b):
    size = max(len(a), len(b))
    return tuple(
        (a[i] if i < len(a) else 0) + (b[i] if i < len(b) else 0)
        for i in range(size)
    )


def multiply(a, b):
    result = [0] * (len(a) + len(b) - 1)
    for i, x in enumerate(a):
        for j, y in enumerate(b):
            result[i + j] += x * y
    return tuple(result)


def solve(n):
    order = 1 << n
    all_vertices = (1 << order) - 1
    adjacency = tuple(
        sum(
            1 << w
            for w in range(order)
            if w != v and popcount(v ^ w) > 4
        )
        for v in range(order)
    )
    expected_degree = sum(
        1
        for difference in range(1, order)
        if popcount(difference) > 4
    )
    assert all(popcount(row) == expected_degree for row in adjacency)

    def components(mask):
        result = []
        remaining = mask
        while remaining:
            seed = remaining & -remaining
            component = seed
            frontier = seed
            while frontier:
                vertex_bit = frontier & -frontier
                frontier ^= vertex_bit
                vertex = vertex_bit.bit_length() - 1
                new = adjacency[vertex] & mask & ~component
                component |= new
                frontier |= new
            result.append(component)
            remaining &= ~component
        return result

    @lru_cache(maxsize=None)
    def polynomial(mask):
        if not mask:
            return (1,)
        parts = components(mask)
        if len(parts) > 1:
            result = (1,)
            for part in parts:
                result = multiply(result, polynomial(part))
            return result
        candidates = []
        remaining = mask
        while remaining:
            vertex_bit = remaining & -remaining
            remaining ^= vertex_bit
            vertex = vertex_bit.bit_length() - 1
            candidates.append((popcount(adjacency[vertex] & mask), vertex))
        vertex = max(candidates)[1]
        without_vertex = mask & ~(1 << vertex)
        excluded = polynomial(without_vertex)
        included_tail = polynomial(without_vertex & ~adjacency[vertex])
        return add(excluded, (0,) + included_tail)

    counts = polynomial(all_vertices)
    assert counts == EXPECTED[n]
    edges = [
        (u, v)
        for u in range(order)
        for v in range(u + 1, order)
        if adjacency[u] >> v & 1
    ]
    assert len(edges) == order * expected_degree // 2
    edge_encoding = "\n".join(f"{u},{v}" for u, v in edges) + "\n"
    count_encoding = json.dumps(counts, separators=(",", ":"))
    ordinary_euler = sum(
        (-1) ** (cardinality - 1) * count
        for cardinality, count in enumerate(counts)
        if cardinality
    )
    return {
        "n": n,
        "vertices": order,
        "forbidden_graph_degree": expected_degree,
        "forbidden_graph_edges": len(edges),
        "edge_list_sha256": hashlib.sha256(edge_encoding.encode()).hexdigest(),
        "independent_set_counts_by_cardinality": counts,
        "counts_sha256": hashlib.sha256(count_encoding.encode()).hexdigest(),
        "total_faces_including_empty": sum(counts),
        "maximum_face_cardinality": len(counts) - 1,
        "ordinary_euler_characteristic": ordinary_euler,
        "reduced_euler_characteristic": ordinary_euler - 1,
        "deletion_contraction_cache_states": polynomial.cache_info().currsize,
    }


def verify_n6_basis_change():
    n = 6
    order = 1 << n
    ones = order - 1

    def old_coordinates(coefficients):
        value = 0
        for i in range(n):
            if coefficients >> i & 1:
                value ^= ones ^ (1 << i)
        return value

    coordinate_map = tuple(old_coordinates(v) for v in range(order))
    assert len(set(coordinate_map)) == order
    for u in range(order):
        for v in range(u + 1, order):
            new_difference = u ^ v
            new_edge = popcount(new_difference) == 1 or new_difference == ones
            old_distance = popcount(coordinate_map[u] ^ coordinate_map[v])
            assert new_edge == (old_distance in (5, 6))
    return hashlib.sha256(bytes(coordinate_map)).hexdigest()


report = {
    "schema": "theoremdb-hypercube-rips-fvectors-v1",
    "method": "exact independence-polynomial deletion-contraction",
    "n6_basis_change": "the forbidden graph is Q_6 plus the antipodal matching",
    "n6_coordinate_map_sha256": verify_n6_basis_change(),
    "cases": [solve(6), solve(7)],
}
canonical = json.dumps(report, sort_keys=True, separators=(",", ":"))
report["report_sha256_without_digest"] = hashlib.sha256(canonical.encode()).hexdigest()
print(json.dumps(report, sort_keys=True, separators=(",", ":")))

5What it produced

Processor
Apple M4, arm64
Processor bound
one single-threaded CPython process on the recorded Apple M4
Time bound
120 seconds per replay on the recorded processor under concurrent local workload
Memory bound
1,040,498,688 bytes observed peak resident set; allow 1.25 GiB
Stopping rule
finish both exact deletion-contraction enumerations and every assertion for n=6 and n=7; no heuristic or node cutoff
Randomness
none
Precision
exact arbitrary-precision integer arithmetic
Source license
CC0-1.0
Network requirements
none
Storage bound
5,534-byte source and less than 4 KB of standard output; no auxiliary files
Peak resident bytes observed
1,040,498,688
Execution date
2026-07-28
Arithmetic
exact arbitrary-precision integers
Randomness
none
N6 cache states
143,848
N7 cache states
2,961,929

6How it connects

Evidence for

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": "R381",
  "content_hash": null,
  "slug": "hr4-artifact-exact-fvectors-six-seven",
  "type": "artifact",
  "title": "Exact deletion-contraction f-vectors for n=6 and n=7",
  "summary": "A standard-library Python replay computes every face count of VR(Q_6;4) and VR(Q_7;4), checks the n=6 graph isomorphism, and obtains reduced Euler characteristics -253 and -3937.",
  "relevance": "For Integral torsion in scale-four hypercube Rips complexes, record hr4-artifact-exact-fvectors-six-seven (“Exact deletion-contraction f-vectors for n=6 and n=7”) supplies evidence or a replay used to check the packet. The record states: A standard-library Python replay computes every face count of VR(Q_6;4) and VR(Q_7;4), checks the n=6 graph isomorphism, and obtains reduced Euler characteristics -253 and -3937.",
  "relevance_source": "recorded",
  "body": "For each \\(n\\in\\{6,7\\}\\), the program builds the graph whose edges join binary words at Hamming distance greater than four. Rips faces are independent sets of this graph. It computes the independence polynomial by\n\\[\nP_G(x)=P_{G-v}(x)+xP_{G-N[v]}(x),\n\\]\nwith exact integer coefficients, connected-component factorization, a maximum-induced-degree pivot, and memoization by the surviving vertex mask.\n\nFor \\(n=6\\), the 23 counts by face cardinality are\n`1, 64, 1792, 29120, 307440, 2239552, 11682944, 44769920, 128380880, 279211520, 464621248, 593908224, 582529360, 435648640, 245610720, 102886976, 31658620, 7189056, 1239840, 165760, 17584, 1408, 64`.\nThey sum to 2,932,100,733 including the empty face. The maximum face cardinality is 22 and \\(\\widetilde\\chi=-253\\).\n\nFor \\(n=7\\), the 30 counts are\n`1, 128, 6272, 159488, 2409792, 23483264, 156322432, 742564352, 2605928992, 6949231744, 14412507648, 23711476992, 31506817664, 34424345984, 31535692288, 24757907456, 17050663168, 10523630208, 5903704576, 3018193920, 1393044352, 570251648, 202612992, 61051648, 15211392, 3040128, 467712, 51968, 3712, 128`.\nThey sum to 209,570,782,049 including the empty face. The maximum face cardinality is 29 and \\(\\widetilde\\chi=-3937\\).\n\nTwo fresh-process replays produced byte-identical standard output.",
  "status": "available",
  "evidence_grade": "executable",
  "scope": {
    "kind": "bounded",
    "statement": "every face of VR(Q_n;4) for n=6 and n=7, counted exactly by cardinality",
    "bounds": {
      "cube_dimension": {
        "min": 6,
        "max": 7
      },
      "scale": {
        "min": 4,
        "max": 4
      },
      "n6_faces_including_empty": {
        "min": 2932100733,
        "max": 2932100733
      },
      "n7_faces_including_empty": {
        "min": 209570782049,
        "max": 209570782049
      }
    },
    "exhaustive": true
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "complete",
    "kind": "inline_python_exact_independence_polynomials",
    "command": "python3 hypercube_rips_fvectors.py",
    "entrypoint": "Join source_lines with LF characters, append one terminal LF, and save as hypercube_rips_fvectors.py",
    "runtime": "CPython 3.12.13, standard library only, macOS arm64",
    "citation": {
      "locator": "Inline deterministic computation authored and executed on 2026-07-28 UTC"
    },
    "dependencies": [
      {
        "name": "CPython standard library",
        "version": "3.12.13",
        "license": "Python-2.0"
      }
    ],
    "outputs": {
      "source_sha256_including_terminal_lf": "eaa48f2d7152ad8e56393e6e02b67ef6146f73c719f6d1bd58797a8142e9ab31",
      "stdout_sha256": "e3cfcb2b5e4c667e435b2b6920acf56caccef5dce5f64c5ad7b40354e2270b8d",
      "replay_count": 2,
      "replays_byte_identical": true,
      "report_sha256_without_digest": "8643f0411d7db0b3e8692da568447b194be2ac8722b0bdd3197d3cdd8897b46d",
      "n6_edge_list_sha256": "b7ba57c50deb226143fef7af9bf1eeeda98ba2e6ffffab330a077d9216338dac",
      "n7_edge_list_sha256": "4ad9f235f4a4b00904bf8af3c1a8baf0ecbfb5f5b9e64209830ea7c12724a081",
      "n6_coordinate_map_sha256": "54fedb34e89ba1f791cdf47f4ba718d6964be4e60ea8614f6cbc5e17595815ce",
      "n6_counts_sha256": "fac3217af540f10fe5d1e69561d0b8706b10f468138c601b2e550d385e670dce",
      "n7_counts_sha256": "c9ccfc4896a2be8f7606af6e5c59768602662f05a6780f60947b7c20121a485a",
      "n6_total_faces_including_empty": 2932100733,
      "n7_total_faces_including_empty": 209570782049,
      "n6_reduced_euler_characteristic": -253,
      "n7_reduced_euler_characteristic": -3937
    },
    "runtime_seconds": 18,
    "inline_source": [
      "#!/usr/bin/env python3",
      "\"\"\"Exact f-vectors of VR(Q_6;4) and VR(Q_7;4).\"\"\"",
      "",
      "import hashlib",
      "import json",
      "from functools import lru_cache",
      "",
      "EXPECTED = {",
      "    6: (",
      "        1, 64, 1792, 29120, 307440, 2239552, 11682944, 44769920,",
      "        128380880, 279211520, 464621248, 593908224, 582529360,",
      "        435648640, 245610720, 102886976, 31658620, 7189056,",
      "        1239840, 165760, 17584, 1408, 64,",
      "    ),",
      "    7: (",
      "        1, 128, 6272, 159488, 2409792, 23483264, 156322432, 742564352,",
      "        2605928992, 6949231744, 14412507648, 23711476992, 31506817664,",
      "        34424345984, 31535692288, 24757907456, 17050663168,",
      "        10523630208, 5903704576, 3018193920, 1393044352, 570251648,",
      "        202612992, 61051648, 15211392, 3040128, 467712, 51968, 3712, 128,",
      "    ),",
      "}",
      "",
      "",
      "def popcount(value):",
      "    return bin(value).count(\"1\")",
      "",
      "",
      "def add(a, b):",
      "    size = max(len(a), len(b))",
      "    return tuple(",
      "        (a[i] if i < len(a) else 0) + (b[i] if i < len(b) else 0)",
      "        for i in range(size)",
      "    )",
      "",
      "",
      "def multiply(a, b):",
      "    result = [0] * (len(a) + len(b) - 1)",
      "    for i, x in enumerate(a):",
      "        for j, y in enumerate(b):",
      "            result[i + j] += x * y",
      "    return tuple(result)",
      "",
      "",
      "def solve(n):",
      "    order = 1 << n",
      "    all_vertices = (1 << order) - 1",
      "    adjacency = tuple(",
      "        sum(",
      "            1 << w",
      "            for w in range(order)",
      "            if w != v and popcount(v ^ w) > 4",
      "        )",
      "        for v in range(order)",
      "    )",
      "    expected_degree = sum(",
      "        1",
      "        for difference in range(1, order)",
      "        if popcount(difference) > 4",
      "    )",
      "    assert all(popcount(row) == expected_degree for row in adjacency)",
      "",
      "    def components(mask):",
      "        result = []",
      "        remaining = mask",
      "        while remaining:",
      "            seed = remaining & -remaining",
      "            component = seed",
      "            frontier = seed",
      "            while frontier:",
      "                vertex_bit = frontier & -frontier",
      "                frontier ^= vertex_bit",
      "                vertex = vertex_bit.bit_length() - 1",
      "                new = adjacency[vertex] & mask & ~component",
      "                component |= new",
      "                frontier |= new",
      "            result.append(component)",
      "            remaining &= ~component",
      "        return result",
      "",
      "    @lru_cache(maxsize=None)",
      "    def polynomial(mask):",
      "        if not mask:",
      "            return (1,)",
      "        parts = components(mask)",
      "        if len(parts) > 1:",
      "            result = (1,)",
      "            for part in parts:",
      "                result = multiply(result, polynomial(part))",
      "            return result",
      "        candidates = []",
      "        remaining = mask",
      "        while remaining:",
      "            vertex_bit = remaining & -remaining",
      "            remaining ^= vertex_bit",
      "            vertex = vertex_bit.bit_length() - 1",
      "            candidates.append((popcount(adjacency[vertex] & mask), vertex))",
      "        vertex = max(candidates)[1]",
      "        without_vertex = mask & ~(1 << vertex)",
      "        excluded = polynomial(without_vertex)",
      "        included_tail = polynomial(without_vertex & ~adjacency[vertex])",
      "        return add(excluded, (0,) + included_tail)",
      "",
      "    counts = polynomial(all_vertices)",
      "    assert counts == EXPECTED[n]",
      "    edges = [",
      "        (u, v)",
      "        for u in range(order)",
      "        for v in range(u + 1, order)",
      "        if adjacency[u] >> v & 1",
      "    ]",
      "    assert len(edges) == order * expected_degree // 2",
      "    edge_encoding = \"\\n\".join(f\"{u},{v}\" for u, v in edges) + \"\\n\"",
      "    count_encoding = json.dumps(counts, separators=(\",\", \":\"))",
      "    ordinary_euler = sum(",
      "        (-1) ** (cardinality - 1) * count",
      "        for cardinality, count in enumerate(counts)",
      "        if cardinality",
      "    )",
      "    return {",
      "        \"n\": n,",
      "        \"vertices\": order,",
      "        \"forbidden_graph_degree\": expected_degree,",
      "        \"forbidden_graph_edges\": len(edges),",
      "        \"edge_list_sha256\": hashlib.sha256(edge_encoding.encode()).hexdigest(),",
      "        \"independent_set_counts_by_cardinality\": counts,",
      "        \"counts_sha256\": hashlib.sha256(count_encoding.encode()).hexdigest(),",
      "        \"total_faces_including_empty\": sum(counts),",
      "        \"maximum_face_cardinality\": len(counts) - 1,",
      "        \"ordinary_euler_characteristic\": ordinary_euler,",
      "        \"reduced_euler_characteristic\": ordinary_euler - 1,",
      "        \"deletion_contraction_cache_states\": polynomial.cache_info().currsize,",
      "    }",
      "",
      "",
      "def verify_n6_basis_change():",
      "    n = 6",
      "    order = 1 << n",
      "    ones = order - 1",
      "",
      "    def old_coordinates(coefficients):",
      "        value = 0",
      "        for i in range(n):",
      "            if coefficients >> i & 1:",
      "                value ^= ones ^ (1 << i)",
      "        return value",
      "",
      "    coordinate_map = tuple(old_coordinates(v) for v in range(order))",
      "    assert len(set(coordinate_map)) == order",
      "    for u in range(order):",
      "        for v in range(u + 1, order):",
      "            new_difference = u ^ v",
      "            new_edge = popcount(new_difference) == 1 or new_difference == ones",
      "            old_distance = popcount(coordinate_map[u] ^ coordinate_map[v])",
      "            assert new_edge == (old_distance in (5, 6))",
      "    return hashlib.sha256(bytes(coordinate_map)).hexdigest()",
      "",
      "",
      "report = {",
      "    \"schema\": \"theoremdb-hypercube-rips-fvectors-v1\",",
      "    \"method\": \"exact independence-polynomial deletion-contraction\",",
      "    \"n6_basis_change\": \"the forbidden graph is Q_6 plus the antipodal matching\",",
      "    \"n6_coordinate_map_sha256\": verify_n6_basis_change(),",
      "    \"cases\": [solve(6), solve(7)],",
      "}",
      "canonical = json.dumps(report, sort_keys=True, separators=(\",\", \":\"))",
      "report[\"report_sha256_without_digest\"] = hashlib.sha256(canonical.encode()).hexdigest()",
      "print(json.dumps(report, sort_keys=True, separators=(\",\", \":\")))"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": null,
    "locator": "Inline deterministic computation authored and executed on 2026-07-28 UTC"
  },
  "relations": [
    {
      "slug": "R388",
      "title": "Torsion-free through n=5 and no 2-primary torsion at n=6",
      "object_type": "claim",
      "relation": "evidences",
      "direction": "outgoing"
    },
    {
      "slug": "R390",
      "title": "The n=6 complex is an independence complex of Q_6 with antipodal edges",
      "object_type": "claim",
      "relation": "evidences",
      "direction": "outgoing"
    },
    {
      "slug": "R391",
      "title": "The n=7 complex has 209,570,782,049 faces and reduced Euler characteristic -3937",
      "object_type": "claim",
      "relation": "evidences",
      "direction": "outgoing"
    },
    {
      "slug": "hypercube-rips-scale-four-torsion-free",
      "title": "hypercube rips scale four torsion free",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}

8Provenance

View source, identifiers, and projection details
Project
hypercube-rips-scale-four-torsion-free-research
Locator
Inline deterministic computation authored and executed on 2026-07-28 UTC
License
CC0-1.0
Public record
R381
Stable alias
hr4-artifact-exact-fvectors-six-seven
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.