Record that revisit 1 forbids joint length-4 and length-6 returns.

research/revisit-one-return-gap/README.md

@@ -0,0 +1,81 @@
+# A revisit-1 length-22 word cannot carry both return lengths 4 and 6
+
+**Partial. No new exponent and no `f(7)` claim.**
+
+Open PR #3730 shows that every even length from 4 through 18 occurs as a
+prefix return for every positive length-22 split, using separate restored
+words. It does not say those lengths can share a word. At split `(11,10)`
+they cannot, for the pair 4 and 6.
+
+A restored length-22 word has 23 prefix positions and returns to the origin
+at the end. Its revisit count in the length-22 witness notes is
+`22 - |distinct prefixes|`. Split `(11,10)` has 21 distinct prefixes, so the
+revisit count is 1 and the 23 positions contain exactly two extra visits.
+
+Those two extras, with the ends identified, fall into one of two patterns:
+
+- the origin also occurs at one intermediate step `k`, and every other prefix
+  is unique, so the return lengths are `{k, 22-k, 22}`;
+- the origin occurs only at the two ends, and exactly one other prefix repeats
+  once, so the return lengths are `{d, 22}` for the distance `d` between that
+  pair.
+
+There are 231 such position patterns. None of them contains both distances
+4 and 6.
+Whenever a pattern meets the range 4 through 18 in two distances, those
+distances add to 22. A one-bit step flips Hamming-weight parity, so an actual
+hypercube return is even; that does not create a pattern containing both 4
+and 6.
+
+The two shapes are attained. One restored `(11,10)` word has return lengths
+exactly `{2, 20, 22}`. Another has exactly `{4, 18, 22}`.
+
+## Scope
+
+Original card: `census-pruning-audit`, priority revision 6, refined to this
+one-word gap after the existence cover. [TASK.json](TASK.json) records the
+scope change. [RESULT.json](RESULT.json) is the executed receipt.
+[SOURCES.json](SOURCES.json) pins the selected record. No selected frontier
+file changes.
+
+This is not a universal-word census and it does not decide `f(7)`. The
+existence cover of the eight even lengths remains the open length note; this
+package does not redo it.
+
+## Reproduce
+
+From the repository root, CPython 3.12:
+
+```sh
+python3.12 -B research/revisit-one-return-gap/verify.py
+python3.12 -B scripts/research_package.py --package research/revisit-one-return-gap
+```
+
+Expected marker:
+
+```text
+PASS_REVISIT_ONE_RETURN_GAP split=11,10 incompatible=4+6 patterns=231 no_new_kappa
+```
+
+The replay finishes in well under a second and uses the standard library only.
+
+## Open next questions
+
+Which pairs of even distances in 4 through 18 can share a restored word at
+revisit 2? Split `(11,9)` has 20 distinct prefixes, so the same counting
+allows one more repeated visit, and the revisit-1 obstruction does not apply.
+The first step is to enumerate the three-extra-visit patterns and test the
+pair 4 and 6. Nothing structural blocks that enumeration; this package stops
+at revisit 1.
+
+## Credit
+
+The positive length-22 splits and the revisit count are the length-22
+split-domain note. The length-2 witness with distances 2, 20 and 22, and the
+question of lengths 4 through 18, are the later witness notes; the existence
+cover is the open even-length note. The one-bit parity fact is the preceding
+return note. The prefix-walk model is Ross Richardson's. The corrected parity
+census that frames `f(7)` is Nicholas Stone's.
+
+Prepared by unpaidmoon with substantial Cursor agent assistance. No independent
+human review is claimed. Apache-2.0.

research/revisit-one-return-gap/RESULT.json

@@ -0,0 +1,8 @@
+{
+  "split": [11, 10],
+  "revisit": 1,
+  "patterns": 231,
+  "incompatible_pair": [4, 6],
+  "attained_sets": ["2,20,22", "4,18,22"],
+  "no_new_kappa": true
+}

research/revisit-one-return-gap/SOURCES.json

