verify_grid_scaffold.py

#!/usr/bin/env python3
"""Finite audit for the degree-two, distance-two scaffold grid construction.

The mathematical note proves the construction for every rectangle.  This
checker builds every rectangle through 32 by 32, evaluates the literal
scaffold descriptors, and compares the resulting undirected graph with the
corresponding Cartesian grid.
"""

from __future__ import annotations

import json


MISSING = None


def follow(nodes: list[tuple[int | None, int | None]], root: int, path: tuple[int, ...]) -> int | None:
    current: int | None = root
    for port in path:
        if current is None:
            return None
        current = nodes[current][port]
    return current


def build_grid(rows: int, columns: int) -> tuple[list[tuple[int | None, int | None]], dict[tuple[int, int], int], int]:
    assert rows >= 1 and columns >= 1
    nodes: list[tuple[int | None, int | None]] = []
    cells: dict[tuple[int, int], int] = {}
    descriptor_evaluations = 0

    order: list[tuple[int, int, str]] = []
    for row in range(rows):
        columns_in_order = range(columns) if row % 2 == 0 else range(columns - 1, -1, -1)
        for offset, column in enumerate(columns_in_order):
            if row == 0 and offset == 0:
                symbol = "A"
            elif row == 0:
                symbol = "H"
            elif offset == 0:
                symbol = "V"
            else:
                symbol = "C"
            order.append((row, column, symbol))

    for row, column, symbol in order:
        if symbol == "A":
            horizontal = vertical = MISSING
        elif symbol == "H":
            horizontal = len(nodes) - 1
            vertical = MISSING
        elif symbol == "V":
            horizontal = MISSING
            vertical = len(nodes) - 1
        else:
            old_root = len(nodes) - 1
            horizontal = old_root
            vertical = follow(nodes, old_root, (1, 0))
            descriptor_evaluations += 1
            assert vertical is not None
        node = len(nodes)
        nodes.append((horizontal, vertical))
        cells[(row, column)] = node

    return nodes, cells, descriptor_evaluations


def graph_edges(nodes: list[tuple[int | None, int | None]]) -> set[frozenset[int]]:
    return {
        frozenset((node, target))
        for node, ports in enumerate(nodes)
        for target in ports
        if target is not None
    }


def expected_edges(rows: int, columns: int, cells: dict[tuple[int, int], int]) -> set[frozenset[int]]:
    edges: set[frozenset[int]] = set()
    for row in range(rows):
        for column in range(columns):
            if row:
                edges.add(frozenset((cells[(row, column)], cells[(row - 1, column)])))
            if column:
                edges.add(frozenset((cells[(row, column)], cells[(row, column - 1)])))
    return edges


def audit() -> dict[str, object]:
    rectangles = cells_checked = edges_checked = descriptor_evaluations = 0
    square_grid_checks = 0
    for rows in range(1, 33):
        for columns in range(1, 33):
            nodes, cells, evaluations = build_grid(rows, columns)
            actual = graph_edges(nodes)
            expected = expected_edges(rows, columns, cells)
            assert len(nodes) == rows * columns
            assert actual == expected
            for (row, column), node in cells.items():
                horizontal, vertical = nodes[node]
                if horizontal is not None:
                    other = next(position for position, identifier in cells.items() if identifier == horizontal)
                    assert other[0] == row and abs(other[1] - column) == 1
                if vertical is not None:
                    assert vertical == cells[(row - 1, column)]
            rectangles += 1
            cells_checked += len(nodes)
            edges_checked += len(actual)
            descriptor_evaluations += evaluations
            if rows == columns:
                square_grid_checks += 1

    return {
        "status": "pass",
        "scope": "all rectangular grids through 32 by 32",
        "degree": 2,
        "distance": 2,
        "control_states": 1,
        "working_labels": 1,
        "input_symbols": ["A", "H", "V", "C"],
        "rectangles": rectangles,
        "cells_checked": cells_checked,
        "edges_checked": edges_checked,
        "length_two_descriptor_evaluations": descriptor_evaluations,
        "square_grid_checks": square_grid_checks,
        "does_not_verify": [
            "the standard theorem that the n by n grid has treewidth n",
            "a pumping theorem or lower bound for scaffold languages",
            "that every scaffold computation has unbounded treewidth",
            "novelty beyond the explicit scaffold construction",
        ],
    }


if __name__ == "__main__":
    print(json.dumps(audit(), indent=2))