diff --git a/research/revisit-one-return-gap/README.md b/research/revisit-one-return-gap/README.md new file mode 100644 index 0000000000..c180014ca8 --- /dev/null +++ b/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. diff --git a/research/revisit-one-return-gap/RESULT.json b/research/revisit-one-return-gap/RESULT.json new file mode 100644 index 0000000000..68923132cf --- /dev/null +++ b/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 +} diff --git a/research/revisit-one-return-gap/SOURCES.json b/research/revisit-one-return-gap/SOURCES.json new file mode 100644 index 0000000000..3f0a9517f9 --- /dev/null +++ b/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" + } + ] +} diff --git a/research/revisit-one-return-gap/TASK.json b/research/revisit-one-return-gap/TASK.json new file mode 100644 index 0000000000..408ff533af --- /dev/null +++ b/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." + } + ] +} diff --git a/research/revisit-one-return-gap/VERIFY.json b/research/revisit-one-return-gap/VERIFY.json new file mode 100644 index 0000000000..1f242f3890 --- /dev/null +++ b/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." + } + ] +} diff --git a/research/revisit-one-return-gap/verify.py b/research/revisit-one-return-gap/verify.py new file mode 100644 index 0000000000..646bb2d512 --- /dev/null +++ b/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()