#!/usr/bin/env python3 """Finite audit for FPRD-T156, residual towers and transport.""" from __future__ import annotations import json from itertools import product from pathlib import Path ALPHABET = (0, 1) def words_exact(length: int) -> list[tuple[int, ...]]: return list(product(ALPHABET, repeat=length)) def words_upto(length: int) -> list[tuple[int, ...]]: return [word for size in range(length + 1) for word in words_exact(size)] def row(language: dict[tuple[int, ...], int], prefix: tuple[int, ...], horizon: int) -> tuple[int, ...]: return tuple(language[prefix + suffix] for suffix in words_upto(horizon)) def audit_finite_language_trees(depth: int = 3) -> dict[str, int]: universe = words_upto(depth) index = {word: position for position, word in enumerate(universe)} languages = 0 restriction_checks = 0 derivative_checks = 0 word_transport_checks = 0 for mask in range(1 << len(universe)): language = {word: (mask >> index[word]) & 1 for word in universe} languages += 1 for prefix_length in range(depth + 1): for prefix in words_exact(prefix_length): remaining = depth - prefix_length for horizon in range(remaining): larger = row(language, prefix, horizon + 1) smaller = row(language, prefix, horizon) assert larger[: len(smaller)] == smaller restriction_checks += 1 large_suffixes = words_upto(horizon + 1) location = {suffix: pos for pos, suffix in enumerate(large_suffixes)} for letter in ALPHABET: derived = tuple( larger[location[(letter,) + suffix]] for suffix in words_upto(horizon) ) assert derived == row(language, prefix + (letter,), horizon) derivative_checks += 1 # Check the general word action whenever a positive transport # word and a nonnegative target horizon fit in the finite tree. for transport_length in range(1, remaining + 1): target_horizon = remaining - transport_length source = row(language, prefix, remaining) source_suffixes = words_upto(remaining) location = {suffix: pos for pos, suffix in enumerate(source_suffixes)} for transport in words_exact(transport_length): derived = tuple( source[location[transport + suffix]] for suffix in words_upto(target_horizon) ) assert derived == row(language, prefix + transport, target_horizon) word_transport_checks += 1 return { "finite_tree_languages": languages, "restriction_checks": restriction_checks, "one_letter_derivative_checks": derivative_checks, "word_transport_checks": word_transport_checks, } def reachable_states(transitions: tuple[int, ...], states: int) -> tuple[int, ...]: reached = {0} frontier = [0] while frontier: state = frontier.pop() for letter in ALPHABET: target = transitions[2 * state + letter] if target not in reached: reached.add(target) frontier.append(target) return tuple(sorted(reached)) def canonical_ids(signatures: dict[int, object]) -> dict[int, int]: values = {value: index for index, value in enumerate(sorted(set(signatures.values()), key=repr))} return {state: values[value] for state, value in signatures.items()} def audit_dfas(max_states: int = 3) -> dict[str, int]: automata = 0 quotient_levels = 0 restriction_surjections = 0 derivative_well_defined_checks = 0 stabilization_checks = 0 for states in range(1, max_states + 1): for transitions in product(range(states), repeat=2 * states): reachable = reachable_states(transitions, states) for outputs in product((0, 1), repeat=states): automata += 1 ids = canonical_ids({state: outputs[state] for state in reachable}) counts = [len(set(ids.values()))] level_ids = [ids] # At most |reachable|-1 strict refinements can occur. for _ in range(len(reachable) + 1): signatures = { state: ( outputs[state], ids[transitions[2 * state]], ids[transitions[2 * state + 1]], ) for state in reachable } next_ids = canonical_ids(signatures) counts.append(len(set(next_ids.values()))) level_ids.append(next_ids) quotient_levels += 1 # Refinement makes restriction a surjection. class_to_old: dict[int, int] = {} for state in reachable: new_class = next_ids[state] old_class = ids[state] assert class_to_old.setdefault(new_class, old_class) == old_class restriction_surjections += 1 # A letter maps each new class to one old class. for letter in ALPHABET: derivative: dict[int, int] = {} for state in reachable: source_class = next_ids[state] target_class = ids[transitions[2 * state + letter]] assert derivative.setdefault(source_class, target_class) == target_class derivative_well_defined_checks += 1 ids = next_ids assert all(left <= right for left, right in zip(counts, counts[1:])) first_equal = next( index for index in range(len(counts) - 1) if counts[index] == counts[index + 1] ) assert all(count == counts[first_equal] for count in counts[first_equal:]) assert counts[first_equal] <= len(reachable) stabilization_checks += 1 return { "binary_dfas": automata, "dfa_quotient_levels": quotient_levels, "dfa_restriction_surjections": restriction_surjections, "dfa_derivative_well_defined_checks": derivative_well_defined_checks, "dfa_stabilization_checks": stabilization_checks, } def audit_unary_completion(witnesses: int = 12) -> dict[str, int]: # alpha = 1, 10, 100, 1000, ... concatenated. sequence: list[int] = [] starts: list[int] = [] for zeros in range(witnesses + 3): starts.append(len(sequence)) sequence.append(1) sequence.extend([0] * zeros) checks = 0 for horizon in range(1, witnesses + 1): block = horizon + 1 shift = starts[block] + 1 assert sequence[shift : shift + horizon] == [0] * horizon assert 1 in sequence[shift + horizon :] checks += 1 return {"unary_ideal_residual_witnesses": checks} def run() -> dict[str, object]: result: dict[str, object] = {"status": "pass"} result.update(audit_finite_language_trees()) result.update(audit_dfas()) result.update(audit_unary_completion()) return result if __name__ == "__main__": result = run() output = Path(__file__).with_name("checker-output.json") output.write_text(json.dumps(result, indent=2) + "\n", encoding="utf-8") print(json.dumps(result, indent=2))