@@ -0,0 +1,18 @@
+{
+  "schema_version": 1,
+  "base_commit": "bb4bccbf42844d2801487450727c2f63e10d1d0f",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "input",
+      "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81",
+      "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5",
+      "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0"
+    }
+  ]
+}

research/revisit-one-return-gap/TASK.json

@@ -0,0 +1,66 @@
+{
+  "schema_version": 1,
+  "task_id": "census-pruning-audit",
+  "priority_revision": 6,
+  "base_commit": "bb4bccbf42844d2801487450727c2f63e10d1d0f",
+  "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": "Can one restored length-22 word of split (11,10) carry both prefix return lengths 4 and 6?",
+  "scope_change_reason": "The even-length existence cover is already in open PR #3730. The remaining one-word question at revisit 1 is this incompatibility, and it does not rerun that cover or the census.",
+  "bottleneck_link": "Revisit 1 limits which return lengths can be priced on the same length-22 word before a universal census.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after the revisit-1 patterns and the two attained shapes. Do not enumerate revisit 2 and do not claim f(7).",
+  "outcome": "completed",
+  "evidence": "All 231 closed coincidence patterns with exactly two extra visits miss the pair 4 and 6. Explicit restored words attain {2,20,22} and {4,18,22} at split (11,10).",
+  "author": "unpaidmoon",
+  "ai_assistance": "Substantial assistance from the Cursor coding agent in the pattern check, witnesses and writeup.",
+  "open_questions": [
+    {
+      "question": "Which pairs of even distances from 4 through 18 can share a restored word at revisit 2?",
+      "why_it_matters": "Split (11,9) has one more repeated visit than (11,10), so the revisit-1 gap does not decide whether 4 and 6 can be priced together there.",
+      "first_step": "Enumerate the three-extra-visit coincidence patterns and test the pair 4 and 6.",
+      "blocked_by": "Nothing structural; this package stops at revisit 1."
+    }
+  ]
+}

research/revisit-one-return-gap/VERIFY.json

@@ -0,0 +1,20 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "certificates/selected-result.json"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "Enumerate the 231 revisit-1 coincidence patterns, reject the pair 4 and 6, and check the two attained return sets."
+    }
+  ]
+}

research/revisit-one-return-gap/verify.py

