[1337isnot1337]

Summary

Adds an independent exhaustive audit of PR #3818's partial union-support
completion bound at (n,L)=(4,8). The verifier scans the full unpruned domain,
checks every canonical restored completion at every prefix, and compares the
surviving universal words with the unpruned set.

Result

• All 4^8 = 65,536 raw label words were scanned; 105 canonical restored
  words remain.
• All 26 unpruned universal words survive the proposed bound.
• Across 840 prefix/completion checks, 227 target/prefix pairs fail the
  completion-capacity condition; none has a universal completion.
• The exact PR Strengthen the length-22 seven-label census with a union-support budget; exclude the (9,9) split (no new kappa) #3818 engine at head
  e09a08b5f85e648be373bece1b6ea1265d5ea8fa was also compiled at N=4,L=8.
  In union-only mode its split (4,4) hit set exactly matched the independent
  unpruned set: 22 universal words.
• The 01021323 control reconstructs the old false-prune: bit-0 excess 8,
  invalid balanced budget 5, valid actual-size budget 9.

The argument behind the bound is that each future same-parity pair can add at
most one new nonzero even mask. A universal completion needs all
2^(n-1)-1 such masks, so the current union plus the maximum number of future
pair incidences is an upper bound on attainable support.

Separate source observation for PR #3818

In the same exact-source check, union-only mode reports
all_restored_leaves=22 although the unpruned (4,8,4,4) domain has 27
restored words; five are removed by the union budget. The JSON writer fills
that field when the two older budgets are disabled, even though the union
budget remains enabled. The full --no-budgets control correctly reports 27.
This package does not edit PR #3818's source; please correct that field's
enablement condition before relying on it as an unpruned count.

Reproduction

python3 -B scripts/research_package.py --package research/f7-l22-union-prune-audit --check-only
python3 -B scripts/research_package.py --package research/f7-l22-union-prune-audit

The second command prints PASS_F7_L22_UNION_PRUNE_TINY_EXHAUSTIVE and
PASS_REGISTERED_RESEARCH_PACKAGE. Full details and source pins are in the
package README and SOURCES.json.

This establishes finite evidence only. It does not replay PR #3818's seven-
label (9,9) L22 exclusion or certify the other five L22 node floors. Credit
Ross Richardson, Aaron Wang, Nicholas Stone and Nick Petalas for the model and
predecessor work. This audit used substantial OpenAI Codex assistance; no
formal proof-kernel or independent human review is claimed.

Current overlap

Open PRs #3699, #3708 and #3733 cover seven-label or length-22 functional classification. This package stays on PR #3818's (n,L)=(4,8) domain and independently checks its tiny union-pruning result, including the recorded reporting-field defect. It claims no f(7) bound.

Publication validation

python3.12 scripts/research_package.py --package research/f7-l22-union-prune-audit passed on CPython 3.12.3, and python3.12 scripts/check_research_commit.py --package research/f7-l22-union-prune-audit --check-source-history passed. The registered replay left the worktree clean. This supersedes any earlier pending note above for the registered package replay; separate full selected cold-replay limits remain as stated.

[rcfc-jreed]

Independent scoped audit of the L22 union-prune tiny-domain package at e687791f: packaging defect (missing RESULT.json); finite domain math otherwise agrees

Code-disjoint checks; does not import package verify.py. Package bytes from head e687791f733e10adb6c3217fa93b3ad8449f1ee8 via GitHub contents API. CLAIM. The PR #3818 C engine comparison was not recompiled here.

Defect found:

• D1 — missing RESULT.json. TASK.evidence and verify.py cite status PASS_F7_L22_UNION_PRUNE_TINY_EXHAUSTIVE, but the package ships no committed RESULT.json. The pass seal exists only as runtime stdout from verify.py, so a seal-only auditor cannot recompute a frozen result artifact from package files alone.

What still passes (independent recomputation):

1. Pins: base 20ecf289…; VERIFY ready.
2. Fixture 01021323: weight split (4,4); bit-0 split (6,2) with excess 8 > substituted budget 5.
3. Domain: 4^8 = 65536 raw; 105 canonical restored; 26 universal; all 26 retained by the union rule; 840 prefix checks; 227 pruned target/prefix pairs; 0 bad; max bound gap 0; split (4,4) has 22 universal words.

Not covered: live PR #3818 C compile; L22 (9,9) billion-node replay; new κ.

