#!/usr/bin/env python3
"""Independent exact checks for recognition cuts and Fold-and-Look bounds.

The recognition audit enumerates every Boolean function on binary words through
total length four.  The Fold-and-Look audit checks the still-valid finite
formula/resource claims and the explicit two-fold counterexample to the former
reflection-line lemma.  Finite checks corroborate, but do not replace, the
unrestricted proofs displayed on the result pages.
"""

from __future__ import annotations

from fractions import Fraction
from itertools import permutations, product
import json
import math


def bit_words(length):
    return tuple(product((0, 1), repeat=length))


def function_value(table, word):
    index = 0
    for bit in word:
        index = 2 * index + bit
    return (table >> index) & 1


def future_row(table, prefix, remaining):
    return tuple(function_value(table, prefix + suffix) for suffix in bit_words(remaining))


def recognition_cut_audit():
    functions = 0
    row_occurrences = 0
    transition_checks = 0
    protocol_pairs = 0
    boundary_checks = 0
    maximum_rows = {}

    for total in range(5):
        functions_at_length = 1 << (1 << total)
        max_rows_at_cut = [0] * (total + 1)
        for table in range(functions_at_length):
            functions += 1
            rows_by_cut = []
            for cut in range(total + 1):
                prefixes = bit_words(cut)
                rows = {prefix: future_row(table, prefix, total - cut) for prefix in prefixes}
                row_set = set(rows.values())
                rows_by_cut.append(rows)
                row_occurrences += len(row_set)
                max_rows_at_cut[cut] = max(max_rows_at_cut[cut], len(row_set))

                # A message/configuration may merge two prefixes exactly when
                # their future rows agree.
                for left in prefixes:
                    for right in prefixes:
                        assert (rows[left] == rows[right]) == all(
                            function_value(table, left + suffix)
                            == function_value(table, right + suffix)
                            for suffix in bit_words(total - cut)
                        )
                        protocol_pairs += 1

                if cut == 0:
                    assert len(row_set) == 1
                    boundary_checks += 1
                if cut == total:
                    assert len(row_set) in (1, 2)
                    boundary_checks += 1

            # Appending one letter gives a representative-independent map on
            # future-row classes.
            for cut in range(total):
                rows = rows_by_cut[cut]
                next_rows = rows_by_cut[cut + 1]
                prefixes = bit_words(cut)
                for left in prefixes:
                    for right in prefixes:
                        if rows[left] != rows[right]:
                            continue
                        for letter in (0, 1):
                            assert next_rows[left + (letter,)] == next_rows[right + (letter,)]
                            transition_checks += 1

        maximum_rows[str(total)] = max_rows_at_cut

    assert maximum_rows["0"] == [1]
    return {
        "boolean_functions": functions,
        "distinct_row_occurrences": row_occurrences,
        "canonical_transition_checks": transition_checks,
        "protocol_prefix_pairs": protocol_pairs,
        "endpoint_boundary_checks": boundary_checks,
        "maximum_rows_by_total_length_and_cut": maximum_rows,
    }


def dyck_step(stack, symbol, bracket_types, neutral):
    if stack is None:
        return None
    if symbol < bracket_types:
        return stack + (symbol,)
    if symbol < 2 * bracket_types:
        wanted = symbol - bracket_types
        return stack[:-1] if stack and stack[-1] == wanted else None
    assert neutral
    return stack


