transformation_linear_loop_review.py

#!/usr/bin/env python3
"""Independent finite checks for the transformation-degree and linear-loop review.

The checks are deliberately independent of the site implementation.  They do
not prove the unbounded theorems; they test the decisive finite mechanisms and
hostile boundary cases used in the published arguments.
"""

from __future__ import annotations

import itertools
import json
from collections import deque
from fractions import Fraction


def compose(f: tuple[int, ...], g: tuple[int, ...]) -> tuple[int, ...]:
    """Return g after f.  The convention is immaterial to kernel equality."""
    return tuple(g[f[i]] for i in range(len(f)))


def transformations(n: int):
    return list(itertools.product(range(n), repeat=n))


def permutations(n: int):
    return list(itertools.permutations(range(n)))


def paired_graph(source, target):
    n, m = len(source[0]), len(target[0])
    start = (tuple(range(n)), tuple(range(m)))
    queue = deque([start])
    distance = {start: 0}
    while queue:
        state = queue.popleft()
        for i in range(2):
            nxt = (compose(state[0], source[i]), compose(state[1], target[i]))
            if nxt not in distance:
                distance[nxt] = distance[state] + 1
                queue.append(nxt)
    return distance


def same_marked_kernel(source, target):
    distance = paired_graph(source, target)
    forward, backward = {}, {}
    for s, t in distance:
        if s in forward and forward[s] != t:
            return False, distance
        if t in backward and backward[t] != s:
            return False, distance
        forward[s] = t
        backward[t] = s
    return True, distance


def transformation_audit():
    checks = equal_kernels = witness_bound_checks = 0
    maximum_reachable = maximum_shortest = 0
    for n in (2, 3):
        source_maps = transformations(n)
        target_pairs = []
        for m in range(1, n):
            maps = transformations(m)
            target_pairs.extend((m, pair) for pair in itertools.product(maps, repeat=2))
        for source in itertools.product(source_maps, repeat=2):
            for m, target in target_pairs:
                equal, distances = same_marked_kernel(source, target)
                checks += 1
                equal_kernels += int(equal)
                maximum_reachable = max(maximum_reachable, len(distances))
                maximum_shortest = max(maximum_shortest, max(distances.values()))
                assert max(distances.values()) < (n**n) * (m**m)
                witness_bound_checks += 1

    group_source_pairs = group_target_checks = 0
    transformation_permutation_agreements = 0
    for n in (2, 3):
        for source in itertools.product(permutations(n), repeat=2):
            group_source_pairs += 1
            for m in range(1, n):
                all_maps = transformations(m)
                all_pairs = list(itertools.product(all_maps, repeat=2))
                perm_pairs = list(itertools.product(permutations(m), repeat=2))
                in_transformations = any(same_marked_kernel(source, t)[0] for t in all_pairs)
                in_permutations = any(same_marked_kernel(source, t)[0] for t in perm_pairs)
                assert in_transformations == in_permutations
                group_target_checks += 1
                transformation_permutation_agreements += 1

    # Hostile non-unital example: a group identity may map to an idempotent
    # projection, but restriction to its image is still a permutation action.
    e = (0, 1, 1)
    g = (1, 0, 0)
    assert compose(e, e) == e
    assert compose(g, g) == e
    assert compose(e, g) == g == compose(g, e)
    restricted = tuple(g[i] for i in (0, 1))
    assert restricted == (1, 0)

    return {
        "paired_kernel_checks": checks,
        "equal_kernel_cases": equal_kernels,
        "shortest_representative_bound_checks": witness_bound_checks,
        "maximum_reachable_paired_values": maximum_reachable,
        "maximum_shortest_representative_length": maximum_shortest,
        "group_source_pairs": group_source_pairs,
        "group_target_degree_checks": group_target_checks,
        "transformation_permutation_agreements": transformation_permutation_agreements,
        "hostile_nonunital_restriction_checks": 1,
    }


def trim(poly):
    poly = list(poly)
    while len(poly) > 1 and poly[-1] == 0:
        poly.pop()
    return tuple(poly)


