audit_fixed_correction_gradient.py

#!/usr/bin/env python3
"""Independent finite audit for FPRD-T78 and FPRD-T79/T80.

The checker deliberately separates exhaustive finite evidence from the
universal arguments in the accompanying README.
"""

from fractions import Fraction
from itertools import product
import json
import random

NEG = None


def enc(n: int) -> str:
    return f"{n:b};"


def prefix(i: int, m: int) -> str:
    return "b" * i + "c" + "a" * m


def suffix(r: int, s: int) -> str:
    return "#" + enc(r) + enc(s)


def target(i: int, m: int, r: int, s: int) -> int:
    return m // (i + 1) + int((i, m) == (r, s))


class Baseline:
    alphabet = "bca#01;"

    def __init__(self, states: int, rng: random.Random):
        self.states = states
        self.transition = {
            (q, a): (rng.randrange(states), rng.randint(-10_000, 10_000))
            for q in range(states)
            for a in self.alphabet
        }
        self.final = [rng.randint(-10_000, 10_000) for _ in range(states)]

    def run(self, word: str, state: int = 0, value: int = 0):
        for letter in word:
            state, weight = self.transition[state, letter]
            value += weight
        return state, value

    def value(self, word: str) -> int:
        state, value = self.run(word)
        return value + self.final[state]


def affine_rank_two(points):
    p0 = points[0]
    vectors = [(x - p0[0], y - p0[1]) for x, y in points[1:]]
    for index, u in enumerate(vectors):
        if u == (0, 0):
            continue
        for v in vectors[index + 1 :]:
            if u[0] * v[1] - u[1] * v[0] != 0:
                return True
    return False


def maxplus_step(vector, matrix):
    result = []
    for j in range(len(vector)):
        candidates = [
            vector[i] + matrix[i][j]
            for i in range(len(vector))
            if vector[i] is not NEG and matrix[i][j] is not NEG
        ]
        result.append(max(candidates) if candidates else NEG)
    return result