This is a finite replay of the tiny domain, not a formal proof. Adding a committed RESULT.json matching the printed status would close D1.

check_3899.py

#!/usr/bin/env python3
"""Independent finite controls for PR3899 (L22 union prune tiny domain).

Recomputes the (n,L)=(4,8) exhaustive domain and fixture without importing
package verify.py. Also checks packaging seals.

Package head e687791f733e10adb6c3217fa93b3ad8449f1ee8 via GitHub API.

James Reed (@rcfc-jreed), with substantial AI assistance (Claude, in Cursor).
Apache-2.0.
"""
from __future__ import annotations

import argparse, json, sys
from collections import Counter, defaultdict
from itertools import product
from pathlib import Path

HEAD = "e687791f733e10adb6c3217fa93b3ad8449f1ee8"
BASE = "20ecf2891d80b5acf18d980b2164fb44ea7faa90"
results = []


def check(name, ok, detail=""):
    results.append((name, bool(ok), detail))
    print(("PASS " if ok else "FAIL ") + name + ((": " + str(detail)) if detail else ""), flush=True)
    return bool(ok)


def load(pkg, name):
    return json.loads((pkg / name).read_text(encoding="utf-8"))


def choose2(n):
    return n * (n - 1) // 2


def canonical(word):
    high = -1
    for label in word:
        if label < 0 or label > high + 1:
            return False
        high = max(high, label)
    return word[0] == 0 and high == max(word)


def path_states(word):
    q = 0
    states = []
    for label in word:
        states.append(q)
        q ^= 1 << label
    return tuple(states), q


def classes(points):
    return tuple({x for x in points if (x.bit_count() & 1) == p} for p in (0, 1))


def within_support(group):
    return {a ^ b for a in group for b in group if a != b}


def pair_supports(points):
    even, odd = classes(points)
    same = within_support(even) | within_support(odd)
    cross = {a ^ b for a in even for b in odd}
    return even, odd, same, cross


def independent_domain():
    n, length = 4, 8
    all_masks = set(range(1 << n))
    need_even = (1 << (n - 1)) - 1
    raw_words = 0
    valid_words = []
    for word in product(range(n), repeat=length):
        raw_words += 1
        if not canonical(word):
            continue
        counts = Counter(word)
        if set(counts) != set(range(n)) or any(c < 2 or c % 2 for c in counts.values()):
            continue
        states, final = path_states(word)
        if final != 0:
            continue
        points = set(states)
        even, odd, same, cross = pair_supports(points)
        universal = {a ^ b for a in points for b in points} == all_masks
        final_split = (len(even), len(odd))
        valid_words.append((word, states, points, final_split, same, cross, universal))

    prefixes = defaultdict(lambda: {"completions": 0, "universal": 0})
    pruned_prefixes = set()
    audits = 0
    max_bound_gap = 0
    universal_words = set()

    for word, states, points, (s, t), final_same, final_cross, universal in valid_words:
        if universal:
            universal_words.add(word)
        for k in range(1, length + 1):
            prefix_points = set(states[:k])
            even, odd, current_same, _ = pair_supports(prefix_points)
            e, o = len(even), len(odd)
            future_same = choose2(s) + choose2(t) - choose2(e) - choose2(o)
            upper = len(current_same) + future_same
            audits += 1
            max_bound_gap = max(max_bound_gap, len(final_same) - upper)
            prefix_labels = word[:k - 1]
            key = ((s, t), prefix_labels)
            prefixes[key]["completions"] += 1
            prefixes[key]["universal"] += int(universal)
            if upper < need_even:
                pruned_prefixes.add(key)

    bad = [key for key in pruned_prefixes if prefixes[key]["universal"]]
    retained = {
        word for word, states, points, (s, t), final_same, final_cross, universal in valid_words
        if universal and all(
            len(pair_supports(set(states[:k]))[2])
            + choose2(s) + choose2(t)
            - choose2(len(pair_supports(set(states[:k]))[0]))
            - choose2(len(pair_supports(set(states[:k]))[1])) >= need_even
            for k in range(1, length + 1)
        )
    }
    return {
        "raw_words": raw_words,
        "canonical_restored": len(valid_words),
        "universal": len(universal_words),
        "retained": len(retained),
        "audits": audits,
        "pruned": len(pruned_prefixes),
        "bad": len(bad),
        "max_gap": max_bound_gap,
        "retained_eq": retained == universal_words,
        "split44_universal": sum(
            1 for w, st, pts, split, *rest in valid_words
            if rest[-1] and split == (4, 4)
        ),
    }