def dyck_midpoint_audit():
    prefix_checks = 0
    row_checks = 0
    cases = 0
    for bracket_types in (1, 2):
        for neutral in (False, True):
            alphabet = tuple(range(2 * bracket_types + int(neutral)))
            for half in range(6):
                stacks = {}
                for prefix in product(alphabet, repeat=half):
                    state = ()
                    for symbol in prefix:
                        state = dyck_step(state, symbol, bracket_types, neutral)
                    stacks[prefix] = state
                    prefix_checks += 1
                rows = {}
                for prefix, state in stacks.items():
                    row = []
                    for suffix in product(alphabet, repeat=half):
                        end = state
                        for symbol in suffix:
                            end = dyck_step(end, symbol, bracket_types, neutral)
                        row.append(int(end == ()))
                    rows[prefix] = tuple(row)
                    row_checks += len(row)
                distinct = len(set(rows.values()))
                if half == 0:
                    expected = 1
                elif neutral:
                    expected = sum(bracket_types ** h for h in range(half + 1)) + 1
                else:
                    expected = sum(
                        bracket_types ** (half - 2 * j)
                        for j in range(half // 2 + 1)
                    ) + 1
                assert distinct == expected
                cases += 1
    return {
        "parameter_cases": cases,
        "midpoint_prefixes": prefix_checks,
        "literal_row_cells": row_checks,
    }


def fold_at(value, center):
    return value if value <= center else 2 * center - value


def two_fold_map(value):
    return fold_at(fold_at(value, Fraction(7)), Fraction(3))


def fold_counterexample_audit():
    p, middle, q, target = map(Fraction, (1, 5, 9, 1))
    assert two_fold_map(p) == two_fold_map(middle) == two_fold_map(q) == target

    # The maximal affine pieces are [0,3], [3,7], and [7,10].  Their slopes
    # are +1, -1, +1, so p and q have equal orientation even though a third
    # layer lies between them.
    pieces = (
        (Fraction(0), Fraction(3), 1),
        (Fraction(3), Fraction(7), -1),
        (Fraction(7), Fraction(10), 1),
    )
    for left, right, slope in pieces:
        probe = (left + right) / 2
        assert two_fold_map(probe + Fraction(1, 10)) - two_fold_map(probe) == slope * Fraction(1, 10)
    assert pieces[0][2] == pieces[2][2]

    radius = Fraction(1, 4)
    footprint = (Fraction(-1), Fraction(3))
    assert footprint[0] < target - radius < target + radius < footprint[1]
    for endpoint in (Fraction(0), Fraction(3), Fraction(7), Fraction(10)):
        assert not target - radius < two_fold_map(endpoint) < target + radius

    truth_table = []
    for x1, x2 in product((0, 1), repeat=2):
        fibre = bool(x1 and True and x2)
        reduced = bool(x1 and x2)
        assert fibre == reduced
        truth_table.append(int(fibre))
    assert truth_table == [0, 0, 0, 1]
    return {
        "folds": 2,
        "affine_pieces": len(pieces),
        "same_orientation_feature_sites": [1, 9],
        "intervening_true_site": 5,
        "common_final_coordinate": 1,
        "punch_radius": "1/4",
        "reduced_term_width": 2,
        "status": "refutes the former orientation-forcing lemma, not the row-count theorem",
    }


def matching_row_audit():
    permutations_checked = 0
    prefix_rows = 0
    for n in range(1, 7):
        words = bit_words(n)
        for permutation in permutations(range(n)):
            rows = set()
            for prefix in words:
                accepting_suffix = tuple(prefix[permutation.index(j)] for j in range(n))
                row = tuple(int(suffix == accepting_suffix) for suffix in words)
                rows.add(row)
            assert len(rows) == 1 << n
            permutations_checked += 1
            prefix_rows += len(rows)
    return {
        "permutations": permutations_checked,
        "distinct_prefix_rows": prefix_rows,
        "maximum_n": 6,
    }


def formula_resource_audit():
    mismatch_assignments = 0
    mismatch_terms = 0
    for n in range(1, 8):
        terms = []
        for i in range(n):
            terms.append((i, 1, 2 * n - 1 - i, 0))
            terms.append((i, 0, 2 * n - 1 - i, 1))
        assert len(terms) == 2 * n
        mismatch_terms += len(terms)
        for assignment in bit_words(2 * n):
            direct = any(assignment[i] != assignment[2 * n - 1 - i] for i in range(n))
            dnf = any(
                assignment[i] == vi and assignment[j] == vj
                for i, vi, j, vj in terms
            )
            assert direct == dnf
            mismatch_assignments += 1

    parity_assignments = 0
    parity_literal_occurrences = 0
    for variables in range(1, 9):
        odd = [assignment for assignment in bit_words(variables) if sum(assignment) % 2]
        assert len(odd) == 1 << (variables - 1)
        for assignment in bit_words(variables):
            covered = assignment in odd
            assert covered == bool(sum(assignment) % 2)
            parity_assignments += 1
        parity_literal_occurrences += variables * len(odd)

    packing_checks = 0
    for folds in range(7):
        for footprint_units in range(1, 10):
            for separation_units in range(1, footprint_units + 1):
                per_piece = footprint_units // separation_units + 1
                sites = (1 << folds) * per_piece
                assert sites <= (1 << folds) * (Fraction(footprint_units, separation_units) + 1)
                packing_checks += 1

    return {
        "mismatch_assignments": mismatch_assignments,
        "mismatch_prime_terms": mismatch_terms,
        "parity_assignments": parity_assignments,
        "parity_literal_occurrences": parity_literal_occurrences,
        "packing_inequality_cases": packing_checks,
    }


def main():
    result = {
        "result": "pass",
        "recognition_cuts": recognition_cut_audit(),
        "dyck_midpoint_instantiation": dyck_midpoint_audit(),
        "fold_counterexample": fold_counterexample_audit(),
        "matching_rows": matching_row_audit(),
        "fold_formula_resources": formula_resource_audit(),
    }
    print(json.dumps(result, indent=2, sort_keys=True))


if __name__ == "__main__":
    main()