check_semantic_epi_gcd.py

#!/usr/bin/env python3
"""Check causal full-future semantic prefix-GCDs in a two-hinge carrier.

The row of prefix x is evaluated by applying every continuation y *after*
x, hence as T_y o T_x. Semantic prefix divisibility is existential causal
factorization modulo equality of those rows.
The script exhaustively checks n <= max_n and emits the first pair with
nonassociated maximal common factors.
"""

from __future__ import annotations

import argparse
import itertools
import json
from pathlib import Path


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


def image_mask(p, mask):
    ans = 0
    for i, j in enumerate(p):
        if mask >> i & 1:
            ans |= 1 << j
    return ans


def generators(n):
    return (
        tuple((-i) % n for i in range(n)),
        tuple((2 - i) % n for i in range(n)),
    )


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


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


def look(mask, blocks):
    return any(all(mask >> i & 1 for i in block) for block in blocks)


def mul(x, y):
    p, a = x
    q, b = y
    return compose_perm(p, q), a | image_mask(p, b)


def future_row(x, elements, blocks):
    # mul(y, x) represents T_y o T_x: prefix x, then continuation y.
    return tuple(look(mul(y, x)[1], blocks) for y in elements)


def orbit_of_mask(mask, group):
    return frozenset(image_mask(p, mask) for p in group)


def search_n(n):
    group = generated_group(n)
    blocks = orbit_partition(n, group)
    elements = tuple(
        (p, mask) for p in group for mask in range(1 << n)
    )
    rows = {x: future_row(x, elements, blocks) for x in elements}
    signatures = tuple(dict.fromkeys(rows.values()))
    class_of = {x: signatures.index(rows[x]) for x in elements}
    representatives = 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(representatives):
        for y in elements:
            # d followed causally by residual y is T_y o T_d.
            divides[i][class_of[mul(y, d)]] = True

    association = [
        [divides[i][j] and divides[j][i] for j in range(len(signatures))]
        for i in range(len(signatures))
    ]

    witness = None
    for a in range(len(signatures)):
        for b in range(a, len(signatures)):
            common = [
                d for d in range(len(signatures))
                if divides[d][a] and divides[d][b]
            ]
            maximal = [
                d for d in common
                if not any(
                    divides[d][e] and not divides[e][d] for e in common
                )
            ]
            bad_pair = next(
                (
                    (d, e) for d, e in itertools.combinations(maximal, 2)
                    if not association[d][e]
                ),
                None,
            )
            if bad_pair:
                d, e = bad_pair
                witness = {
                    "target_class_ids": [a, b],
                    "target_archives": [
                        representatives[a][1],
                        representatives[b][1],
                    ],
                    "maximal_factor_class_ids": [d, e],
                    "maximal_factor_archives": [
                        representatives[d][1],
                        representatives[e][1],
                    ],
                    "all_maximal_factor_class_ids": maximal,
                }
                break
        if witness:
            break

    return {
        "n": n,
        "hinges": [list(g) for g in generators(n)],
        "group_order": len(group),
        "fiber_partition": [list(block) for block in blocks],
        "element_count": len(elements),
        "future_row_class_count": len(signatures),
        "nonassociated_maximal_common_factor_witness": witness,
    }


def verify_explicit_pentagon_certificate():
    n = 5
    group = generated_group(n)
    c1 = 0b00111          # {0,1,2}
    c2 = 0b01011          # {0,1,3}
    edge = 0b00011        # {0,1}
    diagonal = 0b00101    # {0,2}

    edge_orbit = orbit_of_mask(edge, group)
    diagonal_orbit = orbit_of_mask(diagonal, group)
    assert edge_orbit.isdisjoint(diagonal_orbit)
    assert orbit_of_mask(c1, group).isdisjoint(orbit_of_mask(c2, group))

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

    assert contains_translate(c1, edge)
    assert contains_translate(c1, diagonal)
    assert contains_translate(c2, edge)
    assert contains_translate(c2, diagonal)

    for three_set in range(1 << n):
        if three_set.bit_count() == 3:
            assert not (
                contains_translate(c1, three_set)
                and contains_translate(c2, three_set)
            )

    return {
        "targets": {
            "three_consecutive_archive": c1,
            "other_three_site_archive": c2,
        },
        "incomparable_maximal_common_subpatterns": [edge, diagonal],
        "dual_invariants": {
            "target_complement_orbits": "edge versus diagonal",
            "factor_orbits": "edge versus diagonal",
        },
        "verified": True,
    }


def main():
    parser = argparse.ArgumentParser()
    parser.add_argument("--max-n", type=int, default=5)
    parser.add_argument("--certificate", type=Path)
    args = parser.parse_args()

    results = [search_n(n) for n in range(1, args.max_n + 1)]
    certificate = {
        "model": "causal full-future semantic cyclic two-hinge Boolean carrier",
        "status": "verified",
        "explicit_pentagon_certificate": verify_explicit_pentagon_certificate(),
        "census": results,
        "first_failure_n": next(
            (
                row["n"] for row in results
                if row["nonassociated_maximal_common_factor_witness"]
            ),
            None,
        ),
    }
    text = json.dumps(certificate, indent=2) + "\n"
    if args.certificate:
        args.certificate.write_text(text)
    print(text, end="")


if __name__ == "__main__":
    main()