diff --git a/research/ideal-lever-grid-budgets/README.md b/research/ideal-lever-grid-budgets/README.md new file mode 100644 index 0000000000..134a406601 --- /dev/null +++ b/research/ideal-lever-grid-budgets/README.md @@ -0,0 +1,190 @@ +# Ideal combined-lever budget grid for the selected complex local word + +**Planning/screening table inside the retained ceiling model. No new κ; the selected +record is unchanged (`certificates/selected-result.json` stays at +κ = 0.001672660197076918).** No supplier admission, no frontier change, and no +statement about any real construction: every cell is a favorable relaxation that +omits the cost of realizing its levers (the same caveat as the published +one-at-a-time lever rows). + +## What this package computes + +`research/complex-local-word-ceiling/levers.py` prices seven one-at-a-time lever +rows; `docs/research/current-priorities.md` records one combined row (centre free + +rank-16, ×6.51). This package runs the **full 3 × 4 × 2 grid** of the three +published lever families through the parent exact-rational `ceiling()` at grid 1e-12, +under unchanged parent premises: `m = 73`, 896 live families over nine stages +(`w = 896/9`), outer halving guard `R = 51`, fractional idle remainder at rank `R`, +paid centre charge in PR1012's coverage identity. + +* centre charge: `selected` (C = 64, eight rank-8 centre copies), `shared` + (C = 32, four copies), `free` (C = 0, copies removed); +* local shape: the published word `{1:2412, 2:418, 3:432, 4:142, 5:82, 8:8}` + (mass 5,586), or all paid local mass delivered as (fractional) children of rank + 8, 16 or 32. `selected` rows reshape the whole mass (as the published rank-8/16 + rows do); `shared`/`free` rows reshape the non-centre mass 5,522 and keep or drop + the retained rank-8 copies; +* unpaid coordinates per live family: 1 (current coverage law) or 2 (the recorded + what-if changed coverage law). + +## Results (exact rational brackets in `RESULT.json`; decimals rounded) + +| centre | local shape | unpaid u | a cap | × baseline | κ cap = a/(1+a) | κ ≥ 1/99? | +|---|---|---:|---:|---:|---:|---| +| selected (C=64) | published word | 1 | 0.001690054 | x1.000 | 0.001687203 | no | +| selected (C=64) | published word | 2 | 0.006377984 | x3.774 | 0.006337563 | no | +| selected (C=64) | all mass -> rank 8 | 1 | 0.002739504 | x1.621 | 0.002732020 | no | +| selected (C=64) | all mass -> rank 8 | 2 | **0.010354258** | x6.127 | **0.010248146** | **yes** | +| selected (C=64) | all mass -> rank 16 | 1 | 0.003909456 | x2.313 | 0.003894232 | no | +| selected (C=64) | all mass -> rank 16 | 2 | 0.014797223 | x8.755 | 0.014581458 | yes | +| selected (C=64) | all mass -> rank 32 | 1 | 0.006823270 | x4.037 | 0.006777028 | no | +| selected (C=64) | all mass -> rank 32 | 2 | 0.025914724 | x15.334 | 0.025260115 | yes | +| shared (C=32) | published word | 1 | 0.003212973 | x1.901 | 0.003202683 | no | +| shared (C=32) | published word | 2 | 0.007893112 | x4.670 | 0.007831299 | no | +| shared (C=32) | all mass -> rank 8 | 1 | 0.005219872 | x3.089 | 0.005192767 | no | +| shared (C=32) | all mass -> rank 8 | 2 | 0.012842951 | x7.599 | 0.012680101 | yes | +| shared (C=32) | all mass -> rank 16 | 1 | 0.007430577 | x4.397 | 0.007375771 | no | +| shared (C=32) | all mass -> rank 16 | 2 | 0.018307802 | x10.833 | 0.017978652 | yes | +| shared (C=32) | all mass -> rank 32 | 1 | 0.012887708 | x7.626 | 0.012723728 | yes | +| shared (C=32) | all mass -> rank 32 | 2 | 0.031857575 | x18.850 | 0.030874004 | yes | +| free (C=0) | published word | 1 | 0.004737653 | x2.803 | 0.004715314 | no | +| free (C=0) | published word | 2 | 0.009409964 | x5.568 | 0.009322242 | no | +| free (C=0) | all mass -> rank 8 | 1 | 0.007714442 | x4.565 | 0.007655385 | no | +| free (C=0) | all mass -> rank 8 | 2 | 0.015345904 | x9.080 | 0.015113967 | yes | +| free (C=0) | all mass -> rank 16 | 1 | 0.011008425 | x6.514 | 0.010888560 | yes | +| free (C=0) | all mass -> rank 16 | 2 | 0.021929660 | x12.976 | 0.021459070 | yes | +| free (C=0) | all mass -> rank 32 | 1 | 0.019209068 | x11.366 | 0.018847034 | yes | +| free (C=0) | all mass -> rank 32 | 2 | 0.038398085 | x22.720 | 0.036978194 | yes | + +**Screening verdict (measured here).** Inside this model and these three lever +families, 12 of 24 cells reach the ambitious planning target κ ≥ 1/99 +(≈ 0.010101010). The reaching set is upward closed in the lever lattice +(verified, 0 violations), and its minimal elements are exactly + +* `selected centre + all-mass-rank-8 + u = 2` — κ cap 0.010248146 (+1.46 % over target), +* `shared centre + all-mass-rank-32 + u = 1` — κ cap 0.012723728, +* `free centre + all-mass-rank-16 + u = 1` — κ cap 0.010888560 (the published pair row). + +Notable non-reaches: free centre + published word + u = 2 tops out at 0.009322242 +(7.7 % short), and free centre + rank-8 delivery + u = 1 at 0.007655385 — so within +these families no combination of {centre relief} × {coverage relief} reaches the +target without reshaping the local delivery rank, and coverage relief (u = 2) is the +only single lever that, paired with rank-8 delivery at the full centre charge, +crosses 1/99. The tightest reaching cell sits barely 1.46 % over the target, while +#3811 reports a worst-case joint-integrality loss ≈ 1.35 % in the baseline centre +model — so that row's margin over the target is comparable to the reported integrality +cost and should not be treated as target-clearing under integer counts. + +## Controls (all in `verify.py`, PASS_IDEAL_LEVER_GRID_BUDGETS) + +1. All 24 exact brackets recompute and byte-match `RESULT.json`. +2. Every recorded endpoint certified: `relax(a_lo) < 1 < relax(a_hi)` on outward + rational enclosures (`ceiling.py`, 2^-256 rounding). +3. Profile invariants: idle mass 1,646 at the selected cell (published value); + child ranks in `(0, m)` and `≤ R`; local mass 5,586 / 5,554 / 5,522 for + selected / shared / free centre rows. +4. **Live parent control:** the pinned `levers.py` is executed and its seven + published rows agree with the matching grid cells at printed precision + (`×1.00, ×2.80, ×1.90, ×2.31, ×1.62, ×3.77, ×6.51`; baseline cap + 0.001690054109089). +5. Lever monotonicity across the whole lattice: 0 violations. +6. Fail-closed guards: `R = 52` rejected (halving guard), `unpaid = 0` rejected, + over-weight local profile rejected. +7. Bracket nesting: the 1e-8 brackets contain the 1e-12 brackets for three cells. + +## Scope and limits — read before citing + +* Ideal favorable relaxations for planning: fractional child counts, ideal idle + packing at rank 51, no realization, hosting, restoration, precision or + all-size cost for any lever. A reaching cell means "no packing/shape obstruction + inside this model", **not** feasibility. #3811 shows attained integer optima sit + up to ≈ 1.35 % below the fractional reading in the baseline model. +* Complex side only. The ambitious κ > 1/99 program additionally needs the bit + supplier's effective budget above ≈ 1/99 (see the bottleneck brief); nothing + here addresses the bit side, chronology or interfaces. +* Single fixed local-word family: the four shapes keep the paid mass fixed and + reshape ranks; other coverage laws, port counts, templates or outer recipes are + outside the parent ceiling model and outside this table. +* These are planning numbers under the retained balanced reduction κ < a/(1+a); + the seven-step recipe attains slightly less. No new κ, no supplier, no + selected-frontier change, and no claim that any lever is realizable. + +## Reproduce + +```sh +python3 -I -B research/ideal-lever-grid-budgets/verify.py # ~11 s, PASS_IDEAL_LEVER_GRID_BUDGETS +python3 -I -B research/ideal-lever-grid-budgets/grid.py # ~7 s, prints the table +python3 scripts/research_package.py --package research/ideal-lever-grid-budgets +``` + +`verify.py --write` regenerates `RESULT.json`. Exact arithmetic is the parent +`ceiling.py` (atanh log chains, Taylor exp with remainder, outward rounding to +2^-256); this package adds only the grid enumeration and controls. + +## Open next questions + +- **Integer-count twin of the minimal antichain.** Re-price the three minimal + reaching cells with joint integer child counts (the #3811 DP at caps ≥ 32, plus + integer idle), because the `sel|8|u2` margin over the target (1.46 %) is the same + order as the known ≈ 1.35 % integrality loss. First step: reuse + `research/complex-joint-integer-cap-ceiling`'s DP harness on the reshaped + profiles; no new inputs needed if that PR's package lands. +- **Bit-side twin.** The same grid on the bit primitive's local word would say + whether the target needs a third lever on the currently cheaper side. Blocked by: + the bit word's published per-call local profile and coverage identity need to be + pinned first (the ceiling tool is complex-side). +- **Realization pricing.** For `u = 2` (the cheapest crossing lever) no contract is + known that leaves a second unpaid coordinate (`research/p104-*` and the coverage + maps treat one unpaid coordinate as forced by the line-port contract); a plane-port + discussion exists upstream. First useful evidence: a priced contract, not a better + ceiling. + +## Related open work + +Peer packages pricing budgets/ceilings for the same selected complex local word +(none modified here; numeric cross-checks below were run against `RESULT.json`). + +* [#3729](https://github.com/CrocSwap/integer-mult-bounds/pull/3729) — same model + as my baseline cell but with integer idle counts (32x51 + 1x14). Overlap: the + shared fractional anchor `0.001690054109089` lies inside my `sel|word|u1` bracket + `[0.001690054109, 0.001690054110]`, and its attained integer ceiling + `0.001688603446527` sits strictly below it, as integer tightening implies. Its + 0.0858 % integrality-loss column recomputes to 0.0858 % against my cap: agreement. +* [#3799](https://github.com/CrocSwap/integer-mult-bounds/pull/3799) — same + inherited relaxation at φ = 0 (anchor identical to the baseline quote above, + checked inside my bracket), then prices *free removal* of paid mass re-packed as + ideal idle — an axis this grid does not touch (I reshape ranks, remove nothing), + so no cell overlaps beyond the baseline. Its full-elimination figure + `0.013675160009708` reproduces the stated 8.0916x against my grid-level cap. +* [#3805](https://github.com/CrocSwap/integer-mult-bounds/pull/3805) — same word, + coverage law and centre, but sweeps the idle rank cap with optimal integer idle + packing (aggregate 144-call normalization, same w = 896/9). My grid fixes idle at + rank 51, so no cap endpoints coincide; the quoted fractional ceiling + κ < 0.001687202646 agrees with my baseline κ cap to the quoted 12 decimals, and + their per-call integer bracket lower end `0.0016886034465262156` lies below my + baseline bracket exactly as integer tightening implies. +* [#3811](https://github.com/CrocSwap/integer-mult-bounds/pull/3811) — the + integer twin of my shape lever at baseline centre/unpaid: attained joint integer + packings for paid-mass caps 1..51. Shared quantity: its fractional class-relaxation + control at cap 16 is the parent rank-16 lever row, which my `sel|16|u1` cell + reproduces live (`[0.003909456001, 0.003909456002]`); its cap-8 integer-idle row + `0.00273511` sits 0.160 % below my fractional `sel|8|u1` cap, the consistent + direction. Its cap-44 κ `0.01020939` and my minimal reaching cell `sel|8|u2` + κ `0.010248146` are close in magnitude but differ in premises (integer caps at + baseline centre/u1 vs fractional rank-8 delivery with u = 2) — no shared quantity, + no comparison claimed. +* [#1791](https://github.com/CrocSwap/integer-mult-bounds/pull/1791) — planning + overhead budgets for centre-path sharing on the actual selected profiles; the + centre rows here are ideal relaxations of the same lever paired with shape and + coverage changes, not a realization price. No numeric overlap. + +No contradiction found with any of the above; the three shared (or transitively +shared) quantities — the baseline relaxation ceiling, the parent rank-16 lever row, +and #3729's integrality-loss column — all agree numerically. + +## Credit + +Prepared by Nick Petalas with AI assistance. Independent human and formal +proof-kernel review are unclaimed. Model, coverage identity and ceiling tool are +credited to their authors above; no source file is modified by this package. +Apache-2.0. diff --git a/research/ideal-lever-grid-budgets/RESULT.json b/research/ideal-lever-grid-budgets/RESULT.json new file mode 100644 index 0000000000..cdf5bad9d9 --- /dev/null +++ b/research/ideal-lever-grid-budgets/RESULT.json @@ -0,0 +1,288 @@ +{ + "baseline_a_cap": "169005411/100000000000", + "baseline_kappa_cap": "169005411/100169005411", + "credit": "Nick Petalas", + "guards": { + "idle_rank_cap_52_rejected": true, + "over_weight_local_profile_rejected": true, + "unpaid_zero_rejected": true + }, + "model": { + "families": 896, + "fractional_idle": true, + "grid": "1/1000000000000", + "guard_R": 51, + "local_mass_word": 5586, + "m": 73, + "stages": 9 + }, + "monotonicity_violations": 0, + "nesting": { + "free|16|1": "contains_fine_bracket", + "sel|word|1": "contains_fine_bracket", + "shr|32|2": "contains_fine_bracket" + }, + "published_row_agreement": { + "free|16|1": { + "grid_a_cap_float": "0.011008425", + "grid_x_float": "6.513653", + "parent_a_cap_printed": "0.011008", + "parent_x_printed": 6.51 + }, + "free|word|1": { + "grid_a_cap_float": "0.004737653", + "grid_x_float": "2.803255", + "parent_a_cap_printed": "0.004738", + "parent_x_printed": 2.8 + }, + "sel|16|1": { + "grid_a_cap_float": "0.003909456", + "grid_x_float": "2.313214", + "parent_a_cap_printed": "0.003909", + "parent_x_printed": 2.31 + }, + "sel|8|1": { + "grid_a_cap_float": "0.002739504", + "grid_x_float": "1.620957", + "parent_a_cap_printed": "0.002740", + "parent_x_printed": 1.62 + }, + "sel|word|1": { + "grid_a_cap_float": "0.001690054", + "grid_x_float": "1.000000", + "parent_a_cap_printed": "0.001690", + "parent_x_printed": 1.0 + }, + "sel|word|2": { + "grid_a_cap_float": "0.006377984", + "grid_x_float": "3.773834", + "parent_a_cap_printed": "0.006378", + "parent_x_printed": 3.77 + }, + "shr|word|1": { + "grid_a_cap_float": "0.003212973", + "grid_x_float": "1.901107", + "parent_a_cap_printed": "0.003213", + "parent_x_printed": 1.9 + } + }, + "rows": [ + { + "a_hi": "169005411/100000000000", + "a_lo": "1690054109/1000000000000", + "centre": "sel", + "kappa_hi": "169005411/100169005411", + "shape": "word", + "unpaid": 1 + }, + { + "a_hi": "6377984109/1000000000000", + "a_lo": "1594496027/250000000000", + "centre": "sel", + "kappa_hi": "6377984109/1006377984109", + "shape": "word", + "unpaid": 2 + }, + { + "a_hi": "547900877/200000000000", + "a_lo": "10701189/3906250000", + "centre": "sel", + "kappa_hi": "547900877/200547900877", + "shape": "8", + "unpaid": 1 + }, + { + "a_hi": "5177129163/500000000000", + "a_lo": "414170333/40000000000", + "centre": "sel", + "kappa_hi": "5177129163/505177129163", + "shape": "8", + "unpaid": 2 + }, + { + "a_hi": "1954728001/500000000000", + "a_lo": "3909456001/1000000000000", + "centre": "sel", + "kappa_hi": "1954728001/501954728001", + "shape": "16", + "unpaid": 1 + }, + { + "a_hi": "14797222743/1000000000000", + "a_lo": "7398611371/500000000000", + "centre": "sel", + "kappa_hi": "14797222743/1014797222743", + "shape": "16", + "unpaid": 2 + }, + { + "a_hi": "6823269601/1000000000000", + "a_lo": "8529087/1250000000", + "centre": "sel", + "kappa_hi": "6823269601/1006823269601", + "shape": "32", + "unpaid": 1 + }, + { + "a_hi": "25914723877/1000000000000", + "a_lo": "6478680969/250000000000", + "centre": "sel", + "kappa_hi": "25914723877/1025914723877", + "shape": "32", + "unpaid": 2 + }, + { + "a_hi": "1606486447/500000000000", + "a_lo": "3212972893/1000000000000", + "centre": "shr", + "kappa_hi": "1606486447/501606486447", + "shape": "word", + "unpaid": 1 + }, + { + "a_hi": "1973277993/250000000000", + "a_lo": "7893111971/1000000000000", + "centre": "shr", + "kappa_hi": "1973277993/251973277993", + "shape": "word", + "unpaid": 2 + }, + { + "a_hi": "5219872239/1000000000000", + "a_lo": "2609936119/500000000000", + "centre": "shr", + "kappa_hi": "5219872239/1005219872239", + "shape": "8", + "unpaid": 1 + }, + { + "a_hi": "12842951267/1000000000000", + "a_lo": "6421475633/500000000000", + "centre": "shr", + "kappa_hi": "12842951267/1012842951267", + "shape": "8", + "unpaid": 2 + }, + { + "a_hi": "7430576769/1000000000000", + "a_lo": "58051381/7812500000", + "centre": "shr", + "kappa_hi": "7430576769/1007430576769", + "shape": "16", + "unpaid": 1 + }, + { + "a_hi": "18307801851/1000000000000", + "a_lo": "366156037/20000000000", + "centre": "shr", + "kappa_hi": "18307801851/1018307801851", + "shape": "16", + "unpaid": 2 + }, + { + "a_hi": "12887707951/1000000000000", + "a_lo": "257754159/20000000000", + "centre": "shr", + "kappa_hi": "12887707951/1012887707951", + "shape": "32", + "unpaid": 1 + }, + { + "a_hi": "31857574589/1000000000000", + "a_lo": "7964393647/250000000000", + "centre": "shr", + "kappa_hi": "31857574589/1031857574589", + "shape": "32", + "unpaid": 2 + }, + { + "a_hi": "473765347/100000000000", + "a_lo": "4737653469/1000000000000", + "centre": "free", + "kappa_hi": "473765347/100473765347", + "shape": "word", + "unpaid": 1 + }, + { + "a_hi": "9409963999/1000000000000", + "a_lo": "4704981999/500000000000", + "centre": "free", + "kappa_hi": "9409963999/1009409963999", + "shape": "word", + "unpaid": 2 + }, + { + "a_hi": "3857220781/500000000000", + "a_lo": "7714441561/1000000000000", + "centre": "free", + "kappa_hi": "3857220781/503857220781", + "shape": "8", + "unpaid": 1 + }, + { + "a_hi": "7672952119/500000000000", + "a_lo": "15345904237/1000000000000", + "centre": "free", + "kappa_hi": "7672952119/507672952119", + "shape": "8", + "unpaid": 2 + }, + { + "a_hi": "5504212719/500000000000", + "a_lo": "11008425437/1000000000000", + "centre": "free", + "kappa_hi": "5504212719/505504212719", + "shape": "16", + "unpaid": 1 + }, + { + "a_hi": "21929660143/1000000000000", + "a_lo": "10964830071/500000000000", + "centre": "free", + "kappa_hi": "21929660143/1021929660143", + "shape": "16", + "unpaid": 2 + }, + { + "a_hi": "19209067751/1000000000000", + "a_lo": "76836271/4000000000", + "centre": "free", + "kappa_hi": "19209067751/1019209067751", + "shape": "32", + "unpaid": 1 + }, + { + "a_hi": "38398085391/1000000000000", + "a_lo": "3839808539/100000000000", + "centre": "free", + "kappa_hi": "38398085391/1038398085391", + "shape": "32", + "unpaid": 2 + } + ], + "schema_version": 1, + "verdict": { + "minimal_reaching_antichain": [ + "free|16|1", + "sel|8|2", + "shr|32|1" + ], + "reaching_count": 12, + "reaching_rows": [ + "free|16|1", + "free|16|2", + "free|32|1", + "free|32|2", + "free|8|2", + "sel|16|2", + "sel|32|2", + "sel|8|2", + "shr|16|2", + "shr|32|1", + "shr|32|2", + "shr|8|2" + ], + "target_kappa": "1/99", + "target_kappa_float": "0.010101010" + } +} diff --git a/research/ideal-lever-grid-budgets/SOURCES.json b/research/ideal-lever-grid-budgets/SOURCES.json new file mode 100644 index 0000000000..9527e004a9 --- /dev/null +++ b/research/ideal-lever-grid-budgets/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5", + "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0" + }, + { + "path": "research/complex-local-word-ceiling/ceiling.py", + "usage": "input", + "git_blob": "6c0f54527d879396f689523bfde19928a9b6157c", + "sha256": "86a1432870b3b21d8454106ec9162fddc0471472d9214c590a1420f2426cedfc" + }, + { + "path": "research/complex-local-word-ceiling/levers.py", + "usage": "input", + "git_blob": "e6aee6ce1178f5b68b9ce893b2f5b7f80a143b59", + "sha256": "24c71fc5dce5e2d8f9fbd34d059fc9a1c8ad635d93b62102ccb41b03a7b38b9e" + } + ] +} diff --git a/research/ideal-lever-grid-budgets/TASK.json b/research/ideal-lever-grid-budgets/TASK.json new file mode 100644 index 0000000000..bd8fa15028 --- /dev/null +++ b/research/ideal-lever-grid-budgets/TASK.json @@ -0,0 +1,78 @@ +{ + "schema_version": 1, + "task_id": "complex-new-helper-inventory", + "priority_revision": 6, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "original_card": { + "id": "complex-new-helper-inventory", + "question": "Can a new local cost interface change the deficit-to-recursive-cost ratio beyond current packing?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/complex-local-word-ceiling/README.md", + "research/heterogeneous-owner-assembly/README.md", + "certificates/selected-result.json", + "research/selected-k8-unrestricted-ends/README.md" + ], + "methods": [ + "Propose a changed helper inventory and derive an optimistic exact moment.", + "Design a small completed instance and independently verify its endpoint and rank bill." + ], + "acceptance_gate": "A new physically realizable contract outside the frozen catalogue whose per-call profile, screened with ceiling.ceiling(), beats the selected word's packing ceiling; a lower cap does not establish identical circuitry or order attainable optima, and is insufficient to pass the stronger-budget target under this model. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "research/complex-local-word-ceiling/verify.py" + ], + "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING", + "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.", + "scope": "Positive control and planning budget only; this is not a new construction or full cold replay." + }, + "first_experiment": "Before any synthesis, write the candidate per-call local profile (and centre charge / unpaid coordinates if changed) and screen it with ceiling.ceiling(); reject it if even the ideal ceiling does not beat the selected word's by your stated margin.", + "bottleneck_link": "Packing of the selected word is capped at +0.87% (ceiling model); only a lower local excess spend or a changed coverage law raises the cap.", + "allowed_variations": [ + "Narrow to one changed boundary or helper type with explicit counts.", + "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope." + ], + "scope_change_triggers": [ + "Mixing only providers already inside the pinned catalogue.", + "Only changing helper terminal subspaces and monotone frames within the fixed scalar word, entrances and cleanup contract already covered by #1995/#2013.", + "Continuing a partial cost improvement while leaving the same unpriced consumer, restoration or central-readout obligation unresolved; refresh the family expansion decision first. Local product-retiming evidence has a narrow scope and is not a ban on changed graphs or contracts." + ], + "overlap_terms": [ + "helper inventory", + "heterogeneous-owner", + "mutable leaver" + ] + }, + "scope_status": "refined", + "actual_scope": "Ideal combined-lever budget grid: price the full 3x4x2 grid of centre charge {64, 32, 0} x local shape {published word, all mass at rank 8/16/32} x unpaid coordinates {1, 2} through the parent ceiling model, and decide which lever combinations can reach the planning target kappa >= 1/99 inside that model.", + "scope_change_reason": "The card asks whether a changed local cost interface can raise the deficit ratio; before inventing new interfaces, the retained model's own three lever families were enumerated exhaustively to locate where the target becomes unreachable/reachable. This answers the parent package's Open-next-question 1 (screen many profiles) as a planning result; it proposes no new physical interface.", + "bottleneck_link": "Packing of the selected word is capped at +0.87%; the grid quantifies exactly which lever combinations lift the ceiling past the ambitious kappa > 1/99 planning target inside the retained model, and which do not even under ideal relaxation.", + "budget_minutes": 60, + "stop_rule": "Stop after the 24-cell grid, the seven published-row reproductions, monotonicity, guards, nesting and the target decision all pass under one verifier run; do not price realization costs or bit-side numbers in this package.", + "outcome": "completed", + "evidence": "PASS_IDEAL_LEVER_GRID_BUDGETS (verify.py, ~11 s, CPython 3.12): 24 exact-rational brackets at grid 1e-12 byte-match RESULT.json; endpoints certified relax(a_lo)<1= 1/99; minimal reaching antichain {free|rank16|u1: 0.010888560, sel|rank8|u2: 0.010248146, shr|rank32|u1: 0.012723728}; free|word|u2 tops out 7.7% short of target.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Does the minimal reaching cell sel|rank8|u2 (1.46% over target) survive joint integer child counts and integer idle?", + "why_it_matters": "#3811 reports worst-case joint-integrality loss ~1.35% in the baseline centre model, the same order as this margin; fractional-reach may not survive integrality.", + "first_step": "Reuse the DP harness cited in research/complex-joint-integer-cap-ceiling (open PR #3811) on the reshaped rank-8 profile at unpaid=2.", + "blocked_by": "Nothing locally; #3811 is open, so pin its head if it is used as a base." + }, + { + "question": "Bit-side twin of the grid: which centre/shape/unpaid combinations reach 1/99 on the bit primitive local word?", + "why_it_matters": "The ambitious target needs both suppliers above ~1/99; this table is complex-side only.", + "first_step": "Pin the bit word's published per-call local profile and coverage identity, then rerun the same enumeration.", + "blocked_by": "No ceiling tool for the bit local word is retained in this checkout." + }, + { + "question": "Is there any priced contract leaving u = 2 unpaid coordinates per live family?", + "why_it_matters": "u = 2 is the cheapest crossing lever in this grid but the line-port coverage law forces one unpaid coordinate; without a contract the crossing cells are screening numbers only.", + "first_step": "Check the plane-port discussion threads upstream and price one exact small-instance delivery bill.", + "blocked_by": "No accepted contract exists; this is the realization obligation, not this package." + } + ] +} diff --git a/research/ideal-lever-grid-budgets/VERIFY.json b/research/ideal-lever-grid-budgets/VERIFY.json new file mode 100644 index 0000000000..3846855f45 --- /dev/null +++ b/research/ideal-lever-grid-budgets/VERIFY.json @@ -0,0 +1,23 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "certificates/selected-result.json", + "research/complex-local-word-ceiling/ceiling.py", + "research/complex-local-word-ceiling/levers.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "24 exact-rational lever-grid brackets byte-match RESULT.json; endpoint certification relax(a_lo)<1 Fraction count) for one centre/shape cell. + + The sel rows reproduce the parent levers exactly: at centre charge 64 the whole + local mass (including the centre products) is delivered as rank-r children. When + centre copies are retained (shared) or removed (free), only the non-centre mass + 5522 is reshaped; retained shared copies stay rank-8 children. + """ + charge, copies = next((c, k) for t, c, k in CENTRES if t == centre_tag) + prof = {} + if shape == 'word': + for r, n in WORD.items(): + prof[r] = Q(copies if r == 8 else n) + elif centre_tag == 'sel': + prof[shape] = Q(MASS, shape) + else: + if copies: + prof[8] = Q(copies) + prof[shape] = prof.get(shape, Q(0)) + Q(MASS - 64, shape) + prof = {r: n for r, n in prof.items() if n > 0} + mass = sum(r * n for r, n in prof.items()) + assert mass == {64: MASS, 32: MASS - 32, 0: MASS - 64}[charge], (centre_tag, shape, mass) + return prof, charge + + +def row(centre_tag, shape, unpaid, grid=GRID): + prof, charge = profile(centre_tag, shape) + lo, hi = C.ceiling(prof, M, FAM, ST, charge, grid=grid, unpaid=unpaid) + return lo, hi + + +def compute_rows(): + rows = [] + for centre_tag, _, _ in CENTRES: + for shape in SHAPES: + for unpaid in UNPAID: + lo, hi = row(centre_tag, shape, unpaid) + rows.append(dict(centre=centre_tag, shape=str(shape), unpaid=unpaid, + a_lo=str(lo), a_hi=str(hi), + kappa_hi=str(hi / (1 + hi)))) + return rows + + +def main(): + rows = compute_rows() + base = next(Q(r['a_hi']) for r in rows + if (r['centre'], r['shape'], r['unpaid']) == ('sel', 'word', 1)) + for r in rows: + a = Q(r['a_hi']) + print(f"centre={r['centre']:>4s} shape={r['shape']:>4s} unpaid={r['unpaid']} " + f"a_cap={float(a):.9f} x{float(a / base):.3f} " + f"kappa_cap={float(Q(r['kappa_hi'])):.9f} " + f"target={float(TARGET):.6f} {'REACHES' if a / (1 + a) >= TARGET else 'no'}") + + +if __name__ == '__main__': + main() diff --git a/research/ideal-lever-grid-budgets/verify.py b/research/ideal-lever-grid-budgets/verify.py new file mode 100644 index 0000000000..2dd0562c9b --- /dev/null +++ b/research/ideal-lever-grid-budgets/verify.py @@ -0,0 +1,181 @@ +#!/usr/bin/env python3 +"""Verifier for the ideal combined-lever budget grid (research/ideal-lever-grid-budgets). + +Checks, in order: + 1. all 24 grid cells recompute to the exact rational brackets recorded in RESULT.json; + 2. every recorded endpoint is certified (relax(a_lo) < 1 < relax(a_hi)); + 3. profile invariants (local mass per centre variant, child ranks inside the guard); + 4. live control: the parent levers.py runs and its seven published rows agree with + the matching grid cells at printed precision; + 5. lever monotonicity across the whole lattice; + 6. fail-closed guards (idle rank cap 52, unpaid 0, over-weight local profile); + 7. bracket nesting at grid 1e-8 around the 1e-12 brackets for three rows; + 8. target decision: reaching-set size and minimal reaching antichain. + +usage: python3 -B verify.py [--write] +Nick Petalas, with AI assistance. Apache-2.0. +""" +import json +import subprocess +import sys +from fractions import Fraction as Q +from pathlib import Path + +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE)) +import grid as G # noqa: E402 +sys.path.insert(0, str(HERE.parent / 'complex-local-word-ceiling')) +import ceiling as C # noqa: E402 + +RESULT = HERE / 'RESULT.json' +CENTRE_ORDER = {'sel': 0, 'shr': 1, 'free': 2} +SHAPE_ORDER = {'word': 0, '8': 1, '16': 2, '32': 3} + +PUBLISHED = { # grid cell -> (levers.py row name, printed x-multiplier) + ('sel', 'word', 1): ('selected word (baseline)', 1.00), + ('free', 'word', 1): ('centre path free: no 8 rank-8 copies, centre charge 0', 2.80), + ('shr', 'word', 1): ('centre path shared by 2 calls (copies and charge halved)', 1.90), + ('sel', '16', 1): ('local mass delivered as rank-16 children', 2.31), + ('sel', '8', 1): ('local mass delivered as rank-8 children', 1.62), + ('sel', 'word', 2): ('two unpaid coordinates per live family', 3.77), + ('free', '16', 1): ('centre free and rank-16 children combined', 6.51), +} + + +def key(row): + return (row['centre'], row['shape'], row['unpaid']) + + +def fmt(k): + return '|'.join((k[0], k[1], str(k[2]))) + + +def below(a, b): + """a strictly below b in the lever lattice (<= in every coordinate, < in one).""" + ka, kb = key(a), key(b) + le = (CENTRE_ORDER[ka[0]] <= CENTRE_ORDER[kb[0]] + and SHAPE_ORDER[ka[1]] <= SHAPE_ORDER[kb[1]] + and ka[2] <= kb[2]) + lt = (CENTRE_ORDER[ka[0]] < CENTRE_ORDER[kb[0]] + or SHAPE_ORDER[ka[1]] < SHAPE_ORDER[kb[1]] + or ka[2] < kb[2]) + return le and lt + + +def compute_result(): + rows = G.compute_rows() + base = next(Q(r['a_hi']) for r in rows if key(r) == ('sel', 'word', 1)) + + # (2) endpoint certification for every recorded bracket + for r in rows: + prof, charge = G.profile(r['centre'], r['shape'] if r['shape'] == 'word' else int(r['shape'])) + unpaid = r['unpaid'] + lo, hi = Q(r['a_lo']), Q(r['a_hi']) + assert C.relax(prof, G.M, G.FAM, G.ST, charge, lo, unpaid=unpaid)[1] < 1, r + assert C.relax(prof, G.M, G.FAM, G.ST, charge, hi, unpaid=unpaid)[0] > 1, r + + # (3) profile invariants + q = C.model(dict(G.WORD), G.M, G.FAM, G.ST, 64) + assert q['idle_mass'] == 1646, q # published idle mass + for r in rows: + shape = r['shape'] if r['shape'] == 'word' else int(r['shape']) + prof, charge = G.profile(r['centre'], shape) + assert all(0 < rq < G.M and rq <= q['R'] for rq in prof), r + assert sum(rq * n for rq, n in prof.items()) == {64: G.MASS, 32: G.MASS - 32, 0: G.MASS - 64}[charge] + + # (4) live levers.py control + proc = subprocess.run([sys.executable, '-B', str(HERE.parent / 'complex-local-word-ceiling' / 'levers.py')], + capture_output=True, text=True, check=True) + published_rows = {} + for line in proc.stdout.splitlines(): + if 'a_cap=' in line: + name = line.split('a_cap=')[0].strip() + a_cap = float(line.split('a_cap=')[1].split()[0]) + published_rows[name] = a_cap + agree = {} + for cell, (name, mult) in PUBLISHED.items(): + assert name in published_rows, f'parent row missing: {name}' + row = next(r for r in rows if key(r) == cell) + a = Q(row['a_hi']) + assert abs(float(a) - published_rows[name]) <= 1e-6 + 1e-9, (cell, float(a), published_rows[name]) + ratio = float(a / base) + assert abs(ratio - mult) <= 0.005 + 1e-9, (cell, ratio, mult) + agree[fmt(cell)] = { + 'parent_a_cap_printed': f'{published_rows[name]:.6f}', + 'grid_a_cap_float': f'{float(a):.9f}', + 'parent_x_printed': mult, + 'grid_x_float': f'{ratio:.6f}', + } + + # (5) monotonicity across the lattice + violations = [(key(a), key(b)) for a in rows for b in rows + if below(a, b) and Q(a['a_hi']) > Q(b['a_hi'])] + assert not violations, violations + + # (6) fail-closed guards + guards = {} + try: + C.ceiling(dict(G.WORD), G.M, G.FAM, G.ST, 64, grid=G.GRID, R=52) + raise AssertionError('idle rank cap 52 accepted') + except ValueError: + guards['idle_rank_cap_52_rejected'] = True + try: + C.ceiling(dict(G.WORD), G.M, G.FAM, G.ST, 64, grid=G.GRID, unpaid=0) + raise AssertionError('unpaid 0 accepted') + except ValueError: + guards['unpaid_zero_rejected'] = True + try: + C.ceiling({1: 20000}, G.M, G.FAM, G.ST, 64, grid=G.GRID, unpaid=1) + raise AssertionError('over-weight local profile accepted') + except ValueError: + guards['over_weight_local_profile_rejected'] = True + + # (7) bracket nesting at a coarser grid + nesting = {} + for cell in [('sel', 'word', 1), ('free', '16', 1), ('shr', '32', 2)]: + lo8, hi8 = G.row(cell[0], cell[1] if cell[1] == 'word' else int(cell[1]), cell[2], grid=Q(1, 10 ** 8)) + fine = next(r for r in rows if key(r) == cell) + assert Q(str(lo8)) <= Q(fine['a_lo']) and Q(fine['a_hi']) <= Q(str(hi8)), cell + nesting[fmt(cell)] = 'contains_fine_bracket' + + # (8) target decision + reaching = [r for r in rows if Q(r['a_hi']) / (1 + Q(r['a_hi'])) >= G.TARGET] + minimal = [key(r) for r in reaching if not any(below(x, r) for x in reaching)] + verdict = { + 'target_kappa': str(G.TARGET), + 'target_kappa_float': f'{float(G.TARGET):.9f}', + 'reaching_rows': sorted(fmt(k) for k in map(key, reaching)), + 'reaching_count': len(reaching), + 'minimal_reaching_antichain': sorted(fmt(k) for k in minimal), + } + + return { + 'schema_version': 1, + 'model': {'m': G.M, 'families': G.FAM, 'stages': G.ST, 'guard_R': q['R'], + 'local_mass_word': G.MASS, 'grid': str(G.GRID), 'fractional_idle': True}, + 'baseline_a_cap': str(base), + 'baseline_kappa_cap': str(base / (1 + base)), + 'rows': rows, + 'published_row_agreement': agree, + 'monotonicity_violations': len(violations), + 'guards': guards, + 'nesting': nesting, + 'verdict': verdict, + 'credit': 'Nick Petalas', + } + + +def main(): + result = compute_result() + text = json.dumps(result, indent=2, sort_keys=True) + '\n' + if '--write' in sys.argv: + RESULT.write_text(text) + print(f'wrote {RESULT}') + return + if RESULT.read_text() != text: + raise SystemExit('FAIL: RESULT.json does not match recomputation') + print('PASS_IDEAL_LEVER_GRID_BUDGETS') + + +if __name__ == '__main__': + main()