check_causal_future_gcd.py

#!/usr/bin/env python3
# promoted from workspaces/boxlab-workspace/fprd-lab-workspace/work/checks/check_causal_future_gcd.py on 2026-07-29 - status: unverified
# Exact direct future-row quotient and causal semantic-factor checker through the cyclic pentagon; verification instrument, not independently reviewed as software.
"""Exhaustive checker for the cyclic two-hinge semantic-GCD obstruction.

The cyclic carrier on ``X = Z/nZ`` has two named reflections

    h0(i) = -i,             h1(i) = 2-i  (mod n).

An update ``x = (p, A)`` acts on an opened-site mask by
``T_x(S) = A | p(S)``.  Temporal composition is prefix first:
``x ; y = yx``.  A prefix mask ``A`` is observed through every continuation
``(q, B)`` by asking whether ``B | q(A)`` contains an entire group orbit.

Unlike the first received version of this checker, the census below constructs
the complete future-row quotient directly for every n.  This matters for even
n, where the two reflections are not transitive and masks containing a complete
orbit collapse to the constant-one row.  The transitive n=5 carrier still has
one row per mask, and its first failing target pair is the edge/diagonal
pentagon certificate.

This is a checker for a semantic factor preorder.  It does not assert that the
factors are epis in the typed sense of Bianchini--Puppis.
"""

from __future__ import annotations

import argparse
import itertools
import json
from pathlib import Path
from typing import Iterable


Permutation = tuple[int, ...]


def compose_perm(p: Permutation, q: Permutation) -> Permutation:
    """Return p after q."""

    return tuple(p[q[i]] for i in range(len(p)))


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


def generators(n: int) -> tuple[Permutation, Permutation]:
    return (
        tuple((-i) % n for i in range(n)),
        tuple((2 - i) % n for i in range(n)),
    )


def generated_group(n: int) -> tuple[Permutation, ...]:
    ident = tuple(range(n))
    group = {ident}
    todo = [ident]
    while todo:
        p = todo.pop()
        for generator in generators(n):
            candidate = compose_perm(p, generator)
            if candidate not in group:
                group.add(candidate)
                todo.append(candidate)
    return tuple(sorted(group))


def orbit_masks(n: int, group: tuple[Permutation, ...]) -> tuple[int, ...]:
    unseen = set(range(n))
    fibers: list[int] = []
    while unseen:
        seed = min(unseen)
        points = {p[seed] for p in group}
        mask = sum(1 << point for point in points)
        fibers.append(mask)
        unseen.difference_update(points)
    return tuple(fibers)


def look(mask: int, fibers: tuple[int, ...]) -> bool:
    return any(mask & fiber == fiber for fiber in fibers)


def current_look_counterexample(
    n: int, fibers: tuple[int, ...]
) -> dict[str, int] | None:
    masks = range(1 << n)
    for a, b in itertools.combinations(masks, 2):
        if look(a, fibers) != look(b, fibers):
            continue
        for append in masks:
            if look(a | append, fibers) != look(b | append, fibers):
                return {"left": a, "right": b, "common_append": append}
    return None


def fixed_future_signature(
    prefix: int, n: int, fibers: tuple[int, ...]
) -> tuple[bool, ...]:
    return tuple(look(prefix | suffix, fibers) for suffix in range(1 << n))


def causal_future_signature(
    prefix: int,
    n: int,
    group: tuple[Permutation, ...],
    fibers: tuple[int, ...],
) -> tuple[bool, ...]:
    return tuple(
        look(append | image_mask(frame, prefix), fibers)
        for frame in group
        for append in range(1 << n)
    )


def quotient_classes(
    n: int,
    group: tuple[Permutation, ...],
    fibers: tuple[int, ...],
) -> tuple[tuple[tuple[int, ...], ...], dict[int, int]]:
    fixed_buckets: dict[tuple[bool, ...], list[int]] = {}
    causal_buckets: dict[tuple[bool, ...], list[int]] = {}
    for mask in range(1 << n):
        fixed_buckets.setdefault(
            fixed_future_signature(mask, n, fibers), []
        ).append(mask)
        causal_buckets.setdefault(
            causal_future_signature(mask, n, group, fibers), []
        ).append(mask)

    fixed_partition = {
        frozenset(bucket) for bucket in fixed_buckets.values()
    }
    causal_partition = {
        frozenset(bucket) for bucket in causal_buckets.values()
    }
    assert fixed_partition == causal_partition

    classes = tuple(
        sorted(
            (tuple(sorted(bucket)) for bucket in fixed_partition),
            key=lambda bucket: bucket[0],
        )
    )
    class_of = {
        mask: class_id
        for class_id, bucket in enumerate(classes)
        for mask in bucket
    }

    # Equality of fixed-frame rows must survive append and group action.
    for bucket in classes:
        representative = bucket[0]
        for other in bucket[1:]:
            for append in range(1 << n):
                assert class_of[representative | append] == class_of[other | append]
            for frame in group:
                assert class_of[image_mask(frame, representative)] == class_of[
                    image_mask(frame, other)
                ]

    expected = 1
    for fiber in fibers:
        expected *= (1 << fiber.bit_count()) - 1
    expected += 1
    assert len(classes) == expected
    return classes, class_of


