From 08f1eaf5946f57de0e126e82b5e0432564cca4e0 Mon Sep 17 00:00:00 2001 From: Cinna Davis <1337isnot1337@users.noreply.github.com> Date: Wed, 14 Oct 2026 07:42:08 -0500 Subject: [PATCH] Research: exact selected T16 three-role cycle census --- .../README.md | 49 + .../RESULT.json | 1027 +++++++++++++++++ .../SOURCES.json | 78 ++ .../TASK.json | 97 ++ .../VERIFY.json | 35 + .../test_verify.py | 60 + .../verify.py | 412 +++++++ 7 files changed, 1758 insertions(+) create mode 100644 research/selected-t16-three-role-cycle-seedc375/README.md create mode 100644 research/selected-t16-three-role-cycle-seedc375/RESULT.json create mode 100644 research/selected-t16-three-role-cycle-seedc375/SOURCES.json create mode 100644 research/selected-t16-three-role-cycle-seedc375/TASK.json create mode 100644 research/selected-t16-three-role-cycle-seedc375/VERIFY.json create mode 100644 research/selected-t16-three-role-cycle-seedc375/test_verify.py create mode 100644 research/selected-t16-three-role-cycle-seedc375/verify.py diff --git a/research/selected-t16-three-role-cycle-seedc375/README.md b/research/selected-t16-three-role-cycle-seedc375/README.md new file mode 100644 index 0000000000..7837ce27cb --- /dev/null +++ b/research/selected-t16-three-role-cycle-seedc375/README.md @@ -0,0 +1,49 @@ +# Selected T16 same-call three-role cycle census + +**Status: scoped negative result; no new κ.** On the selected PR1094 T16 owner map, every capacity-feasible same-invocation cycle of three whole-helper roles either leaves the idle-rank histogram unchanged or strictly raises the selected complex moment. Cross-call cycles and longer exchange sequences remain open. + +## Object and move + +The source is the selected map in `research/complex-t16-rare-pattern-exchanges/data/`: 144 calls, 480 helper roles per call, 32,256 pending-child/port groups, and 69,120 whole-role placements. The package pins the accepted assembly/profile, source manifest, task catalogue, both exact moment engines, unchanged bit supplier and fixed-word packing ceiling. Seed, exact base, claim, priority revision and selected-record hash are in `TASK.json` and `RESULT.json`. + +At a single call, let three distinct occupied owner groups A, B and C have idle slacks `(rA,rB,rC)`. If their current roles have widths `(x,y,z)`, rotate them `A→B`, `B→C`, `C→A`. The new slacks are + +```text +(rA + x - z, rB + y - x, rC + z - y). +``` + +The same three groups remain occupied in that call, so the per-call physical-family set is preserved. Each group is already eligible at that call, and the exact nonnegative new slacks are the aggregate-capacity test. Reassigning consecutive offsets within each group compacts its hosted intervals without changing helper widths, call times, copies, frames, local paid ranks, precision or restoration work. The only possible cost change is the exact complex moment of the resulting idle-rank profile. + +## Exact result + +The verifier compresses role triples by their actual `(idle slack, outgoing width)` types, separately within every selected call. Multiplicity checks ensure repeated types still represent three distinct occupied groups. It exhausts: + +- 49,408 ordered supported type patterns; +- 4,417 patterns with nonnegative post-cycle slacks; +- 255 distinct ordered transfer states; +- 35 distinct old/new positive-rank histogram transitions. + +At the selected complex endpoint, the pinned Mercator and base-two engines certify 19 exact histogram ties and 16 strictly more expensive transitions. **There are no strictly cheaper same-call cycles.** The smallest strict increase is for histogram `1:2, 7:1 → 1:1, 2:1, 6:1`; its exact interval endpoints are in `RESULT.json` and a source witness is included there. A synthetic arithmetic control `0,3,3` with widths `9,8,9` gives `0,2,4` and strictly lowers both engine prices, checking the sign convention independently of the selected map. + +The selected complex endpoint is `67018507072324140917/40000000000000000000000`; the unchanged bit endpoint is `1733427039589844234749/10^24`, including its retained bad-residue surcharge. Both exact engines reproduce each supplier's endpoint and reject the next `10^-24` tick. The complex side still binds. No feasible cycle in this domain raises its endpoint, so the domain realizes **0%** of the fixed-word packing headroom. The selected-word relaxation remains `a < 1690054109089/10^15`, hence `κ < 1690054109089/1001690054109089` (decimal `0.0016872026453254019`). + +## Open next questions + +This is not a global packing optimum or an impossibility result for owner changes. It excludes cross-call cycles, paths into a free group, longer owner permutations, changed local words and alternative templates. PR #1790 identifies three-role cycles as the next question after its two-role census; this contribution closes only its same-call permutation subdomain on the selected PR1094 map. PR #1154 gives a positive three-owner cycle in the different PR1117 route, with a different local word and slack pattern; it does not census this map. The next finite step is an exact window/family join for cross-call cycles, starting with the seven rank-7 groups and requiring each target family to be free or vacated by another selected move at that call. + +## Reproduce + +From the repository root: + +```sh +python3 -B research/selected-t16-three-role-cycle-seedc375/verify.py +python3 -B research/selected-t16-three-role-cycle-seedc375/test_verify.py +python3 scripts/research_package.py --package research/selected-t16-three-role-cycle-seedc375 --check-only +python3 scripts/research_package.py --package research/selected-t16-three-role-cycle-seedc375 +``` + +Expected census: `49,408 / 4,417 / 255 / 35`, then `19` ties, `16` increases, and `0` decreases. The controls include a known improving algebra fixture, an over-capacity rejection, and a feasible selected-map cycle whose exact price increases. `research_package.py` checks source blobs against the pinned base before replay. + +## Credit + +The selected owner map and rare-pattern packing are Rohan Arun's PR #1094, retaining the PR #1087, PR #1018/#987 and Hao Yan PR #858 controller lineage. This package uses those frozen sources without changing the owner map or upstream data. The selected construction's other suppliers and assumptions remain as stated in the pinned review. Prepared by Codex with substantial OpenAI Codex assistance; new material is Apache-2.0. diff --git a/research/selected-t16-three-role-cycle-seedc375/RESULT.json b/research/selected-t16-three-role-cycle-seedc375/RESULT.json new file mode 100644 index 0000000000..631baf4869 --- /dev/null +++ b/research/selected-t16-three-role-cycle-seedc375/RESULT.json @@ -0,0 +1,1027 @@ +{ + "status": "SCOPED_NEGATIVE_RESULT_NO_IMPROVING_SAME_CALL_3_CYCLES", + "assignment": { + "seed": "c37585e64a1b0aaf41a29afcbfd3f5c7", + "track": "incumbent-optimization", + "task_id": "selected-packing", + "priority_revision": 3, + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "selected_record_sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32", + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-18923820" + }, + "overlap_snapshot": { + "refreshed_at": "2026-10-14T12:38:03Z/12:39:37Z", + "open_prs": 529, + "discussions": 508, + "complete_pagination": true, + "nearest_open_prs": [ + { + "number": 1790, + "head": "48ee04ee708081c8713e8868a370bbbf5aa099e1", + "scope": "selected PR1094 map two-role census; three-role cycles left open" + }, + { + "number": 1617, + "head": "536bc90ea2de310e0e08d2cb65f7add1d9de92b5", + "scope": "selected PR1094 neutral two-move census" + }, + { + "number": 1819, + "head": "eb519ed5b0013e03f4d9657730d57acee65cafd4", + "scope": "selected PR1094 neutral move followed by strict two-step gain" + }, + { + "number": 1154, + "head": "390de2866a03758e7f4ddbb2846e5b2ee4e72154", + "scope": "positive three-owner cycle on the different PR1117 route and changed local word" + } + ] + }, + "selected_source": { + "plan_sha256": "7bd786ba8e66408f02aa9ef446eaf20c1bfe981ea2e4dd1e5a929f0aa7767bc0", + "owners_sha256": "87902c528dfab7d503dcf8a784260e3ab6fb7424c418a1820f7261f25be7b6bc", + "calls": 144, + "roles_per_call": 480, + "owner_groups_in_capacity_model": 32256, + "whole_role_placements": 69120, + "positive_idle_remainders": { + "1": 2276, + "3": 377, + "7": 7, + "48": 4866 + } + }, + "census": { + "ordered_supported_type_patterns": 49408, + "capacity_feasible_type_patterns": 4417, + "unique_ordered_transfer_states": 255, + "distinct_rank_histogram_transitions": 35, + "equal_histogram_transitions": 19, + "strictly_more_expensive_transitions": 16, + "strictly_cheaper_transitions": 0, + "minimum_strict_increase": { + "old_histogram": [ + [ + 1, + 2 + ], + [ + 7, + 1 + ] + ], + "new_histogram": [ + [ + 1, + 1 + ], + [ + 2, + 1 + ], + [ + 6, + 1 + ] + ], + "mercator_delta": [ + "16077209283322400907982540599313238458801010109958486749783/6739986666787659948666753771754907668409286105635143120275902562304", + "32154418566644801815965081198626476917602020219916973499569/13479973333575319897333507543509815336818572211270286240551805124608" + ], + "base_two_delta": [ + "1192673671191767187297/500000000000000000000000000000", + "11926736711917671873/5000000000000000000000000000" + ], + "feasible_source_witness": { + "call": 124, + "old_slacks": [ + 1, + 1, + 7 + ], + "outgoing_widths": [ + 9, + 9, + 4 + ], + "new_slacks": [ + 6, + 1, + 2 + ], + "moves": [ + { + "helper": 44, + "source_group": [ + 7, + 15, + 111 + ], + "destination_group": [ + 7, + 15, + 110 + ], + "width": 9 + }, + { + "helper": 45, + "source_group": [ + 7, + 15, + 110 + ], + "destination_group": [ + 13, + 15, + 14 + ], + "width": 9 + }, + { + "helper": 69, + "source_group": [ + 13, + 15, + 14 + ], + "destination_group": [ + 7, + 15, + 111 + ], + "width": 4 + } + ] + } + }, + "all_transitions": [ + { + "old_histogram": [], + "new_histogram": [], + "classification": "exact-tie" + }, + { + "old_histogram": [ + [ + 1, + 1 + ] + ], + "new_histogram": [ + [ + 1, + 1 + ] + ], + "classification": "exact-tie" + }, + { + "old_histogram": [ + [ + 1, + 1 + ], + [ + 3, + 1 + ] + ], + "new_histogram": [ + [ + 1, + 1 + ], + [ + 3, + 1 + ] + ], + "classification": "exact-tie" + }, + { + "old_histogram": [ + [ + 1, + 1 + ], + [ + 3, + 1 + ] + ], + "new_histogram": [ + [ + 1, + 2 + ], + [ + 2, + 1 + ] + ], + "classification": "strict-increase", + "mercator_delta": [ + "10364717446954362540134158826443169358510239522293082191917/3369993333393829974333376885877453834204643052817571560137951281152", + "82917739575634900321073270611545354868081916178344657535341/26959946667150639794667015087019630673637144422540572481103610249216" + ], + "base_two_delta": [ + "3075589896350427898661/1000000000000000000000000000000", + "1537794948175213949333/500000000000000000000000000000" + ] + }, + { + "old_histogram": [ + [ + 1, + 1 + ], + [ + 3, + 1 + ], + [ + 7, + 1 + ] + ], + "new_histogram": [ + [ + 1, + 1 + ], + [ + 3, + 1 + ], + [ + 7, + 1 + ] + ], + "classification": "exact-tie" + }, + { + "old_histogram": [ + [ + 1, + 1 + ], + [ + 3, + 2 + ] + ], + "new_histogram": [ + [ + 1, + 1 + ], + [ + 3, + 2 + ] + ], + "classification": "exact-tie" + }, + { + "old_histogram": [ + [ + 1, + 1 + ], + [ + 7, + 1 + ] + ], + "new_histogram": [ + [ + 1, + 1 + ], + [ + 2, + 1 + ], + [ + 5, + 1 + ] + ], + "classification": "strict-increase", + "mercator_delta": [ + "90802090365412256426349236261038156987487284602949336016555/13479973333575319897333507543509815336818572211270286240551805124608", + "181604180730824512852698472522076313974974569205898672033115/26959946667150639794667015087019630673637144422540572481103610249216" + ], + "base_two_delta": [ + "1684018360393310938041/250000000000000000000000000000", + "6736073441573243752169/1000000000000000000000000000000" + ] + }, + { + "old_histogram": [ + [ + 1, + 1 + ], + [ + 7, + 1 + ] + ], + "new_histogram": [ + [ + 1, + 1 + ], + [ + 3, + 1 + ], + [ + 4, + 1 + ] + ], + "classification": "strict-increase", + "mercator_delta": [ + "103633109171278791045767101558258939647106685692883751040237/13479973333575319897333507543509815336818572211270286240551805124608", + "207266218342557582091534203116517879294213371385767502080479/26959946667150639794667015087019630673637144422540572481103610249216" + ], + "base_two_delta": [ + "7687931319059366212513/1000000000000000000000000000000", + "3843965659529683106259/500000000000000000000000000000" + ] + }, + { + "old_histogram": [ + [ + 1, + 1 + ], + [ + 7, + 1 + ] + ], + "new_histogram": [ + [ + 1, + 1 + ], + [ + 7, + 1 + ] + ], + "classification": "exact-tie" + }, + { + "old_histogram": [ + [ + 1, + 1 + ], + [ + 7, + 1 + ] + ], + "new_histogram": [ + [ + 1, + 2 + ], + [ + 6, + 1 + ] + ], + "classification": "strict-increase", + "mercator_delta": [ + "124540958723002532148176013469166323708294528537197176137033/26959946667150639794667015087019630673637144422540572481103610249216", + "62270479361501266074088006734583161854147264268598588068519/13479973333575319897333507543509815336818572211270286240551805124608" + ], + "base_two_delta": [ + "4619480901078692571351/1000000000000000000000000000000", + "1154870225269673142839/250000000000000000000000000000" + ] + }, + { + "old_histogram": [ + [ + 1, + 1 + ], + [ + 7, + 1 + ] + ], + "new_histogram": [ + [ + 2, + 1 + ], + [ + 3, + 2 + ] + ], + "classification": "strict-increase", + "mercator_delta": [ + "30584112867255703710470623766418258423110474602157042781563/3369993333393829974333376885877453834204643052817571560137951281152", + "244672902938045629683764990131346067384883796817256342252509/26959946667150639794667015087019630673637144422540572481103610249216" + ], + "base_two_delta": [ + "4537711182421726522961/500000000000000000000000000000", + "9075422364843453045927/1000000000000000000000000000000" + ] + }, + { + "old_histogram": [ + [ + 1, + 1 + ], + [ + 7, + 1 + ] + ], + "new_histogram": [ + [ + 2, + 1 + ], + [ + 6, + 1 + ] + ], + "classification": "strict-increase", + "mercator_delta": [ + "64308837133289603631930162397252953835204040439833946999133/26959946667150639794667015087019630673637144422540572481103610249216", + "64308837133289603631930162397252953835204040439833946999137/26959946667150639794667015087019630673637144422540572481103610249216" + ], + "base_two_delta": [ + "477069468476706874919/200000000000000000000000000000", + "2385347342383534374599/1000000000000000000000000000000" + ] + }, + { + "old_histogram": [ + [ + 1, + 1 + ], + [ + 7, + 1 + ] + ], + "new_histogram": [ + [ + 2, + 2 + ], + [ + 4, + 1 + ] + ], + "classification": "strict-increase", + "mercator_delta": [ + "28743979541059944237045202832018733036150599933343616309739/3369993333393829974333376885877453834204643052817571560137951281152", + "229951836328479553896361622656149864289204799466748930477917/26959946667150639794667015087019630673637144422540572481103610249216" + ], + "base_two_delta": [ + "426469382835731795721/50000000000000000000000000000", + "341175506268585436577/40000000000000000000000000000" + ] + }, + { + "old_histogram": [ + [ + 1, + 1 + ], + [ + 7, + 2 + ] + ], + "new_histogram": [ + [ + 1, + 1 + ], + [ + 7, + 2 + ] + ], + "classification": "exact-tie" + }, + { + "old_histogram": [ + [ + 1, + 2 + ] + ], + "new_histogram": [ + [ + 1, + 2 + ] + ], + "classification": "exact-tie" + }, + { + "old_histogram": [ + [ + 1, + 2 + ], + [ + 3, + 1 + ] + ], + "new_histogram": [ + [ + 1, + 2 + ], + [ + 3, + 1 + ] + ], + "classification": "exact-tie" + }, + { + "old_histogram": [ + [ + 1, + 2 + ], + [ + 7, + 1 + ] + ], + "new_histogram": [ + [ + 1, + 1 + ], + [ + 2, + 1 + ], + [ + 6, + 1 + ] + ], + "classification": "strict-increase", + "mercator_delta": [ + "16077209283322400907982540599313238458801010109958486749783/6739986666787659948666753771754907668409286105635143120275902562304", + "32154418566644801815965081198626476917602020219916973499569/13479973333575319897333507543509815336818572211270286240551805124608" + ], + "base_two_delta": [ + "1192673671191767187297/500000000000000000000000000000", + "11926736711917671873/5000000000000000000000000000" + ] + }, + { + "old_histogram": [ + [ + 1, + 2 + ], + [ + 7, + 1 + ] + ], + "new_histogram": [ + [ + 1, + 2 + ], + [ + 7, + 1 + ] + ], + "classification": "exact-tie" + }, + { + "old_histogram": [ + [ + 1, + 3 + ] + ], + "new_histogram": [ + [ + 1, + 3 + ] + ], + "classification": "exact-tie" + }, + { + "old_histogram": [ + [ + 3, + 1 + ] + ], + "new_histogram": [ + [ + 1, + 1 + ], + [ + 2, + 1 + ] + ], + "classification": "strict-increase", + "mercator_delta": [ + "82917739575634900321073270611545354868081916178344657535337/26959946667150639794667015087019630673637144422540572481103610249216", + "20729434893908725080268317652886338717020479044586164383835/6739986666787659948666753771754907668409286105635143120275902562304" + ], + "base_two_delta": [ + "1537794948175213949331/500000000000000000000000000000", + "615117979270085579733/200000000000000000000000000000" + ] + }, + { + "old_histogram": [ + [ + 3, + 1 + ] + ], + "new_histogram": [ + [ + 3, + 1 + ] + ], + "classification": "exact-tie" + }, + { + "old_histogram": [ + [ + 3, + 1 + ], + [ + 7, + 1 + ] + ], + "new_histogram": [ + [ + 3, + 1 + ], + [ + 7, + 1 + ] + ], + "classification": "exact-tie" + }, + { + "old_histogram": [ + [ + 3, + 1 + ], + [ + 7, + 2 + ] + ], + "new_histogram": [ + [ + 3, + 1 + ], + [ + 7, + 2 + ] + ], + "classification": "exact-tie" + }, + { + "old_histogram": [ + [ + 3, + 2 + ] + ], + "new_histogram": [ + [ + 1, + 1 + ], + [ + 2, + 1 + ], + [ + 3, + 1 + ] + ], + "classification": "strict-increase", + "mercator_delta": [ + "10364717446954362540134158826443169358510239522293082191917/3369993333393829974333376885877453834204643052817571560137951281152", + "82917739575634900321073270611545354868081916178344657535341/26959946667150639794667015087019630673637144422540572481103610249216" + ], + "base_two_delta": [ + "3075589896350427898661/1000000000000000000000000000000", + "1537794948175213949333/500000000000000000000000000000" + ] + }, + { + "old_histogram": [ + [ + 3, + 2 + ] + ], + "new_histogram": [ + [ + 3, + 2 + ] + ], + "classification": "exact-tie" + }, + { + "old_histogram": [ + [ + 3, + 2 + ], + [ + 7, + 1 + ] + ], + "new_histogram": [ + [ + 3, + 2 + ], + [ + 7, + 1 + ] + ], + "classification": "exact-tie" + }, + { + "old_histogram": [ + [ + 3, + 3 + ] + ], + "new_histogram": [ + [ + 3, + 3 + ] + ], + "classification": "exact-tie" + }, + { + "old_histogram": [ + [ + 7, + 1 + ] + ], + "new_histogram": [ + [ + 1, + 1 + ], + [ + 2, + 1 + ], + [ + 4, + 1 + ] + ], + "classification": "strict-increase", + "mercator_delta": [ + "290183957918192482412607473728063234162295287564112159615813/26959946667150639794667015087019630673637144422540572481103610249216", + "290183957918192482412607473728063234162295287564112159615817/26959946667150639794667015087019630673637144422540572481103610249216" + ], + "base_two_delta": [ + "10763521215409794111177/1000000000000000000000000000000", + "10763521215409794111181/1000000000000000000000000000000" + ] + }, + { + "old_histogram": [ + [ + 7, + 1 + ] + ], + "new_histogram": [ + [ + 1, + 1 + ], + [ + 3, + 2 + ] + ], + "classification": "strict-increase", + "mercator_delta": [ + "304905024527758558200010841203259437257974284914619571390405/26959946667150639794667015087019630673637144422540572481103610249216", + "304905024527758558200010841203259437257974284914619571390409/26959946667150639794667015087019630673637144422540572481103610249216" + ], + "base_two_delta": [ + "11309555923538611242679/1000000000000000000000000000000", + "11309555923538611242683/1000000000000000000000000000000" + ] + }, + { + "old_histogram": [ + [ + 7, + 1 + ] + ], + "new_histogram": [ + [ + 1, + 1 + ], + [ + 6, + 1 + ] + ], + "classification": "strict-increase", + "mercator_delta": [ + "62270479361501266074088006734583161854147264268598588068517/13479973333575319897333507543509815336818572211270286240551805124608", + "124540958723002532148176013469166323708294528537197176137037/26959946667150639794667015087019630673637144422540572481103610249216" + ], + "base_two_delta": [ + "577435112634836571419/125000000000000000000000000000", + "923896180215738514271/200000000000000000000000000000" + ] + }, + { + "old_histogram": [ + [ + 7, + 1 + ] + ], + "new_histogram": [ + [ + 2, + 1 + ], + [ + 5, + 1 + ] + ], + "classification": "strict-increase", + "mercator_delta": [ + "181604180730824512852698472522076313974974569205898672033111/26959946667150639794667015087019630673637144422540572481103610249216", + "90802090365412256426349236261038156987487284602949336016557/13479973333575319897333507543509815336818572211270286240551805124608" + ], + "base_two_delta": [ + "1347214688314648750433/200000000000000000000000000000", + "842009180196655469021/125000000000000000000000000000" + ] + }, + { + "old_histogram": [ + [ + 7, + 1 + ] + ], + "new_histogram": [ + [ + 2, + 2 + ], + [ + 3, + 1 + ] + ], + "classification": "strict-increase", + "mercator_delta": [ + "327590642513680530004838260742891422252965712995600999787843/26959946667150639794667015087019630673637144422540572481103610249216", + "327590642513680530004838260742891422252965712995600999787847/26959946667150639794667015087019630673637144422540572481103610249216" + ], + "base_two_delta": [ + "6075506130596940472293/500000000000000000000000000000", + "1215101226119388094459/100000000000000000000000000000" + ] + }, + { + "old_histogram": [ + [ + 7, + 1 + ] + ], + "new_histogram": [ + [ + 3, + 1 + ], + [ + 4, + 1 + ] + ], + "classification": "strict-increase", + "mercator_delta": [ + "207266218342557582091534203116517879294213371385767502080475/26959946667150639794667015087019630673637144422540572481103610249216", + "103633109171278791045767101558258939647106685692883751040239/13479973333575319897333507543509815336818572211270286240551805124608" + ], + "base_two_delta": [ + "3843965659529683106257/500000000000000000000000000000", + "7687931319059366212517/1000000000000000000000000000000" + ] + }, + { + "old_histogram": [ + [ + 7, + 1 + ] + ], + "new_histogram": [ + [ + 7, + 1 + ] + ], + "classification": "exact-tie" + }, + { + "old_histogram": [ + [ + 7, + 2 + ] + ], + "new_histogram": [ + [ + 7, + 2 + ] + ], + "classification": "exact-tie" + } + ] + }, + "supplier_prices": { + "complex_endpoint": "67018507072324140917/40000000000000000000000", + "complex_moment_upper_below_one": true, + "complex_next_tick_lower_above_one": true, + "bit_endpoint": "1733427039589844234749/1000000000000000000000000", + "bit_moment_upper_below_one_with_selected_surcharge": true, + "bit_next_tick_lower_above_one_with_selected_surcharge": true, + "bit_profile_sha256": "b9f0e5ca038abe837b0007c8fe006f366a6f02009244ac57705a8a200e2301f4", + "binding_side": "complex" + }, + "packing_cap": { + "a_upper_bound": "1690054109089/1000000000000000", + "kappa_upper_bound": "1690054109089/1001690054109089", + "selected_kappa": "836330098538459/500000000000000000", + "remaining_kappa_headroom": "7283512886451269093752046149/500845027054544500000000000000000", + "headroom_realized_by_this_domain": "0", + "fraction_of_packing_headroom_realized": "0" + }, + "scope_limit": "One same-invocation three-role permutation among three distinct currently occupied groups. Cross-call cycles, chains, longer sequences, changed local words and a global packing optimum are not covered." +} diff --git a/research/selected-t16-three-role-cycle-seedc375/SOURCES.json b/research/selected-t16-three-role-cycle-seedc375/SOURCES.json new file mode 100644 index 0000000000..b68d663ebb --- /dev/null +++ b/research/selected-t16-three-role-cycle-seedc375/SOURCES.json @@ -0,0 +1,78 @@ +{ + "schema_version": 1, + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "06c96f5579bb67ed1b86d334e78fbed7da6945f1", + "sha256": "6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075" + }, + { + "path": "docs/research/community-batch1099-review.md", + "usage": "provenance", + "git_blob": "6cb6ec061a071a06a2d18cd4dc3e9a2b05d28099", + "sha256": "7e76d2c38e5fce30587835b7251df1430488ae4dd372611ef69a3f03f476b6cb" + }, + { + "path": "research/community-frontier1094-audit/ASSEMBLY.json", + "usage": "input", + "git_blob": "5fd676df060f3b450782fdf5ff5f6beb63a5eeb0", + "sha256": "1122cb3a575f8c788345fc1bf4c108ac7c3250fb81a5988671f5eb04b3ab3045" + }, + { + "path": "research/community-frontier1094-audit/SELECTED-SOURCE.json", + "usage": "provenance", + "git_blob": "6a75493790b4eff9c4a98051ef8b01d6aad0d5a8", + "sha256": "79b3de5db3dbcb9829789ba58e9e45758926031e2a7d80667a08429d369be53b" + }, + { + "path": "research/complex-k492-owner-repair/vendor/multicold/engines/base_two_moment.py", + "usage": "input", + "git_blob": "14a90fa0e788217856f070382c9e61bd7c603c61", + "sha256": "aee70c242a2f1d225528fabe2002e1564d1dc884797c07d28a831c7878ee9098" + }, + { + "path": "research/complex-k492-owner-repair/vendor/multicold/engines/moment.py", + "usage": "input", + "git_blob": "7d697cb45203fe72d97037403d6da41f71f3b7fd", + "sha256": "81cbc864e106418fc7854322746f72180cb8110ff39f74450a3b8d55a82c1482" + }, + { + "path": "research/complex-local-word-ceiling/RESULT.json", + "usage": "input", + "git_blob": "77f55043a679dd722330f1e2499863e36376d9f9", + "sha256": "d91d6c46509875abf1f61de67c2609656d3dc685451299f83caa6f922493692d" + }, + { + "path": "research/complex-t16-rare-pattern-exchanges/README.md", + "usage": "provenance", + "git_blob": "f205b7132243aedcb2aa85110a44f0c8cd1e4fe1", + "sha256": "da542711a6a3eb01ce1ebdf8f28a748e6195512687f61d003b95ac5ff281a7b2" + }, + { + "path": "research/complex-t16-rare-pattern-exchanges/data/OWNERS.json.gz", + "usage": "input", + "git_blob": "d3ba33d7e703a3229d9fb8a360f69d2f318bbb70", + "sha256": "87902c528dfab7d503dcf8a784260e3ab6fb7424c418a1820f7261f25be7b6bc" + }, + { + "path": "research/complex-t16-rare-pattern-exchanges/data/PLAN.json", + "usage": "input", + "git_blob": "f1bec76e8e9b7a1f09c1e05cb6cce973b6e59f1b", + "sha256": "7bd786ba8e66408f02aa9ef446eaf20c1bfe981ea2e4dd1e5a929f0aa7767bc0" + }, + { + "path": "research/e8-bit-p111-tuned/tune/EXPECTED.json", + "usage": "input", + "git_blob": "e293ddc557742637f9f679f083a1a282d87b1b13", + "sha256": "b9f0e5ca038abe837b0007c8fe006f366a6f02009244ac57705a8a200e2301f4" + } + ] +} diff --git a/research/selected-t16-three-role-cycle-seedc375/TASK.json b/research/selected-t16-three-role-cycle-seedc375/TASK.json new file mode 100644 index 0000000000..9ea2faecf5 --- /dev/null +++ b/research/selected-t16-three-role-cycle-seedc375/TASK.json @@ -0,0 +1,97 @@ +{ + "schema_version": 1, + "task_id": "selected-packing", + "priority_revision": 3, + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "original_card": { + "id": "selected-packing", + "question": "Is there a genuinely unsearched, explicitly bounded improvement to the selected packing?", + "starting_points": [ + "certificates/selected-result.json", + "research/heterogeneous-owner-assembly/README.md", + "research/complex-local-word-ceiling/README.md" + ], + "methods": [ + "Search a named unclaimed canonical candidate domain with a reproducible partition.", + "Prove a stronger scoped relaxation or exact optimum for one named residual subproblem." + ], + "acceptance_gate": "Check live PR overlap first, price both suppliers and distinguish a search best from an optimum. Report the word's packing cap from ceiling.ceiling() and the fraction of it realized; label packing gains as such.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Locate the selected packing source in the review and check live PRs for the same residual problem.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Define an unclaimed canonical domain and a favorable bound before starting a new search.", + "bottleneck_link": "An actual paid-profile gain can improve the frontier up to the other supplier cap.", + "allowed_variations": [ + "One bounded residual packing instance or exact relaxation.", + "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope." + ], + "scope_change_triggers": [ + "Rerunning an existing search with only a different seed as a separate mathematical contribution." + ], + "overlap_terms": [ + "T16", + "owner exchange", + "packing" + ] + }, + "scope_status": "refined", + "actual_scope": "Exact census of same-invocation 3-cycle owner permutations among three distinct occupied groups in the selected PR1094 T16 map; only the complex idle-rank moment may change.", + "scope_change_reason": "Refines the selected-packing card to the direct same-call subdomain of the broader three-role cyclic-transfer question left open by PR1790. Every move permutes three existing roles among the same three already eligible families in one invocation, making the capacity and family checks exact and finite. Cross-call cycles and longer sequences are excluded. The positive three-owner cycle in PR #1154 is on the different PR1117 route with a different local word and slack pattern; it does not cover the selected PR1094 map census here.", + "bottleneck_link": "The selected complex supplier binds. A cheaper idle remainder profile could raise its moment endpoint; the bit supplier remains fixed. This exact census finds no strictly cheaper same-call 3-cycle, so the domain realizes 0 percent of the fixed-word packing headroom.", + "budget_minutes": 60, + "stop_rule": "Exhaust all ordered supported (remainder,width) type triples in each of the selected map's 144 calls, check exact nonnegative post-cycle slacks, and compare every distinct resulting rank-histogram transition with the selected complex moment at its certified endpoint using both pinned rational moment engines. Stop this domain if every transition is an exact tie or strictly more expensive; do not generalize to cross-call or longer cycles.", + "outcome": "negative-result", + "evidence": "Selected PR1094 T16 source map: 49,408 supported ordered type patterns, 4,417 capacity-feasible patterns, 255 distinct transfer states, and 35 distinct old/new idle-rank histogram transitions. The two exact engines certify 19 histogram ties and 16 strictly more expensive transitions; none lowers the selected complex moment. A concrete cost-improving algebra fixture and a feasible worsening source witness test the price sign. Both selected suppliers are source-priced; bit is unchanged, complex binds, no new kappa.", + "author": "Codex", + "ai_assistance": "Prepared with substantial OpenAI Codex assistance: source-bounded search design, exact type census, rational interval pricing, verifier, tests, and packaging. Prior owner map/construction credits are retained in README.", + "open_questions": [ + { + "question": "Can cross-call three-role cycles lower idle cost when each destination family is either free at that call or vacated by a simultaneous selected move?", + "why_it_matters": "This extends the no-improvement result beyond same-call permutations and is the remaining direct three-role owner-transfer class identified by PR1790.", + "first_step": "Build an exact join over source role times, destination windows, current family occupancy, and the three affected group slacks; first screen the seven rank-7 groups before any broader search.", + "blocked_by": "A target group already occupied by a nonmoving role in that call is illegal; the same-call type census does not certify cross-call compatibility." + } + ], + "accepted_seed": "c37585e64a1b0aaf41a29afcbfd3f5c7", + "track": "incumbent-optimization", + "catalog_sha256": "6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075", + "selected_record_sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32", + "discussion_claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-18923820", + "discussion_claim_expiry_utc": "2026-10-14T13:25:00Z", + "nearest_overlaps": [ + { + "pr": 1790, + "head": "48ee04ee708081c8713e8868a370bbbf5aa099e1", + "scope": "selected PR1094 map two-role census; three-role cycles left open" + }, + { + "pr": 1617, + "head": "536bc90ea2de310e0e08d2cb65f7add1d9de92b5", + "scope": "selected PR1094 neutral two-move census" + }, + { + "pr": 1819, + "head": "eb519ed5b0013e03f4d9657730d57acee65cafd4", + "scope": "selected PR1094 neutral move followed by strict two-step gain" + }, + { + "pr": 1154, + "head": "390de2866a03758e7f4ddbb2846e5b2ee4e72154", + "scope": "positive three-owner cycle on different PR1117 route and changed local word" + } + ], + "overlap_snapshot": { + "open_prs": 529, + "discussions": 508, + "fetched_open_prs_utc": "2026-10-14T12:38:03.905789Z", + "fetched_discussions_utc": "2026-10-14T12:39:37.492279Z", + "complete_pagination": true + } +} diff --git a/research/selected-t16-three-role-cycle-seedc375/VERIFY.json b/research/selected-t16-three-role-cycle-seedc375/VERIFY.json new file mode 100644 index 0000000000..e48eb3bf50 --- /dev/null +++ b/research/selected-t16-three-role-cycle-seedc375/VERIFY.json @@ -0,0 +1,35 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/complex-t16-rare-pattern-exchanges/data/PLAN.json", + "research/complex-t16-rare-pattern-exchanges/data/OWNERS.json.gz", + "research/community-frontier1094-audit/ASSEMBLY.json", + "research/complex-local-word-ceiling/RESULT.json", + "research/e8-bit-p111-tuned/tune/EXPECTED.json", + "research/complex-k492-owner-repair/vendor/multicold/engines/moment.py", + "research/complex-k492-owner-repair/vendor/multicold/engines/base_two_moment.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Source hashes, complete selected T16 map geometry and call invariants, all compressed same-call three-role type patterns, exact post-cycle slacks, every distinct rank-profile transition under both pinned exact moment engines, selected bit and complex endpoints, fixed-word packing cap, and deterministic RESULT.json." + }, + { + "argv": [ + "{python}", + "-B", + "{package}/test_verify.py" + ], + "timeout_seconds": 60, + "checks": "Positive strict-cost-reduction arithmetic fixture, over-capacity rejection, exact census totals, and a feasible source witness whose cycle strictly raises the priced moment." + } + ] +} diff --git a/research/selected-t16-three-role-cycle-seedc375/test_verify.py b/research/selected-t16-three-role-cycle-seedc375/test_verify.py new file mode 100644 index 0000000000..abeea340fc --- /dev/null +++ b/research/selected-t16-three-role-cycle-seedc375/test_verify.py @@ -0,0 +1,60 @@ +"""Positive and rejecting controls for the bounded owner-cycle census.""" +from fractions import Fraction as Q +import importlib.util +from pathlib import Path +import unittest + +_spec = importlib.util.spec_from_file_location("same_call_cycle_verify", Path(__file__).with_name("verify.py")) +verify = importlib.util.module_from_spec(_spec) +_spec.loader.exec_module(verify) + + +class ThreeRoleCycleTests(unittest.TestCase): + @classmethod + def setUpClass(cls): + cls.result = verify.verify() + + def test_selected_domain_has_no_improving_transition(self): + census = self.result["census"] + self.assertEqual(census["ordered_supported_type_patterns"], 49408) + self.assertEqual(census["capacity_feasible_type_patterns"], 4417) + self.assertEqual(census["unique_ordered_transfer_states"], 255) + self.assertEqual(census["distinct_rank_histogram_transitions"], 35) + self.assertEqual(census["equal_histogram_transitions"], 19) + self.assertEqual(census["strictly_more_expensive_transitions"], 16) + self.assertEqual(census["strictly_cheaper_transitions"], 0) + + def test_known_majorizing_fixture_reduces_both_exact_prices(self): + old = (0, 3, 3) + widths = (9, 8, 9) + new = verify.cycle_slacks(old, widths) + self.assertEqual(new, (0, 2, 4)) + assembly = verify.read_json(verify.ASSEMBLY_PATH) + alpha = Q(assembly["complex_lower"]) + M = verify.load_engine(verify.MOMENT_PATH, "positive_control_moment") + B = verify.load_engine(verify.BASE_TWO_PATH, "positive_control_base_two") + old_hist, new_hist = verify.rank_histogram(old), verify.rank_histogram(new) + ranks = set(dict(old_hist)) | set(dict(new_hist)) + for engine_name, values in ( + ("Mercator", {r: M.moment({r: 1}, verify.M, verify.W, alpha, False) for r in ranks}), + ("base-two", {r: B.moment(verify.M, verify.W, [(r, 1)], alpha) for r in ranks}), + ): + delta = verify.interval_difference(old_hist, new_hist, values, engine_name) + self.assertLess(Q(delta["upper"]), 0, engine_name) + + def test_negative_capacity_control_rejects_overflow(self): + new = verify.cycle_slacks((0, 0, 0), (9, 4, 7)) + self.assertLess(min(new), 0) + + def test_real_source_witness_is_strictly_worse(self): + witness = self.result["census"]["minimum_strict_increase"]["feasible_source_witness"] + groups = {tuple(move["source_group"]) for move in witness["moves"]} + destinations = {tuple(move["destination_group"]) for move in witness["moves"]} + self.assertEqual(len(groups), 3) + self.assertEqual(destinations, groups) + for engine in ("mercator_delta", "base_two_delta"): + self.assertGreater(Q(self.result["census"]["minimum_strict_increase"][engine][0]), 0) + + +if __name__ == "__main__": + unittest.main() diff --git a/research/selected-t16-three-role-cycle-seedc375/verify.py b/research/selected-t16-three-role-cycle-seedc375/verify.py new file mode 100644 index 0000000000..ff37870b69 --- /dev/null +++ b/research/selected-t16-three-role-cycle-seedc375/verify.py @@ -0,0 +1,412 @@ +"""Exact census of selected-map, same-invocation three-owner cycles. + +This is a scoped negative result. It does not search cross-call cycles or +longer owner-exchange sequences. The selected source map and both moment +engines are pinned in SOURCES.json and checked against the frozen base by +scripts/research_package.py. +""" +from collections import Counter, defaultdict +from fractions import Fraction as Q +import gzip +import hashlib +import importlib.util +import json +from pathlib import Path +import sys + + +ROOT = Path(__file__).resolve().parents[2] +HERE = Path(__file__).resolve().parent +PLAN_PATH = "research/complex-t16-rare-pattern-exchanges/data/PLAN.json" +OWNERS_PATH = "research/complex-t16-rare-pattern-exchanges/data/OWNERS.json.gz" +ASSEMBLY_PATH = "research/community-frontier1094-audit/ASSEMBLY.json" +SELECTED_PATH = "certificates/selected-result.json" +CEILING_PATH = "research/complex-local-word-ceiling/RESULT.json" +BIT_PATH = "research/e8-bit-p111-tuned/tune/EXPECTED.json" +MOMENT_PATH = "research/complex-k492-owner-repair/vendor/multicold/engines/moment.py" +BASE_TWO_PATH = "research/complex-k492-owner-repair/vendor/multicold/engines/base_two_moment.py" +V = 112 +HELPERS = 480 +CALLS = 144 +M = 73 +W = 14336 +ALPHA_DENOMINATOR_TICK = 10**24 + +PINS = { + PLAN_PATH: "7bd786ba8e66408f02aa9ef446eaf20c1bfe981ea2e4dd1e5a929f0aa7767bc0", + OWNERS_PATH: "87902c528dfab7d503dcf8a784260e3ab6fb7424c418a1820f7261f25be7b6bc", + ASSEMBLY_PATH: "1122cb3a575f8c788345fc1bf4c108ac7c3250fb81a5988671f5eb04b3ab3045", + SELECTED_PATH: "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32", + CEILING_PATH: "d91d6c46509875abf1f61de67c2609656d3dc685451299f83caa6f922493692d", + BIT_PATH: "b9f0e5ca038abe837b0007c8fe006f366a6f02009244ac57705a8a200e2301f4", + MOMENT_PATH: "81cbc864e106418fc7854322746f72180cb8110ff39f74450a3b8d55a82c1482", + BASE_TWO_PATH: "aee70c242a2f1d225528fabe2002e1564d1dc884797c07d28a831c7878ee9098", +} + + +def require(condition, message): + if not condition: + raise AssertionError(message) + + +def read_json(relative): + return json.loads((ROOT / relative).read_text(encoding="utf-8")) + + +def load_engine(relative, module_name): + spec = importlib.util.spec_from_file_location(module_name, ROOT / relative) + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + return module + + +def rank_histogram(values): + return tuple(sorted(Counter(r for r in values if r > 0).items())) + + +def cycle_slacks(old, widths): + """A(width x)->B, B(width y)->C, C(width z)->A.""" + ra, rb, rc = old + x, y, z = widths + return (ra + x - z, rb + y - x, rc + z - y) + + +def distinct_type_support(types, counts): + return all(counts[t] >= n for t, n in Counter(types).items()) + + +def interval_difference(old_hist, new_hist, rank_costs, engine_name): + """Certified interval for cost(new)-cost(old), with rank 0 priced as zero.""" + old, new = dict(old_hist), dict(new_hist) + lower = sum(n * rank_costs[r][0] for r, n in new.items()) + lower -= sum(n * rank_costs[r][1] for r, n in old.items()) + upper = sum(n * rank_costs[r][1] for r, n in new.items()) + upper -= sum(n * rank_costs[r][0] for r, n in old.items()) + return {"lower": str(lower), "upper": str(upper), "engine": engine_name} + + +def selected_supplier_receipts(plan, assembly, bit_data, M_engine, B_engine): + complex_profile = {int(r): int(n) for r, n in assembly["complex_profile"].items()} + require(complex_profile == {int(r): int(n) for r, n in plan["profile"].items()}, + "selected PLAN and accepted assembly profile differ") + alpha = Q(assembly["complex_lower"]) + bit = bit_data["nine"] + bit_profile = {int(r): int(n) for r, n in bit["profile"].items()} + bit_alpha = Q(bit["bit_lower"]) + + def paired_moment(profile, m, live, at, bad): + mercator = M_engine.moment(profile, m, live, at, bad) + base_two = B_engine.moment(m, live, list(profile.items()), at) + if bad: + surcharge_profile = [(1, 32 * m * m * sum(profile.values()))] + sl, su = B_engine.moment(m, live, surcharge_profile, at) + base_two = (base_two[0] + sl / 10**16, base_two[1] + su / 10**16) + return mercator, base_two + + complex_now = paired_moment(complex_profile, M, W, alpha, False) + complex_next = paired_moment(complex_profile, M, W, + alpha + Q(1, ALPHA_DENOMINATOR_TICK), False) + require(complex_now[0][0] - 1 == Q(assembly["moments"][2]["mercator"][0]), + "selected complex Mercator lower receipt mismatch") + require(complex_now[0][1] - 1 == Q(assembly["moments"][2]["mercator"][1]), + "selected complex Mercator upper receipt mismatch") + require(complex_now[1][0] - 1 == Q(assembly["moments"][2]["base_two"][0]), + "selected complex base-two lower receipt mismatch") + require(complex_now[1][1] - 1 == Q(assembly["moments"][2]["base_two"][1]), + "selected complex base-two upper receipt mismatch") + require(complex_now[0][1] < 1 and complex_now[1][1] < 1, + "selected complex endpoint does not pass") + require(complex_next[0][0] > 1 and complex_next[1][0] > 1, + "selected complex next tick is not rejected") + + bit_live = int(bit["bit"]["live"]) + bit_now = paired_moment(bit_profile, 64, bit_live, bit_alpha, True) + bit_next = paired_moment(bit_profile, 64, bit_live, + bit_alpha + Q(1, ALPHA_DENOMINATOR_TICK), True) + require(str(bit_alpha) == assembly["bit_lower"], "selected bit endpoint differs") + require(bit_now[0][1] < 1 and bit_now[1][1] < 1, + "unchanged bit supplier endpoint does not pass") + require(bit_next[0][0] > 1 and bit_next[1][0] > 1, + "unchanged bit supplier next tick is not rejected") + return { + "complex_endpoint": str(alpha), + "complex_moment_upper_below_one": True, + "complex_next_tick_lower_above_one": True, + "bit_endpoint": str(bit_alpha), + "bit_moment_upper_below_one_with_selected_surcharge": True, + "bit_next_tick_lower_above_one_with_selected_surcharge": True, + "bit_profile_sha256": PINS[BIT_PATH], + "binding_side": assembly["binding"], + } + + +def load_and_check_map(): + plan = read_json(PLAN_PATH) + with gzip.open(ROOT / OWNERS_PATH, "rt", encoding="utf-8") as stream: + owners = json.load(stream) + require((plan["K"], plan["T"], plan["M"], plan["L"], plan["live"]) == (4, 16, 73, 9, 14336), + "not the pinned selected T16 geometry") + order = [tuple(c) for c in plan["order"]] + require(len(order) == CALLS and len(set(order)) == CALLS, "call order is incomplete") + caps = {} + windows = {} + family_of = {} + for key, (cap, times) in plan["windows"].items(): + owner_replica, child = map(int, key.split(",")) + require(len(times) == len(set(times)), "duplicate call in a group window") + for port in range(V): + g = (owner_replica, child, port) + caps[g] = int(cap) + windows[g] = set(times) + family_of[g] = (owner_replica * 8 * V + + (2 * plan["pairs"][str(child)] + plan["sides"][str(child)]) * V + + port) + used = Counter() + by_call = defaultdict(list) + group_at_call = {} + widths_by_helper = {} + for z in owners: + t, h = int(z["time"]), int(z["helper"]) + g = (int(z["owner_replica"]), int(z["child"]), int(z["port"])) + require(0 <= t < CALLS and 0 <= h < HELPERS, "role outside the selected domain") + require((int(z["stage"]), int(z["replica"])) == order[t], "role call key mismatch") + require(g in caps and t in windows[g], "role violates its selected window") + require(int(z["width"]) > 0, "nonpositive helper width") + require(int(z["copy"]) == g[0] * V + g[2], "copy-coordinate mismatch") + require(int(z["family"]) == family_of[g], "physical-family mismatch") + require((g, t) not in group_at_call, "more than one role in a group at one call") + group_at_call[(g, t)] = z + previous = widths_by_helper.setdefault(h, int(z["width"])) + require(previous == int(z["width"]), "helper width changes across calls") + used[g] += int(z["width"]) + by_call[t].append(z) + require(len(owners) == CALLS * HELPERS, "owner role inventory count mismatch") + require(set(widths_by_helper) == set(range(HELPERS)), "helper IDs are not complete") + require(all(len(by_call[t]) == HELPERS for t in range(CALLS)), "a call has the wrong role count") + for t, roles in by_call.items(): + require(len({int(z["helper"]) for z in roles}) == HELPERS, "helper repeated in one call") + require(len({int(z["family"]) for z in roles}) == HELPERS, + "physical family repeated in one call") + require(all(used[g] <= cap for g, cap in caps.items()), "selected owner map exceeds a group capacity") + remainder = {g: cap - used[g] for g, cap in caps.items()} + require(all(r >= 0 for r in remainder.values()), "negative source slack") + idle_histogram = Counter(remainder.values()) + idle_histogram.pop(0, None) + expected_idle = {1: 2276, 3: 377, 7: 7, 48: 4866} + require(dict(sorted(idle_histogram.items())) == expected_idle, + "selected owner-map idle histogram mismatch") + return plan, owners, caps, windows, family_of, remainder, by_call, group_at_call + + +def find_exact_domain(plan, owners, caps, windows, family_of, remainder, by_call, + group_at_call, assembly, M_engine, B_engine): + alpha = Q(assembly["complex_lower"]) + full_profile = {int(r): int(n) for r, n in assembly["complex_profile"].items()} + rank_costs = {} + ranks_needed = set(full_profile) + for r in range(1, 49): + mercator = M_engine.moment({r: 1}, M, W, alpha, False) + base_two = B_engine.moment(M, W, [(r, 1)], alpha) + rank_costs[r] = (mercator, base_two) + + supported_patterns = capacity_feasible_patterns = 0 + transfer_states = set() + witnesses_by_transition = {} + for t in range(CALLS): + members = defaultdict(list) + for z in by_call[t]: + g = (int(z["owner_replica"]), int(z["child"]), int(z["port"])) + typ = (remainder[g], int(z["width"])) + members[typ].append(z) + counts = Counter({typ: len(rows) for typ, rows in members.items()}) + for type_a, type_b, type_c in __import__("itertools").product(counts, repeat=3): + types = (type_a, type_b, type_c) + if not distinct_type_support(types, counts): + continue + supported_patterns += 1 + old = (type_a[0], type_b[0], type_c[0]) + widths = (type_a[1], type_b[1], type_c[1]) + new = cycle_slacks(old, widths) + if min(new) < 0: + continue + capacity_feasible_patterns += 1 + transfer_states.add((*type_a, *type_b, *type_c, new)) + old_hist, new_hist = rank_histogram(old), rank_histogram(new) + transition = (old_hist, new_hist) + if transition not in witnesses_by_transition: + picked = [] + used_groups = set() + for typ in types: + role = next((row for row in members[typ] + if (int(row["owner_replica"]), int(row["child"]), + int(row["port"])) not in used_groups), None) + require(role is not None, "compressed type support lost distinct groups") + g = (int(role["owner_replica"]), int(role["child"]), int(role["port"])) + used_groups.add(g) + picked.append((g, role)) + require(len(used_groups) == 3, "cycle groups are not distinct") + require(len({family_of[g] for g, _ in picked}) == 3, + "occupied cycle groups do not have distinct families") + witnesses_by_transition[transition] = { + "call": t, + "old_slacks": list(old), + "outgoing_widths": list(widths), + "new_slacks": list(new), + "moves": [ + {"helper": int(picked[i][1]["helper"]), + "source_group": list(picked[i][0]), + "destination_group": list(picked[(i + 1) % 3][0]), + "width": int(picked[i][1]["width"])} + for i in range(3) + ], + } + + require(supported_patterns == 49408, "supported-pattern census changed") + require(capacity_feasible_patterns == 4417, "capacity-feasible pattern census changed") + require(len(transfer_states) == 255, "transfer-state census changed") + require(len(witnesses_by_transition) == 35, "rank-histogram transition census changed") + + priced = [] + strict_increases = [] + equal_histograms = strictly_worse = improving = 0 + for (old_hist, new_hist), witness in sorted(witnesses_by_transition.items()): + if old_hist == new_hist: + equal_histograms += 1 + priced.append({"old_histogram": old_hist, "new_histogram": new_hist, + "classification": "exact-tie"}) + continue + mercator = interval_difference(old_hist, new_hist, + {r: pair[0] for r, pair in rank_costs.items()}, + "selected Mercator") + base_two = interval_difference(old_hist, new_hist, + {r: pair[1] for r, pair in rank_costs.items()}, + "selected base-two") + ml, mu = Q(mercator["lower"]), Q(mercator["upper"]) + bl, bu = Q(base_two["lower"]), Q(base_two["upper"]) + if mu < 0 or bu < 0: + improving += 1 + elif ml > 0 and bl > 0: + strictly_worse += 1 + else: + raise AssertionError("exact rank-moment intervals did not decide a nonidentity transition") + row = {"old_histogram": old_hist, "new_histogram": new_hist, + "classification": "strict-increase" if ml > 0 and bl > 0 else "strict-decrease", + "mercator_delta": [mercator["lower"], mercator["upper"]], + "base_two_delta": [base_two["lower"], base_two["upper"]]} + priced.append(row) + if ml > 0 and bl > 0: + strict_increases.append((ml, row, witness)) + require(equal_histograms == 19 and strictly_worse == 16 and improving == 0, + "exact selected-endpoint price classification changed") + _, worst_transition, worst_witness = min(strict_increases, key=lambda entry: entry[0]) + require(Q(worst_transition["mercator_delta"][0]) > 0, + "minimum-cost nonidentity transition is not strictly more expensive") + require(Q(worst_transition["base_two_delta"][0]) > 0, + "second engine does not certify the minimum increase") + return { + "ordered_supported_type_patterns": supported_patterns, + "capacity_feasible_type_patterns": capacity_feasible_patterns, + "unique_ordered_transfer_states": len(transfer_states), + "distinct_rank_histogram_transitions": len(witnesses_by_transition), + "equal_histogram_transitions": equal_histograms, + "strictly_more_expensive_transitions": strictly_worse, + "strictly_cheaper_transitions": improving, + "minimum_strict_increase": { + "old_histogram": worst_transition["old_histogram"], + "new_histogram": worst_transition["new_histogram"], + "mercator_delta": worst_transition["mercator_delta"], + "base_two_delta": worst_transition["base_two_delta"], + "feasible_source_witness": worst_witness, + }, + "all_transitions": priced, + } + + +def verify(): + for relative, expected in PINS.items(): + actual = hashlib.sha256((ROOT / relative).read_bytes()).hexdigest() + require(actual == expected, "source hash mismatch: " + relative) + selected = read_json(SELECTED_PATH) + assembly = read_json(ASSEMBLY_PATH) + ceiling = read_json(CEILING_PATH) + bit_data = read_json(BIT_PATH) + require(selected["kappa"] == "836330098538459/500000000000000000", + "selected record changed") + require(assembly["binding"] == "complex", "selected binding side changed") + alpha_cap = Q(ceiling["ceiling"]["a_ceiling"]) + kappa_cap = alpha_cap / (1 + alpha_cap) + require(ceiling["ceiling"]["kappa_upper_bound"] == "0.0016872026453254019", + "fixed-word packing ceiling changed") + M_engine = load_engine(MOMENT_PATH, "selected_moment_engine") + B_engine = load_engine(BASE_TWO_PATH, "selected_base_two_engine") + supplier_prices = selected_supplier_receipts(read_json(PLAN_PATH), assembly, + bit_data, M_engine, B_engine) + plan, owners, caps, windows, family_of, remainder, by_call, group_at_call = load_and_check_map() + census = find_exact_domain(plan, owners, caps, windows, family_of, remainder, + by_call, group_at_call, assembly, M_engine, B_engine) + current_kappa = Q(selected["kappa"]) + return { + "status": "SCOPED_NEGATIVE_RESULT_NO_IMPROVING_SAME_CALL_3_CYCLES", + "assignment": { + "seed": "c37585e64a1b0aaf41a29afcbfd3f5c7", + "track": "incumbent-optimization", + "task_id": "selected-packing", + "priority_revision": 3, + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "selected_record_sha256": PINS[SELECTED_PATH], + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-18923820", + }, + "overlap_snapshot": { + "refreshed_at": "2026-10-14T12:38:03Z/12:39:37Z", + "open_prs": 529, + "discussions": 508, + "complete_pagination": True, + "nearest_open_prs": [ + {"number": 1790, "head": "48ee04ee708081c8713e8868a370bbbf5aa099e1", + "scope": "selected PR1094 map two-role census; three-role cycles left open"}, + {"number": 1617, "head": "536bc90ea2de310e0e08d2cb65f7add1d9de92b5", + "scope": "selected PR1094 neutral two-move census"}, + {"number": 1819, "head": "eb519ed5b0013e03f4d9657730d57acee65cafd4", + "scope": "selected PR1094 neutral move followed by strict two-step gain"}, + {"number": 1154, "head": "390de2866a03758e7f4ddbb2846e5b2ee4e72154", + "scope": "positive three-owner cycle on the different PR1117 route and changed local word"}, + ], + }, + "selected_source": { + "plan_sha256": PINS[PLAN_PATH], + "owners_sha256": PINS[OWNERS_PATH], + "calls": CALLS, + "roles_per_call": HELPERS, + "owner_groups_in_capacity_model": len(caps), + "whole_role_placements": len(owners), + "positive_idle_remainders": {str(r): n for r, n in sorted(Counter(remainder.values()).items()) if r}, + }, + "census": census, + "supplier_prices": supplier_prices, + "packing_cap": { + "a_upper_bound": str(alpha_cap), + "kappa_upper_bound": str(kappa_cap), + "selected_kappa": str(current_kappa), + "remaining_kappa_headroom": str(kappa_cap - current_kappa), + "headroom_realized_by_this_domain": "0", + "fraction_of_packing_headroom_realized": "0", + }, + "scope_limit": "One same-invocation three-role permutation among three distinct currently occupied groups. Cross-call cycles, chains, longer sequences, changed local words and a global packing optimum are not covered.", + } + + +def main(): + result = verify() + (HERE / "RESULT.json").write_text(json.dumps(result, indent=2) + "\n", encoding="utf-8") + print(result["status"]) + print(json.dumps({k: result["census"][k] for k in ( + "ordered_supported_type_patterns", "capacity_feasible_type_patterns", + "unique_ordered_transfer_states", "distinct_rank_histogram_transitions", + "equal_histogram_transitions", "strictly_more_expensive_transitions", + "strictly_cheaper_transitions")}, sort_keys=True)) + print("selected packing cap", result["packing_cap"]["kappa_upper_bound"], + "headroom realized", result["packing_cap"]["fraction_of_packing_headroom_realized"]) + + +if __name__ == "__main__": + main()