From b5bb91b123697d9a818ae35d2e165478756c960a Mon Sep 17 00:00:00 2001 From: James Reed Date: Fri, 16 Oct 2026 17:13:56 -0700 Subject: [PATCH] Record the bit-0 census false prune on 01021323 The pinned length-18 call groups prefix states by bit 0 and applies the balanced weight budget. That walk rejects this universal four-label word, and 6 of 22 simple canonical universal words at the same size. --- research/f7-bit0-false-prune/README.md | 74 ++++++ research/f7-bit0-false-prune/RESULT.json | 45 ++++ research/f7-bit0-false-prune/SOURCES.json | 30 +++ research/f7-bit0-false-prune/TASK.json | 72 ++++++ research/f7-bit0-false-prune/VERIFY.json | 23 ++ research/f7-bit0-false-prune/test_verify.py | 32 +++ research/f7-bit0-false-prune/verify.py | 241 ++++++++++++++++++++ 7 files changed, 517 insertions(+) create mode 100644 research/f7-bit0-false-prune/README.md create mode 100644 research/f7-bit0-false-prune/RESULT.json create mode 100644 research/f7-bit0-false-prune/SOURCES.json create mode 100644 research/f7-bit0-false-prune/TASK.json create mode 100644 research/f7-bit0-false-prune/VERIFY.json create mode 100644 research/f7-bit0-false-prune/test_verify.py create mode 100644 research/f7-bit0-false-prune/verify.py diff --git a/research/f7-bit0-false-prune/README.md b/research/f7-bit0-false-prune/README.md new file mode 100644 index 0000000000..83b23ff085 --- /dev/null +++ b/research/f7-bit0-false-prune/README.md @@ -0,0 +1,74 @@ +# The length-18 census budget rejects a universal four-label word + +**Partial. No new exponent.** + +The pinned #2542 census groups prefix states by bit 0 and prunes them with a +budget derived for Hamming-weight parity. On the universal word `01021323` +those two groupings disagree. The same budget rejects 6 of the 22 simple +canonical universal words at four labels and length 8. No seven-label census +was run. + +## What was executed + +The word `01021323` has prefix states `0,1,3,2,6,4,12,8` and then returns to +`0`. Those eight states are distinct, their pairwise sums cover all 16 masks, +and every label occurs twice. Grouped by Hamming weight the classes are +`(4, 4)` and the collision count stays 0, inside the balanced budget 5. +Grouped by bit 0 the classes are `(6, 2)` and the collision count reaches 8 +at the seventh step. The budget substituted from the balanced weight split is +5, so that walk is rejected. The budget for the actual bit-0 sizes is 9, and +8 does not exceed it. + +The pinned call is `cyclic_census(7, 18, budget=9, simple=True)`. Its comment +derives 9 from `C(9,2)+C(9,2)-63`, the weight split `(9, 9)`. The engine +itself puts a new state in the odd class when `nq & 1`. The length-20 package +vendors that same engine text. + +The small domain is every restricted-growth word with even label counts at +`(n, L)` in `{(3, 6), (3, 8), (4, 8)}`. The universal counts are 10, 182 and +26. Restricting to words whose nonclosing states are distinct, which is the +`simple=True` walk, leaves no false prune at three labels. At four labels and +length 8 it leaves 6. None of those six exceed the budget of their own weight +split. + +## Scope and evidence + +Original card: `census-pruning-audit`, priority revision 6, refined to this +word and this domain. [TASK.json](TASK.json) records the scope change. +[RESULT.json](RESULT.json) is the executed receipt and is not rewritten. +[SOURCES.json](SOURCES.json) pins the two engines, the length-18 call, and +the task catalogue. No selected frontier file changes. This does not replay +the corrected seven-label census and does not decide `f(7)`. + +## Reproduce + +From the repository root, standard-library Python 3.12: + +```sh +python3.12 -B research/f7-bit0-false-prune/verify.py +python3.12 -B research/f7-bit0-false-prune/test_verify.py +python3.12 -B scripts/research_package.py --package research/f7-bit0-false-prune +``` + +The domain enumeration is the slow command. It finishes in well under a second. + +## Open next questions + +A corrected weight-parity replay would be needed before the length-18 zero-hit +receipt can be read as an exclusion. That replay is a separate seven-label +budget, and this package does not run it. + +The author-checked claim `22 <= f(7) <= 24` in the PR943 model likewise stays +outside this check. + +## Credit + +Aaron Wang supplied the #2542 engine and the length-18 call that this walk +reconstructs. The length-20 package vendors that engine. Nicholas Stone's +#2973 named `01021323` and separated the two budgets; this package recomputes +the walk and the small domain rather than importing that checker. Ross +Richardson supplied the PR943 prefix-walk model in which the later census +question is posed. + +Prepared by jwr with substantial Cursor agent assistance. No independent human +review is claimed. Apache-2.0. diff --git a/research/f7-bit0-false-prune/RESULT.json b/research/f7-bit0-false-prune/RESULT.json new file mode 100644 index 0000000000..57e1b0a84e --- /dev/null +++ b/research/f7-bit0-false-prune/RESULT.json @@ -0,0 +1,45 @@ +{ + "word": [0, 1, 0, 2, 1, 3, 2, 3], + "prefix_states": [0, 1, 3, 2, 6, 4, 12, 8, 0], + "prefix_set": [0, 1, 2, 3, 4, 6, 8, 12], + "universal": true, + "weight_split": [4, 4], + "weight_collisions": 0, + "balanced_budget": 5, + "bit0_split": [6, 2], + "bit0_collisions": 8, + "bit0_actual_budget": 9, + "bit0_exceeds_balanced_at_index": 6, + "predecessor_call": "cyclic_census(7, 18, budget=9, simple=True)", + "vendored_engine_same_text": true, + "domains": [ + { + "n": 3, + "length": 6, + "universal": 10, + "simple_universal": 4, + "balanced_budget": 3, + "simple_false_prunes": 0, + "weight_budget_exceeded": 0 + }, + { + "n": 3, + "length": 8, + "universal": 182, + "simple_universal": 2, + "balanced_budget": 9, + "simple_false_prunes": 0, + "weight_budget_exceeded": 0 + }, + { + "n": 4, + "length": 8, + "universal": 26, + "simple_universal": 22, + "balanced_budget": 5, + "simple_false_prunes": 6, + "weight_budget_exceeded": 0 + } + ], + "no_new_kappa": true +} diff --git a/research/f7-bit0-false-prune/SOURCES.json b/research/f7-bit0-false-prune/SOURCES.json new file mode 100644 index 0000000000..fd1d264b23 --- /dev/null +++ b/research/f7-bit0-false-prune/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "18aacb215fc3717b06be8ceb9fca62aeca0d3e99", + "files": [ + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5", + "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0" + }, + { + "path": "research/universal-f7-singleton-seedb859517b/engine.py", + "usage": "input", + "git_blob": "210bd817b19beb20ed474d8946ea87a22121ac1c", + "sha256": "82e4c407b58864c74ffd14d47f00b6b1675005ee0e0173909b7bd092491175e4" + }, + { + "path": "research/universal-f7-singleton-seedb859517b/search.py", + "usage": "input", + "git_blob": "2bb66b86822fdc248330ffb55bfe955ff4640ea9", + "sha256": "d8bad428035806848f9e0dc6caa3193e1a9abbad6a589dff3ef0e0b66f5f006c" + }, + { + "path": "research/universal-f7-singleton-l20-seed06704c39/engine.py", + "usage": "input", + "git_blob": "210bd817b19beb20ed474d8946ea87a22121ac1c", + "sha256": "82e4c407b58864c74ffd14d47f00b6b1675005ee0e0173909b7bd092491175e4" + } + ] +} diff --git a/research/f7-bit0-false-prune/TASK.json b/research/f7-bit0-false-prune/TASK.json new file mode 100644 index 0000000000..3fa434bd3d --- /dev/null +++ b/research/f7-bit0-false-prune/TASK.json @@ -0,0 +1,72 @@ +{ + "schema_version": 1, + "task_id": "census-pruning-audit", + "priority_revision": 6, + "base_commit": "18aacb215fc3717b06be8ceb9fca62aeca0d3e99", + "original_card": { + "id": "census-pruning-audit", + "question": "Does the reported word-census parity-pruning error invalidate a specific exclusion we still rely on, and what bounded repair is justified?", + "starting_points": [ + "research/f7-weight-parity-census-correction/README.md", + "docs/research/research-family-status.md" + ], + "methods": [ + "Independently reconstruct the tiny counterexample and trace one affected exclusion to its exact pruning code.", + "Compare corrected and unpruned enumeration on a small exhaustive domain, then audit the changed pruning implication." + ], + "acceptance_gate": "Pin the old and proposed corrected engines, distinguish a disproved pruning rule from a disproved final bound, and state exactly which downstream exclusions need revalidation. #2973 is an author-checked source archive; neither its new f(7) claim nor all old conclusions are automatically accepted or rejected.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read #2973 error description and MATH.md; manually reconstruct the prefix states of 01021323 before running any large census.", + "scope": "Source-binding orientation only; no full enumeration or mathematical validation." + }, + "first_experiment": "Reconstruct the eight prefix states of 01021323 and compare bit-0 versus Hamming-weight parity budgets independently. Trace the reported false prune to one pinned predecessor (#2542, #2634 or #2691), then test a small exhaustive domain. Stop after a source-impact handoff or corrected-prune proof; a full seven-label replay needs a separate resource budget and a named research decision it can change.", + "bottleneck_link": "An unsound exclusion can wrongly close a mechanism; correcting its dependency boundary is more useful than extending the same census.", + "allowed_variations": [ + "One predecessor pruning rule, one independently exhaustive small domain, or one downstream dependency audit." + ], + "scope_change_triggers": [ + "Launching a larger census before validating the prune and explaining which active decision it changes.", + "Treating a small-domain counterexample to the old rule as a counterexample to every reported seven-label bound." + ], + "overlap_terms": [ + "2973", + "2542", + "2634", + "2691", + "weight parity", + "bit-0", + "01021323", + "census pruning" + ] + }, + "scope_status": "refined", + "actual_scope": "Does the pinned #2542 bit-0 census, using the balanced weight budget, reject the universal word 01021323, and how many simple canonical universal words at n<=4 and L<=8 does that rule reject?", + "scope_change_reason": "The card asks for the eight prefix states of 01021323, one pinned predecessor, and a small exhaustive domain, then a stop. This does not replay the seven-label census or decide f(7).", + "bottleneck_link": "A word-census exclusion is usable only if its prune matches the partition that justifies the budget. This is that check for the pinned length-18 call, on one universal word and three small domains.", + "budget_minutes": 60, + "stop_rule": "Stop once the bit-0 walk and the weight walk are compared on 01021323 and the simple false prunes are counted for n<=4 and L<=8. Do not run a seven-label census and do not search for a new kappa.", + "outcome": "partial", + "evidence": "The word 01021323 is universal, with distinct prefix states 0,1,3,2,6,4,12,8. Its weight-parity collision count is 0 against budget 5. Its bit-0 collision count is 8 and crosses budget 5 at step 6. The same rule rejects 6 of 22 simple canonical universal words at n=4, L=8, and none of the simple universal words at the two three-label domains.", + "author": "jwr", + "ai_assistance": "Substantial assistance from the Cursor coding agent in the execution, checker and writeup.", + "open_questions": [ + { + "question": "Does the pinned length-18 zero-hit receipt survive when the collision budget is computed from Hamming-weight classes instead of bit 0?", + "why_it_matters": "The call cyclic_census(7, 18, budget=9, simple=True) uses the unsound substitution. A zero hit under that filter does not by itself exclude the (9, 9) words.", + "first_step": "Replay the length-18 simple census with the weight-parity collision counter and the budget 9 that belongs to split (9, 9).", + "blocked_by": "That replay is the seven-label census this package is required to stop before." + }, + { + "question": "Is the author-checked bound 22 <= f(7) <= 24 valid in the PR943 singleton prefix-walk model?", + "why_it_matters": "The small-domain false prune does not decide the seven-label minimum.", + "first_step": "Independently replay one corrected length-20 split and the length-24 witness, or show a sound obstruction the corrected census missed.", + "blocked_by": "No corrected seven-label traversal is executed here." + } + ] +} diff --git a/research/f7-bit0-false-prune/VERIFY.json b/research/f7-bit0-false-prune/VERIFY.json new file mode 100644 index 0000000000..07d0dfc109 --- /dev/null +++ b/research/f7-bit0-false-prune/VERIFY.json @@ -0,0 +1,23 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/universal-f7-singleton-seedb859517b/engine.py", + "research/universal-f7-singleton-seedb859517b/search.py", + "research/universal-f7-singleton-l20-seed06704c39/engine.py" + ], + "commands": [ + { + "argv": ["{python}", "-B", "{package}/verify.py"], + "timeout_seconds": 60, + "checks": "Reconstruct 01021323 under both groupings, pin the length-18 bit-0 call, and count simple false prunes on three small domains." + }, + { + "argv": ["{python}", "-B", "{package}/test_verify.py"], + "timeout_seconds": 30, + "checks": "Check the eight prefix states, both budgets, and the step where the balanced budget is crossed." + } + ] +} diff --git a/research/f7-bit0-false-prune/test_verify.py b/research/f7-bit0-false-prune/test_verify.py new file mode 100644 index 0000000000..a16b962602 --- /dev/null +++ b/research/f7-bit0-false-prune/test_verify.py @@ -0,0 +1,32 @@ +#!/usr/bin/env python3 +"""The eight prefix states and both budgets, without the domain enumeration.""" + +import importlib.util +from pathlib import Path + +HERE = Path(__file__).resolve().parent +spec = importlib.util.spec_from_file_location("f7_bit0_false_prune", HERE / "verify.py") +verify = importlib.util.module_from_spec(spec) +spec.loader.exec_module(verify) + + +def main(): + states = verify.prefixes(verify.WORD) + if states != [0, 1, 3, 2, 6, 4, 12, 8, 0]: + raise SystemExit("prefix states changed") + if verify.budget(4, 4, 4) != 5 or verify.budget(6, 2, 4) != 9: + raise SystemExit("budgets changed") + bit_collisions, bit_even, bit_odd, trace = verify.collision_walk(verify.WORD, verify.bit0) + weight_collisions, weight_even, weight_odd, _ = verify.collision_walk(verify.WORD, verify.weight) + if (bit_collisions, bit_even, bit_odd) != (8, 6, 2): + raise SystemExit("bit-0 walk changed") + if (weight_collisions, weight_even, weight_odd) != (0, 4, 4): + raise SystemExit("weight walk changed") + crossed = next(index for index, value in enumerate(trace) if value > 5) + if crossed != 6 or trace[6] != 8: + raise SystemExit("the balanced budget is not crossed at the recorded step") + print("PASS_F7_BIT0_FALSE_PRUNE_TESTS groups=3") + + +if __name__ == "__main__": + main() diff --git a/research/f7-bit0-false-prune/verify.py b/research/f7-bit0-false-prune/verify.py new file mode 100644 index 0000000000..7ebe9fe80b --- /dev/null +++ b/research/f7-bit0-false-prune/verify.py @@ -0,0 +1,241 @@ +#!/usr/bin/env python3 +"""Reconstruct the 01021323 false prune and count it on a small domain. + +The pinned length-18 census groups prefix states by bit 0 and compares their +collision count with the balanced weight-parity budget. This check walks that +rule independently. It does not run a seven-label census or change kappa. +""" + +from math import comb +import hashlib +import json +from pathlib import Path + +ROOT = Path(__file__).resolve().parents[2] +PACKAGE = Path(__file__).resolve().parent +WORD = (0, 1, 0, 2, 1, 3, 2, 3) +DOMAINS = ((3, 6), (3, 8), (4, 8)) +MARKER = ( + "PASS_F7_BIT0_FALSE_PRUNE word=01021323 bit0_collisions=8 " + "balanced_budget=5 simple_false_prunes=0,0,6 no_new_kappa" +) + + +def fail(message): + raise SystemExit("FAIL_F7_BIT0_FALSE_PRUNE " + message) + + +def require(condition, message): + if not condition: + fail(message) + + +def sha256(path): + digest = hashlib.sha256() + with path.open("rb") as handle: + for block in iter(lambda: handle.read(1 << 20), b""): + digest.update(block) + return digest.hexdigest() + + +def budget(size, other, dimension): + """Even-collision allowance for one actual class split.""" + even_nonzero = (1 << (dimension - 1)) - 1 + return comb(size, 2) + comb(other, 2) - even_nonzero + + +def prefixes(word): + state = 0 + states = [0] + for label in word: + state ^= 1 << label + states.append(state) + return states + + +def universal(points, dimension): + covered = 0 + ordered = list(points) + for index, left in enumerate(ordered): + for right in ordered[index:]: + covered |= 1 << (left ^ right) + return covered.bit_count() == (1 << dimension) + + +def collision_walk(word, odd_class): + """Count new pair-sums the way the pinned census does, for one grouping.""" + even_points = [0] + odd_points = [] + even_support = odd_support = collisions = 0 + state = 0 + trace = [] + for index, label in enumerate(word): + successor = state ^ (1 << label) + closing = index == len(word) - 1 and successor == 0 + if closing: + added = 0 + elif odd_class(successor): + added = 0 + for point in odd_points: + added |= 1 << (successor ^ point) + fresh = (added & odd_support).bit_count() + odd_support |= added + odd_points.append(successor) + else: + added = 0 + for point in even_points: + added |= 1 << (successor ^ point) + fresh = (added & even_support).bit_count() + even_support |= added + even_points.append(successor) + if not closing: + collisions += fresh + state = successor + trace.append(collisions) + return collisions, len(even_points), len(odd_points), trace + + +def bit0(state): + return state & 1 + + +def weight(state): + return state.bit_count() & 1 + + +def even_words(dimension, length): + """Restricted-growth words in which every used label occurs evenly.""" + found = [] + letters = [0] * length + counts = [0] * dimension + + def walk(index, used): + if index == length: + if all(count % 2 == 0 for count in counts[:used]): + found.append(tuple(letters)) + return + for label in range(min(used + 1, dimension)): + letters[index] = label + counts[label] += 1 + walk(index + 1, used + 1 if label == used else used) + counts[label] -= 1 + + counts[0] = 1 + walk(1, 1) + return found + + +def domain_row(dimension, length): + allowance = budget(length // 2, length // 2, dimension) + universal_count = simple_count = false_prunes = weight_exceeded = 0 + for word in even_words(dimension, length): + states = prefixes(word) + if states[-1] != 0: + continue + points = set(states[:-1]) + if not universal(points, dimension): + continue + universal_count += 1 + if len(states[:-1]) != len(points): + continue + simple_count += 1 + bit_collisions, _, _, _ = collision_walk(word, bit0) + weight_collisions, even_size, odd_size, _ = collision_walk(word, weight) + if bit_collisions > allowance: + false_prunes += 1 + if weight_collisions > budget(even_size, odd_size, dimension): + weight_exceeded += 1 + return { + "n": dimension, + "length": length, + "universal": universal_count, + "simple_universal": simple_count, + "balanced_budget": allowance, + "simple_false_prunes": false_prunes, + "weight_budget_exceeded": weight_exceeded, + } + + +def authenticate(): + sources = json.loads((PACKAGE / "SOURCES.json").read_text(encoding="utf-8")) + pinned = {row["path"]: row for row in sources["files"] if row["usage"] == "input"} + expected = { + "research/universal-f7-singleton-seedb859517b/engine.py", + "research/universal-f7-singleton-seedb859517b/search.py", + "research/universal-f7-singleton-l20-seed06704c39/engine.py", + } + require(set(pinned) == expected, "input inventory changed") + texts = {} + for path, row in pinned.items(): + require(sha256(ROOT / path) == row["sha256"], "input drift " + path) + texts[path] = (ROOT / path).read_text(encoding="utf-8") + engine = texts["research/universal-f7-singleton-seedb859517b/engine.py"] + vendored = texts["research/universal-f7-singleton-l20-seed06704c39/engine.py"] + search = texts["research/universal-f7-singleton-seedb859517b/search.py"] + require(engine == vendored, "the length-20 package no longer vendors the same engine") + require("elif nq & 1:" in engine, "census no longer groups by bit 0") + require( + 'if budget is not None and st["coll"] + newcoll > budget:' in engine, + "census no longer prunes on the collision budget", + ) + require( + "r = cyclic_census(7, 18, budget=9, simple=True, prefix=pref)" in search, + "length-18 call changed", + ) + require( + "C(9,2) + C(9,2) - 63 = 9 (budget=9)" in search, + "length-18 budget justification changed", + ) + + +def evaluate(): + authenticate() + states = prefixes(WORD) + points = states[:-1] + require(states == [0, 1, 3, 2, 6, 4, 12, 8, 0], "prefix states changed") + require(len(points) == len(set(points)) == 8, "the eight nonclosing states are not distinct") + require(states[-1] == 0, "the word does not restore") + require(universal(points, 4), "the word is not universal on four labels") + require(sorted(WORD.count(label) for label in range(4)) == [2, 2, 2, 2], "label counts changed") + bit_collisions, bit_even, bit_odd, bit_trace = collision_walk(WORD, bit0) + weight_collisions, weight_even, weight_odd, weight_trace = collision_walk(WORD, weight) + balanced = budget(4, 4, 4) + actual_bit = budget(bit_even, bit_odd, 4) + require(bit_collisions == 8 and balanced == 5 and actual_bit == 9, "counterexample budgets changed") + require(weight_collisions == 0 and (weight_even, weight_odd) == (4, 4), "weight walk changed") + require(all(value <= balanced for value in weight_trace), "weight collisions exceed the balanced budget") + exceed = next(index for index, value in enumerate(bit_trace) if value > balanced) + rows = [domain_row(dimension, length) for dimension, length in DOMAINS] + require( + [(row["universal"], row["simple_false_prunes"]) for row in rows] == [(10, 0), (182, 0), (26, 6)], + "small-domain census changed", + ) + require(all(row["weight_budget_exceeded"] == 0 for row in rows), "a weight-parity budget also rejected a simple word") + return { + "word": list(WORD), + "prefix_states": states, + "prefix_set": sorted(set(points)), + "universal": True, + "weight_split": [weight_even, weight_odd], + "weight_collisions": weight_collisions, + "balanced_budget": balanced, + "bit0_split": [bit_even, bit_odd], + "bit0_collisions": bit_collisions, + "bit0_actual_budget": actual_bit, + "bit0_exceeds_balanced_at_index": exceed, + "predecessor_call": "cyclic_census(7, 18, budget=9, simple=True)", + "vendored_engine_same_text": True, + "domains": rows, + "no_new_kappa": True, + } + + +def main(): + observed = evaluate() + expected = json.loads((PACKAGE / "RESULT.json").read_text(encoding="utf-8")) + require(observed == expected, "RESULT.json does not match the execution: " + json.dumps(observed, sort_keys=True)) + print(MARKER) + + +if __name__ == "__main__": + main()