#!/usr/bin/env python3
"""Hostile checker for fixed-frame and full-semantic two-hinge GCDs.

This is independent of check_two_hinge_epi_gcd.py.  It checks two issues that
the raw-mask calculation does not:

1. equality of the *current* Look bit is generally not a congruence, so a
   "GCD modulo Look" is not even well-defined;
2. with a fixed root frame, equality of rows A |-> (C |-> Look(A union C))
   is a join congruence and retains a GCD;
3. for causal full update rows, a prefix x followed by continuation y is
   T_y o T_x, hence y*x under the multiplication below.  The resulting
   semantic factor preorder first loses its GCD at n=5.

Carrier and hinges:
  X = Z/nZ
  r0(i) = -i, r1(i) = 2-i (mod n)

Look(A) is OR over hinge-group orbits F of the predicate F subseteq A.
Future rows range over every append mask C:
  row_A(C) = Look(A union C).

Those are *fixed-frame mask rows*.  Full update rows additionally retain the
permutation component through the rooted deficit p^{-1}(X\\A); they are
audited separately by the common-superpattern census below.
"""

from __future__ import annotations

import argparse
import itertools
import json
from pathlib import Path


def compose_perm(p: tuple[int, ...], q: tuple[int, ...]) -> tuple[int, ...]:
    return tuple(p[q[i]] for i in range(len(p)))


def image_mask(p: tuple[int, ...], mask: int) -> int:
    out = 0
    for i, j in enumerate(p):
        if (mask >> i) & 1:
            out |= 1 << j
    return out


def mul(left, right):
    """Product representing T_left o T_right."""
    p, a = left
    q, b = right
    return compose_perm(p, q), a | image_mask(p, b)


def generated_group(n: int) -> tuple[tuple[int, ...], ...]:
    gens = (
        tuple((-i) % n for i in range(n)),
        tuple((2 - i) % n for i in range(n)),
    )
    ident = tuple(range(n))
    group = {ident}
    todo = [ident]
    while todo:
        p = todo.pop()
        for g in gens:
            h = compose_perm(p, g)
            if h not in group:
                group.add(h)
                todo.append(h)
    return tuple(sorted(group))


def orbit_partition(n: int, group: tuple[tuple[int, ...], ...]):
    unseen = set(range(n))
    blocks = []
    while unseen:
        i = min(unseen)
        block = {p[i] for p in group}
        unseen -= block
        blocks.append(tuple(sorted(block)))
    return tuple(blocks)


def look(mask: int, blocks: tuple[tuple[int, ...], ...]) -> int:
    return int(any(all((mask >> i) & 1 for i in block) for block in blocks))


def future_row(mask: int, n: int, blocks) -> tuple[int, ...]:
    return tuple(look(mask | suffix, blocks) for suffix in range(1 << n))


def quotient_classes(n: int, blocks):
    by_row: dict[tuple[int, ...], list[int]] = {}
    for mask in range(1 << n):
        by_row.setdefault(future_row(mask, n, blocks), []).append(mask)
    classes = tuple(tuple(v) for _, v in sorted(by_row.items()))
    class_of = {}
    for i, cls in enumerate(classes):
        for mask in cls:
            class_of[mask] = i
    return classes, class_of


def orbit_of_mask(mask: int, group) -> frozenset[int]:
    return frozenset(image_mask(p, mask) for p in group)


def contains_translate(container: int, pattern: int, group) -> bool:
    return any((translate & ~container) == 0
               for translate in orbit_of_mask(pattern, group))


def semantic_gcd_search(n: int) -> dict:
    """Search the causally oriented full-future row preorder.

    Prefix x then continuation y is T_y o T_x = y*x.  Semantic classes and
    divisibility are computed directly from complete rows, avoiding any
    orientation convention hidden in a closed-form formula.
    """
    group = generated_group(n)
    blocks = orbit_partition(n, group)
    elements = tuple(
        (p, a) for p in group for a in range(1 << n)
    )

    def causal_row(x):
        return tuple(look(mul(y, x)[1], blocks) for y in elements)

    rows = {x: causal_row(x) for x in elements}
    signatures = tuple(dict.fromkeys(rows.values()))
    class_of = {x: signatures.index(rows[x]) for x in elements}
    reps = tuple(
        next(x for x in elements if class_of[x] == i)
        for i in range(len(signatures))
    )
    divides = [[False] * len(signatures) for _ in signatures]
    for i, d in enumerate(reps):
        for y in elements:
            divides[i][class_of[mul(y, d)]] = True

    first = None
    pairs_checked = 0
    for e in range(len(signatures)):
        for f in range(e, len(signatures)):
            pairs_checked += 1
            common = [
                d for d in range(len(signatures))
                if divides[d][e] and divides[d][f]
            ]
            maximal = [
                d for d in common
                if not any(
                    divides[d][c] and not divides[c][d] for c in common
                )
            ]
            bad = next(
                (
                    (d, c) for d, c in itertools.combinations(maximal, 2)
                    if not (divides[d][c] and divides[c][d])
                ),
                None,
            )
            if bad:
                first = {
                    "target_class_ids": [e, f],
                    "target_prefix_masks": [reps[e][1], reps[f][1]],
                    "nonassociated_maximal_factor_class_ids": list(bad),
                    "nonassociated_maximal_factor_prefix_masks":
                        [reps[bad[0]][1], reps[bad[1]][1]],
                    "all_maximal_common_factor_class_ids": maximal,
                }
                break
        if first:
            break

    explicit = None
    if n == 5:
        ident = tuple(range(n))
        c1, c2 = class_of[(ident, 0b00111)], class_of[(ident, 0b01011)]
        edge, diagonal = (
            class_of[(ident, 0b00011)],
            class_of[(ident, 0b00101)],
        )
        assert divides[edge][c1] and divides[edge][c2]
        assert divides[diagonal][c1] and divides[diagonal][c2]
        assert not divides[edge][diagonal]
        assert not divides[diagonal][edge]
        common = [
            d for d in range(len(signatures))
            if divides[d][c1] and divides[d][c2]
        ]
        for d in (edge, diagonal):
            assert not any(
                divides[d][e] and not divides[e][d] for e in common
            )
        explicit = {
            "target_prefix_masks": [0b00111, 0b01011],
            "nonassociated_maximal_common_factors": [0b00011, 0b00101],
            "orbit_invariant":
                "target complements and factor pairs are edge versus diagonal",
            "verified": True,
        }

    return {
        "n": n,
        "update_elements": len(elements),
        "causal_future_row_classes": len(signatures),
        "pattern_pairs_checked": pairs_checked,
        "nonassociated_maximal_common_factor_witness": first,
        "explicit_pentagon_certificate": explicit,
    }


