check_spine_incidence_independent.py

#!/usr/bin/env python3
"""Independent finite semantic audit for assessment 205.

No imports from the producer, scheduler or primary research audit.  This checks
literal sibling-pair incidence, not a native time bound.  A deterministic trie
route is deliberately separated from the set intersection stored at its leaf.
"""

import itertools
import json


def trie(words):
    root = {}
    for word in words:
        node = root
        for bit in word:
            node = node.setdefault(bit, {})
        node["terminal"] = True
    return root


def routed(root, word):
    """At most one current trie node; one edge chosen per actual bit."""
    node = root
    for bit in word:
        if bit not in node:
            return False
        node = node[bit]
    return node.get("terminal", False)


def audit():
    # Equal-length parent families retain the theorem-67 per-slot gate for r=2.
    # A singleton leaf has one mixed ancestor per binary band-tree level.
    for length in range(2, 4097):
        band = length.bit_length()
        index_block_start = 1 << (band.bit_length()-1)
        mixed_singleton = band-1
        assert mixed_singleton < 2*index_block_start
    parents = ("00", "01", "10", "11")
    geometry = trie(parents)
    intersections = 0
    monotone_prefixes = 0
    for matrix in range(1 << 12):
        incidence = {
            p: frozenset(v for v in range(3) if matrix & (1 << (4*v+j)))
            for j, p in enumerate(parents)
        }
        rows = [
            frozenset(p+b for p in parents for b in "01" if v in incidence[p])
            for v in range(3)
        ]
        for subset in range(8):
            selected = frozenset(v for v in range(3) if subset & (1 << v))
            literal_union = set().union(*(rows[v] for v in selected))
            for p in parents:
                assert routed(geometry, p)
                expected = bool(selected.intersection(incidence[p]))
                for bit in "01":
                    assert ((p+bit) in literal_union) == expected
                    intersections += 1
            assert "0000" not in literal_union
        for order in itertools.permutations(range(3)):
            old = frozenset()
            snapshots = [old]
            for v in order:
                new = old | rows[v]
                assert old <= new
                snapshots.append(new)
                old = new
            for i, snapshot in enumerate(snapshots):
                for p in parents:
                    assert ((p+"0") in snapshot) == any(
                        v in incidence[p] for v in order[:i]
                    )
                    monotone_prefixes += 1

    # One fixed geometry contains every possible terminal incidence vector.
    # Singleton selections recover every matrix entry without trie ambiguity.
    for vector in range(8):
        owners = {v for v in range(3) if vector & (1 << v)}
        assert [bool({v} & owners) for v in range(3)] == [
            bool(vector & (1 << v)) for v in range(3)
        ]

    # Ancestor-to-incidence semantic reduction on a complete binary tree.
    # Names and static incidence expansion are explicit; no cost transfer claimed.
    ancestors = 0
    nodes = ("", "0", "1", "00", "01", "10", "11")
    leaves = parents
    for marking in range(1 << len(nodes)):
        marked = {v for i, v in enumerate(nodes) if marking & (1 << i)}
        for leaf in leaves:
            owners = {v for v in nodes if leaf.startswith(v)}
            literal = {leaf+b for v in marked for b in "01" if leaf.startswith(v)}
            assert bool(marked & owners) == ((leaf+"0") in literal)
            ancestors += 1

    # Losing correlation between ancestor prefixes and depth intervals is unsound.
    cone_rows = (("0", 3, 3), ("1", 2, 2))
    query = "00"
    prefix_exists = any(query[:-1].startswith(q) for q, _, _ in cone_rows)
    depth_exists = any(lo <= len(query) <= hi for _, lo, hi in cone_rows)
    joint_exists = any(
        query[:-1].startswith(q) and lo <= len(query) <= hi
        for q, lo, hi in cone_rows
    )
    assert prefix_exists and depth_exists and not joint_exists

    return {
        "scope": "finite semantics only; no native or cell-probe lower bound",
        "all_3_by_4_incidence_matrices": 4096,
        "literal_pair_intersection_checks": intersections,
        "insert_only_retained_prefix_checks": monotone_prefixes,
        "marked_ancestor_incidence_checks": ancestors,
        "terminal_incidence_vectors_same_geometry": 8,
        "singleton_depth_budget_checks": 4095,
        "separate_prefix_depth_summary_counterexamples": 1,
        "status": "passed",
    }


if __name__ == "__main__":
    print(json.dumps(audit(), indent=2))