verify_high_slope_independent.py

#!/usr/bin/env python3
"""Independent little-endian digit-list replay for the high-slope theorem.

This implementation does not use integer bit reversal or the symbolic
certificate's polynomial code.  It is a transcription check, not the all-q
proof.
"""

from __future__ import annotations

import json
from pathlib import Path


def digits(n: int) -> list[int]:
    out: list[int] = []
    while n:
        out.append(n & 1)
        n >>= 1
    return out or [0]


def normalize(word: list[int]) -> list[int]:
    while len(word) > 1 and word[-1] == 0:
        word.pop()
    return word


def reverse_canonical(word: list[int]) -> list[int]:
    return normalize(list(reversed(word)))


def add_words(left: list[int], right: list[int]) -> list[int]:
    width = max(len(left), len(right))
    out: list[int] = []
    carry = 0
    for index in range(width):
        total = carry
        if index < len(left):
            total += left[index]
        if index < len(right):
            total += right[index]
        out.append(total & 1)
        carry = total >> 1
    if carry:
        out.append(carry)
    return normalize(out)


def step(word: list[int]) -> tuple[list[int], int]:
    old_length = len(word)
    following = add_words(word, reverse_canonical(word))
    return following, len(following) - old_length


def trace(n: int, horizon: int) -> str:
    word = digits(n)
    output = []
    for _ in range(horizon):
        word, growth = step(word)
        output.append(str(growth))
    return "".join(output)


def main() -> None:
    records = []
    for q in (4, 5, 6, 7, 8, 9, 10, 11, 20, 40, 100):
        a_q = (1 << (9 * q - 1)) + 154
        b_q = (1 << (9 * q - 1)) + 1178
        divergence = 12 * q - 12
        horizon = divergence + 33
        left = trace(a_q, horizon)
        right = trace(b_q, horizon)
        expected_left = "011101111" + "10" * ((horizon - 9 + 1) // 2)
        assert left == expected_left[:horizon]
        assert left[:divergence] == right[:divergence]
        assert left[divergence] == "0"
        assert right[divergence] == "1"
        records.append(
            {
                "q": q,
                "source_length": 9 * q,
                "first_divergence": divergence,
            }
        )
    result = {
        "status": "pass",
        "implementation": "little-endian digit-list addition",
        "role": "independent transcription check; symbolic certificate carries the all-q proof",
        "records": records,
    }
    path = Path(__file__).with_name("independent-verification.json")
    path.write_text(json.dumps(result, indent=2, sort_keys=True) + "\n")
    print(json.dumps({"status": result["status"], "cases": len(records)}, indent=2))


if __name__ == "__main__":
    main()