def fixed_frame_gcd_check(
    n: int,
    group: tuple[Permutation, ...],
    classes: tuple[tuple[int, ...], ...],
    class_of: dict[int, int],
) -> dict[str, int | bool]:
    representatives = [bucket[0] for bucket in classes]

    def below(left: int, right: int) -> bool:
        return class_of[
            representatives[left] | representatives[right]
        ] == right

    pairs_checked = 0
    for left in range(len(classes)):
        for right in range(len(classes)):
            pairs_checked += 1
            lower_bounds = [
                candidate
                for candidate in range(len(classes))
                if below(candidate, left) and below(candidate, right)
            ]
            greatest = [
                candidate
                for candidate in lower_bounds
                if all(below(other, candidate) for other in lower_bounds)
            ]
            assert greatest

    # The raw Boolean-mask theorem has ordinary intersection as its GCD.
    for left in range(1 << n):
        for right in range(1 << n):
            meet = left & right
            assert meet & ~left == 0
            assert meet & ~right == 0
            for candidate in range(1 << n):
                if candidate & ~left == 0 and candidate & ~right == 0:
                    assert candidate & ~meet == 0

    return {
        "verified": True,
        "quotient_mask_class_pairs_checked": pairs_checked,
        "semidirect_update_class_pairs_represented": (
            len(group) * len(classes)
        )
        ** 2,
    }


def causal_divisor_relation(
    n: int,
    group: tuple[Permutation, ...],
    classes: tuple[tuple[int, ...], ...],
    class_of: dict[int, int],
) -> tuple[tuple[frozenset[int], ...], tuple[frozenset[int], ...]]:
    """Return residual reachability and unit association for row classes."""

    reachable: list[frozenset[int]] = []
    unit_orbits: list[frozenset[int]] = []
    for bucket in classes:
        representative = bucket[0]
        target_classes = {
            class_of[append | image_mask(frame, representative)]
            for frame in group
            for append in range(1 << n)
        }
        unit_classes = {
            class_of[image_mask(frame, representative)] for frame in group
        }

        # Right congruence: the choice of representative changes neither set.
        for other in bucket[1:]:
            assert target_classes == {
                class_of[append | image_mask(frame, other)]
                for frame in group
                for append in range(1 << n)
            }
            assert unit_classes == {
                class_of[image_mask(frame, other)] for frame in group
            }

        reachable.append(frozenset(target_classes))
        unit_orbits.append(frozenset(unit_classes))
    return tuple(reachable), tuple(unit_orbits)


def maximal_elements(
    members: Iterable[int], reachable: tuple[frozenset[int], ...]
) -> list[int]:
    items = list(members)
    return [
        candidate
        for candidate in items
        if not any(
            other != candidate
            and other in reachable[candidate]
            and candidate not in reachable[other]
            for other in items
        )
    ]


