Research: cuts through time at block 4, no 3 in 10 and no 2 in 7 without address maps (no new κ)

research/complex-m4-time-unrolled-cuts/.gitattributes

@@ -0,0 +1,2 @@
+# Keep the package bytes exact: verify.py and SOURCES.json record the sha256 of the data files.
+* -text

research/complex-m4-time-unrolled-cuts/TASK.json

@@ -0,0 +1,91 @@
+{
+ "schema_version": 1,
+ "task_id": "scope-navigation",
+ "priority_revision": 8,
+ "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+ "original_card": {
+  "id": "scope-navigation",
+  "question": "Can one misleading historical-current claim or missing research cross-reference be corrected?",
+  "starting_points": [
+   "docs/research/current-status.md",
+   "docs/research/pr-ledger.md",
+   "certificates/selected-result.json"
+  ],
+  "methods": [
+   "Trace one confusing path from onboarding to its authoritative source.",
+   "Index one tightly related family of obstructions with explicit excluded and open hypotheses."
+  ],
+  "acceptance_gate": "Produce evidence-backed navigation, preserve historical records and avoid a duplicate global survey.",
+  "first_step": {
+   "command": [
+    "python3",
+    "-B",
+    "scripts/research_selected_baseline.py"
+   ],
+   "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+   "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.",
+   "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse."
+  },
+  "first_experiment": "Repair one confusing path or produce a scoped map of one related obstruction family.",
+  "bottleneck_link": "Clear navigation lowers entry cost for central research; a global survey without a concrete fix is not required.",
+  "allowed_variations": [
+   "One historical-current ambiguity or one bounded family index."
+  ],
+  "scope_change_triggers": [
+   "Rewriting frozen scientific packages just to change their historical wording."
+  ],
+  "overlap_terms": [
+   "current status",
+   "historical checkpoint",
+   "scope navigation"
+  ]
+ },
+ "scope_status": "changed",
+ "actual_scope": "One bounded family index at block 4: which small complex units the engine game without address maps excludes, and why the same rule cannot reach the engine game with address maps. A counting rule (the end-state chain rows, the cut-set bound of linear network coding applied to the program unrolled in time) is stated and argued by hand for the engine game without address maps (calls C_w, shifts, phases i^(z.x+c), rational mixing with scratch, copies and erasures). With it, stored certificates exclude every order of every 10-call shape for 3 arrays (121,951 certificates over the 80 orbits that plane rows allow; nothing below 10 passes plane rows) and every order of every 7-call shape for 2 arrays (3,098 certificates over 38 orbits). With address maps every direction is equivalent and the rule is false (checked by computer); a unit there needs a cross-frame addition or an end relabelling (argued by hand). The registered check builds the 35 x 35 plane matrices from their definitions, checks n0's 324 certificates and all 3,098 two-in-seven certificates exactly with coverage, recounts the 1,097 and 398 shapes and their orbits, and rejects corrupted files.",
+ "scope_change_reason": "The card's method 'Index one tightly related family of obstructions with explicit excluded and open hypotheses' fits, but the package also adds results that are not on main (the chain-row rule and the two exclusions in the game without address maps), so it is more than navigation. The game is stated in every claim, the earlier bounds (eumemic's certificate method, #288, and my block-4 bound, #4628) and the related hub work (block4-coordinate-face-tariff, #4855; the temporal cuts #2082 and #2090 and p104-cut-maxflow-audit, #2163; the coding-gap note #634) are credited, the withdrawn 3 in 10 (#4818) is disclosed, and the classical source of the rule (Ahlswede, Cai, Li and Yeung; Avestimehr, Diggavi and Tse) is named.",
+ "bottleneck_link": "A 3 in 10 at block 4 would save 1.32e-1 and a 2 in 7 would save 9.63e-2. This package removes both from the engine game without address maps and shows that any such unit in the engine game must use a cross-frame addition or an end relabelling, which narrows where a search should look; it does not change κ.",
+ "budget_minutes": 240,
+ "stop_rule": "Post results already public in my repository with a status no stronger than there; every certificate in the package re-checked by verify.py; every control rejected; no new search, reviewer round or Lean build for this package.",
+ "outcome": "negative-result",
+ "evidence": "verify.py --part main (standard library, about 1 s): the 15 call matrices and the target on the 35 planes from their definitions, each call -8(I - 2Q) with Q a rank-7 projection, one other shift character with the same ranks; two chains (45 < 48 and 47 < 48); n0's 324 certificates (all 3,628,800 orders) and the 3,098 two-in-seven certificates (5,040 orders for each of 38 shapes), each cost and right side recomputed exactly, coverage by non-nested suffixes and counting; sha256 of every data file. --part recount (about 4 s): plane rows at 1,524 sets leave 1,097 ten-call shapes in 80 orbits and none of 9 for W = 3, and 398 seven-call shapes in 38 orbits and none of 6 for W = 2, with the representatives equal to the data files. --part controls: six corrupted files or false claims, each rejected, and no plane-row violation by the plain program. Outside this package (author evidence in my repository): the other 79 ten-call certificate files, two independent checkers with coverage by counting and by listing every order, soundness tests on random and real programs, and the address-map checks.",
+ "author": "Jacob Sussman",
+ "ai_assistance": "Substantial AI assistance: I did this work with the help of AI agents (Anthropic's Claude). The model, the searches, the checkers, the arguments and the texts were written by the agents under my direction. Two AI reviewers checked the work with their own code. No independent human review of this package is claimed.",
+ "open_questions": [
+  {
+   "question": "Is there a 3 in 10 at block 4 in the engine game with a live array relabelled at the end and no cross-frame addition (route B; saving 1.32e-1)?",
+   "why_it_matters": "It is one of the two ways left for the most valuable block-4 unit for three arrays; the chain rule stays valid there with the target relabelled.",
+   "first_step": "Plane sets chosen for each relabelled target, then the chain search with right side sum_l rank R_K[G_l A, U_0^c]; first on 2 in 7, where pairs of relabellings are fewer.",
+   "blocked_by": "None."
+  },
+  {
+   "question": "Is there a rule that survives cross-frame additions and excludes 3 in 10 at block 4 (route A)?",
+   "why_it_matters": "The kept-subspace bound survives them but gives 41W/13 (9.46 for 3 arrays); of the rules built on pieces kept by all free steps, the symmetric part gives at least 7 calls for 3 arrays and constant chains on the 2,295 Lagrangian pieces give at most 15/8 calls per array. All of them allow 10 calls for 3 arrays.",
+   "first_step": "A rule with more structure than the pieces kept by every free step; a search would need a discrete choice of relative relabelling per addition.",
+   "blocked_by": "None."
+  },
+  {
+   "question": "Is there a 2 in 7 at block 4 in the engine game (9.63e-2)?",
+   "why_it_matters": "It is the smallest open shape; it is now excluded without address maps.",
+   "first_step": "The same two routes with W = 2.",
+   "blocked_by": "None."
+  },
+  {
+   "question": "Is there a 3 in 11 at block 4 without address maps (6.28e-2)?",
+   "why_it_matters": "It is the next shape the same rule could settle.",
+   "first_step": "The same chain search over the 11-call shapes that pass plane rows, with sets closed under each shape's symmetries.",
+   "blocked_by": "None."
+  },
+  {
+   "question": "Does the rule settle 3 in 10 when only the 24 bit permutations are free address maps?",
+   "why_it_matters": "Six pieces survive there, so it is a stepping stone between the two games.",
+   "first_step": "Rewrite the chain rows on the 6 pieces kept by bit permutations and rerun the search.",
+   "blocked_by": "None."
+  },
+  {
+   "question": "Is there a short proof in place of the 121,951 certificates?",
+   "why_it_matters": "Trust and explanation; the certificates explain little.",
+   "first_step": "Find a few row families, like 'n0 can never end with a two-bit call', that cover whole groups of shapes.",
+   "blocked_by": "None."
+  }
+ ]
+}

