l_trivial_quotient_family_review.py

#!/usr/bin/env python3
"""Independent checks for the target-isolating theorem and binary family.

This reviewer does not import the preserved research programs.  It rebuilds
the finite monoids and automata from the displayed definitions using tuples,
sets, and breadth-first search.
"""

from __future__ import annotations

import json
from collections import deque
from itertools import product


def compose(first: tuple[int, ...], second: tuple[int, ...]) -> tuple[int, ...]:
    """Right action: apply ``first`` and then ``second``."""
    return tuple(second[q] for q in first)


def generated_monoid(generators: dict[str, tuple[int, ...]]):
    degree = len(next(iter(generators.values())))
    identity = tuple(range(degree))
    words = {identity: ""}
    queue = deque([identity])
    while queue:
        current = queue.popleft()
        for letter, generator in generators.items():
            nxt = compose(current, generator)
            if nxt not in words:
                words[nxt] = words[current] + letter
                queue.append(nxt)
    return words


def apply_word(generators: dict[str, tuple[int, ...]], word: str):
    result = tuple(range(len(next(iter(generators.values())))))
    for letter in word:
        result = compose(result, generators[letter])
    return result


def target_isolating_example():
    # Multiplication is determined by a^2=0, with 1 an identity and 0 a zero.
    elements = ("1", "a", "0")
    table = {
        (x, y): (
            y if x == "1" else x if y == "1" else "0"
        )
        for x, y in product(elements, repeat=2)
    }
    identity = (0, 1)
    top = (1, 1)
    rho = {"1": identity, "a": top, "0": top}

    def tcompose(x, y):
        return tuple(y[q] for q in x)

    assert all(rho[table[x, y]] == tcompose(rho[x], rho[y])
               for x, y in product(elements, repeat=2))
    fibre = tuple(x for x in elements if rho[x] == identity)
    assert fibre == ("1",)
    assert rho["a"] == rho["0"]
    assert all(image[q] >= q for image in rho.values() for q in range(2))

    left_ideals = {
        x: frozenset(table[m, x] for m in elements) for x in elements
    }
    assert len(set(left_ideals.values())) == len(elements)
    return {
        "monoid_elements": len(elements),
        "multiplication_checks": len(elements) ** 2,
        "target_fibre": list(fibre),
        "collapsed_pair": ["a", "0"],
        "podfa_degree": 2,
    }


def family(n: int):
    a = list(range(n))
    a[0] = 2
    a[n - 1] = 1
    b = list(range(n))
    for q in range(2, n - 1):
        b[q] = q + 1
    return {"a": tuple(a), "b": tuple(b)}


def reachable_and_minimal(generators):
    n = len(generators["a"])
    final = {1}
    state_words = {0: ""}
    queue = deque([0])
    while queue:
        q = queue.popleft()
        for letter, generator in generators.items():
            nxt = generator[q]
            if nxt not in state_words:
                state_words[nxt] = state_words[q] + letter
                queue.append(nxt)
    assert len(state_words) == n

    monoid = generated_monoid(generators)
    for p in range(n):
        for q in range(p + 1, n):
            assert any((x[p] in final) != (x[q] in final) for x in monoid)
    return state_words, monoid


def order_and_confluence(generators):
    n = len(generators["a"])
    order = [0] + list(range(2, n)) + [1]
    rank = {q: i for i, q in enumerate(order)}
    assert all(rank[q] <= rank[g[q]] for g in generators.values() for q in range(n))

    # Directly search a common continuation for the two one-letter successors.
    monoid = generated_monoid(generators)
    for q in range(n):
        left = generators["a"][q]
        right = generators["b"][q]
        assert any(x[left] == x[right] for x in monoid)


def green_triviality(monoid_words):
    elements = tuple(monoid_words)
    left_ideals = {
        x: frozenset(compose(m, x) for m in elements) for x in elements
    }
    right_ideals = {
        x: frozenset(compose(x, m) for m in elements) for x in elements
    }
    assert len(set(left_ideals.values())) == len(elements)
    assert len(set(right_ideals.values())) == len(elements)


def binary_family_review():
    rows = []
    for n in range(4, 19):
        generators = family(n)
        state_words, monoid = reachable_and_minimal(generators)
        order_and_confluence(generators)
        target = (n - 1,) + (1,) * (n - 1)
        witness = "ba" + "b" * (n - 4) + "ab"
        assert apply_word(generators, witness) == target
        distance = len(monoid[target])
        expected = 3 if n == 4 else n
        assert distance == expected
        if n <= 12:
            green_triviality(monoid)
        rows.append({
            "states": n,
            "monoid_size": len(monoid),
            "shortest_target_length": distance,
            "displayed_witness_length": len(witness),
            "green_triviality_checked": n <= 12,
            "reachable_states": len(state_words),
        })
    return {
        "parameter_range": [4, 18],
        "theorem_range": [5, 18],
        "hostile_boundary": {
            "states": 4,
            "shortest_target_word": generated_monoid(family(4))[
                (3, 1, 1, 1)
            ],
            "shortest_target_length": 3,
            "reason_for_n_at_least_5": "the one-a lower bound 2n-5 is below n at n=4",
        },
        "rows": rows,
    }


def main():
    report = {
        "artifact_schema": "fprd.independent-mathematical-audit.v1",
        "review_date": "2026-09-01",
        "target_isolating_example": target_isolating_example(),
        "binary_family": binary_family_review(),
        "status": "PASS",
    }
    print(json.dumps(report, indent=2, sort_keys=True))


if __name__ == "__main__":
    main()