def search_n(n: int) -> dict[str, object]:
    group = generated_group(n)
    fibers = orbit_masks(n, group)
    classes, class_of = quotient_classes(n, group, fibers)
    reachable, unit_orbits = causal_divisor_relation(
        n, group, classes, class_of
    )
    representatives = [bucket[0] for bucket in classes]

    witness = None
    pairs_checked = 0
    for left in range(len(classes)):
        for right in range(left, len(classes)):
            pairs_checked += 1
            common = [
                divisor
                for divisor in range(len(classes))
                if left in reachable[divisor] and right in reachable[divisor]
            ]
            greatest = [
                divisor
                for divisor in common
                if all(divisor in reachable[other] for other in common)
            ]
            if greatest:
                continue

            maximal = maximal_elements(common, reachable)
            nonassociated = next(
                (
                    (first, second)
                    for first, second in itertools.combinations(maximal, 2)
                    if second not in unit_orbits[first]
                ),
                None,
            )
            assert nonassociated is not None
            witness = {
                "target_masks": [
                    representatives[left],
                    representatives[right],
                ],
                "nonassociated_maximal_factor_masks": [
                    representatives[nonassociated[0]],
                    representatives[nonassociated[1]],
                ],
                "all_maximal_factor_masks": [
                    representatives[class_id] for class_id in maximal
                ],
            }
            break
        if witness:
            break

    current_counterexample = current_look_counterexample(n, fibers)
    return {
        "n": n,
        "group_order": len(group),
        "fiber_masks": list(fibers),
        "future_row_classes": len(classes),
        "current_look_is_right_congruence": current_counterexample is None,
        "current_look_counterexample": current_counterexample,
        "fixed_frame_gcd": fixed_frame_gcd_check(
            n, group, classes, class_of
        ),
        "causal_target_class_pairs_checked_until_first_failure_or_exhaustion": (
            pairs_checked
        ),
        "witness": witness,
    }


def verify_pentagon() -> dict[str, object]:
    n = 5
    group = generated_group(n)
    fibers = orbit_masks(n, group)
    assert fibers == (0b11111,)
    classes, class_of = quotient_classes(n, group, fibers)
    assert len(classes) == 32
    assert all(len(bucket) == 1 for bucket in classes)
    reachable, unit_orbits = causal_divisor_relation(
        n, group, classes, class_of
    )

    c1 = 0b00111  # {0,1,2}; complement {3,4}, an edge
    c2 = 0b01011  # {0,1,3}; complement {2,4}, a diagonal
    edge = 0b00011  # {0,1}
    diagonal = 0b00101  # {0,2}

    common = [
        divisor
        for divisor in range(len(classes))
        if class_of[c1] in reachable[divisor]
        and class_of[c2] in reachable[divisor]
    ]
    maximal = maximal_elements(common, reachable)
    maximal_masks = [classes[class_id][0] for class_id in maximal]
    assert edge in maximal_masks and diagonal in maximal_masks
    assert all(mask.bit_count() == 2 for mask in maximal_masks)
    assert class_of[diagonal] not in unit_orbits[class_of[edge]]
    assert class_of[c2] not in unit_orbits[class_of[c1]]
    assert not any(
        all(greatest in reachable[other] for other in common)
        for greatest in common
    )

    # Explicit residuals from the proof.
    ident = tuple(range(n))
    h0 = generators(n)[0]
    assert edge | 0b00100 == c1
    assert edge | 0b01000 == c2
    assert diagonal | 0b00010 == c1
    assert image_mask(h0, diagonal) | 0b00010 == c2
    assert image_mask(ident, edge) == edge

    return {
        "targets": [c1, c2],
        "target_complements": {
            "first": "edge",
            "second": "diagonal",
        },
        "maximal_common_factor_representatives": [edge, diagonal],
        "factor_orbits": ["edge", "diagonal"],
        "verified": True,
    }


def build_certificate(max_n: int) -> dict[str, object]:
    rows = [search_n(n) for n in range(1, max_n + 1)]
    first_failure = next(
        (row["n"] for row in rows if row["witness"] is not None),
        None,
    )
    first_current_look_failure = next(
        (
            row["n"]
            for row in rows
            if not row["current_look_is_right_congruence"]
        ),
        None,
    )
    if max_n >= 5:
        assert first_failure == 5
    if max_n >= 3:
        assert first_current_look_failure == 3
    return {
        "model": "causal full-future cyclic two-hinge Boolean carrier",
        "status": "exhaustive finite certificate",
        "semantic_warning": (
            "GCD refers to the causal future-row factor preorder; no typed "
            "epi class is asserted"
        ),
        "explicit_pentagon_certificate": verify_pentagon(),
        "census": rows,
        "first_current_look_congruence_failure_n": (
            first_current_look_failure
        ),
        "first_semantic_gcd_failure_n": first_failure,
    }


def main() -> None:
    parser = argparse.ArgumentParser()
    parser.add_argument("--max-n", type=int, default=5)
    parser.add_argument("--certificate", type=Path)
    args = parser.parse_args()
    if args.max_n < 1:
        parser.error("--max-n must be positive")

    certificate = build_certificate(args.max_n)
    text = json.dumps(certificate, indent=2) + "\n"
    if args.certificate:
        args.certificate.write_text(text, encoding="utf-8")
    print(text, end="")


if __name__ == "__main__":
    main()