From 51633ffdca5df8d4a014fade005149b65d142a20 Mon Sep 17 00:00:00 2001 From: Sagar Thakrar Date: Wed, 14 Oct 2026 13:43:16 +0530 Subject: [PATCH 1/4] Audit: PR442 hosting windows bound the partial width-seven bit rows (no new kappa) Rebuilds the nine-stage idle schedule and its hosting windows (equal to PR442 hosting_core.windows and audit_hosted_k.windows). Capacity-7 children admit one stage each, so the window-free partial width-seven rows of #1023 and #1281 are unreachable for replica-local hosting. Gives the exact window-respecting optimum, an explicit placement and a tight 1e-24 certificate for every k = 0..74 under both local brackets, and reproduces #1281's merged idle optima and priced cases exactly. Prepared with substantial AI assistance from Claude (Anthropic) via Claude Code. --- .../bit589-width7-windows-seed72/README.md | 207 + .../bit589-width7-windows-seed72/RESULT.json | 4880 +++++++++++++++++ .../bit589-width7-windows-seed72/SOURCES.json | 96 + .../bit589-width7-windows-seed72/TASK.json | 72 + .../bit589-width7-windows-seed72/VERIFY.json | 48 + .../test_package.py | 111 + .../bit589-width7-windows-seed72/verify.py | 353 ++ .../bit589-width7-windows-seed72/windows.py | 95 + research/bit589-width7-windows-seed72/wopt.py | 159 + 9 files changed, 6021 insertions(+) create mode 100644 research/bit589-width7-windows-seed72/README.md create mode 100644 research/bit589-width7-windows-seed72/RESULT.json create mode 100644 research/bit589-width7-windows-seed72/SOURCES.json create mode 100644 research/bit589-width7-windows-seed72/TASK.json create mode 100644 research/bit589-width7-windows-seed72/VERIFY.json create mode 100644 research/bit589-width7-windows-seed72/test_package.py create mode 100644 research/bit589-width7-windows-seed72/verify.py create mode 100644 research/bit589-width7-windows-seed72/windows.py create mode 100644 research/bit589-width7-windows-seed72/wopt.py diff --git a/research/bit589-width7-windows-seed72/README.md b/research/bit589-width7-windows-seed72/README.md new file mode 100644 index 0000000000..ba18d68d4d --- /dev/null +++ b/research/bit589-width7-windows-seed72/README.md @@ -0,0 +1,207 @@ +# Audit: PR442 hosting windows and the partial width-seven rows of #1023 and #1281 + +**Adversarial audit: this package finds no new κ and changes no check.** Track 60–74 (adversarial audit), assignment seed 72 +(OS CSPRNG via Python `secrets`). Card `uniform-transfer-audit` (a hosting implication), scope +**refined** in [TASK.json](TASK.json). Base `0b1cccf8`; the selected record frontier1094 (complex-bound) +is unchanged, and `verify.py` binds it to the PR589 record and engines it uses. + +## The audited claims + +- **#1023 (ours, merged, `research/bit589-width-packing`).** It publishes partial width-seven rows: converting k helpers per call to width 7 gives, + for example, k = 37 optimistic 0.0017896275 (+3.24%). The rows are described as achievable + placements in its slot model. They are reached by putting all 9k width-7 residuals in empty + capacity-7 slots. Its README lists window timing as an unchecked obligation. +- **#1281 (mightyOil, merged, `research/bit-partial-width7-optimum`).** It proves the + exact optimum for every k = 0..74 in its mixed-width slot relaxation, replica-local and pooled32. + It openly disclaims temporal constraints. Its **open question 1** asks whether the relaxed optimum + can be hosted in time order. + +This package answers that question for the PR442/PR589 **replica-local** hosting format: the hosted +audit's `hosted[(stage, helper)]` map with per-replica windows `s in W[i]`. + +## The windows + +[windows.py](windows.py) rebuilds the nine-stage idle schedule from the recipe of `global_k.py` +(K = 4, L = 9) and computes the windows. Three implementations agree exactly: this code, PR442's +`hosting_core.windows`, and `audit_hosted_k.windows`, which enforces `s in W[i]` for every hosted +slot. All 14 frozen `selection9-p111` entries lie inside their windows. + +| Idle child | 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | +|---|---|---|---|---|---|---|---|---|---| +| Capacity | 14 | **7** | 28 | **7** | 42 | **7** | 42 | 28 | 14 | +| Admissible stages | 0–1 | **2** | 0–3 | **4** | 0–5 | **6** | 3–8 | 5–8 | 7–8 | + +**Each capacity-7 child admits exactly one stage.** Per replica, at most 3k of the 9k width-7 +residuals can sit in 7-slots. The window-free rows of #1023 and #1281 use all 9k. + +## Results ([RESULT.json](RESULT.json)) + +For every k = 0..74, the package computes the **exact window-respecting optimum**. For each k it +gives: + +- an explicit residual-level placement. Every slot is checked for its window, its width and its + offset, cells must be disjoint, and every (stage, helper) is hosted exactly once; +- that placement's bit endpoint under both of #1023's local brackets, using the pinned engines and + the inherited surcharge; +- a **certificate that no window-feasible placement reaches the next 1e-24 grid point**. The + certificate is tight: it equals the engine moment of the explicit histogram to 1e-50. + +k = 0 reproduces the selected bit endpoint 0.001733427039589844234749. + +Per-replica idle histograms and the width-7 distribution over children 0, 2, 4, 8, 7, 6 are in +RESULT.json for every k. Selected rows, with gain over the selected bit endpoint: + +| k | Bracket | Window-respecting optimum | Window-free optimum (#1281) | Retained | +|---|---|---|---|---| +| 1 | optimistic | 0.001734347102 (+0.053%) | 0.001734846264 (+0.082%) | 0.648 | +| 1 | pessimistic | 0.001734104523 (+0.039%) | 0.001734603545 (+0.068%) | 0.576 | +| 2 | optimistic | 0.001735271920 (+0.106%) | 0.001736327170 (+0.167%) | 0.636 | +| 2 | pessimistic | 0.001734786312 (+0.078%) | 0.001735840971 (+0.139%) | 0.563 | +| 10 | optimistic | 0.001743225534 (+0.565%) | 0.001748291126 (+0.857%) | 0.659 | +| 10 | pessimistic | 0.001740777922 (+0.424%) | 0.001745829269 (+0.715%) | 0.593 | +| 37 | optimistic | 0.001770809187 (+2.157%) | 0.001789671631 (+3.245%) | 0.665 | +| 37 | pessimistic | 0.001761884716 (+1.642%) | 0.001780556367 (+2.719%) | 0.604 | +| 74 | optimistic | 0.001809907119 (+4.412%) | 0.001849754238 (+6.711%) | 0.657 | +| 74 | pessimistic | 0.001792188010 (+3.390%) | 0.001831249661 (+5.643%) | 0.601 | + +Decimals are truncated. The certified bound for each row is the next 1e-24 grid point above the +window-respecting endpoint. + +- **#1023:** all 8 published partial rows (k = 1, 10, 37, 74; optimistic and pessimistic) are + **unreachable** under the windows. Each lies above its certified bound. +- **#1281, replica-local:** every row (k = 1..74, both brackets) is unreachable. The window-free + optimum is re-derived here and matches #1281's merged `EXPECTED.json` (digest-pinned, read as + data; no #1281 code is run). All 75 idle optima agree, and all 9 priced cases agree exactly in + endpoint and full histogram. +- **#1281, pooled32:** its 8 priced rows with k > 0 also lie above the per-replica bound. Pooling + moves residuals between replicas, so it is not replica-local hosting. These rows are unreachable + for replica-local placements only; see the cross-replica caveat below. +- **#1023's all-width-7 optimum `{42:340, 21:1}` stays window-feasible.** 104 sextet splits are + feasible by max-flow, so its +17–23% figure is not affected by the windows. + +Across the whole range, the window-respecting optimum keeps **63.6–67.1%** of the window-free +gain, or 56.3–60.7% under the pessimistic bracket. For small k, the window-free rows overstate the gain +by about 1.5×. None of this changes κ: the selected record is complex-bound, and these are bit +headroom figures. + +## Why it is exact (proof sketch; the code asserts each checked fact) + +1. **Lemma A (exchange): some optimum puts every stage-2, 4 and 6 width-7 residual alone in a copy + of child 1, 3 or 5.** + - Cost per copy is F(r) = 64^a r^(1−a) + λ for r > 0, with F(0) = 0. Here λ ≥ 0 is the + per-child surcharge term. + - F is subadditive on r ≥ 0: r^(1−a) is concave with value 0 at 0, and λ is counted once. + - A capacity-7 copy cannot hold a width-8 residual and holds at most one width-7 residual. Child + 1 has 222 > k copies. + - Moving a stage-2 width-7 residual from a copy with r unused units into an empty copy of child 1 + changes the cost by F(r + 7) − F(r) + F(0) − F(7) ≤ 0. +2. **Width-8 placement is unconstrained (checked for every k ≤ 74).** The windows are stage + intervals, so Hall's condition for the stage → child transport reduces to intervals. For every + proper interval J, the full width-8 capacity of the children whose windows lie in J is at most + the width-8 supply of J. +3. **The width-7 residuals reduce to two nested chains.** After Lemma A, 6k width-7 residuals remain, + from stages 0, 1, 3, 5, 7 and 8, over children 0, 2, 4, 6, 7 and 8. A distribution B is feasible + exactly when all of the following hold: + - B0 ≤ 2k, B0 + B2 ≤ 3k, B0 + B2 + B4 ≤ 4k; + - B8 ≤ 2k, B8 + B7 ≤ 3k, B8 + B7 + B6 ≤ 4k; + - ΣB = 6k. + + This is derived from all 45 interval Hall constraints (asserted for every k). It is also + confirmed by brute force: every distribution for k = 1 and 2 is checked by max-flow against the + chain predicate, all agreeing. +4. **Exact lower bound.** Cost splits three ways: copies holding width-7 residuals (a per-child + knapsack over copy types), copies holding only width-8 slack (#1281's periodic V(S), recomputed + and checked at each a), and the 7-slots. An integer DP over (chain sums, slack mod 5), with + outward-rounded lower bounds of F at 2^−200 from the pinned engine, drops the copy limits and + S ≥ 0. It is therefore a relaxation, which gives a rigorous lower bound. +5. **Attainment and certificate.** The DP minimiser is expanded into the explicit placement above, + whose cost equals the DP value exactly. At a′ = c* + 1e−24, the local moment lower bound plus 32 + times the DP bound exceeds 1. Every replica-local placement, uniform across replicas or not, + therefore has an endpoint below a′. This is grid optimality at each row's own endpoint. + +## Controls ([test_package.py](test_package.py), 11 tests) + +- **C-W1.** #1023's k = 1 placement fills 9 capacity-7 copies per replica, one per stage. The vendored + windows admit only stages 2, 4 and 6 there, so at least 6 residuals sit outside their window. +- **C-W2.** The window-free local rows lie above the certified bound, while the window-respecting + endpoints lie below it. +- **C-W3.** #1281's local and pooled32 priced rows (k > 0) lie above the per-replica bound, and all + 75 idle optima match. +- **C-W4.** The all-width-7 optimum is window-feasible. +- **C-W5 (dropped constraint).** Dropping the chain constraint B0 ≤ 2k breaks the brute-force + agreement. +- **C-W5 (perturbed window).** Widening child 0's window to stages 0–3 breaks the chain structure. + +Also covered: #1023's eight rows are all unreachable, k = 0 reproduces the selected endpoint, the +brute-force reduction holds at k = 2, and the width-8 Hall conditions are vacuous. + +## Reproduce + +```sh +python3 -I -B research/bit589-width7-windows-seed72/verify.py # ~2.5 min on one idle core; PASS_BIT589_WIDTH7_WINDOWS +python3 -I -B -m unittest discover -s research/bit589-width7-windows-seed72 -p test_package.py +python3 scripts/research_package.py --package research/bit589-width7-windows-seed72 --check-only +python3.12 scripts/research_package.py --package research/bit589-width7-windows-seed72 +``` + +Standard-library Python 3.10 or later. The pinned engines, record and slot model come from merged +#1023's `packing.py`, which is imported read-only. `verify.py --kmax K` runs a partial check +(`PASS_PARTIAL`). + +## Scope and remaining obligations + +- **Hosting format.** This applies to the PR442/PR589 nine-stage template (the 2P + 1 stage format + with P = 4; #743) with replica-local hosting, whole residuals, no banks and the frozen stage + recipe. A changed recipe, split residuals or banks lie outside it. Open #1487 (ianlibanio) varies + the nine-stage recipe for width-8 hosting; its recipes may have other capacity-7 windows, which + this package does not check. +- **Cross-replica owner maps are open.** The selected complex T16 supplier uses cross-replica + interleaved owner maps (`owner_replica ≠ replica`). Such a map could admit other replicas' calls + at other stages into the 7-slot windows. That case is **not** ruled out here. +- **Windows are necessary, not sufficient.** + - Projector compatibility is still open. #1307's caveat applies: slots that split q⊥ lie outside + its completion-free argument, and that covers width-7 residuals in 14-, 28- and 42-slots. + - Owner inactivity is still open. + - A physical width-7 helper is still open (#1128, #1271, #1256, #1362). + + So the window optimum is itself only an upper bound for real hosting, while the unreachability + direction holds. +- **Pricing assumption.** The prices keep #1023's assumption that each converted helper removes + one unit from one local child. +- **Uniqueness.** Histograms are not shown to be unique; ties exist, for example at k = 2. + +## Relation to #1023 and #1281 + +- **#1023.** Its partial rows are window-free relaxation values, and this package gives the + window-respecting values. #1023's frozen files are left untouched. +- **#1281.** Its optima are correct for the relaxation it states. This package answers the window + part of its open question 1: the relaxed optimum cannot be hosted chronologically by any + replica-local placement. It gives the exact window-respecting optimum instead. The physical + helper, source access and restoration parts of that question stay open. + +## Open next questions + +1. **Can cross-replica (T16-style) interleaved owner maps lift the one-stage 7-slot windows for the + bit supplier?** That would make #1281's pooled rows a real target. + - First step: compute windows on an interleaved bit timeline and rerun the DP. +2. **Does another nine-stage recipe widen the capacity-7 windows?** #1487 enumerates recipes for + width-8 hosting only. + - First step: feed each of #1487's recipes to `windows.windows` and rerun `wopt.solve` at k = 1 + and k = 37. +3. **Do the window-respecting placements pass projector compatibility (#1307) for mixed-width + slots?** + - First step: run the projector check on the k = 1 explicit placement. + +## Credit + +- #1023: Sagar Thakrar. +- #1281: mightyOil (Philipp), with OpenAI Codex GPT-6 Astra assistance. +- #743: 0xjohnnydev, the 2P + 1 stage bound. #1487: ianlibanio. #1128: aliromman. #1307: commdata2338. +- PR442: DaysSky, the hosting windows. +- PR463, PR510 and PR589: DreamingOfClouds, the hosted audit and the bit supplier. +- PR555: eumemic. +- The retained moment-engine authors. + +Prepared by Sagar Thakrar (thakrarsagar) with substantial AI assistance from Claude (Anthropic) via +Claude Code. Parallel read-only scout and judge subagents found and checked the window obstruction. +New material is Apache-2.0. diff --git a/research/bit589-width7-windows-seed72/RESULT.json b/research/bit589-width7-windows-seed72/RESULT.json new file mode 100644 index 0000000000..999c9ce950 --- /dev/null +++ b/research/bit589-width7-windows-seed72/RESULT.json @@ -0,0 +1,4880 @@ +{ + "all_width7": { + "feasible_sextet_splits": [ + 0, + 103, + 104 + ], + "idle_per_replica": { + "21": 1, + "42": 340 + } + }, + "binding": { + "assembly": "research/community-frontier1094-audit/ASSEMBLY.json", + "assembly_sha256": "1122cb3a575f8c788345fc1bf4c108ac7c3250fb81a5988671f5eb04b3ab3045", + "bit_lower": "1733427039589844234749/1000000000000000000000000", + "record": "certificates/selected-result.json" + }, + "capacity7_children": { + "1": [ + 2 + ], + "3": [ + 4 + ], + "5": [ + 6 + ] + }, + "chain_reduction_brute_force": { + "agree": "all", + "distributions_checked": { + "1": 432, + "2": 5908 + } + }, + "pr1023_partial_rows": { + "k10_optimistic": { + "certified_bound": "217903191776036031689/125000000000000000000000", + "pr1023": "0.001748291126728852518913", + "unreachable": true + }, + "k10_pessimistic": { + "certified_bound": "870388961344220397299/500000000000000000000000", + "pr1023": "0.001745829269907545754175", + "unreachable": true + }, + "k1_optimistic": { + "certified_bound": "1734347102923006399613/1000000000000000000000000", + "pr1023": "0.001734846264120199151475", + "unreachable": true + }, + "k1_pessimistic": { + "certified_bound": "108381532739553010717/62500000000000000000000", + "pr1023": "0.001734603545275303824122", + "unreachable": true + }, + "k37_optimistic": { + "certified_bound": "1770809187427053553943/1000000000000000000000000", + "pr1023": "0.001789627464386638781647", + "unreachable": true + }, + "k37_pessimistic": { + "certified_bound": "1761884716885951335477/1000000000000000000000000", + "pr1023": "0.001780512649923341060004", + "unreachable": true + }, + "k74_optimistic": { + "certified_bound": "904953559530015237129/500000000000000000000000", + "pr1023": "0.001849705707539871039662", + "unreachable": true + }, + "k74_pessimistic": { + "certified_bound": "56005875337664138131/31250000000000000000000", + "pr1023": "0.001831202097168172884608", + "unreachable": true + } + }, + "pr1281": { + "idle_optima_matched": 75, + "local_rows_unreachable": "148 of 148 (both brackets, k = 1..74)", + "merged": "e4a7f61f168837f628a1d8b54aa5cff0680f9a38", + "path": "research/bit-partial-width7-optimum/EXPECTED.json", + "priced_cases": { + "k0_optimistic": { + "certified_bound": "6933708158359376939/4000000000000000000000", + "local": "0.001733427039589844234749", + "pooled32": "0.001733427039589844234749", + "unreachable": false + }, + "k1_optimistic": { + "certified_bound": "1734347102923006399613/1000000000000000000000000", + "local": "0.001734846264120199151475", + "pooled32": "0.001734900431583947157341", + "unreachable": true + }, + "k1_pessimistic": { + "certified_bound": "108381532739553010717/62500000000000000000000", + "local": "0.001734603545275303824122", + "pooled32": "0.001734657697586404233802", + "unreachable": true + }, + "k2_optimistic": { + "certified_bound": "1388217536169998549/800000000000000000000", + "local": "0.001736327170598942735353", + "pooled32": "0.0017363781660342837852", + "unreachable": true + }, + "k2_pessimistic": { + "certified_bound": "216848289009341626869/125000000000000000000000", + "local": "0.0017358409713034135953", + "pooled32": "0.001735891938199934503774", + "unreachable": true + }, + "k37_optimistic": { + "certified_bound": "1770809187427053553943/1000000000000000000000000", + "local": "0.001789671631346367026824", + "pooled32": "0.001789725802593008582027", + "unreachable": true + }, + "k37_pessimistic": { + "certified_bound": "1761884716885951335477/1000000000000000000000000", + "local": "0.001780556367920637129218", + "pooled32": "0.001780609989052611495117", + "unreachable": true + }, + "k74_optimistic": { + "certified_bound": "904953559530015237129/500000000000000000000000", + "local": "0.00184975423837042835336", + "pooled32": "0.001849803954130003404634", + "unreachable": true + }, + "k74_pessimistic": { + "certified_bound": "56005875337664138131/31250000000000000000000", + "local": "0.001831249661111873873002", + "pooled32": "0.001831298387323686469848", + "unreachable": true + } + }, + "sha256": "a6ec64866b949626d6508ee7172b144c3fd29f1065822b523fafd7d2a59e2e91" + }, + "rows": { + "0": { + "idle": { + "2": 435, + "4": 444, + "42": 9, + "6": 444, + "7": 666 + }, + "optimistic": { + "certified_bound": "6933708158359376939/4000000000000000000000", + "endpoint": "1733427039589844234749/1000000000000000000000000", + "endpoint_decimal": "0.001733427039589844234749", + "gain_percent": "0.000000", + "lb_minus_one_at_bound": "1.669e-24", + "retained_fraction": null, + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001733427039589844234749", + "windowfree_endpoint": "1733427039589844234749/1000000000000000000000000", + "windowfree_gain_percent": "0.000000", + "windowfree_unreachable": true + }, + "pessimistic": { + "certified_bound": "6933708158359376939/4000000000000000000000", + "endpoint": "1733427039589844234749/1000000000000000000000000", + "endpoint_decimal": "0.001733427039589844234749", + "gain_percent": "0.000000", + "lb_minus_one_at_bound": "1.669e-24", + "retained_fraction": null, + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001733427039589844234749", + "windowfree_endpoint": "1733427039589844234749/1000000000000000000000000", + "windowfree_gain_percent": "0.000000", + "windowfree_unreachable": true + }, + "width7_distribution": [ + [ + 0, + 0 + ], + [ + 2, + 0 + ], + [ + 4, + 0 + ], + [ + 8, + 0 + ], + [ + 7, + 0 + ], + [ + 6, + 0 + ] + ] + }, + "1": { + "idle": { + "2": 434, + "4": 442, + "42": 10, + "5": 2, + "6": 442, + "7": 663 + }, + "optimistic": { + "certified_bound": "1734347102923006399613/1000000000000000000000000", + "endpoint": "433586775730751599903/250000000000000000000000", + "endpoint_decimal": "0.001734347102923006399612", + "gain_percent": "0.053078", + "lb_minus_one_at_bound": "2.522e-24", + "retained_fraction": "0.648286", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001734846264120199151475", + "windowfree_endpoint": "69393850564807966059/40000000000000000000000", + "windowfree_gain_percent": "0.081874", + "windowfree_unreachable": true + }, + "pessimistic": { + "certified_bound": "108381532739553010717/62500000000000000000000", + "endpoint": "1734104523832848171471/1000000000000000000000000", + "endpoint_decimal": "0.001734104523832848171471", + "gain_percent": "0.039084", + "lb_minus_one_at_bound": "1.881e-24", + "retained_fraction": "0.575844", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001734603545275303824122", + "windowfree_endpoint": "867301772637651912061/500000000000000000000000", + "windowfree_gain_percent": "0.067872", + "windowfree_unreachable": true + }, + "width7_distribution": [ + [ + 0, + 2 + ], + [ + 2, + 1 + ], + [ + 4, + 0 + ], + [ + 8, + 2 + ], + [ + 7, + 1 + ], + [ + 6, + 0 + ] + ] + }, + "10": { + "idle": { + "2": 424, + "35": 1, + "4": 438, + "42": 19, + "5": 1, + "6": 425, + "7": 636 + }, + "optimistic": { + "certified_bound": "217903191776036031689/125000000000000000000000", + "endpoint": "1743225534208288253511/1000000000000000000000000", + "endpoint_decimal": "0.001743225534208288253511", + "gain_percent": "0.565267", + "lb_minus_one_at_bound": "1.905e-24", + "retained_fraction": "0.659206", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001748291126728852518913", + "windowfree_endpoint": "1748291126728852518913/1000000000000000000000000", + "windowfree_gain_percent": "0.857497", + "windowfree_unreachable": true + }, + "pessimistic": { + "certified_bound": "870388961344220397299/500000000000000000000000", + "endpoint": "1740777922688440794597/1000000000000000000000000", + "endpoint_decimal": "0.001740777922688440794597", + "gain_percent": "0.424066", + "lb_minus_one_at_bound": "1.013e-24", + "retained_fraction": "0.592707", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001745829269907545754175", + "windowfree_endpoint": "69833170796301830167/40000000000000000000000", + "windowfree_gain_percent": "0.715475", + "windowfree_unreachable": true + }, + "width7_distribution": [ + [ + 0, + 20 + ], + [ + 2, + 9 + ], + [ + 4, + 0 + ], + [ + 8, + 18 + ], + [ + 7, + 12 + ], + [ + 6, + 1 + ] + ] + }, + "11": { + "idle": { + "2": 422, + "4": 440, + "42": 21, + "6": 422, + "7": 633 + }, + "optimistic": { + "certified_bound": "1744330661643884226319/1000000000000000000000000", + "endpoint": "872165330821942113159/500000000000000000000000", + "endpoint_decimal": "0.001744330661643884226318", + "gain_percent": "0.629021", + "lb_minus_one_at_bound": "3.072e-25", + "retained_fraction": "0.668616", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001749734800684953364557", + "windowfree_endpoint": "1749734800684953364557/1000000000000000000000000", + "windowfree_gain_percent": "0.940782", + "windowfree_unreachable": true + }, + "pessimistic": { + "certified_bound": "1741635252808621897623/1000000000000000000000000", + "endpoint": "870817626404310948811/500000000000000000000000", + "endpoint_decimal": "0.001741635252808621897622", + "gain_percent": "0.473525", + "lb_minus_one_at_bound": "1.972e-24", + "retained_fraction": "0.603739", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001747022665782330980176", + "windowfree_endpoint": "109188916611395686261/62500000000000000000000", + "windowfree_gain_percent": "0.784321", + "windowfree_unreachable": true + }, + "width7_distribution": [ + [ + 0, + 22 + ], + [ + 2, + 8 + ], + [ + 4, + 0 + ], + [ + 8, + 22 + ], + [ + 7, + 8 + ], + [ + 6, + 6 + ] + ] + }, + "12": { + "idle": { + "14": 1, + "2": 422, + "4": 438, + "42": 22, + "6": 419, + "7": 630 + }, + "optimistic": { + "certified_bound": "1745371382219323090437/1000000000000000000000000", + "endpoint": "436342845554830772609/250000000000000000000000", + "endpoint_decimal": "0.001745371382219323090436", + "gain_percent": "0.689059", + "lb_minus_one_at_bound": "8.085e-25", + "retained_fraction": "0.670496", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001751241239857222673239", + "windowfree_endpoint": "1751241239857222673239/1000000000000000000000000", + "windowfree_gain_percent": "1.027687", + "windowfree_unreachable": true + }, + "pessimistic": { + "certified_bound": "1742427840027304876499/1000000000000000000000000", + "endpoint": "871213920013652438249/500000000000000000000000", + "endpoint_decimal": "0.001742427840027304876498", + "gain_percent": "0.519249", + "lb_minus_one_at_bound": "2.657e-24", + "retained_fraction": "0.606081", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001748277868469094889924", + "windowfree_endpoint": "437069467117273722481/250000000000000000000000", + "windowfree_gain_percent": "0.856732", + "windowfree_unreachable": true + }, + "width7_distribution": [ + [ + 0, + 24 + ], + [ + 2, + 12 + ], + [ + 4, + 0 + ], + [ + 8, + 24 + ], + [ + 7, + 12 + ], + [ + 6, + 0 + ] + ] + }, + "13": { + "idle": { + "14": 1, + "2": 421, + "4": 436, + "42": 23, + "5": 2, + "6": 417, + "7": 627 + }, + "optimistic": { + "certified_bound": "109144010777026365099/62500000000000000000000", + "endpoint": "1746304172432421841583/1000000000000000000000000", + "endpoint_decimal": "0.001746304172432421841583", + "gain_percent": "0.742871", + "lb_minus_one_at_bound": "3.134e-24", + "retained_fraction": "0.667277", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001752725068382635327284", + "windowfree_endpoint": "438181267095658831821/250000000000000000000000", + "windowfree_gain_percent": "1.113288", + "windowfree_unreachable": true + }, + "pessimistic": { + "certified_bound": "1743112374709363298659/1000000000000000000000000", + "endpoint": "871556187354681649329/500000000000000000000000", + "endpoint_decimal": "0.001743112374709363298658", + "gain_percent": "0.558739", + "lb_minus_one_at_bound": "2.671e-24", + "retained_fraction": "0.602220", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001749509761147745330485", + "windowfree_endpoint": "349901952229549066097/200000000000000000000000", + "windowfree_gain_percent": "0.927799", + "windowfree_unreachable": true + }, + "width7_distribution": [ + [ + 0, + 26 + ], + [ + 2, + 13 + ], + [ + 4, + 0 + ], + [ + 8, + 26 + ], + [ + 7, + 13 + ], + [ + 6, + 0 + ] + ] + }, + "14": { + "idle": { + "14": 1, + "2": 420, + "4": 436, + "42": 24, + "6": 417, + "7": 624 + }, + "optimistic": { + "certified_bound": "69889671569225700957/40000000000000000000000", + "endpoint": "436810447307660630981/250000000000000000000000", + "endpoint_decimal": "0.001747241789230642523924", + "gain_percent": "0.796962", + "lb_minus_one_at_bound": "2.301e-24", + "retained_fraction": "0.663079", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001754261293834767149934", + "windowfree_endpoint": "877130646917383574967/500000000000000000000000", + "windowfree_gain_percent": "1.201911", + "windowfree_unreachable": true + }, + "pessimistic": { + "certified_bound": "435950315246260270633/250000000000000000000000", + "endpoint": "1743801260985041082531/1000000000000000000000000", + "endpoint_decimal": "0.001743801260985041082531", + "gain_percent": "0.598480", + "lb_minus_one_at_bound": "1.269e-25", + "retained_fraction": "0.597386", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001750793073736949073023", + "windowfree_endpoint": "1750793073736949073023/1000000000000000000000000", + "windowfree_gain_percent": "1.001832", + "windowfree_unreachable": true + }, + "width7_distribution": [ + [ + 0, + 26 + ], + [ + 2, + 16 + ], + [ + 4, + 0 + ], + [ + 8, + 26 + ], + [ + 7, + 16 + ], + [ + 6, + 0 + ] + ] + }, + "15": { + "idle": { + "2": 418, + "20": 1, + "4": 437, + "42": 25, + "6": 414, + "7": 621 + }, + "optimistic": { + "certified_bound": "1748284831515160763663/1000000000000000000000000", + "endpoint": "874142415757580381831/500000000000000000000000", + "endpoint_decimal": "0.001748284831515160763662", + "gain_percent": "0.857134", + "lb_minus_one_at_bound": "2.833e-24", + "retained_fraction": "0.663528", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001755819153288163217027", + "windowfree_endpoint": "1755819153288163217027/1000000000000000000000000", + "windowfree_gain_percent": "1.291783", + "windowfree_unreachable": true + }, + "pessimistic": { + "certified_bound": "218074333617804495809/125000000000000000000000", + "endpoint": "1744594668942435966471/1000000000000000000000000", + "endpoint_decimal": "0.001744594668942435966471", + "gain_percent": "0.644251", + "lb_minus_one_at_bound": "1.178e-24", + "retained_fraction": "0.598156", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001752097128267923208925", + "windowfree_endpoint": "70083885130716928357/40000000000000000000000", + "windowfree_gain_percent": "1.077062", + "windowfree_unreachable": true + }, + "width7_distribution": [ + [ + 0, + 30 + ], + [ + 2, + 12 + ], + [ + 4, + 0 + ], + [ + 8, + 30 + ], + [ + 7, + 12 + ], + [ + 6, + 6 + ] + ] + }, + "16": { + "idle": { + "2": 418, + "28": 1, + "4": 435, + "42": 26, + "6": 412, + "7": 618 + }, + "optimistic": { + "certified_bound": "218674835368541460447/125000000000000000000000", + "endpoint": "69975947317933267343/40000000000000000000000", + "endpoint_decimal": "0.001749398682948331683575", + "gain_percent": "0.921391", + "lb_minus_one_at_bound": "1.769e-24", + "retained_fraction": "0.669720", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001757275289506767564823", + "windowfree_endpoint": "1757275289506767564823/1000000000000000000000000", + "windowfree_gain_percent": "1.375786", + "windowfree_unreachable": true + }, + "pessimistic": { + "certified_bound": "1745458048685316688627/1000000000000000000000000", + "endpoint": "872729024342658344313/500000000000000000000000", + "endpoint_decimal": "0.001745458048685316688626", + "gain_percent": "0.694059", + "lb_minus_one_at_bound": "8.661e-25", + "retained_fraction": "0.605423", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001753299105862952831687", + "windowfree_endpoint": "1753299105862952831687/1000000000000000000000000", + "windowfree_gain_percent": "1.146403", + "windowfree_unreachable": true + }, + "width7_distribution": [ + [ + 0, + 32 + ], + [ + 2, + 16 + ], + [ + 4, + 0 + ], + [ + 8, + 32 + ], + [ + 7, + 16 + ], + [ + 6, + 0 + ] + ] + }, + "17": { + "idle": { + "2": 417, + "28": 1, + "4": 433, + "42": 27, + "5": 2, + "6": 410, + "7": 615 + }, + "optimistic": { + "certified_bound": "218791973004356650329/125000000000000000000000", + "endpoint": "1750335784034853202631/1000000000000000000000000", + "endpoint_decimal": "0.001750335784034853202631", + "gain_percent": "0.975452", + "lb_minus_one_at_bound": "1.303e-24", + "retained_fraction": "0.666546", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001758794743301734257496", + "windowfree_endpoint": "219849342912716782187/125000000000000000000000", + "windowfree_gain_percent": "1.463442", + "windowfree_unreachable": true + }, + "pessimistic": { + "certified_bound": "873072482585735407049/500000000000000000000000", + "endpoint": "1746144965171470814097/1000000000000000000000000", + "endpoint_decimal": "0.001746144965171470814097", + "gain_percent": "0.733687", + "lb_minus_one_at_bound": "1.497e-24", + "retained_fraction": "0.601710", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001754563340771590827773", + "windowfree_endpoint": "1754563340771590827773/1000000000000000000000000", + "windowfree_gain_percent": "1.219336", + "windowfree_unreachable": true + }, + "width7_distribution": [ + [ + 0, + 34 + ], + [ + 2, + 17 + ], + [ + 4, + 0 + ], + [ + 8, + 34 + ], + [ + 7, + 17 + ], + [ + 6, + 0 + ] + ] + }, + "18": { + "idle": { + "2": 416, + "28": 1, + "4": 433, + "42": 28, + "6": 410, + "7": 612 + }, + "optimistic": { + "certified_bound": "70051109453572015057/40000000000000000000000", + "endpoint": "218909717042412547053/125000000000000000000000", + "endpoint_decimal": "0.001751277736339300376424", + "gain_percent": "1.029792", + "lb_minus_one_at_bound": "2.620e-24", + "retained_fraction": "0.664475", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001760291402090735786868", + "windowfree_endpoint": "440072850522683946717/250000000000000000000000", + "windowfree_gain_percent": "1.549783", + "windowfree_unreachable": true + }, + "pessimistic": { + "certified_bound": "1746836249339631477849/1000000000000000000000000", + "endpoint": "218354531167453934731/125000000000000000000000", + "endpoint_decimal": "0.001746836249339631477848", + "gain_percent": "0.773566", + "lb_minus_one_at_bound": "2.242e-24", + "retained_fraction": "0.599239", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001755804104196774268397", + "windowfree_endpoint": "1755804104196774268397/1000000000000000000000000", + "windowfree_gain_percent": "1.290915", + "windowfree_unreachable": true + }, + "width7_distribution": [ + [ + 0, + 34 + ], + [ + 2, + 20 + ], + [ + 4, + 0 + ], + [ + 8, + 34 + ], + [ + 7, + 20 + ], + [ + 6, + 0 + ] + ] + }, + "19": { + "idle": { + "2": 413, + "34": 1, + "4": 436, + "42": 29, + "6": 406, + "7": 609 + }, + "optimistic": { + "certified_bound": "1752350182670529114823/1000000000000000000000000", + "endpoint": "876175091335264557411/500000000000000000000000", + "endpoint_decimal": "0.001752350182670529114822", + "gain_percent": "1.091661", + "lb_minus_one_at_bound": "4.598e-25", + "retained_fraction": "0.665982", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001761840921980323321143", + "windowfree_endpoint": "1761840921980323321143/1000000000000000000000000", + "windowfree_gain_percent": "1.639174", + "windowfree_unreachable": true + }, + "pessimistic": { + "certified_bound": "1747656867307138910843/1000000000000000000000000", + "endpoint": "873828433653569455421/500000000000000000000000", + "endpoint_decimal": "0.001747656867307138910842", + "gain_percent": "0.820907", + "lb_minus_one_at_bound": "2.395e-24", + "retained_fraction": "0.601185", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.00175709666421695193847", + "windowfree_endpoint": "175709666421695193847/100000000000000000000000", + "windowfree_gain_percent": "1.365481", + "windowfree_unreachable": true + }, + "width7_distribution": [ + [ + 0, + 38 + ], + [ + 2, + 16 + ], + [ + 4, + 0 + ], + [ + 8, + 38 + ], + [ + 7, + 16 + ], + [ + 6, + 6 + ] + ] + }, + "2": { + "idle": { + "2": 433, + "4": 442, + "42": 11, + "6": 442, + "7": 660 + }, + "optimistic": { + "certified_bound": "1388217536169998549/800000000000000000000", + "endpoint": "1735271920212498186249/1000000000000000000000000", + "endpoint_decimal": "0.001735271920212498186249", + "gain_percent": "0.106430", + "lb_minus_one_at_bound": "2.328e-24", + "retained_fraction": "0.636137", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001736327170598942735353", + "windowfree_endpoint": "1736327170598942735353/1000000000000000000000000", + "windowfree_gain_percent": "0.167306", + "windowfree_unreachable": true + }, + "pessimistic": { + "certified_bound": "216848289009341626869/125000000000000000000000", + "endpoint": "1734786312074733014951/1000000000000000000000000", + "endpoint_decimal": "0.001734786312074733014951", + "gain_percent": "0.078415", + "lb_minus_one_at_bound": "7.260e-25", + "retained_fraction": "0.563095", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.0017358409713034135953", + "windowfree_endpoint": "17358409713034135953/10000000000000000000000", + "windowfree_gain_percent": "0.139258", + "windowfree_unreachable": true + }, + "width7_distribution": [ + [ + 0, + 2 + ], + [ + 2, + 4 + ], + [ + 4, + 0 + ], + [ + 8, + 2 + ], + [ + 7, + 4 + ], + [ + 6, + 0 + ] + ] + }, + "20": { + "idle": { + "2": 413, + "4": 434, + "42": 31, + "6": 404, + "7": 606 + }, + "optimistic": { + "certified_bound": "350700906027895837607/200000000000000000000000", + "endpoint": "876752265069739594017/500000000000000000000000", + "endpoint_decimal": "0.001753504530139479188034", + "gain_percent": "1.158254", + "lb_minus_one_at_bound": "1.954e-24", + "retained_fraction": "0.669579", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001763412274866765722996", + "windowfree_endpoint": "440853068716691430749/250000000000000000000000", + "windowfree_gain_percent": "1.729824", + "windowfree_unreachable": true + }, + "pessimistic": { + "certified_bound": "874286367363627332993/500000000000000000000000", + "endpoint": "349714546945450933197/200000000000000000000000", + "endpoint_decimal": "0.001748572734727254665985", + "gain_percent": "0.873743", + "lb_minus_one_at_bound": "2.400e-24", + "retained_fraction": "0.605886", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001758424630312570240676", + "windowfree_endpoint": "439606157578142560169/250000000000000000000000", + "windowfree_gain_percent": "1.442091", + "windowfree_unreachable": true + }, + "width7_distribution": [ + [ + 0, + 40 + ], + [ + 2, + 20 + ], + [ + 4, + 0 + ], + [ + 8, + 40 + ], + [ + 7, + 20 + ], + [ + 6, + 0 + ] + ] + }, + "21": { + "idle": { + "2": 412, + "4": 432, + "42": 32, + "5": 2, + "6": 402, + "7": 603 + }, + "optimistic": { + "certified_bound": "1754446036292845882477/1000000000000000000000000", + "endpoint": "438611509073211470619/250000000000000000000000", + "endpoint_decimal": "0.001754446036292845882476", + "gain_percent": "1.212569", + "lb_minus_one_at_bound": "1.729e-24", + "retained_fraction": "0.668246", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.00176488103537514269847", + "windowfree_endpoint": "176488103537514269847/100000000000000000000000", + "windowfree_gain_percent": "1.814556", + "windowfree_unreachable": true + }, + "pessimistic": { + "certified_bound": "10932977881335001821/6250000000000000000000", + "endpoint": "1749276461013600291359/1000000000000000000000000", + "endpoint_decimal": "0.001749276461013600291359", + "gain_percent": "0.914340", + "lb_minus_one_at_bound": "1.109e-24", + "retained_fraction": "0.604414", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001759649830472077888855", + "windowfree_endpoint": "351929966094415577771/200000000000000000000000", + "windowfree_gain_percent": "1.512772", + "windowfree_unreachable": true + }, + "width7_distribution": [ + [ + 0, + 42 + ], + [ + 2, + 21 + ], + [ + 4, + 0 + ], + [ + 8, + 42 + ], + [ + 7, + 21 + ], + [ + 6, + 0 + ] + ] + }, + "22": { + "idle": { + "2": 411, + "4": 432, + "42": 33, + "6": 402, + "7": 600 + }, + "optimistic": { + "certified_bound": "1755392418851553848853/1000000000000000000000000", + "endpoint": "438848104712888462213/250000000000000000000000", + "endpoint_decimal": "0.001755392418851553848852", + "gain_percent": "1.267165", + "lb_minus_one_at_bound": "2.570e-25", + "retained_fraction": "0.665887", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001766413673139362860825", + "windowfree_endpoint": "70656546925574514433/40000000000000000000000", + "windowfree_gain_percent": "1.902972", + "windowfree_unreachable": true + }, + "pessimistic": { + "certified_bound": "69999383782186044911/40000000000000000000000", + "endpoint": "874992297277325561387/500000000000000000000000", + "endpoint_decimal": "0.001749984594554651122774", + "gain_percent": "0.955192", + "lb_minus_one_at_bound": "2.549e-24", + "retained_fraction": "0.601858", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.00176093778671695228992", + "windowfree_endpoint": "2751465291745237953/1562500000000000000000", + "windowfree_gain_percent": "1.587073", + "windowfree_unreachable": true + }, + "width7_distribution": [ + [ + 0, + 42 + ], + [ + 2, + 24 + ], + [ + 4, + 0 + ], + [ + 8, + 42 + ], + [ + 7, + 24 + ], + [ + 6, + 0 + ] + ] + }, + "23": { + "idle": { + "14": 1, + "2": 409, + "4": 434, + "42": 34, + "6": 397, + "7": 597 + }, + "optimistic": { + "certified_bound": "70257050597313043093/40000000000000000000000", + "endpoint": "439106566233206519331/250000000000000000000000", + "endpoint_decimal": "0.001756426264932826077324", + "gain_percent": "1.326807", + "lb_minus_one_at_bound": "1.999e-24", + "retained_fraction": "0.666716", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001767923329283196106744", + "windowfree_endpoint": "220990416160399513343/125000000000000000000000", + "windowfree_gain_percent": "1.990063", + "windowfree_unreachable": true + }, + "pessimistic": { + "certified_bound": "875389593803073389239/500000000000000000000000", + "endpoint": "1750779187606146778477/1000000000000000000000000", + "endpoint_decimal": "0.001750779187606146778477", + "gain_percent": "1.001031", + "lb_minus_one_at_bound": "6.817e-25", + "retained_fraction": "0.603026", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001762202149104734122094", + "windowfree_endpoint": "881101074552367061047/500000000000000000000000", + "windowfree_gain_percent": "1.660013", + "windowfree_unreachable": true + }, + "width7_distribution": [ + [ + 0, + 46 + ], + [ + 2, + 20 + ], + [ + 4, + 0 + ], + [ + 8, + 46 + ], + [ + 7, + 20 + ], + [ + 6, + 6 + ] + ] + }, + "24": { + "idle": { + "2": 409, + "20": 1, + "4": 431, + "42": 35, + "6": 396, + "7": 594 + }, + "optimistic": { + "certified_bound": "439375112322867772889/250000000000000000000000", + "endpoint": "351500089858294218311/200000000000000000000000", + "endpoint_decimal": "0.001757500449291471091555", + "gain_percent": "1.388775", + "lb_minus_one_at_bound": "1.776e-25", + "retained_fraction": "0.667607", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001769486316891898908698", + "windowfree_endpoint": "884743158445949454349/500000000000000000000000", + "windowfree_gain_percent": "2.080230", + "windowfree_unreachable": true + }, + "pessimistic": { + "certified_bound": "350322672016177147609/200000000000000000000000", + "endpoint": "437903340020221434511/250000000000000000000000", + "endpoint_decimal": "0.001751613360080885738044", + "gain_percent": "1.049154", + "lb_minus_one_at_bound": "2.792e-24", + "retained_fraction": "0.604363", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001763518734841258475571", + "windowfree_endpoint": "1763518734841258475571/1000000000000000000000000", + "windowfree_gain_percent": "1.735965", + "windowfree_unreachable": true + }, + "width7_distribution": [ + [ + 0, + 48 + ], + [ + 2, + 24 + ], + [ + 4, + 0 + ], + [ + 8, + 48 + ], + [ + 7, + 24 + ], + [ + 6, + 0 + ] + ] + }, + "25": { + "idle": { + "2": 408, + "21": 1, + "4": 430, + "42": 36, + "5": 1, + "6": 394, + "7": 591 + }, + "optimistic": { + "certified_bound": "1758460857758681225193/1000000000000000000000000", + "endpoint": "219807607219835153149/125000000000000000000000", + "endpoint_decimal": "0.001758460857758681225192", + "gain_percent": "1.444181", + "lb_minus_one_at_bound": "1.896e-24", + "retained_fraction": "0.665010", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.0017710713392409857771", + "windowfree_endpoint": "17710713392409857771/10000000000000000000000", + "windowfree_gain_percent": "2.171669", + "windowfree_unreachable": true + }, + "pessimistic": { + "certified_bound": "438083509552206000627/250000000000000000000000", + "endpoint": "1752334038208824002507/1000000000000000000000000", + "endpoint_decimal": "0.001752334038208824002507", + "gain_percent": "1.090729", + "lb_minus_one_at_bound": "2.974e-24", + "retained_fraction": "0.601571", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001764856422378060414395", + "windowfree_endpoint": "352971284475612082879/200000000000000000000000", + "windowfree_gain_percent": "1.813136", + "windowfree_unreachable": true + }, + "width7_distribution": [ + [ + 0, + 50 + ], + [ + 2, + 25 + ], + [ + 4, + 0 + ], + [ + 8, + 50 + ], + [ + 7, + 25 + ], + [ + 6, + 0 + ] + ] + }, + "26": { + "idle": { + "2": 407, + "21": 1, + "4": 429, + "42": 37, + "5": 1, + "6": 393, + "7": 588 + }, + "optimistic": { + "certified_bound": "43985240917235468051/25000000000000000000000", + "endpoint": "1759409636689418722039/1000000000000000000000000", + "endpoint_decimal": "0.001759409636689418722039", + "gain_percent": "1.498915", + "lb_minus_one_at_bound": "1.847e-24", + "retained_fraction": "0.664078", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001772552888886713287992", + "windowfree_endpoint": "221569111110839160999/125000000000000000000000", + "windowfree_gain_percent": "2.257139", + "windowfree_unreachable": true + }, + "pessimistic": { + "certified_bound": "876521360514888438823/500000000000000000000000", + "endpoint": "350608544205955375529/200000000000000000000000", + "endpoint_decimal": "0.001753042721029776877645", + "gain_percent": "1.131613", + "lb_minus_one_at_bound": "2.896e-24", + "retained_fraction": "0.600537", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001766090598917588997591", + "windowfree_endpoint": "1766090598917588997591/1000000000000000000000000", + "windowfree_gain_percent": "1.884334", + "windowfree_unreachable": true + }, + "width7_distribution": [ + [ + 0, + 50 + ], + [ + 2, + 28 + ], + [ + 4, + 0 + ], + [ + 8, + 52 + ], + [ + 7, + 26 + ], + [ + 6, + 0 + ] + ] + }, + "27": { + "idle": { + "2": 405, + "28": 1, + "4": 431, + "42": 38, + "6": 390, + "7": 585 + }, + "optimistic": { + "certified_bound": "1760504802988934617047/1000000000000000000000000", + "endpoint": "880252401494467308523/500000000000000000000000", + "endpoint_decimal": "0.001760504802988934617046", + "gain_percent": "1.562094", + "lb_minus_one_at_bound": "2.014e-24", + "retained_fraction": "0.665762", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001774098882916864160214", + "windowfree_endpoint": "887049441458432080107/500000000000000000000000", + "windowfree_gain_percent": "2.346326", + "windowfree_unreachable": true + }, + "pessimistic": { + "certified_bound": "1753896249862764223553/1000000000000000000000000", + "endpoint": "27404628904105690993/15625000000000000000000", + "endpoint_decimal": "0.001753896249862764223552", + "gain_percent": "1.180852", + "lb_minus_one_at_bound": "1.802e-25", + "retained_fraction": "0.602728", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001767387997773151530099", + "windowfree_endpoint": "1767387997773151530099/1000000000000000000000000", + "windowfree_gain_percent": "1.959180", + "windowfree_unreachable": true + }, + "width7_distribution": [ + [ + 0, + 54 + ], + [ + 2, + 24 + ], + [ + 4, + 0 + ], + [ + 8, + 54 + ], + [ + 7, + 24 + ], + [ + 6, + 6 + ] + ] + }, + "28": { + "idle": { + "2": 404, + "34": 1, + "4": 430, + "42": 39, + "6": 388, + "7": 582 + }, + "optimistic": { + "certified_bound": "352321764317168922111/200000000000000000000000", + "endpoint": "880804410792922305277/500000000000000000000000", + "endpoint_decimal": "0.001761608821585844610554", + "gain_percent": "1.625784", + "lb_minus_one_at_bound": "2.145e-24", + "retained_fraction": "0.667899", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001775621706420117170615", + "windowfree_endpoint": "355124341284023434123/200000000000000000000000", + "windowfree_gain_percent": "2.434176", + "windowfree_unreachable": true + }, + "pessimistic": { + "certified_bound": "1754758039661670273367/1000000000000000000000000", + "endpoint": "877379019830835136683/500000000000000000000000", + "endpoint_decimal": "0.001754758039661670273366", + "gain_percent": "1.230568", + "lb_minus_one_at_bound": "1.784e-24", + "retained_fraction": "0.605399", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001768661636465039916523", + "windowfree_endpoint": "1768661636465039916523/1000000000000000000000000", + "windowfree_gain_percent": "2.032655", + "windowfree_unreachable": true + }, + "width7_distribution": [ + [ + 0, + 56 + ], + [ + 2, + 28 + ], + [ + 4, + 0 + ], + [ + 8, + 56 + ], + [ + 7, + 28 + ], + [ + 6, + 0 + ] + ] + }, + "29": { + "idle": { + "2": 403, + "35": 1, + "4": 429, + "42": 40, + "5": 1, + "6": 386, + "7": 579 + }, + "optimistic": { + "certified_bound": "352515749775447349991/200000000000000000000000", + "endpoint": "881289374438618374977/500000000000000000000000", + "endpoint_decimal": "0.001762578748877236749954", + "gain_percent": "1.681738", + "lb_minus_one_at_bound": "1.448e-24", + "retained_fraction": "0.666001", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.00177719833805342055584", + "windowfree_endpoint": "5553744806416939237/3125000000000000000000", + "windowfree_gain_percent": "2.525131", + "windowfree_unreachable": true + }, + "pessimistic": { + "certified_bound": "54858946511608451001/31250000000000000000000", + "endpoint": "1755486288371470432031/1000000000000000000000000", + "endpoint_decimal": "0.001755486288371470432031", + "gain_percent": "1.272580", + "lb_minus_one_at_bound": "2.816e-24", + "retained_fraction": "0.603357", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001769987888491670462225", + "windowfree_endpoint": "70799515539666818489/40000000000000000000000", + "windowfree_gain_percent": "2.109166", + "windowfree_unreachable": true + }, + "width7_distribution": [ + [ + 0, + 58 + ], + [ + 2, + 28 + ], + [ + 4, + 0 + ], + [ + 8, + 58 + ], + [ + 7, + 29 + ], + [ + 6, + 1 + ] + ] + }, + "3": { + "idle": { + "14": 1, + "2": 431, + "4": 444, + "42": 12, + "6": 437, + "7": 657 + }, + "optimistic": { + "certified_bound": "21703527433879803101/12500000000000000000000", + "endpoint": "1736282194710384248079/1000000000000000000000000", + "endpoint_decimal": "0.001736282194710384248079", + "gain_percent": "0.164712", + "lb_minus_one_at_bound": "1.500e-24", + "retained_fraction": "0.655034", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001737785828526572282621", + "windowfree_endpoint": "1737785828526572282621/1000000000000000000000000", + "windowfree_gain_percent": "0.251455", + "windowfree_unreachable": true + }, + "pessimistic": { + "certified_bound": "1735553035608016810371/1000000000000000000000000", + "endpoint": "173555303560801681037/100000000000000000000000", + "endpoint_decimal": "0.00173555303560801681037", + "gain_percent": "0.122647", + "lb_minus_one_at_bound": "1.296e-24", + "retained_fraction": "0.585938", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001737055405325398588442", + "windowfree_endpoint": "868527702662699294221/500000000000000000000000", + "windowfree_gain_percent": "0.209317", + "windowfree_unreachable": true + }, + "width7_distribution": [ + [ + 0, + 6 + ], + [ + 2, + 0 + ], + [ + 4, + 0 + ], + [ + 8, + 6 + ], + [ + 7, + 0 + ], + [ + 6, + 6 + ] + ] + }, + "30": { + "idle": { + "2": 402, + "35": 1, + "4": 428, + "42": 41, + "5": 1, + "6": 385, + "7": 576 + }, + "optimistic": { + "certified_bound": "88176598892601370613/50000000000000000000000", + "endpoint": "1763531977852027412259/1000000000000000000000000", + "endpoint_decimal": "0.001763531977852027412259", + "gain_percent": "1.736729", + "lb_minus_one_at_bound": "6.929e-25", + "retained_fraction": "0.663540", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.00177879720896923166925", + "windowfree_endpoint": "7115188835876926677/4000000000000000000000", + "windowfree_gain_percent": "2.617368", + "windowfree_unreachable": true + }, + "pessimistic": { + "certified_bound": "1756197521865595441237/1000000000000000000000000", + "endpoint": "439049380466398860309/250000000000000000000000", + "endpoint_decimal": "0.001756197521865595441236", + "gain_percent": "1.313611", + "lb_minus_one_at_bound": "5.329e-25", + "retained_fraction": "0.600672", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001771335404534037183197", + "windowfree_endpoint": "1771335404534037183197/1000000000000000000000000", + "windowfree_gain_percent": "2.186903", + "windowfree_unreachable": true + }, + "width7_distribution": [ + [ + 0, + 60 + ], + [ + 2, + 29 + ], + [ + 4, + 0 + ], + [ + 8, + 58 + ], + [ + 7, + 32 + ], + [ + 6, + 1 + ] + ] + }, + "31": { + "idle": { + "2": 400, + "4": 430, + "42": 43, + "6": 382, + "7": 573 + }, + "optimistic": { + "certified_bound": "1764663008093750916959/1000000000000000000000000", + "endpoint": "882331504046875458479/500000000000000000000000", + "endpoint_decimal": "0.001764663008093750916958", + "gain_percent": "1.801978", + "lb_minus_one_at_bound": "2.328e-24", + "retained_fraction": "0.666514", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001780291715481813360838", + "windowfree_endpoint": "890145857740906680419/500000000000000000000000", + "windowfree_gain_percent": "2.703585", + "windowfree_unreachable": true + }, + "pessimistic": { + "certified_bound": "351420402115253497383/200000000000000000000000", + "endpoint": "878551005288133743457/500000000000000000000000", + "endpoint_decimal": "0.001757102010576267486914", + "gain_percent": "1.365790", + "lb_minus_one_at_bound": "2.349e-24", + "retained_fraction": "0.604426", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001772596390013438084387", + "windowfree_endpoint": "1772596390013438084387/1000000000000000000000000", + "windowfree_gain_percent": "2.259648", + "windowfree_unreachable": true + }, + "width7_distribution": [ + [ + 0, + 62 + ], + [ + 2, + 28 + ], + [ + 4, + 0 + ], + [ + 8, + 62 + ], + [ + 7, + 28 + ], + [ + 6, + 6 + ] + ] + }, + "32": { + "idle": { + "14": 1, + "2": 400, + "4": 428, + "42": 44, + "6": 379, + "7": 570 + }, + "optimistic": { + "certified_bound": "882864069907994036431/500000000000000000000000", + "endpoint": "1765728139815988072861/1000000000000000000000000", + "endpoint_decimal": "0.001765728139815988072861", + "gain_percent": "1.863424", + "lb_minus_one_at_bound": "1.634e-24", + "retained_fraction": "0.667045", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001781851241089199281214", + "windowfree_endpoint": "890925620544599640607/500000000000000000000000", + "windowfree_gain_percent": "2.793553", + "windowfree_unreachable": true + }, + "pessimistic": { + "certified_bound": "1757940673064063681529/1000000000000000000000000", + "endpoint": "219742584133007960191/125000000000000000000000", + "endpoint_decimal": "0.001757940673064063681528", + "gain_percent": "1.414172", + "lb_minus_one_at_bound": "7.244e-25", + "retained_fraction": "0.605363", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.00177392112190032035548", + "windowfree_endpoint": "44348028047508008887/25000000000000000000000", + "windowfree_gain_percent": "2.336071", + "windowfree_unreachable": true + }, + "width7_distribution": [ + [ + 0, + 64 + ], + [ + 2, + 32 + ], + [ + 4, + 0 + ], + [ + 8, + 64 + ], + [ + 7, + 32 + ], + [ + 6, + 0 + ] + ] + }, + "33": { + "idle": { + "14": 1, + "2": 399, + "4": 426, + "42": 45, + "5": 2, + "6": 377, + "7": 567 + }, + "optimistic": { + "certified_bound": "1766682821922551979451/1000000000000000000000000", + "endpoint": "35333656438451039589/20000000000000000000000", + "endpoint_decimal": "0.00176668282192255197945", + "gain_percent": "1.918499", + "lb_minus_one_at_bound": "2.762e-24", + "retained_fraction": "0.665643", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001783387404933562338963", + "windowfree_endpoint": "1783387404933562338963/1000000000000000000000000", + "windowfree_gain_percent": "2.882173", + "windowfree_unreachable": true + }, + "pessimistic": { + "certified_bound": "879334706186533317213/500000000000000000000000", + "endpoint": "70346776494922665377/40000000000000000000000", + "endpoint_decimal": "0.001758669412373066634425", + "gain_percent": "1.456212", + "lb_minus_one_at_bound": "2.350e-24", + "retained_fraction": "0.603958", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001775221976828768120969", + "windowfree_endpoint": "1775221976828768120969/1000000000000000000000000", + "windowfree_gain_percent": "2.411116", + "windowfree_unreachable": true + }, + "width7_distribution": [ + [ + 0, + 66 + ], + [ + 2, + 33 + ], + [ + 4, + 0 + ], + [ + 8, + 66 + ], + [ + 7, + 33 + ], + [ + 6, + 0 + ] + ] + }, + "34": { + "idle": { + "14": 1, + "2": 398, + "4": 426, + "42": 46, + "6": 377, + "7": 564 + }, + "optimistic": { + "certified_bound": "441910613968117642891/250000000000000000000000", + "endpoint": "1767642455872470571563/1000000000000000000000000", + "endpoint_decimal": "0.001767642455872470571563", + "gain_percent": "1.973860", + "lb_minus_one_at_bound": "2.186e-24", + "retained_fraction": "0.663722", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001784977859987008208923", + "windowfree_endpoint": "1784977859987008208923/1000000000000000000000000", + "windowfree_gain_percent": "2.973925", + "windowfree_unreachable": true + }, + "pessimistic": { + "certified_bound": "879701319057055421459/500000000000000000000000", + "endpoint": "1759402638114110842917/1000000000000000000000000", + "endpoint_decimal": "0.001759402638114110842917", + "gain_percent": "1.498511", + "lb_minus_one_at_bound": "7.857e-25", + "retained_fraction": "0.602000", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001776575895514210305369", + "windowfree_endpoint": "1776575895514210305369/1000000000000000000000000", + "windowfree_gain_percent": "2.489223", + "windowfree_unreachable": true + }, + "width7_distribution": [ + [ + 0, + 66 + ], + [ + 2, + 36 + ], + [ + 4, + 0 + ], + [ + 8, + 66 + ], + [ + 7, + 36 + ], + [ + 6, + 0 + ] + ] + }, + "35": { + "idle": { + "2": 396, + "20": 1, + "4": 427, + "42": 47, + "6": 374, + "7": 561 + }, + "optimistic": { + "certified_bound": "442177501175919936129/250000000000000000000000", + "endpoint": "353742000940735948903/200000000000000000000000", + "endpoint_decimal": "0.001768710004703679744515", + "gain_percent": "2.035446", + "lb_minus_one_at_bound": "7.191e-25", + "retained_fraction": "0.663666", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001786590761715504823101", + "windowfree_endpoint": "1786590761715504823101/1000000000000000000000000", + "windowfree_gain_percent": "3.066972", + "windowfree_unreachable": true + }, + "pessimistic": { + "certified_bound": "1760242325031025325341/1000000000000000000000000", + "endpoint": "88012116251551266267/50000000000000000000000", + "endpoint_decimal": "0.00176024232503102532534", + "gain_percent": "1.546952", + "lb_minus_one_at_bound": "1.024e-24", + "retained_fraction": "0.602262", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001777951298449145439021", + "windowfree_endpoint": "1777951298449145439021/1000000000000000000000000", + "windowfree_gain_percent": "2.568568", + "windowfree_unreachable": true + }, + "width7_distribution": [ + [ + 0, + 70 + ], + [ + 2, + 32 + ], + [ + 4, + 0 + ], + [ + 8, + 70 + ], + [ + 7, + 32 + ], + [ + 6, + 6 + ] + ] + }, + "36": { + "idle": { + "2": 396, + "28": 1, + "4": 425, + "42": 48, + "6": 372, + "7": 558 + }, + "optimistic": { + "certified_bound": "221231255202696736899/125000000000000000000000", + "endpoint": "1769850041621573895191/1000000000000000000000000", + "endpoint_decimal": "0.001769850041621573895191", + "gain_percent": "2.101213", + "lb_minus_one_at_bound": "1.631e-24", + "retained_fraction": "0.666217", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001788098395769609129334", + "windowfree_endpoint": "894049197884804564667/500000000000000000000000", + "windowfree_gain_percent": "3.153946", + "windowfree_unreachable": true + }, + "pessimistic": { + "certified_bound": "88057665644395826253/50000000000000000000000", + "endpoint": "1761153312887916525059/1000000000000000000000000", + "endpoint_decimal": "0.001761153312887916525059", + "gain_percent": "1.599506", + "lb_minus_one_at_bound": "2.428e-24", + "retained_fraction": "0.605447", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001779221718055879172315", + "windowfree_endpoint": "355844343611175834463/200000000000000000000000", + "windowfree_gain_percent": "2.641858", + "windowfree_unreachable": true + }, + "width7_distribution": [ + [ + 0, + 72 + ], + [ + 2, + 36 + ], + [ + 4, + 0 + ], + [ + 8, + 72 + ], + [ + 7, + 36 + ], + [ + 6, + 0 + ] + ] + }, + "37": { + "idle": { + "2": 395, + "28": 1, + "4": 423, + "42": 49, + "5": 2, + "6": 370, + "7": 555 + }, + "optimistic": { + "certified_bound": "1770809187427053553943/1000000000000000000000000", + "endpoint": "885404593713526776971/500000000000000000000000", + "endpoint_decimal": "0.001770809187427053553942", + "gain_percent": "2.156546", + "lb_minus_one_at_bound": "5.172e-25", + "retained_fraction": "0.664635", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001789671631346367026824", + "windowfree_endpoint": "223708953918295878353/125000000000000000000000", + "windowfree_gain_percent": "3.244705", + "windowfree_unreachable": true + }, + "pessimistic": { + "certified_bound": "1761884716885951335477/1000000000000000000000000", + "endpoint": "440471179221487833869/250000000000000000000000", + "endpoint_decimal": "0.001761884716885951335476", + "gain_percent": "1.641700", + "lb_minus_one_at_bound": "6.941e-25", + "retained_fraction": "0.603821", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001780556367920637129218", + "windowfree_endpoint": "890278183960318564609/500000000000000000000000", + "windowfree_gain_percent": "2.718853", + "windowfree_unreachable": true + }, + "width7_distribution": [ + [ + 0, + 74 + ], + [ + 2, + 37 + ], + [ + 4, + 0 + ], + [ + 8, + 74 + ], + [ + 7, + 37 + ], + [ + 6, + 0 + ] + ] + }, + "38": { + "idle": { + "2": 394, + "28": 1, + "4": 423, + "42": 50, + "6": 370, + "7": 552 + }, + "optimistic": { + "certified_bound": "1771773310666228584789/1000000000000000000000000", + "endpoint": "442943327666557146197/250000000000000000000000", + "endpoint_decimal": "0.001771773310666228584788", + "gain_percent": "2.212165", + "lb_minus_one_at_bound": "5.391e-26", + "retained_fraction": "0.663496", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001791221311556070956683", + "windowfree_endpoint": "1791221311556070956683/1000000000000000000000000", + "windowfree_gain_percent": "3.334105", + "windowfree_unreachable": true + }, + "pessimistic": { + "certified_bound": "440655156209656608647/250000000000000000000000", + "endpoint": "1762620624838626434587/1000000000000000000000000", + "endpoint_decimal": "0.001762620624838626434587", + "gain_percent": "1.684154", + "lb_minus_one_at_bound": "1.842e-24", + "retained_fraction": "0.602676", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001781866969226050037437", + "windowfree_endpoint": "1781866969226050037437/1000000000000000000000000", + "windowfree_gain_percent": "2.794460", + "windowfree_unreachable": true + }, + "width7_distribution": [ + [ + 0, + 74 + ], + [ + 2, + 40 + ], + [ + 4, + 0 + ], + [ + 8, + 74 + ], + [ + 7, + 40 + ], + [ + 6, + 0 + ] + ] + }, + "39": { + "idle": { + "2": 391, + "34": 1, + "4": 426, + "42": 51, + "6": 366, + "7": 549 + }, + "optimistic": { + "certified_bound": "354574202515653208393/200000000000000000000000", + "endpoint": "443217753144566510491/250000000000000000000000", + "endpoint_decimal": "0.001772871012578266041964", + "gain_percent": "2.275491", + "lb_minus_one_at_bound": "3.101e-24", + "retained_fraction": "0.664054", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001792825772583236621384", + "windowfree_endpoint": "224103221572904577673/125000000000000000000000", + "windowfree_gain_percent": "3.426665", + "windowfree_unreachable": true + }, + "pessimistic": { + "certified_bound": "176348827572192368043/100000000000000000000000", + "endpoint": "1763488275721923680429/1000000000000000000000000", + "endpoint_decimal": "0.001763488275721923680429", + "gain_percent": "1.734208", + "lb_minus_one_at_bound": "2.678e-24", + "retained_fraction": "0.603591", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001783231039194929965356", + "windowfree_endpoint": "445807759798732491339/250000000000000000000000", + "windowfree_gain_percent": "2.873152", + "windowfree_unreachable": true + }, + "width7_distribution": [ + [ + 0, + 78 + ], + [ + 2, + 36 + ], + [ + 4, + 0 + ], + [ + 8, + 78 + ], + [ + 7, + 36 + ], + [ + 6, + 6 + ] + ] + }, + "4": { + "idle": { + "2": 431, + "20": 1, + "4": 441, + "42": 13, + "6": 436, + "7": 654 + }, + "optimistic": { + "certified_bound": "27145810528568710931/15625000000000000000000", + "endpoint": "1737331873828397499583/1000000000000000000000000", + "endpoint_decimal": "0.001737331873828397499583", + "gain_percent": "0.225267", + "lb_minus_one_at_bound": "1.996e-24", + "retained_fraction": "0.665340", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001739295973174498110179", + "windowfree_endpoint": "1739295973174498110179/1000000000000000000000000", + "windowfree_gain_percent": "0.338574", + "windowfree_unreachable": true + }, + "pessimistic": { + "certified_bound": "1736358621450252381173/1000000000000000000000000", + "endpoint": "434089655362563095293/250000000000000000000000", + "endpoint_decimal": "0.001736358621450252381172", + "gain_percent": "0.169121", + "lb_minus_one_at_bound": "2.302e-24", + "retained_fraction": "0.599079", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001738320518100529549947", + "windowfree_endpoint": "1738320518100529549947/1000000000000000000000000", + "windowfree_gain_percent": "0.282301", + "windowfree_unreachable": true + }, + "width7_distribution": [ + [ + 0, + 8 + ], + [ + 2, + 4 + ], + [ + 4, + 0 + ], + [ + 8, + 8 + ], + [ + 7, + 4 + ], + [ + 6, + 0 + ] + ] + }, + "40": { + "idle": { + "2": 391, + "4": 424, + "42": 53, + "6": 364, + "7": 546 + }, + "optimistic": { + "certified_bound": "443513140161605817981/250000000000000000000000", + "endpoint": "1774052560646423271923/1000000000000000000000000", + "endpoint_decimal": "0.001774052560646423271923", + "gain_percent": "2.343653", + "lb_minus_one_at_bound": "1.358e-24", + "retained_fraction": "0.665710", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001794452890581441726686", + "windowfree_endpoint": "897226445290720863343/500000000000000000000000", + "windowfree_gain_percent": "3.520532", + "windowfree_unreachable": true + }, + "pessimistic": { + "certified_bound": "1764438373922963686867/1000000000000000000000000", + "endpoint": "882219186961481843433/500000000000000000000000", + "endpoint_decimal": "0.001764438373922963686866", + "gain_percent": "1.789019", + "lb_minus_one_at_bound": "5.965e-25", + "retained_fraction": "0.605812", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001784616762309996405185", + "windowfree_endpoint": "356923352461999281037/200000000000000000000000", + "windowfree_gain_percent": "2.953094", + "windowfree_unreachable": true + }, + "width7_distribution": [ + [ + 0, + 80 + ], + [ + 2, + 40 + ], + [ + 4, + 0 + ], + [ + 8, + 80 + ], + [ + 7, + 40 + ], + [ + 6, + 0 + ] + ] + }, + "41": { + "idle": { + "2": 390, + "4": 422, + "42": 54, + "5": 2, + "6": 362, + "7": 543 + }, + "optimistic": { + "certified_bound": "1775016268051187830899/1000000000000000000000000", + "endpoint": "887508134025593915449/500000000000000000000000", + "endpoint_decimal": "0.001775016268051187830898", + "gain_percent": "2.399249", + "lb_minus_one_at_bound": "1.087e-25", + "retained_fraction": "0.664930", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.00179597382586181304332", + "windowfree_endpoint": "44899345646545326083/25000000000000000000000", + "windowfree_gain_percent": "3.608273", + "windowfree_unreachable": true + }, + "pessimistic": { + "certified_bound": "176517250762109234073/100000000000000000000000", + "endpoint": "1765172507621092340729/1000000000000000000000000", + "endpoint_decimal": "0.001765172507621092340729", + "gain_percent": "1.831370", + "lb_minus_one_at_bound": "1.708e-24", + "retained_fraction": "0.605025", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001785896722237232554952", + "windowfree_endpoint": "223237090279654069369/125000000000000000000000", + "windowfree_gain_percent": "3.026933", + "windowfree_unreachable": true + }, + "width7_distribution": [ + [ + 0, + 82 + ], + [ + 2, + 41 + ], + [ + 4, + 0 + ], + [ + 8, + 82 + ], + [ + 7, + 41 + ], + [ + 6, + 0 + ] + ] + }, + "42": { + "idle": { + "2": 389, + "4": 422, + "42": 55, + "6": 362, + "7": 540 + }, + "optimistic": { + "certified_bound": "1775984979058612131837/1000000000000000000000000", + "endpoint": "443996244764653032959/250000000000000000000000", + "endpoint_decimal": "0.001775984979058612131836", + "gain_percent": "2.455133", + "lb_minus_one_at_bound": "1.838e-24", + "retained_fraction": "0.663579", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001797560952948869937332", + "windowfree_endpoint": "449390238237217484333/250000000000000000000000", + "windowfree_gain_percent": "3.699833", + "windowfree_unreachable": true + }, + "pessimistic": { + "certified_bound": "1765911163230181680457/1000000000000000000000000", + "endpoint": "220738895403772710057/125000000000000000000000", + "endpoint_decimal": "0.001765911163230181680456", + "gain_percent": "1.873983", + "lb_minus_one_at_bound": "2.792e-24", + "retained_fraction": "0.603633", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001787241401797609433989", + "windowfree_endpoint": "1787241401797609433989/1000000000000000000000000", + "windowfree_gain_percent": "3.104507", + "windowfree_unreachable": true + }, + "width7_distribution": [ + [ + 0, + 82 + ], + [ + 2, + 44 + ], + [ + 4, + 0 + ], + [ + 8, + 82 + ], + [ + 7, + 44 + ], + [ + 6, + 0 + ] + ] + }, + "43": { + "idle": { + "14": 1, + "2": 387, + "4": 424, + "42": 56, + "6": 357, + "7": 537 + }, + "optimistic": { + "certified_bound": "1777043231391603053139/1000000000000000000000000", + "endpoint": "888521615695801526569/500000000000000000000000", + "endpoint_decimal": "0.001777043231391603053138", + "gain_percent": "2.516183", + "lb_minus_one_at_bound": "2.641e-24", + "retained_fraction": "0.663896", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001799124328657857631304", + "windowfree_endpoint": "224890541082232203913/125000000000000000000000", + "windowfree_gain_percent": "3.790023", + "windowfree_unreachable": true + }, + "pessimistic": { + "certified_bound": "353347579139285925659/200000000000000000000000", + "endpoint": "883368947848214814147/500000000000000000000000", + "endpoint_decimal": "0.001766737895696429628294", + "gain_percent": "1.921676", + "lb_minus_one_at_bound": "9.237e-25", + "retained_fraction": "0.604171", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001788561859345693234105", + "windowfree_endpoint": "357712371869138646821/200000000000000000000000", + "windowfree_gain_percent": "3.180683", + "windowfree_unreachable": true + }, + "width7_distribution": [ + [ + 0, + 86 + ], + [ + 2, + 40 + ], + [ + 4, + 0 + ], + [ + 8, + 86 + ], + [ + 7, + 40 + ], + [ + 6, + 6 + ] + ] + }, + "44": { + "idle": { + "2": 387, + "20": 1, + "4": 421, + "42": 57, + "6": 356, + "7": 534 + }, + "optimistic": { + "certified_bound": "444535697307914381821/250000000000000000000000", + "endpoint": "1778142789231657527283/1000000000000000000000000", + "endpoint_decimal": "0.001778142789231657527283", + "gain_percent": "2.579615", + "lb_minus_one_at_bound": "3.174e-24", + "retained_fraction": "0.664267", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001800742981440136675067", + "windowfree_endpoint": "1800742981440136675067/1000000000000000000000000", + "windowfree_gain_percent": "3.883402", + "windowfree_unreachable": true + }, + "pessimistic": { + "certified_bound": "1767604972196246702511/1000000000000000000000000", + "endpoint": "176760497219624670251/100000000000000000000000", + "endpoint_decimal": "0.00176760497219624670251", + "gain_percent": "1.971697", + "lb_minus_one_at_bound": "2.307e-24", + "retained_fraction": "0.604821", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001789936195110962406361", + "windowfree_endpoint": "1789936195110962406361/1000000000000000000000000", + "windowfree_gain_percent": "3.259967", + "windowfree_unreachable": true + }, + "width7_distribution": [ + [ + 0, + 88 + ], + [ + 2, + 44 + ], + [ + 4, + 0 + ], + [ + 8, + 88 + ], + [ + 7, + 44 + ], + [ + 6, + 0 + ] + ] + }, + "45": { + "idle": { + "2": 386, + "21": 1, + "4": 420, + "42": 58, + "5": 1, + "6": 354, + "7": 531 + }, + "optimistic": { + "certified_bound": "889562948527471556921/500000000000000000000000", + "endpoint": "1779125897054943113841/1000000000000000000000000", + "endpoint_decimal": "0.001779125897054943113841", + "gain_percent": "2.636330", + "lb_minus_one_at_bound": "2.470e-24", + "retained_fraction": "0.662711", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001802384504447150778913", + "windowfree_endpoint": "1802384504447150778913/1000000000000000000000000", + "windowfree_gain_percent": "3.978100", + "windowfree_unreachable": true + }, + "pessimistic": { + "certified_bound": "884178255832272896057/500000000000000000000000", + "endpoint": "1768356511664545792113/1000000000000000000000000", + "endpoint_decimal": "0.001768356511664545792113", + "gain_percent": "2.015053", + "lb_minus_one_at_bound": "2.183e-24", + "retained_fraction": "0.603217", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001791332354912780995295", + "windowfree_endpoint": "358266470982556199059/200000000000000000000000", + "windowfree_gain_percent": "3.340511", + "windowfree_unreachable": true + }, + "width7_distribution": [ + [ + 0, + 90 + ], + [ + 2, + 45 + ], + [ + 4, + 0 + ], + [ + 8, + 90 + ], + [ + 7, + 45 + ], + [ + 6, + 0 + ] + ] + }, + "46": { + "idle": { + "2": 385, + "21": 1, + "4": 419, + "42": 59, + "5": 1, + "6": 353, + "7": 528 + }, + "optimistic": { + "certified_bound": "445024278278648266577/250000000000000000000000", + "endpoint": "1780097113114593066307/1000000000000000000000000", + "endpoint_decimal": "0.001780097113114593066307", + "gain_percent": "2.692359", + "lb_minus_one_at_bound": "1.034e-24", + "retained_fraction": "0.662063", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001803918917715244555416", + "windowfree_endpoint": "225489864714405569427/125000000000000000000000", + "windowfree_gain_percent": "4.066619", + "windowfree_unreachable": true + }, + "pessimistic": { + "certified_bound": "1769095870528314037209/1000000000000000000000000", + "endpoint": "221136983816039254651/125000000000000000000000", + "endpoint_decimal": "0.001769095870528314037208", + "gain_percent": "2.057706", + "lb_minus_one_at_bound": "7.733e-25", + "retained_fraction": "0.602566", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.00179262196295230277064", + "windowfree_endpoint": "22407774536903784633/12500000000000000000000", + "windowfree_gain_percent": "3.414907", + "windowfree_unreachable": true + }, + "width7_distribution": [ + [ + 0, + 90 + ], + [ + 2, + 48 + ], + [ + 4, + 0 + ], + [ + 8, + 92 + ], + [ + 7, + 46 + ], + [ + 6, + 0 + ] + ] + }, + "47": { + "idle": { + "2": 383, + "28": 1, + "4": 421, + "42": 60, + "6": 350, + "7": 525 + }, + "optimistic": { + "certified_bound": "222652274038024291717/125000000000000000000000", + "endpoint": "356243638460838866747/200000000000000000000000", + "endpoint_decimal": "0.001781218192304194333735", + "gain_percent": "2.757033", + "lb_minus_one_at_bound": "1.305e-24", + "retained_fraction": "0.662909", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001805520121072081379214", + "windowfree_endpoint": "902760060536040689607/500000000000000000000000", + "windowfree_gain_percent": "4.158991", + "windowfree_unreachable": true + }, + "pessimistic": { + "certified_bound": "1769982777013209001461/1000000000000000000000000", + "endpoint": "88499138850660450073/50000000000000000000000", + "endpoint_decimal": "0.00176998277701320900146", + "gain_percent": "2.108871", + "lb_minus_one_at_bound": "1.390e-24", + "retained_fraction": "0.603731", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001793976785609002254295", + "windowfree_endpoint": "358795357121800450859/200000000000000000000000", + "windowfree_gain_percent": "3.493066", + "windowfree_unreachable": true + }, + "width7_distribution": [ + [ + 0, + 94 + ], + [ + 2, + 44 + ], + [ + 4, + 0 + ], + [ + 8, + 94 + ], + [ + 7, + 44 + ], + [ + 6, + 6 + ] + ] + }, + "48": { + "idle": { + "2": 382, + "34": 1, + "4": 420, + "42": 61, + "6": 348, + "7": 522 + }, + "optimistic": { + "certified_bound": "891174174829900925921/500000000000000000000000", + "endpoint": "1782348349659801851841/1000000000000000000000000", + "endpoint_decimal": "0.001782348349659801851841", + "gain_percent": "2.822231", + "lb_minus_one_at_bound": "6.817e-25", + "retained_fraction": "0.664057", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001807097374592966321348", + "windowfree_endpoint": "451774343648241580337/250000000000000000000000", + "windowfree_gain_percent": "4.249982", + "windowfree_unreachable": true + }, + "pessimistic": { + "certified_bound": "1770878139528467808249/1000000000000000000000000", + "endpoint": "221359767441058476031/125000000000000000000000", + "endpoint_decimal": "0.001770878139528467808248", + "gain_percent": "2.160524", + "lb_minus_one_at_bound": "2.619e-24", + "retained_fraction": "0.605220", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001795307210921745754892", + "windowfree_endpoint": "448826802730436438723/250000000000000000000000", + "windowfree_gain_percent": "3.569817", + "windowfree_unreachable": true + }, + "width7_distribution": [ + [ + 0, + 96 + ], + [ + 2, + 48 + ], + [ + 4, + 0 + ], + [ + 8, + 96 + ], + [ + 7, + 48 + ], + [ + 6, + 0 + ] + ] + }, + "49": { + "idle": { + "2": 381, + "35": 1, + "4": 419, + "42": 62, + "5": 1, + "6": 346, + "7": 519 + }, + "optimistic": { + "certified_bound": "178334125567092398941/100000000000000000000000", + "endpoint": "1783341255670923989409/1000000000000000000000000", + "endpoint_decimal": "0.001783341255670923989409", + "gain_percent": "2.879511", + "lb_minus_one_at_bound": "1.804e-24", + "retained_fraction": "0.662842", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001808730408211207476258", + "windowfree_endpoint": "904365204105603738129/500000000000000000000000", + "windowfree_gain_percent": "4.344190", + "windowfree_unreachable": true + }, + "pessimistic": { + "certified_bound": "885818768655640676869/500000000000000000000000", + "endpoint": "1771637537311281353737/1000000000000000000000000", + "endpoint_decimal": "0.001771637537311281353737", + "gain_percent": "2.204333", + "lb_minus_one_at_bound": "8.935e-25", + "retained_fraction": "0.603976", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001796691928723952476988", + "windowfree_endpoint": "449172982180988119247/250000000000000000000000", + "windowfree_gain_percent": "3.649700", + "windowfree_unreachable": true + }, + "width7_distribution": [ + [ + 0, + 98 + ], + [ + 2, + 48 + ], + [ + 4, + 0 + ], + [ + 8, + 98 + ], + [ + 7, + 49 + ], + [ + 6, + 1 + ] + ] + }, + "5": { + "idle": { + "2": 430, + "21": 1, + "4": 440, + "42": 14, + "5": 1, + "6": 434, + "7": 651 + }, + "optimistic": { + "certified_bound": "434567590029703483473/250000000000000000000000", + "endpoint": "1738270360118813933891/1000000000000000000000000", + "endpoint_decimal": "0.001738270360118813933891", + "gain_percent": "0.279407", + "lb_minus_one_at_bound": "2.126e-24", + "retained_fraction": "0.654474", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001740827361879356617556", + "windowfree_endpoint": "435206840469839154389/250000000000000000000000", + "windowfree_gain_percent": "0.426919", + "windowfree_unreachable": true + }, + "pessimistic": { + "certified_bound": "434263162481061730423/250000000000000000000000", + "endpoint": "1737052649924246921691/1000000000000000000000000", + "endpoint_decimal": "0.001737052649924246921691", + "gain_percent": "0.209159", + "lb_minus_one_at_bound": "1.171e-24", + "retained_fraction": "0.586761", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001739606065404019878544", + "windowfree_endpoint": "108725379087751242409/62500000000000000000000", + "windowfree_gain_percent": "0.356463", + "windowfree_unreachable": true + }, + "width7_distribution": [ + [ + 0, + 10 + ], + [ + 2, + 5 + ], + [ + 4, + 0 + ], + [ + 8, + 10 + ], + [ + 7, + 5 + ], + [ + 6, + 0 + ] + ] + }, + "50": { + "idle": { + "2": 380, + "35": 1, + "4": 418, + "42": 63, + "5": 1, + "6": 345, + "7": 516 + }, + "optimistic": { + "certified_bound": "1784317080745667523951/1000000000000000000000000", + "endpoint": "35686341614913350479/20000000000000000000000", + "endpoint_decimal": "0.00178431708074566752395", + "gain_percent": "2.935805", + "lb_minus_one_at_bound": "1.543e-24", + "retained_fraction": "0.661258", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001810386528321116966112", + "windowfree_endpoint": "56574579010034905191/31250000000000000000000", + "windowfree_gain_percent": "4.439730", + "windowfree_unreachable": true + }, + "pessimistic": { + "certified_bound": "886189820479707573269/500000000000000000000000", + "endpoint": "1772379640959415146537/1000000000000000000000000", + "endpoint_decimal": "0.001772379640959415146537", + "gain_percent": "2.247144", + "lb_minus_one_at_bound": "1.845e-25", + "retained_fraction": "0.602314", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001798098643478155937176", + "windowfree_endpoint": "224762330434769492147/125000000000000000000000", + "windowfree_gain_percent": "3.730852", + "windowfree_unreachable": true + }, + "width7_distribution": [ + [ + 0, + 100 + ], + [ + 2, + 49 + ], + [ + 4, + 0 + ], + [ + 8, + 98 + ], + [ + 7, + 52 + ], + [ + 6, + 1 + ] + ] + }, + "51": { + "idle": { + "2": 378, + "4": 420, + "42": 65, + "6": 342, + "7": 513 + }, + "optimistic": { + "certified_bound": "71418997410478340649/40000000000000000000000", + "endpoint": "3487255732933512727/1953125000000000000000", + "endpoint_decimal": "0.001785474935261958516224", + "gain_percent": "3.002601", + "lb_minus_one_at_bound": "2.041e-24", + "retained_fraction": "0.662967", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001811934599483512354478", + "windowfree_endpoint": "905967299741756177239/500000000000000000000000", + "windowfree_gain_percent": "4.529037", + "windowfree_unreachable": true + }, + "pessimistic": { + "certified_bound": "443325216639099076641/250000000000000000000000", + "endpoint": "1773300866556396306563/1000000000000000000000000", + "endpoint_decimal": "0.001773300866556396306563", + "gain_percent": "2.300289", + "lb_minus_one_at_bound": "9.737e-25", + "retained_fraction": "0.604415", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001799398009050532923647", + "windowfree_endpoint": "1799398009050532923647/1000000000000000000000000", + "windowfree_gain_percent": "3.805812", + "windowfree_unreachable": true + }, + "width7_distribution": [ + [ + 0, + 102 + ], + [ + 2, + 48 + ], + [ + 4, + 0 + ], + [ + 8, + 102 + ], + [ + 7, + 48 + ], + [ + 6, + 6 + ] + ] + }, + "52": { + "idle": { + "14": 1, + "2": 378, + "4": 418, + "42": 66, + "6": 339, + "7": 510 + }, + "optimistic": { + "certified_bound": "1786565347181794677507/1000000000000000000000000", + "endpoint": "893282673590897338753/500000000000000000000000", + "endpoint_decimal": "0.001786565347181794677506", + "gain_percent": "3.065506", + "lb_minus_one_at_bound": "1.365e-24", + "retained_fraction": "0.663209", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001813550067159790351208", + "windowfree_endpoint": "226693758394973793901/125000000000000000000000", + "windowfree_gain_percent": "4.622232", + "windowfree_unreachable": true + }, + "pessimistic": { + "certified_bound": "443538764354310567513/250000000000000000000000", + "endpoint": "1774155057417242270051/1000000000000000000000000", + "endpoint_decimal": "0.001774155057417242270051", + "gain_percent": "2.349566", + "lb_minus_one_at_bound": "1.226e-24", + "retained_fraction": "0.604847", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001800763089919006232047", + "windowfree_endpoint": "1800763089919006232047/1000000000000000000000000", + "windowfree_gain_percent": "3.884562", + "windowfree_unreachable": true + }, + "width7_distribution": [ + [ + 0, + 104 + ], + [ + 2, + 52 + ], + [ + 4, + 0 + ], + [ + 8, + 104 + ], + [ + 7, + 52 + ], + [ + 6, + 0 + ] + ] + }, + "53": { + "idle": { + "14": 1, + "2": 377, + "4": 416, + "42": 67, + "5": 2, + "6": 337, + "7": 507 + }, + "optimistic": { + "certified_bound": "71501708039654643361/40000000000000000000000", + "endpoint": "223442837623920760503/125000000000000000000000", + "endpoint_decimal": "0.001787542700991366084024", + "gain_percent": "3.121889", + "lb_minus_one_at_bound": "2.134e-24", + "retained_fraction": "0.662254", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001815141384054657838136", + "windowfree_endpoint": "226892673006832229767/125000000000000000000000", + "windowfree_gain_percent": "4.714034", + "windowfree_unreachable": true + }, + "pessimistic": { + "certified_bound": "887448647525950140087/500000000000000000000000", + "endpoint": "1774897295051900280173/1000000000000000000000000", + "endpoint_decimal": "0.001774897295051900280173", + "gain_percent": "2.392385", + "lb_minus_one_at_bound": "2.950e-24", + "retained_fraction": "0.603849", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001802103596205987678904", + "windowfree_endpoint": "225262949525748459863/125000000000000000000000", + "windowfree_gain_percent": "3.961895", + "windowfree_unreachable": true + }, + "width7_distribution": [ + [ + 0, + 106 + ], + [ + 2, + 53 + ], + [ + 4, + 0 + ], + [ + 8, + 106 + ], + [ + 7, + 53 + ], + [ + 6, + 0 + ] + ] + }, + "54": { + "idle": { + "14": 1, + "2": 376, + "4": 416, + "42": 68, + "6": 337, + "7": 504 + }, + "optimistic": { + "certified_bound": "447131284199111488623/250000000000000000000000", + "endpoint": "1788525136796445954491/1000000000000000000000000", + "endpoint_decimal": "0.001788525136796445954491", + "gain_percent": "3.178565", + "lb_minus_one_at_bound": "1.375e-24", + "retained_fraction": "0.660950", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.00181678899096271982437", + "windowfree_endpoint": "181678899096271982437/100000000000000000000000", + "windowfree_gain_percent": "4.809083", + "windowfree_unreachable": true + }, + "pessimistic": { + "certified_bound": "887822053972035645511/500000000000000000000000", + "endpoint": "1775644107944071291021/1000000000000000000000000", + "endpoint_decimal": "0.001775644107944071291021", + "gain_percent": "2.435468", + "lb_minus_one_at_bound": "1.909e-25", + "retained_fraction": "0.602483", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001803498814045955152132", + "windowfree_endpoint": "450874703511488788033/250000000000000000000000", + "windowfree_gain_percent": "4.042384", + "windowfree_unreachable": true + }, + "width7_distribution": [ + [ + 0, + 106 + ], + [ + 2, + 56 + ], + [ + 4, + 0 + ], + [ + 8, + 106 + ], + [ + 7, + 56 + ], + [ + 6, + 0 + ] + ] + }, + "55": { + "idle": { + "2": 374, + "20": 1, + "4": 417, + "42": 69, + "6": 334, + "7": 501 + }, + "optimistic": { + "certified_bound": "357923613219758999133/200000000000000000000000", + "endpoint": "111851129131174687229/62500000000000000000000", + "endpoint_decimal": "0.001789618066098794995664", + "gain_percent": "3.241615", + "lb_minus_one_at_bound": "9.667e-25", + "retained_fraction": "0.660815", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001818459903699457001954", + "windowfree_endpoint": "909229951849728500977/500000000000000000000000", + "windowfree_gain_percent": "4.905477", + "windowfree_unreachable": true + }, + "pessimistic": { + "certified_bound": "888249681142792392993/500000000000000000000000", + "endpoint": "355299872457116957197/200000000000000000000000", + "endpoint_decimal": "0.001776499362285584785985", + "gain_percent": "2.484807", + "lb_minus_one_at_bound": "2.554e-24", + "retained_fraction": "0.602501", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001804916203810485777792", + "windowfree_endpoint": "14100907842269420139/7812500000000000000000", + "windowfree_gain_percent": "4.124152", + "windowfree_unreachable": true + }, + "width7_distribution": [ + [ + 0, + 110 + ], + [ + 2, + 52 + ], + [ + 4, + 0 + ], + [ + 8, + 110 + ], + [ + 7, + 52 + ], + [ + 6, + 6 + ] + ] + }, + "56": { + "idle": { + "2": 374, + "28": 1, + "4": 415, + "42": 70, + "6": 332, + "7": 498 + }, + "optimistic": { + "certified_bound": "895392611424552257411/500000000000000000000000", + "endpoint": "1790785222849104514821/1000000000000000000000000", + "endpoint_decimal": "0.001790785222849104514821", + "gain_percent": "3.308947", + "lb_minus_one_at_bound": "8.426e-25", + "retained_fraction": "0.662375", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.00182002181587810261589", + "windowfree_endpoint": "182002181587810261589/100000000000000000000000", + "windowfree_gain_percent": "4.995582", + "windowfree_unreachable": true + }, + "pessimistic": { + "certified_bound": "1777427247431766372651/1000000000000000000000000", + "endpoint": "35548544948635327453/20000000000000000000000", + "endpoint_decimal": "0.00177742724743176637265", + "gain_percent": "2.538336", + "lb_minus_one_at_bound": "2.430e-24", + "retained_fraction": "0.604412", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001806225437995932150308", + "windowfree_endpoint": "451556359498983037577/250000000000000000000000", + "windowfree_gain_percent": "4.199681", + "windowfree_unreachable": true + }, + "width7_distribution": [ + [ + 0, + 112 + ], + [ + 2, + 56 + ], + [ + 4, + 0 + ], + [ + 8, + 112 + ], + [ + 7, + 56 + ], + [ + 6, + 0 + ] + ] + }, + "57": { + "idle": { + "2": 373, + "28": 1, + "4": 413, + "42": 71, + "5": 2, + "6": 330, + "7": 495 + }, + "optimistic": { + "certified_bound": "358353440098593998693/200000000000000000000000", + "endpoint": "223970900061621249183/125000000000000000000000", + "endpoint_decimal": "0.001791767200492969993464", + "gain_percent": "3.365597", + "lb_minus_one_at_bound": "1.054e-24", + "retained_fraction": "0.661268", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001821651739287210566448", + "windowfree_endpoint": "113853233705450660403/62500000000000000000000", + "windowfree_gain_percent": "5.089611", + "windowfree_unreachable": true + }, + "pessimistic": { + "certified_bound": "1778172224150067273073/1000000000000000000000000", + "endpoint": "111135764009379204567/62500000000000000000000", + "endpoint_decimal": "0.001778172224150067273072", + "gain_percent": "2.581313", + "lb_minus_one_at_bound": "1.962e-24", + "retained_fraction": "0.603247", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001807600893938887777475", + "windowfree_endpoint": "72304035757555511099/40000000000000000000000", + "windowfree_gain_percent": "4.279029", + "windowfree_unreachable": true + }, + "width7_distribution": [ + [ + 0, + 114 + ], + [ + 2, + 57 + ], + [ + 4, + 0 + ], + [ + 8, + 114 + ], + [ + 7, + 57 + ], + [ + 6, + 0 + ] + ] + }, + "58": { + "idle": { + "2": 372, + "28": 1, + "4": 413, + "42": 72, + "6": 330, + "7": 492 + }, + "optimistic": { + "certified_bound": "448188571682525860807/250000000000000000000000", + "endpoint": "1792754286730103443227/1000000000000000000000000", + "endpoint_decimal": "0.001792754286730103443227", + "gain_percent": "3.422541", + "lb_minus_one_at_bound": "1.219e-24", + "retained_fraction": "0.660437", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001823257308440319312159", + "windowfree_endpoint": "1823257308440319312159/1000000000000000000000000", + "windowfree_gain_percent": "5.182235", + "windowfree_unreachable": true + }, + "pessimistic": { + "certified_bound": "3474456629237064853/1953125000000000000000", + "endpoint": "355784358833875440947/200000000000000000000000", + "endpoint_decimal": "0.001778921794169377204735", + "gain_percent": "2.624555", + "lb_minus_one_at_bound": "2.923e-24", + "retained_fraction": "0.602384", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001808951596129293475659", + "windowfree_endpoint": "1808951596129293475659/1000000000000000000000000", + "windowfree_gain_percent": "4.356950", + "windowfree_unreachable": true + }, + "width7_distribution": [ + [ + 0, + 114 + ], + [ + 2, + 60 + ], + [ + 4, + 0 + ], + [ + 8, + 114 + ], + [ + 7, + 60 + ], + [ + 6, + 0 + ] + ] + }, + "59": { + "idle": { + "2": 369, + "34": 1, + "4": 416, + "42": 73, + "6": 326, + "7": 489 + }, + "optimistic": { + "certified_bound": "896939073481380082719/500000000000000000000000", + "endpoint": "1793878146962760165437/1000000000000000000000000", + "endpoint_decimal": "0.001793878146962760165437", + "gain_percent": "3.487375", + "lb_minus_one_at_bound": "8.211e-25", + "retained_fraction": "0.660721", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001824919684540601679408", + "windowfree_endpoint": "114057480283787604963/62500000000000000000000", + "windowfree_gain_percent": "5.278136", + "windowfree_unreachable": true + }, + "pessimistic": { + "certified_bound": "355961111987620545473/200000000000000000000000", + "endpoint": "444951389984525681841/250000000000000000000000", + "endpoint_decimal": "0.001779805559938102727364", + "gain_percent": "2.675539", + "lb_minus_one_at_bound": "2.282e-25", + "retained_fraction": "0.602863", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.00181035743380154188234", + "windowfree_endpoint": "90517871690077094117/50000000000000000000000", + "windowfree_gain_percent": "4.438052", + "windowfree_unreachable": true + }, + "width7_distribution": [ + [ + 0, + 118 + ], + [ + 2, + 56 + ], + [ + 4, + 0 + ], + [ + 8, + 118 + ], + [ + 7, + 56 + ], + [ + 6, + 6 + ] + ] + }, + "6": { + "idle": { + "2": 429, + "21": 1, + "4": 439, + "42": 15, + "5": 1, + "6": 433, + "7": 648 + }, + "optimistic": { + "certified_bound": "173919747053991766211/100000000000000000000000", + "endpoint": "1739197470539917662109/1000000000000000000000000", + "endpoint_decimal": "0.001739197470539917662109", + "gain_percent": "0.332891", + "lb_minus_one_at_bound": "2.395e-25", + "retained_fraction": "0.653378", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001742258732839957487271", + "windowfree_endpoint": "1742258732839957487271/1000000000000000000000000", + "windowfree_gain_percent": "0.509493", + "windowfree_unreachable": true + }, + "pessimistic": { + "certified_bound": "1737734863522697566559/1000000000000000000000000", + "endpoint": "868867431761348783279/500000000000000000000000", + "endpoint_decimal": "0.001737734863522697566558", + "gain_percent": "0.248515", + "lb_minus_one_at_bound": "1.640e-24", + "retained_fraction": "0.584990", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001740790971074191536598", + "windowfree_endpoint": "870395485537095768299/500000000000000000000000", + "windowfree_gain_percent": "0.424819", + "windowfree_unreachable": true + }, + "width7_distribution": [ + [ + 0, + 10 + ], + [ + 2, + 8 + ], + [ + 4, + 0 + ], + [ + 8, + 12 + ], + [ + 7, + 6 + ], + [ + 6, + 0 + ] + ] + }, + "60": { + "idle": { + "2": 369, + "4": 414, + "42": 75, + "6": 324, + "7": 486 + }, + "optimistic": { + "certified_bound": "448771967120584809139/250000000000000000000000", + "endpoint": "359017573696467847311/200000000000000000000000", + "endpoint_decimal": "0.001795087868482339236555", + "gain_percent": "3.557163", + "lb_minus_one_at_bound": "2.839e-24", + "retained_fraction": "0.661749", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001826605588934817674247", + "windowfree_endpoint": "1826605588934817674247/1000000000000000000000000", + "windowfree_gain_percent": "5.375395", + "windowfree_unreachable": true + }, + "pessimistic": { + "certified_bound": "445193328244652420507/250000000000000000000000", + "endpoint": "1780773312978609682027/1000000000000000000000000", + "endpoint_decimal": "0.001780773312978609682027", + "gain_percent": "2.731368", + "lb_minus_one_at_bound": "2.327e-24", + "retained_fraction": "0.604226", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001811785620460707912821", + "windowfree_endpoint": "1811785620460707912821/1000000000000000000000000", + "windowfree_gain_percent": "4.520443", + "windowfree_unreachable": true + }, + "width7_distribution": [ + [ + 0, + 120 + ], + [ + 2, + 60 + ], + [ + 4, + 0 + ], + [ + 8, + 120 + ], + [ + 7, + 60 + ], + [ + 6, + 0 + ] + ] + }, + "61": { + "idle": { + "2": 368, + "4": 412, + "42": 76, + "5": 2, + "6": 322, + "7": 483 + }, + "optimistic": { + "certified_bound": "35921491435259234169/20000000000000000000000", + "endpoint": "1796074571762961708449/1000000000000000000000000", + "endpoint_decimal": "0.001796074571762961708449", + "gain_percent": "3.614085", + "lb_minus_one_at_bound": "1.544e-24", + "retained_fraction": "0.661156", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001828181528539168004781", + "windowfree_endpoint": "1828181528539168004781/1000000000000000000000000", + "windowfree_gain_percent": "5.466310", + "windowfree_unreachable": true + }, + "pessimistic": { + "certified_bound": "222690136968394700837/125000000000000000000000", + "endpoint": "356304219149431521339/200000000000000000000000", + "endpoint_decimal": "0.001781521095747157606695", + "gain_percent": "2.774507", + "lb_minus_one_at_bound": "4.068e-25", + "retained_fraction": "0.603607", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001813104836030644332546", + "windowfree_endpoint": "906552418015322166273/500000000000000000000000", + "windowfree_gain_percent": "4.596547", + "windowfree_unreachable": true + }, + "width7_distribution": [ + [ + 0, + 122 + ], + [ + 2, + 61 + ], + [ + 4, + 0 + ], + [ + 8, + 122 + ], + [ + 7, + 61 + ], + [ + 6, + 0 + ] + ] + }, + "62": { + "idle": { + "2": 367, + "4": 412, + "42": 77, + "6": 322, + "7": 480 + }, + "optimistic": { + "certified_bound": "1797066410838626471909/1000000000000000000000000", + "endpoint": "449266602709656617977/250000000000000000000000", + "endpoint_decimal": "0.001797066410838626471908", + "gain_percent": "3.671304", + "lb_minus_one_at_bound": "1.910e-24", + "retained_fraction": "0.660166", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001829826102533750638131", + "windowfree_endpoint": "1829826102533750638131/1000000000000000000000000", + "windowfree_gain_percent": "5.561184", + "windowfree_unreachable": true + }, + "pessimistic": { + "certified_bound": "89113674515392896523/50000000000000000000000", + "endpoint": "1782273490307857930459/1000000000000000000000000", + "endpoint_decimal": "0.001782273490307857930459", + "gain_percent": "2.817912", + "lb_minus_one_at_bound": "2.487e-24", + "retained_fraction": "0.602568", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001814490785691299652247", + "windowfree_endpoint": "1814490785691299652247/1000000000000000000000000", + "windowfree_gain_percent": "4.676502", + "windowfree_unreachable": true + }, + "width7_distribution": [ + [ + 0, + 122 + ], + [ + 2, + 64 + ], + [ + 4, + 0 + ], + [ + 8, + 122 + ], + [ + 7, + 64 + ], + [ + 6, + 0 + ] + ] + }, + "63": { + "idle": { + "14": 1, + "2": 365, + "4": 414, + "42": 78, + "6": 317, + "7": 477 + }, + "optimistic": { + "certified_bound": "1798149943968650176033/1000000000000000000000000", + "endpoint": "56192185749020318001/31250000000000000000000", + "endpoint_decimal": "0.001798149943968650176032", + "gain_percent": "3.733812", + "lb_minus_one_at_bound": "2.396e-24", + "retained_fraction": "0.660309", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001831446116226194524244", + "windowfree_endpoint": "457861529056548631061/250000000000000000000000", + "windowfree_gain_percent": "5.654641", + "windowfree_unreachable": true + }, + "pessimistic": { + "certified_bound": "445778901906082712171/250000000000000000000000", + "endpoint": "1783115607624330848683/1000000000000000000000000", + "endpoint_decimal": "0.001783115607624330848683", + "gain_percent": "2.866493", + "lb_minus_one_at_bound": "2.440e-25", + "retained_fraction": "0.602835", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001815851800466673794732", + "windowfree_endpoint": "453962950116668448683/250000000000000000000000", + "windowfree_gain_percent": "4.755018", + "windowfree_unreachable": true + }, + "width7_distribution": [ + [ + 0, + 126 + ], + [ + 2, + 60 + ], + [ + 4, + 0 + ], + [ + 8, + 126 + ], + [ + 7, + 60 + ], + [ + 6, + 6 + ] + ] + }, + "64": { + "idle": { + "2": 365, + "20": 1, + "4": 411, + "42": 79, + "6": 316, + "7": 474 + }, + "optimistic": { + "certified_bound": "359855157007315588383/200000000000000000000000", + "endpoint": "899637892518288970957/500000000000000000000000", + "endpoint_decimal": "0.001799275785036577941914", + "gain_percent": "3.798761", + "lb_minus_one_at_bound": "2.934e-24", + "retained_fraction": "0.660493", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001833123460947206687319", + "windowfree_endpoint": "1833123460947206687319/1000000000000000000000000", + "windowfree_gain_percent": "5.751406", + "windowfree_unreachable": true + }, + "pessimistic": { + "certified_bound": "891999413689993432787/500000000000000000000000", + "endpoint": "1783998827379986865573/1000000000000000000000000", + "endpoint_decimal": "0.001783998827379986865573", + "gain_percent": "2.917445", + "lb_minus_one_at_bound": "1.643e-24", + "retained_fraction": "0.603184", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001817268379593606199578", + "windowfree_endpoint": "908634189796803099789/500000000000000000000000", + "windowfree_gain_percent": "4.836739", + "windowfree_unreachable": true + }, + "width7_distribution": [ + [ + 0, + 128 + ], + [ + 2, + 64 + ], + [ + 4, + 0 + ], + [ + 8, + 128 + ], + [ + 7, + 64 + ], + [ + 6, + 0 + ] + ] + }, + "65": { + "idle": { + "2": 364, + "21": 1, + "4": 410, + "42": 80, + "5": 1, + "6": 314, + "7": 471 + }, + "optimistic": { + "certified_bound": "1800282406569969106089/1000000000000000000000000", + "endpoint": "225035300821246138261/125000000000000000000000", + "endpoint_decimal": "0.001800282406569969106088", + "gain_percent": "3.856832", + "lb_minus_one_at_bound": "2.985e-24", + "retained_fraction": "0.659339", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001834824559615220660834", + "windowfree_endpoint": "917412279807610330417/500000000000000000000000", + "windowfree_gain_percent": "5.849541", + "windowfree_unreachable": true + }, + "pessimistic": { + "certified_bound": "892382182422784974261/500000000000000000000000", + "endpoint": "1784764364845569948521/1000000000000000000000000", + "endpoint_decimal": "0.001784764364845569948521", + "gain_percent": "2.961609", + "lb_minus_one_at_bound": "2.019e-24", + "retained_fraction": "0.601982", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001818707486892917101347", + "windowfree_endpoint": "1818707486892917101347/1000000000000000000000000", + "windowfree_gain_percent": "4.919760", + "windowfree_unreachable": true + }, + "width7_distribution": [ + [ + 0, + 130 + ], + [ + 2, + 65 + ], + [ + 4, + 0 + ], + [ + 8, + 130 + ], + [ + 7, + 65 + ], + [ + 6, + 0 + ] + ] + }, + "66": { + "idle": { + "2": 363, + "21": 1, + "4": 409, + "42": 81, + "5": 1, + "6": 313, + "7": 468 + }, + "optimistic": { + "certified_bound": "1801276865164076882307/1000000000000000000000000", + "endpoint": "900638432582038441153/500000000000000000000000", + "endpoint_decimal": "0.001801276865164076882306", + "gain_percent": "3.914201", + "lb_minus_one_at_bound": "2.546e-24", + "retained_fraction": "0.658815", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001836414716416322767724", + "windowfree_endpoint": "459103679104080691931/250000000000000000000000", + "windowfree_gain_percent": "5.941276", + "windowfree_unreachable": true + }, + "pessimistic": { + "certified_bound": "178551750081308413751/100000000000000000000000", + "endpoint": "1785517500813084137509/1000000000000000000000000", + "endpoint_decimal": "0.001785517500813084137509", + "gain_percent": "3.005056", + "lb_minus_one_at_bound": "7.047e-25", + "retained_fraction": "0.601439", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001820036798342255074588", + "windowfree_endpoint": "455009199585563768647/250000000000000000000000", + "windowfree_gain_percent": "4.996447", + "windowfree_unreachable": true + }, + "width7_distribution": [ + [ + 0, + 130 + ], + [ + 2, + 68 + ], + [ + 4, + 0 + ], + [ + 8, + 132 + ], + [ + 7, + 66 + ], + [ + 6, + 0 + ] + ] + }, + "67": { + "idle": { + "2": 361, + "28": 1, + "4": 411, + "42": 82, + "6": 310, + "7": 465 + }, + "optimistic": { + "certified_bound": "360484957584368276809/200000000000000000000000", + "endpoint": "450606196980460346011/250000000000000000000000", + "endpoint_decimal": "0.001802424787921841384044", + "gain_percent": "3.980424", + "lb_minus_one_at_bound": "3.137e-24", + "retained_fraction": "0.659337", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001838074139365852880514", + "windowfree_endpoint": "919037069682926440257/500000000000000000000000", + "windowfree_gain_percent": "6.037006", + "windowfree_unreachable": true + }, + "pessimistic": { + "certified_bound": "446605235342557252389/250000000000000000000000", + "endpoint": "357284188274045801911/200000000000000000000000", + "endpoint_decimal": "0.001786420941370229009555", + "gain_percent": "3.057175", + "lb_minus_one_at_bound": "2.204e-24", + "retained_fraction": "0.602160", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001821433362178349626866", + "windowfree_endpoint": "910716681089174813433/500000000000000000000000", + "windowfree_gain_percent": "5.077013", + "windowfree_unreachable": true + }, + "width7_distribution": [ + [ + 0, + 134 + ], + [ + 2, + 64 + ], + [ + 4, + 0 + ], + [ + 8, + 134 + ], + [ + 7, + 64 + ], + [ + 6, + 6 + ] + ] + }, + "68": { + "idle": { + "2": 360, + "34": 1, + "4": 410, + "42": 83, + "6": 308, + "7": 462 + }, + "optimistic": { + "certified_bound": "901791011711650214329/500000000000000000000000", + "endpoint": "1803582023423300428657/1000000000000000000000000", + "endpoint_decimal": "0.001803582023423300428657", + "gain_percent": "4.047184", + "lb_minus_one_at_bound": "1.006e-24", + "retained_fraction": "0.660085", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001839708793352244770194", + "windowfree_endpoint": "919854396676122385097/500000000000000000000000", + "windowfree_gain_percent": "6.131308", + "windowfree_unreachable": true + }, + "pessimistic": { + "certified_bound": "446833250997083419891/250000000000000000000000", + "endpoint": "1787333003988333679563/1000000000000000000000000", + "endpoint_decimal": "0.001787333003988333679563", + "gain_percent": "3.109791", + "lb_minus_one_at_bound": "3.062e-24", + "retained_fraction": "0.603125", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.00182280480800609487063", + "windowfree_endpoint": "182280480800609487063/100000000000000000000000", + "windowfree_gain_percent": "5.156131", + "windowfree_unreachable": true + }, + "width7_distribution": [ + [ + 0, + 136 + ], + [ + 2, + 68 + ], + [ + 4, + 0 + ], + [ + 8, + 136 + ], + [ + 7, + 68 + ], + [ + 6, + 0 + ] + ] + }, + "69": { + "idle": { + "2": 359, + "35": 1, + "4": 409, + "42": 84, + "5": 1, + "6": 306, + "7": 459 + }, + "optimistic": { + "certified_bound": "451149683627392912821/250000000000000000000000", + "endpoint": "1804598734509571651283/1000000000000000000000000", + "endpoint_decimal": "0.001804598734509571651283", + "gain_percent": "4.105837", + "lb_minus_one_at_bound": "2.195e-24", + "retained_fraction": "0.659154", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001841401309728277678527", + "windowfree_endpoint": "1841401309728277678527/1000000000000000000000000", + "windowfree_gain_percent": "6.228948", + "windowfree_unreachable": true + }, + "pessimistic": { + "certified_bound": "1788106572520652931281/1000000000000000000000000", + "endpoint": "22351332156508161641/12500000000000000000000", + "endpoint_decimal": "0.00178810657252065293128", + "gain_percent": "3.154418", + "lb_minus_one_at_bound": "4.342e-25", + "retained_fraction": "0.602163", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001824232252072967365576", + "windowfree_endpoint": "228029031509120920697/125000000000000000000000", + "windowfree_gain_percent": "5.238479", + "windowfree_unreachable": true + }, + "width7_distribution": [ + [ + 0, + 138 + ], + [ + 2, + 68 + ], + [ + 4, + 0 + ], + [ + 8, + 138 + ], + [ + 7, + 69 + ], + [ + 6, + 1 + ] + ] + }, + "7": { + "idle": { + "2": 427, + "28": 1, + "4": 441, + "42": 16, + "6": 430, + "7": 645 + }, + "optimistic": { + "certified_bound": "1740267612097359464709/1000000000000000000000000", + "endpoint": "435066903024339866177/250000000000000000000000", + "endpoint_decimal": "0.001740267612097359464708", + "gain_percent": "0.394627", + "lb_minus_one_at_bound": "2.471e-24", + "retained_fraction": "0.662507", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001743752323848821409039", + "windowfree_endpoint": "1743752323848821409039/1000000000000000000000000", + "windowfree_gain_percent": "0.595657", + "windowfree_unreachable": true + }, + "pessimistic": { + "certified_bound": "1358249512153064437/781250000000000000000", + "endpoint": "1738559375555922479359/1000000000000000000000000", + "endpoint_decimal": "0.001738559375555922479359", + "gain_percent": "0.296080", + "lb_minus_one_at_bound": "1.961e-24", + "retained_fraction": "0.596076", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001742037237922629638392", + "windowfree_endpoint": "217754654740328704799/125000000000000000000000", + "windowfree_gain_percent": "0.496715", + "windowfree_unreachable": true + }, + "width7_distribution": [ + [ + 0, + 14 + ], + [ + 2, + 4 + ], + [ + 4, + 0 + ], + [ + 8, + 14 + ], + [ + 7, + 4 + ], + [ + 6, + 6 + ] + ] + }, + "70": { + "idle": { + "2": 358, + "35": 1, + "4": 408, + "42": 85, + "5": 1, + "6": 305, + "7": 456 + }, + "optimistic": { + "certified_bound": "902798984376378105637/500000000000000000000000", + "endpoint": "1805597968752756211273/1000000000000000000000000", + "endpoint_decimal": "0.001805597968752756211273", + "gain_percent": "4.163482", + "lb_minus_one_at_bound": "1.285e-24", + "retained_fraction": "0.657949", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001843117808953168022583", + "windowfree_endpoint": "1843117808953168022583/1000000000000000000000000", + "windowfree_gain_percent": "6.327972", + "windowfree_unreachable": true + }, + "pessimistic": { + "certified_bound": "223607816295482069427/125000000000000000000000", + "endpoint": "357772506072771311083/200000000000000000000000", + "endpoint_decimal": "0.001788862530363856555415", + "gain_percent": "3.198029", + "lb_minus_one_at_bound": "1.147e-25", + "retained_fraction": "0.600892", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001825682405654768870163", + "windowfree_endpoint": "1825682405654768870163/1000000000000000000000000", + "windowfree_gain_percent": "5.322137", + "windowfree_unreachable": true + }, + "width7_distribution": [ + [ + 0, + 140 + ], + [ + 2, + 69 + ], + [ + 4, + 0 + ], + [ + 8, + 138 + ], + [ + 7, + 72 + ], + [ + 6, + 1 + ] + ] + }, + "71": { + "idle": { + "2": 356, + "4": 410, + "42": 87, + "6": 302, + "7": 453 + }, + "optimistic": { + "certified_bound": "1806783613242489729003/1000000000000000000000000", + "endpoint": "903391806621244864501/500000000000000000000000", + "endpoint_decimal": "0.001806783613242489729002", + "gain_percent": "4.231881", + "lb_minus_one_at_bound": "2.832e-25", + "retained_fraction": "0.659116", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001844722376159760278639", + "windowfree_endpoint": "1844722376159760278639/1000000000000000000000000", + "windowfree_gain_percent": "6.420538", + "windowfree_unreachable": true + }, + "pessimistic": { + "certified_bound": "894900480697739166023/500000000000000000000000", + "endpoint": "357960192279095666409/200000000000000000000000", + "endpoint_decimal": "0.001789800961395478332045", + "gain_percent": "3.252166", + "lb_minus_one_at_bound": "3.236e-25", + "retained_fraction": "0.602318", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001827021929234936921771", + "windowfree_endpoint": "1827021929234936921771/1000000000000000000000000", + "windowfree_gain_percent": "5.399413", + "windowfree_unreachable": true + }, + "width7_distribution": [ + [ + 0, + 142 + ], + [ + 2, + 68 + ], + [ + 4, + 0 + ], + [ + 8, + 142 + ], + [ + 7, + 68 + ], + [ + 6, + 6 + ] + ] + }, + "72": { + "idle": { + "14": 1, + "2": 356, + "4": 408, + "42": 88, + "6": 299, + "7": 450 + }, + "optimistic": { + "certified_bound": "361580043231310636587/200000000000000000000000", + "endpoint": "903950108078276591467/500000000000000000000000", + "endpoint_decimal": "0.001807900216156553182934", + "gain_percent": "4.296297", + "lb_minus_one_at_bound": "1.949e-24", + "retained_fraction": "0.659231", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001846396850030219355802", + "windowfree_endpoint": "923198425015109677901/500000000000000000000000", + "windowfree_gain_percent": "6.517137", + "windowfree_unreachable": true + }, + "pessimistic": { + "certified_bound": "447667778903807861131/250000000000000000000000", + "endpoint": "1790671115615231444523/1000000000000000000000000", + "endpoint_decimal": "0.001790671115615231444523", + "gain_percent": "3.302364", + "lb_minus_one_at_bound": "1.534e-24", + "retained_fraction": "0.602555", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001828429229553527797737", + "windowfree_endpoint": "1828429229553527797737/1000000000000000000000000", + "windowfree_gain_percent": "5.480599", + "windowfree_unreachable": true + }, + "width7_distribution": [ + [ + 0, + 144 + ], + [ + 2, + 72 + ], + [ + 4, + 0 + ], + [ + 8, + 144 + ], + [ + 7, + 72 + ], + [ + 6, + 0 + ] + ] + }, + "73": { + "idle": { + "14": 1, + "2": 355, + "4": 406, + "42": 89, + "5": 2, + "6": 297, + "7": 447 + }, + "optimistic": { + "certified_bound": "1808901058959374809869/1000000000000000000000000", + "endpoint": "452225264739843702467/250000000000000000000000", + "endpoint_decimal": "0.001808901058959374809868", + "gain_percent": "4.354035", + "lb_minus_one_at_bound": "6.239e-25", + "retained_fraction": "0.658476", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.00184804634361746113431", + "windowfree_endpoint": "184804634361746113431/100000000000000000000000", + "windowfree_gain_percent": "6.612295", + "windowfree_unreachable": true + }, + "pessimistic": { + "certified_bound": "895713614921645772309/500000000000000000000000", + "endpoint": "1791427229843291544617/1000000000000000000000000", + "endpoint_decimal": "0.001791427229843291544617", + "gain_percent": "3.345984", + "lb_minus_one_at_bound": "2.078e-24", + "retained_fraction": "0.601760", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001829811226721176726863", + "windowfree_endpoint": "1829811226721176726863/1000000000000000000000000", + "windowfree_gain_percent": "5.560326", + "windowfree_unreachable": true + }, + "width7_distribution": [ + [ + 0, + 146 + ], + [ + 2, + 73 + ], + [ + 4, + 0 + ], + [ + 8, + 146 + ], + [ + 7, + 73 + ], + [ + 6, + 0 + ] + ] + }, + "74": { + "idle": { + "14": 1, + "2": 354, + "4": 406, + "42": 90, + "6": 297, + "7": 444 + }, + "optimistic": { + "certified_bound": "904953559530015237129/500000000000000000000000", + "endpoint": "1809907119060030474257/1000000000000000000000000", + "endpoint_decimal": "0.001809907119060030474257", + "gain_percent": "4.412074", + "lb_minus_one_at_bound": "1.428e-24", + "retained_fraction": "0.657457", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.00184975423837042835336", + "windowfree_endpoint": "23121927979630354417/12500000000000000000000", + "windowfree_gain_percent": "6.710822", + "windowfree_unreachable": true + }, + "pessimistic": { + "certified_bound": "56005875337664138131/31250000000000000000000", + "endpoint": "1792188010805252420191/1000000000000000000000000", + "endpoint_decimal": "0.001792188010805252420191", + "gain_percent": "3.389873", + "lb_minus_one_at_bound": "1.355e-24", + "retained_fraction": "0.600689", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001831249661111873873002", + "windowfree_endpoint": "915624830555936936501/500000000000000000000000", + "windowfree_gain_percent": "5.643308", + "windowfree_unreachable": true + }, + "width7_distribution": [ + [ + 0, + 146 + ], + [ + 2, + 76 + ], + [ + 4, + 0 + ], + [ + 8, + 146 + ], + [ + 7, + 76 + ], + [ + 6, + 0 + ] + ] + }, + "8": { + "idle": { + "2": 426, + "34": 1, + "4": 440, + "42": 17, + "6": 428, + "7": 642 + }, + "optimistic": { + "certified_bound": "348269277673726119781/200000000000000000000000", + "endpoint": "217668298546078824863/125000000000000000000000", + "endpoint_decimal": "0.001741346388368630598904", + "gain_percent": "0.456861", + "lb_minus_one_at_bound": "8.495e-25", + "retained_fraction": "0.671333", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001745223486350668740543", + "windowfree_endpoint": "1745223486350668740543/1000000000000000000000000", + "windowfree_gain_percent": "0.680527", + "windowfree_unreachable": true + }, + "pessimistic": { + "certified_bound": "869695985237661013993/500000000000000000000000", + "endpoint": "347878394095064405597/200000000000000000000000", + "endpoint_decimal": "0.001739391970475322027985", + "gain_percent": "0.344112", + "lb_minus_one_at_bound": "2.335e-24", + "retained_fraction": "0.606604", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.00174326035458121563512", + "windowfree_endpoint": "21790754432265195439/12500000000000000000000", + "windowfree_gain_percent": "0.567276", + "windowfree_unreachable": true + }, + "width7_distribution": [ + [ + 0, + 16 + ], + [ + 2, + 8 + ], + [ + 4, + 0 + ], + [ + 8, + 16 + ], + [ + 7, + 8 + ], + [ + 6, + 0 + ] + ] + }, + "9": { + "idle": { + "2": 425, + "35": 1, + "4": 439, + "42": 18, + "5": 1, + "6": 426, + "7": 639 + }, + "optimistic": { + "certified_bound": "217786765685837276261/125000000000000000000000", + "endpoint": "1742294125486698210087/1000000000000000000000000", + "endpoint_decimal": "0.001742294125486698210087", + "gain_percent": "0.511535", + "lb_minus_one_at_bound": "1.449e-24", + "retained_fraction": "0.665720", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001746746587687713680687", + "windowfree_endpoint": "1746746587687713680687/1000000000000000000000000", + "windowfree_gain_percent": "0.768394", + "windowfree_unreachable": true + }, + "pessimistic": { + "certified_bound": "1740093319809604620489/1000000000000000000000000", + "endpoint": "217511664976200577561/125000000000000000000000", + "endpoint_decimal": "0.001740093319809604620488", + "gain_percent": "0.384572", + "lb_minus_one_at_bound": "7.109e-25", + "retained_fraction": "0.600161", + "same_argmin_at_bound": true, + "windowfree_decimal": "0.001744534518556053685783", + "windowfree_endpoint": "1744534518556053685783/1000000000000000000000000", + "windowfree_gain_percent": "0.640781", + "windowfree_unreachable": true + }, + "width7_distribution": [ + [ + 0, + 18 + ], + [ + 2, + 8 + ], + [ + 4, + 0 + ], + [ + 8, + 18 + ], + [ + 7, + 9 + ], + [ + 6, + 1 + ] + ] + } + }, + "status": "PASS_BIT589_WIDTH7_WINDOWS", + "windows": { + "0": { + "capacity": 14, + "stages": [ + 0, + 1 + ] + }, + "1": { + "capacity": 7, + "stages": [ + 2 + ] + }, + "2": { + "capacity": 28, + "stages": [ + 0, + 1, + 2, + 3 + ] + }, + "3": { + "capacity": 7, + "stages": [ + 4 + ] + }, + "4": { + "capacity": 42, + "stages": [ + 0, + 1, + 2, + 3, + 4, + 5 + ] + }, + "5": { + "capacity": 7, + "stages": [ + 6 + ] + }, + "6": { + "capacity": 42, + "stages": [ + 3, + 4, + 5, + 6, + 7, + 8 + ] + }, + "7": { + "capacity": 28, + "stages": [ + 5, + 6, + 7, + 8 + ] + }, + "8": { + "capacity": 14, + "stages": [ + 7, + 8 + ] + } + } +} diff --git a/research/bit589-width7-windows-seed72/SOURCES.json b/research/bit589-width7-windows-seed72/SOURCES.json new file mode 100644 index 0000000000..1cdc6c9918 --- /dev/null +++ b/research/bit589-width7-windows-seed72/SOURCES.json @@ -0,0 +1,96 @@ +{ + "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": "research/bit-partial-width7-optimum/EXPECTED.json", + "usage": "input", + "git_blob": "b118ea87a6e9ec6805b27f847b9ae7d12ecbdc8a", + "sha256": "a6ec64866b949626d6508ee7172b144c3fd29f1065822b523fafd7d2a59e2e91" + }, + { + "path": "research/bit589-width-packing/RESULT.json", + "usage": "input", + "git_blob": "f11f6e569cd6d780946548c9bd3bc10d65ed6ab9", + "sha256": "200b91e2d801c789426835b640381b7d0a4bae5e67c3859cbd97b52dc7053b09" + }, + { + "path": "research/bit589-width-packing/SOURCES.json", + "usage": "input", + "git_blob": "f6a97de32691a1d426ac4819aad24c0c8414d97e", + "sha256": "53fe98c8f01de7e32e3110e591d62e60292abb38cc11ecde4839f2eebd3b5fbc" + }, + { + "path": "research/bit589-width-packing/packing.py", + "usage": "input", + "git_blob": "a6079ee0dd4d8037be477a3c4497f472348bde07", + "sha256": "2bb5515807714807961289e4ee6958c3ad7e0c27bbec4d9212b138c662a6cc7b" + }, + { + "path": "research/community-frontier1094-audit/ASSEMBLY.json", + "usage": "input", + "git_blob": "5fd676df060f3b450782fdf5ff5f6beb63a5eeb0", + "sha256": "1122cb3a575f8c788345fc1bf4c108ac7c3250fb81a5988671f5eb04b3ab3045" + }, + { + "path": "research/e8-bit-p111-tuned/data/selection9-p111.json", + "usage": "input", + "git_blob": "e69ea66a3add357f570fc5552ab6368b3c8f9bb2", + "sha256": "4ab1ed4529683cd184987f8bc3031fb7408b9cd22c25ab9cf541a8aaf896eaf1" + }, + { + "path": "research/e8-bit-p111-tuned/tune/EXPECTED.json", + "usage": "input", + "git_blob": "e293ddc557742637f9f679f083a1a282d87b1b13", + "sha256": "b9f0e5ca038abe837b0007c8fe006f366a6f02009244ac57705a8a200e2301f4" + }, + { + "path": "research/e8-bit-p111-tuned/vendor/pr510/e8-r480-nine-stage/vendor/e8-r715-eleven-stage-whole/code/audit_hosted_k.py", + "usage": "input", + "git_blob": "8864ca9b942a3507171edca0cf6cbaaf10fcf434", + "sha256": "57e558c80a2fea6e291587b04afd76dfaee3550729997798b61f33daf90b8ec9" + }, + { + "path": "research/e8-bit-p111-tuned/vendor/pr510/e8-r480-nine-stage/vendor/e8-r715-eleven-stage-whole/code/global_k.py", + "usage": "provenance", + "git_blob": "3df12bd632f1fdba825ced57110a1fee82eb2857", + "sha256": "6368196a393ac25bb2918880e4c4bd31ed733b762c27b6873ab391cbc0c5c3c8" + }, + { + "path": "research/e8-bit-p111-tuned/vendor/pr510/e8-r480-nine-stage/vendor/idle-axis-hosting/hosting_core.py", + "usage": "input", + "git_blob": "68b536daa9e6546c0aa046934bf840aaa3c3fde3", + "sha256": "d8b90cd5d152df3c7c351230863d9e61816ad5e1f21d69bea1a86a5daad559a3" + }, + { + "path": "research/native-complex-moment552/engines/base_two_moment.py", + "usage": "input", + "git_blob": "14a90fa0e788217856f070382c9e61bd7c603c61", + "sha256": "aee70c242a2f1d225528fabe2002e1564d1dc884797c07d28a831c7878ee9098" + }, + { + "path": "research/native-complex-moment552/engines/moment.py", + "usage": "input", + "git_blob": "7d697cb45203fe72d97037403d6da41f71f3b7fd", + "sha256": "81cbc864e106418fc7854322746f72180cb8110ff39f74450a3b8d55a82c1482" + }, + { + "path": "research/native-complex-moment552/engines/outer.py", + "usage": "input", + "git_blob": "43007488ad2c43187c77cc6798beff8b1cd76ad2", + "sha256": "c1ebb52163a7219504c728a5c2b098bf1e50bf20148a2879c5a74c3cadc7c03c" + } + ] +} diff --git a/research/bit589-width7-windows-seed72/TASK.json b/research/bit589-width7-windows-seed72/TASK.json new file mode 100644 index 0000000000..def1366f6b --- /dev/null +++ b/research/bit589-width7-windows-seed72/TASK.json @@ -0,0 +1,72 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 3, + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Can one exact all-size/compiler, precision, hosting or restoration implication be proved or falsified?", + "starting_points": [ + "certificates/selected-result.json", + "docs/audit.md" + ], + "methods": [ + "Prove one missing implication with explicit quantified hypotheses.", + "Find an exact counterexample at the claimed interface boundary." + ], + "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read the selected review scope and choose one exact all-size or precision implication.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Write its quantified inputs and conclusion; find a missing hypothesis or construct a minimal exact adversarial instance.", + "bottleneck_link": "Finite supplier improvements are useful only under the retained transfer obligations.", + "allowed_variations": [ + "Choose one tape, precision, hosting or restoration lemma." + ], + "scope_change_triggers": [ + "Replacing a quantified obligation with another finite smoke test." + ], + "overlap_terms": [ + "uniform transfer", + "all-size", + "precision" + ] + }, + "scope_status": "refined", + "actual_scope": "One hosting implication for the selected PR589 bit supplier: do the window-free partial width-seven rows of merged #1023 and merged #1281 (width-7 residuals placed in capacity-7 idle slots without time order) survive PR442's replica-local hosting windows (audit_hosted_k: s in W[i] for every hosted slot) on the nine-stage template? Exact window-respecting optimum and certificate for every k = 0..74.", + "scope_change_reason": "The card asks for one exact hosting implication; this narrows it to the time-order hypothesis that #1023 lists as unchecked and that #1281 states as its open question 1. Replica-local hosting only; cross-replica owner maps, projector compatibility, owner inactivity and a physical width-7 helper stay open.", + "bottleneck_link": "Side result on the bit supplier; the selected record is complex-bound, so no kappa changes. It corrects the bit headroom any partial width-seven helper mechanism can buy under replica-local hosting: about two thirds of the window-free gain, so the published rows overstate it by about 1.5x.", + "budget_minutes": 180, + "stop_rule": "Stop once every k = 0..74 has an explicit window-feasible placement and a tight grid certificate under both local brackets, k = 0 reproduces the selected bit endpoint, and every #1023 and #1281 row is compared; report any row not decided instead of claiming it.", + "outcome": "completed", + "evidence": "RESULT.json: windows equal in three implementations (own, PR442 hosting_core, audit_hosted_k), frozen selection inside them; capacity-7 children 1/3/5 admit only stages 2/4/6, so at most 3k of 9k width-7 residuals per replica sit in 7-slots. Exact window-respecting optimum with explicit placement and tight 1e-24 certificate for every k = 0..74, both brackets; k = 0 reproduces 0.001733427039589844234749. k = 37 optimistic 0.001770809187 (+2.157%) vs window-free 0.001789671631 (+3.245%); k = 74 0.001809907119 (+4.412%) vs 0.001849754238 (+6.711%). Retained fraction 0.636-0.671 (optimistic), 0.563-0.607 (pessimistic). All 8 #1023 partial rows and all 148 #1281 local rows unreachable; #1281's 75 idle optima and 9 priced cases reproduced exactly from its merged EXPECTED.json; its pooled32 rows above the per-replica bound. #1023's all-width-7 optimum stays window-feasible (104 sextet splits). 11 tests pass.", + "author": "Sagar Thakrar (thakrarsagar)", + "ai_assistance": "Substantial: Claude (Anthropic) via Claude Code. Parallel read-only scout and judge subagents proposed and ranked audit candidates and found the window obstruction; the DP, placement builder and certificates were written with Claude and checked by the controls in test_package.py.", + "open_questions": [ + { + "question": "Can cross-replica (T16-style) interleaved owner maps lift the one-stage capacity-7 windows for the bit supplier?", + "why_it_matters": "Only then could #1281's pooled rows, or the window-free local rows, be reached; replica-local hosting is ruled out here.", + "first_step": "Compute windows on an interleaved bit timeline with owner_replica != replica and rerun wopt.solve.", + "blocked_by": "An interleaved bit timeline; the selected T16 maps are complex-side." + }, + { + "question": "Does another nine-stage stage recipe widen the capacity-7 windows?", + "why_it_matters": "The obstruction is recipe-specific; open #1487 enumerates recipes for width-8 hosting only.", + "first_step": "Feed each of #1487's recipes to windows.windows and rerun wopt.solve at k = 1 and k = 37.", + "blocked_by": "None." + }, + { + "question": "Do the window-respecting placements pass projector compatibility (#1307) for mixed-width slots?", + "why_it_matters": "Windows are necessary, not sufficient; slots that split q-perp lie outside #1307's completion-free argument.", + "first_step": "Run #1307's projector check on the k = 1 explicit placement.", + "blocked_by": "None." + } + ] +} diff --git a/research/bit589-width7-windows-seed72/VERIFY.json b/research/bit589-width7-windows-seed72/VERIFY.json new file mode 100644 index 0000000000..e182b3bd6c --- /dev/null +++ b/research/bit589-width7-windows-seed72/VERIFY.json @@ -0,0 +1,48 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/bit-partial-width7-optimum/EXPECTED.json", + "research/bit589-width-packing/RESULT.json", + "research/bit589-width-packing/SOURCES.json", + "research/bit589-width-packing/packing.py", + "research/community-frontier1094-audit/ASSEMBLY.json", + "research/e8-bit-p111-tuned/data/selection9-p111.json", + "research/e8-bit-p111-tuned/tune/EXPECTED.json", + "research/e8-bit-p111-tuned/vendor/pr510/e8-r480-nine-stage/vendor/e8-r715-eleven-stage-whole/code/audit_hosted_k.py", + "research/e8-bit-p111-tuned/vendor/pr510/e8-r480-nine-stage/vendor/idle-axis-hosting/hosting_core.py", + "research/native-complex-moment552/engines/base_two_moment.py", + "research/native-complex-moment552/engines/moment.py", + "research/native-complex-moment552/engines/outer.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 600, + "checks": "Binds selected record -> frontier1094 ASSEMBLY -> the PR589 record and engines pinned by #1023's packing.py; rebuilds the nine-stage idle schedule and windows, equal to PR442 hosting_core.windows and audit_hosted_k.windows, frozen selection inside its windows; capacity-7 children admit one stage each; chain reduction by brute force (k = 1, 2); for every k = 0..74 the DP optimum, an explicit residual-level placement attaining it (window, width, offset, disjoint cells, hosted once), both local brackets priced with the pinned engines, a 1e-24 grid certificate tight to 1e-50 against the explicit histogram; #1023's eight partial rows and merged #1281's EXPECTED.json (75 idle optima, 9 priced cases with exact endpoints and histograms; local and pooled32 rows above the bound); #1023's all-width-7 optimum window-feasible; RESULT.json byte-identical." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "-m", + "unittest", + "discover", + "-s", + "{package}", + "-p", + "test_package.py" + ], + "timeout_seconds": 300, + "checks": "Capacity-7 windows, #1023's k = 1 placement outside its windows, k = 0 reproduction, window-free rows above and window-respecting rows below the bound, #1281 local and pooled rows, all-width-7 feasibility, brute-force reduction, dropped chain constraint and perturbed window controls, width-8 Hall vacuity." + } + ] +} diff --git a/research/bit589-width7-windows-seed72/test_package.py b/research/bit589-width7-windows-seed72/test_package.py new file mode 100644 index 0000000000..ca85e2d97d --- /dev/null +++ b/research/bit589-width7-windows-seed72/test_package.py @@ -0,0 +1,111 @@ +# SPDX-License-Identifier: Apache-2.0 +"""Controls for the width-7 window audit (about 15 s). + +Run: python3 -I -B -m unittest discover -s research/bit589-width7-windows-seed72 -p test_package.py -v +""" +import copy +import itertools +import json +import sys +import unittest +from collections import Counter +from fractions import Fraction as Q +from pathlib import Path + +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE)) +import verify as V # noqa: E402 +import windows # noqa: E402 +import wopt # noqa: E402 + +RESULT = json.loads((HERE / 'RESULT.json').read_text()) + + +class Windows(unittest.TestCase): + def test_capacity7_children_admit_one_stage_each(self): + ah = windows._load('audit_hosted_k', windows.AUDIT_HOSTED) + W, rank, _ = ah.windows(windows.schedule()) + sevens = {i: sorted(W[i]) for i in W if rank[i] == 7 and W[i]} + self.assertEqual(sevens, {1: [2], 3: [4], 5: [6]}) + + def test_cw1_window_free_k1_uses_nine_seven_slots(self): + # #1023's partial placement (packing.width7_partial_idle) fills 9 capacity-7 copies per replica + # with one width-7 residual from each of the 9 stages; the vendored windows admit only stages + # 2, 4 and 6 there, so at least 6 of the 9 residuals sit outside their window. + model = wopt.P.slot_model(wopt.P.pinned_json('bit_record'), wopt.P.pinned_json('selection')) + idle = wopt.P.width7_partial_idle(model, 1) + self.assertEqual(Counter(model['idle_rep'])[7] - idle[7], 9) + admitted = {s for i in wopt.SEVEN for s in wopt.WIN[i][1]} + self.assertEqual(len(set(range(9)) - admitted), 6) + + +class Certificates(unittest.TestCase): + def test_k0_reproduces_the_selected_endpoint_and_is_tight(self): + row = RESULT['rows']['0']['optimistic'] + self.assertEqual(Q(row['endpoint']), Q(wopt.P.pinned_json('bit_record')['nine']['bit_lower'])) + self.assertTrue(row['same_argmin_at_bound']) + + def test_cw2_window_free_local_rows_exceed_the_bound(self): + for k in ('1', '2', '10', '37', '74'): + for b in ('optimistic', 'pessimistic'): + r = RESULT['rows'][k][b] + self.assertGreaterEqual(Q(r['windowfree_endpoint']), Q(r['certified_bound'])) + self.assertLess(Q(r['endpoint']), Q(r['certified_bound'])) + + def test_cw3_pr1281_local_and_pooled_rows_exceed_the_per_replica_bound(self): + priced = RESULT['pr1281']['priced_cases'] + self.assertEqual(len(priced), 9) + for key, row in priced.items(): + if key != 'k0_optimistic': + self.assertTrue(row['unreachable'], key) + self.assertEqual(RESULT['pr1281']['idle_optima_matched'], 75) + + def test_pr1023_partial_rows_all_unreachable(self): + rows = RESULT['pr1023_partial_rows'] + self.assertEqual(len(rows), 8) + self.assertTrue(all(r['unreachable'] for r in rows.values())) + + def test_cw4_all_width7_optimum_is_window_feasible(self): + lo, hi, n = RESULT['all_width7']['feasible_sextet_splits'] + self.assertGreater(n, 0) + x4 = lo + cps = {i: ([wopt.CAP[i] // 7] * wopt.N if wopt.CAP[i] in (7, 14, 28) else []) for i in wopt.WIN} + cps[4] = [6] * x4 + cps[6] = [6] * (103 - x4) + [3] + x = V.maxflow_assign({s: wopt.R for s in range(9)}, {i: sum(cps[i]) for i in wopt.WIN}, + {i: set(wopt.WIN[i][1]) for i in wopt.WIN}) + self.assertIsNotNone(x) + + +class Reduction(unittest.TestCase): + def test_brute_force_matches_the_chains(self): + n, agree = V.brute_force_reduction(2) + self.assertEqual(n, agree) + + def test_cw5_dropping_a_chain_constraint_breaks_agreement(self): + original = V.chain_ok + try: + V.chain_ok = lambda B, k: (B[0] + B[2] <= 3 * k and B[0] + B[2] + B[4] <= 4 * k and B[8] <= 2 * k + and B[8] + B[7] <= 3 * k and B[8] + B[7] + B[6] <= 4 * k + and B[0] + B[2] + B[4] + B[8] + B[7] + B[6] == 6 * k) # B0 <= 2k dropped + n, agree = V.brute_force_reduction(1) + self.assertLess(agree, n) + finally: + V.chain_ok = original + + def test_cw5_a_perturbed_window_changes_the_structure(self): + saved = dict(wopt.WIN) + try: + wopt.WIN[0] = (14, (0, 1, 2, 3)) # child 0 would also admit stages 2 and 3 + with self.assertRaises(AssertionError): + wopt.check_chain_reduction(1) + finally: + wopt.WIN.clear() + wopt.WIN.update(saved) + + def test_hall_width8_conditions_are_vacuous_in_range(self): + self.assertTrue(all(V.w8_vacuous(k) for k in (0, 1, 37, 74))) + + +if __name__ == '__main__': + unittest.main() diff --git a/research/bit589-width7-windows-seed72/verify.py b/research/bit589-width7-windows-seed72/verify.py new file mode 100644 index 0000000000..6a62a9ee8a --- /dev/null +++ b/research/bit589-width7-windows-seed72/verify.py @@ -0,0 +1,353 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Audit: PR442 hosting windows and the partial width-seven rows of #1023 and #1281 (no new kappa). + +Usage: python3 -I -B research/bit589-width7-windows-seed72/verify.py [--write] [--kmax K] + +0. Binds the selected record -> frontier1094 ASSEMBLY -> the PR589 record and engines pinned by #1023's packing.py. +1. Rebuilds the nine-stage idle schedule and its hosting windows, cross-checked against both vendored + predicates and the frozen PR589 selection (windows.py). Capacity-7 children admit one stage each. +2. Checks the interval Hall reduction to two nested chains by brute force for k = 1, 2. +3. For every k = 0..74 converted helpers per call: the exact window-respecting optimum (DP lower bound), + an explicit residual-level placement attaining it (window, width, offset, disjoint cells, every + (stage, helper) hosted once), its bit endpoint under both of #1023's local brackets with the pinned + engines, a certificate that no window-feasible placement reaches the next 1e-24 grid point, and a + tightness check against the engine moment of the explicit histogram. +4. Compares with the window-free rows: #1023's eight partial rows (its RESULT.json) and merged #1281's + EXPECTED.json (digest-pinned): its local idle optimum for every k, and its nine priced cases + (local endpoints and histograms reproduced exactly; local and pooled32 endpoints above the bound). +5. Checks that #1023's all-width-7 optimum {42:340, 21:1} is window-feasible. +Expected last line: PASS_BIT589_WIDTH7_WINDOWS +""" +import argparse +import itertools +import json +import sys +from collections import Counter, deque +from fractions import Fraction as Q +from pathlib import Path + +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE)) +import wopt # noqa: E402 +from wopt import CAP, M, N, P, R, REST, SEVEN, SHIFT, STG, T, WIN # noqa: E402 + +PR1281 = dict(merged='e4a7f61f168837f628a1d8b54aa5cff0680f9a38', path='research/bit-partial-width7-optimum/EXPECTED.json', + sha256='a6ec64866b949626d6508ee7172b144c3fd29f1065822b523fafd7d2a59e2e91') + + +RECORDS = ('certificates/selected-result.json', 'certificates/checkpoints/frontier1094.json') +ASSEMBLY = 'research/community-frontier1094-audit/ASSEMBLY.json' + + +def bind(): + """Selected record -> frontier1094 ASSEMBLY -> the PR589 record and engines that #1023's packing.py pins.""" + raw = (P.ROOT / ASSEMBLY).read_bytes() + bound = None + for path in RECORDS: + f = P.ROOT / path + rec = json.loads(f.read_text()) if f.is_file() else {} + if rec.get('certificate') == ASSEMBLY and rec.get('certificate_sha256') == P.sha256(raw): + bound = path + break + need(bound is not None, 'a record binds the frontier1094 certificate') + asm = json.loads(raw) + need(asm['input_sha256']['package:inputs/PR589-EXPECTED.json'] == P.SOURCES['inputs']['bit_record']['sha256'], + 'the certificate pins the PR589 record that packing.py reads') + for name in ('moment.py', 'base_two_moment.py', 'outer.py'): + need(asm['input_sha256']['engines/' + name] == P.SOURCES['engines'][name], 'the certificate pins engine ' + name) + need(Q(asm['bit_lower']) == Q(P.pinned_json('bit_record')['nine']['bit_lower']), 'certificate bit endpoint = PR589 record') + return dict(record=bound, assembly=ASSEMBLY, assembly_sha256=P.sha256(raw), bit_lower=asm['bit_lower']) + + +def need(ok, label): + if not ok: + raise SystemExit('FAIL ' + label) + + +def maxflow_assign(supply, demand, allowed): + """Transportation by augmenting paths: x[(stage, child)] or None if infeasible.""" + src, snk = 'S', 'T' + cap, adj = {}, {} + + def add(u, v, c): + cap[(u, v)] = cap.get((u, v), 0) + c + cap.setdefault((v, u), 0) + adj.setdefault(u, set()).add(v) + adj.setdefault(v, set()).add(u) + for s, n in supply.items(): + if n: + add(src, ('s', s), n) + for i, n in demand.items(): + if n: + add(('c', i), snk, n) + for s in allowed[i]: + if supply.get(s, 0): + add(('s', s), ('c', i), 10 ** 9) + flow = 0 + while True: + par, dq = {src: None}, deque([src]) + while dq and snk not in par: + u = dq.popleft() + for v in sorted(adj.get(u, ()), key=str): + if v not in par and cap[(u, v)] > 0: + par[v] = u + dq.append(v) + if snk not in par: + break + b, v = None, snk + while par[v] is not None: + u = par[v] + b = cap[(u, v)] if b is None else min(b, cap[(u, v)]) + v = u + v = snk + while par[v] is not None: + u = par[v] + cap[(u, v)] -= b + cap[(v, u)] += b + v = u + flow += b + if flow != sum(supply.values()) or flow != sum(demand.values()): + return None + return {(s, i): cap[(('c', i), ('s', s))] for i in demand for s in allowed[i] + if (('c', i), ('s', s)) in cap and cap[(('c', i), ('s', s))]} + + +def w8_vacuous(k): + for lo in range(STG): + for hi in range(lo, STG): + if (lo, hi) == (0, STG - 1): + continue + J = set(range(lo, hi + 1)) + if sum(N * (CAP[i] // 8) for i in WIN if set(WIN[i][1]) <= J) > (R - k) * len(J): + return False + return True + + +def chain_ok(B, k): + """The two nested chains (children 0,2,4 and 8,7,6) and the total, as derived in README.""" + L0, L1, L2 = B[0], B[0] + B[2], B[0] + B[2] + B[4] + R0, R1, R2 = B[8], B[8] + B[7], B[8] + B[7] + B[6] + return L0 <= 2 * k and L1 <= 3 * k and L2 <= 4 * k and R0 <= 2 * k and R1 <= 3 * k and R2 <= 4 * k and L2 + R2 == 6 * k + + +def brute_force_reduction(k): + """Every distribution of the 6k non-7-slot width-7 residuals over children 0,2,4,6,7,8: window + transport feasibility (max-flow) must equal the chain predicate.""" + supply = {s: (0 if s in (2, 4, 6) else k) for s in range(STG)} + count = agree = 0 + for parts in itertools.product(range(4 * k + 1), repeat=5): + last = 6 * k - sum(parts) + if last < 0: + continue + B = dict(zip(REST, list(parts) + [last])) + feasible = maxflow_assign(supply, {i: B[i] for i in REST}, {i: set(WIN[i][1]) for i in REST}) is not None + count += 1 + agree += feasible == chain_ok(B, k) + return count, agree + + +def build(k, plan): + """Explicit per-replica hosting from the DP plan, verified in the audit_hosted_k style.""" + copies = {i: [] for i in WIN} + for i in WIN: + for (l, b, r) in plan['copies'][i]: + copies[i].append([CAP[i] // 8 - l, b]) + for c, l in plan['pure8']: + opts = [i for i in WIN if CAP[i] == c and len(copies[i]) < N] + need(bool(opts), 'free copy of capacity %d' % c) + copies[opts[0]].append([c // 8 - l, 0]) + for i in WIN: + need(len(copies[i]) <= N, 'copy count') + copies[i] += [[CAP[i] // 8, 0] for _ in range(N - len(copies[i]))] + out = {} + for w, per_stage in ((7, k), (8, R - k)): + dem = {i: sum(cp[0 if w == 8 else 1] for cp in copies[i]) for i in WIN} + x = maxflow_assign({s: per_stage for s in range(STG)}, dem, {i: set(WIN[i][1]) for i in WIN}) + need(x is not None, 'stage transport k=%d width %d' % (k, w)) + out[w] = x + pool = {(s, w): deque(range(0, k) if w == 7 else range(k, R)) for s in range(STG) for w in (7, 8)} + slots = [] + for i in WIN: + want = {w: deque() for w in (7, 8)} + for w in (7, 8): + for (s, j), n in sorted(out[w].items()): + if j == i: + want[w].extend([s] * n) + for cp, (a8, b7) in enumerate(copies[i]): + off = 0 + for w, n in ((8, a8), (7, b7)): + for _ in range(n): + s = want[w].popleft() + slots.append((i, cp, off, w, s, pool[(s, w)].popleft())) + off += w + need(not want[7] and not want[8], 'every residual placed') + used, hosted, rem = {}, set(), Counter() + for i, cp, off, w, s, h in slots: + need(s in WIN[i][1], 'slot inside its window') + need(w == (7 if h < k else 8), 'residual width') + need(0 <= off and off + w <= CAP[i], 'slot within capacity') + cells = set(range(off, off + w)) + need(not cells & used.get((i, cp), set()), 'disjoint cells') + used.setdefault((i, cp), set()).update(cells) + need((s, h) not in hosted, 'hosted once') + hosted.add((s, h)) + need(hosted == {(s, h) for s in range(STG) for h in range(R)}, 'every (stage, helper) hosted') + for i in WIN: + for cp in range(N): + r = CAP[i] - len(used.get((i, cp), ())) + if r: + rem[r] += 1 + return +rem + + +def windowfree_idle(k): + """#1281's replica-local optimum without windows (every width-7 role in a 7-slot; S = 45 + 9k = 5q + t).""" + S = 45 + 9 * k + q, t = divmod(S, 5) + idle = Counter({7: 666 - 9 * k, 6: 444, 4: 444, 2: 444}) + idle[2] -= q + idle[42] += q + part = {1: (14, 6, 14), 2: (28, 4, 20), 3: (28, 4, 28), 4: (42, 2, 34)} + if t: + _, old, new = part[t] + idle[old] -= 1 + idle[new] += 1 + return +idle + + +def main(): + ap = argparse.ArgumentParser(description=__doc__.split('\n\n')[0]) + ap.add_argument('--write', action='store_true') + ap.add_argument('--kmax', type=int, default=74) + a = ap.parse_args() + binding = bind() + record = P.pinned_json('bit_record') + selection = P.pinned_json('selection') + model = P.slot_model(record, selection) + W = record['nine']['bit']['live'] + calls = model['calls'] + need(model['caps'] == {i: CAP[i] for i in CAP}, 'slot model = idle children with the same capacities') + c0 = Q(record['nine']['bit_lower']) + out = dict(binding=binding, windows={str(i): dict(capacity=c, stages=list(st)) for i, (c, st) in WIN.items()}, + capacity7_children={str(i): list(WIN[i][1]) for i in SEVEN}) + need(all(len(WIN[i][1]) == 1 for i in SEVEN), 'each capacity-7 child admits exactly one stage') + + # Hall reduction, brute force + bf = {} + for k in (1, 2): + n, agree = brute_force_reduction(k) + need(n == agree, 'chain reduction brute force k=%d' % k) + bf[str(k)] = n + out['chain_reduction_brute_force'] = dict(distributions_checked=bf, agree='all') + + def price(local, idle): + H = Counter({r: n * calls for r, n in local.items()}) + H.update({r: n * T for r, n in idle.items()}) + H = +H + need(sum(r * n for r, n in H.items()) == sum(r * n for r, n in model['H'].items()), 'rank mass') + return P.endpoint(dict(H), W), H + + def lower_bound(k, local, at): + """Moment lower bound at `at` over every window-feasible placement, and the DP argmin there.""" + tot5, _, plan, _ = wopt.solve(k, at, True) + lo_local, _ = P.MOMENT.moment(dict(Counter({r: n * calls for r, n in local.items()})), M, W, at, True) + return lo_local + Q(T * tot5, 5 * SHIFT * M * W), plan + + rows, windowfree_H = {}, {} + for k in range(0, a.kmax + 1): + need(w8_vacuous(k), 'width-8 Hall conditions vacuous k=%d' % k) + tot5, best, plan, F = wopt.solve(k, Q(1, 570), True) + idle = build(k, plan) + need(5 * sum(F[r] * n for r, n in idle.items()) == tot5, 'DP value attained by the explicit placement k=%d' % k) + opt, pes = P.local_bracket(model['local'], k) + row = dict(idle=dict(sorted((str(r), n) for r, n in idle.items())), width7_distribution=[[i, B] for i, B, _ in best[1]]) + for name, local in (('optimistic', opt), ('pessimistic', pes)): + c, H = price(local, idle) + cwf, Hwf = price(local, windowfree_idle(k)) + windowfree_H[(k, name)] = Hwf + nxt = c + Q(1, 10 ** 24) + lb, plan_n = lower_bound(k, local, nxt) + need(lb > 1, 'certificate k=%d %s' % (k, name)) + lo_full, _ = P.MOMENT.moment(dict(H), M, W, nxt, True) + need(abs(lb - lo_full) < Q(1, 10 ** 50), 'tight certificate k=%d %s' % (k, name)) + row[name] = dict(endpoint=str(c), endpoint_decimal=P.dec(c, 22), certified_bound=str(nxt), + lb_minus_one_at_bound='%.3e' % float(lb - 1), same_argmin_at_bound=build(k, plan_n) == idle, + windowfree_endpoint=str(cwf), windowfree_decimal=P.dec(cwf, 22), + gain_percent='%.6f' % float(100 * (c - c0) / c0), + windowfree_gain_percent='%.6f' % float(100 * (cwf - c0) / c0), + retained_fraction=None if k == 0 else '%.6f' % float((c - c0) / (cwf - c0)), + windowfree_unreachable=k == 0 or cwf >= nxt) + if k == 0: + need(c == c0, 'k = 0 reproduces the selected bit endpoint') + rows[str(k)] = row + out['rows'] = rows + + # #1023 (merged): its eight partial rows against the certified bounds + rec1023 = json.loads((P.ROOT / 'research/bit589-width-packing/RESULT.json').read_text())['scenarios'] + unreach = {} + for k in (1, 10, 37, 74): + if str(k) not in rows: + continue + for name in ('optimistic', 'pessimistic'): + v = Q(rec1023['width7_k%d_%s' % (k, name)]['bit_lower']) + unreach['k%d_%s' % (k, name)] = dict(pr1023=P.dec(v, 22), certified_bound=rows[str(k)][name]['certified_bound'], + unreachable=v >= Q(rows[str(k)][name]['certified_bound'])) + need(all(x['unreachable'] for x in unreach.values()), '#1023 partial rows unreachable under windows') + out['pr1023_partial_rows'] = unreach + # #1281 (merged): its EXPECTED.json, digest-pinned, read as data (no #1281 code is run) + raw = (P.ROOT / PR1281['path']).read_bytes() + need(P.sha256(raw) == PR1281['sha256'], '#1281 EXPECTED.json digest') + e1281 = json.loads(raw) + need(e1281['status'] == 'PASS_BIT_PARTIAL_WIDTH7_OPTIMUM' and len(e1281['cases']) == 75, '#1281 EXPECTED.json shape') + for case in e1281['cases']: + if case['k'] <= a.kmax: + need(Counter({int(r): n for r, n in case['idle'].items()}) == windowfree_idle(case['k']), '#1281 local idle optimum k=%d' % case['k']) + priced = {} + for key, case in sorted(e1281['priced_cases'].items()): + k, name = int(key[1:key.index('_')]), key[key.index('_') + 1:] + if k > a.kmax: + continue + r = rows[str(k)][name] + need(Q(case['optimal']['lower']) == Q(r['windowfree_endpoint']), '#1281 %s local endpoint reproduced' % key) + need(Counter({int(x): n for x, n in case['histogram'].items()}) == windowfree_H[(k, name)], '#1281 %s histogram' % key) + bound = Q(r['certified_bound']) + priced[key] = dict(local=P.dec(Q(case['optimal']['lower']), 22), pooled32=P.dec(Q(case['pooled32']['lower']), 22), + certified_bound=r['certified_bound'], + unreachable=k > 0 and Q(case['optimal']['lower']) >= bound and Q(case['pooled32']['lower']) >= bound) + need(all(v['unreachable'] for key, v in priced.items() if not key.startswith('k0_')), '#1281 priced rows unreachable under windows') + local_unreach = sum(rows[str(k)][b]['windowfree_unreachable'] for k in range(1, a.kmax + 1) for b in ('optimistic', 'pessimistic')) + need(local_unreach == 2 * a.kmax, '#1281 local rows unreachable under windows') + out['pr1281'] = dict(PR1281, idle_optima_matched=sum(c['k'] <= a.kmax for c in e1281['cases']), priced_cases=priced, + local_rows_unreachable='%d of %d (both brackets, k = 1..%d)' % (local_unreach, 2 * a.kmax, a.kmax)) + + # #1023's all-width-7 optimum stays window-feasible + feasible = [] + for x4 in range(104): + cps = {i: ([CAP[i] // 7] * N if CAP[i] in (7, 14, 28) else []) for i in WIN} + cps[4] = [6] * x4 + cps[6] = [6] * (103 - x4) + [3] + if len(cps[4]) > N or len(cps[6]) > N: + continue + if maxflow_assign({s: R for s in range(STG)}, {i: sum(cps[i]) for i in WIN}, {i: set(WIN[i][1]) for i in WIN}) is not None: + feasible.append(x4) + need(bool(feasible), 'all-width-7 optimum window-feasible') + out['all_width7'] = dict(idle_per_replica={'42': 340, '21': 1}, feasible_sextet_splits=[min(feasible), max(feasible), len(feasible)]) + + text = json.dumps(dict(status='PASS_BIT589_WIDTH7_WINDOWS', **out), indent=1, sort_keys=True) + '\n' + target = HERE / 'RESULT.json' + if a.write: + target.write_text(text) + elif a.kmax == 74: + need(text == target.read_text(), 'RESULT.json reproduced byte for byte') + for k in (1, 2, 10, 37, 74): + if str(k) in rows: + r = rows[str(k)]['optimistic'] + print('k=%2d window-respecting %s (+%s%%) window-free %s (+%s%%) retained %s' % ( + k, r['endpoint_decimal'][:14], r['gain_percent'][:6], r['windowfree_decimal'][:14], + r['windowfree_gain_percent'][:6], r['retained_fraction'])) + print('PASS_BIT589_WIDTH7_WINDOWS' if a.kmax == 74 else 'PASS_PARTIAL kmax=%d' % a.kmax) + + +if __name__ == '__main__': + main() diff --git a/research/bit589-width7-windows-seed72/windows.py b/research/bit589-width7-windows-seed72/windows.py new file mode 100644 index 0000000000..9d957615cd --- /dev/null +++ b/research/bit589-width7-windows-seed72/windows.py @@ -0,0 +1,95 @@ +# SPDX-License-Identifier: Apache-2.0 +"""The PR442/PR463 hosting windows of the nine-stage PR589 bit template, rebuilt independently. + +The idle schedule follows global_k.py's recipe (K = 4 bank pairs, L = 9 stages): a local cover sweep +per stage, the idle children it inserts, and the bridges. A child's window is the set of stages whose +sweep falls strictly after the child's pair was last touched and before the child is inserted, on +another pair. The result is cross-checked against BOTH vendored predicates (PR442 +hosting_core.windows and the hosted audit's audit_hosted_k.windows) and against the frozen PR589 +hosting selection. Standard library only. +""" +import importlib.util +import json +from pathlib import Path + +ROOT = Path(__file__).resolve().parents[2] +VENDOR = ROOT / 'research/e8-bit-p111-tuned/vendor/pr510/e8-r480-nine-stage/vendor' +HOSTING_CORE = VENDOR / 'idle-axis-hosting/hosting_core.py' +AUDIT_HOSTED = VENDOR / 'e8-r715-eleven-stage-whole/code/audit_hosted_k.py' +SELECTION = ROOT / 'research/e8-bit-p111-tuned/data/selection9-p111.json' +K, L = 4, 9 + + +def _load(name, path): + spec = importlib.util.spec_from_file_location(name, path) + mod = importlib.util.module_from_spec(spec) + spec.loader.exec_module(mod) + return mod + + +def schedule(): + events = [('local', 0, 0)] + stage = 1 + for j in range(K): + events.append(('local', stage, j)); stage += 1 + if j < K - 1: + events.append(('bridge', j, j + 1)) + events.append(('local', stage, j)); stage += 1 + if j < K - 1: + events.append(('bridge', j, j + 1)) + for j in reversed(range(K - 1)): + events.append(('bridge', j + 1, j)) + sched, level = [], [-1] * K + for e in events: + if e[0] == 'local': + _, s, p = e + level[p] = s + sched.append(dict(kind='local_cover_sweep', stage=s, pair=p)) + if s % 2 == 1 and s <= 2 * K - 3: + j = (s + 1) // 2; level[j] = s; sched.append(dict(kind='idle', pair=j, rank=7 * (s + 1))) + elif s % 2 == 0 and 2 <= s <= 2 * K - 2: + j = s // 2; level[j] = s; sched.append(dict(kind='idle', pair=j, rank=7)) + elif s == 2 * K: + for j in range(K): + sched.append(dict(kind='idle', pair=j, rank=7 * (2 * K - level[j]))); level[j] = 2 * K + else: + sched.append(dict(kind='bridge', dst=e[1], src=e[2])) + sched.append(dict(kind='exchange')) + i = 0 + for e in sched: + if e['kind'] == 'idle': + e['idx'] = i + i += 1 + return sched + + +def windows(sched): + out, last, seen = {}, {}, [] + for pos, e in enumerate(sched): + if e['kind'] == 'local_cover_sweep': + seen.append((pos, e['stage'], e['pair'])); last[e['pair']] = pos + elif e['kind'] == 'bridge': + last[e['dst']] = pos; last[e['src']] = pos + elif e['kind'] == 'idle': + out[e['idx']] = (e['pair'], e['rank'], + tuple(sorted(s for q, s, p in seen if last.get(e['pair'], -1) < q < pos and p != e['pair']))) + return out + + +def checked_windows(): + """{child: (capacity, stages)} for the children that can host, after the three-way cross-check.""" + sched = schedule() + mine = windows(sched) + hc = _load('pr442_hosting_core', HOSTING_CORE) + ah = _load('audit_hosted_k', AUDIT_HOSTED) + hc_sched = [dict(e, kind='local') if e['kind'] == 'local_cover_sweep' else e for e in sched if e['kind'] != 'exchange'] + theirs = {i: (p, r, tuple(sorted(st))) for i, (p, r, st) in hc.windows(hc_sched).items()} + W, rank, pair = ah.windows(sched) + audit = {i: (pair[i], rank[i], tuple(sorted(W[i]))) for i in W} + if not (mine == theirs == audit): + raise ValueError('window predicates disagree') + win = {i: (r, st) for i, (p, r, st) in mine.items() if r > 0 and st} + for i, w, s, n in json.loads(SELECTION.read_text())['bit']['stages']: + if s not in win[i][1]: + raise ValueError('frozen selection entry outside its window') + return win diff --git a/research/bit589-width7-windows-seed72/wopt.py b/research/bit589-width7-windows-seed72/wopt.py new file mode 100644 index 0000000000..4e0bd3704d --- /dev/null +++ b/research/bit589-width7-windows-seed72/wopt.py @@ -0,0 +1,159 @@ +# SPDX-License-Identifier: Apache-2.0 +"""Exact window-respecting optimum of k width-7 helpers per call on the PR589 nine-stage bit hosting. + +Per replica: 9 idle children with 222 copies each, capacities and one-level windows from windows.py, +and per stage 439-k width-8 plus k width-7 residuals. The cost of a copy with r unused units is +F_a(r) = r (64/r)^a + 32*64^2*64^a/1e16 for r > 0 (the moment term plus the inherited bad-residue +surcharge) and 0 for r = 0. solve(k, a) returns an exact integer lower bound (units 2^-200, x5) of +the minimum total cost over all window-feasible placements, the minimising width-7 distribution and, +on request, an explicit plan attaining it. The proof steps (Lemma A, interval Hall reduction to two +nested chains, slack decomposition, DP relaxation) are written out in README.md; the code asserts the +checked facts for each k. Uses the merged PR1023 packing.py only for the pinned moment engine. +""" +import importlib.util +import sys +from collections import Counter +from fractions import Fraction as Q +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +sys.path.insert(0, str(HERE)) +import windows # noqa: E402 + + +def _load(name, path): + spec = importlib.util.spec_from_file_location(name, path); m = importlib.util.module_from_spec(spec); spec.loader.exec_module(m); return m + + +P = _load('pr1023_packing', ROOT / 'research/bit589-width-packing/packing.py') +MOM = P.MOMENT +WIN = windows.checked_windows() +M, N, T, STG, R = 64, 222, 32, 9, 439 +CAP = {i: WIN[i][0] for i in WIN} +SEVEN = [i for i in WIN if CAP[i] == 7] # 1, 3, 5 +REST = [i for i in WIN if CAP[i] != 7] # 0, 2, 4, 6, 7, 8 +SHIFT = 1 << 200 + +def Ftilde(a): + """integer lower bounds of F_a(r) = r (64/r)^a + 32*64^2*64^a/1e16 (r>0), F(0)=0, in units 2^-200""" + out = [0] + l, _ = MOM.logarithm(Q(M)); e64, _ = MOM.exponential(a * l, a * MOM.logarithm(Q(M))[1]) + lam = Q(32 * M * M, 10 ** 16) * e64 + for r in range(1, 43): + lo, hi = MOM.logarithm(Q(M, r)); e, _ = MOM.exponential(a * lo, a * hi) + x = (r * e + lam) * SHIFT + out.append(x.numerator // x.denominator) + return out + +def types(c): + m, f = c % 8, c // 8 + w7 = [(l, b, m + 8 * l - 7 * b) for l in range(f + 1) for b in range(1, 7) if m + 8 * l - 7 * b >= 0] + p8 = [(l, m + 8 * l) for l in range(1, f + 1)] + return m, f, w7, p8 + +def V_table(F, Smax): + INF = None; V = [0] + [INF] * Smax; bp = [None] * (Smax + 1) + moves = [(c, l, F[r] - F[c % 8]) for c in (14, 28, 42) for (l, r) in types(c)[3]] + for S in range(1, Smax + 1): + for c, l, d in moves: + if l <= S and V[S - l] is not None: + v = V[S - l] + d + if V[S] is None or v < V[S]: V[S] = v; bp[S] = (c, l) + return V, bp + +def knap(F, c, A, Bmax): + m, f, w7, _ = types(c) + E = [[None] * 5 for _ in range(Bmax + 1)]; bp = [[None] * 5 for _ in range(Bmax + 1)] + E[0][0] = 0 + for B in range(1, Bmax + 1): + for (l, b, r) in w7: + if b > B: continue + cost = 5 * (F[r] - F[m]) - l * A + for rho in range(5): + prev = E[B - b][(rho - l) % 5] + if prev is None: continue + v = prev + cost + if E[B][rho] is None or v < E[B][rho]: E[B][rho] = v; bp[B][rho] = (l, b, r) + return E, bp + +def chain_constraints(k): + """all 45 interval Hall constraints for the width-7 roles of children REST after the 7-slots take stages 2,4,6""" + supply = {s: (0 if s in (2, 4, 6) else k) for s in range(STG)} + cons = [] + for lo in range(STG): + for hi in range(lo, STG): + C = frozenset(i for i in REST if set(WIN[i][1]) <= set(range(lo, hi + 1))) + cons.append((C, sum(supply[s] for s in range(lo, hi + 1)))) + return cons + +LEFT, RIGHT = (0, 2, 4), (8, 7, 6) +def check_chain_reduction(k): + cons = chain_constraints(k) + best = {} + for C, s in cons: + best[C] = min(s, best.get(C, s)) + lb = [best.get(frozenset(LEFT[:j]), None) for j in range(4)] + rb = [best.get(frozenset(RIGHT[:j]), None) for j in range(4)] + assert lb[1:] == [2 * k, 3 * k, 4 * k] and rb[1:] == [2 * k, 3 * k, 4 * k], (lb, rb) + assert best[frozenset(REST)] == 6 * k + for C, s in best.items(): + jl = max(j for j in range(4) if frozenset(LEFT[:j]) <= C); jr = max(j for j in range(4) if frozenset(RIGHT[:j]) <= C) + assert C == frozenset(LEFT[:jl]) | frozenset(RIGHT[:jr]), C + bl = 0 if jl == 0 else lb[jl]; br = 0 if jr == 0 else rb[jr] + assert bl + br <= s or s >= 6 * k, (C, s) + return True + +def solve(k, a, want_plan=False): + F = Ftilde(a) + S0 = 45 + 9 * k + V, vbp = V_table(F, max(S0, 10)) + A = F[42] - F[2] + for S in range(S0 + 1): + assert V[S] == (S // 5) * A + V[S % 5], ('V not periodic', S) + R5 = [5 * V[t] - t * A for t in range(5)] + check_chain_reduction(k) + E = {c: knap(F, c, A, 4 * k) for c in (14, 28, 42)} + bound = {0: 2 * k, 2: 3 * k, 4: 4 * k, 8: 2 * k, 7: 3 * k, 6: 4 * k} + def chain(order): + tab = {(0, 0): (0, ())} + for i in order: + Ec = E[CAP[i]][0]; new = {} + for (Pp, rp), (v, hist) in tab.items(): + for B in range(0, bound[i] - Pp + 1): + for rho in range(5): + e = Ec[B][rho] + if e is None: continue + key = (Pp + B, (rp + rho) % 5); val = v + e + if key not in new or val < new[key][0]: new[key] = (val, hist + ((i, B, rho),)) + tab = new + return tab + Lt, Rt = chain(LEFT), chain(RIGHT) + best = None + for (pl, rl), (vl, hl) in Lt.items(): + for rr in range(5): + if (6 * k - pl, rr) not in Rt: continue + vr, hr = Rt[(6 * k - pl, rr)] + t = (S0 - rl - rr) % 5 + v = vl + vr + R5[t] + if best is None or v < best[0]: best = (v, hl + hr, t) + const5 = 5 * N * sum(F[CAP[i] % 8] for i in WIN) + 15 * k * (F[0] - F[7]) + S0 * A + total5 = const5 + best[0] + plan = None + if want_plan: + copies = {i: [] for i in WIN} + for i in SEVEN: copies[i] = [(0, 1, 0)] * k + lam = 0 + for i, B, rho in best[1]: + bp = E[CAP[i]][1]; b_, r_ = B, rho + while b_: + l, b, r = bp[b_][r_]; copies[i].append((l, b, r)); b_ -= b; r_ = (r_ - l) % 5; lam += l + assert r_ == 0 + S = S0 - lam + assert S >= 0 and S % 5 == best[2] + moves = [(42, 5)] * (S // 5); t = S % 5 + while t: + c, l = vbp[t]; moves.append((c, l)); t -= l + plan = dict(copies=copies, pure8=moves, S=S, lam=lam) + return total5, best, plan, F + From 2bc1959a68a344b730d52395df17b0e746f27105 Mon Sep 17 00:00:00 2001 From: Sagar Thakrar Date: Wed, 14 Oct 2026 14:21:14 +0530 Subject: [PATCH 2/4] Anchor the schedule to global_k.py and correct claims after adversarial review - windows.py: match the nine-stage schedule event by event with the one the pinned global_k.py produces (recipe() and its idle-insertion rule extracted with ast and replayed); a dropped bridge is now rejected (new control). - verify.py: max-flow brute force over every distribution of the 6k residuals (462 / 6188); record binding no longer writes the matched path and accepts a checkpoint record once the frontier moves; certificate bound at module level; #1281 priced rows split into local / pooled32 flags. - test_package.py: real k = 0 tightness check; schedule-anchor control. - VERIFY/SOURCES: declare global_k.py and the selected record as inputs. - README/TASK: per-replica, frozen-recipe scope of #1281's open question 1; #1281's optimum transcribed (not re-derived), 148 rows priced here; overstatement about 1.5x (optimistic) / 1.7x (pessimistic); placement built at run time; #1256 relation; credits (chafreaky PR439/443/444, PR386/436); inherited assumptions; environment; feasible open-question first steps. --- .../bit589-width7-windows-seed72/README.md | 263 +++++++++--------- .../bit589-width7-windows-seed72/RESULT.json | 35 ++- .../bit589-width7-windows-seed72/SOURCES.json | 2 +- .../bit589-width7-windows-seed72/TASK.json | 18 +- .../bit589-width7-windows-seed72/VERIFY.json | 6 +- .../test_package.py | 34 ++- .../bit589-width7-windows-seed72/verify.py | 80 +++--- .../bit589-width7-windows-seed72/windows.py | 60 +++- 8 files changed, 294 insertions(+), 204 deletions(-) diff --git a/research/bit589-width7-windows-seed72/README.md b/research/bit589-width7-windows-seed72/README.md index ba18d68d4d..cd57f5bba2 100644 --- a/research/bit589-width7-windows-seed72/README.md +++ b/research/bit589-width7-windows-seed72/README.md @@ -1,57 +1,54 @@ # Audit: PR442 hosting windows and the partial width-seven rows of #1023 and #1281 -**Adversarial audit: this package finds no new κ and changes no check.** Track 60–74 (adversarial audit), assignment seed 72 -(OS CSPRNG via Python `secrets`). Card `uniform-transfer-audit` (a hosting implication), scope -**refined** in [TASK.json](TASK.json). Base `0b1cccf8`; the selected record frontier1094 (complex-bound) -is unchanged, and `verify.py` binds it to the PR589 record and engines it uses. +**Adversarial audit: no new κ, and no existing check is changed.** + +- Track: 60–74 (adversarial audit), assignment seed 72, drawn with the OS CSPRNG via Python `secrets`. +- Card: `uniform-transfer-audit` (a hosting implication). The scope is **refined** in [TASK.json](TASK.json). +- Base: `0b1cccf8`. The selected record frontier1094 (complex-bound) is unchanged. `verify.py` binds its certificate to the PR589 record and the engines used here. ## The audited claims -- **#1023 (ours, merged, `research/bit589-width-packing`).** It publishes partial width-seven rows: converting k helpers per call to width 7 gives, - for example, k = 37 optimistic 0.0017896275 (+3.24%). The rows are described as achievable - placements in its slot model. They are reached by putting all 9k width-7 residuals in empty - capacity-7 slots. Its README lists window timing as an unchecked obligation. -- **#1281 (mightyOil, merged, `research/bit-partial-width7-optimum`).** It proves the - exact optimum for every k = 0..74 in its mixed-width slot relaxation, replica-local and pooled32. - It openly disclaims temporal constraints. Its **open question 1** asks whether the relaxed optimum - can be hosted in time order. +- **#1023 (ours, merged, `research/bit589-width-packing`).** It publishes partial width-seven rows: k helpers per call are converted to width 7. + - Example: k = 37 optimistic gives 0.0017896275 (+3.24%). + - The rows are described as achievable placements in #1023's slot model. They are reached by putting all 9k width-7 residuals in empty capacity-7 slots. + - Its README lists window timing as an unchecked obligation. +- **#1281 (mightyOil, merged, `research/bit-partial-width7-optimum`).** It proves the exact optimum for every k = 0..74 in its mixed-width slot relaxation, both replica-local and pooled32. + - It openly disclaims temporal constraints. + - Its **open question 1** asks whether the relaxed optimum can be hosted chronologically for an actual width-seven helper. It proposes starting from PR1179's changed entry/exit contract, and testing both per-replica restrictions and possible cross-replica pooling. -This package answers that question for the PR442/PR589 **replica-local** hosting format: the hosted -audit's `hosted[(stage, helper)]` map with per-replica windows `s in W[i]`. +This package settles one part of that question: **per-replica hosting on the frozen PR589 stage recipe**. That means the hosted audit's `hosted[(stage, helper)]` map with per-replica windows `s in W[i]`, whole residuals and no banks. PR1179's contract and cross-replica pooling stay open. ## The windows -[windows.py](windows.py) rebuilds the nine-stage idle schedule from the recipe of `global_k.py` -(K = 4, L = 9) and computes the windows. Three implementations agree exactly: this code, PR442's -`hosting_core.windows`, and `audit_hosted_k.windows`, which enforces `s in W[i]` for every hosted -slot. All 14 frozen `selection9-p111` entries lie inside their windows. +[windows.py](windows.py) writes out the nine-stage idle schedule (K = 4, L = 9) and checks it two ways. + +1. **It matches `global_k.py`.** At run time the schedule is compared, event by event, with the schedule the pinned `global_k.py` itself produces. Its `recipe()` and its idle-insertion rule are extracted from the file with `ast` and replayed, asserts included. +2. **Three window predicates agree.** This code, PR442's `hosting_core.windows`, and `audit_hosted_k.windows` (which enforces `s in W[i]` for every hosted slot) give identical windows on that one shared schedule. + +All 14 frozen `selection9-p111` entries lie inside their windows. + +The selection hosts nothing in children 1, 3 and 5. So the decisive singleton windows rest on the `global_k.py` match: a test drops one bridge from the schedule, and the check rejects it. On such a mutated schedule the three predicates would still agree with each other, while the capacity-7 windows widen. | Idle child | 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | |---|---|---|---|---|---|---|---|---|---| | Capacity | 14 | **7** | 28 | **7** | 42 | **7** | 42 | 28 | 14 | | Admissible stages | 0–1 | **2** | 0–3 | **4** | 0–5 | **6** | 3–8 | 5–8 | 7–8 | -**Each capacity-7 child admits exactly one stage.** Per replica, at most 3k of the 9k width-7 -residuals can sit in 7-slots. The window-free rows of #1023 and #1281 use all 9k. +**Each capacity-7 child admits exactly one stage.** Per replica, at most 3k of the 9k width-7 residuals can sit in 7-slots. The window-free rows of #1023 and #1281 use all 9k. ## Results ([RESULT.json](RESULT.json)) -For every k = 0..74, the package computes the **exact window-respecting optimum**. For each k it -gives: +For every k = 0..74, `verify.py` computes the **exact window-respecting optimum** and does three things: -- an explicit residual-level placement. Every slot is checked for its window, its width and its - offset, cells must be disjoint, and every (stage, helper) is hosted exactly once; -- that placement's bit endpoint under both of #1023's local brackets, using the pinned engines and - the inherited surcharge; -- a **certificate that no window-feasible placement reaches the next 1e-24 grid point**. The - certificate is tight: it equals the engine moment of the explicit histogram to 1e-50. +- **Builds and checks an explicit residual-level placement at run time** (`verify.build`). Every slot is checked for its window, its width and its offset; cells must be disjoint; and every (stage, helper) must be hosted exactly once. RESULT.json records the placement's per-replica idle histogram and its width-7 distribution. The slot list itself is regenerated by `build()`. +- **Prices the placement's bit endpoint** under both of #1023's local brackets, using the pinned engines and the inherited surcharge. +- **Certifies that no window-feasible replica-local placement reaches the next 1e-24 grid point.** The certificate is tight: it equals the engine moment of the explicit histogram to within 1e-50. k = 0 reproduces the selected bit endpoint 0.001733427039589844234749. -Per-replica idle histograms and the width-7 distribution over children 0, 2, 4, 8, 7, 6 are in -RESULT.json for every k. Selected rows, with gain over the selected bit endpoint: +Selected rows, with the gain over the selected bit endpoint: -| k | Bracket | Window-respecting optimum | Window-free optimum (#1281) | Retained | +| k | Bracket | Window-respecting optimum | Window-free optimum (#1281 profile) | Retained | |---|---|---|---|---| | 1 | optimistic | 0.001734347102 (+0.053%) | 0.001734846264 (+0.082%) | 0.648 | | 1 | pessimistic | 0.001734104523 (+0.039%) | 0.001734603545 (+0.068%) | 0.576 | @@ -64,144 +61,148 @@ RESULT.json for every k. Selected rows, with gain over the selected bit endpoint | 74 | optimistic | 0.001809907119 (+4.412%) | 0.001849754238 (+6.711%) | 0.657 | | 74 | pessimistic | 0.001792188010 (+3.390%) | 0.001831249661 (+5.643%) | 0.601 | -Decimals are truncated. The certified bound for each row is the next 1e-24 grid point above the -window-respecting endpoint. - -- **#1023:** all 8 published partial rows (k = 1, 10, 37, 74; optimistic and pessimistic) are - **unreachable** under the windows. Each lies above its certified bound. -- **#1281, replica-local:** every row (k = 1..74, both brackets) is unreachable. The window-free - optimum is re-derived here and matches #1281's merged `EXPECTED.json` (digest-pinned, read as - data; no #1281 code is run). All 75 idle optima agree, and all 9 priced cases agree exactly in - endpoint and full histogram. -- **#1281, pooled32:** its 8 priced rows with k > 0 also lie above the per-replica bound. Pooling - moves residuals between replicas, so it is not replica-local hosting. These rows are unreachable - for replica-local placements only; see the cross-replica caveat below. -- **#1023's all-width-7 optimum `{42:340, 21:1}` stays window-feasible.** 104 sextet splits are - feasible by max-flow, so its +17–23% figure is not affected by the windows. - -Across the whole range, the window-respecting optimum keeps **63.6–67.1%** of the window-free -gain, or 56.3–60.7% under the pessimistic bracket. For small k, the window-free rows overstate the gain -by about 1.5×. None of this changes κ: the selected record is complex-bound, and these are bit -headroom figures. +Notes on the table: +- Endpoints are truncated; percentages and retained fractions are rounded. +- The certified bound for each row is the next 1e-24 grid point above the window-respecting endpoint. +- The window-free column is this package's pricing of #1281's closed-form idle profile. #1281 itself prices k = 0, 1, 2, 37 and 74. + +### How the published rows fare + +- **#1023:** all 8 published partial rows (k = 1, 10, 37 and 74; both brackets) lie above their certified bounds. None is reachable under the windows. +- **#1281, replica-local:** + - #1281's closed-form local optimum is transcribed here (`windowfree_idle`) and checked against its merged `EXPECTED.json`. That file is digest-pinned and read as data; no #1281 code is run. + - All 75 idle profiles agree. All 9 of #1281's priced cases are reproduced exactly, in local endpoint and local histogram. + - Its optimality is #1281's result; this package does not re-derive it. + - Priced here under both brackets, all 148 local rows (k = 1..74) lie above the per-replica bound. 8 of them are also priced by #1281. +- **#1281, pooled32:** its 8 priced rows with k > 0 also lie above the per-replica bound. Pooling moves residuals between replicas, so these rows are ruled out only for replica-local placements. See the cross-replica caveat below. +- **#1023's all-width-7 optimum `{42:340, 21:1}` stays window-feasible.** Max-flow finds 104 feasible sextet splits, so its +17–23% figure is not affected by the windows. + +### How much of the gain survives + +Across k = 1..74, the window-respecting optimum keeps 63.6–67.1% of the window-free gain (optimistic bracket), or 56.3–60.7% (pessimistic). Put the other way, the window-free rows overstate the gain by about 1.5× (1.49–1.57×) or about 1.7× (1.65–1.78×). The ratio is roughly flat in k. + +These figures hold under #1023's one-unit local pricing, the frozen recipe and replica-local hosting. None of this changes κ: the selected record is complex-bound, and these are bit headroom figures. ## Why it is exact (proof sketch; the code asserts each checked fact) -1. **Lemma A (exchange): some optimum puts every stage-2, 4 and 6 width-7 residual alone in a copy - of child 1, 3 or 5.** - - Cost per copy is F(r) = 64^a r^(1−a) + λ for r > 0, with F(0) = 0. Here λ ≥ 0 is the - per-child surcharge term. +1. **Lemma A (exchange): some optimum puts every stage-2, 4 and 6 width-7 residual alone in a copy of child 1, 3 or 5.** + - Cost per copy is F(r) = 64^a r^(1−a) + λ for r > 0, with F(0) = 0. Here λ ≥ 0 is the per-child surcharge term. - F is subadditive on r ≥ 0: r^(1−a) is concave with value 0 at 0, and λ is counted once. - - A capacity-7 copy cannot hold a width-8 residual and holds at most one width-7 residual. Child - 1 has 222 > k copies. - - Moving a stage-2 width-7 residual from a copy with r unused units into an empty copy of child 1 - changes the cost by F(r + 7) − F(r) + F(0) − F(7) ≤ 0. -2. **Width-8 placement is unconstrained (checked for every k ≤ 74).** The windows are stage - intervals, so Hall's condition for the stage → child transport reduces to intervals. For every - proper interval J, the full width-8 capacity of the children whose windows lie in J is at most - the width-8 supply of J. -3. **The width-7 residuals reduce to two nested chains.** After Lemma A, 6k width-7 residuals remain, - from stages 0, 1, 3, 5, 7 and 8, over children 0, 2, 4, 6, 7 and 8. A distribution B is feasible - exactly when all of the following hold: + - A capacity-7 copy cannot hold a width-8 residual and holds at most one width-7 residual. Child 1 has 222 > k copies. + - Moving a stage-2 width-7 residual from a copy with r unused units into an empty copy of child 1 changes the cost by F(r + 7) − F(r) + F(0) − F(7) ≤ 0. +2. **Width-8 placement is unconstrained (checked for every k ≤ 74).** + - The windows are stage intervals, so Hall's condition for the stage → child transport reduces to intervals. + - For every proper interval J, the full width-8 capacity of the children whose windows lie in J is at most the width-8 supply of J. +3. **The width-7 residuals reduce to two nested chains.** After Lemma A, 6k width-7 residuals remain, from stages 0, 1, 3, 5, 7 and 8, over children 0, 2, 4, 6, 7 and 8. A distribution B is feasible exactly when all of the following hold: - B0 ≤ 2k, B0 + B2 ≤ 3k, B0 + B2 + B4 ≤ 4k; - B8 ≤ 2k, B8 + B7 ≤ 3k, B8 + B7 + B6 ≤ 4k; - ΣB = 6k. - This is derived from all 45 interval Hall constraints (asserted for every k). It is also - confirmed by brute force: every distribution for k = 1 and 2 is checked by max-flow against the - chain predicate, all agreeing. -4. **Exact lower bound.** Cost splits three ways: copies holding width-7 residuals (a per-child - knapsack over copy types), copies holding only width-8 slack (#1281's periodic V(S), recomputed - and checked at each a), and the 7-slots. An integer DP over (chain sums, slack mod 5), with - outward-rounded lower bounds of F at 2^−200 from the pinned engine, drops the copy limits and - S ≥ 0. It is therefore a relaxation, which gives a rigorous lower bound. -5. **Attainment and certificate.** The DP minimiser is expanded into the explicit placement above, - whose cost equals the DP value exactly. At a′ = c* + 1e−24, the local moment lower bound plus 32 - times the DP bound exceeds 1. Every replica-local placement, uniform across replicas or not, - therefore has an endpoint below a′. This is grid optimality at each row's own endpoint. - -## Controls ([test_package.py](test_package.py), 11 tests) - -- **C-W1.** #1023's k = 1 placement fills 9 capacity-7 copies per replica, one per stage. The vendored - windows admit only stages 2, 4 and 6 there, so at least 6 residuals sit outside their window. -- **C-W2.** The window-free local rows lie above the certified bound, while the window-respecting - endpoints lie below it. -- **C-W3.** #1281's local and pooled32 priced rows (k > 0) lie above the per-replica bound, and all - 75 idle optima match. + This is derived from all 45 interval Hall constraints, asserted for every k. It is also confirmed by brute force: max-flow is checked against the chain predicate on every distribution of the 6k residuals, all 462 at k = 1 and all 6188 at k = 2, and they agree on every one. +4. **Exact lower bound.** + - Cost splits three ways: + - copies holding width-7 residuals (a per-child knapsack over copy types); + - copies holding only width-8 slack (#1281's periodic V(S), recomputed and checked at each a); + - the 7-slots. + - An integer DP runs over (chain sums, slack mod 5). It uses outward-rounded lower bounds of F at 2^−200 from the pinned engine. + - The DP drops the copy limits and S ≥ 0, so it is a relaxation and gives a rigorous lower bound. +5. **Attainment and certificate.** + - The DP minimiser is expanded into the explicit placement above, whose cost equals the DP value exactly. + - At a′ = c* + 1e−24, the local moment lower bound plus 32 times the DP bound exceeds 1. + - So every replica-local placement, uniform across replicas or not, has an endpoint below a′. This is grid optimality at each row's own endpoint. + +## Controls ([test_package.py](test_package.py), 12 tests) + +- **C-W0 (schedule anchor).** The schedule equals the one `global_k.py` produces. Dropping one bridge is rejected. +- **C-W1.** #1023's k = 1 placement fills 9 capacity-7 copies per replica, one per stage. The windows admit only stages 2, 4 and 6 there, so at least 6 residuals sit outside their window. +- **C-W2.** The window-free local rows lie above the certified bound, while the window-respecting endpoints lie below it. +- **C-W3.** #1281's local and pooled32 priced rows (k > 0) lie above the per-replica bound, and all 75 idle profiles match. - **C-W4.** The all-width-7 optimum is window-feasible. -- **C-W5 (dropped constraint).** Dropping the chain constraint B0 ≤ 2k breaks the brute-force - agreement. +- **C-W5 (dropped constraint).** Dropping the chain constraint B0 ≤ 2k breaks the brute-force agreement. - **C-W5 (perturbed window).** Widening child 0's window to stages 0–3 breaks the chain structure. -Also covered: #1023's eight rows are all unreachable, k = 0 reproduces the selected endpoint, the -brute-force reduction holds at k = 2, and the width-8 Hall conditions are vacuous. +Also covered: +- #1023's eight rows are all unreachable. +- k = 0 reproduces the selected endpoint, and its certificate is recomputed and checked for tightness. +- The exhaustive brute-force reduction holds at k = 2. +- The width-8 Hall conditions are vacuous. ## Reproduce ```sh -python3 -I -B research/bit589-width7-windows-seed72/verify.py # ~2.5 min on one idle core; PASS_BIT589_WIDTH7_WINDOWS +python3 -I -B research/bit589-width7-windows-seed72/verify.py # about 140 s of CPU; PASS_BIT589_WIDTH7_WINDOWS python3 -I -B -m unittest discover -s research/bit589-width7-windows-seed72 -p test_package.py python3 scripts/research_package.py --package research/bit589-width7-windows-seed72 --check-only python3.12 scripts/research_package.py --package research/bit589-width7-windows-seed72 ``` -Standard-library Python 3.10 or later. The pinned engines, record and slot model come from merged -#1023's `packing.py`, which is imported read-only. `verify.py --kmax K` runs a partial check -(`PASS_PARTIAL`). +- **Requirements.** Standard-library Python 3.10 or later. The pinned engines, record and slot model come from merged #1023's `packing.py`, which is imported read-only. `verify.py --kmax K` runs a partial check (`PASS_PARTIAL`). +- **Where it was run.** `verify.py` and the tests pass on Python 3.12.15 and 3.14.8 (macOS 26.5, arm64). `--check-only` passes. +- **Registered replay.** The python3.12 replay was run locally. It exceeded its 600 s wall-clock limit only because the host was heavily loaded (load average about 100). `verify.py` itself needs about 140 s of CPU. ## Scope and remaining obligations -- **Hosting format.** This applies to the PR442/PR589 nine-stage template (the 2P + 1 stage format - with P = 4; #743) with replica-local hosting, whole residuals, no banks and the frozen stage - recipe. A changed recipe, split residuals or banks lie outside it. Open #1487 (ianlibanio) varies - the nine-stage recipe for width-8 hosting; its recipes may have other capacity-7 windows, which - this package does not check. -- **Cross-replica owner maps are open.** The selected complex T16 supplier uses cross-replica - interleaved owner maps (`owner_replica ≠ replica`). Such a map could admit other replicas' calls - at other stages into the 7-slot windows. That case is **not** ruled out here. +- **Hosting format.** + - This applies to the PR442/PR589 nine-stage template with replica-local hosting, whole residuals, no banks and the frozen stage recipe. (#743 proves the 2P + 1 stage lower bound that this format attains.) + - A changed recipe, split residuals or banks lie outside it. + - Open #1487 (ianlibanio) varies the nine-stage recipe for width-8 hosting. Its recipes may have other capacity-7 windows, which this package does not check. +- **Cross-replica owner maps are open.** The selected complex T16 supplier uses cross-replica interleaved owner maps (`owner_replica ≠ replica`). Such a map could admit other replicas' calls at other stages into the 7-slot windows. That case is **not** ruled out here. - **Windows are necessary, not sufficient.** - - Projector compatibility is still open. #1307's caveat applies: slots that split q⊥ lie outside - its completion-free argument, and that covers width-7 residuals in 14-, 28- and 42-slots. + - Projector compatibility is still open. #1307's caveat applies: slots that split q⊥ lie outside its completion-free argument, and that covers width-7 residuals in 14-, 28- and 42-slots. - Owner inactivity is still open. - - A physical width-7 helper is still open (#1128, #1271, #1256, #1362). + - A physical width-7 helper is still open: #1128, #1179, #1256, #1271, and #1393 (discussion #1362). - So the window optimum is itself only an upper bound for real hosting, while the unreachability - direction holds. -- **Pricing assumption.** The prices keep #1023's assumption that each converted helper removes - one unit from one local child. + So the window optimum is itself only an upper bound for real hosting, while the unreachability direction holds. +- **Pricing assumption.** The prices keep #1023's assumption that each converted helper removes one unit from one local child. - **Uniqueness.** Histograms are not shown to be unique; ties exist, for example at k = 2. - -## Relation to #1023 and #1281 - -- **#1023.** Its partial rows are window-free relaxation values, and this package gives the - window-respecting values. #1023's frozen files are left untouched. -- **#1281.** Its optima are correct for the relaxation it states. This package answers the window - part of its open question 1: the relaxed optimum cannot be hosted chronologically by any - replica-local placement. It gives the exact window-respecting optimum instead. The physical - helper, source access and restoration parts of that question stay open. +- **Inherited assumptions.** All of them remain: + - all-size compilation; + - common-label/mutable-source realization; + - whole-call hosting; + - precision/tape; + - analytic transfer; + - bit H1–H5; + - the bit bad-residue surcharge, which every price above keeps. + + This is not a construction and not a formal proof of the multiplication theorem. + +## Relation to earlier work + +- **#1023.** Its partial rows are window-free relaxation values; this package gives the window-respecting values. #1023's frozen files are left untouched. +- **#1281.** Its optima are correct for the relaxation it states. + - This package settles the per-replica, frozen-recipe part of the window question in its open question 1. Under the frozen PR589 stage recipe, whole residuals and no banks (`s in W[i]`), the relaxed optimum cannot be hosted chronologically by any replica-local placement. The exact window-respecting optimum is given instead. + - The rest of that question stays open: the PR1179 boundary-contract audit (#1179, adamgall), the cross-replica pooling test, and the physical helper, source-access and restoration parts. + - Whether PR1179's changed entrance leaves these stage windows unchanged is not checked here. +- **#1256.** Its two-slot relaxation moves a width-seven residual into a formerly idle rank-seven slot and leaves the owner/window assignment open. Under this recipe, that move is window-feasible only for a residual hosted at stage 2, 4 or 6 (children 1, 3 and 5). Residuals from the other six stages need a larger host. ## Open next questions -1. **Can cross-replica (T16-style) interleaved owner maps lift the one-stage 7-slot windows for the - bit supplier?** That would make #1281's pooled rows a real target. +1. **Can cross-replica (T16-style) interleaved owner maps lift the one-stage 7-slot windows for the bit supplier?** This is one route to #1281's pooled rows; a changed recipe, split residuals or banks are others. - First step: compute windows on an interleaved bit timeline and rerun the DP. -2. **Does another nine-stage recipe widen the capacity-7 windows?** #1487 enumerates recipes for - width-8 hosting only. - - First step: feed each of #1487's recipes to `windows.windows` and rerun `wopt.solve` at k = 1 - and k = 37. -3. **Do the window-respecting placements pass projector compatibility (#1307) for mixed-width - slots?** - - First step: run the projector check on the k = 1 explicit placement. +2. **Does another nine-stage recipe widen the capacity-7 windows?** #1487 enumerates recipes for width-8 hosting only. + - First step: generalise `wopt`'s two-chain DP to arbitrary interval windows (or use a min-cost-flow bound), then apply it to #1487's hostable recipes. + - Blocked by: the generalised DP. `wopt.solve` currently asserts this recipe's chain structure. +3. **Do the window-respecting placements pass projector compatibility (#1307) for mixed-width slots?** + - First step: regenerate the k = 1 placement with `verify.build` and run #1307's projector check on it. ## Credit - #1023: Sagar Thakrar. - #1281: mightyOil (Philipp), with OpenAI Codex GPT-6 Astra assistance. -- #743: 0xjohnnydev, the 2P + 1 stage bound. #1487: ianlibanio. #1128: aliromman. #1307: commdata2338. - PR442: DaysSky, the hosting windows. +- PR444: chafreaky, the ownership/window audit that `audit_hosted_k` extends. +- PR439 and PR443: chafreaky, the recipe that `global_k.py` generalises. +- PR386 and PR436: Zhihao Chen and eumemic, the global identity and template. - PR463, PR510 and PR589: DreamingOfClouds, the hosted audit and the bit supplier. - PR555: eumemic. +- Also cited: + - #743: 0xjohnnydev; + - #1179: adamgall; + - #1256: RossRichardson; + - #1393: 1337isnot1337; + - #1487: ianlibanio; + - #1128: aliromman; + - #1307: commdata2338. - The retained moment-engine authors. -Prepared by Sagar Thakrar (thakrarsagar) with substantial AI assistance from Claude (Anthropic) via -Claude Code. Parallel read-only scout and judge subagents found and checked the window obstruction. -New material is Apache-2.0. +Prepared by Sagar Thakrar (thakrarsagar) with substantial AI assistance from Claude (Anthropic) via Claude Code. Parallel read-only scout and judge subagents found the window obstruction. A post-PR adversarial review found the overclaims and the missing schedule anchor fixed in the second commit. New material is Apache-2.0. diff --git a/research/bit589-width7-windows-seed72/RESULT.json b/research/bit589-width7-windows-seed72/RESULT.json index 999c9ce950..7050ee6dd7 100644 --- a/research/bit589-width7-windows-seed72/RESULT.json +++ b/research/bit589-width7-windows-seed72/RESULT.json @@ -14,7 +14,7 @@ "assembly": "research/community-frontier1094-audit/ASSEMBLY.json", "assembly_sha256": "1122cb3a575f8c788345fc1bf4c108ac7c3250fb81a5988671f5eb04b3ab3045", "bit_lower": "1733427039589844234749/1000000000000000000000000", - "record": "certificates/selected-result.json" + "named_by": "certificates/selected-result.json or certificates/checkpoints/*.json" }, "capacity7_children": { "1": [ @@ -30,8 +30,8 @@ "chain_reduction_brute_force": { "agree": "all", "distributions_checked": { - "1": 432, - "2": 5908 + "1": 462, + "2": 6188 } }, "pr1023_partial_rows": { @@ -78,63 +78,72 @@ }, "pr1281": { "idle_optima_matched": 75, - "local_rows_unreachable": "148 of 148 (both brackets, k = 1..74)", + "local_rows_unreachable": "148 of 148 priced here (both brackets, k = 1..74; 8 priced by #1281)", "merged": "e4a7f61f168837f628a1d8b54aa5cff0680f9a38", "path": "research/bit-partial-width7-optimum/EXPECTED.json", "priced_cases": { "k0_optimistic": { "certified_bound": "6933708158359376939/4000000000000000000000", "local": "0.001733427039589844234749", + "local_above_bound": false, "pooled32": "0.001733427039589844234749", - "unreachable": false + "pooled32_above_per_replica_bound": false }, "k1_optimistic": { "certified_bound": "1734347102923006399613/1000000000000000000000000", "local": "0.001734846264120199151475", + "local_above_bound": true, "pooled32": "0.001734900431583947157341", - "unreachable": true + "pooled32_above_per_replica_bound": true }, "k1_pessimistic": { "certified_bound": "108381532739553010717/62500000000000000000000", "local": "0.001734603545275303824122", + "local_above_bound": true, "pooled32": "0.001734657697586404233802", - "unreachable": true + "pooled32_above_per_replica_bound": true }, "k2_optimistic": { "certified_bound": "1388217536169998549/800000000000000000000", "local": "0.001736327170598942735353", + "local_above_bound": true, "pooled32": "0.0017363781660342837852", - "unreachable": true + "pooled32_above_per_replica_bound": true }, "k2_pessimistic": { "certified_bound": "216848289009341626869/125000000000000000000000", "local": "0.0017358409713034135953", + "local_above_bound": true, "pooled32": "0.001735891938199934503774", - "unreachable": true + "pooled32_above_per_replica_bound": true }, "k37_optimistic": { "certified_bound": "1770809187427053553943/1000000000000000000000000", "local": "0.001789671631346367026824", + "local_above_bound": true, "pooled32": "0.001789725802593008582027", - "unreachable": true + "pooled32_above_per_replica_bound": true }, "k37_pessimistic": { "certified_bound": "1761884716885951335477/1000000000000000000000000", "local": "0.001780556367920637129218", + "local_above_bound": true, "pooled32": "0.001780609989052611495117", - "unreachable": true + "pooled32_above_per_replica_bound": true }, "k74_optimistic": { "certified_bound": "904953559530015237129/500000000000000000000000", "local": "0.00184975423837042835336", + "local_above_bound": true, "pooled32": "0.001849803954130003404634", - "unreachable": true + "pooled32_above_per_replica_bound": true }, "k74_pessimistic": { "certified_bound": "56005875337664138131/31250000000000000000000", "local": "0.001831249661111873873002", + "local_above_bound": true, "pooled32": "0.001831298387323686469848", - "unreachable": true + "pooled32_above_per_replica_bound": true } }, "sha256": "a6ec64866b949626d6508ee7172b144c3fd29f1065822b523fafd7d2a59e2e91" diff --git a/research/bit589-width7-windows-seed72/SOURCES.json b/research/bit589-width7-windows-seed72/SOURCES.json index 1cdc6c9918..2d84eb3a01 100644 --- a/research/bit589-width7-windows-seed72/SOURCES.json +++ b/research/bit589-width7-windows-seed72/SOURCES.json @@ -64,7 +64,7 @@ }, { "path": "research/e8-bit-p111-tuned/vendor/pr510/e8-r480-nine-stage/vendor/e8-r715-eleven-stage-whole/code/global_k.py", - "usage": "provenance", + "usage": "input", "git_blob": "3df12bd632f1fdba825ced57110a1fee82eb2857", "sha256": "6368196a393ac25bb2918880e4c4bd31ed733b762c27b6873ab391cbc0c5c3c8" }, diff --git a/research/bit589-width7-windows-seed72/TASK.json b/research/bit589-width7-windows-seed72/TASK.json index def1366f6b..cba3630b0a 100644 --- a/research/bit589-width7-windows-seed72/TASK.json +++ b/research/bit589-width7-windows-seed72/TASK.json @@ -40,32 +40,32 @@ ] }, "scope_status": "refined", - "actual_scope": "One hosting implication for the selected PR589 bit supplier: do the window-free partial width-seven rows of merged #1023 and merged #1281 (width-7 residuals placed in capacity-7 idle slots without time order) survive PR442's replica-local hosting windows (audit_hosted_k: s in W[i] for every hosted slot) on the nine-stage template? Exact window-respecting optimum and certificate for every k = 0..74.", + "actual_scope": "One hosting implication for the selected PR589 bit supplier: do the window-free partial width-seven rows of merged #1023 and merged #1281 (width-7 residuals placed in capacity-7 idle slots without time order) survive PR442's replica-local hosting windows (audit_hosted_k: s in W[i] for every hosted slot) on the frozen nine-stage recipe, whole residuals, no banks? Exact window-respecting optimum and certificate for every k = 0..74.", "scope_change_reason": "The card asks for one exact hosting implication; this narrows it to the time-order hypothesis that #1023 lists as unchecked and that #1281 states as its open question 1. Replica-local hosting only; cross-replica owner maps, projector compatibility, owner inactivity and a physical width-7 helper stay open.", - "bottleneck_link": "Side result on the bit supplier; the selected record is complex-bound, so no kappa changes. It corrects the bit headroom any partial width-seven helper mechanism can buy under replica-local hosting: about two thirds of the window-free gain, so the published rows overstate it by about 1.5x.", + "bottleneck_link": "Side result on the bit supplier; the selected record is complex-bound, so no kappa changes. Under #1023's one-unit local pricing, the frozen recipe and replica-local hosting, it corrects the bit headroom a partial width-seven helper mechanism can buy: the window-respecting optimum keeps 63.6-67.1% (optimistic) or 56.3-60.7% (pessimistic) of the window-free gain, i.e. the published rows overstate it by about 1.5x or 1.7x, roughly flat in k.", "budget_minutes": 180, "stop_rule": "Stop once every k = 0..74 has an explicit window-feasible placement and a tight grid certificate under both local brackets, k = 0 reproduces the selected bit endpoint, and every #1023 and #1281 row is compared; report any row not decided instead of claiming it.", "outcome": "completed", - "evidence": "RESULT.json: windows equal in three implementations (own, PR442 hosting_core, audit_hosted_k), frozen selection inside them; capacity-7 children 1/3/5 admit only stages 2/4/6, so at most 3k of 9k width-7 residuals per replica sit in 7-slots. Exact window-respecting optimum with explicit placement and tight 1e-24 certificate for every k = 0..74, both brackets; k = 0 reproduces 0.001733427039589844234749. k = 37 optimistic 0.001770809187 (+2.157%) vs window-free 0.001789671631 (+3.245%); k = 74 0.001809907119 (+4.412%) vs 0.001849754238 (+6.711%). Retained fraction 0.636-0.671 (optimistic), 0.563-0.607 (pessimistic). All 8 #1023 partial rows and all 148 #1281 local rows unreachable; #1281's 75 idle optima and 9 priced cases reproduced exactly from its merged EXPECTED.json; its pooled32 rows above the per-replica bound. #1023's all-width-7 optimum stays window-feasible (104 sextet splits). 11 tests pass.", + "evidence": "RESULT.json: the nine-stage idle schedule equals, event by event, the one the pinned global_k.py produces (recipe and idle rule extracted and replayed); three window predicates agree on it; the frozen selection lies inside. Capacity-7 children 1/3/5 admit only stages 2/4/6, so at most 3k of 9k width-7 residuals per replica sit in 7-slots. Exact window-respecting optimum, an explicit placement built and checked at run time, and a tight 1e-24 certificate for every k = 0..74, both brackets; k = 0 reproduces 0.001733427039589844234749. k = 37 optimistic 0.001770809187 (+2.157%) vs window-free 0.001789671631 (+3.245%); k = 74 0.001809907119 (+4.412%) vs 0.001849754238 (+6.711%). Retained fraction 0.636-0.671 (optimistic), 0.563-0.607 (pessimistic). All 8 #1023 partial rows unreachable; #1281's closed-form local optimum transcribed and checked against its 75 idle profiles; all 148 local rows priced here from it (8 also priced by #1281, reproduced exactly in local endpoint and histogram) lie above the per-replica bound, as do #1281's 8 priced pooled32 rows with k > 0. Chain reduction confirmed by max-flow on every distribution (462 at k = 1, 6188 at k = 2). #1023's all-width-7 optimum stays window-feasible (104 sextet splits). 12 tests pass.", "author": "Sagar Thakrar (thakrarsagar)", - "ai_assistance": "Substantial: Claude (Anthropic) via Claude Code. Parallel read-only scout and judge subagents proposed and ranked audit candidates and found the window obstruction; the DP, placement builder and certificates were written with Claude and checked by the controls in test_package.py.", + "ai_assistance": "Substantial: Claude (Anthropic) via Claude Code. Parallel read-only scout and judge subagents proposed and ranked audit candidates and found the window obstruction; the DP, placement builder and certificates were written with Claude and checked by the controls in test_package.py. A post-PR adversarial review (three reviewers and a verifier) found overclaims and the missing schedule anchor, fixed in the second commit.", "open_questions": [ { "question": "Can cross-replica (T16-style) interleaved owner maps lift the one-stage capacity-7 windows for the bit supplier?", - "why_it_matters": "Only then could #1281's pooled rows, or the window-free local rows, be reached; replica-local hosting is ruled out here.", - "first_step": "Compute windows on an interleaved bit timeline with owner_replica != replica and rerun wopt.solve.", + "why_it_matters": "One route (others: a changed recipe, split residuals, banks) to #1281's pooled rows or the window-free local rows; replica-local hosting on the frozen recipe is ruled out here.", + "first_step": "Compute windows on an interleaved bit timeline with owner_replica != replica and rerun the DP.", "blocked_by": "An interleaved bit timeline; the selected T16 maps are complex-side." }, { "question": "Does another nine-stage stage recipe widen the capacity-7 windows?", "why_it_matters": "The obstruction is recipe-specific; open #1487 enumerates recipes for width-8 hosting only.", - "first_step": "Feed each of #1487's recipes to windows.windows and rerun wopt.solve at k = 1 and k = 37.", - "blocked_by": "None." + "first_step": "Generalise wopt's two-chain DP to arbitrary interval windows (or use a min-cost-flow bound), then apply it to #1487's hostable recipes.", + "blocked_by": "The generalised DP: wopt.solve asserts this recipe's chain structure." }, { "question": "Do the window-respecting placements pass projector compatibility (#1307) for mixed-width slots?", "why_it_matters": "Windows are necessary, not sufficient; slots that split q-perp lie outside #1307's completion-free argument.", - "first_step": "Run #1307's projector check on the k = 1 explicit placement.", + "first_step": "Regenerate the k = 1 placement with verify.build and run #1307's projector check on it.", "blocked_by": "None." } ] diff --git a/research/bit589-width7-windows-seed72/VERIFY.json b/research/bit589-width7-windows-seed72/VERIFY.json index e182b3bd6c..66ebec981f 100644 --- a/research/bit589-width7-windows-seed72/VERIFY.json +++ b/research/bit589-width7-windows-seed72/VERIFY.json @@ -4,6 +4,7 @@ "python": "3.12", "requirements": [], "inputs": [ + "certificates/selected-result.json", "research/bit-partial-width7-optimum/EXPECTED.json", "research/bit589-width-packing/RESULT.json", "research/bit589-width-packing/SOURCES.json", @@ -12,6 +13,7 @@ "research/e8-bit-p111-tuned/data/selection9-p111.json", "research/e8-bit-p111-tuned/tune/EXPECTED.json", "research/e8-bit-p111-tuned/vendor/pr510/e8-r480-nine-stage/vendor/e8-r715-eleven-stage-whole/code/audit_hosted_k.py", + "research/e8-bit-p111-tuned/vendor/pr510/e8-r480-nine-stage/vendor/e8-r715-eleven-stage-whole/code/global_k.py", "research/e8-bit-p111-tuned/vendor/pr510/e8-r480-nine-stage/vendor/idle-axis-hosting/hosting_core.py", "research/native-complex-moment552/engines/base_two_moment.py", "research/native-complex-moment552/engines/moment.py", @@ -26,7 +28,7 @@ "{package}/verify.py" ], "timeout_seconds": 600, - "checks": "Binds selected record -> frontier1094 ASSEMBLY -> the PR589 record and engines pinned by #1023's packing.py; rebuilds the nine-stage idle schedule and windows, equal to PR442 hosting_core.windows and audit_hosted_k.windows, frozen selection inside its windows; capacity-7 children admit one stage each; chain reduction by brute force (k = 1, 2); for every k = 0..74 the DP optimum, an explicit residual-level placement attaining it (window, width, offset, disjoint cells, hosted once), both local brackets priced with the pinned engines, a 1e-24 grid certificate tight to 1e-50 against the explicit histogram; #1023's eight partial rows and merged #1281's EXPECTED.json (75 idle optima, 9 priced cases with exact endpoints and histograms; local and pooled32 rows above the bound); #1023's all-width-7 optimum window-feasible; RESULT.json byte-identical." + "checks": "Binds the frontier1094 certificate (named by the selected or a checkpoint record) -> the PR589 record and engines pinned by #1023's packing.py; matches the nine-stage idle schedule event by event with the one the pinned global_k.py produces (recipe and idle-insertion rule extracted and replayed); three window predicates agree on it and the frozen selection lies inside; capacity-7 children admit one stage each; chain reduction by max-flow over every distribution for k = 1, 2; for every k = 0..74 the DP optimum, an explicit residual-level placement built and checked at run time (window, width, offset, disjoint cells, hosted once), both local brackets priced with the pinned engines, a 1e-24 grid certificate tight to 1e-50 against the explicit histogram; #1023's eight partial rows; merged #1281's EXPECTED.json (75 idle profiles; 9 priced cases reproduced exactly in local endpoint and local histogram; local and pooled32 endpoints above the per-replica bound); #1023's all-width-7 optimum window-feasible; RESULT.json byte-identical." }, { "argv": [ @@ -42,7 +44,7 @@ "test_package.py" ], "timeout_seconds": 300, - "checks": "Capacity-7 windows, #1023's k = 1 placement outside its windows, k = 0 reproduction, window-free rows above and window-respecting rows below the bound, #1281 local and pooled rows, all-width-7 feasibility, brute-force reduction, dropped chain constraint and perturbed window controls, width-8 Hall vacuity." + "checks": "Capacity-7 windows; schedule = global_k.py's and a dropped bridge is caught; #1023's k = 1 placement outside its windows; k = 0 endpoint and a recomputed tight certificate; window-free rows above and window-respecting rows below the bound; #1281 local and pooled32 rows; all-width-7 feasibility; exhaustive brute-force reduction (6188 distributions at k = 2); dropped chain constraint and perturbed window controls; width-8 Hall vacuity." } ] } diff --git a/research/bit589-width7-windows-seed72/test_package.py b/research/bit589-width7-windows-seed72/test_package.py index ca85e2d97d..0a0917ef6a 100644 --- a/research/bit589-width7-windows-seed72/test_package.py +++ b/research/bit589-width7-windows-seed72/test_package.py @@ -21,6 +21,10 @@ RESULT = json.loads((HERE / 'RESULT.json').read_text()) +def row_idle(k): + return RESULT['rows'][k]['idle'] + + class Windows(unittest.TestCase): def test_capacity7_children_admit_one_stage_each(self): ah = windows._load('audit_hosted_k', windows.AUDIT_HOSTED) @@ -28,6 +32,18 @@ def test_capacity7_children_admit_one_stage_each(self): sevens = {i: sorted(W[i]) for i in W if rank[i] == 7 and W[i]} self.assertEqual(sevens, {1: [2], 3: [4], 5: [6]}) + def test_schedule_matches_global_k_and_a_dropped_bridge_is_caught(self): + sched = windows.schedule() + self.assertEqual(windows._events(sched), windows._events(windows.global_k_schedule())) + first_bridge = next(n for n, e in enumerate(sched) if e['kind'] == 'bridge') + mutated = sched[:first_bridge] + sched[first_bridge + 1:] + with self.assertRaisesRegex(ValueError, 'global_k.py'): + windows.checked_windows(mutated) + # without the anchor, the three predicates would still agree on the mutated schedule + # while the capacity-7 windows widen, which is why the anchor is needed + widened = {i: st for i, (p, r, st) in windows.windows(mutated).items() if r == 7} + self.assertNotEqual(widened, {1: (2,), 3: (4,), 5: (6,)}) + def test_cw1_window_free_k1_uses_nine_seven_slots(self): # #1023's partial placement (packing.width7_partial_idle) fills 9 capacity-7 copies per replica # with one width-7 residual from each of the 9 stages; the vendored windows admit only stages @@ -42,8 +58,18 @@ def test_cw1_window_free_k1_uses_nine_seven_slots(self): class Certificates(unittest.TestCase): def test_k0_reproduces_the_selected_endpoint_and_is_tight(self): row = RESULT['rows']['0']['optimistic'] - self.assertEqual(Q(row['endpoint']), Q(wopt.P.pinned_json('bit_record')['nine']['bit_lower'])) - self.assertTrue(row['same_argmin_at_bound']) + record = wopt.P.pinned_json('bit_record') + self.assertEqual(Q(row['endpoint']), Q(record['nine']['bit_lower'])) + model = wopt.P.slot_model(record, wopt.P.pinned_json('selection')) + W, calls = record['nine']['bit']['live'], model['calls'] + local, _ = wopt.P.local_bracket(model['local'], 0) + at = Q(row['certified_bound']) + lb, _ = V.certificate_bound(0, local, at, calls, W) + H = Counter({r: n * calls for r, n in local.items()}) + H.update({int(r): n * wopt.T for r, n in row_idle('0').items()}) + lo, _ = wopt.P.MOMENT.moment(dict(+H), wopt.M, W, at, True) + self.assertGreater(lb, 1) + self.assertLess(abs(lb - lo), Q(1, 10 ** 50)) def test_cw2_window_free_local_rows_exceed_the_bound(self): for k in ('1', '2', '10', '37', '74'): @@ -57,7 +83,7 @@ def test_cw3_pr1281_local_and_pooled_rows_exceed_the_per_replica_bound(self): self.assertEqual(len(priced), 9) for key, row in priced.items(): if key != 'k0_optimistic': - self.assertTrue(row['unreachable'], key) + self.assertTrue(row['local_above_bound'] and row['pooled32_above_per_replica_bound'], key) self.assertEqual(RESULT['pr1281']['idle_optima_matched'], 75) def test_pr1023_partial_rows_all_unreachable(self): @@ -80,7 +106,7 @@ def test_cw4_all_width7_optimum_is_window_feasible(self): class Reduction(unittest.TestCase): def test_brute_force_matches_the_chains(self): n, agree = V.brute_force_reduction(2) - self.assertEqual(n, agree) + self.assertEqual((n, agree), (6188, 6188)) # every composition of 12 into six parts def test_cw5_dropping_a_chain_constraint_breaks_agreement(self): original = V.chain_ok diff --git a/research/bit589-width7-windows-seed72/verify.py b/research/bit589-width7-windows-seed72/verify.py index 6a62a9ee8a..75b33acf8c 100644 --- a/research/bit589-width7-windows-seed72/verify.py +++ b/research/bit589-width7-windows-seed72/verify.py @@ -4,18 +4,23 @@ Usage: python3 -I -B research/bit589-width7-windows-seed72/verify.py [--write] [--kmax K] -0. Binds the selected record -> frontier1094 ASSEMBLY -> the PR589 record and engines pinned by #1023's packing.py. -1. Rebuilds the nine-stage idle schedule and its hosting windows, cross-checked against both vendored - predicates and the frozen PR589 selection (windows.py). Capacity-7 children admit one stage each. -2. Checks the interval Hall reduction to two nested chains by brute force for k = 1, 2. +0. Binds the frontier1094 certificate (named by the selected record, or by a checkpoint record once + the frontier moves) -> the PR589 record and engines pinned by #1023's packing.py. +1. Builds the nine-stage idle schedule, matches it event by event with the schedule the pinned + global_k.py produces, and runs three window predicates on it (windows.py); the frozen PR589 + selection lies inside the windows. Capacity-7 children admit one stage each. +2. Checks the interval Hall reduction to two nested chains by max-flow over every distribution of + the 6k residuals for k = 1, 2. 3. For every k = 0..74 converted helpers per call: the exact window-respecting optimum (DP lower bound), an explicit residual-level placement attaining it (window, width, offset, disjoint cells, every - (stage, helper) hosted once), its bit endpoint under both of #1023's local brackets with the pinned + (stage, helper) hosted once; built and checked at run time by build()), its bit endpoint under both of #1023's local brackets with the pinned engines, a certificate that no window-feasible placement reaches the next 1e-24 grid point, and a tightness check against the engine moment of the explicit histogram. 4. Compares with the window-free rows: #1023's eight partial rows (its RESULT.json) and merged #1281's - EXPECTED.json (digest-pinned): its local idle optimum for every k, and its nine priced cases - (local endpoints and histograms reproduced exactly; local and pooled32 endpoints above the bound). + EXPECTED.json (digest-pinned). #1281's closed-form local optimum is transcribed in windowfree_idle(), + checked against its 75 idle profiles and re-priced here for every k; its nine priced cases are + reproduced exactly in local endpoint and local histogram; local and pooled32 endpoints of the + priced cases lie above the per-replica bound. 5. Checks that #1023's all-width-7 optimum {42:340, 21:1} is window-feasible. Expected last line: PASS_BIT589_WIDTH7_WINDOWS """ @@ -36,28 +41,28 @@ sha256='a6ec64866b949626d6508ee7172b144c3fd29f1065822b523fafd7d2a59e2e91') -RECORDS = ('certificates/selected-result.json', 'certificates/checkpoints/frontier1094.json') ASSEMBLY = 'research/community-frontier1094-audit/ASSEMBLY.json' def bind(): - """Selected record -> frontier1094 ASSEMBLY -> the PR589 record and engines that #1023's packing.py pins.""" + """frontier1094 ASSEMBLY -> the PR589 record and engines that #1023's packing.py pins. The certificate + must be named, with its digest, by the selected record or (after the frontier moves) by a record in + certificates/checkpoints/; which one is not written to RESULT.json.""" raw = (P.ROOT / ASSEMBLY).read_bytes() - bound = None - for path in RECORDS: - f = P.ROOT / path + records = [P.ROOT / 'certificates/selected-result.json'] + sorted((P.ROOT / 'certificates/checkpoints').glob('*.json')) + named = False + for f in records: rec = json.loads(f.read_text()) if f.is_file() else {} - if rec.get('certificate') == ASSEMBLY and rec.get('certificate_sha256') == P.sha256(raw): - bound = path - break - need(bound is not None, 'a record binds the frontier1094 certificate') + named = named or (rec.get('certificate') == ASSEMBLY and rec.get('certificate_sha256') == P.sha256(raw)) + need(named, 'a selected or checkpoint record names the frontier1094 certificate') asm = json.loads(raw) need(asm['input_sha256']['package:inputs/PR589-EXPECTED.json'] == P.SOURCES['inputs']['bit_record']['sha256'], 'the certificate pins the PR589 record that packing.py reads') for name in ('moment.py', 'base_two_moment.py', 'outer.py'): need(asm['input_sha256']['engines/' + name] == P.SOURCES['engines'][name], 'the certificate pins engine ' + name) need(Q(asm['bit_lower']) == Q(P.pinned_json('bit_record')['nine']['bit_lower']), 'certificate bit endpoint = PR589 record') - return dict(record=bound, assembly=ASSEMBLY, assembly_sha256=P.sha256(raw), bit_lower=asm['bit_lower']) + return dict(assembly=ASSEMBLY, assembly_sha256=P.sha256(raw), bit_lower=asm['bit_lower'], + named_by='certificates/selected-result.json or certificates/checkpoints/*.json') def need(ok, label): @@ -132,15 +137,14 @@ def chain_ok(B, k): def brute_force_reduction(k): - """Every distribution of the 6k non-7-slot width-7 residuals over children 0,2,4,6,7,8: window - transport feasibility (max-flow) must equal the chain predicate.""" + """Every distribution of the 6k non-7-slot width-7 residuals over children 0,2,4,6,7,8 (all + compositions of 6k into six parts): window transport feasibility (max-flow) must equal the chain + predicate.""" supply = {s: (0 if s in (2, 4, 6) else k) for s in range(STG)} count = agree = 0 - for parts in itertools.product(range(4 * k + 1), repeat=5): - last = 6 * k - sum(parts) - if last < 0: - continue - B = dict(zip(REST, list(parts) + [last])) + for bars in itertools.combinations(range(6 * k + 5), 5): + cuts = (-1,) + bars + (6 * k + 5,) + B = dict(zip(REST, [cuts[i + 1] - cuts[i] - 1 for i in range(6)])) feasible = maxflow_assign(supply, {i: B[i] for i in REST}, {i: set(WIN[i][1]) for i in REST}) is not None count += 1 agree += feasible == chain_ok(B, k) @@ -201,8 +205,17 @@ def build(k, plan): return +rem +def certificate_bound(k, local, at, calls, W): + """Moment lower bound at `at` over every window-feasible replica-local placement (DP over the idle + children, exact moment of the fixed local histogram), and the DP argmin plan there.""" + tot5, _, plan, _ = wopt.solve(k, at, True) + lo_local, _ = P.MOMENT.moment(dict(Counter({r: n * calls for r, n in local.items()})), M, W, at, True) + return lo_local + Q(T * tot5, 5 * SHIFT * M * W), plan + + def windowfree_idle(k): - """#1281's replica-local optimum without windows (every width-7 role in a 7-slot; S = 45 + 9k = 5q + t).""" + """#1281's replica-local optimum without windows, transcribed from its closed form (every width-7 role in + a 7-slot; S = 45 + 9k = 5q + t) and checked against its EXPECTED.json idle profiles in main().""" S = 45 + 9 * k q, t = divmod(S, 5) idle = Counter({7: 666 - 9 * k, 6: 444, 4: 444, 2: 444}) @@ -248,12 +261,6 @@ def price(local, idle): need(sum(r * n for r, n in H.items()) == sum(r * n for r, n in model['H'].items()), 'rank mass') return P.endpoint(dict(H), W), H - def lower_bound(k, local, at): - """Moment lower bound at `at` over every window-feasible placement, and the DP argmin there.""" - tot5, _, plan, _ = wopt.solve(k, at, True) - lo_local, _ = P.MOMENT.moment(dict(Counter({r: n * calls for r, n in local.items()})), M, W, at, True) - return lo_local + Q(T * tot5, 5 * SHIFT * M * W), plan - rows, windowfree_H = {}, {} for k in range(0, a.kmax + 1): need(w8_vacuous(k), 'width-8 Hall conditions vacuous k=%d' % k) @@ -267,7 +274,7 @@ def lower_bound(k, local, at): cwf, Hwf = price(local, windowfree_idle(k)) windowfree_H[(k, name)] = Hwf nxt = c + Q(1, 10 ** 24) - lb, plan_n = lower_bound(k, local, nxt) + lb, plan_n = certificate_bound(k, local, nxt, calls, W) need(lb > 1, 'certificate k=%d %s' % (k, name)) lo_full, _ = P.MOMENT.moment(dict(H), M, W, nxt, True) need(abs(lb - lo_full) < Q(1, 10 ** 50), 'tight certificate k=%d %s' % (k, name)) @@ -314,12 +321,15 @@ def lower_bound(k, local, at): bound = Q(r['certified_bound']) priced[key] = dict(local=P.dec(Q(case['optimal']['lower']), 22), pooled32=P.dec(Q(case['pooled32']['lower']), 22), certified_bound=r['certified_bound'], - unreachable=k > 0 and Q(case['optimal']['lower']) >= bound and Q(case['pooled32']['lower']) >= bound) - need(all(v['unreachable'] for key, v in priced.items() if not key.startswith('k0_')), '#1281 priced rows unreachable under windows') + local_above_bound=Q(case['optimal']['lower']) >= bound, + pooled32_above_per_replica_bound=Q(case['pooled32']['lower']) >= bound) + need(all(v['local_above_bound'] and v['pooled32_above_per_replica_bound'] for key, v in priced.items() + if not key.startswith('k0_')), '#1281 priced rows above the per-replica bound') local_unreach = sum(rows[str(k)][b]['windowfree_unreachable'] for k in range(1, a.kmax + 1) for b in ('optimistic', 'pessimistic')) need(local_unreach == 2 * a.kmax, '#1281 local rows unreachable under windows') out['pr1281'] = dict(PR1281, idle_optima_matched=sum(c['k'] <= a.kmax for c in e1281['cases']), priced_cases=priced, - local_rows_unreachable='%d of %d (both brackets, k = 1..%d)' % (local_unreach, 2 * a.kmax, a.kmax)) + local_rows_unreachable='%d of %d priced here (both brackets, k = 1..%d; %d priced by #1281)' % ( + local_unreach, 2 * a.kmax, a.kmax, sum(1 for x in priced if not x.startswith('k0_')))) # #1023's all-width-7 optimum stays window-feasible feasible = [] diff --git a/research/bit589-width7-windows-seed72/windows.py b/research/bit589-width7-windows-seed72/windows.py index 9d957615cd..7ea9484488 100644 --- a/research/bit589-width7-windows-seed72/windows.py +++ b/research/bit589-width7-windows-seed72/windows.py @@ -1,13 +1,17 @@ # SPDX-License-Identifier: Apache-2.0 -"""The PR442/PR463 hosting windows of the nine-stage PR589 bit template, rebuilt independently. +"""The PR442 hosting windows of the nine-stage PR589 bit template. The idle schedule follows global_k.py's recipe (K = 4 bank pairs, L = 9 stages): a local cover sweep -per stage, the idle children it inserts, and the bridges. A child's window is the set of stages whose -sweep falls strictly after the child's pair was last touched and before the child is inserted, on -another pair. The result is cross-checked against BOTH vendored predicates (PR442 -hosting_core.windows and the hosted audit's audit_hosted_k.windows) and against the frozen PR589 -hosting selection. Standard library only. +per stage, the idle children it inserts, and the bridges. schedule() writes it out here; at run time +it is compared event by event with the schedule that the pinned global_k.py itself produces (its +recipe() and its idle-insertion rule, extracted from the file with ast and replayed, asserts +included). A child's window is the set of stages whose sweep falls strictly after the child's pair +was last touched and before the child is inserted, on another pair. Three implementations of that +predicate (this one, PR442 hosting_core.windows and audit_hosted_k.windows) are run on the one +shared schedule and must agree; the frozen PR589 hosting selection must lie inside the windows. +Standard library only. """ +import ast import importlib.util import json from pathlib import Path @@ -17,6 +21,7 @@ HOSTING_CORE = VENDOR / 'idle-axis-hosting/hosting_core.py' AUDIT_HOSTED = VENDOR / 'e8-r715-eleven-stage-whole/code/audit_hosted_k.py' SELECTION = ROOT / 'research/e8-bit-p111-tuned/data/selection9-p111.json' +GLOBAL_K = VENDOR / 'e8-r715-eleven-stage-whole/code/global_k.py' K, L = 4, 9 @@ -63,6 +68,40 @@ def schedule(): return sched +def global_k_schedule(k=K): + """The schedule produced by the pinned global_k.py: its recipe(K) and the idle-insertion if-block of + its main loop, both extracted with ast and executed (the scalar replay around them is not needed).""" + tree = ast.parse(GLOBAL_K.read_text()) + recipe_fn = [n for n in tree.body if isinstance(n, ast.FunctionDef) and n.name == 'recipe'] + rules = [n for n in ast.walk(tree) if isinstance(n, ast.If) and ast.unparse(n.test) == 's % 2 == 1 and s <= 2 * K - 3'] + if len(recipe_fn) != 1 or len(rules) != 1: + raise ValueError('global_k.py: recipe() or the idle-insertion rule not found exactly once') + ns = {} + exec(compile(ast.Module(body=recipe_fn, type_ignores=[]), str(GLOBAL_K), 'exec'), ns) + rule = compile(ast.Module(body=rules, type_ignores=[]), str(GLOBAL_K), 'exec') + levels, sched = [-1] * k, [] + for e in ns['recipe'](k): + if e['kind'] == 'local': + s, p = e['stage'], e['pair'] + if levels[p] != s - 1: + raise ValueError('global_k.py: stage order') + levels[p] = s + sched.append(dict(kind='local_cover_sweep', **{x: v for x, v in e.items() if x != 'kind'})) + exec(rule, dict(s=s, K=k, levels=levels, schedule=sched)) + elif e['kind'] == 'bridge': + if levels[e['dst']] != levels[e['src']]: + raise ValueError('global_k.py: bridge levels') + sched.append(e) + else: + sched.append(e) + return sched + + +def _events(sched): + keys = dict(local_cover_sweep=('stage', 'pair'), idle=('pair', 'rank'), bridge=('dst', 'src'), exchange=()) + return [(e['kind'],) + tuple(e[x] for x in keys[e['kind']]) for e in sched] + + def windows(sched): out, last, seen = {}, {}, [] for pos, e in enumerate(sched): @@ -76,9 +115,12 @@ def windows(sched): return out -def checked_windows(): - """{child: (capacity, stages)} for the children that can host, after the three-way cross-check.""" - sched = schedule() +def checked_windows(sched=None): + """{child: (capacity, stages)} for the children that can host, after the schedule is matched with + global_k.py and the three window predicates agree on it.""" + sched = schedule() if sched is None else sched + if _events(sched) != _events(global_k_schedule()): + raise ValueError('schedule differs from the one global_k.py produces') mine = windows(sched) hc = _load('pr442_hosting_core', HOSTING_CORE) ah = _load('audit_hosted_k', AUDIT_HOSTED) From a60329f06f62b3f193ee03574ce00ed940f5c399 Mon Sep 17 00:00:00 2001 From: Sagar Thakrar Date: Wed, 14 Oct 2026 14:33:37 +0530 Subject: [PATCH 3/4] Close recheck gaps: field-level anchor controls, exposed placement, wording - windows.py: three_way() split out; exchange-level check added; docstring says recipe() and the idle block are executed inside a transcribed loop. - verify.py: build() can return the checked slot list; bind() skips malformed checkpoint records. - test_package.py (14 tests): six single-field schedule mutations rejected; the unanchored three-way path accepts a dropped bridge (widened windows); k = 1 bound recomputed against #1281's own values; record binding and the explicit k = 1 slot list. - README/TASK/VERIFY: PR1179 contract open in scope_change_reason; open question 1 blocked by a cross-replica DP; open question 3 uses the exposed slot list; PR443 vs PR439 credit corrected. --- .../bit589-width7-windows-seed72/README.md | 23 +++++++---- .../bit589-width7-windows-seed72/TASK.json | 8 ++-- .../bit589-width7-windows-seed72/VERIFY.json | 2 +- .../test_package.py | 39 +++++++++++++++++-- .../bit589-width7-windows-seed72/verify.py | 14 +++++-- .../bit589-width7-windows-seed72/windows.py | 31 +++++++++------ 6 files changed, 87 insertions(+), 30 deletions(-) diff --git a/research/bit589-width7-windows-seed72/README.md b/research/bit589-width7-windows-seed72/README.md index cd57f5bba2..2ab40019bc 100644 --- a/research/bit589-width7-windows-seed72/README.md +++ b/research/bit589-width7-windows-seed72/README.md @@ -22,12 +22,16 @@ This package settles one part of that question: **per-replica hosting on the fro [windows.py](windows.py) writes out the nine-stage idle schedule (K = 4, L = 9) and checks it two ways. -1. **It matches `global_k.py`.** At run time the schedule is compared, event by event, with the schedule the pinned `global_k.py` itself produces. Its `recipe()` and its idle-insertion rule are extracted from the file with `ast` and replayed, asserts included. +1. **It matches `global_k.py`.** At run time the schedule is compared, event by event and field by field, with a reference schedule built from the pinned `global_k.py`. + - `global_k.py`'s own `recipe()` and its idle-insertion `if` block are extracted with `ast` and executed, with their asserts. + - They run inside a transcription of the surrounding loop of `global_k.main()`: the level bookkeeping, the event appends, and the stage-order, bridge-level and exchange checks. 2. **Three window predicates agree.** This code, PR442's `hosting_core.windows`, and `audit_hosted_k.windows` (which enforces `s in W[i]` for every hosted slot) give identical windows on that one shared schedule. All 14 frozen `selection9-p111` entries lie inside their windows. -The selection hosts nothing in children 1, 3 and 5. So the decisive singleton windows rest on the `global_k.py` match: a test drops one bridge from the schedule, and the check rejects it. On such a mutated schedule the three predicates would still agree with each other, while the capacity-7 windows widen. +The selection hosts nothing in children 1, 3 and 5. So the decisive singleton windows rest on the `global_k.py` match. +- A test drops one bridge from the schedule. The three predicates still agree with each other on that schedule, while child 1's window widens to stages 0–2; the anchor rejects it. +- Further tests mutate single fields (an idle rank or pair, a sweep's stage or pair, a bridge end), and the anchor rejects each one. | Idle child | 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | |---|---|---|---|---|---|---|---|---|---| @@ -40,7 +44,7 @@ The selection hosts nothing in children 1, 3 and 5. So the decisive singleton wi For every k = 0..74, `verify.py` computes the **exact window-respecting optimum** and does three things: -- **Builds and checks an explicit residual-level placement at run time** (`verify.build`). Every slot is checked for its window, its width and its offset; cells must be disjoint; and every (stage, helper) must be hosted exactly once. RESULT.json records the placement's per-replica idle histogram and its width-7 distribution. The slot list itself is regenerated by `build()`. +- **Builds and checks an explicit residual-level placement at run time** (`verify.build`). Every slot is checked for its window, its width and its offset; cells must be disjoint; and every (stage, helper) must be hosted exactly once. RESULT.json records the placement's per-replica idle histogram and its width-7 distribution. `build(k, plan, slots)` returns the checked slot list (child, copy, offset, width, stage, helper); a test rebuilds the k = 1 placement this way. - **Prices the placement's bit endpoint** under both of #1023's local brackets, using the pinned engines and the inherited surcharge. - **Certifies that no window-feasible replica-local placement reaches the next 1e-24 grid point.** The certificate is tight: it equals the engine moment of the explicit histogram to within 1e-50. @@ -111,12 +115,12 @@ These figures hold under #1023's one-unit local pricing, the frozen recipe and r - At a′ = c* + 1e−24, the local moment lower bound plus 32 times the DP bound exceeds 1. - So every replica-local placement, uniform across replicas or not, has an endpoint below a′. This is grid optimality at each row's own endpoint. -## Controls ([test_package.py](test_package.py), 12 tests) +## Controls ([test_package.py](test_package.py), 14 tests) -- **C-W0 (schedule anchor).** The schedule equals the one `global_k.py` produces. Dropping one bridge is rejected. +- **C-W0 (schedule anchor).** The schedule equals the `global_k.py` reference. Dropping one bridge is rejected, as is each of six single-field mutations. - **C-W1.** #1023's k = 1 placement fills 9 capacity-7 copies per replica, one per stage. The windows admit only stages 2, 4 and 6 there, so at least 6 residuals sit outside their window. - **C-W2.** The window-free local rows lie above the certified bound, while the window-respecting endpoints lie below it. -- **C-W3.** #1281's local and pooled32 priced rows (k > 0) lie above the per-replica bound, and all 75 idle profiles match. +- **C-W3.** #1281's local and pooled32 priced rows (k > 0) lie above the per-replica bound, and all 75 idle profiles match. At k = 1 the test recomputes the certificate at the recorded bound and reads #1281's values from its own file. - **C-W4.** The all-width-7 optimum is window-feasible. - **C-W5 (dropped constraint).** Dropping the chain constraint B0 ≤ 2k breaks the brute-force agreement. - **C-W5 (perturbed window).** Widening child 0's window to stages 0–3 breaks the chain structure. @@ -126,6 +130,7 @@ Also covered: - k = 0 reproduces the selected endpoint, and its certificate is recomputed and checked for tightness. - The exhaustive brute-force reduction holds at k = 2. - The width-8 Hall conditions are vacuous. +- The record binding holds, and the explicit k = 1 placement hosts every (stage, helper) inside its window. ## Reproduce @@ -179,6 +184,7 @@ python3.12 scripts/research_package.py --package research/bit589-width7-windows- 1. **Can cross-replica (T16-style) interleaved owner maps lift the one-stage 7-slot windows for the bit supplier?** This is one route to #1281's pooled rows; a changed recipe, split residuals or banks are others. - First step: compute windows on an interleaved bit timeline and rerun the DP. + - Blocked by: a cross-replica DP. `wopt.solve` and the `global_k.py` anchor are specific to this per-replica schedule. 2. **Does another nine-stage recipe widen the capacity-7 windows?** #1487 enumerates recipes for width-8 hosting only. - First step: generalise `wopt`'s two-chain DP to arbitrary interval windows (or use a min-cost-flow bound), then apply it to #1487's hostable recipes. - Blocked by: the generalised DP. `wopt.solve` currently asserts this recipe's chain structure. @@ -191,7 +197,8 @@ python3.12 scripts/research_package.py --package research/bit589-width7-windows- - #1281: mightyOil (Philipp), with OpenAI Codex GPT-6 Astra assistance. - PR442: DaysSky, the hosting windows. - PR444: chafreaky, the ownership/window audit that `audit_hosted_k` extends. -- PR439 and PR443: chafreaky, the recipe that `global_k.py` generalises. +- PR443: chafreaky, the `global_kernel.py` recipe that `global_k.py` generalises. +- PR439: chafreaky, the explicit residual bank routes. - PR386 and PR436: Zhihao Chen and eumemic, the global identity and template. - PR463, PR510 and PR589: DreamingOfClouds, the hosted audit and the bit supplier. - PR555: eumemic. @@ -205,4 +212,4 @@ python3.12 scripts/research_package.py --package research/bit589-width7-windows- - #1307: commdata2338. - The retained moment-engine authors. -Prepared by Sagar Thakrar (thakrarsagar) with substantial AI assistance from Claude (Anthropic) via Claude Code. Parallel read-only scout and judge subagents found the window obstruction. A post-PR adversarial review found the overclaims and the missing schedule anchor fixed in the second commit. New material is Apache-2.0. +Prepared by Sagar Thakrar (thakrarsagar) with substantial AI assistance from Claude (Anthropic) via Claude Code. Parallel read-only scout and judge subagents found the window obstruction. A post-PR adversarial review found overclaims and the missing schedule anchor, which the second commit fixes. A recheck found smaller gaps, which the third commit closes. New material is Apache-2.0. diff --git a/research/bit589-width7-windows-seed72/TASK.json b/research/bit589-width7-windows-seed72/TASK.json index cba3630b0a..c792e7bd9d 100644 --- a/research/bit589-width7-windows-seed72/TASK.json +++ b/research/bit589-width7-windows-seed72/TASK.json @@ -41,12 +41,12 @@ }, "scope_status": "refined", "actual_scope": "One hosting implication for the selected PR589 bit supplier: do the window-free partial width-seven rows of merged #1023 and merged #1281 (width-7 residuals placed in capacity-7 idle slots without time order) survive PR442's replica-local hosting windows (audit_hosted_k: s in W[i] for every hosted slot) on the frozen nine-stage recipe, whole residuals, no banks? Exact window-respecting optimum and certificate for every k = 0..74.", - "scope_change_reason": "The card asks for one exact hosting implication; this narrows it to the time-order hypothesis that #1023 lists as unchecked and that #1281 states as its open question 1. Replica-local hosting only; cross-replica owner maps, projector compatibility, owner inactivity and a physical width-7 helper stay open.", + "scope_change_reason": "The card asks for one exact hosting implication. This narrows it to the time-order hypothesis that #1023 lists as unchecked, and to the per-replica, frozen-recipe part of #1281's open question 1. That question's PR1179 boundary-contract audit and cross-replica pooling stay open, as do projector compatibility, owner inactivity and a physical width-7 helper.", "bottleneck_link": "Side result on the bit supplier; the selected record is complex-bound, so no kappa changes. Under #1023's one-unit local pricing, the frozen recipe and replica-local hosting, it corrects the bit headroom a partial width-seven helper mechanism can buy: the window-respecting optimum keeps 63.6-67.1% (optimistic) or 56.3-60.7% (pessimistic) of the window-free gain, i.e. the published rows overstate it by about 1.5x or 1.7x, roughly flat in k.", "budget_minutes": 180, "stop_rule": "Stop once every k = 0..74 has an explicit window-feasible placement and a tight grid certificate under both local brackets, k = 0 reproduces the selected bit endpoint, and every #1023 and #1281 row is compared; report any row not decided instead of claiming it.", "outcome": "completed", - "evidence": "RESULT.json: the nine-stage idle schedule equals, event by event, the one the pinned global_k.py produces (recipe and idle rule extracted and replayed); three window predicates agree on it; the frozen selection lies inside. Capacity-7 children 1/3/5 admit only stages 2/4/6, so at most 3k of 9k width-7 residuals per replica sit in 7-slots. Exact window-respecting optimum, an explicit placement built and checked at run time, and a tight 1e-24 certificate for every k = 0..74, both brackets; k = 0 reproduces 0.001733427039589844234749. k = 37 optimistic 0.001770809187 (+2.157%) vs window-free 0.001789671631 (+3.245%); k = 74 0.001809907119 (+4.412%) vs 0.001849754238 (+6.711%). Retained fraction 0.636-0.671 (optimistic), 0.563-0.607 (pessimistic). All 8 #1023 partial rows unreachable; #1281's closed-form local optimum transcribed and checked against its 75 idle profiles; all 148 local rows priced here from it (8 also priced by #1281, reproduced exactly in local endpoint and histogram) lie above the per-replica bound, as do #1281's 8 priced pooled32 rows with k > 0. Chain reduction confirmed by max-flow on every distribution (462 at k = 1, 6188 at k = 2). #1023's all-width-7 optimum stays window-feasible (104 sextet splits). 12 tests pass.", + "evidence": "RESULT.json: the nine-stage idle schedule equals, event by event and field by field, the global_k.py reference (its recipe() and idle-insertion block executed via ast inside a transcribed loop); three window predicates agree on it; the frozen selection lies inside. Capacity-7 children 1/3/5 admit only stages 2/4/6, so at most 3k of 9k width-7 residuals per replica sit in 7-slots. Exact window-respecting optimum, an explicit placement built and checked at run time, and a tight 1e-24 certificate for every k = 0..74, both brackets; k = 0 reproduces 0.001733427039589844234749. k = 37 optimistic 0.001770809187 (+2.157%) vs window-free 0.001789671631 (+3.245%); k = 74 0.001809907119 (+4.412%) vs 0.001849754238 (+6.711%). Retained fraction 0.636-0.671 (optimistic), 0.563-0.607 (pessimistic). All 8 #1023 partial rows unreachable; #1281's closed-form local optimum transcribed and checked against its 75 idle profiles; all 148 local rows priced here from it (8 also priced by #1281, reproduced exactly in local endpoint and histogram) lie above the per-replica bound, as do #1281's 8 priced pooled32 rows with k > 0. Chain reduction confirmed by max-flow on every distribution (462 at k = 1, 6188 at k = 2). #1023's all-width-7 optimum stays window-feasible (104 sextet splits). 14 tests pass.", "author": "Sagar Thakrar (thakrarsagar)", "ai_assistance": "Substantial: Claude (Anthropic) via Claude Code. Parallel read-only scout and judge subagents proposed and ranked audit candidates and found the window obstruction; the DP, placement builder and certificates were written with Claude and checked by the controls in test_package.py. A post-PR adversarial review (three reviewers and a verifier) found overclaims and the missing schedule anchor, fixed in the second commit.", "open_questions": [ @@ -54,7 +54,7 @@ "question": "Can cross-replica (T16-style) interleaved owner maps lift the one-stage capacity-7 windows for the bit supplier?", "why_it_matters": "One route (others: a changed recipe, split residuals, banks) to #1281's pooled rows or the window-free local rows; replica-local hosting on the frozen recipe is ruled out here.", "first_step": "Compute windows on an interleaved bit timeline with owner_replica != replica and rerun the DP.", - "blocked_by": "An interleaved bit timeline; the selected T16 maps are complex-side." + "blocked_by": "An interleaved bit timeline (the selected T16 maps are complex-side) and a cross-replica DP; wopt.solve and the global_k.py anchor are specific to this per-replica schedule." }, { "question": "Does another nine-stage stage recipe widen the capacity-7 windows?", @@ -65,7 +65,7 @@ { "question": "Do the window-respecting placements pass projector compatibility (#1307) for mixed-width slots?", "why_it_matters": "Windows are necessary, not sufficient; slots that split q-perp lie outside #1307's completion-free argument.", - "first_step": "Regenerate the k = 1 placement with verify.build and run #1307's projector check on it.", + "first_step": "Rebuild the k = 1 placement with verify.build(1, plan, slots) and run #1307's projector check on the returned slot list.", "blocked_by": "None." } ] diff --git a/research/bit589-width7-windows-seed72/VERIFY.json b/research/bit589-width7-windows-seed72/VERIFY.json index 66ebec981f..5899054462 100644 --- a/research/bit589-width7-windows-seed72/VERIFY.json +++ b/research/bit589-width7-windows-seed72/VERIFY.json @@ -44,7 +44,7 @@ "test_package.py" ], "timeout_seconds": 300, - "checks": "Capacity-7 windows; schedule = global_k.py's and a dropped bridge is caught; #1023's k = 1 placement outside its windows; k = 0 endpoint and a recomputed tight certificate; window-free rows above and window-respecting rows below the bound; #1281 local and pooled32 rows; all-width-7 feasibility; exhaustive brute-force reduction (6188 distributions at k = 2); dropped chain constraint and perturbed window controls; width-8 Hall vacuity." + "checks": "Capacity-7 windows; schedule = global_k.py reference, with a dropped bridge and six single-field mutations rejected (and the unanchored three-way path shown to accept the dropped bridge); #1023's k = 1 placement outside its windows; k = 0 endpoint and a recomputed tight certificate; window-free rows above and window-respecting rows below the bound; #1281 local and pooled32 rows, with the k = 1 bound recomputed; all-width-7 feasibility; exhaustive brute-force reduction (6188 distributions at k = 2); dropped chain constraint and perturbed window controls; width-8 Hall vacuity; record binding and the explicit k = 1 slot list." } ] } diff --git a/research/bit589-width7-windows-seed72/test_package.py b/research/bit589-width7-windows-seed72/test_package.py index 0a0917ef6a..67470f7004 100644 --- a/research/bit589-width7-windows-seed72/test_package.py +++ b/research/bit589-width7-windows-seed72/test_package.py @@ -39,11 +39,24 @@ def test_schedule_matches_global_k_and_a_dropped_bridge_is_caught(self): mutated = sched[:first_bridge] + sched[first_bridge + 1:] with self.assertRaisesRegex(ValueError, 'global_k.py'): windows.checked_windows(mutated) - # without the anchor, the three predicates would still agree on the mutated schedule - # while the capacity-7 windows widen, which is why the anchor is needed - widened = {i: st for i, (p, r, st) in windows.windows(mutated).items() if r == 7} + # without the anchor the three predicates still agree on the mutated schedule, while the + # capacity-7 windows widen: the anchor is what pins the singleton windows + widened = {i: st for i, (p, r, st) in windows.three_way(mutated).items() if r == 7} + self.assertEqual(widened[1], (0, 1, 2)) self.assertNotEqual(widened, {1: (2,), 3: (4,), 5: (6,)}) + def test_anchor_compares_every_field(self): + base = windows.schedule() + idle = [n for n, e in enumerate(base) if e['kind'] == 'idle'] + local = [n for n, e in enumerate(base) if e['kind'] == 'local_cover_sweep'] + bridge = [n for n, e in enumerate(base) if e['kind'] == 'bridge'] + for n, field, value in ((idle[1], 'rank', 14), (idle[1], 'pair', 0), (local[3], 'pair', 2), + (local[3], 'stage', 4), (bridge[0], 'dst', 2), (bridge[0], 'src', 0)): + mutated = copy.deepcopy(base) + mutated[n][field] = value + with self.assertRaisesRegex(ValueError, 'global_k.py', msg=(n, field, value)): + windows.checked_windows(mutated) + def test_cw1_window_free_k1_uses_nine_seven_slots(self): # #1023's partial placement (packing.width7_partial_idle) fills 9 capacity-7 copies per replica # with one width-7 residual from each of the 9 stages; the vendored windows admit only stages @@ -85,6 +98,26 @@ def test_cw3_pr1281_local_and_pooled_rows_exceed_the_per_replica_bound(self): if key != 'k0_optimistic': self.assertTrue(row['local_above_bound'] and row['pooled32_above_per_replica_bound'], key) self.assertEqual(RESULT['pr1281']['idle_optima_matched'], 75) + # recompute one bound independently of RESULT's flags: at k = 1 (optimistic) the certificate holds + # at the recorded bound, and #1281's published local and pooled32 values (read from its file) lie above it + record = wopt.P.pinned_json('bit_record') + model = wopt.P.slot_model(record, wopt.P.pinned_json('selection')) + local, _ = wopt.P.local_bracket(model['local'], 1) + bound = Q(RESULT['rows']['1']['optimistic']['certified_bound']) + lb, _ = V.certificate_bound(1, local, bound, model['calls'], record['nine']['bit']['live']) + self.assertGreater(lb, 1) + e1281 = json.loads((wopt.ROOT / V.PR1281['path']).read_text())['priced_cases']['k1_optimistic'] + self.assertGreaterEqual(Q(e1281['optimal']['lower']), bound) + self.assertGreaterEqual(Q(e1281['pooled32']['lower']), bound) + + def test_record_binding_and_explicit_k1_placement(self): + self.assertEqual(V.bind()['assembly'], V.ASSEMBLY) + _, _, plan, _ = wopt.solve(1, Q(1, 570), True) + slots = [] + idle = V.build(1, plan, slots) + self.assertEqual(len(slots), 9 * wopt.R) # every (stage, helper) once + self.assertTrue(all(s in wopt.WIN[i][1] for i, cp, off, w, s, h in slots)) + self.assertEqual({str(r): n for r, n in sorted(idle.items())}, RESULT['rows']['1']['idle']) def test_pr1023_partial_rows_all_unreachable(self): rows = RESULT['pr1023_partial_rows'] diff --git a/research/bit589-width7-windows-seed72/verify.py b/research/bit589-width7-windows-seed72/verify.py index 75b33acf8c..7f79a47146 100644 --- a/research/bit589-width7-windows-seed72/verify.py +++ b/research/bit589-width7-windows-seed72/verify.py @@ -52,7 +52,11 @@ def bind(): records = [P.ROOT / 'certificates/selected-result.json'] + sorted((P.ROOT / 'certificates/checkpoints').glob('*.json')) named = False for f in records: - rec = json.loads(f.read_text()) if f.is_file() else {} + try: + rec = json.loads(f.read_text()) if f.is_file() else {} + except ValueError: + rec = {} + rec = rec if isinstance(rec, dict) else {} named = named or (rec.get('certificate') == ASSEMBLY and rec.get('certificate_sha256') == P.sha256(raw)) need(named, 'a selected or checkpoint record names the frontier1094 certificate') asm = json.loads(raw) @@ -151,8 +155,10 @@ def brute_force_reduction(k): return count, agree -def build(k, plan): - """Explicit per-replica hosting from the DP plan, verified in the audit_hosted_k style.""" +def build(k, plan, slots_out=None): + """Explicit per-replica hosting from the DP plan, verified in the audit_hosted_k style. Returns the idle + remainder histogram; if slots_out is a list, the checked slots (child, copy, offset, width, stage, + helper) are appended to it.""" copies = {i: [] for i in WIN} for i in WIN: for (l, b, r) in plan['copies'][i]: @@ -197,6 +203,8 @@ def build(k, plan): need((s, h) not in hosted, 'hosted once') hosted.add((s, h)) need(hosted == {(s, h) for s in range(STG) for h in range(R)}, 'every (stage, helper) hosted') + if slots_out is not None: + slots_out.extend(slots) for i in WIN: for cp in range(N): r = CAP[i] - len(used.get((i, cp), ())) diff --git a/research/bit589-width7-windows-seed72/windows.py b/research/bit589-width7-windows-seed72/windows.py index 7ea9484488..4bb4f075ad 100644 --- a/research/bit589-width7-windows-seed72/windows.py +++ b/research/bit589-width7-windows-seed72/windows.py @@ -3,9 +3,10 @@ The idle schedule follows global_k.py's recipe (K = 4 bank pairs, L = 9 stages): a local cover sweep per stage, the idle children it inserts, and the bridges. schedule() writes it out here; at run time -it is compared event by event with the schedule that the pinned global_k.py itself produces (its -recipe() and its idle-insertion rule, extracted from the file with ast and replayed, asserts -included). A child's window is the set of stages whose sweep falls strictly after the child's pair +it is compared event by event with the schedule obtained by executing the pinned global_k.py's own +recipe() and its idle-insertion if-block (extracted with ast, their asserts included) inside a +transcription of the surrounding loop of global_k.main() (level bookkeeping, the sweep, bridge and +exchange appends, and its stage-order, bridge-level and exchange checks). A child's window is the set of stages whose sweep falls strictly after the child's pair was last touched and before the child is inserted, on another pair. Three implementations of that predicate (this one, PR442 hosting_core.windows and audit_hosted_k.windows) are run on the one shared schedule and must agree; the frozen PR589 hosting selection must lie inside the windows. @@ -69,8 +70,8 @@ def schedule(): def global_k_schedule(k=K): - """The schedule produced by the pinned global_k.py: its recipe(K) and the idle-insertion if-block of - its main loop, both extracted with ast and executed (the scalar replay around them is not needed).""" + """global_k.py's schedule: its recipe(K) and the idle-insertion if-block of main(), both extracted with + ast and executed, inside a transcription of the surrounding loop (the scalar replay is not needed).""" tree = ast.parse(GLOBAL_K.read_text()) recipe_fn = [n for n in tree.body if isinstance(n, ast.FunctionDef) and n.name == 'recipe'] rules = [n for n in ast.walk(tree) if isinstance(n, ast.If) and ast.unparse(n.test) == 's % 2 == 1 and s <= 2 * K - 3'] @@ -93,6 +94,8 @@ def global_k_schedule(k=K): raise ValueError('global_k.py: bridge levels') sched.append(e) else: + if levels != [2 * k] * k: + raise ValueError('global_k.py: exchange levels') sched.append(e) return sched @@ -115,12 +118,8 @@ def windows(sched): return out -def checked_windows(sched=None): - """{child: (capacity, stages)} for the children that can host, after the schedule is matched with - global_k.py and the three window predicates agree on it.""" - sched = schedule() if sched is None else sched - if _events(sched) != _events(global_k_schedule()): - raise ValueError('schedule differs from the one global_k.py produces') +def three_way(sched): + """The windows of `sched` after checking that the three predicates agree on it (no anchor).""" mine = windows(sched) hc = _load('pr442_hosting_core', HOSTING_CORE) ah = _load('audit_hosted_k', AUDIT_HOSTED) @@ -130,6 +129,16 @@ def checked_windows(sched=None): audit = {i: (pair[i], rank[i], tuple(sorted(W[i]))) for i in W} if not (mine == theirs == audit): raise ValueError('window predicates disagree') + return mine + + +def checked_windows(sched=None): + """{child: (capacity, stages)} for the children that can host, after the schedule is matched with + global_k.py and the three window predicates agree on it.""" + sched = schedule() if sched is None else sched + if _events(sched) != _events(global_k_schedule()): + raise ValueError('schedule differs from the one global_k.py produces') + mine = three_way(sched) win = {i: (r, st) for i, (p, r, st) in mine.items() if r > 0 and st} for i, w, s, n in json.loads(SELECTION.read_text())['bit']['stages']: if s not in win[i][1]: From b4fd72163234c164d9a05f2f7dac9c57dcd7fb66 Mon Sep 17 00:00:00 2001 From: Sagar Thakrar Date: Wed, 14 Oct 2026 15:18:51 +0530 Subject: [PATCH 4/4] README: registered python3.12 replay passes (80 s on an unloaded host) --- research/bit589-width7-windows-seed72/README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/research/bit589-width7-windows-seed72/README.md b/research/bit589-width7-windows-seed72/README.md index 2ab40019bc..a61e23fb47 100644 --- a/research/bit589-width7-windows-seed72/README.md +++ b/research/bit589-width7-windows-seed72/README.md @@ -143,7 +143,7 @@ python3.12 scripts/research_package.py --package research/bit589-width7-windows- - **Requirements.** Standard-library Python 3.10 or later. The pinned engines, record and slot model come from merged #1023's `packing.py`, which is imported read-only. `verify.py --kmax K` runs a partial check (`PASS_PARTIAL`). - **Where it was run.** `verify.py` and the tests pass on Python 3.12.15 and 3.14.8 (macOS 26.5, arm64). `--check-only` passes. -- **Registered replay.** The python3.12 replay was run locally. It exceeded its 600 s wall-clock limit only because the host was heavily loaded (load average about 100). `verify.py` itself needs about 140 s of CPU. +- **Registered replay.** The python3.12 replay passes (`PASS_REGISTERED_RESEARCH_PACKAGE`, 80 s of wall time on an unloaded host). An earlier attempt timed out at 600 s only because the host was heavily loaded (load average about 100). `verify.py` itself needs about 140 s of CPU. ## Scope and remaining obligations