diff --git a/research/f7-record-map/README.md b/research/f7-record-map/README.md new file mode 100644 index 0000000000..5ca2306d18 --- /dev/null +++ b/research/f7-record-map/README.md @@ -0,0 +1,130 @@ +# The f(7) records agree; a second engine at length 22 + +**Navigation index plus a complete second-engine replay of the length-22 census. No new bound, no κ, no +supplier or frontier change.** The model throughout is Ross Richardson's PR943 +abstract singleton prefix-walk model. Seven immutable sources, singleton +additions, paired readouts, eventual restoration. A restored word is universal +iff its prefix set `P` satisfies `P + P = F2^7`. + +## The question + +Item 5 of petalas's [consolidation handoff](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19230473) +says the records disagree on f(7). The two records are #3058, titled "f(7) = 24", +and `research/f7-independent-full-replay` (#3333), which says `{22,24}` and does +not cite #3058. + +**They do not disagree.** #3333 is a length-20 replay. It says it "does not +decide whether length 22 is attainable". Its `{22,24}` is a scope limit, not +a contrary finding. Length 22 is excluded on main by two routes that share no +search code. Every record below is `partially_reviewed` in +`docs/research/pr-ledger.json` at the base commit. Archival merge is not +scientific approval. + +## Record map + +| Step | Route | Records on main | Independent coverage | Still open | +|---|---|---|---|---| +| L ≤ 20 excluded, so f(7) ≥ 22 | census | #2973 (Nicholas Stone), corrected census | #3005 (Nick Petalas, separate C++ engine), #3333 (1337isnot1337, separate C engine) | none at this step; #2542/#2634/#2691 used the bit-0 prune and are retired (#4946, JoyboyBrian) | +| L ≤ 20 excluded | covering code | #3058 (conorholds) §1–2: `ell(7,2)=19` gives a 20-point cover floor, and the published 19-point classification gives L ≥ 24 for a 20-point cover | #3728 re-checks the `\|P\|=20` step. #3732 (James Reed) excludes two of its five representatives by a multiplicity count. | the two published results are imported, not re-derived | +| L = 22 excluded | covering code | #3058 §3 (21 distinct prefixes), §4 (patterns A and B via f(6)=16, f(5)=12), §5 (complete small-path search) | engine audits: capacity #3224, propagation #3244, domain #3261, search #3276, caller #3287. SAT proofs for 4 of the 77 B cases (#3360). | §3 is checked by #3058's own two implementations, but no separate audit package covers it on main. #3360 lists it as out of scope. Pattern A has #3058's own Python port and solver checks. The other 73 B cases rest on the single native search. | +| L = 22 excluded | census | split domain #3708, independently #3712; probes #3731 and #3818; closure #4221; receipt binding #4871 | before this package, every split ran on one engine (#3818's `union_census.c`). **This package adds a second engine for the splits below.** | #3899 (tiny-domain audit of the union prune) is open. Both engines share #3005's union-support bound and #3708's domain and symmetry. | +| L = 24 attained | witness | #1185 (Douglas Colkitt) Gray cycle; #2973's `UPPER-WITNESS.json` | `verify.py` checks `010201030102010345464546` directly | none | + +Consumers cite only #3058 for f(7) = 24: `research/eight-source-singleton-floor` +(#5234), `research/eight-source-lift-obstruction` (#5430) and +`research/seven-source-duo-21-calls` (#6005). They use only the value, so the +census route serves as well. It avoids the two imported literature results, but +it needs #3708's split domain and the pruning proofs of #2973, #3005 and #3818. + +#4221's second open question (re-derive the domain inside the verifier) is +already answered by #4871. Its first open question, a second engine at length +22, is what the next section addresses. + +## Second engine at length 22 + +`research/f7-union-support-audit/census.cpp` (#3005, Nick Petalas) is gated at +`L <= 20` only through `max_length`. `verify.py` rebuilds it from the pinned +bytes with exactly two changed lines: `max_length = 22` and the matching error +message. It uses #3005's compiler flags. + +The two engines are separately written but not mathematically independent. +#3818's `union_census.c` is #2973's `corrected_census.c` with #3005's +union-support bound ported in. That bound's proof (in #3005) is therefore a +premise of both engines, and a flaw in it would affect both. What the second +engine removes is the single implementation: state representation, traversal, +the other prunes and the sharding. The proof in #3005 is written for general +even L. Its small-domain oracle checks (L ≤ 12) do not touch the changed +constant. + +Controls, all rerun by the default `verify.py`: + +- **Unchanged at L ≤ 20.** On L=18 `(9,9)` and L=20 `(10,7)`, `(10,8)`, + `(9,9)`, every summary field equals #3005's `FULL.json`. +- **Depth-22 leaves work.** A capped n=6, L=22 `(11,11)` run finds hits. Every + hit is checked by direct XOR coverage as a simple restored universal word. +- **Fails closed.** A capped n=7 run exits 2 with `complete=false`. + +Results at n=7, L=22 (LOCAL-ONLY; full receipts in [RESULT.json](RESULT.json)): + +| Split | This engine: entered nodes | Hits | Status | Prior engine (nodes) | +|---|---:|---:|---|---| +| `(11,11)` | 37,567,052,539 | 0 | complete, exit 0 (3751 s wall) | #4221 cover sum 55,385,607,437 | +| `(11,10)` | 40,743,043,536 | 0 | complete, exit 0 (4188 s wall) | #4221 cover sum 52,957,641,635 | +| `(11,9)` | 11,942,611,230 | 0 | complete, exit 0 (1537 s wall) | #4221 cover sum 14,058,107,415 | +| `(10,10)` | 37,400,857,165 | 0 | complete, exit 0 (4117 s wall) | #4221 cover sum 44,378,511,529 | +| `(11,8)` | 973,631,241 | 0 | complete, exit 0 (130 s wall) | #3731 1,349,702,650 | +| `(10,9)` | 6,624,261,154 | 0 | complete, exit 0 (830 s wall) | #4221 cover sum 7,027,617,655 | +| `(11,7)` | 8,613,944 | 0 | complete, exit 0 (1 s wall) | #3731 8,784,744 | +| `(10,8)` | 238,010,457 | 0 | complete, exit 0 (32 s wall) | #3731 597,933,297 | +| `(9,9)` | 386,427,869 | 0 | complete, exit 0 (50 s wall) | #3818 388,563,293 | +| `(11,6)` | 1,020 | 0 | complete, exit 0 (0 s wall) | #4221 cover sum 2,247 | +| `(10,7)` | 699,412 | 0 | complete, exit 0 (0 s wall) | #4221 cover sum 700,909 | + +Entered-node counts track the #3731/#3818 node counts closely. `(9,9)` gives +386,427,869 here against 388,563,293. `(11,7)` gives 8,613,944 against +8,784,744. Throughput was about 7.5 M entered nodes per second per core on a +shared 10-core machine. + +**All eleven splits close on the second engine with zero hits.** Every census-route length-22 exclusion now rests on two separately written engines. The engines still share #3708's domain and symmetry premises. + +The census route still imports #3708's rotation symmetry, so only `s >= t` +runs. It also imports its four necessary conditions, as #4221 does. + +## Reproduce + +Requires Python 3.10+ and a C++20 compiler; no Python packages. + +```sh +python3 -I -B research/f7-record-map/verify.py # ~5 s +python3 -I -B research/f7-record-map/verify.py --splits 9:9,10:8 # ~1 min +python3 -I -B research/f7-record-map/verify.py --full --workers 8 # every completed split +python3 scripts/research_package.py --package research/f7-record-map --check-only +``` + +The default run authenticates every live input and checks each quoted sentence +of the record map against its pinned README. It also checks the witness and +the #4221 receipt closure (7 + 4 = 11 splits), then runs the controls above +and replays `(11,6)`, `(10,7)` and `(11,7)` exactly. + +## Open next questions + +1. **A tiny-domain audit of the union prune.** #3899 (open) does this at `(n,L)=(4,8)`. Both engines depend on that bound, so it is the main shared premise left. First step: review #3899. Blocked by: none. +2. **Audit #3058 §3, the 21-distinct-prefix case, separately.** #3058 checks it + with two implementations of its own. No separate audit package covers it + on main, and #3360 lists it as out of scope. First step: re-derive the + degree-four/degree-two walk structure and the 16 surviving classes from + `table6.json` without reading #3058's checkers. Blocked by: none. +3. **The remaining 73 pattern-B cases.** #3058 says its B exhaustion "rests + on this single native implementation". #3360's SAT translation covers 4 of + the 77. First step: run that translation on the next named template. + Blocked by: solver and proof-checking budget. + +## Credit + +Item 5 and the question are petalas's. The engine is Nick Petalas's (#3005), +unchanged except for the length gate. The routes belong to conorholds (#3058), +Nicholas Stone (#2973), Nick Petalas (#3708, #3728, #3731, #3818, #4221, engine +audits), James Reed (jwr404, #3712, #3732), codyw912 (#4871), 1337isnot1337 (#3333, #3899), +commdata2338 (#3224), krzysztofwojt (#3261), JoyboyBrian (#4946), Douglas +Colkitt (#1185) and Ross Richardson (#943). Prepared by Claude Opus 5.5 for +JosieElliston; see TASK.json for the AI-assistance disclosure. Apache-2.0. diff --git a/research/f7-record-map/RESULT.json b/research/f7-record-map/RESULT.json new file mode 100644 index 0000000000..73e199b876 --- /dev/null +++ b/research/f7-record-map/RESULT.json @@ -0,0 +1,552 @@ +{ + "model": "PR943 abstract singleton prefix-walk model (Ross Richardson): seven immutable sources, singleton additions, paired readouts, eventual restoration; a restored word is universal iff P+P = F2^7", + "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419", + "item5_resolution": "No contradiction. #3333 (research/f7-independent-full-replay) is a length-20 replay and says it does not search length 22; its {22,24} is a scope limit. Length 22 is excluded on main by two routes that share no search code: #3058's covering-code argument and the census chain #2973 -> #3708 -> #3731/#3818 -> #4221, bound to its domain by #4871. Every record involved is partially_reviewed in the ledger at the base commit.", + "record_map": [ + { + "step": "L <= 20 excluded (f(7) >= 22), census route", + "status": "corroborated by three separately written engines", + "prs": [ + 2973, + 3005, + 3333 + ], + "retired": "#2542 (L18), #2634 (partial L20), #2691 ((10,10) L20) used the bit-0 prune; #4946 classifies them as retired with replacement evidence", + "sources": [ + { + "path": "research/f7-weight-parity-census-correction/README.md", + "quotes": [ + "**`22 <= f(7) <= 24`**" + ] + }, + { + "path": "research/f7-union-support-audit/README.md", + "quotes": [ + "this corroborates `22 <= f(7) <= 24`" + ] + }, + { + "path": "research/f7-independent-full-replay/README.md", + "quotes": [ + "The full result independently reproduces the lower bound `f(7) >= 22`", + "this work does not decide whether length 22 is attainable" + ] + }, + { + "path": "research/census-prune-source-impact/README.md", + "quotes": [ + "no exclusion that the current f(7) line relies on uses the faulty rule" + ] + } + ] + }, + { + "step": "L <= 20 excluded (f(7) >= 22), covering-code route", + "status": "imports two published results (Struik ell(7,2)=19; Davydov-Marcugini-Pambianco classification); |P|=20 step independently re-checked by #3728", + "prs": [ + 3058, + 3728, + 3732 + ], + "sources": [ + { + "path": "research/connector-covering-code/README.md", + "quotes": [ + "Hence **f(7) >= 22 follows from sections 1-2 alone**, with no word census." + ] + }, + { + "path": "research/f7-l22-confinement-audit/README.md", + "quotes": [ + "**Step audited: `|P| = 20` is impossible.**" + ] + } + ] + }, + { + "step": "L = 22 excluded, covering-code route (#3058 sections 3-5)", + "status": "section 3 (21 distinct prefixes) is checked by #3058's own two implementations, with no separate audit package on main (#3360 lists it as out of scope); sections 4-5 engine audited piecewise; pattern A corroborated by #3058's own Python port and solver checks; 4 of 77 pattern-B cases have independent SAT proofs, the rest rest on the single native search", + "prs": [ + 3058, + 3224, + 3244, + 3261, + 3276, + 3287, + 3360 + ], + "sources": [ + { + "path": "research/connector-covering-code/README.md", + "quotes": [ + "Thus a 22-step candidate must have **22 distinct prefixes: a simple cycle**.", + "Both checkers exhaust all **234 characters and 2,808 structural branches**.", + "The pattern A exclusion is corroborated by an independent Python port and solver checks; the pattern B exhaustion rests on this single native implementation" + ] + }, + { + "path": "research/connector-capacity-parity-audit/README.md", + "quotes": [ + "necessary condition for a simple restored universal word" + ] + }, + { + "path": "research/connector-path-propagation-audit/README.md", + "quotes": [ + "No defect was found in this scope." + ] + }, + { + "path": "research/connector-domain-completeness/README.md", + "quotes": [ + "It does not certify a completed search or the full `f(7)=24` claim." + ] + }, + { + "path": "research/connector-search-exhaustion-audit/README.md", + "quotes": [ + "No source defect was found in this scope." + ] + }, + { + "path": "research/connector-caller-exhaustion-audit/README.md", + "quotes": [ + "No source defect was found within this scope." + ] + }, + { + "path": "research/connector-b-occupancy-sat/README.md", + "quotes": [ + "The other 73 B cases were not run with this encoding", + "the 21-prefix reduction, all 77 B cases" + ] + } + ] + }, + { + "step": "L = 22 excluded, census route", + "status": "eleven-split domain derived twice (#3708, #3712) and re-derived by #4871; every split closed by one engine (#3818 union_census.c); this package adds a second engine (#3005 census.cpp, gate lifted) for the splits listed in second_engine_l22", + "prs": [ + 3708, + 3712, + 3731, + 3818, + 4221, + 4871 + ], + "pending": "#3899 (tiny-domain audit of the union prune) is open", + "sources": [ + { + "path": "research/f7-l22-split-domain/README.md", + "quotes": [ + "leave **11 split representatives at length 22**" + ] + }, + { + "path": "research/l22-split-domain/README.md", + "quotes": [ + "# Eleven length-22 splits survive" + ] + }, + { + "path": "research/f7-l22-census-probe/README.md", + "quotes": [ + "**`(11,7)`, `(10,8)` and `(11,8)` are finite" + ] + }, + { + "path": "research/f7-l22-union-census/README.md", + "quotes": [ + "new finite split exclusion" + ] + }, + { + "path": "research/f7-l22-deep-shard-census/README.md", + "quotes": [ + "**`f(7) = 24` inside PR943's prefix-walk model**", + "#3005's separately implemented C++ census has not been run at length 22." + ] + }, + { + "path": "research/f7-l22-receipt-domain/README.md", + "quotes": [ + "derives **eleven** representatives" + ] + } + ] + }, + { + "step": "L = 24 attained", + "status": "witness checked directly here", + "prs": [ + 1185, + 2973 + ], + "sources": [] + } + ], + "l22_domain": { + "source": "#3708 table, as listed in research/f7-l22-deep-shard-census/README.md", + "splits": [ + [ + 11, + 11 + ], + [ + 11, + 10 + ], + [ + 11, + 9 + ], + [ + 10, + 10 + ], + [ + 11, + 8 + ], + [ + 10, + 9 + ], + [ + 11, + 7 + ], + [ + 10, + 8 + ], + [ + 9, + 9 + ], + [ + 11, + 6 + ], + [ + 10, + 7 + ] + ], + "excluded_by_3731_3818": [ + [ + 11, + 7 + ], + [ + 10, + 8 + ], + [ + 11, + 8 + ], + [ + 9, + 9 + ] + ] + }, + "second_engine_l22": { + "engine": "research/f7-union-support-audit/census.cpp (#3005, Nick Petalas) with max_length 20 -> 22 and its error message; no other change", + "engine_sha256": "88f4a6a2196e60c55d66d992d69a4086ce6a9e76f99326241211f5bdda4cc695", + "compiler": "Apple clang 21.0.0, flags as #3005 verify.py (-std=c++20 -O3 ... -Werror)", + "environment": "local macOS arm64, 10 cores shared with other sessions; LOCAL-ONLY evidence until replayed", + "symmetry_premise": "#3708 rotation symmetry: only representatives s >= t are run", + "runs": [ + { + "n": 7, + "length": 22, + "split": [ + 11, + 11 + ], + "prune": true, + "cap": 0, + "complete": true, + "attempts": 262967842859, + "entered": 37567052539, + "candidate_leaves": 0, + "hits": 0, + "restoration_prunes": 127606738457, + "size_prunes": 31908107595, + "same_prunes": 64005526587, + "cross_prunes": 1880417682 + }, + { + "n": 7, + "length": 22, + "split": [ + 11, + 10 + ], + "prune": true, + "cap": 0, + "complete": true, + "attempts": 285196543267, + "entered": 40743043536, + "candidate_leaves": 0, + "hits": 0, + "restoration_prunes": 114662362937, + "size_prunes": 36277910836, + "same_prunes": 91780027840, + "cross_prunes": 1733198119 + }, + { + "n": 7, + "length": 22, + "split": [ + 11, + 9 + ], + "prune": true, + "cap": 0, + "complete": true, + "attempts": 83593730999, + "entered": 11942611230, + "candidate_leaves": 0, + "hits": 0, + "restoration_prunes": 25194325475, + "size_prunes": 11284193423, + "same_prunes": 33454203834, + "cross_prunes": 1718397038 + }, + { + "n": 7, + "length": 22, + "split": [ + 10, + 10 + ], + "prune": true, + "cap": 0, + "complete": true, + "attempts": 261789060244, + "entered": 37400857165, + "candidate_leaves": 0, + "hits": 0, + "restoration_prunes": 82624190942, + "size_prunes": 34567494590, + "same_prunes": 105634229919, + "cross_prunes": 1562287629 + }, + { + "n": 7, + "length": 22, + "split": [ + 11, + 8 + ], + "prune": true, + "cap": 0, + "complete": true, + "attempts": 6814862965, + "entered": 973631241, + "candidate_leaves": 0, + "hits": 0, + "restoration_prunes": 961722461, + "size_prunes": 1131773947, + "same_prunes": 3267781048, + "cross_prunes": 479954269 + }, + { + "n": 7, + "length": 22, + "split": [ + 10, + 9 + ], + "prune": true, + "cap": 0, + "complete": true, + "attempts": 46363380480, + "entered": 6624261154, + "candidate_leaves": 0, + "hits": 0, + "restoration_prunes": 8140196900, + "size_prunes": 6882799870, + "same_prunes": 24446502258, + "cross_prunes": 269620299 + }, + { + "n": 7, + "length": 22, + "split": [ + 11, + 7 + ], + "prune": true, + "cap": 0, + "complete": true, + "attempts": 60244610, + "entered": 8613944, + "candidate_leaves": 0, + "hits": 0, + "restoration_prunes": 1076222, + "size_prunes": 11556541, + "same_prunes": 17596821, + "cross_prunes": 21401083 + }, + { + "n": 7, + "length": 22, + "split": [ + 10, + 8 + ], + "prune": true, + "cap": 0, + "complete": true, + "attempts": 1665262768, + "entered": 238010457, + "candidate_leaves": 0, + "hits": 0, + "restoration_prunes": 92523122, + "size_prunes": 277797425, + "same_prunes": 1038642254, + "cross_prunes": 18289511 + }, + { + "n": 7, + "length": 22, + "split": [ + 9, + 9 + ], + "prune": true, + "cap": 0, + "complete": true, + "attempts": 2702735781, + "entered": 386427869, + "candidate_leaves": 0, + "hits": 0, + "restoration_prunes": 138219740, + "size_prunes": 426032099, + "same_prunes": 1751975903, + "cross_prunes": 80171 + }, + { + "n": 7, + "length": 22, + "split": [ + 11, + 6 + ], + "prune": true, + "cap": 0, + "complete": true, + "attempts": 6900, + "entered": 1020, + "candidate_leaves": 0, + "hits": 0, + "restoration_prunes": 0, + "size_prunes": 1602, + "same_prunes": 0, + "cross_prunes": 4279 + }, + { + "n": 7, + "length": 22, + "split": [ + 10, + 7 + ], + "prune": true, + "cap": 0, + "complete": true, + "attempts": 4873766, + "entered": 699412, + "candidate_leaves": 0, + "hits": 0, + "restoration_prunes": 0, + "size_prunes": 919828, + "same_prunes": 3254527, + "cross_prunes": 0 + } + ], + "timing_local_only": [ + { + "split": [ + 11, + 11 + ], + "wall_seconds": 3751 + }, + { + "split": [ + 11, + 10 + ], + "wall_seconds": 4188 + }, + { + "split": [ + 11, + 9 + ], + "wall_seconds": 1537 + }, + { + "split": [ + 10, + 10 + ], + "wall_seconds": 4117 + }, + { + "split": [ + 11, + 8 + ], + "wall_seconds": 130 + }, + { + "split": [ + 10, + 9 + ], + "wall_seconds": 830 + }, + { + "split": [ + 11, + 7 + ], + "wall_seconds": 1 + }, + { + "split": [ + 10, + 8 + ], + "wall_seconds": 32 + }, + { + "split": [ + 9, + 9 + ], + "wall_seconds": 50 + }, + { + "split": [ + 11, + 6 + ], + "wall_seconds": 0 + }, + { + "split": [ + 10, + 7 + ], + "wall_seconds": 0 + } + ] + } +} diff --git a/research/f7-record-map/SOURCES.json b/research/f7-record-map/SOURCES.json new file mode 100644 index 0000000000..587e2dcb0b --- /dev/null +++ b/research/f7-record-map/SOURCES.json @@ -0,0 +1,144 @@ +{ + "schema_version": 1, + "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/census-prune-source-impact/README.md", + "usage": "input", + "git_blob": "e036e5381d164bd8710d61ac6e8722d3bb2494c5", + "sha256": "cc8306b9a06a78f211eebc092fb84b0304d06826628481562cde56eddfd3b801" + }, + { + "path": "research/connector-b-occupancy-sat/README.md", + "usage": "input", + "git_blob": "f5696baba3b616756f4fd6db282b8c1fb922d84c", + "sha256": "711b9dc1a0f0236364806bb4f9980d21575a5e43b942878c25128b9425b5a36c" + }, + { + "path": "research/connector-caller-exhaustion-audit/README.md", + "usage": "input", + "git_blob": "da5d832836decfea1ca710f2d9b4798baa35841a", + "sha256": "2c506286f3d4ffbfe4b124ff599b17c305d3cdc8adf73ab3764b472170d827bb" + }, + { + "path": "research/connector-capacity-parity-audit/README.md", + "usage": "input", + "git_blob": "11e76c254bb126124ad6267f5c6c23449864dce9", + "sha256": "838b08c5f59ea6da9f90699ee839bb4673b864ea4b21d3b29ba8fbd061eae156" + }, + { + "path": "research/connector-covering-code/README.md", + "usage": "input", + "git_blob": "c194503e34e43988d5f83fec70a6f94e89e3db5d", + "sha256": "35252e16e58481df87fc7ac3eb7326bf87e991f9fd8f7e30d14716c16f2152e4" + }, + { + "path": "research/connector-domain-completeness/README.md", + "usage": "input", + "git_blob": "dc58535f171594102bcc9d64ad2b1a76a4655817", + "sha256": "427374332eb28d7737ad5614527903cf957505256e0a33ae0c1c61a9f43ec6ef" + }, + { + "path": "research/connector-path-propagation-audit/README.md", + "usage": "input", + "git_blob": "fb25d5392b37105f934fa47a4396be3938485b09", + "sha256": "35d1161ca272047e428e38dc291cf76780427d21a9e76c743b8f05f8f01353d7" + }, + { + "path": "research/connector-search-exhaustion-audit/README.md", + "usage": "input", + "git_blob": "1be743a10cfa6faa006f8d30f75d5e9723795243", + "sha256": "5b2a087f0fe5ab3db726ec1002479f0fe9ca19cd903a5e5f38a0063474b84e68" + }, + { + "path": "research/f7-independent-full-replay/README.md", + "usage": "input", + "git_blob": "7bb4d24e5d699e13d579259f7ffd852971aff16c", + "sha256": "ce688aa1712884958b0f910e769e6b467d7e908a99560efe1d852ee0d7b51fbe" + }, + { + "path": "research/f7-l22-census-probe/README.md", + "usage": "input", + "git_blob": "3820303ebb11208adee9489cace474c69a7c0e7b", + "sha256": "ec7184ccb27e1adf09cd937701bafd69a590906c5c169f5fedea48736efd32f6" + }, + { + "path": "research/f7-l22-confinement-audit/README.md", + "usage": "input", + "git_blob": "f90b6cd79cbd48aa5ce13de592aca34656e7ad3a", + "sha256": "e1242b189d4cef1aeeef457a0fd0142916b84f16e0913a973f86c8a13a2d2ddf" + }, + { + "path": "research/f7-l22-deep-shard-census/README.md", + "usage": "input", + "git_blob": "073e240af36bdd9ecf3ba5b7ab7bf6f1d3f933fc", + "sha256": "abc753bb54116e2ab5d65a1aae952a694766860f93115c63ea08152eddca68ec" + }, + { + "path": "research/f7-l22-deep-shard-census/RESULT.json", + "usage": "input", + "git_blob": "baf89975f1e7821ad37c952a234801092f37de8d", + "sha256": "a50770ce1c7de12438c0463bc2d2d47bbabfddfa9b3a0ec76bb60bdbf5b320ea" + }, + { + "path": "research/f7-l22-receipt-domain/README.md", + "usage": "input", + "git_blob": "2346bd0100b540045fa35d1271007e9733174e21", + "sha256": "ff04b6edb4dcd1d70ef8ae961d92e7886ebd5bcd2a10c7aad7d5fec616274dbc" + }, + { + "path": "research/f7-l22-split-domain/README.md", + "usage": "input", + "git_blob": "949fcf03f5d59fae90d26f5dca44c597d920d9ab", + "sha256": "d503e26c0d3bcbf09c66c0e4ff689382717e1c1c5b67cc98923394173a26a9b5" + }, + { + "path": "research/f7-l22-union-census/README.md", + "usage": "input", + "git_blob": "7fdb9c2a4cc84fdee577bad15263fbfd0a9f6687", + "sha256": "d5b490a7c55a74f7be571655530018db49689cd7207a28b9e3ea9c9b2c8b779c" + }, + { + "path": "research/f7-union-support-audit/README.md", + "usage": "input", + "git_blob": "2c913f603f4190a15eda7fbe3def58524e0826dd", + "sha256": "41eb7cfb56c593482fe1654c136ea755d780aa94d23075e255727b326739784a" + }, + { + "path": "research/f7-weight-parity-census-correction/README.md", + "usage": "input", + "git_blob": "0221748ce35d4a2dc6ee5ce61be210eb34a2ea83", + "sha256": "9bc7867ccfa97a682e4683052647d4bf8f191da5a219271f87d3e0a10de1446a" + }, + { + "path": "research/l22-split-domain/README.md", + "usage": "input", + "git_blob": "58b1ad7a335259de8824577262d34d441cab1f25", + "sha256": "2c6df655c75ef39bf80fb8870d2534b318d63892c1bfeb133dd5fe6211eb3f7e" + }, + { + "path": "research/f7-union-support-audit/census.cpp", + "usage": "input", + "git_blob": "5b290af8c8dd74f0b5a8ad0aec9bf2d55492507d", + "sha256": "3cd2c77fdb613e0463148265d9be084bcaa871f0a2c6c40ae3d94fea27c06949" + }, + { + "path": "research/f7-union-support-audit/FULL.json", + "usage": "input", + "git_blob": "4399bff28be91c10d87747bc2780e7beefa55512", + "sha256": "a31b976d9bd6edba2b2281a0843790f79cb85ba3868a9894204a794a444afa7a" + } + ] +} diff --git a/research/f7-record-map/TASK.json b/research/f7-record-map/TASK.json new file mode 100644 index 0000000000..1b6810993f --- /dev/null +++ b/research/f7-record-map/TASK.json @@ -0,0 +1,73 @@ +{ + "schema_version": 1, + "task_id": "scope-navigation", + "priority_revision": 8, + "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419", + "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": "Map the f(7) records in PR943's prefix-walk model (item 5 of petalas's consolidation handoff): per length step, the routes, independent coverage and open obligations. Extended with a complete second-engine replay of the length-22 census (#4221/#4871 open question 1), using #3005's engine with only its length gate lifted.", + "scope_change_reason": "The map identified the single-engine dependency of the census route as its main open obligation, and the blocker recorded by #4221 (#3005's engine gated at L<=20, throughput unmeasured) turned out to be a two-line constant change. Running it settles that blocker, so the extension stayed inside the same family index.", + "bottleneck_link": "Side result for navigation: f(7) is a finite connector-model value used by #5234, #5430 and #6005, not a \u03ba input. Clear status stops sessions from reopening a settled question, and it names the precise open steps.", + "budget_minutes": 60, + "stop_rule": "Stop at the session budget; report any split not finished as unfinished, not excluded. All eleven finished (the three heaviest in background after the session, 3751-4188 s each).", + "outcome": "completed", + "evidence": "verify.py: pinned inputs, 21 quoted scope sentences against their READMEs, the length-24 witness by direct XOR, #4221 receipt closure (7+4=11 splits), lifted-engine controls (L18/L20 exact equality with #3005 FULL.json, n=6 L22 positive control, cap fail-closed), exact replay of completed L22 splits. All eleven L22 splits complete with zero hits on the lifted engine. The full L22 runs are local-only receipts in RESULT.json.", + "author": "JosieElliston (Claude Opus 5.5 session)", + "ai_assistance": "Prepared by Claude Opus 5.5 (Anthropic) in Claude Code for JosieElliston, in an unattended overnight session. No human review.", + "open_questions": [ + { + "question": "Does #3899's tiny-domain audit of the union-support prune hold up?", + "why_it_matters": "Both length-22 engines depend on #3005's union-support bound, so it is the main premise they share.", + "first_step": "Review open PR #3899 at (n,L)=(4,8).", + "blocked_by": "none" + }, + { + "question": "Does a separate audit confirm #3058 section 3 (the 21-distinct-prefix case)?", + "why_it_matters": "It is checked only by #3058's own two implementations; no separate audit package covers it and #3360 lists it as out of scope.", + "first_step": "Re-derive the walk structure and the 16 surviving classes from research/connector-covering-code/table6.json without reading #3058's checkers.", + "blocked_by": "none" + }, + { + "question": "Can the remaining 73 pattern-B cases get independent proofs?", + "why_it_matters": "#3058 states its B exhaustion rests on a single native implementation; #3360 proves 4 of 77 by SAT.", + "first_step": "Apply #3360's SAT translation to the next named B template.", + "blocked_by": "solver and proof-checking budget" + } + ] +} diff --git a/research/f7-record-map/VERIFY.json b/research/f7-record-map/VERIFY.json new file mode 100644 index 0000000000..173a2c8550 --- /dev/null +++ b/research/f7-record-map/VERIFY.json @@ -0,0 +1,55 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/census-prune-source-impact/README.md", + "research/connector-b-occupancy-sat/README.md", + "research/connector-caller-exhaustion-audit/README.md", + "research/connector-capacity-parity-audit/README.md", + "research/connector-covering-code/README.md", + "research/connector-domain-completeness/README.md", + "research/connector-path-propagation-audit/README.md", + "research/connector-search-exhaustion-audit/README.md", + "research/f7-independent-full-replay/README.md", + "research/f7-l22-census-probe/README.md", + "research/f7-l22-confinement-audit/README.md", + "research/f7-l22-deep-shard-census/README.md", + "research/f7-l22-deep-shard-census/RESULT.json", + "research/f7-l22-receipt-domain/README.md", + "research/f7-l22-split-domain/README.md", + "research/f7-l22-union-census/README.md", + "research/f7-union-support-audit/FULL.json", + "research/f7-union-support-audit/README.md", + "research/f7-union-support-audit/census.cpp", + "research/f7-weight-parity-census-correction/README.md", + "research/l22-split-domain/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Input pins; 21 quoted scope sentences of the record map against their pinned READMEs; length-24 witness by direct XOR; #4221 receipt plus #3731/#3818 close the eleven-split #3708 domain; #3005 engine rebuilt with exactly two changed lines; L18/L20 summaries equal #3005 FULL.json; capped n=6 L22 positive control with every hit checked directly; capped n=7 run fails closed; exact replay of L22 splits (11,6), (10,7), (11,7). Requires a C++20 compiler." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py", + "--splits", + "9:9,10:8", + "--workers", + "2" + ], + "timeout_seconds": 300, + "checks": "Same checks, then exact uncapped replay of L22 splits (9,9) and (10,8) on the lifted #3005 engine (about 6.2e8 entered nodes)." + } + ] +} diff --git a/research/f7-record-map/verify.py b/research/f7-record-map/verify.py new file mode 100644 index 0000000000..f42efd9801 --- /dev/null +++ b/research/f7-record-map/verify.py @@ -0,0 +1,225 @@ +#!/usr/bin/env python3 +"""Check the f(7) record map and the second-engine length-22 census. + +Default mode (well under two minutes): + +1. Every live input matches its SHA256 pin in SOURCES.json. +2. Every quoted scope sentence in RESULT.json's record map occurs in the + pinned README it is attributed to (whitespace-normalized), so the map + fails closed if a cited record changes. This grounds the quotes only; the + map's summaries around them are prose for a reviewer to check. +3. The length-24 witness is restored, uses all seven labels and is universal + (P + P = F2^7); a direct XOR check, not a census. +4. The #4221 receipt summary has seven complete zero-hit splits, and with the + #3731 and #3818 exclusions they are exactly the eleven-split #3708 domain. + Shard rows are not replayed here; #4221's own verifier does that. +5. Second engine: #3005's census.cpp is rebuilt with exactly one textual + change (max_length 20 -> 22, plus its error message). Controls: the L=18 + and three L=20 cases equal #3005's FULL.json in every field; a capped + n=6, L=22 run finds hits and each hit is checked by direct XOR coverage; + a capped n=7 run exits 2 with complete=false. Then the cheap n=7, L=22 + splits are replayed and must equal RESULT.json in every field. + +--full replays every n=7, L=22 split that RESULT.json records as complete; +splits recorded as unfinished are not excluded and are not run. --splits +replays named splits and fails if one has no complete receipt. Wall times +are in RESULT.json (timing_local_only). Requires a C++20 compiler. + +JosieElliston, Claude Opus 5.5 session. Apache-2.0. +""" + +import argparse +import concurrent.futures +import hashlib +import json +import os +import re +import subprocess +import sys +import tempfile +from pathlib import Path + +ROOT = Path(__file__).resolve().parents[2] +PACKAGE = Path(__file__).resolve().parent +MARKER = "PASS_F7_RECORD_MAP" +ENGINE = "research/f7-union-support-audit/census.cpp" +FULL = "research/f7-union-support-audit/FULL.json" +DEEP = "research/f7-l22-deep-shard-census/RESULT.json" +FLAGS = ["-std=c++20", "-O3", "-Wall", "-Wextra", "-Wpedantic", "-Wconversion", + "-Wsign-conversion", "-Wshadow", "-Werror"] +EDITS = [ + ("constexpr int max_length = 20;", "constexpr int max_length = 22;"), + ("even 2n<=L<=20", "even 2n<=L<=22"), +] +WITNESS = "010201030102010345464546" +QUICK_L22 = [(11, 6), (10, 7), (11, 7)] +L20_CONTROLS = [(18, 9, 9), (20, 10, 7), (20, 10, 8), (20, 9, 9)] + + +def fail(message): + raise SystemExit("FAIL_F7_RECORD_MAP " + message) + + +def require(condition, message): + if not condition: + fail(message) + + +def sha256(path): + return hashlib.sha256(path.read_bytes()).hexdigest() + + +def authenticate(): + sources = json.loads((PACKAGE / "SOURCES.json").read_text(encoding="utf-8")) + rows = [row for row in sources["files"] if row["usage"] == "input"] + require(len(rows) >= 20, "too few live inputs") + for row in rows: + require(sha256(ROOT / row["path"]) == row["sha256"], "pin mismatch " + row["path"]) + return {row["path"] for row in rows} + + +def normalized(text): + return re.sub(r"\s+", " ", text).strip() + + +def check_map(result, pinned): + rows = result["record_map"] + quotes = 0 + for row in rows: + for source in row["sources"]: + path = source["path"] + require(path in pinned, "map cites an unpinned file " + path) + text = normalized((ROOT / path).read_text(encoding="utf-8")) + for quote in source["quotes"]: + require(normalized(quote) in text, f"quote not in {path}: {quote[:60]}") + quotes += 1 + return len(rows), quotes + + +def universal(word, n): + state, prefixes, counts = 0, [], [0] * n + for ch in word: + label = int(ch) + prefixes.append(state) + state ^= 1 << label + counts[label] += 1 + restored = state == 0 and all(c > 0 and c % 2 == 0 for c in counts) + sums = {a ^ b for a in prefixes for b in prefixes} + return restored, len(sums) == 1 << n, len(set(prefixes)) + + +def check_witness(): + restored, covered, distinct = universal(WITNESS, 7) + require(len(WITNESS) == 24 and restored and covered, "length-24 witness") + require(not universal(WITNESS[:-2], 7)[0], "a truncated witness must not be restored") + # Negative control: drop label 6 entirely; the prefix set loses a coordinate. + restored, covered, _ = universal(WITNESS.replace("6", ""), 7) + require(not covered, "a word missing a label must not be universal") + return distinct + + +def check_deep_receipt(result): + deep = json.loads((ROOT / DEEP).read_text(encoding="utf-8")) + closed = set() + for row in deep["splits"]: + require(row["complete"] and row["hits"] == 0 and not row["hit_words"], "deep receipt row") + closed.add(tuple(row["split"])) + require(len(closed) == 7, "deep receipt split count") + domain = {tuple(s) for s in result["l22_domain"]["splits"]} + earlier = {tuple(s) for s in result["l22_domain"]["excluded_by_3731_3818"]} + require(len(domain) == 11 and closed | earlier == domain and not closed & earlier, + "census route does not close the eleven-split domain") + return sorted(closed) + + +def build(work): + source = (ROOT / ENGINE).read_text(encoding="utf-8") + for old, new in EDITS: + require(source.count(old) == 1, "engine edit anchor " + old) + source = source.replace(old, new) + changed = [i for i, (a, b) in enumerate(zip( + (ROOT / ENGINE).read_text(encoding="utf-8").splitlines(), source.splitlines())) if a != b] + require(len(changed) == 2, "engine change is not exactly two lines") + cpp = work / "census22.cpp" + cpp.write_text(source, encoding="utf-8") + binary = work / "census22" + compiler = os.environ.get("CXX", "c++") + subprocess.run([compiler, *FLAGS, "-o", str(binary), str(cpp)], check=True) + return binary, hashlib.sha256(source.encode()).hexdigest() + + +def run(binary, work, n, length, s, t, cap=0): + hits = work / f"hits_{n}_{length}_{s}_{t}_{cap}.txt" + proc = subprocess.run([str(binary), str(n), str(length), str(s), str(t), "1", str(cap), + str(hits)], capture_output=True, text=True) + require(proc.returncode in (0, 2), f"engine error {n},{length},{s},{t}: {proc.stderr}") + summary = json.loads(proc.stdout) + words = hits.read_text().split() + return proc.returncode, summary, words + + +def controls(binary, work): + full = {(c["length"], *c["split"]): c for c in + json.loads((ROOT / FULL).read_text(encoding="utf-8"))["cases"]} + for key in L20_CONTROLS: + rc, summary, words = run(binary, work, 7, *key) + require(rc == 0 and not words and summary == full[key], f"L<=20 control {key}") + rc, summary, words = run(binary, work, 6, 22, 11, 11, cap=200000) + require(rc == 2 and not summary["complete"] and summary["hits"] == len(words) > 0, + "n=6 L=22 positive control") + for word in words: + restored, covered, distinct = universal(word, 6) + require(len(word) == 22 and restored and covered and distinct == 22, + "positive-control hit is not a simple universal restored word " + word) + rc, summary, _ = run(binary, work, 7, 22, 10, 7, cap=1000) + require(rc == 2 and summary["complete"] is False, "cap control must fail closed") + return len(words) + + +def replay(binary, work, result, splits, workers): + recorded = {tuple(r["split"]): r for r in result["second_engine_l22"]["runs"] + if r.get("complete")} + todo = list(splits) + require(todo, "no split selected for replay") + missing = [s for s in todo if s not in recorded] + require(not missing, f"no complete RESULT.json receipt for requested split(s) {missing}") + with concurrent.futures.ThreadPoolExecutor(max_workers=workers) as pool: + outs = list(pool.map(lambda s: run(binary, work, 7, 22, *s), todo)) + for split, (rc, summary, words) in zip(todo, outs): + require(rc == 0 and not words and summary == recorded[split], + f"L=22 replay differs from RESULT.json at {split}") + return todo + + +def main(): + parser = argparse.ArgumentParser(description=__doc__.splitlines()[0]) + parser.add_argument("--full", action="store_true") + parser.add_argument("--workers", type=int, default=4) + parser.add_argument("--splits", default="", + help="completed L=22 splits to replay, for example 9:9,10:8") + args = parser.parse_args() + pinned = authenticate() + result = json.loads((PACKAGE / "RESULT.json").read_text(encoding="utf-8")) + rows, quotes = check_map(result, pinned) + distinct = check_witness() + closed = check_deep_receipt(result) + with tempfile.TemporaryDirectory() as tmp: + work = Path(tmp) + binary, digest = build(work) + require(digest == result["second_engine_l22"]["engine_sha256"], "lifted engine digest") + positive = controls(binary, work) + if args.full: + splits = [tuple(r["split"]) for r in result["second_engine_l22"]["runs"] + if r.get("complete")] + elif args.splits: + splits = [tuple(int(x) for x in item.split(":")) for item in args.splits.split(",")] + else: + splits = QUICK_L22 + done = replay(binary, work, result, splits, args.workers) + print(f"{MARKER} map_rows={rows} quotes={quotes} witness_distinct_prefixes={distinct} " + f"census_route_closed={len(closed)}+4 positive_hits={positive} " + f"l22_replayed={len(done)} mode={'full' if args.full else 'splits' if args.splits else 'quick'} no_new_kappa") + + +if __name__ == "__main__": + sys.exit(main())