research/complex-m4-time-unrolled-cuts/VERIFY.json

@@ -0,0 +1,42 @@
+{
+ "schema_version": 1,
+ "status": "ready",
+ "python": "3.12",
+ "requirements": [],
+ "inputs": [],
+ "commands": [
+  {
+   "argv": [
+    "{python}",
+    "-B",
+    "{package}/verify.py",
+    "--part",
+    "main"
+   ],
+   "timeout_seconds": 120,
+   "checks": "Standard library, under 1 s and under 30 MB, no files written. Builds the 15 call matrices and the target on the 35 planes of Lambda^3(C^16) from their definitions (exact Gaussian integers); checks each call is -8(I - 2Q) with Q a rank-7 projection, the target is M1 M2 M4 M8, and one other shift character gives the same ranks; evaluates the scrambled-program chain of n0 (45 < 48) and the two-bit-ending chain (47 < 48); checks every certificate of data/n0_certs.txt (324; all 3,628,800 orders) and of data/two-in-seven/ (3,098; all 5,040 orders of each of 38 shapes) exactly, with coverage by non-nested suffixes and counting; checks the sha256 of every data file. Prints PASS_COMPLEX_M4_TIME_UNROLLED_CUTS_MAIN."
+  },
+  {
+   "argv": [
+    "{python}",
+    "-B",
+    "{package}/verify.py",
+    "--part",
+    "recount"
+   ],
+   "timeout_seconds": 120,
+   "checks": "About 4 s and under 40 MB. Plane rows at the 1,524 sets of data/cut_sets_and_images.txt leave 1,097 shapes of 10 directions for W = 3 (80 orbits under the 24 bit permutations, equal to data/ten-move-orbit-lists.txt; none of 9) and 398 of 7 for W = 2 (38 orbits, equal to data/two-in-seven/schedules.txt; none of 6). Prints PASS_COMPLEX_M4_TIME_UNROLLED_CUTS_RECOUNT."
+  },
+  {
+   "argv": [
+    "{python}",
+    "-B",
+    "{package}/verify.py",
+    "--part",
+    "controls"
+   ],
+   "timeout_seconds": 60,
+   "checks": "Under 1 s. Each must be rejected: n0's file with one certificate dropped (orders uncovered), with a cost lowered by one, with a chain whose last set grows; n0's certificates read with W = 2; n0's certificates applied to the plain 12-call shape; a two-in-seven file read with W = 1. The plain 12-call program must violate no plane row at the 324 bottom sets. Prints PASS_COMPLEX_M4_TIME_UNROLLED_CUTS_CONTROLS."
+  }
+ ]
+}