def run_audit():
    result = {
        "batch": "result-review-2026-09-01-batch-25",
        "status": "passed",
        "fixed_state_correction": {},
        "gradient_ambiguity": {},
    }

    # T78: the 0/1 horizon construction.
    raw_checks = 0
    for i in range(1, 65):
        accumulated = 0
        for m in range(0, 513):
            if m > 0 and m % (i + 1) == 0:
                accumulated += 1
            assert accumulated == m // (i + 1)
            raw_checks += 1

    # T78: a collision among k+1 addresses makes the baseline contribution
    # difference independent of the shared continuation.
    rng = random.Random(78079)
    collision_checks = 0
    large_value_checks = 0
    hostile_equal_slope_checks = 0
    baseline_instances = 0
    for k in range(1, 7):
        for _ in range(80):
            baseline_instances += 1
            baseline = Baseline(k, rng)
            seen = {}
            pair = None
            access = {}
            for i in range(1, k + 2):
                q, alpha = baseline.run("b" * i + "c")
                access[i] = (q, alpha)
                if q in seen and pair is None:
                    pair = (seen[q], i)
                seen.setdefault(q, i)
            assert pair is not None
            i, j = pair
            q_i, alpha_i = access[i]
            q_j, alpha_j = access[j]
            assert q_i == q_j
            z0 = suffix(k + 2, 0)
            M = 96
            big = 0
            slope_gap = Fraction(1, i + 1) - Fraction(1, j + 1)
            for m in range(0, 2 * M + 1):
                wi = prefix(i, m) + z0
                wj = prefix(j, m) + z0
                baseline_difference = baseline.value(wi) - baseline.value(wj)
                assert baseline_difference == alpha_i - alpha_j
                collision_checks += 1
                if m >= M:
                    gi = target(i, m, k + 2, 0) - baseline.value(wi)
                    gj = target(j, m, k + 2, 0) - baseline.value(wj)
                    if max(abs(gi), abs(gj)) >= float(slope_gap * M / 16):
                        big += 1
                        large_value_checks += 1
            assert big >= (M + 1) // 2

            # Hostile control: if the two slopes are made equal, the affine
            # separation mechanism disappears exactly.
            for m in range(0, 33):
                equal_difference = m // (i + 1) - m // (i + 1)
                assert equal_difference == 0
                hostile_equal_slope_checks += 1

    # T78: exhaustive abstract challenge-row lemma for two baseline states.
    # delta(t) represents beta_0(t)-beta_1(t).  For each state assignment,
    # at most one ordered prefix pair may be merge-compatible per ordered
    # pair of distinct baseline states.
    points = tuple(range(6))
    challenge_configurations = 0
    eligible_pairs = 0
    for assignment in product((0, 1), repeat=len(points)):
        for delta in product((-1, 0, 1), repeat=len(points)):
            challenge_configurations += 1
            incident = set()
            per_ordered_state_pair = {(0, 1): 0, (1, 0): 0}
            for x in points:
                for y in points:
                    if x == y or assignment[x] == assignment[y]:
                        continue
                    sign = 1 if (assignment[x], assignment[y]) == (0, 1) else -1
                    row = [
                        int(t == x) - int(t == y) - sign * delta[t]
                        for t in points
                    ]
                    if len(set(row)) == 1:
                        key = (assignment[x], assignment[y])
                        per_ordered_state_pair[key] += 1
                        incident.update((x, y))
                        eligible_pairs += 1
            assert max(per_ordered_state_pair.values()) <= 1
            assert len(incident) <= 4

    same_state_controls = 0
    for x in points:
        for y in points:
            if x == y:
                continue
            row = [int(t == x) - int(t == y) for t in points]
            assert len(set(row)) > 1
            same_state_controls += 1

    # T78: the repaired nonrationality boundary.  Every simple cycle in an
    # n-state unary automaton has length at most n; its integer-weight mean
    # has reduced denominator at most n and cannot equal 1/(n+1).
    cycle_mean_checks = 0
    forbidden_slope_checks = 0
    for n in range(1, 21):
        means = set()
        for length in range(1, n + 1):
            for total_weight in range(-2 * n, 2 * n + 1):
                mean = Fraction(total_weight, length)
                assert mean.denominator <= length <= n
                means.add(mean)
                cycle_mean_checks += 1
        assert Fraction(1, n + 1) not in means
        forbidden_slope_checks += 1

    result["fixed_state_correction"] = {
        "raw_accumulation_checks": raw_checks,
        "baseline_instances": baseline_instances,
        "shared_continuation_checks": collision_checks,
        "large_residual_witnesses": large_value_checks,
        "equal_slope_hostile_controls": hostile_equal_slope_checks,
        "challenge_configurations": challenge_configurations,
        "eligible_challenge_pairs": eligible_pairs,
        "same_state_merge_controls": same_state_controls,
        "cycle_mean_checks": cycle_mean_checks,
        "forbidden_denominator_checks": forbidden_slope_checks,
    }

    # T79: boundary-state factorization on independent random max-plus
    # automata.  This is finite evidence for the algebraic identity only.
    rng = random.Random(7980)
    factorization_checks = 0
    for _ in range(400):
        n = rng.randint(2, 4)
        choices = (NEG, -3, -2, -1, 0, 1)
        initial = [rng.choice(choices) for _ in range(n)]
        final = [rng.choice(choices) for _ in range(n)]
        matrix_a = [[rng.choice(choices) for _ in range(n)] for _ in range(n)]
        matrix_b = [[rng.choice(choices) for _ in range(n)] for _ in range(n)]
        for x in range(7):
            after_a = initial[:]
            for _ in range(x):
                after_a = maxplus_step(after_a, matrix_a)
            for y in range(7):
                direct = after_a[:]
                for _ in range(y):
                    direct = maxplus_step(direct, matrix_b)
                direct_value = max(
                    (
                        direct[q] + final[q]
                        for q in range(n)
                        if direct[q] is not NEG and final[q] is not NEG
                    ),
                    default=NEG,
                )

                factored = NEG
                for q in range(n):
                    if after_a[q] is NEG:
                        continue
                    continuation = [NEG] * n
                    continuation[q] = 0
                    for _ in range(y):
                        continuation = maxplus_step(continuation, matrix_b)
                    right = max(
                        (
                            continuation[r] + final[r]
                            for r in range(n)
                            if continuation[r] is not NEG and final[r] is not NEG
                        ),
                        default=NEG,
                    )
                    if right is not NEG:
                        candidate = after_a[q] + right
                        factored = candidate if factored is NEG else max(factored, candidate)
                assert factored == direct_value
                factorization_checks += 1

    # T79/T80: every residue cell meets each open cone in affine rank two.
    cone_rank_checks = 0
    cones = (
        lambda x, y: y > 2 * x,
        lambda x, y: 2 * y > x and 2 * x > y,
        lambda x, y: x > 2 * y,
    )
    for modulus in range(1, 13):
        for residue_x in range(modulus):
            for residue_y in range(modulus):
                for cone in cones:
                    cone_points = [
                        (residue_x + modulus * i, residue_y + modulus * j)
                        for i in range(1, 31)
                        for j in range(1, 31)
                        if cone(residue_x + modulus * i, residue_y + modulus * j)
                    ]
                    assert len(cone_points) >= 3 and affine_rank_two(cone_points)
                    cone_rank_checks += 1

    # T80: direct three-component realization on every binary word through
    # length 16, and a hostile finite search for a two-affine presentation.
    word_checks = 0
    for length in range(17):
        for letters in product((0, 1), repeat=length):
            x = sum(1 for letter in letters if letter == 0)
            y = length - x
            expected = max(-3 * x, -x - y, -3 * y)
            components = (-3 * x, -x - y, -3 * y)
            assert max(components) == expected
            word_checks += 1

    forms = [
        (a, b, c)
        for a in range(-4, 2)
        for b in range(-4, 2)
        for c in range(-3, 4)
    ]
    two_form_pairs = 0
    finite_two_form_matches = 0
    grid = [(x, y) for x in range(11) for y in range(11)]
    expected_grid = [max(-3 * x, -x - y, -3 * y) for x, y in grid]
    for index, left in enumerate(forms):
        for right in forms[index:]:
            two_form_pairs += 1
            values = [
                max(
                    left[0] * x + left[1] * y + left[2],
                    right[0] * x + right[1] * y + right[2],
                )
                for x, y in grid
            ]
            if values == expected_grid:
                finite_two_form_matches += 1
    assert finite_two_form_matches == 0

    # Hostile period boundary: five states can require eventual modulus six.
    period_support_checks = 0
    support = []
    for m in range(121):
        accepted = m % 2 == 0 or m % 3 == 0
        support.append(accepted)
        period_support_checks += 1
    valid_periods = [
        period
        for period in range(1, 13)
        if all(support[m] == support[m + period] for m in range(121 - period))
    ]
    assert min(valid_periods) == 6

    result["gradient_ambiguity"] = {
        "boundary_factorization_checks": factorization_checks,
        "cone_rank_checks": cone_rank_checks,
        "three_component_word_checks": word_checks,
        "two_affine_pairs_excluded_on_grid": two_form_pairs,
        "finite_two_affine_matches": finite_two_form_matches,
        "period_support_checks": period_support_checks,
        "five_state_least_period": 6,
    }

    return result


if __name__ == "__main__":
    print(json.dumps(run_audit(), indent=2, sort_keys=True))