def fixture_ok():
    word = tuple(map(int, "01021323"))
    states, final = path_states(word)
    points = set(states)
    coverage = {a ^ b for a in points for b in points}
    by_weight = [set(x for x in points if (x.bit_count() & 1) == p) for p in (0, 1)]
    by_bit0 = [set(x for x in points if (x & 1) == p) for p in (0, 1)]
    need = 7
    weight_excess = sum(choose2(len(g)) - len(within_support(g)) for g in by_weight)
    bit0_excess = sum(choose2(len(g)) - len(within_support(g)) for g in by_bit0)
    substituted_budget = 2 * choose2(4) - need
    actual_bit0_budget = sum(choose2(len(g)) for g in by_bit0) - need
    return (
        final == 0 and len(points) == 8 and coverage == set(range(16))
        and tuple(map(len, by_weight)) == (4, 4)
        and tuple(map(len, by_bit0)) == (6, 2)
        and bit0_excess == 8 and substituted_budget == 5
        and bit0_excess > substituted_budget
        and bit0_excess <= actual_bit0_budget == 9
        and weight_excess <= substituted_budget
    )


def run(pkg: Path):
    task = load(pkg, "TASK.json")
    sources = load(pkg, "SOURCES.json")
    verify = load(pkg, "VERIFY.json")
    readme = (pkg / "README.md").read_text(encoding="utf-8")
    verify_py = (pkg / "verify.py").read_text(encoding="utf-8")

    check("I1 TASK/SOURCES base_commit == 20ecf289…; VERIFY ready",
          task["base_commit"] == BASE == sources["base_commit"]
          and verify["status"] == "ready")
    check("D1 packaging: RESULT.json is absent despite TASK.evidence citing PASS_F7_L22_UNION_PRUNE_TINY_EXHAUSTIVE",
          not (pkg / "RESULT.json").exists()
          and "PASS_F7_L22_UNION_PRUNE_TINY_EXHAUSTIVE" in task["evidence"]
          and "PASS_F7_L22_UNION_PRUNE_TINY_EXHAUSTIVE" in verify_py)

    check("F1 fixture 01021323: weight (4,4) excess OK; bit0 (6,2) excess 8 > budget 5",
          fixture_ok())

    dom = independent_domain()
    check("M1 domain: 4^8=65536 raw; 105 canonical restored; 26 universal",
          dom["raw_words"] == 65536
          and dom["canonical_restored"] == 105
          and dom["universal"] == 26)
    check("M2 union retention: all 26 universal words retained; retained set equals unpruned",
          dom["retained"] == 26 and dom["retained_eq"])
    check("M3 prefix audits: 840 checks; 227 pruned target/prefix pairs; 0 bad; max gap 0",
          dom["audits"] == 840
          and dom["pruned"] == 227
          and dom["bad"] == 0
          and dom["max_gap"] == 0)
    check("M4 README table agrees with independent recomputation",
          "| Canonical restored words | 105 |" in readme
          and "| Universal words in the unpruned domain | 26 |" in readme
          and "| Prefix/completion checks | 840 |" in readme
          and "| Distinct target/prefix pairs rejected by the bound | 227 |" in readme
          and "| Rejected pairs with a universal completion | 0 |" in readme)
    check("M5 split (4,4) has 22 universal words (matches claimed C engine hit-set size)",
          dom["split44_universal"] == 22)
    check("N1 scope: tiny domain only; L22 (9,9) replay explicitly not claimed",
          "does not certify" in readme.lower()
          and "length-22" in readme.lower()
          and "no seven-label" in readme.lower())

    failed = [name for name, ok, _ in results if not ok]
    print(f"\n{len(results) - len(failed)}/{len(results)} PASS", flush=True)
    if failed:
        print("FAILED:", ", ".join(failed), flush=True)
        return 1
    return 0


def main():
    ap = argparse.ArgumentParser()
    ap.add_argument("--pkg", required=True)
    ap.add_argument("--expect-head", default=HEAD)
    args = ap.parse_args()
    check("HEAD pin recorded (API fetch)", args.expect_head == HEAD, args.expect_head)
    return run(Path(args.pkg))


if __name__ == "__main__":
    sys.exit(main())

James Reed (@rcfc-jreed), with substantial AI assistance (Claude, in Cursor).