Record the bit-0 census false prune on 01021323

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.

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
+}

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"
+    }
+  ]
+}

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."
+    }
+  ]
+}

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."
+    }
+  ]
+}

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()