def verify_n(n: int) -> dict:
    group = generated_group(n)
    blocks = orbit_partition(n, group)
    classes, class_of = quotient_classes(n, blocks)
    qsize = len(classes)

    # The future-row quotient must be a join congruence.
    for a, b in itertools.product(range(1 << n), repeat=2):
        if class_of[a] != class_of[b]:
            continue
        for c in range(1 << n):
            assert class_of[a | c] == class_of[b | c]
        for p in group:
            assert class_of[image_mask(p, a)] == class_of[image_mask(p, b)]

    # Quotient join and the induced order.
    def qjoin(x: int, y: int) -> int:
        return class_of[classes[x][0] | classes[y][0]]

    bottom = class_of[0]
    assert all(qjoin(bottom, x) == x for x in range(qsize))
    qle = {
        (x, y): qjoin(x, y) == y
        for x in range(qsize)
        for y in range(qsize)
    }

    def qact(p, x: int) -> int:
        return class_of[image_mask(p, classes[x][0])]

    def mmul(left, right):
        p, x = left
        q, y = right
        return compose_perm(p, q), qjoin(x, qact(p, y))

    monoid = tuple((p, x) for p in group for x in range(qsize))
    # Exhaustive multiplication witnesses for left divisibility.
    divides = {
        (d, v): any(mmul(d, r) == v for r in monoid)
        for d in monoid
        for v in monoid
    }
    assert all(
        divides[(d, v)] == qle[(d[1], v[1])]
        for d in monoid
        for v in monoid
    )

    # Every pair has a greatest common quotient component, computed as the
    # join of all common lower bounds.  All maximal common divisors are
    # associates through permutation units.
    gcd_pairs_checked = 0
    for a, b in itertools.product(monoid, repeat=2):
        lower = [
            x for x in range(qsize)
            if qle[(x, a[1])] and qle[(x, b[1])]
        ]
        meet = bottom
        for x in lower:
            meet = qjoin(meet, x)
        assert qle[(meet, a[1])] and qle[(meet, b[1])]
        assert all(qle[(x, meet)] for x in lower)
        d = (tuple(range(n)), meet)
        assert divides[(d, a)] and divides[(d, b)]
        common = [e for e in monoid if divides[(e, a)] and divides[(e, b)]]
        assert all(divides[(e, d)] for e in common)
        gcd_pairs_checked += 1

    # Find a minimal local witness showing that current-Look equality alone
    # is not stable under a common append.
    local_witness = None
    for a, b, c in itertools.product(range(1 << n), repeat=3):
        if look(a, blocks) != look(b, blocks):
            continue
        if look(a | c, blocks) != look(b | c, blocks):
            local_witness = {
                "a": a,
                "b": b,
                "common_append": c,
                "look_before": look(a, blocks),
                "look_after_a": look(a | c, blocks),
                "look_after_b": look(b | c, blocks),
            }
            break

    predicted = 1
    for block in blocks:
        predicted *= (1 << len(block)) - 1
    predicted += 1
    assert qsize == predicted

    return {
        "n": n,
        "group_order": len(group),
        "orbit_fibers": [list(block) for block in blocks],
        "raw_masks": 1 << n,
        "future_row_classes": qsize,
        "class_count_formula": f"1 + product_F (2^|F|-1) = {predicted}",
        "quotient_class_sizes": sorted(map(len, classes)),
        "future_row_is_join_and_group_congruence": True,
        "observable_semidirect_elements": len(monoid),
        "gcd_pairs_checked": gcd_pairs_checked,
        "all_pairs_have_greatest_common_left_divisor_up_to_units": True,
        "current_look_kernel_congruence_failure": local_witness,
    }


def main() -> None:
    parser = argparse.ArgumentParser()
    parser.add_argument("--max-n", type=int, default=4)
    parser.add_argument("--max-semantic-n", type=int, default=5)
    parser.add_argument("--certificate", type=Path)
    args = parser.parse_args()
    results = [verify_n(n) for n in range(1, args.max_n + 1)]
    semantic = [
        semantic_gcd_search(n) for n in range(1, args.max_semantic_n + 1)
    ]
    cert = {
        "model": "fixed-frame and full-semantic Boolean two-hinge audit",
        "status": "exhaustively verified",
        "fixed_frame_results": results,
        "causal_full_semantic_results": semantic,
        "first_full_semantic_gcd_failure_n": next(
            (
                row["n"] for row in semantic
                if row["nonassociated_maximal_common_factor_witness"]
            ),
            None,
        ),
    }
    text = json.dumps(cert, indent=2) + "\n"
    if args.certificate:
        args.certificate.write_text(text)
    print(text, end="")


if __name__ == "__main__":
    main()