From ef714b6a7de822c8f14e087236e35181d33abd0b Mon Sep 17 00:00:00 2001 From: Sagar Thakrar <18622288+thakrarsagar@users.noreply.github.com> Date: Mon, 19 Oct 2026 10:40:34 +0530 Subject: [PATCH 1/3] Research: bit-lever budgets at the +10% bit endpoint on the actual PR589 histogram (no new kappa) Prices each catalogued revision-3 bit lever, one premise at a time, at the +10% bit endpoint c* = 921658892752012102303/5e23 of centre-sharing-overhead-budget (PR1791 OQ1), with sharp integer budgets (surcharge recomputed) and a second method (levers.py interval arithmetic, 40 signs at c* and c*+1e-24). Admitted levers net nothing: halving-depth 3/4 caps are slack (max idle window 42 < 45), the record's width-8 hosting is optimal (concavity certificate), rank-8 copy carriage loses 2,578 units. Clearing the 649 requirement needs a new word/decoder: 93 copies (one per call), bit-side two-call centre sharing (+9,040; overhead <= 8,391 rank-1 children, ~29.1 units/call), >= 40 pure helper deletions per call, >= 649 doubly-unpaid families, or ideal shapes in >= 52 of 288 calls. The complex half of the same route has <= ~28.3 units/call of sharing overhead at c*. Planning bound / scoped proof; no construction, no kappa claim. Co-Authored-By: Claude Opus 5.5 --- research/bit-endpoint-lever-budgets/README.md | 210 ++++++++ .../bit-endpoint-lever-budgets/RESULT.json | 469 ++++++++++++++++++ .../bit-endpoint-lever-budgets/SOURCES.json | 54 ++ research/bit-endpoint-lever-budgets/TASK.json | 73 +++ .../bit-endpoint-lever-budgets/VERIFY.json | 52 ++ .../bit-endpoint-lever-budgets/independent.py | 148 ++++++ .../test_package.py | 43 ++ research/bit-endpoint-lever-budgets/verify.py | 346 +++++++++++++ 8 files changed, 1395 insertions(+) create mode 100644 research/bit-endpoint-lever-budgets/README.md create mode 100644 research/bit-endpoint-lever-budgets/RESULT.json create mode 100644 research/bit-endpoint-lever-budgets/SOURCES.json create mode 100644 research/bit-endpoint-lever-budgets/TASK.json create mode 100644 research/bit-endpoint-lever-budgets/VERIFY.json create mode 100644 research/bit-endpoint-lever-budgets/independent.py create mode 100644 research/bit-endpoint-lever-budgets/test_package.py create mode 100644 research/bit-endpoint-lever-budgets/verify.py diff --git a/research/bit-endpoint-lever-budgets/README.md b/research/bit-endpoint-lever-budgets/README.md new file mode 100644 index 000000000..cd1a3b2b0 --- /dev/null +++ b/research/bit-endpoint-lever-budgets/README.md @@ -0,0 +1,210 @@ +# Bit-lever budgets at the +10% bit endpoint, on the actual PR589 histogram + +**Planning bound and scoped proof (bit supplier). No construction, no κ claim, not a multiplication theorem.** +The selected record is unchanged: κ = 0.001672660197076918 (#1094), complex-bound. + +- Track: bit (weight 20). Card: `bit-helper-contract`, scope **changed** to lever pricing (see [TASK.json](TASK.json)). + Consuming decision: `centre-path-sharing`. +- Base: canonical main `20ecf2891d80b5acf18d980b2164fb44ea7faa90` (priority revision 6). Pins: [SOURCES.json](SOURCES.json). + +## Statement + +[centre-sharing-overhead-budget](../centre-sharing-overhead-budget/README.md) (PR1791) showed that two-call centre +sharing makes the complex side stop binding. A **+10%** whole-bound κ then needs the bit endpoint +**c\* = 921658892752012102303/5·10²³ ≈ 0.0018433178** (1.0634× the selected bit endpoint). On the cited PR589 bit +histogram that is a net saving of **649 rank-1 children** (648 fails). Its open question 1 asks whether any bit lever +supplies that. This package prices each catalogued revision-3 bit lever **on the actual histogram** (deficit 10,272, +m = 64, W = 28,416, T = 32 replicas, 288 stage calls, nine rank-7 copies per call, halving depth 2). The surcharge is +recomputed from each histogram's child count. Every count below is a **sharp integer at c\***: the stated count +passes the exact moment test and one less fails (one more, for budgets). The same signs hold at c\* + 10⁻²⁴. + +| Lever (one premise changed on the actual histogram) | Admitted today? | Net saving at c\* (rank-1 units) | Sharp size that clears 649 | +|---|---|---:|---| +| (a) Halving depth 3 / 4 (idle cap 45 → 50 / 53) | yes (r740 row bound) | **0 exactly** | none: the cap is slack | +| (a′) Width-8 re-hosting inside the actual idle windows | yes | **0 exactly** (record is optimal) | none | +| (b1) Rank-8 copy carriage, 9 copies per call (cst 63 → 72) | in (Bat) window | **−2,577.6** | none (makes things worse) | +| (b2) Fewer rank-7 copies | no (new decoder contract) | +2,008.8 for one fewer per call | **93 copies** record-wide (92 fails), i.e. one per call | +| (b3) Bit centre path shared by two calls (cst 31.5) | no (unconstructed) | **+9,039.5** | passes with overhead ≤ **8,391 rank-1 / 1,203 rank-7 / 201 rank-42** children (29.1–29.3 units per call) | +| (c) Second unpaid coordinate on F families | no (coverage-law change) | ≤ F | **F ≥ 649** of 28,416 (2.28%), necessary | +| (d) Pure helper deletion, most favorable (8 rank-1 climbs each), optimal width-8 re-hosting | no (PR1250: one removable helper) | +658.5 at d = 40 | **d = 40 per call** (39 fails for every hosting) | +| (d) Helper deletion, PR1043's measured delta | no | ≤ +169.8 | none: the model runs out of rank-7 climbs at d ≤ 19 | +| (e) Ideal in-window local shapes (single rank-7 data climbs, single rank-8 helper climbs) | no (no such word) | +3,647.6 in all 288 calls | **52 of 288 calls** (51 fails) | + +**Conclusion.** No admitted bit lever nets anything at c\*. The admitted levers are the halving-depth cap raise, +width-8 re-hosting and rank-8 copy carriage. Their nets are 0, 0 and −2,578, so any combination of them also fails. +Every lever that clears 649 changes the word, the decoder or the coverage law. The cheapest stated sizes are one +fewer rank-7 copy per call, 40 pure helper deletions per call (9.3% of 430) or the ideal local shapes in 52 calls. + +**Consequence for `centre-path-sharing`.** The catalogued route to +10% through two-call sharing is to share the +centre path **on both suppliers**. The bit-side copy of the same mechanism (row b3) has about 14× the needed saving. +Its overhead budget is ≈ 29.1–29.3 paid-mass units per call. With the complex side at c\* + 10⁻²⁴ and the bit side +at c\*, κ is still ≥ 1.1× selected (checked). The complex side's two-call overhead budget **at c\*** is +≤ 4,079 rank-1 or 511 rank-8 children in total: **≈ 28.3–28.4 units per call**. That is tighter than the +30.5–30.8 that PR1791 gives at the selected bit endpoint, which is the right figure only for the +3.45% cap. Without +a bit-side mechanism of one of the stated sizes, the card's stop rule holds for the catalogued lever set. + +## Why the admitted levers give exactly zero (proof) + +**Windows.** The nine-stage recipe (`global_k.py`, PR #463/#510 lineage, K = 4 pairs) creates nine idle events per +replica: ranks 14, 28, 42 for s = 1, 3, 5, then 7, 7, 7 for s = 2, 4, 6, then 42, 28, 14 (and one rank-0 event) at +s = 8. Each event covers 2v = 222 coordinates. Per replica that gives windows {7: 666, 14: 444, 28: 444, 42: 444}. +`verify.py` derives this from the recipe rules and checks that the record's idle part (profile minus 288 shipped +words) equals T × {2: 435, 4: 444, 6: 444, 7: 666, 42: 9}, the remainder left after hosting 9 × 439 width-8 helpers +per replica. + +**(a) The cap is slack.** HD = 2 caps children at 45, since 2r² < 64² ⇔ r ≤ 45. HD = 3 and 4 raise the cap to 50 +and 53. But every idle child is a window remainder, at most the largest window 7(2K − 2) = 42, and every local +child has rank ≤ 7. So the record's max child is 42 < 45, and raising the halving depth admits no histogram the +fixed windows can produce. Its net saving is exactly 0. Longer windows need a different recipe. In +[bit589-recipe-floor](../bit589-recipe-floor/README.md) (PR1487)'s whole class of nine-stage recipes, that package +reports the longest advance as 2(K − 1) = 6 levels, i.e. a window of 42, so the cap is slack there too. + +**(a′) Width-8 re-hosting cannot help.** A rank-r window holds at most ⌊r/8⌋ width-8 helpers. 8 divides no window +rank, so every window keeps exactly one nonzero remainder child, and the child count (hence the surcharge) is fixed. +Write φ(x) = x(m/x)^a, which is concave. A window with base remainder ρ = r − 8⌊r/8⌋ and u unused slots costs +φ(ρ + 8u), so its extra cost g_ρ(u) = φ(ρ + 8u) − φ(ρ) is concave in u with g_ρ(0) = 0. Hence +g_ρ(u) ≥ u·g_ρ(cap)/cap. Each replica has exactly 3,996 − 3,951 = 45 unused slots. So the total extra cost is +at least 45·min over ρ of g_ρ(cap)/cap. + +At c\* the per-slot costs are certified as 7.94284 (rank-42 window) < 7.94625 (rank 28) < 7.95184 (rank 14) rank-1 +units. So the minimum is 45·g_2(5)/5, which the record attains by leaving 9 rank-42 windows empty. The record's +hosting therefore minimizes the bill over all width-8 hostings of the actual windows, even with the per-stage window +constraints relaxed. The same bound holds record-wide (1,440 unused slots), so pooling across replicas does not +help either. This re-certifies, at c\*, what our merged +[bit589-width-packing](../bit589-width-packing/README.md) (#1023) proved at the selected endpoint. + +**(b1) Copy carriage.** The decoder constant is the sum of the copy ranks: format-limits' T(2Kv − L·cst). With whole +copies, rank-8 carriage of the nine copies raises cst to 72 and the paid mass by 2,592. That increases the bill. +PR1334's "rank-8 carriage" row kept cst = 63 with 63/8 fractional copies, which is the fewer-copies lever (b2). + +**(c) One unit of rank mass is worth at most one rank-1 child.** Trimming a rank-r child to r − 1 saves +φ(r) − φ(r − 1) < φ(1), certified for r = 2..42 at c\*. Removing a rank-1 child also removes its surcharge. So F +doubly-unpaid families save at most F rank-1 children, and F ≥ 649 is necessary. + +**(d) Deletion bounds.** For d deletions per call, the 45 + 9d unused slots per replica are priced two ways: +- from below, by the concavity bound (all at the rank-42 per-slot cost, fractional); +- from above, by an explicit hosting (⌊(45 + 9d)/5⌋ empty rank-42 windows plus one partly used rank-42 window). + +In the most favorable pure-deletion model each deleted helper removes 8 rank-1 climbs, the most a mass-8 removal can +save. There the lower bound fails at d = 39 and the explicit hosting passes at d = 40. So 40 is sharp in the +stage-relaxed slot model, and d ≤ 39 fails for every pure-deletion word. Deltas that also merge other climbs belong +to lever (e); the [bit-deletion-ladder](../bit-deletion-ladder/README.md) (PR2465) notes that they can beat RANK1 +at equal mass. + +Linearity makes every budget sharp. f(a) = (1/(mW)) Σ n_r r (m/r)^a + c_s m^a with c_s = 32mN/(10¹⁶W) is affine in +the counts, so each one-parameter family is monotone and the boundary is a single integer. + +## Second method + +[independent.py](independent.py) rebuilds every boundary histogram from the pinned PR589 and #1094 records with its +own code, requires byte-identical histograms, and recomputes all **40 signs**: 16 bit rows and 4 complex rows, each +at c\* and at c\* + 10⁻²⁴. It uses the separate interval arithmetic of our merged +[bit-revision3-levers-seed03/levers.py](../bit-revision3-levers-seed03/levers.py) (PR1334): ln by atanh prime chains, +exp by Taylor with a remainder bound, outward dyadic rounding. It also re-checks the re-hosting order and the +trimming lemma. The primary [verify.py](verify.py) uses the D/E-diagnostic engine (PR1293, Navinor). The two +methods agree on every sign. + +## Reproduce + +From the repository root (standard library and `git`; about 15 s): + +```sh +python3 -I -B research/bit-endpoint-lever-budgets/verify.py && python3 -I -B research/bit-endpoint-lever-budgets/independent.py +``` + +Expected output: + +```text +PASS_BIT_ENDPOINT_LEVER_BUDGETS need_rank1=649 admitted_levers_max_net=0 copies_sharp=93 deletions_per_call=RANK1:40/TEMPLATE:None ideal_shape_calls=52 no_new_kappa +PASS_BIT_ENDPOINT_LEVER_BUDGETS_INDEPENDENT signs=40 at c* and c*+1e-24 (levers.py interval arithmetic) +``` + +`verify.py` regenerates [RESULT.json](RESULT.json) and requires byte equality (`--write` rewrites it). It refuses +to run under `-O`. + +**Controls in `verify.py`:** +- its bill equals the pinned engine's on the record; +- the selected bit endpoint is accepted and its next grid point rejected; +- the selected κ is recomputed; +- c\* is the least grid point with κ ≥ 1.1× selected (and c\* − 10⁻²⁴ is not); +- the record fails at c\*; +- the 649/648 rank-1 and 16 rank-42 requirements are re-derived. + +**Negative controls that must fail:** every "one less" boundary row (648 rank-1, 92 copies, 39 deletions, +51 reshaped calls) and every "one more" overhead row. [test_package.py](test_package.py) checks that tampering is +rejected by the independent method: +- off-by-one counts; +- a flipped verdict; +- an edited histogram; +- an edited complex verdict. + +```sh +python3 -I -B -m unittest discover -s research/bit-endpoint-lever-budgets -p test_package.py +``` + +## Scope, inherited assumptions and unresolved obligations + +- **Inherited:** + - the fixed-histogram bill and surcharge law of the selected record; + - the coverage identity D = T(2Kv − L·cst) at fixed m, W; + - PR1791's endpoint model, with the complex side at 3/1000 under two-call sharing; + - the PR589 H1–H5, all-size/compiler, precision and analytic obligations, unchanged. +- **Scope of each row:** + - (a) and (a′) hold for the PR589 nine-stage windows and width-8 helpers. (a′) also holds with stage windows + relaxed. No banks are used. + - (b2), (b3), (c), (d) and (e) are pricing passes for hypothetical words or decoders. + - (d)'s d = 40 pass is in the stage-relaxed slot model; its d ≤ 39 fail holds for every hosting. + - (e) is the in-window ideal relaxation of PR1334, applied call by call. +- **Unpaid obligations of every passing row:** the word or decoder itself, then: + - the dirty-input endpoint and restoration; + - hosting under the real stage windows; + - the row-coefficient invoice; + - the recomputed surcharge (included here); + - the native precision/tape; + - admission. + + For (b3) add the bit analogue of PR1748's ownership/sink blocker. Overhead that changes the windows, the coverage + law or the outer recipe is outside the model. +- Run on Linux with CPython 3.14.4. The registered replay + (`python3.12 scripts/research_package.py --package research/bit-endpoint-lever-budgets`) also passed with CPython + 3.12.15: `PASS_REGISTERED_RESEARCH_PACKAGE`. + +## Open next questions + +1. **Can the bit centre path be shared by two calls within ≈ 29 units of overhead per call?** + - *Why it matters:* it is the only catalogued route on which centre sharing reaches +10%. The complex half must + also stay within ≈ 28.3 units per call at c\*. + - *First step:* write the bit analogue of PR1748's two-call reverse phase for the nine rank-7 copies of one + replica, and price its restoration/hosting children. + - *Blocked by:* no bit sharing word exists, and PR1748's ownership/sink blocker has no bit analogue yet. +2. **Is there a decoder contract with eight retained totals (cst ≤ 56)?** + - *Why it matters:* one fewer copy per call nets ≈ 2,009 units, 3.1× the requirement. + - *First step:* test whether one of the nine retained totals of the v = 111 word can be recomputed instead of + copied, and price the extra climbs. + - *Blocked by:* a replacement contract for the decoder's copied totals (the `centre-path-sharing` card's + scope-change trigger). +3. **Which bit word reaches the 52-call reshaping or the 40-deletion size?** + - *Why it matters:* these are the non-sharing alternatives. + - *First step:* measure the best per-call delta of PR1043-style deletions combined with climb merges. + - *Blocked by:* PR1250 found only one removable helper in the fixed word. + +## Credit and provenance + +- **Requirement, endpoint and sharp-removal method:** rtyu193-rgb, `centre-sharing-overhead-budget` (PR1791, head + `00d05a648985`). +- **Moment enclosures:** Navinor, `selected-suppliers-de-diagnostic` (PR1293, head `85a361233431`). +- **Bootstrap/outer formulas:** Wronskode, `frontier1042-invoice-audit-seed81`. +- **Independent arithmetic:** our merged `bit-revision3-levers-seed03` (PR1334, head `5ad74a4a04d1`). +- **Re-hosting optimality at the selected endpoint and the slot model:** our merged `bit589-width-packing` (#1023). +- **Deletion models:** our merged `bit-deletion-ladder` (PR2465, head `9494fc4e2ecd`), from Ali Romman's PR1043 delta. +- **Recipe class:** ianlibanio, `bit589-recipe-floor` (PR1487). +- **Halving-depth admission:** the r740 elementary-cover row bound authors. +- **Bit supplier:** DreamingOfClouds (PR589) and eumemic (PR555), with the PR510/PR463/PR442 template and hosting + lineage. +- **Selected construction:** Rohan Arun (#1094). + +All are loaded unchanged as pinned Git blobs. Predecessor code is reused without modification. + +Prepared by Sagar Thakrar (thakrarsagar) with substantial AI assistance from Claude (Anthropic, Claude Opus 5.5). The +question was scoped, and the code and prose written, in one session of an automated research loop. Before submission +it is checked only by AI review passes in the same loop; there is no independent human review. Apache-2.0. diff --git a/research/bit-endpoint-lever-budgets/RESULT.json b/research/bit-endpoint-lever-budgets/RESULT.json new file mode 100644 index 000000000..e8fb2ae93 --- /dev/null +++ b/research/bit-endpoint-lever-budgets/RESULT.json @@ -0,0 +1,469 @@ +{ + "boundary_checks": [ + { + "hist": { + "1": "380375", + "2": "400416", + "3": "22752", + "4": "26880", + "42": "288", + "5": "29376", + "6": "17376", + "7": "26784" + }, + "label": "remove 649 rank-1", + "verdict": "pass" + }, + { + "hist": { + "1": "380376", + "2": "400416", + "3": "22752", + "4": "26880", + "42": "288", + "5": "29376", + "6": "17376", + "7": "26784" + }, + "label": "remove 648 rank-1", + "verdict": "fail" + }, + { + "hist": { + "1": "381024", + "2": "400416", + "3": "22752", + "4": "26880", + "42": "288", + "5": "29376", + "6": "17376", + "7": "24192", + "8": "2592" + }, + "label": "rank-8 carriage of all 2592 copies (cst 72)", + "verdict": "fail" + }, + { + "hist": { + "1": "381024", + "2": "400416", + "3": "22752", + "4": "26880", + "42": "288", + "5": "29376", + "6": "17376", + "7": "26691" + }, + "label": "remove 93 rank-7 copies", + "verdict": "pass" + }, + { + "hist": { + "1": "381024", + "2": "400416", + "3": "22752", + "4": "26880", + "42": "288", + "5": "29376", + "6": "17376", + "7": "26692" + }, + "label": "remove 92 rank-7 copies", + "verdict": "fail" + }, + { + "hist": { + "1": "389415", + "2": "400416", + "3": "22752", + "4": "26880", + "42": "288", + "5": "29376", + "6": "17376", + "7": "25488" + }, + "label": "two-call sharing + 8391 rank-1 overhead", + "verdict": "pass" + }, + { + "hist": { + "1": "389416", + "2": "400416", + "3": "22752", + "4": "26880", + "42": "288", + "5": "29376", + "6": "17376", + "7": "25488" + }, + "label": "two-call sharing + 8392 rank-1 overhead", + "verdict": "fail" + }, + { + "hist": { + "1": "381024", + "2": "400416", + "3": "22752", + "4": "26880", + "42": "288", + "5": "29376", + "6": "17376", + "7": "26691" + }, + "label": "two-call sharing + 1203 rank-7 overhead", + "verdict": "pass" + }, + { + "hist": { + "1": "381024", + "2": "400416", + "3": "22752", + "4": "26880", + "42": "288", + "5": "29376", + "6": "17376", + "7": "26692" + }, + "label": "two-call sharing + 1204 rank-7 overhead", + "verdict": "fail" + }, + { + "hist": { + "1": "381024", + "2": "400416", + "3": "22752", + "4": "26880", + "42": "489", + "5": "29376", + "6": "17376", + "7": "25488" + }, + "label": "two-call sharing + 201 rank-42 overhead", + "verdict": "pass" + }, + { + "hist": { + "1": "381024", + "2": "400416", + "3": "22752", + "4": "26880", + "42": "490", + "5": "29376", + "6": "17376", + "7": "25488" + }, + "label": "two-call sharing + 202 rank-42 overhead", + "verdict": "fail" + }, + { + "hist": { + "1": "288864", + "2": "398112", + "3": "22752", + "4": "26880", + "42": "2592", + "5": "29376", + "6": "17376", + "7": "26784" + }, + "label": "RANK1: 40 deletions per call, explicit hosting", + "verdict": "pass" + }, + { + "hist": { + "1": "291168", + "2": "1990848/5", + "3": "22752", + "4": "26880", + "42": "12672/5", + "5": "29376", + "6": "17376", + "7": "26784" + }, + "label": "RANK1: 39 deletions per call, concavity bound", + "verdict": "fail" + }, + { + "hist": { + "1": "370080", + "2": "2051328/5", + "3": "17280", + "4": "26880", + "42": "6912/5", + "5": "29376", + "6": "17376", + "7": "21312" + }, + "label": "TEMPLATE: 19 deletions per call (model exhausted), concavity bound", + "verdict": "fail" + }, + { + "hist": { + "1": "312228", + "2": "330632", + "3": "18644", + "4": "24592", + "42": "288", + "5": "24072", + "6": "16804", + "7": "37808", + "8": "22828" + }, + "label": "ideal shapes in 52 calls", + "verdict": "pass" + }, + { + "hist": { + "1": "313551", + "2": "331974", + "3": "18723", + "4": "24636", + "42": "288", + "5": "24174", + "6": "16815", + "7": "37596", + "8": "22389" + }, + "label": "ideal shapes in 51 calls", + "verdict": "fail" + } + ], + "context_complex_at_c_star": { + "boundary_checks": [ + { + "hist": { + "1": 353683, + "2": 60192, + "3": 62585, + "4": 20448, + "48": 4866, + "5": 11808, + "7": 7, + "8": 576 + }, + "label": "complex two-call sharing + 4079 rank-1 overhead", + "verdict": "pass" + }, + { + "hist": { + "1": 353684, + "2": 60192, + "3": 62585, + "4": 20448, + "48": 4866, + "5": 11808, + "7": 7, + "8": 576 + }, + "label": "complex two-call sharing + 4080 rank-1 overhead", + "verdict": "fail" + }, + { + "hist": { + "1": 349604, + "2": 60192, + "3": 62585, + "4": 20448, + "48": 4866, + "5": 11808, + "7": 7, + "8": 1087 + }, + "label": "complex two-call sharing + 511 rank-8 overhead", + "verdict": "pass" + }, + { + "hist": { + "1": 349604, + "2": 60192, + "3": 62585, + "4": 20448, + "48": 4866, + "5": 11808, + "7": 7, + "8": 1088 + }, + "label": "complex two-call sharing + 512 rank-8 overhead", + "verdict": "fail" + } + ], + "model": "centre-sharing-overhead-budget k=2: 1152 -> 576 rank-8 centre children", + "overhead_budget": { + "1": { + "mass_per_call": 28.326, + "per_call": 28.326, + "total": 4079 + }, + "8": { + "mass_per_call": 28.389, + "per_call": 3.549, + "total": 511 + } + } + }, + "controls": [ + "F equals the pinned D/E-diagnostic bill on the record", + "selected bit endpoint accepted, next grid rejected", + "selected kappa recomputed", + "c* is the least grid point with kappa >= 1.1 x selected (complex at 3/1000)", + "complex endpoint c* + 1e-24 with bit endpoint c* already gives kappa >= 1.1 x selected", + "the record fails at c*" + ], + "endpoint": { + "c_star": "921658892752012102303/500000000000000000000000", + "c_star_decimal": "0.0018433177855040", + "next_grid": "1843317785504024204607/1000000000000000000000000" + }, + "lever_a_idle_cap": { + "halving_caps": { + "2": 45, + "3": 50, + "4": 53 + }, + "max_child": 42, + "net_rank1_units_hd3": 0, + "net_rank1_units_hd4": 0, + "note": "every child is at most the largest idle window 42 < 45, so HD 3/4 caps admit no new histogram; spare width-8 slots are cheapest in emptied rank-42 windows, which the record already does", + "per_slot_cost_rank1_units": { + "14": [ + 7.951844688593213, + 7.951844688593213 + ], + "28": [ + 7.946250285348496, + 7.946250285348496 + ], + "42": [ + 7.942836070759622, + 7.942836070759622 + ] + }, + "record_remainder_per_replica": { + "2": 435, + "4": 444, + "42": 9, + "6": 444, + "7": 666 + }, + "rehost_net_rank1_units": 0, + "window_ranks_per_replica": { + "7": 666, + "14": 444, + "28": 444, + "42": 444 + } + }, + "lever_b_copy_charge": { + "copies": 2592, + "cst_per_call": 63, + "fewer_copies": { + "deficit_one_fewer_per_call": 12288, + "net_rank1_units_one_fewer_per_call": [ + 2008.7817010200051, + 2008.7817010200051 + ], + "per_call_uniform": 1, + "sharp_total_copies": 93 + }, + "rank8_carriage": { + "cst_per_call": 72, + "deficit": 7680, + "net_rank1_units": [ + -2577.6342550966274, + -2577.6342550966274 + ] + }, + "two_call_bit_centre_sharing": { + "copies_removed": 1296, + "cst_per_call": 31.5, + "net_rank1_units": [ + 9039.517654590023, + 9039.517654590023 + ], + "overhead_budget": { + "1": { + "mass_per_call": 29.135, + "per_call": 29.135, + "total": 8391 + }, + "42": { + "mass_per_call": 29.312, + "per_call": 0.698, + "total": 201 + }, + "7": { + "mass_per_call": 29.24, + "per_call": 4.177, + "total": 1203 + } + } + } + }, + "lever_c_unpaid": { + "families": 28416, + "fraction": 0.02284, + "note": "necessary for any u-lever; sufficient only if every saved unit is a rank-1 child", + "sharp_families_needed_if_each_removes_a_rank1_child": 649 + }, + "lever_d_helper_deletion": { + "known_removable_helpers_of_the_fixed_word": 1, + "models": { + "RANK1": { + "1": -8 + }, + "TEMPLATE": { + "1": -2, + "2": 2, + "3": -1, + "7": -1 + } + }, + "sharp": { + "RANK1": { + "net_rank1_units": [ + 658.5284660484807, + 658.5284660484807 + ], + "of_helpers": 430, + "per_call": 40, + "total": 11520 + }, + "TEMPLATE": { + "exhausted_at": 19, + "net_rank1_units_at_exhaustion": [ + 169.8356703347478, + 169.8356703347478 + ], + "of_helpers": 430, + "per_call": null + } + } + }, + "lever_e_local_shape": { + "ideal_per_call": { + "7": 231, + "8": 439 + }, + "net_rank1_units_all_calls": [ + 3647.6015838508097, + 3647.6015838508097 + ], + "of_calls": 288, + "sharp_calls": 52 + }, + "record": { + "T": 32, + "W": 28416, + "calls": 288, + "children": 904896, + "deficit": 10272, + "m": 64, + "rank_mass": 1808352 + }, + "requirement": { + "rank1_children": 649, + "rank1_per_replica": 20.281, + "rank42_children": 16 + }, + "status": "PASS_BIT_ENDPOINT_LEVER_BUDGETS" +} diff --git a/research/bit-endpoint-lever-budgets/SOURCES.json b/research/bit-endpoint-lever-budgets/SOURCES.json new file mode 100644 index 000000000..60c63cde1 --- /dev/null +++ b/research/bit-endpoint-lever-budgets/SOURCES.json @@ -0,0 +1,54 @@ +{ + "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/community-frontier1094-audit/ASSEMBLY.json", + "usage": "input", + "git_blob": "5fd676df060f3b450782fdf5ff5f6beb63a5eeb0", + "sha256": "1122cb3a575f8c788345fc1bf4c108ac7c3250fb81a5988671f5eb04b3ab3045" + }, + { + "path": "research/e8-bit-p111-tuned/tune/EXPECTED.json", + "usage": "input", + "git_blob": "e293ddc557742637f9f679f083a1a282d87b1b13", + "sha256": "b9f0e5ca038abe837b0007c8fe006f366a6f02009244ac57705a8a200e2301f4" + }, + { + "path": "research/selected-suppliers-de-diagnostic/verify.py", + "usage": "input", + "git_blob": "f9a9d5e5103b6ccbadb3f50fea34e25ccfce7ff1", + "sha256": "e69fc72f0534a8eb9ea8e6c0f83deb1ae6537d2f6bf8e511bca23026b68a270f" + }, + { + "path": "research/frontier1042-invoice-audit-seed81/verify.py", + "usage": "input", + "git_blob": "8ee1d7a01473e1b5674710165566e4e9761f7c65", + "sha256": "f5d80137fa58fd078722e171a8d36a300dce4ba7181170047667fca06febfd33" + }, + { + "path": "research/bit-revision3-levers-seed03/levers.py", + "usage": "input", + "git_blob": "f2c4c00fc89ab561469df99dc4a20365e989c40e", + "sha256": "287a1c1201548665087b9b2034210fac92e805f36ea9d4ab41c2471a92d69d7f" + }, + { + "path": "research/centre-sharing-overhead-budget/RESULT.json", + "usage": "input", + "git_blob": "a3758cbd5f157a85e741912783b7203f4061429c", + "sha256": "44fc848b984dbca3aa8ee66898f64f35c305855d0158f1cb4bec0d4d0b28d2b2" + } + ] +} diff --git a/research/bit-endpoint-lever-budgets/TASK.json b/research/bit-endpoint-lever-budgets/TASK.json new file mode 100644 index 000000000..a655a7d5e --- /dev/null +++ b/research/bit-endpoint-lever-budgets/TASK.json @@ -0,0 +1,73 @@ +{ + "schema_version": 1, + "task_id": "bit-helper-contract", + "priority_revision": 6, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "original_card": { + "id": "bit-helper-contract", + "question": "Can one precisely specified helper-mixing word satisfy a replacement for the inherited H2/K interface?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/r439-bsection-stars-seed01/README.md", + "research/r439-copy-path-sharing-barrier/README.md" + ], + "methods": [ + "Derive a replacement interface lemma and price its implementation.", + "Seek an exact dirty-input or chronological-cut counterexample to the proposed replacement." + ], + "acceptance_gate": "A full boundary contract and paid profile; unchanged scalar counts alone are insufficient. 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/r439-bsection-stars-seed01/verify.py" + ], + "expected": "PASS_R439_BSECTION_STARS", + "inspect": "Compare the two false H2/K flags with the unchanged paid profile in its README.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Write one replacement H2/K implication for a single helper-star operation, then try to falsify it on dirty inputs.", + "bottleneck_link": "A legitimate replacement could admit a cheaper bit circuit; scalar savings alone do not alter the selected moment.", + "allowed_variations": [ + "Choose one helper-star or quartet instance; narrow to one boundary implication." + ], + "scope_change_triggers": [ + "Changing only source count or scalar addition count without an interface argument." + ], + "overlap_terms": [ + "H2_D_frame0_targets_from_helpers", + "K_equals_D", + "helper-star" + ] + }, + "scope_status": "changed", + "actual_scope": "Sharp integer pricing, at the +10% bit endpoint c* = 921658892752012102303/5e23 of centre-sharing-overhead-budget, of each catalogued revision-3 bit lever changed one premise at a time on the actual PR589 histogram (surcharge recomputed): halving-depth cap raise, width-8 re-hosting in the actual idle windows, copy carriage/count, two-call bit centre sharing with its overhead budget, unpaid coordinates, helper deletion (two local models, optimal re-hosting) and ideal local shapes; plus the complex-side two-call overhead budget at the same endpoint. Second method: levers.py interval arithmetic on independently rebuilt histograms.", + "scope_change_reason": "The card's H2/K helper-interface question is saturated by other packages; this answers the explicit, unowned open question 1 of centre-sharing-overhead-budget (PR1791), which decides whether the strongest complex lever (two-call centre sharing) can be part of a +10% route. That needs a bit lever netting at least 649 rank-1 units on the actual histogram, which no package had priced.", + "bottleneck_link": "Two-call centre sharing makes the bit side bind; +10% kappa needs the bit endpoint 0.0018433. No admitted bit lever nets anything there (halving-depth cap slack at max window 42, record hosting optimal, rank-8 carriage loses 2,578 units); clearing 649 needs a new word/decoder: one fewer rank-7 copy per call, bit-side two-call centre sharing (overhead <= ~29.1 units/call), >= 40 pure helper deletions per call, >= 649 doubly-unpaid families, or ideal shapes in >= 52 of 288 calls. The complex half of the route must keep its sharing overhead <= ~28.3 units/call at that endpoint. No kappa claim.", + "budget_minutes": 90, + "stop_rule": "Stop once the lever table is exact and the primary (D/E-diagnostic engine) and independent (levers.py) methods agree on every pass/fail sign at c* and c* + 1e-24; build no construction and search for no new bit word.", + "outcome": "completed", + "evidence": "RESULT.json: requirement 649 rank-1 (648 fails) / 16 rank-42; (a) caps 45/50/53, max child 42 = max window, net 0; (a') per-slot costs 7.94284 < 7.94625 < 7.95184 rank-1 units, record optimal, net 0; (b1) cst 72: -2577.6; (b2) 93 copies sharp (92 fails), one fewer per call +2008.8; (b3) cst 31.5: +9039.5, overhead budget 8391 rank-1 / 1203 rank-7 / 201 rank-42; (c) F >= 649 families; (d) RANK1 40 per call (39 fails for every hosting), TEMPLATE exhausted by d = 19 at +169.8; (e) 52 of 288 calls (51 fails), all calls +3647.6; complex k=2 overhead at c*: 4079 rank-1 / 511 rank-8 (28.3-28.4 units per call). 40 signs reproduced by independent.py.", + "author": "Sagar Thakrar (thakrarsagar)", + "ai_assistance": "Claude (Anthropic, Claude Opus 5.5) via Claude Code scoped the question and wrote the code and prose in one session of an automated research loop; checked only by AI review passes in the same loop, no independent human review.", + "open_questions": [ + { + "question": "Can the bit centre path be shared by two calls within about 29 paid-mass units of overhead per call (8,391 rank-1 / 1,203 rank-7 / 201 rank-42 children in total)?", + "why_it_matters": "It is the only catalogued route on which centre sharing reaches +10% kappa; the complex half must also stay within about 28.3 units per call at c*.", + "first_step": "Write the bit analogue of PR1748's two-call reverse phase for the nine rank-7 copies of one replica and price its restoration and hosting children.", + "blocked_by": "No bit sharing word exists, and PR1748's ownership/sink blocker has no bit analogue yet." + }, + { + "question": "Is there a decoder contract with eight retained totals (cst <= 56 per call)?", + "why_it_matters": "One fewer rank-7 copy per call nets about 2,009 rank-1 units, 3.1x the requirement.", + "first_step": "Test whether one of the nine retained totals of the v = 111 word can be recomputed instead of copied, and price the extra climbs.", + "blocked_by": "A replacement contract for the decoder's copied totals (the centre-path-sharing card's scope-change trigger)." + }, + { + "question": "Which bit word reaches the 52-call reshaping or the 40-deletion size?", + "why_it_matters": "These are the non-sharing alternatives for the bit half of a +10% route.", + "first_step": "Measure the best per-call delta of PR1043-style deletions combined with climb merges.", + "blocked_by": "PR1250 found only one removable helper in the fixed word." + } + ] +} diff --git a/research/bit-endpoint-lever-budgets/VERIFY.json b/research/bit-endpoint-lever-budgets/VERIFY.json new file mode 100644 index 000000000..2cd75f0d5 --- /dev/null +++ b/research/bit-endpoint-lever-budgets/VERIFY.json @@ -0,0 +1,52 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/community-frontier1094-audit/ASSEMBLY.json", + "research/e8-bit-p111-tuned/tune/EXPECTED.json", + "research/selected-suppliers-de-diagnostic/verify.py", + "research/frontier1042-invoice-audit-seed81/verify.py", + "research/bit-revision3-levers-seed03/levers.py", + "research/centre-sharing-overhead-budget/RESULT.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "Endpoint, kappa and +10% controls; re-derived 649/16 requirement; window derivation and idle-remainder identity; slack halving cap; certified re-hosting order; sharp copy, sharing-budget, deletion and reshaping boundaries; complex k=2 budget at c*; every boundary sign also at c*+1e-24; RESULT.json byte comparison." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/independent.py" + ], + "timeout_seconds": 120, + "checks": "Rebuilds every boundary histogram independently, requires equality with RESULT.json, and recomputes all 40 signs at c* and c*+1e-24 with levers.py interval arithmetic." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "-m", + "unittest", + "discover", + "-s", + "{package}", + "-p", + "test_package.py" + ], + "timeout_seconds": 120, + "checks": "Tampered counts, verdicts and histograms are rejected by the independent method." + } + ] +} diff --git a/research/bit-endpoint-lever-budgets/independent.py b/research/bit-endpoint-lever-budgets/independent.py new file mode 100644 index 000000000..ecacce294 --- /dev/null +++ b/research/bit-endpoint-lever-budgets/independent.py @@ -0,0 +1,148 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Independent second method for bit-endpoint-lever-budgets. + +Rebuilds every boundary histogram from the pinned PR589 and #1094 records with its own code, checks that it equals +the histogram in RESULT.json, and recomputes each pass/fail sign at c* and at c* + 1e-24 with the separate interval +arithmetic of bit-revision3-levers-seed03/levers.py (ln by atanh prime chains, exp by Taylor with a remainder bound, +outward dyadic rounding). It shares no arithmetic with verify.py, which uses the D/E-diagnostic engine. +Standard library and git only. + +Prepared by Sagar Thakrar (thakrarsagar) with substantial AI assistance from Claude (Anthropic, Claude Opus 5.5). +""" +import hashlib +import json +from fractions import Fraction as Q +from pathlib import Path +import subprocess +import sys +import types + +if not __debug__: + raise SystemExit("checks use assert; run without -O") + +PKG = Path(__file__).resolve().parent +ROOT = PKG.parents[1] +BASE = "20ecf2891d80b5acf18d980b2164fb44ea7faa90" +PINS = {"levers": ("research/bit-revision3-levers-seed03/levers.py", "f2c4c00fc89ab561469df99dc4a20365e989c40e"), + "assembly": ("research/community-frontier1094-audit/ASSEMBLY.json", "5fd676df060f3b450782fdf5ff5f6beb63a5eeb0"), + "pr589": ("research/e8-bit-p111-tuned/tune/EXPECTED.json", "e293ddc557742637f9f679f083a1a282d87b1b13")} +GRID = Q(1, 10 ** 24) + + +def blob(key): + path, sha = PINS[key] + raw = subprocess.run(["git", "-C", str(ROOT), "show", BASE + ":" + path], capture_output=True, check=True).stdout + assert hashlib.sha1(b"blob %d\0" % len(raw) + raw).hexdigest() == sha, "pinned blob differs: " + path + return raw + + +def main(res=None): + """Raise AssertionError unless every sign in res (default: RESULT.json) is reproduced.""" + lv = types.ModuleType("pinned_levers") + exec(compile(blob("levers"), str(ROOT / PINS["levers"][0]), "exec"), lv.__dict__) + asm, rec = json.loads(blob("assembly")), json.loads(blob("pr589")) + res = res or json.loads((PKG / "RESULT.json").read_text(encoding="utf-8")) + c = Q(res["endpoint"]["c_star"]) + assert c == Q(921658892752012102303, 5 * 10 ** 23) + + H0 = {int(r): Q(n) for r, n in rec["nine"]["profile"].items()} + W, m, T, calls = rec["nine"]["bit"]["live"], 64, 32, 288 + assert sum(r * n for r, n in H0.items()) == m * W - 10272 + word = {int(r): n for r, n in rec["word"]["local_histogram"].items()} + + def shift(h, **moves): + out = dict(h) + for key, n in moves.items(): + r = int(key[1:]) + out[r] = out.get(r, Q(0)) + Q(n) + assert out[r] >= 0 + return {r: n for r, n in out.items() if n} + + def bit_sign(h, a): + return lv.verdict(h, m, Q(W), a, surcharge=True) + + # Own derivation of the record's idle remainder: profile minus 288 shipped words, per replica. + idle = {r: (H0.get(r, 0) - calls * word.get(r, 0)) / T for r in set(H0) | set(word)} + assert {r: n for r, n in idle.items() if n} == {2: 435, 4: 444, 6: 444, 7: 666, 42: 9} + assert max(H0) == 42 and all(2 * 42 ** hd < 64 ** hd for hd in (2, 3, 4)) + + a_req = res["requirement"]["rank1_children"] + b = res["lever_b_copy_charge"] + x = b["fewer_copies"]["sharp_total_copies"] + sb = b["two_call_bit_centre_sharing"]["overhead_budget"] + d40 = res["lever_d_helper_deletion"]["sharp"]["RANK1"]["per_call"] + dT = res["lever_d_helper_deletion"]["sharp"]["TEMPLATE"]["exhausted_at"] + k = res["lever_e_local_shape"]["sharp_calls"] + shared = shift(H0, r7=-1296) + + def deletion(delta, d, upper): + h = dict(H0) + for r, n in delta.items(): + h = shift(h, **{"r%d" % r: calls * d * n}) + s = 45 + 9 * d + if not upper: + return shift(h, r42=Q(T * 9 * d, 5), r2=-Q(T * 9 * d, 5)) + n, s0 = divmod(s, 5) + h = shift(h, r42=T * (n - 9), r2=-T * (n - 9)) + return shift(h, **{"r%d" % (2 + 8 * s0): T, "r2": -T}) if s0 else h + + ideal_delta = {1: -1323, 2: -1342, 3: -79, 4: -44, 5: -102, 6: -11, 7: 212, 8: 439} + + def reshaped(kk): + h = dict(H0) + for r, n in ideal_delta.items(): + h = shift(h, **{"r%d" % r: kk * n}) + return h + + mine = [(shift(H0, r1=-a_req), "pass"), (shift(H0, r1=-(a_req - 1)), "fail"), + (shift(H0, r7=-2592, r8=2592), "fail"), + (shift(H0, r7=-x), "pass"), (shift(H0, r7=-(x - 1)), "fail")] + for r in ("1", "7", "42"): + y = sb[r]["total"] + mine += [(shift(shared, **{"r" + r: y}), "pass"), (shift(shared, **{"r" + r: y + 1}), "fail")] + mine += [(deletion({1: -8}, d40, True), "pass"), (deletion({1: -8}, d40 - 1, False), "fail"), + (deletion({1: -2, 2: 2, 3: -1, 7: -1}, dT, False), "fail"), + (reshaped(k), "pass"), (reshaped(k - 1), "fail")] + recorded = res["boundary_checks"] + assert len(recorded) == len(mine), "boundary row count" + for (h, v), row in zip(mine, recorded): + assert {str(r): str(n) for r, n in sorted(h.items())} == row["hist"], "histogram rebuilt differently: " + row["label"] + assert row["verdict"] == v + for a in (c, c + GRID): + assert bit_sign(h, a) == v, "independent sign differs: %s at %s" % (row["label"], a) + + # The TEMPLATE deletion model really is exhausted: its rank-7 consumption equals the word's 19 rank-7 climbs. + assert dT == word[7] == 19 + + # Re-hosting: a spare width-8 slot is cheapest in an emptied rank-42 window (per-slot child-cost comparison). + def ch(r, a): + return lv.child(r, m, a) + for a in (c, c + GRID): + q42 = ((ch(42, a)[0] - ch(2, a)[1]) / 5, (ch(42, a)[1] - ch(2, a)[0]) / 5) + q28 = ((ch(28, a)[0] - ch(4, a)[1]) / 3, (ch(28, a)[1] - ch(4, a)[0]) / 3) + q14 = (ch(14, a)[0] - ch(6, a)[1], ch(14, a)[1] - ch(6, a)[0]) + assert q42[1] < q28[0] and q42[1] < q14[0], "re-hosting order" + # Lever c lemma: trimming one unit from a rank-r child saves less than one rank-1 child. + assert all(ch(r, a)[1] - ch(r - 1, a)[0] < ch(1, a)[0] for r in range(2, 43)) + + # Context: complex side of the same route (no surcharge), boundary signs with levers.py. + HC = {int(r): Q(n) for r, n in asm["complex_profile"].items()} + assert HC[8] == 1152 + for row in res["context_complex_at_c_star"]["boundary_checks"]: + y, r = (int(t) for t in row["label"].split("+ ")[1].split(" rank-")[0:1] + + [row["label"].split("rank-")[1].split(" ")[0]]) + h = dict(HC) + h[8] = Q(576) + h[r] = h.get(r, Q(0)) + y + assert {str(q): int(n) for q, n in sorted(h.items())} == row["hist"], "complex histogram: " + row["label"] + for a in (c, c + GRID): + assert lv.verdict(h, 73, Q(14336), a) == row["verdict"], "complex sign: " + row["label"] + + print("PASS_BIT_ENDPOINT_LEVER_BUDGETS_INDEPENDENT signs=%d at c* and c*+1e-24 (levers.py interval arithmetic)" + % (2 * (len(recorded) + len(res["context_complex_at_c_star"]["boundary_checks"])))) + + +if __name__ == "__main__": + sys.set_int_max_str_digits(1000000) + main() diff --git a/research/bit-endpoint-lever-budgets/test_package.py b/research/bit-endpoint-lever-budgets/test_package.py new file mode 100644 index 000000000..7bc03a2c3 --- /dev/null +++ b/research/bit-endpoint-lever-budgets/test_package.py @@ -0,0 +1,43 @@ +# SPDX-License-Identifier: Apache-2.0 +"""Negative controls: tampered budgets or histograms must be rejected by the independent method.""" +import copy +import importlib.util +import json +from pathlib import Path +import unittest + +PKG = Path(__file__).resolve().parent +spec = importlib.util.spec_from_file_location("independent", PKG / "independent.py") +independent = importlib.util.module_from_spec(spec) +spec.loader.exec_module(independent) +RESULT = json.loads((PKG / "RESULT.json").read_text(encoding="utf-8")) + + +def tampered(edit): + res = copy.deepcopy(RESULT) + edit(res) + return res + + +class Package(unittest.TestCase): + def test_result_reproduced(self): + independent.main(copy.deepcopy(RESULT)) + + def test_rejections(self): + edits = { + "one copy fewer than the sharp count": lambda r: r["lever_b_copy_charge"]["fewer_copies"].update(sharp_total_copies=92), + "one deletion fewer per call": lambda r: r["lever_d_helper_deletion"]["sharp"]["RANK1"].update(per_call=39), + "one reshaped call fewer": lambda r: r["lever_e_local_shape"].update(sharp_calls=51), + "requirement 648": lambda r: r["requirement"].update(rank1_children=648), + "bit sharing budget +1": lambda r: r["lever_b_copy_charge"]["two_call_bit_centre_sharing"]["overhead_budget"]["1"].update(total=8392), + "flipped recorded verdict": lambda r: r["boundary_checks"][2].update(verdict="pass"), + "edited histogram": lambda r: r["boundary_checks"][0]["hist"].update({"42": "289"}), + "complex budget +1": lambda r: r["context_complex_at_c_star"]["boundary_checks"][0].update(verdict="fail"), + } + for name, edit in edits.items(): + with self.subTest(name), self.assertRaises(AssertionError): + independent.main(tampered(edit)) + + +if __name__ == "__main__": + unittest.main() diff --git a/research/bit-endpoint-lever-budgets/verify.py b/research/bit-endpoint-lever-budgets/verify.py new file mode 100644 index 000000000..2b41a8469 --- /dev/null +++ b/research/bit-endpoint-lever-budgets/verify.py @@ -0,0 +1,346 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Sharp bit-lever budgets at the +10% bit endpoint on the actual PR589 histogram (primary method). + +Planning bound / scoped proof for the bit-helper-contract card; consuming decision: centre-path-sharing. +No construction, no kappa claim, not a multiplication theorem. + +The exact moment enclosures (Navinor's selected-suppliers-de-diagnostic) and the bootstrap/outer formulas +(Wronskode's frontier1042-invoice-audit-seed81) are loaded unchanged as pinned Git blobs at BASE, as in +centre-sharing-overhead-budget. The bit bill is f(a) = (1/(mW)) sum_r n_r r (m/r)^a + c_s m^a with the surcharge +c_s = 32 m N / (1e16 W) recomputed from each histogram's child count N. It is linear in the counts n_r, so every +budget below is a sharp integer: the stated count passes the exact test f(c*) < 1 and one less fails. +Standard library and git only. + +Prepared by Sagar Thakrar (thakrarsagar) with substantial AI assistance from Claude (Anthropic, Claude Opus 5.5). +""" +import argparse +import hashlib +import json +from collections import Counter +from fractions import Fraction as Q +from pathlib import Path +import subprocess +import sys +import types + +if not __debug__: + raise SystemExit("checks use assert; run without -O") +sys.set_int_max_str_digits(1000000) + +PKG = Path(__file__).resolve().parent +ROOT = PKG.parents[1] +BASE = "20ecf2891d80b5acf18d980b2164fb44ea7faa90" +PINS = {"de": ("research/selected-suppliers-de-diagnostic/verify.py", "f9a9d5e5103b6ccbadb3f50fea34e25ccfce7ff1"), + "seed81": ("research/frontier1042-invoice-audit-seed81/verify.py", "8ee1d7a01473e1b5674710165566e4e9761f7c65"), + "assembly": ("research/community-frontier1094-audit/ASSEMBLY.json", "5fd676df060f3b450782fdf5ff5f6beb63a5eeb0"), + "pr589": ("research/e8-bit-p111-tuned/tune/EXPECTED.json", "e293ddc557742637f9f679f083a1a282d87b1b13"), + "predecessor": ("research/centre-sharing-overhead-budget/RESULT.json", "a3758cbd5f157a85e741912783b7203f4061429c")} +C_STAR = Q(921658892752012102303, 5 * 10 ** 23) # centre-sharing-overhead-budget: bit endpoint for +10% kappa +GRID = Q(1, 10 ** 24) +ETA = BETA = Q(1, 10 ** 24) +B_CERTIFIED_K2 = Q(3, 1000) # complex acceptance point with two-call sharing (predecessor's premise) +NEED_RANK1 = 649 # predecessor's sharp rank-1 requirement, re-derived below +DELETION_MODELS = {"RANK1": {1: -8}, "TEMPLATE": {1: -2, 2: 2, 3: -1, 7: -1}} # bit-deletion-ladder (per deletion) + + +def blob(key): + path, sha = PINS[key] + raw = subprocess.run(["git", "-C", str(ROOT), "show", BASE + ":" + path], capture_output=True, check=True).stdout + assert hashlib.sha1(b"blob %d\0" % len(raw) + raw).hexdigest() == sha, "pinned blob differs: " + path + return raw + + +def load_module(key): + mod = types.ModuleType("pinned_" + key) + mod.__file__ = str(ROOT / PINS[key][0]) + exec(compile(blob(key), mod.__file__, "exec"), mod.__dict__) + return mod + + +def idle_window_ranks(K): + """Idle-event ranks of the nine-stage recipe, transcribed from global_k.py (PR #463/#510 lineage).""" + out = [7 * (s + 1) for s in range(1, 2 * K - 2, 2)] # s odd, s <= 2K-3: pair (s+1)/2 waits s+1 levels + out += [7 for s in range(2, 2 * K - 1, 2)] # s even, 2 <= s <= 2K-2: one level + out += [7 * (2 * K - (2 * j + 2)) for j in range(K)] # s = 2K: every pair from level 2j+2 to 2K + return [r for r in out if r] + + +def main(): + ap = argparse.ArgumentParser(description=__doc__.splitlines()[0]) + ap.add_argument("--write", action="store_true") + args = ap.parse_args() + de, s81 = load_module("de"), load_module("seed81") + asm, expected, pred = (json.loads(blob(k)) for k in ("assembly", "pr589", "predecessor")) + bit_bill, info = de.bit_ledger(asm, expected) + m, W, T = info["m"], info["W"], info["T"] + H = dict(bit_bill.hist) + word = expected["word"] + calls = 9 * T # L = 9 stage calls per replica + c_sel, k_sel = Q(asm["bit_lower"]), Q(asm["kappa"]) + assert C_STAR == Q(pred["ten_percent_target"]["bit_endpoint_needed"]), "endpoint differs from predecessor" + out = {"endpoint": {"c_star": str(C_STAR), "c_star_decimal": "%.16f" % float(C_STAR), "next_grid": str(C_STAR + GRID)}, + "record": {"m": m, "W": W, "T": T, "calls": calls, "deficit": info["deficit"], "children": sum(H.values()), + "rank_mass": sum(r * n for r, n in H.items())}} + + unit_cache = {} + + def unit(r, a): + """Certified enclosure of r (m/r)^a / (mW): the bill of one rank-r child, from the pinned engine.""" + if (r, a) not in unit_cache: + lo, hi = de.Bill({r: 1}, m, W).residual(a) + unit_cache[r, a] = (lo + 1, hi + 1) + return unit_cache[r, a] + + def F(h, a): + """Certified enclosure of f(a) for a histogram (fractional counts allowed), surcharge recomputed.""" + lo = hi = Q(0) + for r, n in h.items(): + assert n >= 0 and 0 < r < m, "histogram range" + if n: + u = unit(r, a) + lo, hi = lo + n * u[0], hi + n * u[1] + cs = Q(32 * m, 10 ** 16 * W) * sum(h.values()) # c_s m^a = cs * (mW * unit(1)) + u1 = unit(1, a) + return lo + cs * m * W * u1[0], hi + cs * m * W * u1[1] + + def verdict(h, a): + lo, hi = F(h, a) + return "pass" if hi < 1 else "fail" if lo > 1 else "undecided" + + def add(h, delta, k=1): + o = Counter(h) + for r, n in delta.items(): + o[r] += k * n + assert all(n >= 0 for n in o.values()), "negative count" + return {r: n for r, n in o.items() if n} + + def sharp_min(build, lo, hi): + """Least k in (lo, hi] with build(k) passing at c*, given build(lo) fails and build(hi) passes.""" + assert verdict(build(lo), C_STAR) == "fail" and verdict(build(hi), C_STAR) == "pass" + while hi - lo > 1: + mid = (lo + hi) // 2 + v = verdict(build(mid), C_STAR) + assert v != "undecided", "undecided boundary" + lo, hi = (mid, hi) if v == "fail" else (lo, mid) + return hi + + def sharp_max(build, lo, hi): + """Largest k in [lo, hi) with build(k) passing at c*, given build(lo) passes and build(hi) fails.""" + assert verdict(build(lo), C_STAR) == "pass" and verdict(build(hi), C_STAR) == "fail" + while hi - lo > 1: + mid = (lo + hi) // 2 + v = verdict(build(mid), C_STAR) + assert v != "undecided", "undecided boundary" + lo, hi = (mid, hi) if v == "pass" else (lo, mid) + return lo + + def units_saved(h, a=C_STAR): + """Net bill reduction against the record, in rank-1 children (certified interval, rounded outward).""" + r_lo, r_hi = F(H, a) + l_lo, l_hi = F(h, a) + u1 = unit(1, a) + one = (u1[0] * (1 + Q(32 * m * m * W, 10 ** 16 * W)), u1[1] * (1 + Q(32 * m * m * W, 10 ** 16 * W))) + d_lo, d_hi = r_lo - l_hi, r_hi - l_lo + lo = d_lo / one[1] if d_lo >= 0 else d_lo / one[0] + hi = d_hi / one[0] if d_hi >= 0 else d_hi / one[1] + return [float(lo), float(hi)] + + boundary = [] # (label, histogram, expected verdict) for the next-grid and independent checks + + def record(label, h, v): + assert verdict(h, C_STAR) == v, label + boundary.append(dict(label=label, hist={str(r): str(n) for r, n in sorted(h.items())}, verdict=v)) + + # ---- Controls ----------------------------------------------------------------------------------------- + assert F(H, c_sel) == tuple(x + 1 for x in bit_bill.residual(c_sel)), "F reproduces the pinned bill" + assert verdict(H, c_sel) == "pass" and verdict(H, c_sel + GRID) == "fail", "selected bit endpoint" + + def kappa(b, c): + a, _ = s81.bootstrap(b, c, ETA, BETA) + k = s81.kappa_from(a, ETA) + slacks, _ = s81.assembly_slacks(a, b, k, ETA, BETA) + assert all(v > 0 for v in slacks.values()), "outer slack" + return k + assert kappa(Q(asm["complex_lower"]), c_sel) == k_sel, "selected kappa" + target = k_sel * Q(11, 10) + assert kappa(B_CERTIFIED_K2, C_STAR) >= target > kappa(B_CERTIFIED_K2, C_STAR - GRID), "c* is the +10% endpoint" + assert kappa(C_STAR + GRID, C_STAR) >= target, "complex accepted at c* + 1e-24 suffices with bit at c*" + assert verdict(H, C_STAR) == "fail", "the record fails at c*" + out["controls"] = ["F equals the pinned D/E-diagnostic bill on the record", + "selected bit endpoint accepted, next grid rejected", "selected kappa recomputed", + "c* is the least grid point with kappa >= 1.1 x selected (complex at 3/1000)", + "complex endpoint c* + 1e-24 with bit endpoint c* already gives kappa >= 1.1 x selected", + "the record fails at c*"] + + # ---- Baseline requirement (predecessor's sharp removal, re-derived) ------------------------------------ + need1 = sharp_min(lambda x: add(H, {1: -x}), 0, 2000) + need42 = sharp_min(lambda x: add(H, {42: -x}), 0, 100) + assert need1 == NEED_RANK1 and need42 == 16, "predecessor requirement" + record("remove %d rank-1" % need1, add(H, {1: -need1}), "pass") + record("remove %d rank-1" % (need1 - 1), add(H, {1: -(need1 - 1)}), "fail") + out["requirement"] = dict(rank1_children=need1, rank42_children=need42, rank1_per_replica=round(need1 / T, 3)) + + # ---- (a) idle cap / halving depth, and width-8 re-hosting in the actual windows ------------------------- + K, V, R = 4, word["v"], word["R"] + local = {int(r): n for r, n in word["local_histogram"].items()} + assert sum(r * n for r, n in local.items()) == word["legality"]["rank_mass"] == 5129 + ev = idle_window_ranks(K) + assert sorted(ev) == [7, 7, 7, 14, 14, 28, 28, 42, 42] + windows = Counter({r: 2 * V * c for r, c in Counter(ev).items()}) # per replica + assert windows == Counter({7: 666, 14: 444, 28: 444, 42: 444}) + slots = {r: r // 8 for r in windows} # width-8 helper slots per window + spare = sum(windows[r] * slots[r] for r in windows) - 9 * R # 3996 - 3951 = 45 per replica + assert spare == 45 and spare % slots[42] == 0 + rem = Counter({r % 8 if slots[r] else r: n for r, n in windows.items()}) + rem[42 % 8] -= spare // slots[42] + rem[42] += spare // slots[42] + idle = Counter(H) + idle.subtract({r: calls * n for r, n in local.items()}) + assert +idle == Counter({r: T * n for r, n in rem.items()}), "record idle part = optimal width-8 remainder" + caps = {} + for hd in (2, 3, 4): + caps[hd] = max(r for r in range(1, m) if 2 * r ** hd < m ** hd) + assert caps == {2: 45, 3: 50, 4: 53} and expected["nine"]["bit"]["halving_depth"] == 2 + assert max(H) == max(windows) == 7 * (2 * K - 2) == 42 < caps[2], "the halving cap is slack" + assert all(r % 8 for r in windows), "every window keeps a nonzero remainder: child count is fixed" + q = {} + for r, lo_rem in ((42, 2), (28, 4), (14, 6)): + a_, b_ = unit(r, C_STAR), unit(lo_rem, C_STAR) + q[r] = ((a_[0] - b_[1]) / slots[r], (a_[1] - b_[0]) / slots[r]) + assert q[42][1] < q[28][0] and q[42][1] < q[14][0], "emptying rank-42 windows is the cheapest use of a spare slot" + for cs in (C_STAR, C_STAR + GRID): + a_, b_ = unit(42, cs), unit(2, cs) + c_, d_ = unit(28, cs), unit(4, cs) + e_, f_ = unit(14, cs), unit(6, cs) + assert (a_[1] - b_[0]) / 5 < (c_[0] - d_[1]) / 3 and (a_[1] - b_[0]) / 5 < e_[0] - f_[1] + out["lever_a_idle_cap"] = dict( + halving_caps=caps, max_child=max(H), window_ranks_per_replica=dict(sorted(windows.items())), + record_remainder_per_replica={str(r): n for r, n in sorted((+rem).items())}, + per_slot_cost_rank1_units={str(r): [float(q[r][0] / unit(1, C_STAR)[1]), float(q[r][1] / unit(1, C_STAR)[0])] + for r in q}, + net_rank1_units_hd3=0, net_rank1_units_hd4=0, rehost_net_rank1_units=0, + note="every child is at most the largest idle window 42 < 45, so HD 3/4 caps admit no new histogram; " + "spare width-8 slots are cheapest in emptied rank-42 windows, which the record already does") + + # ---- (b) copy charge: rank-8 carriage, fewer rank-7 copies, two-call bit centre sharing ------------------ + copies = calls * len(word["copy_ranks"]) + assert set(word["copy_ranks"]) == {7} and copies == 2592 + b1 = add(H, {7: -copies, 8: copies}) + record("rank-8 carriage of all 2592 copies (cst 72)", b1, "fail") + x_star = sharp_min(lambda x: add(H, {7: -x}), 0, copies) + record("remove %d rank-7 copies" % x_star, add(H, {7: -x_star}), "pass") + record("remove %d rank-7 copies" % (x_star - 1), add(H, {7: -(x_star - 1)}), "fail") + one_per_call = add(H, {7: -calls}) + shared = add(H, {7: -copies // 2}) # two calls share one centre path: 4.5 copies per call + budget = {} + for r in (1, 7, 42): + y = sharp_max(lambda y: add(shared, {r: y}), 0, 20000 if r == 1 else 3000 if r == 7 else 400) + record("two-call sharing + %d rank-%d overhead" % (y, r), add(shared, {r: y}), "pass") + record("two-call sharing + %d rank-%d overhead" % (y + 1, r), add(shared, {r: y + 1}), "fail") + budget[str(r)] = dict(total=y, per_call=round(y / calls, 3), mass_per_call=round(y * r / calls, 3)) + out["lever_b_copy_charge"] = dict( + copies=copies, cst_per_call=63, + rank8_carriage=dict(cst_per_call=72, deficit=info["deficit"] - copies, net_rank1_units=units_saved(b1)), + fewer_copies=dict(sharp_total_copies=x_star, per_call_uniform=1, deficit_one_fewer_per_call=info["deficit"] + 7 * calls, + net_rank1_units_one_fewer_per_call=units_saved(one_per_call)), + two_call_bit_centre_sharing=dict(cst_per_call=31.5, copies_removed=copies // 2, + net_rank1_units=units_saved(shared), overhead_budget=budget)) + + # ---- (c) unpaid coordinates: one unit of rank mass is worth at most one rank-1 child --------------------- + for r in range(2, max(H) + 1): + a_, b_ = unit(r, C_STAR), unit(r - 1, C_STAR) + assert a_[1] - b_[0] < unit(1, C_STAR)[0], "trimming one unit saves less than removing a rank-1 child" + out["lever_c_unpaid"] = dict(families=W, sharp_families_needed_if_each_removes_a_rank1_child=need1, + fraction=round(need1 / W, 5), + note="necessary for any u-lever; sufficient only if every saved unit is a rank-1 child") + + # ---- (d) helper deletions with optimal width-8 re-hosting (stage-relaxed slot model) --------------------- + def deletion(model, d, upper): + h = add(H, DELETION_MODELS[model], calls * d) + s = spare + 9 * d # spare slots per replica + if not upper: # fractional concavity bound (lower bill) + return add(h, {42: Q(T * 9 * d, 5), 2: -Q(T * 9 * d, 5)}) + n, s0 = divmod(s, 5) + assert n + (s0 > 0) <= windows[42] + h = add(h, {42: T * (n - 9), 2: -T * (n - 9)}) + return add(h, {2 + 8 * s0: T, 2: -T}) if s0 else h + assert deletion("RANK1", 0, True) == deletion("RANK1", 0, False) == H + dels = {} + for model, dm in DELETION_MODELS.items(): + d_max = min(local[r] // -n for r, n in dm.items() if n < 0) # the word's climbs the model consumes + d = 0 + while d <= d_max and verdict(deletion(model, d, True), C_STAR) != "pass": + assert verdict(deletion(model, d, False), C_STAR) == "fail", "lower bound must fail below the boundary" + d += 1 + if d > d_max: + record("%s: %d deletions per call (model exhausted), concavity bound" % (model, d_max), + deletion(model, d_max, False), "fail") + dels[model] = dict(per_call=None, exhausted_at=d_max, of_helpers=430, + net_rank1_units_at_exhaustion=units_saved(deletion(model, d_max, True))) + continue + assert verdict(deletion(model, d - 1, False), C_STAR) == "fail", "deletion boundary not sharp: " + model + record("%s: %d deletions per call, explicit hosting" % (model, d), deletion(model, d, True), "pass") + record("%s: %d deletions per call, concavity bound" % (model, d - 1), deletion(model, d - 1, False), "fail") + dels[model] = dict(per_call=d, of_helpers=430, total=calls * d, + net_rank1_units=units_saved(deletion(model, d, True))) + out["lever_d_helper_deletion"] = dict(models={k: {str(r): n for r, n in v.items()} for k, v in DELETION_MODELS.items()}, + sharp=dels, known_removable_helpers_of_the_fixed_word=1) + + # ---- (e) local rank shape: replace the shipped word by the ideal in-window shapes in k calls ------------- + ideal = {7: 2 * V + 9, 8: R} + assert sum(r * n for r, n in ideal.items()) == 5129 + delta = dict(Counter(ideal) - Counter(local)) | {r: -n for r, n in (Counter(local) - Counter(ideal)).items()} + assert delta == {1: -1323, 2: -1342, 3: -79, 4: -44, 5: -102, 6: -11, 7: 212, 8: 439} + k_star = sharp_min(lambda k: add(H, delta, k), 0, calls) + record("ideal shapes in %d calls" % k_star, add(H, delta, k_star), "pass") + record("ideal shapes in %d calls" % (k_star - 1), add(H, delta, k_star - 1), "fail") + out["lever_e_local_shape"] = dict(ideal_per_call={str(r): n for r, n in ideal.items()}, sharp_calls=k_star, + of_calls=calls, net_rank1_units_all_calls=units_saved(add(H, delta, calls))) + + # ---- Context: the complex side of the same route at c* (predecessor's two-call sharing model) ----------- + HC = {int(r): int(n) for r, n in asm["complex_profile"].items()} + MC, WC, NC = 73, 14336, asm["provider_counts"]["gauge44"] + shared_c = {**HC, 8: HC[8] // 2} + + def cverdict(h, a): + lo, hi = de.Bill(h, MC, WC).residual(a) + return "pass" if hi < 0 else "fail" if lo > 0 else "undecided" + assert cverdict(HC, Q(asm["complex_lower"])) == "pass" and cverdict(HC, C_STAR) == "fail" + assert cverdict(shared_c, B_CERTIFIED_K2) == "pass" and cverdict(shared_c, C_STAR) == "pass" + complex_budget, complex_boundary = {}, [] + for r in (1, 8): + lo, hi = 0, 9000 if r == 1 else 1150 # within the shared deficit 5120 + 4608 + assert cverdict(add(shared_c, {r: hi}), C_STAR) == "fail" + while hi - lo > 1: + mid = (lo + hi) // 2 + lo, hi = (mid, hi) if cverdict(add(shared_c, {r: mid}), C_STAR) == "pass" else (lo, mid) + for y, v in ((lo, "pass"), (lo + 1, "fail")): + h = add(shared_c, {r: y}) + assert cverdict(h, C_STAR) == v and cverdict(h, C_STAR + GRID) == v + complex_boundary.append(dict(label="complex two-call sharing + %d rank-%d overhead" % (y, r), + hist={str(q): n for q, n in sorted(h.items())}, verdict=v)) + complex_budget[str(r)] = dict(total=lo, per_call=round(lo / NC, 3), mass_per_call=round(lo * r / NC, 3)) + out["context_complex_at_c_star"] = dict(model="centre-sharing-overhead-budget k=2: 1152 -> 576 rank-8 centre children", + overhead_budget=complex_budget, boundary_checks=complex_boundary) + + # ---- Adjacent grid point: every boundary verdict is unchanged at c* + 1e-24 ---------------------------- + for b in boundary: + h = {int(r): Q(n) for r, n in b["hist"].items()} + assert verdict(h, C_STAR + GRID) == b["verdict"], "next-grid verdict: " + b["label"] + out["boundary_checks"] = boundary + out["status"] = "PASS_BIT_ENDPOINT_LEVER_BUDGETS" + + text = json.dumps(out, indent=1, sort_keys=True) + "\n" + path = PKG / "RESULT.json" + if args.write: + path.write_text(text, encoding="utf-8", newline="\n") + print("WROTE", path.relative_to(ROOT).as_posix()) + else: + assert path.read_text(encoding="utf-8") == text, "RESULT.json differs from the regenerated result" + print("%s need_rank1=%d admitted_levers_max_net=0 copies_sharp=%d deletions_per_call=%s ideal_shape_calls=%d no_new_kappa" + % (out["status"], need1, x_star, "/".join("%s:%s" % (k, v["per_call"]) for k, v in dels.items()), k_star)) + + +if __name__ == "__main__": + main() From 01e304a24d072d55234362fac7e7d1e2a260e95a Mon Sep 17 00:00:00 2001 From: Sagar Thakrar <18622288+thakrarsagar@users.noreply.github.com> Date: Mon, 19 Oct 2026 11:12:19 +0530 Subject: [PATCH 2/3] Revise bit-endpoint-lever-budgets: complex need at c*, width-7 row, review fixes - Reframe around the +10% route's requirement map: the complex endpoint must itself reach c* (asserted); complex need 511 rank-1 (about 3.55/call), correcting PR1791 OQ1's 1.33/call. - Add lever (f): width-7 conversion in #1023's placement (71 per call in the optimistic bracket, 70 fails; trimmed bracket fails at 74), not admitted. - Check every boundary sign at c*-1e-24 too (75 signs); compute the admitted maximum net; TEMPLATE upper bound +170.4; consistent-shift tamper test. - Proof of (a): windows are bridge-delimited; scope (c), (e), complex budget; cite PR1888, PR3075, #1112, #1281, bit-width-seven-boundary, r439 barrier. Co-Authored-By: Claude Opus 5.5 --- research/bit-endpoint-lever-budgets/README.md | 178 ++++++++++++------ .../bit-endpoint-lever-budgets/RESULT.json | 77 +++++++- research/bit-endpoint-lever-budgets/TASK.json | 20 +- .../bit-endpoint-lever-budgets/VERIFY.json | 6 +- .../bit-endpoint-lever-budgets/independent.py | 43 ++++- .../test_package.py | 7 + research/bit-endpoint-lever-budgets/verify.py | 86 ++++++++- 7 files changed, 327 insertions(+), 90 deletions(-) diff --git a/research/bit-endpoint-lever-budgets/README.md b/research/bit-endpoint-lever-budgets/README.md index cd1a3b2b0..1a29a0e50 100644 --- a/research/bit-endpoint-lever-budgets/README.md +++ b/research/bit-endpoint-lever-budgets/README.md @@ -1,47 +1,72 @@ -# Bit-lever budgets at the +10% bit endpoint, on the actual PR589 histogram +# The +10% centre-sharing route at c\* ≈ 0.0018433: complex need and bit-lever budgets on the actual histograms **Planning bound and scoped proof (bit supplier). No construction, no κ claim, not a multiplication theorem.** The selected record is unchanged: κ = 0.001672660197076918 (#1094), complex-bound. -- Track: bit (weight 20). Card: `bit-helper-contract`, scope **changed** to lever pricing (see [TASK.json](TASK.json)). - Consuming decision: `centre-path-sharing`. +- Track: bit (weight 20). Card: `bit-helper-contract`, scope **changed** to lever pricing (see [TASK.json](TASK.json)): + the claim was filed on that card because its H2/K question is saturated; the consuming decision is + `centre-path-sharing` (recursive interfaces). - Base: canonical main `20ecf2891d80b5acf18d980b2164fb44ea7faa90` (priority revision 6). Pins: [SOURCES.json](SOURCES.json). ## Statement [centre-sharing-overhead-budget](../centre-sharing-overhead-budget/README.md) (PR1791) showed that two-call centre -sharing makes the complex side stop binding. A **+10%** whole-bound κ then needs the bit endpoint -**c\* = 921658892752012102303/5·10²³ ≈ 0.0018433178** (1.0634× the selected bit endpoint). On the cited PR589 bit -histogram that is a net saving of **649 rank-1 children** (648 fails). Its open question 1 asks whether any bit lever -supplies that. This package prices each catalogued revision-3 bit lever **on the actual histogram** (deficit 10,272, -m = 64, W = 28,416, T = 32 replicas, 288 stage calls, nine rank-7 copies per call, halving depth 2). The surcharge is -recomputed from each histogram's child count. Every count below is a **sharp integer at c\***: the stated count -passes the exact moment test and one less fails (one more, for budgets). The same signs hold at c\* + 10⁻²⁴. - -| Lever (one premise changed on the actual histogram) | Admitted today? | Net saving at c\* (rank-1 units) | Sharp size that clears 649 | +sharing makes the complex side stop binding. A **+10%** whole-bound κ then needs **both** endpoints at +**c\* = 921658892752012102303/5·10²³ ≈ 0.0018433178** (1.0634× the selected bit endpoint). This package gives the +requirement map of that route on the actual histograms. + +- **Complex side: PR1791's sufficient condition is too weak at c\*.** Its open question 1 says a complex saving of + ≥ 1.33 units per call, together with a 649-unit bit mechanism, reaches +10%. The 1.33 figure is the complex need + at the selected bit endpoint. With the bit side at c\*, the complex endpoint must itself reach c\*: κ(complex, bit) at + (c\* − 10⁻²⁴, c\*) and even at (c\* − 10⁻²⁴, 3/1000) is below 1.1× selected (asserted). On the #1094 complex profile that is a net + saving of **≥ 511 rank-1 children** (510 fails), **≈ 3.55 units per call** over 144 calls. Two-call centre sharing + covers it with an additive rank-1 / rank-8 overhead of at most **4,079 rank-1 or 511 rank-8 children (≈ 28.3–28.4 + units per call)**, not the 30.5–30.8 PR1791 states for the selected bit endpoint. +- **Bit side: no admitted bit lever nets anything.** On the PR589 histogram (deficit 10,272, m = 64, W = 28,416, + T = 32 replicas, 288 stage calls, nine rank-7 copies per call, halving depth HD = 2), c\* needs a net saving of + **649 rank-1 children** (648 fails). Each bit lever in the table below (revision-3 catalogue) is changed one + premise at a time on the actual histogram, with the surcharge recomputed from the child count. cst is the copy-rank + sum per call (63 = 9 × 7). Every row below is a certified sign at c\* − 10⁻²⁴, c\* and c\* + 10⁻²⁴. The budgets + are sharp integers in the stated model: the stated count passes and one less fails (one more, for budgets). The + exceptions are marked: (c) is a necessary bound, (d) and (f) are sharp between an explicit hosting and the + concavity bound, and the TEMPLATE and width-7 trimmed brackets have no boundary in range. + +| Lever (one premise changed on the actual histogram) | Admitted today? | Net saving at c\* (rank-1 units) | Size that clears 649 | |---|---|---:|---| -| (a) Halving depth 3 / 4 (idle cap 45 → 50 / 53) | yes (r740 row bound) | **0 exactly** | none: the cap is slack | +| (a) Halving depth 3 / 4 (idle cap 45 → 50 / 53) | admissible under the merged r740 elementary-cover row bound (invoice not redone) | **0 exactly** | none: the cap is slack | | (a′) Width-8 re-hosting inside the actual idle windows | yes | **0 exactly** (record is optimal) | none | -| (b1) Rank-8 copy carriage, 9 copies per call (cst 63 → 72) | in (Bat) window | **−2,577.6** | none (makes things worse) | -| (b2) Fewer rank-7 copies | no (new decoder contract) | +2,008.8 for one fewer per call | **93 copies** record-wide (92 fails), i.e. one per call | +| (b1) Rank-8 copy carriage, 9 copies per call (cst 63 → 72) | allowed by format-limits' copy cap (copies up to rank 8) | **−2,577.6** | none (makes things worse) | +| (b2) Fewer rank-7 copies | no (new decoder contract) | +2,008.8 for one fewer per call | threshold **93 copies** record-wide (92 fails); a uniform decoder change removes 288 (one per call) | | (b3) Bit centre path shared by two calls (cst 31.5) | no (unconstructed) | **+9,039.5** | passes with overhead ≤ **8,391 rank-1 / 1,203 rank-7 / 201 rank-42** children (29.1–29.3 units per call) | -| (c) Second unpaid coordinate on F families | no (coverage-law change) | ≤ F | **F ≥ 649** of 28,416 (2.28%), necessary | -| (d) Pure helper deletion, most favorable (8 rank-1 climbs each), optimal width-8 re-hosting | no (PR1250: one removable helper) | +658.5 at d = 40 | **d = 40 per call** (39 fails for every hosting) | -| (d) Helper deletion, PR1043's measured delta | no | ≤ +169.8 | none: the model runs out of rank-7 climbs at d ≤ 19 | +| (c) Second unpaid coordinate on F families, pure removal (one unit per family, no reshaping) | no (coverage-law change) | ≤ F | **F ≥ 649** of 28,416 (2.28%), necessary in this model | +| (d) Pure helper deletion, most favorable (8 rank-1 climbs each), optimal width-8 re-hosting | no (see PR1250 below) | +658.5 at d = 40 | **d = 40 per call** (39 fails for every hosting) | +| (d) Helper deletion, PR1043's measured delta | no | +169.8 (explicit hosting), ≤ +170.4 (concavity bound) | none: the model runs out of rank-7 climbs at d = 19 (d = 10 if the 9 copies are kept) | +| (f) Width-7 helper conversion, #1023's placement, rank-1 child removed per helper | no (bit-width-seven-boundary: needs a changed prefix) | +656.0 at k = 71 | **k = 71 per call** (70 fails at the concavity bound) | +| (f) Width-7 conversion, largest local child trimmed per helper | no | +580.6 at k = 74 | none in this placement: fails at k = 74, when all 666 empty 7-slots per replica are used | | (e) Ideal in-window local shapes (single rank-7 data climbs, single rank-8 helper climbs) | no (no such word) | +3,647.6 in all 288 calls | **52 of 288 calls** (51 fails) | +(e) uses PR1334's most favorable in-window premise. PR1334's cruder "rank-8 children (window h = 8)" row and its +"rank-16 children (beyond the window)" row are not priced here. A same-loop float estimate, not certified, puts them +at about 50 and 34 calls; the rank-16 row needs longer windows, hence a different recipe. + **Conclusion.** No admitted bit lever nets anything at c\*. The admitted levers are the halving-depth cap raise, width-8 re-hosting and rank-8 copy carriage. Their nets are 0, 0 and −2,578, so any combination of them also fails. -Every lever that clears 649 changes the word, the decoder or the coverage law. The cheapest stated sizes are one -fewer rank-7 copy per call, 40 pure helper deletions per call (9.3% of 430) or the ideal local shapes in 52 calls. - -**Consequence for `centre-path-sharing`.** The catalogued route to +10% through two-call sharing is to share the -centre path **on both suppliers**. The bit-side copy of the same mechanism (row b3) has about 14× the needed saving. -Its overhead budget is ≈ 29.1–29.3 paid-mass units per call. With the complex side at c\* + 10⁻²⁴ and the bit side -at c\*, κ is still ≥ 1.1× selected (checked). The complex side's two-call overhead budget **at c\*** is -≤ 4,079 rank-1 or 511 rank-8 children in total: **≈ 28.3–28.4 units per call**. That is tighter than the -30.5–30.8 that PR1791 gives at the selected bit endpoint, which is the right figure only for the +3.45% cap. Without -a bit-side mechanism of one of the stated sizes, the card's stop rule holds for the catalogued lever set. +Every lever that clears 649 changes the word, the decoder or the coverage law. The stated sizes are: one fewer +rank-7 copy per call, 40 pure helper deletions per call (9.3% of the 430 helpers), 71 width-7 helpers per call in +the optimistic bracket of #1023's placement, the ideal local shapes in 52 calls, ≥ 649 doubly-unpaid families, or +bit-side two-call sharing within ≈ 29.1 units of overhead per call. + +**Consequence for `centre-path-sharing`.** At c\* the route needs a complex saving of ≥ 511 net rank-1 units +(≈ 3.55 per call), not PR1791's 1.33, plus one of the bit-side mechanisms above. Bit-side two-call sharing (row b3) +is the only clearing row that reuses a mechanism already constructed on the complex side (PR1708/PR1748). It has +about 14× the needed saving, with an overhead budget of ≈ 29.1–29.3 paid-mass units per call. Rows b2, c, d, e and +f also clear 649, each with a new decoder, coverage law or word of the stated size. With the complex side at +c\* + 10⁻²⁴ and the bit side at c\*, κ is still ≥ 1.1× selected (asserted). The complex overhead figure is an +additive rank-1 / rank-8 budget in PR1791's treatment. Mixed ranks allow more added mass: PR1888's mixed-rank +maxima reach 30.87 units per call at the selected bit endpoint, with rank-51 children. PR3075 charges the named +k = 2 costs at about 12 units per call, inside this budget, and reports that eligibility and demand coupling, not +the named costs, are the blocker. Without a bit-side mechanism of one of the stated sizes, the card's stop rule +holds for the catalogued lever set. ## Why the admitted levers give exactly zero (proof) @@ -49,15 +74,21 @@ a bit-side mechanism of one of the stated sizes, the card's stop rule holds for replica: ranks 14, 28, 42 for s = 1, 3, 5, then 7, 7, 7 for s = 2, 4, 6, then 42, 28, 14 (and one rank-0 event) at s = 8. Each event covers 2v = 222 coordinates. Per replica that gives windows {7: 666, 14: 444, 28: 444, 42: 444}. `verify.py` derives this from the recipe rules and checks that the record's idle part (profile minus 288 shipped -words) equals T × {2: 435, 4: 444, 6: 444, 7: 666, 42: 9}, the remainder left after hosting 9 × 439 width-8 helpers -per replica. +words) equals T × {2: 435, 4: 444, 6: 444, 7: 666, 42: 9}, the remainder left after hosting 9 × 439 width-8 residuals +per replica (439 = 430 helpers + 9 retained totals). **(a) The cap is slack.** HD = 2 caps children at 45, since 2r² < 64² ⇔ r ≤ 45. HD = 3 and 4 raise the cap to 50 and 53. But every idle child is a window remainder, at most the largest window 7(2K − 2) = 42, and every local -child has rank ≤ 7. So the record's max child is 42 < 45, and raising the halving depth admits no histogram the +child has rank ≤ 7. No idle child can span two consecutive windows of the same pair: the windows are delimited by +the recipe's bridges, each of which aligns the levels of two pairs and writes the source pair's coordinates. The +record already keeps pair 1's 14 and 7 windows (21 < 45) and pair 2's 28 and 7 windows (35 < 45) as separate +children at HD 2, so the split is structural, not a cap effect; pair 3's 42 + 7 = 49 likewise cannot merge under +the HD-3 cap of 50. So the record's max child is 42 < 45, and raising the halving depth admits no histogram the fixed windows can produce. Its net saving is exactly 0. Longer windows need a different recipe. In [bit589-recipe-floor](../bit589-recipe-floor/README.md) (PR1487)'s whole class of nine-stage recipes, that package -reports the longest advance as 2(K − 1) = 6 levels, i.e. a window of 42, so the cap is slack there too. +reports the longest advance as 2(K − 1) = 6 levels, i.e. a window of 42, so the cap is slack there too. In +particular, PR1334's cap-50/53 columns and its halving-depth-4 escape (145 ≥ 138) cannot be reached by any +nine-stage recipe. **(a′) Width-8 re-hosting cannot help.** A rank-r window holds at most ⌊r/8⌋ width-8 helpers. 8 divides no window rank, so every window keeps exactly one nonzero remainder child, and the child count (hence the surcharge) is fixed. @@ -73,13 +104,14 @@ constraints relaxed. The same bound holds record-wide (1,440 unused slots), so p help either. This re-certifies, at c\*, what our merged [bit589-width-packing](../bit589-width-packing/README.md) (#1023) proved at the selected endpoint. -**(b1) Copy carriage.** The decoder constant is the sum of the copy ranks: format-limits' T(2Kv − L·cst). With whole +**(b1) Copy carriage.** cst is the sum of the copy ranks (63), entering the deficit D = T(2Kv − L·cst). With whole copies, rank-8 carriage of the nine copies raises cst to 72 and the paid mass by 2,592. That increases the bill. PR1334's "rank-8 carriage" row kept cst = 63 with 63/8 fractional copies, which is the fewer-copies lever (b2). **(c) One unit of rank mass is worth at most one rank-1 child.** Trimming a rank-r child to r − 1 saves φ(r) − φ(r − 1) < φ(1), certified for r = 2..42 at c\*. Removing a rank-1 child also removes its surcharge. So F -doubly-unpaid families save at most F rank-1 children, and F ≥ 649 is necessary. +doubly-unpaid families save at most F rank-1 children, and F ≥ 649 is necessary, when each unpaid coordinate is a +pure removal of one unit of mass. Reshaping or merges that accompany the unpaid coordinate are outside this model. **(d) Deletion bounds.** For d deletions per call, the 45 + 9d unused slots per replica are priced two ways: - from below, by the concavity bound (all at the rank-42 per-slot cost, fractional); @@ -89,7 +121,19 @@ In the most favorable pure-deletion model each deleted helper removes 8 rank-1 c save. There the lower bound fails at d = 39 and the explicit hosting passes at d = 40. So 40 is sharp in the stage-relaxed slot model, and d ≤ 39 fails for every pure-deletion word. Deltas that also merge other climbs belong to lever (e); the [bit-deletion-ladder](../bit-deletion-ladder/README.md) (PR2465) notes that they can beat RANK1 -at equal mass. +at equal mass. PR1043's measured TEMPLATE delta consumes one rank-7 climb per deletion; the word's 19 rank-7 climbs +include its 9 rank-7 copies, so with the copies kept that model is exhausted at d = 10, and even consuming all 19 it +nets at most +170.4 (concavity bound; +169.8 with the explicit hosting). + +**(f) Width-7 conversion.** [bit589-width-packing](../bit589-width-packing/README.md) (#1023) prices helpers of +width 7 in a constructive placement: the 9k width-7 residuals per replica fill 9k of the 666 empty 7-slots exactly, +and the freed width-8 slack goes to emptied rank-42 windows. Its bracket removes one unit per converted helper either +as a rank-1 child (optimistic) or by trimming the largest local child (pessimistic). Here the slack is hosted as in +(d). In the optimistic bracket k = 71 per call passes with the explicit hosting and k = 70 fails at the concavity +bound. The pessimistic bracket fails at k = 74, when every empty 7-slot is used; beyond that, this placement does not +apply (#1023's all-439 slot-exact optimum is a different placement). The lever is not admitted: +[bit-width-seven-boundary](../bit-width-seven-boundary/README.md) (Ali Romman) shows that the selected PR589 word +cannot obtain width-7 helpers by replacing its cleanup alone; a changed prefix is needed. Linearity makes every budget sharp. f(a) = (1/(mW)) Σ n_r r (m/r)^a + c_s m^a with c_s = 32mN/(10¹⁶W) is affine in the counts, so each one-parameter family is monotone and the boundary is a single integer. @@ -97,16 +141,17 @@ the counts, so each one-parameter family is monotone and the boundary is a singl ## Second method [independent.py](independent.py) rebuilds every boundary histogram from the pinned PR589 and #1094 records with its -own code, requires byte-identical histograms, and recomputes all **40 signs**: 16 bit rows and 4 complex rows, each -at c\* and at c\* + 10⁻²⁴. It uses the separate interval arithmetic of our merged +own code, requires byte-identical histograms, and recomputes all **75 signs**: 19 bit rows, 4 complex budget rows and +the 2 complex need rows, each at c\* − 10⁻²⁴, c\* and c\* + 10⁻²⁴. It uses the separate interval arithmetic of our merged [bit-revision3-levers-seed03/levers.py](../bit-revision3-levers-seed03/levers.py) (PR1334): ln by atanh prime chains, exp by Taylor with a remainder bound, outward dyadic rounding. It also re-checks the re-hosting order and the trimming lemma. The primary [verify.py](verify.py) uses the D/E-diagnostic engine (PR1293, Navinor). The two -methods agree on every sign. +methods agree on every sign. Only the histogram code and the arithmetic are independent: the lever definitions, the +hosting model and the boundary integers (read from RESULT.json) are shared with verify.py. ## Reproduce -From the repository root (standard library and `git`; about 15 s): +From the repository root (standard library and `git`; under a minute, about 55 s for `verify.py` on a shared host): ```sh python3 -I -B research/bit-endpoint-lever-budgets/verify.py && python3 -I -B research/bit-endpoint-lever-budgets/independent.py @@ -115,8 +160,8 @@ python3 -I -B research/bit-endpoint-lever-budgets/verify.py && python3 -I -B res Expected output: ```text -PASS_BIT_ENDPOINT_LEVER_BUDGETS need_rank1=649 admitted_levers_max_net=0 copies_sharp=93 deletions_per_call=RANK1:40/TEMPLATE:None ideal_shape_calls=52 no_new_kappa -PASS_BIT_ENDPOINT_LEVER_BUDGETS_INDEPENDENT signs=40 at c* and c*+1e-24 (levers.py interval arithmetic) +PASS_BIT_ENDPOINT_LEVER_BUDGETS need_rank1=649 admitted_levers_max_net=0 copies_sharp=93 deletions_per_call=RANK1:40/TEMPLATE:None width7_per_call=71 ideal_shape_calls=52 complex_need_rank1=511 no_new_kappa +PASS_BIT_ENDPOINT_LEVER_BUDGETS_INDEPENDENT signs=75 at c*-1e-24, c* and c*+1e-24 (levers.py interval arithmetic) ``` `verify.py` regenerates [RESULT.json](RESULT.json) and requires byte equality (`--write` rewrites it). It refuses @@ -127,13 +172,17 @@ to run under `-O`. - the selected bit endpoint is accepted and its next grid point rejected; - the selected κ is recomputed; - c\* is the least grid point with κ ≥ 1.1× selected (and c\* − 10⁻²⁴ is not); +- the complex endpoint c\* is necessary: κ(c\* − 10⁻²⁴, c\*) and κ(c\* − 10⁻²⁴, 3/1000) are below the target; +- the admitted-lever maximum net (0) is computed from rows (a), (a′) and (b1), and (b1) is asserted negative; - the record fails at c\*; - the 649/648 rank-1 and 16 rank-42 requirements are re-derived. **Negative controls that must fail:** every "one less" boundary row (648 rank-1, 92 copies, 39 deletions, -51 reshaped calls) and every "one more" overhead row. [test_package.py](test_package.py) checks that tampering is -rejected by the independent method: -- off-by-one counts; +70 width-7 helpers, 51 reshaped calls, 510 complex rank-1) and every "one more" overhead row. Fail rows are checked at +c\* − 10⁻²⁴ as well, where monotonicity does not make the check automatic. [test_package.py](test_package.py) checks +that tampering is rejected by the independent method: +- off-by-one counts, including one consistent shift (requirement 648 with its rows rebuilt) that only the sign + arithmetic can catch; - a flipped verdict; - an edited histogram; - an edited complex verdict. @@ -155,6 +204,8 @@ python3 -I -B -m unittest discover -s research/bit-endpoint-lever-budgets -p tes - (b2), (b3), (c), (d) and (e) are pricing passes for hypothetical words or decoders. - (d)'s d = 40 pass is in the stage-relaxed slot model; its d ≤ 39 fail holds for every hosting. - (e) is the in-window ideal relaxation of PR1334, applied call by call. + - (f) is #1023's constructive 7-slot placement; its k = 70 fail is for every width-8 slack hosting in that + placement, not for every width-7 placement. - **Unpaid obligations of every passing row:** the word or decoder itself, then: - the dirty-input endpoint and restoration; - hosting under the real stage windows; @@ -172,35 +223,48 @@ python3 -I -B -m unittest discover -s research/bit-endpoint-lever-budgets -p tes ## Open next questions 1. **Can the bit centre path be shared by two calls within ≈ 29 units of overhead per call?** - - *Why it matters:* it is the only catalogued route on which centre sharing reaches +10%. The complex half must - also stay within ≈ 28.3 units per call at c\*. + - *Why it matters:* it is the only clearing row that reuses a mechanism already constructed on the complex side. + The complex half must then deliver ≥ 511 net rank-1 units at c\*, i.e. keep its additive rank-1/rank-8 overhead + within ≈ 28.3 units per call. - *First step:* write the bit analogue of PR1748's two-call reverse phase for the nine rank-7 copies of one replica, and price its restoration/hosting children. - *Blocked by:* no bit sharing word exists, and PR1748's ownership/sink blocker has no bit analogue yet. + [r439-copy-path-sharing-barrier](../r439-copy-path-sharing-barrier/README.md) (section T) records that the + nine retained totals read pairwise-disjoint source sets, which a sharing word must respect. 2. **Is there a decoder contract with eight retained totals (cst ≤ 56)?** - *Why it matters:* one fewer copy per call nets ≈ 2,009 units, 3.1× the requirement. - *First step:* test whether one of the nine retained totals of the v = 111 word can be recomputed instead of copied, and price the extra climbs. - *Blocked by:* a replacement contract for the decoder's copied totals (the `centre-path-sharing` card's - scope-change trigger). -3. **Which bit word reaches the 52-call reshaping or the 40-deletion size?** + scope-change trigger); r439-copy-path-sharing-barrier section T shows the totals' source sets are disjoint. +3. **Which bit word reaches the 52-call reshaping, the 40-deletion size or 71 width-7 helpers per call?** - *Why it matters:* these are the non-sharing alternatives. - - *First step:* measure the best per-call delta of PR1043-style deletions combined with climb merges. - - *Blocked by:* PR1250 found only one removable helper in the fixed word. + - *First step:* measure the best per-call delta of PR1043-style deletions combined with climb merges, or test the + six after-scatter width-7 survivors of bit-width-seven-boundary in a changed prefix. + - *Blocked by:* PR1250 found no further single deletion beyond PR1043 within arbitrary source XOR masks on the + fixed R439 word (sole survivor helper 470); it does not exclude simultaneous deletions. Width-7 helpers need a + changed prefix. ## Credit and provenance - **Requirement, endpoint and sharp-removal method:** rtyu193-rgb, `centre-sharing-overhead-budget` (PR1791, head `00d05a648985`). - **Moment enclosures:** Navinor, `selected-suppliers-de-diagnostic` (PR1293, head `85a361233431`). -- **Bootstrap/outer formulas:** Wronskode, `frontier1042-invoice-audit-seed81`. +- **Bootstrap/outer formulas:** Wronskode, `frontier1042-invoice-audit-seed81` (PR #1112). - **Independent arithmetic:** our merged `bit-revision3-levers-seed03` (PR1334, head `5ad74a4a04d1`). -- **Re-hosting optimality at the selected endpoint and the slot model:** our merged `bit589-width-packing` (#1023). -- **Deletion models:** our merged `bit-deletion-ladder` (PR2465, head `9494fc4e2ecd`), from Ali Romman's PR1043 delta. -- **Recipe class:** ianlibanio, `bit589-recipe-floor` (PR1487). -- **Halving-depth admission:** the r740 elementary-cover row bound authors. -- **Bit supplier:** DreamingOfClouds (PR589) and eumemic (PR555), with the PR510/PR463/PR442 template and hosting - lineage. +- **Re-hosting optimality at the selected endpoint, the slot model and the width-7 placement/bracket:** our merged + `bit589-width-packing` (#1023, head `babca68167d8`); earlier width-7 pricing by mightyOil (#1281). +- **Width-7 admission boundary:** Ali Romman, `bit-width-seven-boundary`. +- **Deletion models:** our merged `bit-deletion-ladder` (PR2465, head `9494fc4e2ecd`), from Ali Romman's PR1043 delta + (head `e309e17f83f5`); single-deletion scope from PR1250 (head `67667b11049e`). +- **Recipe class:** ianlibanio, `bit589-recipe-floor` (PR1487, head `cfd97ca1e9d3`). +- **Halving-depth admission:** the merged r740 elementary-cover row bound, + `research/e8-bit-carrier-skeleton/code/hub/r740-hosted-eleven/code/row_bound.py` (as cited by PR1334). +- **Complex overhead context:** RossRichardson, `centre-sharing-mixed-overhead` (PR1888, head `9c0fd1d20d33`); + navinor / Aaron Wang, `centre-shared-kcall-charged-seed615415` (PR3075, head `378b8e47fc01`); the two-call + mechanism PR1708/PR1748 (PR1748 head `ea14f191752c`); `r439-copy-path-sharing-barrier`. +- **Bit supplier:** DreamingOfClouds (PR589, head `a5afc8c6169e`) and eumemic (PR555, head `65a6bc19f820`), with the + PR510/PR463/PR442 template and hosting lineage. - **Selected construction:** Rohan Arun (#1094). All are loaded unchanged as pinned Git blobs. Predecessor code is reused without modification. diff --git a/research/bit-endpoint-lever-budgets/RESULT.json b/research/bit-endpoint-lever-budgets/RESULT.json index e8fb2ae93..8fbe8d07f 100644 --- a/research/bit-endpoint-lever-budgets/RESULT.json +++ b/research/bit-endpoint-lever-budgets/RESULT.json @@ -197,6 +197,48 @@ "label": "TEMPLATE: 19 deletions per call (model exhausted), concavity bound", "verdict": "fail" }, + { + "hist": { + "1": "360576", + "2": "396320", + "3": "22752", + "34": "32", + "4": "26880", + "42": "4352", + "5": "29376", + "6": "17376", + "7": "6336" + }, + "label": "width-7: 71 helpers per call, rank-1 removed, explicit hosting", + "verdict": "pass" + }, + { + "hist": { + "1": "360864", + "2": "396384", + "3": "22752", + "4": "26880", + "42": "4320", + "5": "29376", + "6": "17376", + "7": "6624" + }, + "label": "width-7: 70 helpers per call, rank-1 removed, concavity bound", + "verdict": "fail" + }, + { + "hist": { + "1": "381024", + "2": "1980768/5", + "3": "22752", + "4": "39552", + "42": "22752/5", + "5": "19872", + "6": "19680" + }, + "label": "width-7: 74 helpers per call, largest trimmed, concavity bound", + "verdict": "fail" + }, { "hist": { "1": "312228", @@ -301,12 +343,19 @@ } } }, + "context_complex_at_c_star_need": { + "calls": 144, + "net_rank1_children": 511, + "note": "PR1791 OQ1's >= 1.33 units per call holds only at the selected bit endpoint; at c* the complex side needs this net saving", + "per_call": 3.549 + }, "controls": [ "F equals the pinned D/E-diagnostic bill on the record", "selected bit endpoint accepted, next grid rejected", "selected kappa recomputed", "c* is the least grid point with kappa >= 1.1 x selected (complex at 3/1000)", "complex endpoint c* + 1e-24 with bit endpoint c* already gives kappa >= 1.1 x selected", + "complex endpoint c* - 1e-24 fails the target with bit at c* and even with bit at 3/1000", "the record fails at c*" ], "endpoint": { @@ -430,10 +479,15 @@ }, "TEMPLATE": { "exhausted_at": 19, - "net_rank1_units_at_exhaustion": [ + "net_rank1_units_at_exhaustion_explicit_hosting": [ 169.8356703347478, 169.8356703347478 ], + "net_rank1_units_at_exhaustion_upper_bound": [ + 170.39130761908615, + 170.39130761908615 + ], + "note": "the model's 19 rank-7 climbs include the 9 rank-7 copies; with copies kept it is exhausted at d = 10", "of_helpers": 430, "per_call": null } @@ -451,6 +505,27 @@ "of_calls": 288, "sharp_calls": 52 }, + "lever_f_width7": { + "admitted": false, + "largest_trimmed": { + "fails_at": 74, + "net_rank1_units_at_max": [ + 580.5954304386772, + 580.5954304386772 + ], + "per_call": null + }, + "max_per_call_in_this_placement": 74, + "placement": "#1023: width-7 residuals in empty 7-slots, width-8 slack in emptied rank-42 windows", + "rank1_removed": { + "net_rank1_units": [ + 656.0393819674475, + 656.0393819674475 + ], + "sharp_per_call": 71, + "total": 20448 + } + }, "record": { "T": 32, "W": 28416, diff --git a/research/bit-endpoint-lever-budgets/TASK.json b/research/bit-endpoint-lever-budgets/TASK.json index a655a7d5e..af8307ea7 100644 --- a/research/bit-endpoint-lever-budgets/TASK.json +++ b/research/bit-endpoint-lever-budgets/TASK.json @@ -41,33 +41,33 @@ ] }, "scope_status": "changed", - "actual_scope": "Sharp integer pricing, at the +10% bit endpoint c* = 921658892752012102303/5e23 of centre-sharing-overhead-budget, of each catalogued revision-3 bit lever changed one premise at a time on the actual PR589 histogram (surcharge recomputed): halving-depth cap raise, width-8 re-hosting in the actual idle windows, copy carriage/count, two-call bit centre sharing with its overhead budget, unpaid coordinates, helper deletion (two local models, optimal re-hosting) and ideal local shapes; plus the complex-side two-call overhead budget at the same endpoint. Second method: levers.py interval arithmetic on independently rebuilt histograms.", + "actual_scope": "Requirement map of the +10% two-call centre-sharing route at c* = 921658892752012102303/5e23 (centre-sharing-overhead-budget, PR1791). Complex side: the complex endpoint must itself reach c* (asserted), a net saving of >= 511 rank-1 children (about 3.55 units per call), correcting PR1791 OQ1's 1.33 units per call; additive rank-1/rank-8 two-call overhead budget at c*. Bit side: sharp integer pricing of each listed revision-3 bit lever, one premise at a time on the actual PR589 histogram (surcharge recomputed): halving-depth cap raise, width-8 re-hosting, copy carriage/count, two-call bit centre sharing with its overhead budget, unpaid coordinates (pure removal), helper deletion (two local models), width-7 helper conversion (#1023's placement and bracket) and ideal local shapes. Second method: levers.py interval arithmetic on independently rebuilt histograms.", "scope_change_reason": "The card's H2/K helper-interface question is saturated by other packages; this answers the explicit, unowned open question 1 of centre-sharing-overhead-budget (PR1791), which decides whether the strongest complex lever (two-call centre sharing) can be part of a +10% route. That needs a bit lever netting at least 649 rank-1 units on the actual histogram, which no package had priced.", - "bottleneck_link": "Two-call centre sharing makes the bit side bind; +10% kappa needs the bit endpoint 0.0018433. No admitted bit lever nets anything there (halving-depth cap slack at max window 42, record hosting optimal, rank-8 carriage loses 2,578 units); clearing 649 needs a new word/decoder: one fewer rank-7 copy per call, bit-side two-call centre sharing (overhead <= ~29.1 units/call), >= 40 pure helper deletions per call, >= 649 doubly-unpaid families, or ideal shapes in >= 52 of 288 calls. The complex half of the route must keep its sharing overhead <= ~28.3 units/call at that endpoint. No kappa claim.", + "bottleneck_link": "Two-call centre sharing makes the bit side bind; +10% kappa needs both endpoints at 0.0018433. The complex side then needs >= 511 net rank-1 units (about 3.55 per call; overhead <= about 28.3 units per call in the additive rank-1/rank-8 model), not PR1791's 1.33. On the bit side no admitted lever nets anything (halving-depth cap slack at max window 42, record hosting optimal, rank-8 carriage loses 2,578 units); clearing 649 needs a new word, decoder or coverage law: one fewer rank-7 copy per call (threshold 93 record-wide), bit-side two-call centre sharing (overhead <= about 29.1 units per call), >= 40 pure helper deletions per call, 71 width-7 helpers per call (optimistic bracket of #1023's placement), >= 649 doubly-unpaid families, or ideal shapes in >= 52 of 288 calls. No kappa claim.", "budget_minutes": 90, - "stop_rule": "Stop once the lever table is exact and the primary (D/E-diagnostic engine) and independent (levers.py) methods agree on every pass/fail sign at c* and c* + 1e-24; build no construction and search for no new bit word.", + "stop_rule": "Stop once the lever table is exact and the primary (D/E-diagnostic engine) and independent (levers.py) methods agree on every pass/fail sign at c* - 1e-24, c* and c* + 1e-24; build no construction and search for no new bit word.", "outcome": "completed", - "evidence": "RESULT.json: requirement 649 rank-1 (648 fails) / 16 rank-42; (a) caps 45/50/53, max child 42 = max window, net 0; (a') per-slot costs 7.94284 < 7.94625 < 7.95184 rank-1 units, record optimal, net 0; (b1) cst 72: -2577.6; (b2) 93 copies sharp (92 fails), one fewer per call +2008.8; (b3) cst 31.5: +9039.5, overhead budget 8391 rank-1 / 1203 rank-7 / 201 rank-42; (c) F >= 649 families; (d) RANK1 40 per call (39 fails for every hosting), TEMPLATE exhausted by d = 19 at +169.8; (e) 52 of 288 calls (51 fails), all calls +3647.6; complex k=2 overhead at c*: 4079 rank-1 / 511 rank-8 (28.3-28.4 units per call). 40 signs reproduced by independent.py.", + "evidence": "RESULT.json: requirement 649 rank-1 (648 fails) / 16 rank-42; complex need at c* 511 rank-1 (510 fails), 3.549 per call; (a) caps 45/50/53, max child 42 = max window, net 0; (a') per-slot costs 7.94284 < 7.94625 < 7.95184 rank-1 units, record optimal, net 0; (b1) cst 72: -2577.6; (b2) 93 copies threshold (92 fails), one fewer per call +2008.8; (b3) cst 31.5: +9039.5, overhead budget 8391 rank-1 / 1203 rank-7 / 201 rank-42; (c) F >= 649 families (pure removal); (d) RANK1 40 per call (39 fails for every hosting), TEMPLATE exhausted by d = 19 at +169.8 (explicit hosting), <= +170.4 (concavity bound); (f) width-7 rank-1-removed 71 per call (70 fails), +656.0; largest-trimmed fails at 74 (+580.6); (e) 52 of 288 calls (51 fails), all calls +3647.6; complex k=2 overhead at c*: 4079 rank-1 / 511 rank-8 (28.3-28.4 units per call). 75 signs reproduced by independent.py at c* - 1e-24, c* and c* + 1e-24.", "author": "Sagar Thakrar (thakrarsagar)", "ai_assistance": "Claude (Anthropic, Claude Opus 5.5) via Claude Code scoped the question and wrote the code and prose in one session of an automated research loop; checked only by AI review passes in the same loop, no independent human review.", "open_questions": [ { "question": "Can the bit centre path be shared by two calls within about 29 paid-mass units of overhead per call (8,391 rank-1 / 1,203 rank-7 / 201 rank-42 children in total)?", - "why_it_matters": "It is the only catalogued route on which centre sharing reaches +10% kappa; the complex half must also stay within about 28.3 units per call at c*.", + "why_it_matters": "It is the only clearing row that reuses a mechanism already constructed on the complex side (PR1708/PR1748); the complex half must then deliver >= 511 net rank-1 units at c*, i.e. keep its additive rank-1/rank-8 overhead within about 28.3 units per call.", "first_step": "Write the bit analogue of PR1748's two-call reverse phase for the nine rank-7 copies of one replica and price its restoration and hosting children.", - "blocked_by": "No bit sharing word exists, and PR1748's ownership/sink blocker has no bit analogue yet." + "blocked_by": "No bit sharing word exists, PR1748's ownership/sink blocker has no bit analogue yet, and r439-copy-path-sharing-barrier (section T) shows the nine retained totals read pairwise-disjoint source sets." }, { "question": "Is there a decoder contract with eight retained totals (cst <= 56 per call)?", "why_it_matters": "One fewer rank-7 copy per call nets about 2,009 rank-1 units, 3.1x the requirement.", "first_step": "Test whether one of the nine retained totals of the v = 111 word can be recomputed instead of copied, and price the extra climbs.", - "blocked_by": "A replacement contract for the decoder's copied totals (the centre-path-sharing card's scope-change trigger)." + "blocked_by": "A replacement contract for the decoder's copied totals (the centre-path-sharing card's scope-change trigger); r439-copy-path-sharing-barrier section T shows the totals' source sets are disjoint." }, { - "question": "Which bit word reaches the 52-call reshaping or the 40-deletion size?", + "question": "Which bit word reaches the 52-call reshaping, the 40-deletion size or 71 width-7 helpers per call?", "why_it_matters": "These are the non-sharing alternatives for the bit half of a +10% route.", - "first_step": "Measure the best per-call delta of PR1043-style deletions combined with climb merges.", - "blocked_by": "PR1250 found only one removable helper in the fixed word." + "first_step": "Measure the best per-call delta of PR1043-style deletions combined with climb merges, or test the six after-scatter width-7 survivors of bit-width-seven-boundary in a changed prefix.", + "blocked_by": "PR1250 found no further single deletion beyond PR1043 within arbitrary source XOR masks on the fixed R439 word (it does not exclude simultaneous deletions); width-7 helpers need a changed prefix (bit-width-seven-boundary)." } ] } diff --git a/research/bit-endpoint-lever-budgets/VERIFY.json b/research/bit-endpoint-lever-budgets/VERIFY.json index 2cd75f0d5..427801a26 100644 --- a/research/bit-endpoint-lever-budgets/VERIFY.json +++ b/research/bit-endpoint-lever-budgets/VERIFY.json @@ -20,7 +20,7 @@ "{package}/verify.py" ], "timeout_seconds": 300, - "checks": "Endpoint, kappa and +10% controls; re-derived 649/16 requirement; window derivation and idle-remainder identity; slack halving cap; certified re-hosting order; sharp copy, sharing-budget, deletion and reshaping boundaries; complex k=2 budget at c*; every boundary sign also at c*+1e-24; RESULT.json byte comparison." + "checks": "Endpoint, kappa and +10% controls, including necessity of the complex endpoint c*; re-derived 649/16 requirement and complex 511 need; window derivation and idle-remainder identity; slack halving cap; certified re-hosting order; sharp copy, sharing-budget, deletion, width-7 and reshaping boundaries; complex k=2 budget at c*; every boundary sign also at c*-1e-24 and c*+1e-24; RESULT.json byte comparison." }, { "argv": [ @@ -30,7 +30,7 @@ "{package}/independent.py" ], "timeout_seconds": 120, - "checks": "Rebuilds every boundary histogram independently, requires equality with RESULT.json, and recomputes all 40 signs at c* and c*+1e-24 with levers.py interval arithmetic." + "checks": "Rebuilds every boundary histogram independently, requires equality with RESULT.json, and recomputes all 75 signs at c*-1e-24, c* and c*+1e-24 with levers.py interval arithmetic." }, { "argv": [ @@ -46,7 +46,7 @@ "test_package.py" ], "timeout_seconds": 120, - "checks": "Tampered counts, verdicts and histograms are rejected by the independent method." + "checks": "Tampered counts, verdicts and histograms, including a consistent shift, are rejected by the independent method." } ] } diff --git a/research/bit-endpoint-lever-budgets/independent.py b/research/bit-endpoint-lever-budgets/independent.py index ecacce294..e3773c3e5 100644 --- a/research/bit-endpoint-lever-budgets/independent.py +++ b/research/bit-endpoint-lever-budgets/independent.py @@ -3,9 +3,11 @@ """Independent second method for bit-endpoint-lever-budgets. Rebuilds every boundary histogram from the pinned PR589 and #1094 records with its own code, checks that it equals -the histogram in RESULT.json, and recomputes each pass/fail sign at c* and at c* + 1e-24 with the separate interval -arithmetic of bit-revision3-levers-seed03/levers.py (ln by atanh prime chains, exp by Taylor with a remainder bound, -outward dyadic rounding). It shares no arithmetic with verify.py, which uses the D/E-diagnostic engine. +the histogram in RESULT.json, and recomputes each pass/fail sign at c* - 1e-24, c* and c* + 1e-24 with the separate +interval arithmetic of bit-revision3-levers-seed03/levers.py (ln by atanh prime chains, exp by Taylor with a remainder +bound, outward dyadic rounding). It shares no arithmetic with verify.py, which uses the D/E-diagnostic engine. The +lever definitions, the hosting model and the boundary integers (read from RESULT.json) are shared with verify.py; only +the histogram code and the arithmetic are independent. Standard library and git only. Prepared by Sagar Thakrar (thakrarsagar) with substantial AI assistance from Claude (Anthropic, Claude Opus 5.5). @@ -76,8 +78,8 @@ def bit_sign(h, a): k = res["lever_e_local_shape"]["sharp_calls"] shared = shift(H0, r7=-1296) - def deletion(delta, d, upper): - h = dict(H0) + def deletion(delta, d, upper, base=None): + h = dict(base or H0) for r, n in delta.items(): h = shift(h, **{"r%d" % r: calls * d * n}) s = 45 + 9 * d @@ -87,6 +89,21 @@ def deletion(delta, d, upper): h = shift(h, r42=T * (n - 9), r2=-T * (n - 9)) return shift(h, **{"r%d" % (2 + 8 * s0): T, "r2": -T}) if s0 else h + def trimmed(k): + """#1023's pessimistic bracket: trim one unit from the k largest local children of every call.""" + h, left = dict(H0), k + for r in sorted(word, reverse=True): + t = min(left, word[r]) + h = shift(h, **{"r%d" % r: -calls * t}) + if r > 1: + h = shift(h, **{"r%d" % (r - 1): calls * t}) + left -= t + if not left: + return h + + w7 = res["lever_f_width7"] + k7, kmax = w7["rank1_removed"]["sharp_per_call"], w7["max_per_call_in_this_placement"] + assert kmax == 666 // 9 == w7["largest_trimmed"]["fails_at"] ideal_delta = {1: -1323, 2: -1342, 3: -79, 4: -44, 5: -102, 6: -11, 7: 212, 8: 439} def reshaped(kk): @@ -103,13 +120,15 @@ def reshaped(kk): mine += [(shift(shared, **{"r" + r: y}), "pass"), (shift(shared, **{"r" + r: y + 1}), "fail")] mine += [(deletion({1: -8}, d40, True), "pass"), (deletion({1: -8}, d40 - 1, False), "fail"), (deletion({1: -2, 2: 2, 3: -1, 7: -1}, dT, False), "fail"), + (deletion({1: -1, 7: -1}, k7, True), "pass"), (deletion({1: -1, 7: -1}, k7 - 1, False), "fail"), + (deletion({7: -1}, kmax, False, base=trimmed(kmax)), "fail"), (reshaped(k), "pass"), (reshaped(k - 1), "fail")] recorded = res["boundary_checks"] assert len(recorded) == len(mine), "boundary row count" for (h, v), row in zip(mine, recorded): assert {str(r): str(n) for r, n in sorted(h.items())} == row["hist"], "histogram rebuilt differently: " + row["label"] assert row["verdict"] == v - for a in (c, c + GRID): + for a in (c - GRID, c, c + GRID): assert bit_sign(h, a) == v, "independent sign differs: %s at %s" % (row["label"], a) # The TEMPLATE deletion model really is exhausted: its rank-7 consumption equals the word's 19 rank-7 climbs. @@ -136,11 +155,17 @@ def ch(r, a): h[8] = Q(576) h[r] = h.get(r, Q(0)) + y assert {str(q): int(n) for q, n in sorted(h.items())} == row["hist"], "complex histogram: " + row["label"] - for a in (c, c + GRID): + for a in (c - GRID, c, c + GRID): assert lv.verdict(h, 73, Q(14336), a) == row["verdict"], "complex sign: " + row["label"] + need = res["context_complex_at_c_star_need"]["net_rank1_children"] + for x, v in ((need, "pass"), (need - 1, "fail")): + h = dict(HC) + h[1] -= x + for a in (c - GRID, c, c + GRID): + assert lv.verdict(h, 73, Q(14336), a) == v, "complex need sign: %d at %s" % (x, a) - print("PASS_BIT_ENDPOINT_LEVER_BUDGETS_INDEPENDENT signs=%d at c* and c*+1e-24 (levers.py interval arithmetic)" - % (2 * (len(recorded) + len(res["context_complex_at_c_star"]["boundary_checks"])))) + print("PASS_BIT_ENDPOINT_LEVER_BUDGETS_INDEPENDENT signs=%d at c*-1e-24, c* and c*+1e-24 (levers.py interval arithmetic)" + % (3 * (len(recorded) + len(res["context_complex_at_c_star"]["boundary_checks"]) + 2))) if __name__ == "__main__": diff --git a/research/bit-endpoint-lever-budgets/test_package.py b/research/bit-endpoint-lever-budgets/test_package.py index 7bc03a2c3..b6781a39f 100644 --- a/research/bit-endpoint-lever-budgets/test_package.py +++ b/research/bit-endpoint-lever-budgets/test_package.py @@ -32,6 +32,13 @@ def test_rejections(self): "bit sharing budget +1": lambda r: r["lever_b_copy_charge"]["two_call_bit_centre_sharing"]["overhead_budget"]["1"].update(total=8392), "flipped recorded verdict": lambda r: r["boundary_checks"][2].update(verdict="pass"), "edited histogram": lambda r: r["boundary_checks"][0]["hist"].update({"42": "289"}), + "consistent shift: requirement 648 with rows rebuilt": lambda r: ( + r["requirement"].update(rank1_children=648), + r["boundary_checks"][0].update(hist=r["boundary_checks"][1]["hist"]), + r["boundary_checks"][1].update(hist=dict(r["boundary_checks"][1]["hist"], + **{"1": str(int(r["boundary_checks"][1]["hist"]["1"]) + 1)}))), + "width-7 one helper fewer": lambda r: r["lever_f_width7"]["rank1_removed"].update(sharp_per_call=70), + "complex need 510": lambda r: r["context_complex_at_c_star_need"].update(net_rank1_children=510), "complex budget +1": lambda r: r["context_complex_at_c_star"]["boundary_checks"][0].update(verdict="fail"), } for name, edit in edits.items(): diff --git a/research/bit-endpoint-lever-budgets/verify.py b/research/bit-endpoint-lever-budgets/verify.py index 2b41a8469..5c14a0762 100644 --- a/research/bit-endpoint-lever-budgets/verify.py +++ b/research/bit-endpoint-lever-budgets/verify.py @@ -9,7 +9,8 @@ (Wronskode's frontier1042-invoice-audit-seed81) are loaded unchanged as pinned Git blobs at BASE, as in centre-sharing-overhead-budget. The bit bill is f(a) = (1/(mW)) sum_r n_r r (m/r)^a + c_s m^a with the surcharge c_s = 32 m N / (1e16 W) recomputed from each histogram's child count N. It is linear in the counts n_r, so every -budget below is a sharp integer: the stated count passes the exact test f(c*) < 1 and one less fails. +budget below is a sharp integer in its stated model: the stated count passes the exact test f(c*) < 1 and +one less fails (README lists the bounded exceptions). Standard library and git only. Prepared by Sagar Thakrar (thakrarsagar) with substantial AI assistance from Claude (Anthropic, Claude Opus 5.5). @@ -166,11 +167,14 @@ def kappa(b, c): target = k_sel * Q(11, 10) assert kappa(B_CERTIFIED_K2, C_STAR) >= target > kappa(B_CERTIFIED_K2, C_STAR - GRID), "c* is the +10% endpoint" assert kappa(C_STAR + GRID, C_STAR) >= target, "complex accepted at c* + 1e-24 suffices with bit at c*" + assert kappa(C_STAR, C_STAR) >= target > kappa(C_STAR - GRID, C_STAR), "complex endpoint c* is necessary" + assert target > kappa(C_STAR - GRID, B_CERTIFIED_K2), "complex below c* fails even with bit at 3/1000" assert verdict(H, C_STAR) == "fail", "the record fails at c*" out["controls"] = ["F equals the pinned D/E-diagnostic bill on the record", "selected bit endpoint accepted, next grid rejected", "selected kappa recomputed", "c* is the least grid point with kappa >= 1.1 x selected (complex at 3/1000)", "complex endpoint c* + 1e-24 with bit endpoint c* already gives kappa >= 1.1 x selected", + "complex endpoint c* - 1e-24 fails the target with bit at c* and even with bit at 3/1000", "the record fails at c*"] # ---- Baseline requirement (predecessor's sharp removal, re-derived) ------------------------------------ @@ -239,9 +243,11 @@ def kappa(b, c): record("two-call sharing + %d rank-%d overhead" % (y, r), add(shared, {r: y}), "pass") record("two-call sharing + %d rank-%d overhead" % (y + 1, r), add(shared, {r: y + 1}), "fail") budget[str(r)] = dict(total=y, per_call=round(y / calls, 3), mass_per_call=round(y * r / calls, 3)) + b1_net = units_saved(b1) + assert b1_net[1] < 0, "rank-8 carriage must lose" out["lever_b_copy_charge"] = dict( copies=copies, cst_per_call=63, - rank8_carriage=dict(cst_per_call=72, deficit=info["deficit"] - copies, net_rank1_units=units_saved(b1)), + rank8_carriage=dict(cst_per_call=72, deficit=info["deficit"] - copies, net_rank1_units=b1_net), fewer_copies=dict(sharp_total_copies=x_star, per_call_uniform=1, deficit_one_fewer_per_call=info["deficit"] + 7 * calls, net_rank1_units_one_fewer_per_call=units_saved(one_per_call)), two_call_bit_centre_sharing=dict(cst_per_call=31.5, copies_removed=copies // 2, @@ -256,8 +262,8 @@ def kappa(b, c): note="necessary for any u-lever; sufficient only if every saved unit is a rank-1 child") # ---- (d) helper deletions with optimal width-8 re-hosting (stage-relaxed slot model) --------------------- - def deletion(model, d, upper): - h = add(H, DELETION_MODELS[model], calls * d) + def rehosted(h, d, upper): + """Host the 45 + 9d spare width-8 slots per replica: explicit (upper) or concavity lower bound.""" s = spare + 9 * d # spare slots per replica if not upper: # fractional concavity bound (lower bill) return add(h, {42: Q(T * 9 * d, 5), 2: -Q(T * 9 * d, 5)}) @@ -265,6 +271,9 @@ def deletion(model, d, upper): assert n + (s0 > 0) <= windows[42] h = add(h, {42: T * (n - 9), 2: -T * (n - 9)}) return add(h, {2 + 8 * s0: T, 2: -T}) if s0 else h + + def deletion(model, d, upper): + return rehosted(add(H, DELETION_MODELS[model], calls * d), d, upper) assert deletion("RANK1", 0, True) == deletion("RANK1", 0, False) == H dels = {} for model, dm in DELETION_MODELS.items(): @@ -277,7 +286,10 @@ def deletion(model, d, upper): record("%s: %d deletions per call (model exhausted), concavity bound" % (model, d_max), deletion(model, d_max, False), "fail") dels[model] = dict(per_call=None, exhausted_at=d_max, of_helpers=430, - net_rank1_units_at_exhaustion=units_saved(deletion(model, d_max, True))) + net_rank1_units_at_exhaustion_explicit_hosting=units_saved(deletion(model, d_max, True)), + net_rank1_units_at_exhaustion_upper_bound=units_saved(deletion(model, d_max, False)), + note="the model's 19 rank-7 climbs include the 9 rank-7 copies; with copies kept it " + "is exhausted at d = 10") continue assert verdict(deletion(model, d - 1, False), C_STAR) == "fail", "deletion boundary not sharp: " + model record("%s: %d deletions per call, explicit hosting" % (model, d), deletion(model, d, True), "pass") @@ -287,6 +299,42 @@ def deletion(model, d, upper): out["lever_d_helper_deletion"] = dict(models={k: {str(r): n for r, n in v.items()} for k, v in DELETION_MODELS.items()}, sharp=dels, known_removable_helpers_of_the_fixed_word=1) + # ---- (f) width-7 helper conversion (#1023's constructive placement and bracket) -------------------------- + def width7(k, upper, pes=False): + """k helpers per call converted to width 7: one unit removed from one local child per converted helper + (rank-1 child removed, or largest child trimmed: #1023's bracket); the 9k width-7 residuals per replica fill + 9k empty 7-slots exactly; the freed width-8 slack is hosted as in (d).""" + assert 9 * k <= windows[7], "this placement uses empty 7-slots only" + delta, left = Counter({1: -k}), k + if pes: + delta = Counter() + for r in sorted(local, reverse=True): + take = min(left, local[r]) + delta[r] -= take + delta[r - 1] += take if r > 1 else 0 + left -= take + if not left: + break + assert left == 0 + delta[7] -= k + return rehosted(add(H, delta, calls), k, upper) + assert width7(0, True) == width7(0, False) == width7(0, True, True) == H + kmax = windows[7] // 9 + k7 = 0 + while k7 <= kmax and verdict(width7(k7, True), C_STAR) != "pass": + assert verdict(width7(k7, False), C_STAR) == "fail" + k7 += 1 + assert k7 <= kmax and verdict(width7(k7 - 1, False), C_STAR) == "fail" + record("width-7: %d helpers per call, rank-1 removed, explicit hosting" % k7, width7(k7, True), "pass") + record("width-7: %d helpers per call, rank-1 removed, concavity bound" % (k7 - 1), width7(k7 - 1, False), "fail") + record("width-7: %d helpers per call, largest trimmed, concavity bound" % kmax, width7(kmax, False, True), "fail") + out["lever_f_width7"] = dict( + placement="#1023: width-7 residuals in empty 7-slots, width-8 slack in emptied rank-42 windows", + max_per_call_in_this_placement=kmax, + rank1_removed=dict(sharp_per_call=k7, total=calls * k7, net_rank1_units=units_saved(width7(k7, True))), + largest_trimmed=dict(per_call=None, fails_at=kmax, net_rank1_units_at_max=units_saved(width7(kmax, True, True))), + admitted=False) + # ---- (e) local rank shape: replace the shipped word by the ideal in-window shapes in k calls ------------- ideal = {7: 2 * V + 9, 8: R} assert sum(r * n for r, n in ideal.items()) == 5129 @@ -317,18 +365,34 @@ def cverdict(h, a): lo, hi = (mid, hi) if cverdict(add(shared_c, {r: mid}), C_STAR) == "pass" else (lo, mid) for y, v in ((lo, "pass"), (lo + 1, "fail")): h = add(shared_c, {r: y}) - assert cverdict(h, C_STAR) == v and cverdict(h, C_STAR + GRID) == v + assert all(cverdict(h, cs) == v for cs in (C_STAR - GRID, C_STAR, C_STAR + GRID)) complex_boundary.append(dict(label="complex two-call sharing + %d rank-%d overhead" % (y, r), hist={str(q): n for q, n in sorted(h.items())}, verdict=v)) complex_budget[str(r)] = dict(total=lo, per_call=round(lo / NC, 3), mass_per_call=round(lo * r / NC, 3)) + cneed = 0 + lo, hi = 0, 2000 + assert cverdict(add(HC, {1: -hi}), C_STAR) == "pass" + while hi - lo > 1: + mid = (lo + hi) // 2 + lo, hi = (mid, hi) if cverdict(add(HC, {1: -mid}), C_STAR) == "fail" else (lo, mid) + cneed = hi + for cs in (C_STAR - GRID, C_STAR, C_STAR + GRID): + assert cverdict(add(HC, {1: -cneed}), cs) == "pass" and cverdict(add(HC, {1: -(cneed - 1)}), cs) == "fail" + out["context_complex_at_c_star_need"] = dict(net_rank1_children=cneed, calls=NC, per_call=round(cneed / NC, 3), + note="PR1791 OQ1's >= 1.33 units per call holds only at the selected " + "bit endpoint; at c* the complex side needs this net saving") out["context_complex_at_c_star"] = dict(model="centre-sharing-overhead-budget k=2: 1152 -> 576 rank-8 centre children", overhead_budget=complex_budget, boundary_checks=complex_boundary) - # ---- Adjacent grid point: every boundary verdict is unchanged at c* + 1e-24 ---------------------------- + # ---- Adjacent grid points: every boundary verdict is unchanged at c* - 1e-24 and c* + 1e-24 ------------ for b in boundary: h = {int(r): Q(n) for r, n in b["hist"].items()} - assert verdict(h, C_STAR + GRID) == b["verdict"], "next-grid verdict: " + b["label"] + for cs in (C_STAR - GRID, C_STAR + GRID): + assert verdict(h, cs) == b["verdict"], "adjacent-grid verdict: %s at %s" % (b["label"], cs) out["boundary_checks"] = boundary + admitted_max = max(out["lever_a_idle_cap"]["net_rank1_units_hd3"], out["lever_a_idle_cap"]["net_rank1_units_hd4"], + out["lever_a_idle_cap"]["rehost_net_rank1_units"], b1_net[1]) + assert admitted_max == 0 out["status"] = "PASS_BIT_ENDPOINT_LEVER_BUDGETS" text = json.dumps(out, indent=1, sort_keys=True) + "\n" @@ -338,8 +402,10 @@ def cverdict(h, a): print("WROTE", path.relative_to(ROOT).as_posix()) else: assert path.read_text(encoding="utf-8") == text, "RESULT.json differs from the regenerated result" - print("%s need_rank1=%d admitted_levers_max_net=0 copies_sharp=%d deletions_per_call=%s ideal_shape_calls=%d no_new_kappa" - % (out["status"], need1, x_star, "/".join("%s:%s" % (k, v["per_call"]) for k, v in dels.items()), k_star)) + print("%s need_rank1=%d admitted_levers_max_net=%d copies_sharp=%d deletions_per_call=%s width7_per_call=%d " + "ideal_shape_calls=%d complex_need_rank1=%d no_new_kappa" + % (out["status"], need1, admitted_max, x_star, "/".join("%s:%s" % (k, v["per_call"]) for k, v in dels.items()), + k7, k_star, cneed)) if __name__ == "__main__": From 5505853988cfc05bc8ad9bfcf07879727932b0d5 Mon Sep 17 00:00:00 2001 From: Sagar Thakrar <18622288+thakrarsagar@users.noreply.github.com> Date: Mon, 19 Oct 2026 11:38:16 +0530 Subject: [PATCH 3/3] Revise bit-endpoint-lever-budgets (round 2): width-7 row scoped window-free per PR1736, drop 'only' claim, review fixes Co-Authored-By: Claude Opus 5.5 --- research/bit-endpoint-lever-budgets/README.md | 80 ++++++++++++------- .../bit-endpoint-lever-budgets/RESULT.json | 7 +- research/bit-endpoint-lever-budgets/TASK.json | 14 ++-- research/bit-endpoint-lever-budgets/verify.py | 10 ++- 4 files changed, 68 insertions(+), 43 deletions(-) diff --git a/research/bit-endpoint-lever-budgets/README.md b/research/bit-endpoint-lever-budgets/README.md index 1a29a0e50..83f600718 100644 --- a/research/bit-endpoint-lever-budgets/README.md +++ b/research/bit-endpoint-lever-budgets/README.md @@ -41,30 +41,35 @@ requirement map of that route on the actual histograms. | (c) Second unpaid coordinate on F families, pure removal (one unit per family, no reshaping) | no (coverage-law change) | ≤ F | **F ≥ 649** of 28,416 (2.28%), necessary in this model | | (d) Pure helper deletion, most favorable (8 rank-1 climbs each), optimal width-8 re-hosting | no (see PR1250 below) | +658.5 at d = 40 | **d = 40 per call** (39 fails for every hosting) | | (d) Helper deletion, PR1043's measured delta | no | +169.8 (explicit hosting), ≤ +170.4 (concavity bound) | none: the model runs out of rank-7 climbs at d = 19 (d = 10 if the 9 copies are kept) | -| (f) Width-7 helper conversion, #1023's placement, rank-1 child removed per helper | no (bit-width-seven-boundary: needs a changed prefix) | +656.0 at k = 71 | **k = 71 per call** (70 fails at the concavity bound) | -| (f) Width-7 conversion, largest local child trimmed per helper | no | +580.6 at k = 74 | none in this placement: fails at k = 74, when all 666 empty 7-slots per replica are used | +| (f) Width-7 helper conversion, #1023's **window-free** placement, rank-1 child removed per helper | no (#1128: needs a changed prefix) | +656.0 at k = 71 (window-free) | window-free only: k = 71 per call (70 fails at the concavity bound). **Under replica-local windows no k ≤ 74 clears** (PR1736) | +| (f) Width-7 conversion, largest local child trimmed per helper (window-free) | no | +580.6 at k = 74 (explicit hosting), ≤ +581.2 (concavity bound) | none: fails at k = 74, when all 666 empty 7-slots per replica are used | | (e) Ideal in-window local shapes (single rank-7 data climbs, single rank-8 helper climbs) | no (no such word) | +3,647.6 in all 288 calls | **52 of 288 calls** (51 fails) | -(e) uses PR1334's most favorable in-window premise. PR1334's cruder "rank-8 children (window h = 8)" row and its +(e) uses PR1334's ideal in-window shapes (rank-7 data climbs, rank-8 helper climbs). PR1334's cruder "rank-8 children (window h = 8)" row, which ignores the 7-level data climb, and its "rank-16 children (beyond the window)" row are not priced here. A same-loop float estimate, not certified, puts them at about 50 and 34 calls; the rank-16 row needs longer windows, hence a different recipe. **Conclusion.** No admitted bit lever nets anything at c\*. The admitted levers are the halving-depth cap raise, width-8 re-hosting and rank-8 copy carriage. Their nets are 0, 0 and −2,578, so any combination of them also fails. Every lever that clears 649 changes the word, the decoder or the coverage law. The stated sizes are: one fewer -rank-7 copy per call, 40 pure helper deletions per call (9.3% of the 430 helpers), 71 width-7 helpers per call in -the optimistic bracket of #1023's placement, the ideal local shapes in 52 calls, ≥ 649 doubly-unpaid families, or -bit-side two-call sharing within ≈ 29.1 units of overhead per call. +rank-7 copy per call (93 of the 2,592 copies record-wide), 40 pure helper deletions per call (9.3% of the 430 +helpers; a stage-relaxed pass), the ideal local shapes in 52 calls, ≥ 649 doubly-unpaid families, or +bit-side two-call sharing within ≈ 29.1 units of overhead per call. Partial width-7 conversion (f) clears only in +#1023's window-free relaxation (k = 71); our merged PR1736 shows that under replica-local windows on the frozen +recipe no partial conversion k ≤ 74 reaches c\* (certified maximum 0.0018099 at k = 74), so width-7 clears only by +the full all-439 conversion (#1023, window-feasible per PR1736), which needs a changed prefix (#1128). **Consequence for `centre-path-sharing`.** At c\* the route needs a complex saving of ≥ 511 net rank-1 units -(≈ 3.55 per call), not PR1791's 1.33, plus one of the bit-side mechanisms above. Bit-side two-call sharing (row b3) -is the only clearing row that reuses a mechanism already constructed on the complex side (PR1708/PR1748). It has -about 14× the needed saving, with an overhead budget of ≈ 29.1–29.3 paid-mass units per call. Rows b2, c, d, e and -f also clear 649, each with a new decoder, coverage law or word of the stated size. With the complex side at +(≈ 3.55 per call), not PR1791's 1.33, plus one of the bit-side mechanisms above. Rows b3 and f both have +constructed complex-side analogues: the PR1708/PR1748 two-call centre phase (scalar-macro level, not admitted) and +the PR601/PR593/PR569 width-7 helpers (per #1023). Each is blocked on the bit side, by the analogue of PR1748's +ownership/sink blocker and by #1128's changed prefix respectively. Bit-side sharing (b3) has about 14× the needed +saving, with an overhead budget of ≈ 29.1–29.3 paid-mass units per call. Rows b2, c, d and e (and f +only in the window-free relaxation) also clear 649, each with a new decoder, coverage law or word of the stated size. With the complex side at c\* + 10⁻²⁴ and the bit side at c\*, κ is still ≥ 1.1× selected (asserted). The complex overhead figure is an additive rank-1 / rank-8 budget in PR1791's treatment. Mixed ranks allow more added mass: PR1888's mixed-rank maxima reach 30.87 units per call at the selected bit endpoint, with rank-51 children. PR3075 charges the named -k = 2 costs at about 12 units per call, inside this budget, and reports that eligibility and demand coupling, not +k = 2 costs (per call: 4 ADD, 4 scratch CLEAR and 4 precision rank-1 children) inside this budget, and reports that eligibility and demand coupling, not the named costs, are the blocker. Without a bit-side mechanism of one of the stated sizes, the card's stop rule holds for the catalogued lever set. @@ -80,7 +85,9 @@ per replica (439 = 430 helpers + 9 retained totals). **(a) The cap is slack.** HD = 2 caps children at 45, since 2r² < 64² ⇔ r ≤ 45. HD = 3 and 4 raise the cap to 50 and 53. But every idle child is a window remainder, at most the largest window 7(2K − 2) = 42, and every local child has rank ≤ 7. No idle child can span two consecutive windows of the same pair: the windows are delimited by -the recipe's bridges, each of which aligns the levels of two pairs and writes the source pair's coordinates. The +the recipe's bridges, each of which needs both pairs at a common level, reading the source pair's side-0 +coordinates and writing its side-1 coordinates there, so every coordinate of the source pair must be materialized +at that level. The record already keeps pair 1's 14 and 7 windows (21 < 45) and pair 2's 28 and 7 windows (35 < 45) as separate children at HD 2, so the split is structural, not a cap effect; pair 3's 42 + 7 = 49 likewise cannot merge under the HD-3 cap of 50. So the record's max child is 42 < 45, and raising the halving depth admits no histogram the @@ -88,7 +95,7 @@ fixed windows can produce. Its net saving is exactly 0. Longer windows need a di [bit589-recipe-floor](../bit589-recipe-floor/README.md) (PR1487)'s whole class of nine-stage recipes, that package reports the longest advance as 2(K − 1) = 6 levels, i.e. a window of 42, so the cap is slack there too. In particular, PR1334's cap-50/53 columns and its halving-depth-4 escape (145 ≥ 138) cannot be reached by any -nine-stage recipe. +recipe in that class. **(a′) Width-8 re-hosting cannot help.** A rank-r window holds at most ⌊r/8⌋ width-8 helpers. 8 divides no window rank, so every window keeps exactly one nonzero remainder child, and the child count (hence the surcharge) is fixed. @@ -106,12 +113,15 @@ help either. This re-certifies, at c\*, what our merged **(b1) Copy carriage.** cst is the sum of the copy ranks (63), entering the deficit D = T(2Kv − L·cst). With whole copies, rank-8 carriage of the nine copies raises cst to 72 and the paid mass by 2,592. That increases the bill. -PR1334's "rank-8 carriage" row kept cst = 63 with 63/8 fractional copies, which is the fewer-copies lever (b2). +PR1334's receipt instead keeps cst = 63 as 63/8 rank-8 copies per call. That mass-preserving reshaping nets only +about +4.45 rank-1 units here (same-loop review check, not shipped) and fails. **(c) One unit of rank mass is worth at most one rank-1 child.** Trimming a rank-r child to r − 1 saves φ(r) − φ(r − 1) < φ(1), certified for r = 2..42 at c\*. Removing a rank-1 child also removes its surcharge. So F doubly-unpaid families save at most F rank-1 children, and F ≥ 649 is necessary, when each unpaid coordinate is a -pure removal of one unit of mass. Reshaping or merges that accompany the unpaid coordinate are outside this model. +pure removal of one unit of mass. Reshaping or merges that accompany the unpaid coordinate are outside this model. JosieElliston's PR1808 +(`plane-port-copy-budgets`) priced this lever earlier at the +10% target as an all-families ideal-packing +relaxation; (c) instead gives a necessary pure-removal count on the actual histogram, and the two do not conflict. **(d) Deletion bounds.** For d deletions per call, the 45 + 9d unused slots per replica are priced two ways: - from below, by the concavity bound (all at the rank-42 per-slot cost, fractional); @@ -126,13 +136,20 @@ include its 9 rank-7 copies, so with the copies kept that model is exhausted at nets at most +170.4 (concavity bound; +169.8 with the explicit hosting). **(f) Width-7 conversion.** [bit589-width-packing](../bit589-width-packing/README.md) (#1023) prices helpers of -width 7 in a constructive placement: the 9k width-7 residuals per replica fill 9k of the 666 empty 7-slots exactly, +width 7 in a **window-free** placement: the 9k width-7 residuals per replica fill 9k of the 666 empty 7-slots exactly, and the freed width-8 slack goes to emptied rank-42 windows. Its bracket removes one unit per converted helper either as a rank-1 child (optimistic) or by trimming the largest local child (pessimistic). Here the slack is hosted as in (d). In the optimistic bracket k = 71 per call passes with the explicit hosting and k = 70 fails at the concavity bound. The pessimistic bracket fails at k = 74, when every empty 7-slot is used; beyond that, this placement does not -apply (#1023's all-439 slot-exact optimum is a different placement). The lever is not admitted: -[bit-width-seven-boundary](../bit-width-seven-boundary/README.md) (Ali Romman) shows that the selected PR589 word +apply (#1023's all-439 slot-exact optimum is a different placement). Within the slot model, mightyOil's #1281 (step-1 +subadditivity lemma) shows an optimum puts each width-7 role alone in a 7-slot, so the k = 70 fail holds for every +slot-model placement and +656.0 is the slot-model optimum. But the slot model ignores stage windows: our merged +[bit589-width7-windows-seed72](../bit589-width7-windows-seed72/README.md) (PR1736, head `b4fd72163234`) proves +that each capacity-7 idle child admits exactly one stage, so at most 3k of the 9k residuals per replica fit, and its +certified window-respecting optimum stays below c\* for every k ≤ 74 (maximum 0.0018099 at k = 74). So under +replica-local windows on the frozen recipe no partial width-7 conversion clears; cross-replica owner maps and other +recipes are open. The lever is not admitted either: +[bit-width-seven-boundary](../bit-width-seven-boundary/README.md) (#1128, Ali Romman, head `df29b159239b`) shows that the selected PR589 word cannot obtain width-7 helpers by replacing its cleanup alone; a changed prefix is needed. Linearity makes every budget sharp. f(a) = (1/(mW)) Σ n_r r (m/r)^a + c_s m^a with c_s = 32mN/(10¹⁶W) is affine in @@ -160,7 +177,7 @@ python3 -I -B research/bit-endpoint-lever-budgets/verify.py && python3 -I -B res Expected output: ```text -PASS_BIT_ENDPOINT_LEVER_BUDGETS need_rank1=649 admitted_levers_max_net=0 copies_sharp=93 deletions_per_call=RANK1:40/TEMPLATE:None width7_per_call=71 ideal_shape_calls=52 complex_need_rank1=511 no_new_kappa +PASS_BIT_ENDPOINT_LEVER_BUDGETS need_rank1=649 admitted_levers_max_net=0 copies_sharp=93 deletions_per_call=RANK1:40/TEMPLATE:None width7_windowfree_per_call=71 ideal_shape_calls=52 complex_need_rank1=511 no_new_kappa PASS_BIT_ENDPOINT_LEVER_BUDGETS_INDEPENDENT signs=75 at c*-1e-24, c* and c*+1e-24 (levers.py interval arithmetic) ``` @@ -201,11 +218,11 @@ python3 -I -B -m unittest discover -s research/bit-endpoint-lever-budgets -p tes - **Scope of each row:** - (a) and (a′) hold for the PR589 nine-stage windows and width-8 helpers. (a′) also holds with stage windows relaxed. No banks are used. - - (b2), (b3), (c), (d) and (e) are pricing passes for hypothetical words or decoders. + - (b2), (b3), (c), (d), (e) and (f) are pricing passes for hypothetical words or decoders. - (d)'s d = 40 pass is in the stage-relaxed slot model; its d ≤ 39 fail holds for every hosting. - (e) is the in-window ideal relaxation of PR1334, applied call by call. - - (f) is #1023's constructive 7-slot placement; its k = 70 fail is for every width-8 slack hosting in that - placement, not for every width-7 placement. + - (f) is #1023's window-free slot model; with #1281's lemma its k = 70 fail holds for every slot-model + placement, but under replica-local windows no k ≤ 74 clears at all (PR1736). - **Unpaid obligations of every passing row:** the word or decoder itself, then: - the dirty-input endpoint and restoration; - hosting under the real stage windows; @@ -223,7 +240,8 @@ python3 -I -B -m unittest discover -s research/bit-endpoint-lever-budgets -p tes ## Open next questions 1. **Can the bit centre path be shared by two calls within ≈ 29 units of overhead per call?** - - *Why it matters:* it is the only clearing row that reuses a mechanism already constructed on the complex side. + - *Why it matters:* it has the largest margin of the clearing rows (about 14× the need) and a constructed + complex-side analogue (PR1708/PR1748, scalar-macro level, not admitted). The complex half must then deliver ≥ 511 net rank-1 units at c\*, i.e. keep its additive rank-1/rank-8 overhead within ≈ 28.3 units per call. - *First step:* write the bit analogue of PR1748's two-call reverse phase for the nine rank-7 copies of one @@ -237,10 +255,11 @@ python3 -I -B -m unittest discover -s research/bit-endpoint-lever-budgets -p tes copied, and price the extra climbs. - *Blocked by:* a replacement contract for the decoder's copied totals (the `centre-path-sharing` card's scope-change trigger); r439-copy-path-sharing-barrier section T shows the totals' source sets are disjoint. -3. **Which bit word reaches the 52-call reshaping, the 40-deletion size or 71 width-7 helpers per call?** +3. **Which bit word reaches the 52-call reshaping, the 40-deletion size or a window-feasible width-7 conversion?** - *Why it matters:* these are the non-sharing alternatives. - *First step:* measure the best per-call delta of PR1043-style deletions combined with climb merges, or test the - six after-scatter width-7 survivors of bit-width-seven-boundary in a changed prefix. + six width-7 survivors of #1128 with a B/C rewrite (prefix through scatter fixed); the other 433 need a changed + prefix, and partial conversion must also beat PR1736's window bound. - *Blocked by:* PR1250 found no further single deletion beyond PR1043 within arbitrary source XOR masks on the fixed R439 word (sole survivor helper 470); it does not exclude simultaneous deletions. Width-7 helpers need a changed prefix. @@ -253,16 +272,19 @@ python3 -I -B -m unittest discover -s research/bit-endpoint-lever-budgets -p tes - **Bootstrap/outer formulas:** Wronskode, `frontier1042-invoice-audit-seed81` (PR #1112). - **Independent arithmetic:** our merged `bit-revision3-levers-seed03` (PR1334, head `5ad74a4a04d1`). - **Re-hosting optimality at the selected endpoint, the slot model and the width-7 placement/bracket:** our merged - `bit589-width-packing` (#1023, head `babca68167d8`); earlier width-7 pricing by mightyOil (#1281). -- **Width-7 admission boundary:** Ali Romman, `bit-width-seven-boundary`. + `bit589-width-packing` (#1023, head `babca68167d8`); exact partial width-7 slot optima by mightyOil (#1281). Window-respecting width-7 bound: our merged + `bit589-width7-windows-seed72` (PR1736, head `b4fd72163234`). +- **Width-7 admission boundary:** Ali Romman, `bit-width-seven-boundary` (#1128, head `df29b159239b`). +- **Bit second-unpaid-coordinate pricing at +10% (all-families relaxation, predecessor of row c):** JosieElliston, + `plane-port-copy-budgets` (PR1808, head `b3d9b9813e0f`). - **Deletion models:** our merged `bit-deletion-ladder` (PR2465, head `9494fc4e2ecd`), from Ali Romman's PR1043 delta - (head `e309e17f83f5`); single-deletion scope from PR1250 (head `67667b11049e`). + (head `e309e17f83f5`); single-deletion scope from PR1250 (bbMisk, head `67667b11049e`). - **Recipe class:** ianlibanio, `bit589-recipe-floor` (PR1487, head `cfd97ca1e9d3`). - **Halving-depth admission:** the merged r740 elementary-cover row bound, `research/e8-bit-carrier-skeleton/code/hub/r740-hosted-eleven/code/row_bound.py` (as cited by PR1334). - **Complex overhead context:** RossRichardson, `centre-sharing-mixed-overhead` (PR1888, head `9c0fd1d20d33`); navinor / Aaron Wang, `centre-shared-kcall-charged-seed615415` (PR3075, head `378b8e47fc01`); the two-call - mechanism PR1708/PR1748 (PR1748 head `ea14f191752c`); `r439-copy-path-sharing-barrier`. + mechanism PR1708 (1337isnot1337) / PR1748 (ToikY; PR1748 head `ea14f191752c`); `r439-copy-path-sharing-barrier`. - **Bit supplier:** DreamingOfClouds (PR589, head `a5afc8c6169e`) and eumemic (PR555, head `65a6bc19f820`), with the PR510/PR463/PR442 template and hosting lineage. - **Selected construction:** Rohan Arun (#1094). diff --git a/research/bit-endpoint-lever-budgets/RESULT.json b/research/bit-endpoint-lever-budgets/RESULT.json index 8fbe8d07f..178eaf079 100644 --- a/research/bit-endpoint-lever-budgets/RESULT.json +++ b/research/bit-endpoint-lever-budgets/RESULT.json @@ -451,7 +451,7 @@ "lever_c_unpaid": { "families": 28416, "fraction": 0.02284, - "note": "necessary for any u-lever; sufficient only if every saved unit is a rank-1 child", + "note": "necessary when each unpaid coordinate is a pure one-unit removal (no reshaping or merges); sufficient if every removed unit is a rank-1 child", "sharp_families_needed_if_each_removes_a_rank1_child": 649 }, "lever_d_helper_deletion": { @@ -516,7 +516,7 @@ "per_call": null }, "max_per_call_in_this_placement": 74, - "placement": "#1023: width-7 residuals in empty 7-slots, width-8 slack in emptied rank-42 windows", + "placement": "#1023 window-free relaxation: width-7 residuals in empty 7-slots, width-8 slack in emptied rank-42 windows", "rank1_removed": { "net_rank1_units": [ 656.0393819674475, @@ -524,7 +524,8 @@ ], "sharp_per_call": 71, "total": 20448 - } + }, + "window_respecting": "PR1736 (bit589-width7-windows-seed72): under replica-local windows at most 3k of the 9k residuals fit; no partial conversion k <= 74 reaches c* (certified max 0.001809907119 at k = 74); cited, not re-derived here" }, "record": { "T": 32, diff --git a/research/bit-endpoint-lever-budgets/TASK.json b/research/bit-endpoint-lever-budgets/TASK.json index af8307ea7..f10754012 100644 --- a/research/bit-endpoint-lever-budgets/TASK.json +++ b/research/bit-endpoint-lever-budgets/TASK.json @@ -41,19 +41,19 @@ ] }, "scope_status": "changed", - "actual_scope": "Requirement map of the +10% two-call centre-sharing route at c* = 921658892752012102303/5e23 (centre-sharing-overhead-budget, PR1791). Complex side: the complex endpoint must itself reach c* (asserted), a net saving of >= 511 rank-1 children (about 3.55 units per call), correcting PR1791 OQ1's 1.33 units per call; additive rank-1/rank-8 two-call overhead budget at c*. Bit side: sharp integer pricing of each listed revision-3 bit lever, one premise at a time on the actual PR589 histogram (surcharge recomputed): halving-depth cap raise, width-8 re-hosting, copy carriage/count, two-call bit centre sharing with its overhead budget, unpaid coordinates (pure removal), helper deletion (two local models), width-7 helper conversion (#1023's placement and bracket) and ideal local shapes. Second method: levers.py interval arithmetic on independently rebuilt histograms.", + "actual_scope": "Requirement map of the +10% two-call centre-sharing route at c* = 921658892752012102303/5e23 (centre-sharing-overhead-budget, PR1791). Complex side: the complex endpoint must itself reach c* (asserted), a net saving of >= 511 rank-1 children (about 3.55 units per call), correcting PR1791 OQ1's 1.33 units per call; additive rank-1/rank-8 two-call overhead budget at c*. Bit side: sharp integer pricing of each listed revision-3 bit lever, one premise at a time on the actual PR589 histogram (surcharge recomputed): halving-depth cap raise, width-8 re-hosting, copy carriage/count, two-call bit centre sharing with its overhead budget, unpaid coordinates (pure removal), helper deletion (two local models), width-7 helper conversion (#1023's window-free placement and bracket; PR1736's window bound cited) and ideal local shapes. Second method: levers.py interval arithmetic on independently rebuilt histograms.", "scope_change_reason": "The card's H2/K helper-interface question is saturated by other packages; this answers the explicit, unowned open question 1 of centre-sharing-overhead-budget (PR1791), which decides whether the strongest complex lever (two-call centre sharing) can be part of a +10% route. That needs a bit lever netting at least 649 rank-1 units on the actual histogram, which no package had priced.", - "bottleneck_link": "Two-call centre sharing makes the bit side bind; +10% kappa needs both endpoints at 0.0018433. The complex side then needs >= 511 net rank-1 units (about 3.55 per call; overhead <= about 28.3 units per call in the additive rank-1/rank-8 model), not PR1791's 1.33. On the bit side no admitted lever nets anything (halving-depth cap slack at max window 42, record hosting optimal, rank-8 carriage loses 2,578 units); clearing 649 needs a new word, decoder or coverage law: one fewer rank-7 copy per call (threshold 93 record-wide), bit-side two-call centre sharing (overhead <= about 29.1 units per call), >= 40 pure helper deletions per call, 71 width-7 helpers per call (optimistic bracket of #1023's placement), >= 649 doubly-unpaid families, or ideal shapes in >= 52 of 288 calls. No kappa claim.", + "bottleneck_link": "Two-call centre sharing makes the bit side bind; +10% kappa needs both endpoints at least 0.0018433. The complex side then needs >= 511 net rank-1 units (about 3.55 per call; overhead <= about 28.3 units per call in the additive rank-1/rank-8 model), not PR1791's 1.33. On the bit side no admitted lever nets anything (halving-depth cap slack at max window 42, record hosting optimal, rank-8 carriage loses 2,578 units); clearing 649 needs a new word, decoder or coverage law: one fewer rank-7 copy per call (threshold 93 record-wide), bit-side two-call centre sharing (overhead <= about 29.1 units per call), >= 40 pure helper deletions per call (stage-relaxed), a full window-feasible width-7 conversion (partial k <= 74 clears only window-free: k = 71; under replica-local windows none clears, PR1736), >= 649 doubly-unpaid families, or ideal shapes in >= 52 of 288 calls. No kappa claim.", "budget_minutes": 90, "stop_rule": "Stop once the lever table is exact and the primary (D/E-diagnostic engine) and independent (levers.py) methods agree on every pass/fail sign at c* - 1e-24, c* and c* + 1e-24; build no construction and search for no new bit word.", "outcome": "completed", - "evidence": "RESULT.json: requirement 649 rank-1 (648 fails) / 16 rank-42; complex need at c* 511 rank-1 (510 fails), 3.549 per call; (a) caps 45/50/53, max child 42 = max window, net 0; (a') per-slot costs 7.94284 < 7.94625 < 7.95184 rank-1 units, record optimal, net 0; (b1) cst 72: -2577.6; (b2) 93 copies threshold (92 fails), one fewer per call +2008.8; (b3) cst 31.5: +9039.5, overhead budget 8391 rank-1 / 1203 rank-7 / 201 rank-42; (c) F >= 649 families (pure removal); (d) RANK1 40 per call (39 fails for every hosting), TEMPLATE exhausted by d = 19 at +169.8 (explicit hosting), <= +170.4 (concavity bound); (f) width-7 rank-1-removed 71 per call (70 fails), +656.0; largest-trimmed fails at 74 (+580.6); (e) 52 of 288 calls (51 fails), all calls +3647.6; complex k=2 overhead at c*: 4079 rank-1 / 511 rank-8 (28.3-28.4 units per call). 75 signs reproduced by independent.py at c* - 1e-24, c* and c* + 1e-24.", + "evidence": "RESULT.json: requirement 649 rank-1 (648 fails) / 16 rank-42; complex need at c* 511 rank-1 (510 fails), 3.549 per call; (a) caps 45/50/53, max child 42 = max window, net 0; (a') per-slot costs 7.94284 < 7.94625 < 7.95184 rank-1 units, record optimal, net 0; (b1) cst 72: -2577.6; (b2) 93 copies threshold (92 fails), one fewer per call +2008.8; (b3) cst 31.5: +9039.5, overhead budget 8391 rank-1 / 1203 rank-7 / 201 rank-42; (c) F >= 649 families (pure removal); (d) RANK1 40 per call (39 fails for every hosting), TEMPLATE exhausted by d = 19 at +169.8 (explicit hosting), <= +170.4 (concavity bound); (f) window-free only: width-7 rank-1-removed 71 per call (70 fails), +656.0; largest-trimmed fails at 74 (+580.6 explicit, <= +581.2 bound); under replica-local windows no k <= 74 reaches c* (PR1736, cited); (e) 52 of 288 calls (51 fails), all calls +3647.6; complex k=2 overhead at c*: 4079 rank-1 / 511 rank-8 (28.3-28.4 units per call). 75 signs reproduced by independent.py at c* - 1e-24, c* and c* + 1e-24.", "author": "Sagar Thakrar (thakrarsagar)", "ai_assistance": "Claude (Anthropic, Claude Opus 5.5) via Claude Code scoped the question and wrote the code and prose in one session of an automated research loop; checked only by AI review passes in the same loop, no independent human review.", "open_questions": [ { "question": "Can the bit centre path be shared by two calls within about 29 paid-mass units of overhead per call (8,391 rank-1 / 1,203 rank-7 / 201 rank-42 children in total)?", - "why_it_matters": "It is the only clearing row that reuses a mechanism already constructed on the complex side (PR1708/PR1748); the complex half must then deliver >= 511 net rank-1 units at c*, i.e. keep its additive rank-1/rank-8 overhead within about 28.3 units per call.", + "why_it_matters": "It has the largest margin of the clearing rows (about 14x the need) and a constructed complex-side analogue (PR1708/PR1748, scalar-macro level, not admitted; row f also has complex analogues PR601/PR593/PR569 per #1023); the complex half must then deliver >= 511 net rank-1 units at c*, i.e. keep its additive rank-1/rank-8 overhead within about 28.3 units per call.", "first_step": "Write the bit analogue of PR1748's two-call reverse phase for the nine rank-7 copies of one replica and price its restoration and hosting children.", "blocked_by": "No bit sharing word exists, PR1748's ownership/sink blocker has no bit analogue yet, and r439-copy-path-sharing-barrier (section T) shows the nine retained totals read pairwise-disjoint source sets." }, @@ -64,10 +64,10 @@ "blocked_by": "A replacement contract for the decoder's copied totals (the centre-path-sharing card's scope-change trigger); r439-copy-path-sharing-barrier section T shows the totals' source sets are disjoint." }, { - "question": "Which bit word reaches the 52-call reshaping, the 40-deletion size or 71 width-7 helpers per call?", + "question": "Which bit word reaches the 52-call reshaping, the 40-deletion size or a window-feasible width-7 conversion?", "why_it_matters": "These are the non-sharing alternatives for the bit half of a +10% route.", - "first_step": "Measure the best per-call delta of PR1043-style deletions combined with climb merges, or test the six after-scatter width-7 survivors of bit-width-seven-boundary in a changed prefix.", - "blocked_by": "PR1250 found no further single deletion beyond PR1043 within arbitrary source XOR masks on the fixed R439 word (it does not exclude simultaneous deletions); width-7 helpers need a changed prefix (bit-width-seven-boundary)." + "first_step": "Measure the best per-call delta of PR1043-style deletions combined with climb merges, or test the six width-7 survivors of #1128 with a B/C rewrite (prefix through scatter fixed); the other 433 need a changed prefix, and partial conversion must beat PR1736's window bound.", + "blocked_by": "PR1250 found no further single deletion beyond PR1043 within arbitrary source XOR masks on the fixed R439 word (it does not exclude simultaneous deletions); width-7 helpers need a changed prefix (bit-width-seven-boundary, #1128)." } ] } diff --git a/research/bit-endpoint-lever-budgets/verify.py b/research/bit-endpoint-lever-budgets/verify.py index 5c14a0762..3f754e860 100644 --- a/research/bit-endpoint-lever-budgets/verify.py +++ b/research/bit-endpoint-lever-budgets/verify.py @@ -259,7 +259,7 @@ def kappa(b, c): assert a_[1] - b_[0] < unit(1, C_STAR)[0], "trimming one unit saves less than removing a rank-1 child" out["lever_c_unpaid"] = dict(families=W, sharp_families_needed_if_each_removes_a_rank1_child=need1, fraction=round(need1 / W, 5), - note="necessary for any u-lever; sufficient only if every saved unit is a rank-1 child") + note="necessary when each unpaid coordinate is a pure one-unit removal (no reshaping or merges); sufficient if every removed unit is a rank-1 child") # ---- (d) helper deletions with optimal width-8 re-hosting (stage-relaxed slot model) --------------------- def rehosted(h, d, upper): @@ -299,7 +299,7 @@ def deletion(model, d, upper): out["lever_d_helper_deletion"] = dict(models={k: {str(r): n for r, n in v.items()} for k, v in DELETION_MODELS.items()}, sharp=dels, known_removable_helpers_of_the_fixed_word=1) - # ---- (f) width-7 helper conversion (#1023's constructive placement and bracket) -------------------------- + # ---- (f) width-7 helper conversion (#1023's WINDOW-FREE placement and bracket; PR1736: unreachable under windows) -------------------------- def width7(k, upper, pes=False): """k helpers per call converted to width 7: one unit removed from one local child per converted helper (rank-1 child removed, or largest child trimmed: #1023's bracket); the 9k width-7 residuals per replica fill @@ -329,7 +329,8 @@ def width7(k, upper, pes=False): record("width-7: %d helpers per call, rank-1 removed, concavity bound" % (k7 - 1), width7(k7 - 1, False), "fail") record("width-7: %d helpers per call, largest trimmed, concavity bound" % kmax, width7(kmax, False, True), "fail") out["lever_f_width7"] = dict( - placement="#1023: width-7 residuals in empty 7-slots, width-8 slack in emptied rank-42 windows", + placement="#1023 window-free relaxation: width-7 residuals in empty 7-slots, width-8 slack in emptied rank-42 windows", + window_respecting="PR1736 (bit589-width7-windows-seed72): under replica-local windows at most 3k of the 9k residuals fit; no partial conversion k <= 74 reaches c* (certified max 0.001809907119 at k = 74); cited, not re-derived here", max_per_call_in_this_placement=kmax, rank1_removed=dict(sharp_per_call=k7, total=calls * k7, net_rank1_units=units_saved(width7(k7, True))), largest_trimmed=dict(per_call=None, fails_at=kmax, net_rank1_units_at_max=units_saved(width7(kmax, True, True))), @@ -355,6 +356,7 @@ def cverdict(h, a): lo, hi = de.Bill(h, MC, WC).residual(a) return "pass" if hi < 0 else "fail" if lo > 0 else "undecided" assert cverdict(HC, Q(asm["complex_lower"])) == "pass" and cverdict(HC, C_STAR) == "fail" + assert cverdict(HC, Q(asm["complex_lower"]) + GRID) == "fail" # selected complex endpoint is sharp assert cverdict(shared_c, B_CERTIFIED_K2) == "pass" and cverdict(shared_c, C_STAR) == "pass" complex_budget, complex_boundary = {}, [] for r in (1, 8): @@ -402,7 +404,7 @@ def cverdict(h, a): print("WROTE", path.relative_to(ROOT).as_posix()) else: assert path.read_text(encoding="utf-8") == text, "RESULT.json differs from the regenerated result" - print("%s need_rank1=%d admitted_levers_max_net=%d copies_sharp=%d deletions_per_call=%s width7_per_call=%d " + print("%s need_rank1=%d admitted_levers_max_net=%d copies_sharp=%d deletions_per_call=%s width7_windowfree_per_call=%d " "ideal_shape_calls=%d complex_need_rank1=%d no_new_kappa" % (out["status"], need1, admitted_max, x_star, "/".join("%s:%s" % (k, v["per_call"]) for k, v in dels.items()), k7, k_star, cneed))