verify_row_count_barrier.py

#!/usr/bin/env python3
"""Finite audit for FPRD-T154, the universal row-count barrier."""

from __future__ import annotations

import json
from pathlib import Path


def continuation_count(alphabet_size: int, horizon: int) -> int:
    if alphabet_size == 1:
        return horizon + 1
    return (alphabet_size ** (horizon + 1) - 1) // (alphabet_size - 1)


def view_count(degree: int, radius: int) -> int:
    value = 2
    for _ in range(radius):
        value = 1 + 2 * value**degree
    return value


def readable_radius(horizon: int) -> int:
    return 0 if horizon == 0 else horizon + 1


def run() -> dict[str, object]:
    exact_cases = 0
    exact_row_inequalities = 0
    symbolic_cases = 0
    symbolic_exponent_inequalities = 0
    weak_degree_failures = 0
    weak_distance_failures = 0
    samples: list[dict[str, int]] = []

    # Exact big-integer recurrence checks. The upper corner has roughly
    # 5^8 bits and remains quick while exercising the actual V recurrence.
    for alphabet_size in range(1, 6):
        degree = max(2, alphabet_size)
        for horizon in range(0, 8):
            n_continuations = continuation_count(alphabet_size, horizon)
            radius = readable_radius(horizon)
            views = view_count(degree, radius)
            exact_cases += 1
            assert n_continuations <= views.bit_length() - 1
            exact_row_inequalities += 1
            if horizon in (0, 1, 4, 7):
                samples.append(
                    {
                        "alphabet_size": alphabet_size,
                        "horizon": horizon,
                        "degree": degree,
                        "radius": radius,
                        "continuations": n_continuations,
                        "floor_log2_views": views.bit_length() - 1,
                    }
                )

    # The proof reduces the large ranges to N_s(h) <= d^(h+1). This check
    # avoids constructing astronomically large view-count integers.
    for alphabet_size in range(1, 65):
        degree = max(2, alphabet_size)
        for horizon in range(0, 257):
            n_continuations = continuation_count(alphabet_size, horizon)
            exponent_floor = 1 if horizon == 0 else degree ** (horizon + 1)
            symbolic_cases += 1
            assert n_continuations <= exponent_floor
            symbolic_exponent_inequalities += 1

            # Mutant 1: reduce degree below the alphabet size.
            if alphabet_size >= 3 and horizon >= 1:
                if n_continuations > (alphabet_size - 1) ** (horizon + 1):
                    weak_degree_failures += 1

            # Mutant 2: distance one makes the readable radius stay one for
            # every positive horizon, whose recurrence lower exponent is d.
            if horizon >= 1 and n_continuations > degree:
                weak_distance_failures += 1

    assert weak_degree_failures > 0
    assert weak_distance_failures > 0

    return {
        "status": "pass",
        "exact_cases": exact_cases,
        "exact_row_inequalities": exact_row_inequalities,
        "symbolic_cases": symbolic_cases,
        "symbolic_exponent_inequalities": symbolic_exponent_inequalities,
        "weak_degree_failures": weak_degree_failures,
        "weak_distance_failures": weak_distance_failures,
        "samples": samples,
    }


if __name__ == "__main__":
    result = run()
    output = Path(__file__).with_name("checker-output.json")
    output.write_text(json.dumps(result, indent=2) + "\n", encoding="utf-8")
    print(json.dumps(result, indent=2))