audit_weighted_height_boundaries.py

#!/usr/bin/env python3
"""Independent finite audit for FPRD-T72--T74.

The finite checks support, but do not replace, the written proofs.  The script
uses only the Python standard library and emits a deterministic JSON receipt.
"""

from __future__ import annotations

import itertools
import json
from collections import defaultdict


def parity_comb_word(j: int) -> str:
    carrier = "a" if j % 2 == 0 else "d"
    return "b" * j + "c" + carrier * (2**j)


def parity_comb_value(j: int) -> int:
    return (1 if j % 2 == 0 else -1) * (2**j)


def normalized_residual_signature(prefix: str, graph: dict[str, int]) -> tuple:
    residual = {
        word[len(prefix) :]: value
        for word, value in graph.items()
        if word.startswith(prefix)
    }
    if not residual:
        raise AssertionError("only live prefixes are signed")
    anchor = min(residual)
    offset = residual[anchor]
    return tuple(sorted((suffix, value - offset) for suffix, value in residual.items()))


def audit_parity_comb() -> dict:
    tested = []
    total_prefixes = 0
    total_gauges = 0
    for k in range(3, 11):
        graph = {parity_comb_word(j): parity_comb_value(j) for j in range(k + 1)}
        prefixes = {word[:i] for word in graph for i in range(len(word) + 1)}
        signatures = {normalized_residual_signature(prefix, graph) for prefix in prefixes}
        expected_states = k + 3 * 2 ** (k - 1) + 2
        assert len(signatures) == expected_states
        total_prefixes += len(prefixes)

        delta = lambda j: 3 * 2 ** (j - 2)
        best = None
        minimizers = []
        for lam in range(-12, 13):
            # The constant c affects only the final coordinate and can always
            # make it zero, so it does not enter the remaining maximum.
            coords = [-3 + 2 * lam]
            coords.extend(
                (1 + lam) * delta(j) + 2 * lam
                for j in range(2, k + 1, 2)
            )
            coords.extend(
                (lam - 1) * delta(j) + 2 * lam
                for j in range(3, k + 1, 2)
            )
            height = max(abs(value) for value in coords)
            total_gauges += 1
            if best is None or height < best:
                best = height
                minimizers = [lam]
            elif height == best:
                minimizers.append(lam)
        expected_height = 3 * 2 ** (k - 2)
        assert best == expected_height
        assert 0 in minimizers
        # Raw height zero would force equal repaired values at w_0 and w_2.
        assert all(3 + 5 * lam != 0 for lam in range(-12, 13))
        tested.append(
            {
                "k": k,
                "horizon": k + 1 + 2**k,
                "states": len(signatures),
                "canonical_height": best,
                "tested_integer_gauge_minimizers": minimizers,
            }
        )
    return {
        "families": tested,
        "live_prefixes_signed": total_prefixes,
        "integer_gauges_checked": total_gauges,
        "hostile_boundary": "The source theorem starts at k=3; the public statement must not omit this hypothesis.",
    }


def min_count(word: str) -> int:
    return -min(word.count("a"), word.count("b"))


def tracker_step(state: int, letter: str, cap: int) -> tuple[int, int]:
    if letter == "a":
        return min(cap, state + 1), (-1 if state < 0 else 0)
    return max(-cap, state - 1), (-1 if state > 0 else 0)


def tracker_value(word: str, cap: int) -> int:
    state = 0
    value = 0
    for letter in word:
        state, increment = tracker_step(state, letter, cap)
        value += increment
    return value


def words_through(n: int):
    for length in range(n + 1):
        yield from map("".join, itertools.product("ab", repeat=length))


def audit_min_count() -> dict:
    words_checked = 0
    pair_witnesses = 0
    horizons = []
    for n in range(2, 15):
        cap = n // 2
        for word in words_through(n):
            assert tracker_value(word, cap) == min_count(word)
            words_checked += 1

        prefixes = {
            d: ("a" * d if d >= 0 else "b" * (-d))
            for d in range(-cap, cap + 1)
        }
        suffixes = ("a" * cap, "b" * cap)
        for d, e in itertools.combinations(prefixes, 2):
            assert any(
                min_count(prefixes[d] + suffix) != min_count(prefixes[e] + suffix)
                for suffix in suffixes
            )
            pair_witnesses += 1

        # BFS access words a^s and b^{-s} have accumulated weight zero.
        access_weights = {}
        for state in range(-cap, cap + 1):
            access = "a" * state if state >= 0 else "b" * (-state)
            access_weights[state] = tracker_value(access, cap)
        assert set(access_weights.values()) == {0}
        transition_weights = {
            tracker_step(state, letter, cap)[1]
            for state in range(-cap, cap + 1)
            for letter in "ab"
        }
        assert transition_weights <= {-1, 0, 1}
        assert -1 in transition_weights
        horizons.append({"N": n, "states": 2 * cap + 1, "raw_height": 1, "canonical_height": 1})

    # At N=1 the function is identically zero, so the N>=2 boundary is sharp.
    assert {min_count(word) for word in words_through(1)} == {0}
    return {
        "horizons": horizons,
        "words_checked": words_checked,
        "distinguishable_prefix_pairs": pair_witnesses,
        "hostile_boundary": "At N=1 one state of height zero suffices; the height-one formula begins at N=2.",
    }


def audit_unambiguous_controls() -> dict:
    # Classical unary unambiguous/nonsequential control: S(a^n)=n for even n,
    # and zero for odd n.  Adjacent values expose a linear Lipschitz modulus.
    gaps = []
    for horizon in range(2, 65):
        values = [n if n % 2 == 0 else 0 for n in range(horizon + 1)]
        gap = max(abs(values[n + 1] - values[n]) for n in range(horizon))
        assert horizon - 1 <= gap <= horizon
        gaps.append(gap)

    # The ambiguity-two boundary is a global length shift of max-count.
    shift_checks = 0
    for word in words_through(14):
        max_count = max(word.count("a"), word.count("b"))
        assert min_count(word) == max_count - len(word)
        shift_checks += 1
    return {
        "unary_adjacent_gaps": gaps,
        "length_shift_identities": shift_checks,
        "classical_boundary": "Klimann--Lombardy--Mairesse--Prieur Section 3.2 proves max-count is not unambiguous; the exact finite-horizon demands are separate FPRD deductions.",
    }


def main() -> None:
    receipt = {
        "schema": "fprd.result-review.weighted-height-boundaries.v1",
        "review_units": ["FPRD-T72", "FPRD-T73/T74"],
        "parity_comb": audit_parity_comb(),
        "min_count": audit_min_count(),
        "unambiguous_controls": audit_unambiguous_controls(),
        "status": "passed",
    }
    print(json.dumps(receipt, indent=2, sort_keys=True))


if __name__ == "__main__":
    main()