diff --git a/research/bit589-width7-windows-seed72/README.md b/research/bit589-width7-windows-seed72/README.md new file mode 100644 index 0000000000..a61e23fb47 --- /dev/null +++ b/research/bit589-width7-windows-seed72/README.md @@ -0,0 +1,215 @@ +# Audit: PR442 hosting windows and the partial width-seven rows of #1023 and #1281 + +**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: 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 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) 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 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. 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 | +|---|---|---|---|---|---|---|---|---|---| +| 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, `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. `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. + +k = 0 reproduces the selected bit endpoint 0.001733427039589844234749. + +Selected rows, with the gain over the selected bit endpoint: + +| 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 | +| 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 | + +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. + - 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: 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), 14 tests) + +- **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. 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. + +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. +- The record binding holds, and the explicit k = 1 placement hosts every (stage, helper) inside its window. + +## Reproduce + +```sh +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 +``` + +- **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 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 + +- **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. + - Owner inactivity is still open. + - 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. +- **Uniqueness.** Histograms are not shown to be unique; ties exist, for example at k = 2. +- **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?** 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. +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. +- PR442: DaysSky, the hosting windows. +- PR444: chafreaky, the ownership/window audit that `audit_hosted_k` extends. +- 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. +- 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 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/RESULT.json b/research/bit589-width7-windows-seed72/RESULT.json new file mode 100644 index 0000000000..7050ee6dd7 --- /dev/null +++ b/research/bit589-width7-windows-seed72/RESULT.json @@ -0,0 +1,4889 @@ +{ + "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", + "named_by": "certificates/selected-result.json or certificates/checkpoints/*.json" + }, + "capacity7_children": { + "1": [ + 2 + ], + "3": [ + 4 + ], + "5": [ + 6 + ] + }, + "chain_reduction_brute_force": { + "agree": "all", + "distributions_checked": { + "1": 462, + "2": 6188 + } + }, + "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 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", + "pooled32_above_per_replica_bound": false + }, + "k1_optimistic": { + "certified_bound": "1734347102923006399613/1000000000000000000000000", + "local": "0.001734846264120199151475", + "local_above_bound": true, + "pooled32": "0.001734900431583947157341", + "pooled32_above_per_replica_bound": true + }, + "k1_pessimistic": { + "certified_bound": "108381532739553010717/62500000000000000000000", + "local": "0.001734603545275303824122", + "local_above_bound": true, + "pooled32": "0.001734657697586404233802", + "pooled32_above_per_replica_bound": true + }, + "k2_optimistic": { + "certified_bound": "1388217536169998549/800000000000000000000", + "local": "0.001736327170598942735353", + "local_above_bound": true, + "pooled32": "0.0017363781660342837852", + "pooled32_above_per_replica_bound": true + }, + "k2_pessimistic": { + "certified_bound": "216848289009341626869/125000000000000000000000", + "local": "0.0017358409713034135953", + "local_above_bound": true, + "pooled32": "0.001735891938199934503774", + "pooled32_above_per_replica_bound": true + }, + "k37_optimistic": { + "certified_bound": "1770809187427053553943/1000000000000000000000000", + "local": "0.001789671631346367026824", + "local_above_bound": true, + "pooled32": "0.001789725802593008582027", + "pooled32_above_per_replica_bound": true + }, + "k37_pessimistic": { + "certified_bound": "1761884716885951335477/1000000000000000000000000", + "local": "0.001780556367920637129218", + "local_above_bound": true, + "pooled32": "0.001780609989052611495117", + "pooled32_above_per_replica_bound": true + }, + "k74_optimistic": { + "certified_bound": "904953559530015237129/500000000000000000000000", + "local": "0.00184975423837042835336", + "local_above_bound": true, + "pooled32": "0.001849803954130003404634", + "pooled32_above_per_replica_bound": true + }, + "k74_pessimistic": { + "certified_bound": "56005875337664138131/31250000000000000000000", + "local": "0.001831249661111873873002", + "local_above_bound": true, + "pooled32": "0.001831298387323686469848", + "pooled32_above_per_replica_bound": 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..2d84eb3a01 --- /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": "input", + "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..c792e7bd9d --- /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 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 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 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": [ + { + "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) 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?", + "why_it_matters": "The obstruction is recipe-specific; open #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 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": "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 new file mode 100644 index 0000000000..5899054462 --- /dev/null +++ b/research/bit589-width7-windows-seed72/VERIFY.json @@ -0,0 +1,50 @@ +{ + "schema_version": 1, + "status": "ready", + "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", + "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/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", + "research/native-complex-moment552/engines/outer.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 600, + "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": [ + "{python}", + "-I", + "-B", + "-m", + "unittest", + "discover", + "-s", + "{package}", + "-p", + "test_package.py" + ], + "timeout_seconds": 300, + "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 new file mode 100644 index 0000000000..67470f7004 --- /dev/null +++ b/research/bit589-width7-windows-seed72/test_package.py @@ -0,0 +1,170 @@ +# 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()) + + +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) + 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_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 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 + # 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'] + 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'): + 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['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'] + 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), (6188, 6188)) # every composition of 12 into six parts + + 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..7f79a47146 --- /dev/null +++ b/research/bit589-width7-windows-seed72/verify.py @@ -0,0 +1,371 @@ +#!/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 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; 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). #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 +""" +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') + + +ASSEMBLY = 'research/community-frontier1094-audit/ASSEMBLY.json' + + +def bind(): + """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() + records = [P.ROOT / 'certificates/selected-result.json'] + sorted((P.ROOT / 'certificates/checkpoints').glob('*.json')) + named = False + for f in records: + 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) + 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(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): + 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 (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 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) + return count, agree + + +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]: + 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') + 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), ())) + if r: + rem[r] += 1 + 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, 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}) + 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 + + 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 = 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)) + 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'], + 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 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 = [] + 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..4bb4f075ad --- /dev/null +++ b/research/bit589-width7-windows-seed72/windows.py @@ -0,0 +1,146 @@ +# SPDX-License-Identifier: Apache-2.0 +"""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. schedule() writes it out here; at run time +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. +Standard library only. +""" +import ast +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' +GLOBAL_K = VENDOR / 'e8-r715-eleven-stage-whole/code/global_k.py' +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 global_k_schedule(k=K): + """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'] + 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: + if levels != [2 * k] * k: + raise ValueError('global_k.py: exchange levels') + 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): + 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 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) + 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') + 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]: + 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 +