diff --git a/docs/ci-verification.md b/docs/ci-verification.md index 582e416aaf..50e8120dc0 100644 --- a/docs/ci-verification.md +++ b/docs/ci-verification.md @@ -2,6 +2,18 @@ ## Current selected-family replay +Resolve the [selected record](../certificates/selected-result.json) before +running a historical checkpoint. The current cold replay is +`make frontier4359-verify`, using the +[proof review](research/pr-intake-evidence/pr4359/PROOF-REVIEW.md), +[validation](research/pr-intake-evidence/pr4359/VALIDATION.json) and +[source manifest](../certificates/frontier4359-source.json). +The [frontier4359 workflow](../.github/workflows/frontier4359.yml) provides +hosted replay evidence. Metadata and source-pin checks are separate from +operator replay and do not discharge the inherited theorem assumptions. + +## Historical frontier1094 replay + Start with the [selected record](../certificates/selected-result.json). Its `reproduce`, `review`, `source_manifest` and `validation` fields identify the replay command, scoped assessment, source bindings and integration evidence. diff --git a/docs/research/current-status.md b/docs/research/current-status.md index 62a8cbb097..532af84312 100644 --- a/docs/research/current-status.md +++ b/docs/research/current-status.md @@ -1,12 +1,14 @@ # Current reviewed status -Selected conditional κ: **0.0023 = 23/10000**, zxv’s #4359 productive-helper construction, using Jacob Alan Sussman’s mixed-target recursion and the credited cumulative native/outer lineage. +Selected conditional κ: **0.0023** (= 23/10000), zxv’s #4359 productive-helper construction, using Jacob Alan Sussman’s mixed-target recursion and the credited cumulative native/outer lineage. [Selected record](../../certificates/selected-result.json) · [Proof review](pr-intake-evidence/pr4359/PROOF-REVIEW.md) · [Integration receipt](pr-intake-evidence/pr4359/INTEGRATION.json) · [Contributors](community-productive4359-contributors.md). Cold replay: `make frontier4359-verify`. The fresh 23-stage replay and 59 normalized artifacts pass; the changed interfaces have an AI-assisted proof review under retained analytic/native/fixed-tape hypotheses. Winning uniform templates are not materialized. This is not a complete formal or independent human verification. #4404 independently checks a narrower arithmetic/flow scope. -## Historical selected status through #1094 +All sections below are a historical snapshot; the selected-result.json record above is authoritative. + +## Historical checkpoint through #1094 Historical selected conditional κ: **0.001672660197076918**, Rohan Arun's #1094 on Jeremy Kothe's #1087 packing and the cumulative k8/slot/T16 construction. The bit supplier remains #589 on #555. diff --git a/research/d8-mixed-target-seeda97c8e/SOURCES.json b/research/d8-mixed-target-seeda97c8e/SOURCES.json index 9384463ff4..5dcfa9dd60 100644 --- a/research/d8-mixed-target-seeda97c8e/SOURCES.json +++ b/research/d8-mixed-target-seeda97c8e/SOURCES.json @@ -4,25 +4,25 @@ "files": [ { "path": "autoresearch.md", - "usage": "input", + "usage": "provenance", "git_blob": "8d5403e0f10f68a61d0cb9294fa2e83e872d1d82", "sha256": "215b3222f6a943edc69422a28ac21ea1f397ddf54770f1d87ac4195385d73699" }, { "path": "certificates/selected-result.json", - "usage": "input", + "usage": "provenance", "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" }, { "path": "docs/research/agent-task-catalog.json", - "usage": "input", + "usage": "provenance", "git_blob": "06c96f5579bb67ed1b86d334e78fbed7da6945f1", "sha256": "6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075" }, { "path": "docs/research/current-status.md", - "usage": "input", + "usage": "provenance", "git_blob": "d73b4ff9da41f044e793422db4318be17e234a6c", "sha256": "adb54af005eb11edaf84d782fe729338680ff908f6d4fbf39ba1062d2e7d8a77" }, diff --git a/research/d8-mixed-target-seeda97c8e/VERIFY.json b/research/d8-mixed-target-seeda97c8e/VERIFY.json index caff4adf82..2726200ed3 100644 --- a/research/d8-mixed-target-seeda97c8e/VERIFY.json +++ b/research/d8-mixed-target-seeda97c8e/VERIFY.json @@ -4,10 +4,6 @@ "python": "3.12", "requirements": [], "inputs": [ - "autoresearch.md", - "certificates/selected-result.json", - "docs/research/agent-task-catalog.json", - "docs/research/current-status.md", "research/bit-three-register-lower-bound/README.md", "research/d8-mixed-target-seeda97c8e/verify.py" ], diff --git a/research/historical-1042-link/RESULT.json b/research/historical-1042-link/RESULT.json index a9d58d2881..30ec98c793 100644 --- a/research/historical-1042-link/RESULT.json +++ b/research/historical-1042-link/RESULT.json @@ -2,8 +2,9 @@ "historical_href": "../../certificates/selected-result.json", "checkpoint": "certificates/checkpoints/frontier1042.json", "historical_kappa": "1672188119205421/1000000000000000000", - "live_kappa": "836330098538459/500000000000000000", + "live_kappa": "23/10000", "same_href": true, "kappas_differ": true, - "no_new_kappa": true + "no_new_kappa": true, + "intermediate_checkpoint": "certificates/checkpoints/frontier1094.json" } diff --git a/research/historical-1042-link/SOURCES.json b/research/historical-1042-link/SOURCES.json index c6119ca5a8..c84edb7634 100644 --- a/research/historical-1042-link/SOURCES.json +++ b/research/historical-1042-link/SOURCES.json @@ -11,20 +11,29 @@ { "path": "docs/research/current-status.md", "usage": "input", - "git_blob": "4e0a8b7cdacc1d9680f7f81d03624118bb20416d", - "sha256": "00a08925c51b26d168b8099ddeed659ac4381f7e04f3c7fd0e9de8e71f206823" + "git_blob": "532af84312cbfeb39a1e4659d8398deb560f1e4a", + "sha256": "54c843968d0b178369a7e56161be44c4692935c3f46ce261678aeedadb309891", + "pin": "head:41beb2e687da0ad1e06e2fcec00eb377560ca2db:docs/research/current-status.md" }, { "path": "certificates/selected-result.json", "usage": "input", - "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", - "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + "git_blob": "ed33caef5c5827693e9572d252a66f99cbb73d40", + "sha256": "5732707cc1e460b090b53f2463162749ad860de878a18f7408938671d295a9d9", + "pin": "head:41beb2e687da0ad1e06e2fcec00eb377560ca2db:certificates/selected-result.json" }, { "path": "certificates/checkpoints/frontier1042.json", "usage": "input", "git_blob": "f451ced6626a1f03aba6915ce23a136b01ebe51d", "sha256": "207d1f49f113c585024b9d3c17eadbb8b1be17c1321e3d190aabe2f18ce1c5b7" + }, + { + "path": "certificates/checkpoints/frontier1094.json", + "usage": "input", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129", + "pin": "head:41beb2e687da0ad1e06e2fcec00eb377560ca2db:certificates/checkpoints/frontier1094.json" } ] } diff --git a/research/historical-1042-link/VERIFY.json b/research/historical-1042-link/VERIFY.json index 5cff7b26c9..5138c1b017 100644 --- a/research/historical-1042-link/VERIFY.json +++ b/research/historical-1042-link/VERIFY.json @@ -6,16 +6,25 @@ "inputs": [ "docs/research/current-status.md", "certificates/selected-result.json", - "certificates/checkpoints/frontier1042.json" + "certificates/checkpoints/frontier1042.json", + "certificates/checkpoints/frontier1094.json" ], "commands": [ { - "argv": ["{python}", "-B", "{package}/verify.py"], + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], "timeout_seconds": 30, "checks": "Compare the #1042 status link with the live record and the frontier1042 checkpoint." }, { - "argv": ["{python}", "-B", "{package}/test_verify.py"], + "argv": [ + "{python}", + "-B", + "{package}/test_verify.py" + ], "timeout_seconds": 30, "checks": "Check the printed decimal and the historical section cut." } diff --git a/research/historical-1042-link/verify.py b/research/historical-1042-link/verify.py index 12170922e5..2ffd4a8ce4 100644 --- a/research/historical-1042-link/verify.py +++ b/research/historical-1042-link/verify.py @@ -2,7 +2,8 @@ """Separate the #1042 status link from the live selected record. The historical section states the #1042 kappa and links to the live record. -The matching checkpoint is the selected record's previous_record field. +The matching checkpoint is reached through the selected record's historical +previous_record chain (currently via frontier1094). """ import hashlib @@ -16,6 +17,7 @@ MARKER = "PASS_HISTORICAL_1042_LINK kappas_differ=true no_new_kappa" HREF = "../../certificates/selected-result.json" CHECKPOINT = "certificates/checkpoints/frontier1042.json" +INTERMEDIATE = "certificates/checkpoints/frontier1094.json" SHOWN = "0.001672188119205421" @@ -43,6 +45,7 @@ def authenticate(): "docs/research/current-status.md", "certificates/selected-result.json", "certificates/checkpoints/frontier1042.json", + "certificates/checkpoints/frontier1094.json", } require(set(pinned) == expected, "input inventory changed") for path, row in pinned.items(): @@ -64,12 +67,15 @@ def evaluate(): require(HREF in section, "the historical section lost the live-record link") require(SHOWN in section, "the historical kappa sentence moved") require(Fraction(SHOWN) == Fraction(old["kappa"]), "the checkpoint kappa left the printed decimal") - require(live["previous_record"] == CHECKPOINT, "the previous-record pointer moved") + require(live["previous_record"] == INTERMEDIATE, "the live previous-record pointer moved") + intermediate = json.loads((ROOT / INTERMEDIATE).read_text(encoding="utf-8")) + require(intermediate["previous_record"] == CHECKPOINT, "the checkpoint ancestry link moved") require(Fraction(live["kappa"]) != Fraction(old["kappa"]), "the live and historical kappas agree") require(text.index(HREF) < text.index("# Historical status through #1042"), "the live section lost its record link") return { "historical_href": HREF, "checkpoint": CHECKPOINT, + "intermediate_checkpoint": INTERMEDIATE, "historical_kappa": old["kappa"], "live_kappa": live["kappa"], "same_href": True, diff --git a/research/six-source-higher-arity-toggle-floor-seedd45c17a9/EXTERNAL-PINS.json b/research/six-source-higher-arity-toggle-floor-seedd45c17a9/EXTERNAL-PINS.json new file mode 100644 index 0000000000..09dd04421c --- /dev/null +++ b/research/six-source-higher-arity-toggle-floor-seedd45c17a9/EXTERNAL-PINS.json @@ -0,0 +1,32 @@ +{ + "academic_source": { + "author": "Volodymyr Gavrylkiv", + "title": "Bases in Dihedral and Boolean Groups", + "publication": "Journal of Integer Sequences, Vol. 20 (2017), Article 17.8.1", + "url": "https://cs.uwaterloo.ca/journals/JIS/VOL20/Gavrylkiv/gav4.pdf", + "locator": "Introduction definition of basis; Table 3, page 7: r[(C2)^6]=14", + "downloaded_sha256": "3418224e0e4427bba18ef907f14000069de9aed7400dfc240dafba1cf29f6584" + }, + "duo_witness": { + "pr": 2128, + "head": "697369a971eed02c0fbcd75ebefec9f59945f08e", + "path": "research/connector-six-source-duo/CERTIFICATE.json", + "sha256": "e611d16e100eb9fd9861d9c872c21ae7d1ac280880efe783d2407151dd1e6bb2" + }, + "closest_predecessors": [ + { + "pr": 2156, + "head": "05b4672fa4450ef50b06315e3a0893d4ba43d42d", + "scope": "DUO-domain six-source full-batch optimum and exact 142-add floor" + }, + { + "pr": 2146, + "head": "302b0e87d9328fabc2a670248afb357bbb44041b", + "scope": "one fixed six-source single-TRIO call profile" + }, + { + "pr": 1518, + "scope": "atomic triple-sum connector budget result" + } + ] +} diff --git a/research/six-source-higher-arity-toggle-floor-seedd45c17a9/README.md b/research/six-source-higher-arity-toggle-floor-seedd45c17a9/README.md new file mode 100644 index 0000000000..e33c0a3fcb --- /dev/null +++ b/research/six-source-higher-arity-toggle-floor-seedd45c17a9/README.md @@ -0,0 +1,65 @@ +# Six-source additive-cost floor for high-arity connector toggles + +**Scoped negative result; no supplier or new κ.** Extending the six-source universal dirty-connector alphabet with one source-hyperedge operation for every subset of size four through six cannot improve its full 63-mask batch when every source tap is charged. The exact optimistic full-batch Pareto point remains 140 total queries and 142 total additions. The known attaining word uses 14 source calls and 16 source additions. The argument closes the entire arity-4..6 family, including schedules that use more than two output readouts, without enumerating its words. + +## Assignment and changed scope + +- Cycle 43 seed: `d45c17a9abef1858e6b314d2bb66be28`; track `recursive-interfaces`; task `connector-alphabet-change`; priority revision 4. +- Base: `0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2`. +- Selected record SHA-256: `10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32`. +- Catalogue SHA-256: `d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7`. +- The broad card is refined to a new parametrized operation family, `H_S: z += sum(B_j x_j)` for `4 <= |S| <= 6`, on the fixed six-source, all-63-output instance. It keeps read-only sources, arbitrary dirty connector contents, complete restoration, and separate output readouts. Its most favorable full price is one dispatch plus `|S|` charged source additions; any routing, frame, or implementation cost adds to this bill. + +This is a changed connector contract relative to the selector's broader starting suggestions. Earlier work covers the pair-source DUO witness (#2128), a fixed one-TRIO profile (#2146), and the DUO full-batch optimum (#2156). This result derives an all-arity floor for source subsets of size four through six. It neither claims those earlier constructions nor independently replays their searches. + +## Exact lower bound + +A source word is a closed walk `q_0,...,q_k` in `F2^6`; a hyperedge call on `S` changes `q` by the indicator vector of `S`. Let `P` be the distinct prefix set and let `D(P)={a+b:a,b in P}`. A mask in `D(P)` can be realized with two output readouts. The exact group basis result `r[(C2)^6]=14` (Volodymyr Gavrylkiv, *Bases in Dihedral and Boolean Groups*, Journal of Integer Sequences 20 (2017), Article 17.8.1, Table 3) implies that a prefix set of size at most 13 cannot cover every mask. + +The lower bound must also allow outputs with more than two readouts. Each output needs an even number of `A_i` reads to cancel its arbitrary dirty-connector contribution. A nonzero output needs at least two reads; if its mask is missing from `D(P)`, two reads cannot realize it, so it needs at least four. If `M` of the 63 nonzero masks are missing, the total output-read count is `R >= 126 + 2M`. + +Now split by the number `k` of source-call dispatches. If `k >= 14`, then `k+R >= 140`. If `k` is 12 or 13, `|P| <= k <= 13`, so the basis-size result forces `M >= 1`; hence `k+R >= k+128 >= 140`. If `k <= 11`, at most `binom(k,2)` nonzero pair differences occur, so `M >= 63-binomial(k,2)`. Thus + +```text +k + R >= k + 126 + 2(63 - binomial(k,2)) >= 153 for 0 <= k <= 11. +``` + +Therefore **every schedule, including those with four or more readouts on some outputs, has at least 140 total queries**. This case split depends on source-prefix geometry, not on whether one source call toggles one, two, or six sources. + +For the source-add charge, expand every hyperedge step `S` into `|S|` singleton toggles in any fixed order. The expanded path retains every original boundary, so all original output-readout placements remain valid. It is a singleton source word of length `W=sum |S|`; the pinned exact six-source result `f(6)=16` in `research/universal-connector-six-source` gives `W >= 16`. Also `R >= 126`, hence total additions `W+R >= 142`. + +The most favorable complete price is therefore + +```text +queries Q >= 140 +source additions W >= 16 +output readouts R >= 126 +total additions W+R >= 142 +price >= 140 o + 142 p, for o,p >= 0 +``` + +Here `o` is the fully charged dispatch/entry-exit cost and `p` the per-add cost. Any routing, frame, or implementation surcharge only increases the bill. The 14-step DUO witness from PR #2128 attains `Q=140`, `W=16`, and `R=126`, so it reaches `(140,142)`. Its witness is attributed to that PR and pinned in [EXTERNAL-PINS.json](EXTERNAL-PINS.json). + +## Verification + +The local verifier checks the cited six-source census receipt, the exact pinned 14-step witness and its all-mask difference coverage, expansion of every six-bit source subset, the complete 63-row dirty-connector schedule, reverse restoration, the all-k query-floor case split, and three failure controls. The six-source census prerequisite was also run locally under CPython 3.14.7; its output is recorded in `RESULT.json`. + +From repository root: + +```sh +python3 -I -O -B research/six-source-higher-arity-toggle-floor-seedd45c17a9/verify.py +python3 scripts/research_package.py --package research/six-source-higher-arity-toggle-floor-seedd45c17a9 --check-only +python3.12 scripts/research_package.py --package research/six-source-higher-arity-toggle-floor-seedd45c17a9 +``` + +## Limits + +This excludes an improvement only for source-hyperedge calls whose fully charged source-add price is at least the sum of their constituent source taps, with the six-source universal dirty-connector contract and 63 separate outputs fixed. It does not cover subadditive physical fusion, mutable sources, new output operations, different target families, supplier placement, or a multiplication exponent. The result is an abstract interface bound, not physical admission into the selected supplier. + +## Open next questions + +**Question:** Can a concrete selected-supplier interface realize any source-hyperedge of arity at least four with a total cost strictly below its constituent source reads while preserving arbitrary dirty-state restoration? First step: name one existing supplier frame, compile one such hyperedge into literal native operations, and charge its complete route/frame/precision bill. It matters because only a physically realizable subadditive charge escapes the floor proved here. The present six-source abstract connector has no admitted supplier realization, which is the blocker. + +## Credit + +The exact `f(6)=16` source-word result is predecessor work in `research/universal-connector-six-source`. The 14-call/16-add upper witness is Aaron Wang/Navinor's PR #2128. PR #2156 provides the closely related DUO-domain global optimum and credits Gavrylkiv for the group basis value. PR #2146 tests one fixed six-source TRIO profile. Prepared by Cinna Davis with substantial OpenAI Codex assistance; this package adds the all-arity source-expansion lower bound and full charged interpretation. No independent human review is claimed. diff --git a/research/six-source-higher-arity-toggle-floor-seedd45c17a9/RESULT.json b/research/six-source-higher-arity-toggle-floor-seedd45c17a9/RESULT.json new file mode 100644 index 0000000000..22b1c8edfe --- /dev/null +++ b/research/six-source-higher-arity-toggle-floor-seedd45c17a9/RESULT.json @@ -0,0 +1,57 @@ +{ + "status": "PASS_HIGH_ARITY_CONNECTOR_FLOOR", + "scope": "F2^6, full 63-row batch, source hyperedges |S|=4..6, sources read-only, arbitrary dirty connector, separate readouts, per-dispatch o and per-source-add p", + "lower_bounds": { + "total_queries": 140, + "source_adds": 16, + "separate_readouts": 126, + "total_additions": 142 + }, + "priced_lower_bound": "140 o + 142 p, for o,p >= 0, before nonnegative implementation surcharge", + "attaining_predecessor": { + "pr": 2128, + "head": "697369a971eed02c0fbcd75ebefec9f59945f08e", + "steps": [ + 2, + 16, + 8, + 16, + 1, + 4, + 48, + 4, + 3, + 4, + 32, + 8, + 4, + 16 + ], + "source_calls": 14, + "source_adds": 16, + "full_difference_coverage": true + }, + "proof_inputs": { + "singleton_f6": "research/universal-connector-six-source/EXPECTED.json; source pins in SOURCES.json", + "difference_basis": "Gavrylkiv, JIS 20 (2017), Article 17.8.1, Table 3; exact PDF hash in EXTERNAL-PINS.json" + }, + "dirty_replay_cases": 8064, + "limitations": [ + "abstract connector model only", + "no physical supplier or selected-bound admission", + "no kappa change claimed", + "does not cover subadditive physical fusion or changed output alphabet" + ], + "predecessor_check": { + "command": "python3 -I -O -B research/universal-connector-six-source/verify.py", + "expected": "PASS_SIX_SOURCE_CONNECTOR f(6)=16 max14=59/64 max12=49/64 batch63=142 f(7) in [18,24]", + "observed": "PASS_SIX_SOURCE_CONNECTOR f(6)=16 max14=59/64 max12=49/64 batch63=142 f(7) in [18,24]", + "environment": "CPython 3.14.7" + }, + "query_bound_case_split": { + "k_ge_14": "Q>=k+126>=140", + "k_12_or_13": "r((C2)^6)=14 implies at least one missing pair mask; Q>=k+128", + "k_le_11": "M>=63-binomial(k,2); Q>=k+126+2M>=153", + "allows_more_than_two_readouts": true + } +} diff --git a/research/six-source-higher-arity-toggle-floor-seedd45c17a9/SOURCES.json b/research/six-source-higher-arity-toggle-floor-seedd45c17a9/SOURCES.json new file mode 100644 index 0000000000..d93c62bf0a --- /dev/null +++ b/research/six-source-higher-arity-toggle-floor-seedd45c17a9/SOURCES.json @@ -0,0 +1,42 @@ +{ + "schema_version": 1, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "e8870e5917057d59b730eb14721a778639eca050", + "sha256": "d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7" + }, + { + "path": "research/universal-connector-six-source/EXPECTED.json", + "usage": "input", + "git_blob": "160a96c50f77ba411af957b554da05a8470e70ca", + "sha256": "f1b1bec330640c81ac0da25ee8b3a0a49fe9ea5bb2eadaaa787c64bd62c9e73a" + }, + { + "path": "research/universal-connector-six-source/README.md", + "usage": "input", + "git_blob": "c7123c3cfd7545deb6af607800df0d15c6e8c0d2", + "sha256": "ea9cca56d1547dcd984f5f99f6c6243c9417a7ede08f68782c7a6616aa6eb563" + }, + { + "path": "research/universal-connector-six-source/SOURCES.json", + "usage": "input", + "git_blob": "26fb2bba89ea96ff51f2fd6428f8cf41cd725412", + "sha256": "1223c03bb3d831880099d76b0d086cd5b833ca3b7f2416f96562f8d19b3b0bcf" + }, + { + "path": "research/universal-connector-six-source/verify.py", + "usage": "input", + "git_blob": "069d299dfd206697d073d731a86e5b5079558331", + "sha256": "930c3c2135c28192a907b88cce9cc07ab2fdf1e36f263249cd3bf38d4a3aed5b" + } + ] +} diff --git a/research/six-source-higher-arity-toggle-floor-seedd45c17a9/TASK.json b/research/six-source-higher-arity-toggle-floor-seedd45c17a9/TASK.json new file mode 100644 index 0000000000..89cfd7b300 --- /dev/null +++ b/research/six-source-higher-arity-toggle-floor-seedd45c17a9/TASK.json @@ -0,0 +1,87 @@ +{ + "schema_version": 1, + "task_id": "connector-alphabet-change", + "priority_revision": 4, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "original_card": { + "id": "connector-alphabet-change", + "question": "Does one explicit extension of the connector alphabet offer a favorable completed budget?", + "starting_points": [ + "research/universal-connector-boundary/README.md", + "certificates/selected-result.json" + ], + "methods": [ + "Construct and charge a legal extra operation on a minimal instance.", + "Prove a target-specific bound after adding one specified operation family." + ], + "acceptance_gate": "State which fixed-alphabet premise changes and charge its implementation; do not declare it free.", + "first_step": { + "command": [ + "python3", + "-B", + "research/universal-connector-boundary/verify.py" + ], + "expected": "PASS_UNIVERSAL_CONNECTOR_BOUNDARY", + "inspect": "Reproduce the 945-pairing control, then read Exact interface to list the allowed calls.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Add exactly one legally priced operation and test a tiny dirty-input instance before enumerating larger cases.", + "bottleneck_link": "A new legal connector operation could change recursive interface cost; a larger census in the same alphabet is a separate side result.", + "allowed_variations": [ + "Choose one additional operation and a small source count for its first counterexample." + ], + "scope_change_triggers": [ + "Keeping the alphabet and only increasing the source count; record this as a changed assignment." + ], + "overlap_terms": [ + "universal connector", + "source-toggle", + "connector alphabet" + ] + }, + "scope_status": "changed", + "actual_scope": "In the six-source, all-63-mask universal dirty-connector model, add a parametrized source-hyperedge family z += sum_{j in S} B_j x_j for 4 <= |S| <= 6, with read-only sources and full price one dispatch plus |S| source additions. Prove the exact charged batch floor and test the PR #2128 witness as a positive dirty-state control.", + "scope_change_reason": "The suggested joint-query scope is densely claimed, while the connector-alphabet task has one fixed DUO upper construction, one fixed TRIO profile, and an open handoff for a changed connector contract. This refinement changes the operation family from arity two/three to all arities four through six at fixed n=6, and asks for a family-wide additive-price theorem rather than another finite word census.", + "bottleneck_link": "A lower-cost source operation could reduce the paid recursive interface. The optimistic complete price includes dispatch, every constituent source addition, and any implementation surcharge. The result tests whether higher arity alone can improve the full six-source connector profile.", + "budget_minutes": 60, + "stop_rule": "Prove the query-call/readout case split for any number of output readouts, prove W>=16 by singleton expansion, verify the exact positive word and dirty batch schedule, then stop once Q>=140 and total additions>=142 close the additive-price profile. Do not enumerate words after the general floor is proved.", + "outcome": "negative-result", + "evidence": "For each hyperedge S, splitting into |S| singleton toggles retains every original boundary, so W>=f(6)=16. Let M be missing nonzero pairwise prefix differences. Each output needs an even readout count; a missing mask needs at least four reads, so R>=126+2M. The published exact r((C2)^6)=14 forces M>=1 for k=12,13; for k<=11, M>=63-binomial(k,2); for k>=14, R>=126 suffices. Thus Q=k+R>=140 for all k and any arity. Also W+R>=142. The PR #2128 witness attains (Q,W+R)=(140,142). No supplier or kappa result.", + "author": "Cinna Davis", + "ai_assistance": "Substantial OpenAI Codex assistance in task selection, mathematical derivation, verifier implementation and drafting. The 14-call/16-add witness belongs to Aaron Wang/Navinor PR #2128; f(6)=16 is predecessor work in research/universal-connector-six-source; the basis-size 14 result is Volodymyr Gavrylkiv 2017. No independent human review is claimed.", + "open_questions": [ + { + "question": "Can one concrete selected-supplier interface implement an arity-four-or-higher source hyperedge at a total charge below the sum of its source taps?", + "why_it_matters": "Only a realizable subadditive charge escapes the exact additive-price profile floor proved here.", + "first_step": "Choose one existing supplier frame, instantiate a four-source hyperedge on its literal registers, derive its complete native routing/frame/precision invoice, and compare against four separate source reads.", + "blocked_by": "No admitted physical realization of the six-source abstract connector interface is currently available." + } + ], + "selector": { + "seed": "d45c17a9abef1858e6b314d2bb66be28", + "track": "recursive-interfaces", + "task_id": "connector-alphabet-change", + "scope_key": "e45d80707887c042f0c8", + "priority_revision": 4, + "catalogue_sha256": "d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7", + "selected_record_sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32", + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-18938454", + "rejected_nearby_scope": "joint-query-controller due to overlapping active QQ16 observation/controller work" + }, + "overlap": { + "searched_at": "2026-10-15T01:51:57.601188+00:00", + "open_prs": 476, + "complete_pr_pagination": true, + "discussions": 946, + "complete_discussion_pagination": true, + "warnings": [], + "nearest": [ + "#2128 DUO witness", + "#2156 DUO optimum handoff", + "#2146 fixed one-TRIO profile", + "#1518 triple-sum connector", + "#2221 seven-source connector" + ] + } +} diff --git a/research/six-source-higher-arity-toggle-floor-seedd45c17a9/VERIFY.json b/research/six-source-higher-arity-toggle-floor-seedd45c17a9/VERIFY.json new file mode 100644 index 0000000000..a779652790 --- /dev/null +++ b/research/six-source-higher-arity-toggle-floor-seedd45c17a9/VERIFY.json @@ -0,0 +1,25 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/universal-connector-six-source/README.md", + "research/universal-connector-six-source/EXPECTED.json", + "research/universal-connector-six-source/verify.py", + "research/universal-connector-six-source/SOURCES.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "exact six-source census binding, all-k query/readout lower-bound cases, source-hyperedge expansion, dirty full-batch replay, reverse restoration and three failure controls" + } + ] +} diff --git a/research/six-source-higher-arity-toggle-floor-seedd45c17a9/verify.py b/research/six-source-higher-arity-toggle-floor-seedd45c17a9/verify.py new file mode 100644 index 0000000000..97920fc5bc --- /dev/null +++ b/research/six-source-higher-arity-toggle-floor-seedd45c17a9/verify.py @@ -0,0 +1,190 @@ +#!/usr/bin/env python3 +"""Exact replay of the additive-cost high-arity connector floor.""" +from __future__ import annotations + +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +STEPS = (2, 16, 8, 16, 1, 4, 48, 4, 3, 4, 32, 8, 4, 16) +EXPECTED = (ROOT / "research/universal-connector-six-source/EXPECTED.json") + + +def need(ok: bool, label: str) -> None: + if not ok: + raise SystemExit("FAIL: " + label) + + +def weight(mask: int) -> int: + return mask.bit_count() + + +def prefixes(steps: tuple[int, ...]) -> list[int]: + q = 0 + out = [q] + for step in steps: + need(0 < step < 64, "nonempty six-source step") + q ^= step + out.append(q) + return out + + +def differences(points: list[int]) -> set[int]: + return {a ^ b for a in points for b in points} + + +def singleton_expand(mask: int) -> tuple[int, ...]: + return tuple(1 << j for j in range(6) if mask & (1 << j)) + + +def macro_effect(mask: int, x: int, z: int) -> int: + return z ^ ((mask & x).bit_count() & 1) + + +def optimistic_query_floor(k: int) -> int: + # P has at most k distinct prefixes because the final prefix repeats zero. + # r((C2)^6)=14 forces at least one missing pair-difference for k=12,13. + if k >= 14: + return k + 126 + if k >= 12: + return k + 128 + missing = 63 - k * (k - 1) // 2 + return k + 126 + 2 * missing + + +def make_pairs(points: list[int]) -> dict[int, tuple[int, int]]: + unique = points[:-1] # the closing boundary repeats q_0 + pairs: dict[int, tuple[int, int]] = {} + for mask in range(1, 64): + pair = next(((a, b) for a in range(len(unique)) + for b in range(a + 1, len(unique)) + if unique[a] ^ unique[b] == mask), None) + need(pair is not None, f"readout boundary for mask {mask}") + pairs[mask] = pair + return pairs + + +def batch_schedule(steps: tuple[int, ...], pairs: dict[int, tuple[int, int]]): + reads: list[list[int]] = [[] for _ in range(len(steps) + 1)] + for mask, (a, b) in pairs.items(): + reads[a].append(mask) + reads[b].append(mask) + ops: list[tuple[str, int]] = [] + for boundary in range(len(steps)): + ops.extend(("read", mask) for mask in sorted(reads[boundary])) + ops.append(("source", steps[boundary])) + ops.extend(("read", mask) for mask in sorted(reads[-1])) + return ops + + +def apply(ops, x: int, z: int, y: list[int]) -> tuple[int, list[int]]: + for kind, arg in ops: + if kind == "source": + z = macro_effect(arg, x, z) + else: + y[arg] ^= z + return z, y + + +def replay_batch(steps: tuple[int, ...], pairs: dict[int, tuple[int, int]]) -> bool: + ops = batch_schedule(steps, pairs) + if len(ops) != 140: + return False + for x in range(64): + for z0 in range(2): + for seed in (0, 1): + y0 = [((mask * 0x2D + seed) >> (mask % 6)) & 1 + for mask in range(64)] + z, y = apply(ops, x, z0, y0.copy()) + if z != z0: + return False + for mask in range(1, 64): + if y[mask] != (y0[mask] ^ ((mask & x).bit_count() & 1)): + return False + zr, yr = apply(list(reversed(ops)), x, z, y.copy()) + if zr != z0 or yr != y0: + return False + return True + + +def main() -> None: + receipt = json.loads(EXPECTED.read_text(encoding="utf-8")) + census = {row["length"]: row for row in receipt["censuses"] + if row["sources"] == 6} + need(census[12]["max_coverage"] == 49 and census[12]["words"] == 10395, + "pinned length-12 singleton census prerequisite") + need(census[14]["max_coverage"] == 59 and census[14]["words"] == 945945, + "pinned length-14 singleton census prerequisite") + need(receipt["batch"]["optimum_queries"] == 142, + "pinned six-source batch receipt") + query_floors = [optimistic_query_floor(k) for k in range(15)] + need(min(query_floors) == 140 and optimistic_query_floor(12) == 140 + and optimistic_query_floor(13) == 141 and optimistic_query_floor(11) == 153, + "all-readout query lower-bound case split") + + q = prefixes(STEPS) + need(len(STEPS) == 14 and q[-1] == 0, "14-call witness closes dirty connector") + need(sum(map(weight, STEPS)) == 16, "witness source-add charge W=16") + witness_points = q[:-1] + need(len(set(witness_points)) == 14, "14 distinct witness boundaries") + need(differences(witness_points) == set(range(64)), + "witness prefix differences cover every source mask") + + expanded: list[int] = [] + q_expanded = 0 + retained = {0} + expanded_prefixes = [0] + for step in STEPS: + for singleton in singleton_expand(step): + expanded.append(singleton) + q_expanded ^= singleton + expanded_prefixes.append(q_expanded) + retained.add(q_expanded) + need(len(expanded) == 16 and q_expanded == 0, + "expansion has exactly W=16 singleton toggles and closes") + need(retained == set(witness_points), "all original event boundaries survive expansion") + need(differences(expanded_prefixes) == set(range(64)), + "expanded singleton word remains universal") + + # Tiny exact dirty-state test for every source-hyperedge, including arities 4..6. + macro_cases = 0 + for mask in range(1, 64): + split = singleton_expand(mask) + for x in range(64): + for z0 in range(2): + z_macro = macro_effect(mask, x, z0) + z_split = z0 + for bit in split: + z_split = macro_effect(bit, x, z_split) + need(z_macro == z_split, f"dirty macro/split identity S={mask}") + macro_cases += 1 + need(macro_cases == 8064, "complete small macro-state coverage") + + pairs = make_pairs(q) + ops = batch_schedule(STEPS, pairs) + need(sum(kind == "source" for kind, _ in ops) == 14, + "full-batch source calls") + need(sum(weight(arg) for kind, arg in ops if kind == "source") == 16, + "full-batch source-add invoice") + need(sum(kind == "read" for kind, _ in ops) == 126, + "two readouts for each nonzero row") + need(len(ops) == 140 and replay_batch(STEPS, pairs), + "full dirty-input batch and reverse replay") + + # Failure controls: open connector, wrong output mask, and undercharged arity. + need(prefixes(STEPS[:-1])[-1] != 0, "missing final source event is rejected") + mutated_pairs = dict(pairs) + mutated_pairs[1] = (0, 0) + need(not replay_batch(STEPS, mutated_pairs), "wrong mask boundary is rejected") + correct_macro_price = 1 + weight(0b001111) + fake_macro_price = 1 + weight(0b001111) - 1 + need(correct_macro_price == 5 and fake_macro_price < correct_macro_price, + "a four-tap macro cannot be billed as three taps") + + print("PASS_HIGH_ARITY_CONNECTOR_FLOOR arities=4..6 queries>=140 W>=16 " + "readouts>=126 adds>=142 dirty_macro_cases=8064 query_cases=15 reverse=True controls=3") + + +if __name__ == "__main__": + main() diff --git a/research/test-suite-locale-reads/SOURCES.json b/research/test-suite-locale-reads/SOURCES.json index be5f08378a..98f4744e2f 100644 --- a/research/test-suite-locale-reads/SOURCES.json +++ b/research/test-suite-locale-reads/SOURCES.json @@ -17,8 +17,9 @@ { "path": "docs/research/current-status.md", "usage": "input", - "git_blob": "d73b4ff9da41f044e793422db4318be17e234a6c", - "sha256": "adb54af005eb11edaf84d782fe729338680ff908f6d4fbf39ba1062d2e7d8a77" + "git_blob": "532af84312cbfeb39a1e4659d8398deb560f1e4a", + "sha256": "54c843968d0b178369a7e56161be44c4692935c3f46ce261678aeedadb309891", + "pin": "head:41beb2e687da0ad1e06e2fcec00eb377560ca2db:docs/research/current-status.md" }, { "path": "tests/test_research_current_status.py", diff --git a/scripts/pr_intake_initial_heads.py b/scripts/pr_intake_initial_heads.py index bfcf7cd309..409dfebbfa 100644 --- a/scripts/pr_intake_initial_heads.py +++ b/scripts/pr_intake_initial_heads.py @@ -1,8 +1,7 @@ -"""Authenticate three initial intake observations after exact recorded revisions. +"""Authenticate four initial intake observations after exact recorded revisions. -The mutable intake metadata describes the revised head. These existing receipts -retain its initial observation, independently confirmed in the first committed -intake records (82d67beb, 09fbc0f0 and 24db9bff respectively). No Git access is +The mutable intake metadata describes the revised head. These receipts retain their original observations in immutable intake +evidence, including #4110 before its documented October 21 update. No Git access is needed, including inside historical replay copies. This is an exact checkpoint adapter: changed receipt bytes or another revision require explicit maintenance, not a fallback to unverified ledger history. Future intake needs a durable pin @@ -18,11 +17,15 @@ 'queue-tail-20261017': '1f5d355fe5fc44839f7ede91ce7f98691f1a87f1f9f856c7e057f00b98ad6249', 'queue-refresh-20261017': '618a67ccba7857ba533da75742b01fa3e40020097b01ccb3e205c49b993e65b3', 'queue-oct18-20261018': '9b8407cee0210bb30b193c8a1040aa14913de5405b496ca003ba279896c28e79', + 'queue-oct20f-20261020': '28751ed30182c5892e4569988a5ad8b931468c68c7d341a5bc2cbb22ee44191d', + 'queue-oct21a-20261021': 'd527aa1989ccffb02d33b1e5937606d8714440662ad5ac86bf1a22a9c137472f', } REVISIONS = { 3107: ('queue-next-20261017', 'initial_archived_head', 'queue-next-20261017'), 3184: ('queue-tail-20261017', 'previously_reviewed_head', 'queue-tail-20261017'), 3251: ('queue-refresh-20261017', 'head', 'queue-oct18-20261018'), + # #4110's reviewed October 21 successor changed the mutable intake head. + 4110: ('queue-oct20f-20261020', 'head', 'queue-oct21a-20261021'), } diff --git a/scripts/replay_historical_check.py b/scripts/replay_historical_check.py index 1e92fff278..6a828a51b1 100755 --- a/scripts/replay_historical_check.py +++ b/scripts/replay_historical_check.py @@ -155,7 +155,9 @@ 'path': 'scripts/partial_swap/shared.py', 'input_from_root': True, 'input': 'research/partial-swap-digest/baseline.py', 'sha256': '81e9af92cdf38243a540cdcff2062778e449467848d444da37a9553c12ca4c34', - 'accepted_live_sha256': ['7290bd639600aecff11941d3faf95c9ce95589125cc6a7f7440fb86af7a0f17c'], + 'accepted_live_sha256': ['7290bd639600aecff11941d3faf95c9ce95589125cc6a7f7440fb86af7a0f17c', + # Reviewed hot-loop and byte-stable digest successor. + '5a0646a50b9f3e8ea55168620a78e8853b0ab810517cefc8cfb8696aedee278a'], } CONFIG['skip-clones']['additional_inputs'] = [dict(LEGACY_SHARED)] CONFIG['skip-clones-tests']['additional_inputs'] = [dict(LEGACY_SHARED)] @@ -178,7 +180,9 @@ 'field': 'files', 'path': 'certificates/partial-swap-network.json', 'input': 'partial-swap-network.json', 'sha256': 'f3c4be597b2f2136da4ae2cc80c7454f63c90aa01f84e5b8131cee4dd55de815', - 'accepted_live_sha256': ['2b19ed45b6207647017f6ee9f87f41df484981822fe555d088e5c1185dc7c62a'], + 'accepted_live_sha256': ['2b19ed45b6207647017f6ee9f87f41df484981822fe555d088e5c1185dc7c62a', + # Certificate source digest refreshed; proof values unchanged. + '4c0b9d37e1034b2076e30a70f8e514416298c462d9ee98bc87fe6556b14df786'], }] # Retain every original unittest command, isolating only frozen family tests. @@ -236,7 +240,9 @@ 'accepted_live_sha256': [ 'ae5bcac684ce2188632f38dee8ed46ebdc9588f490401505aa1cac33c55d84db', # Tekalign's PR3139 appends deadline usage; replay still restores PR695 bytes. - 'a3711fe12d560fac7726c530b9c8c622182f3d4f231a876c163616e49bd911bc']}, + 'a3711fe12d560fac7726c530b9c8c622182f3d4f231a876c163616e49bd911bc', + # Current #4359 CI navigation update, archive remains immutable. + '6c3e67d7765addf682bc40c75140bfa8e691579c6ead3ceeae275d63ab0b5628']}, {'manifest': 'research/community-frontier890-audit/CONTENT-COVERAGE.json', 'field': ['pull_requests', '853', 'files'], 'path': 'scripts/verify_complex741_parallel.py',