def add(p, q):
    out = [0] * max(len(p), len(q))
    for i, value in enumerate(p):
        out[i] += value
    for i, value in enumerate(q):
        out[i] += value
    return trim(out)


def mul(p, q):
    out = [0] * (len(p) + len(q) - 1)
    for i, a in enumerate(p):
        for j, b in enumerate(q):
            out[i + j] += a * b
    return trim(out)


def scale(c, p):
    return trim([c * value for value in p])


def compose_poly(f, g):
    out = (0,)
    power = (1,)
    for coefficient in f:
        out = add(out, scale(coefficient, power))
        power = mul(power, g)
    return trim(out)


def rank(matrix):
    a = [[Fraction(x) for x in row] for row in matrix]
    rows, cols, pivot_row = len(a), len(a[0]), 0
    for col in range(cols):
        pivot = next((r for r in range(pivot_row, rows) if a[r][col]), None)
        if pivot is None:
            continue
        a[pivot_row], a[pivot] = a[pivot], a[pivot_row]
        value = a[pivot_row][col]
        a[pivot_row] = [x / value for x in a[pivot_row]]
        for r in range(rows):
            if r != pivot_row and a[r][col]:
                factor = a[r][col]
                a[r] = [x - factor * y for x, y in zip(a[r], a[pivot_row])]
        pivot_row += 1
        if pivot_row == rows:
            break
    return pivot_row


def linear_loop_audit():
    identity_checks = identities = infinite_identity_checks = 0
    graph_rank_checks = graph_value_checks = 0
    for degree in (2, 3, 4):
        for prefix in itertools.product((-1, 0, 1), repeat=degree):
            for lead in (-1, 1):
                f = tuple(prefix) + (lead,)
                support = {i for i, c in enumerate(f) if c}
                exponents = sorted({1} | support)
                r_f = len(exponents)

                samples = [[base**n for base in (2,)] for n in range(1)]
                del samples  # keep the rank calculation below explicit
                sequences = [[2 ** (k * n) for n in range(r_f)] for k in exponents]
                assert rank(sequences) == r_f
                graph_rank_checks += 1
                for n in range(8):
                    x = 2**n
                    y = sum(c * x**k for k, c in enumerate(f))
                    assert y == sum(c * 2 ** (k * n) for k, c in enumerate(f))
                    graph_value_checks += 1

                for a, b, c in itertools.product(range(-2, 3), repeat=3):
                    for d in range(-16, 17):
                        lhs = compose_poly(f, add((0, a), scale(b, f)))
                        rhs = add((0, c), scale(d, f))
                        identity_checks += 1
                        if lhs != rhs:
                            continue
                        identities += 1
                        if b == 0 and a not in (0, 1, -1):
                            infinite_identity_checks += 1
                            nonlinear = [k for k in support if k >= 2]
                            assert f[0] == 0
                            assert len(nonlinear) == 1

    # The strict example, including the state order (x,z,y), initial state,
    # update, invariant, and hostile n=0 boundary.
    strict_checks = 0
    state = (1, -1, 2)
    for n in range(21):
        x, z, y = state
        assert x == 2**n
        assert z == -(4**n)
        assert y == 8**n + 4**n
        assert y == x**3 + x**2
        state = (2 * x, 4 * z, 8 * y + 4 * z)
        strict_checks += 1

    return {
        "polynomial_identity_checks": identity_checks,
        "polynomial_identities_found": identities,
        "infinite_orbit_identity_classification_checks": infinite_identity_checks,
        "vandermonde_rank_checks": graph_rank_checks,
        "graph_orbit_value_checks": graph_value_checks,
        "strict_three_state_recurrence_checks": strict_checks,
    }


def main():
    result = {
        "protocol": "fprd-result-review-independent-audit.v1",
        "scope": [
            "minimum faithful transformation degree",
            "linear-loop polynomial invariants",
        ],
        "transformation_degree": transformation_audit(),
        "linear_loops": linear_loop_audit(),
        "result": "pass",
        "limitations": [
            "Finite enumeration corroborates but does not prove the unbounded theorems.",
            "No external or specialist review is represented by this audit.",
        ],
    }
    print(json.dumps(result, indent=2, sort_keys=True))


if __name__ == "__main__":
    main()