@@ -0,0 +1,155 @@
+#!/usr/bin/env python3
+"""No restored (11,10) word has both a length-4 and a length-6 return.
+
+Revisit 1 leaves two extra prefix visits. The resulting return-length sets
+are enumerated exhaustively. Odd distances are excluded by weight parity.
+"""
+
+import hashlib
+import json
+from fractions import Fraction
+from pathlib import Path
+
+ROOT = Path(__file__).resolve().parents[2]
+PACKAGE = Path(__file__).resolve().parent
+MARKER = "PASS_REVISIT_ONE_RETURN_GAP split=11,10 incompatible=4+6 patterns=231 no_new_kappa"
+LABELS = 7
+LENGTH = 22
+SPLIT = (11, 10)
+KAPPA = Fraction(836330098538459, 500000000000000000)
+WITNESS_TWO = (5, 5, 4, 0, 4, 1, 4, 0, 4, 2, 0, 1, 0, 3, 0, 1, 0, 2, 0, 1, 0, 3)
+WITNESS_FOUR = (0, 1, 0, 1, 2, 3, 2, 4, 2, 3, 2, 5, 2, 3, 2, 4, 2, 3, 2, 6, 5, 6)
+
+
+def fail(message):
+    raise SystemExit("FAIL_REVISIT_ONE_RETURN_GAP " + 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 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"}
+    require(set(pinned) == {"certificates/selected-result.json"}, "input inventory changed")
+    for path, row in pinned.items():
+        require(sha256(ROOT / path) == row["sha256"], "input drift " + path)
+
+
+def positive_domain():
+    half = 1 << (LABELS - 1)
+    rows = []
+    for small in range(1, LENGTH):
+        for large in range(small, LENGTH):
+            budget = large * (large - 1) // 2 + small * (small - 1) // 2 - (half - 1)
+            excess = large * small - half
+            need = -((-excess) // 2) if excess > 0 else 0
+            upper = budget + budget * budget // 4 if budget > 0 else budget
+            if (
+                large <= LENGTH // 2
+                and small <= LENGTH // 2
+                and large * small >= half
+                and budget >= 0
+                and upper >= need
+            ):
+                rows.append((large, small))
+    return rows
+
+
+def prefixes(word):
+    state = 0
+    states = [0]
+    for label in word:
+        state ^= 1 << label
+        states.append(state)
+    return states
+
+
+def split_of(states):
+    unique = set(states)
+    even = sum(state.bit_count() % 2 == 0 for state in unique)
+    odd = len(unique) - even
+    return tuple(sorted((even, odd), reverse=True)), len(unique)
+
+
+def return_lengths(states):
+    return {
+        right - left
+        for left, earlier in enumerate(states)
+        for right in range(left + 1, len(states))
+        if states[right] == earlier
+    }
+
+
+def coincidence_patterns():
+    """Partitions of 23 prefix positions with exactly two extra visits and a closed origin."""
+    patterns = []
+    for middle in range(1, LENGTH):
+        patterns.append(frozenset({middle, LENGTH - middle, LENGTH}))
+    for left in range(1, LENGTH):
+        for right in range(left + 1, LENGTH):
+            patterns.append(frozenset({LENGTH, right - left}))
+    return patterns
+
+
+def evaluate():
+    authenticate()
+    selected = json.loads((ROOT / "certificates/selected-result.json").read_text(encoding="utf-8"))
+    require(Fraction(selected["kappa"]) == KAPPA, "the selected kappa moved")
+    for state in range(1 << LABELS):
+        for label in range(LABELS):
+            require((state ^ (1 << label)).bit_count() % 2 != state.bit_count() % 2, "a step kept the weight parity")
+    require(SPLIT in positive_domain(), "split (11,10) left the positive domain")
+    require(LENGTH - sum(SPLIT) == 1, "the split is no longer revisit 1")
+    patterns = coincidence_patterns()
+    require(len(patterns) == 231, "the coincidence inventory moved")
+    require(all(4 not in pattern or 6 not in pattern for pattern in patterns), "a pattern carries both 4 and 6")
+    for pattern in patterns:
+        interior = {distance for distance in pattern if 4 <= distance <= 18}
+        if len(interior) == 2:
+            left, right = sorted(interior)
+            require(left + right == LENGTH, "two interior distances do not complement")
+        require(len(interior) <= 2, "a revisit-1 pattern has three interior distances")
+    require(frozenset({4, 6, LENGTH}) not in patterns, "the forbidden pair was enumerated")
+    for word, expected in (
+        (WITNESS_TWO, frozenset({2, 20, 22})),
+        (WITNESS_FOUR, frozenset({4, 18, 22})),
+    ):
+        states = prefixes(word)
+        observed_split, unique = split_of(states)
+        lengths = return_lengths(states)
+        require(states[-1] == 0 and len(word) == LENGTH, "a witness is not restored")
+        require(observed_split == SPLIT and unique == sum(SPLIT), "a witness missed the split")
+        require(lengths == expected, "a witness return set moved")
+        broken = list(word)
+        broken[-1] = (broken[-1] + 1) % LABELS
+        require(prefixes(broken)[-1] != 0, "a broken closure stayed closed")
+    return {
+        "split": [11, 10],
+        "revisit": 1,
+        "patterns": len(patterns),
+        "incompatible_pair": [4, 6],
+        "attained_sets": ["2,20,22", "4,18,22"],
+        "no_new_kappa": True,
+    }
+
+
+def main():
+    observed = evaluate()
+    stored = json.loads((PACKAGE / "RESULT.json").read_text(encoding="utf-8"))
+    require(observed == stored, "RESULT.json does not match the execution")
+    print(MARKER)
+
+
+if __name__ == "__main__":
+    main()