From cd96cf39d3ebb8f4ff06d13257a2a4c5ff1c7383 Mon Sep 17 00:00:00 2001 From: Sagar Thakrar Date: Wed, 14 Oct 2026 04:26:40 +0530 Subject: [PATCH 1/3] Research: certified bit-side revision-3 lever budgets for the PR589 bit supplier at a = 1/99 (no new kappa) --- .../bit-revision3-levers-seed03/README.md | 231 +++++++ .../bit-revision3-levers-seed03/RESULT.json | 581 ++++++++++++++++++ .../bit-revision3-levers-seed03/SOURCES.json | 48 ++ .../bit-revision3-levers-seed03/TASK.json | 72 +++ .../bit-revision3-levers-seed03/VERIFY.json | 41 ++ .../bit-revision3-levers-seed03/levers.py | 156 +++++ .../test_package.py | 116 ++++ .../bit-revision3-levers-seed03/verify.py | 276 +++++++++ 8 files changed, 1521 insertions(+) create mode 100644 research/bit-revision3-levers-seed03/README.md create mode 100644 research/bit-revision3-levers-seed03/RESULT.json create mode 100644 research/bit-revision3-levers-seed03/SOURCES.json create mode 100644 research/bit-revision3-levers-seed03/TASK.json create mode 100644 research/bit-revision3-levers-seed03/VERIFY.json create mode 100644 research/bit-revision3-levers-seed03/levers.py create mode 100644 research/bit-revision3-levers-seed03/test_package.py create mode 100644 research/bit-revision3-levers-seed03/verify.py diff --git a/research/bit-revision3-levers-seed03/README.md b/research/bit-revision3-levers-seed03/README.md new file mode 100644 index 0000000000..09a05fc85f --- /dev/null +++ b/research/bit-revision3-levers-seed03/README.md @@ -0,0 +1,231 @@ +# Bit-side revision-3 levers: certified budgets for the PR589 bit supplier at a = 1/99 + +**Scoped obstruction plus a screening table. No new κ; the selected record is unchanged.** + +- **Track:** 00–19, bit supplier; assignment seed 3 (OS CSPRNG via Python `secrets`). +- **Card:** `bit-helper-contract`, scope **changed** (see [TASK.json](TASK.json)). +- **Base:** `bce54fb3`. The selected record is frontier1094: κ = 0.001672660197076918, complex side binding. + +## Question + +Priority revision 3 (#1272, built on #1240) aims new effort at the centre path, the rank shape and the +coverage law. It quantifies those levers for the **complex** supplier only. It also says a large +jump needs the bit side to advance, and #1293 leaves the bit word's realizability-aware ceiling +open. + +This package asks three questions about the selected PR589 bit supplier: +- Which revision-3 levers can reach the planning target a = 1/99? +- How many helpers, of what width, does a given per-call copy charge leave room for? + +## The model, and why it is favorable + +Every number is an exact rational interval, computed by [levers.py](levers.py) using only the +standard library, with no repository engine imported: +- ln uses atanh prime chains; +- exp uses a Taylor series with a remainder bound; +- rounding is outward and dyadic. + +For one call, the bill at saving a is B(a) = (1/w) Σ n_r (r/m)^(1−a). This is the bit side of the +coverage-law relaxation of #1240: + +- **Coverage law (checked).** Per call, the paid rank mass is (m − u)·w + cst. + - On the selected record, m = 64, w = 888/9 live families per call, u = 1 unpaid coordinate, and the + copy charge is cst = 63 (nine rank-7 copies). + - Then total mass = 63W + 63N = 1,808,352, and D = W − 63N = 10,272. Both equal the record (R3). + - This is the bit form of the coverage identity of #1012. +- **Children.** + - The local children are either the replayed word itself, or its most favorable in-window + shapes. In those shapes each data register is one rank-7 climb, and each helper is one climb + whose rank equals its width. + - All remaining mass goes to idle children at one rank R, with fractional counts allowed. +- **Idle cap.** R = 45, the largest rank allowed by the halving guard m² > 2·maxchild². The guard + comes from `global_k.py`'s `halving_integer_inequality=[M**HD,2*max(paid)**HD]` with the record's + `halving_depth` = 2. Cap 63 is reported as a robustness bound only, because it violates the guard. +- **Surcharge omitted.** + +Each relaxation step can only **lower** the bill: +- the cost per unit mass r^(−a)·m^(a−1) decreases in r, so idle mass is cheapest at the cap; +- r^(1−a) is subadditive, so merging a register's climbs into one climb is cheaper; +- the bill is linear in the counts, so fractional counts form a superset; +- the surcharge is a positive term. + +`test_package.py` checks each step at a = 1/99. So a certified "fail" in the relaxation rules out +every construction that satisfies the premises, and a "pass" is only an upper target. + +**Relation to the merged `research/format-limits`.** Under its accounting axioms, format-limits +section A already proves bit a ≤ X* = 6.0005·10⁻³ < 1/99. This model keeps the coverage law and the +in-window child shapes. It drops the per-stage window climb (Win), the B_K schedule (Sch), the +stage count s and slot domination. So its ceilings are weaker but cover a broader scope: +- the helper-free ceiling under O1 is 0.006794 rather than 0.0060005; +- unlike format-limits A.7's one-at-a-time multipliers, it prices **joint** budgets on the actual + PR589 word. + +## Results ([RESULT.json](RESULT.json); verdicts certified at a = 1/99, idle cap 45) + +| Lever (bit, PR589 word) | Root a (certified bracket in receipt) | × ceiling | At 1/99 | +|---|---:|---:|---| +| Word as shipped, ideal idle packing (**packing ceiling**) | 0.001955918756 | 1 | fail | +| Centre path free (no rank-7 copies, cst 0) | 0.005419644435 | 2.771 | fail | +| Centre path shared by two calls (cst 31.5) | 0.003686367065 | 1.885 | fail | +| Two unpaid coordinates per family | 0.007312036734 | 3.738 | fail | +| Rank-8 children (window h = 8) | 0.003211353255 | 1.642 | fail | +| Rank-16 children (**beyond the window**) | 0.004730915412 | 2.419 | fail | +| Centre free + rank-8 children | 0.008938289238 | 4.570 | **fail** | +| Centre free + rank-16 children | 0.01316705483 | 6.732 | pass | +| Centre free + two unpaid coordinates | 0.01075873179 | 5.501 | pass | + +**Packing ceiling.** With the local word fixed, no idle repacking lifts the bit supplier above +0.0019559, which is +12.8% over the selected bit endpoint 0.0017334. The cap-42 value is 0.0019475; +the cap-63 robustness value is 0.0019982. Open #1293's certified D/E value, 0.0017386, is the bound +for the **fixed** full histogram. Its screening extremum, 0.0161, ranges over all rank-mass-preserving +repackings, including the local word. The value here sits between the two because only the idle +part moves. + +**O1 (copy charge 63).** +- Configuration: no helpers at all, every data register a single rank-7 climb, idle mass at the + cap. +- The bill exceeds 1 at a = 1/99 at caps 42, 45 and 63. At cap 45 the helper-free ceiling is + 0.006794. +- So **as long as the bit copy charge stays at 63 per call, no helper design, data shape or idle + packing reaches 1/99** under these premises. + +**O2 (centre path shared by two calls, copy charge 31.5, cap 45).** The largest helper counts that +still reach 1/99 are certified as boundaries: k passes, and k + 1 fails. + +| Helper width | 8 | 7 | 6 | 4 | 2 | +|---|---:|---:|---:|---:|---:| +| Max helpers | 104 | 110 | 118 | 148 | 229 | + +The comparison uses the design-free helper floors of format-limits section D: at least 138 (strict) +and at least 212 (sink-only targets) bit helpers. Those floors are cited as argued premises, not +re-proved here. Against them: +- **Sharing the centre path is not enough with width-8 helpers.** It leaves room for at most 104, + fewer than either floor. +- Only helpers of width ≤ 4 can meet the strict floor, and only width 2 can meet the sink-only + floor. +- At the robustness cap 63, the width-8 bound becomes 181 helpers. + +**Joint surface (width-8 helpers, cap 45).** The table gives the maximum number of helpers +(including totals) at a = 1/99 for each copy charge per call. "Ideal data" means every data register +is a single rank-7 climb; "shipped data" keeps the replayed shapes. + +| Copy charge per call | 0 | 7 | 14 | 21 | 28 | 31.5 | 35 | 42 | ≥ 49 | +|---|---:|---:|---:|---:|---:|---:|---:|---:|---:| +| Ideal data | 332 | 281 | 230 | 180 | 129 | 104 | 78 | 28 | none | +| Shipped data | 215 | 164 | 113 | 63 | 12 | none | none | none | none | + +The receipt also gives the cap-63 columns and the width sweep at copy charges 0 and 31.5. + +**The complex side and #1272.** The same code reproduces #1240's complex word ceiling, 0.0016900541090 +(m = 73, w = 896/9, cst 64, cap 51). It then prices #1272's combined lever, "centre free and rank-16": +- The combined lever gives 0.011008 (×6.514, matching #1272's 6.5×). This **requires rank-16 local + children**, larger than the complex stage window h = 9. +- Inside the window, with rank-9 children, the same combination gives **0.008128 < 1/99**. + +The bit side behaves the same way: centre free + rank-8 children gives 0.00894 < 1/99. Read either +way, **a 1/99-scale gain from these levers needs a wider local frame window, or a second unpaid +coordinate, on top of freeing the centre path.** + +## Bindings and replay + +The bindings are checked in this order (B1–B5): +1. A record names the frontier1094 certificate. This is the selected record, or a checkpoint once + the frontier moves. +2. The certificate pins `PR589-EXPECTED.json` (`b9f0e5ca…`). +3. That record pins the bit word `bitE8mut-p111-tuned.json.gz` (`e3e301e6…`), the bit profile, the + endpoint and the halving depth. +4. The halving-guard source line is required verbatim. + +**Positive control (P1).** Using the full selected bit profile with the inherited surcharge, the new +code accepts the endpoint 0.001733427039589844234749 and rejects the next 1e-24 grid point. Without +the surcharge, it would also accept that next point. + +**Replay (R1–R3).** +- Every register's frame itinerary is replayed through D, A, B and C, with frame dimensions computed + as rational ranks of the E8 line sets. Every frame change is a climb. +- The local histogram equals the record: `{1:1323, 2:1342, 3:79, 4:44, 5:102, 6:11, 7:19}`, mass 5,129. +- Class split: + - sources `{1:317, 2:209, 3:10, 4:3}` and targets `{1:10, 2:92, 5:92, 6:10, 7:9}`, mass 777 each; + - 430 helpers `{1:969, 2:1041, 3:69, 4:41, 5:1, 6:1, 7:1}`, mass 3,440; + - 9 retained totals `{1:27, 5:9}`, mass 72; + - 9 rank-7 copies. +- The profile is exactly 288 × the local word plus idle children `{2:13920, 4:14208, 6:14208, + 7:21312, 42:288}`. + +## Controls ([test_package.py](test_package.py), 12 tests, < 2 s) + +- **Interval engine.** It contains the float values. +- **Selected endpoint.** It is accepted, the next grid point is rejected, and omitting the surcharge + would accept the next point. +- **Favorable-relaxation steps.** + - One rank-7 climb is cheaper than a 3 + 4 split. + - Idle mass at rank 45 is cheaper than at rank 42, and rank 63 is cheaper than rank 45. + - The surcharge only raises the bill. +- **Guards.** Excess local mass is rejected by the coverage law. An idle child of rank 64 is + rejected. The cap is 45, since 46 violates the guard. +- **O1 and O2.** O1 fails at caps 42, 45 and 63. The O2 boundary is certified: 104 passes and 105 + fails. +- **Replay.** A gate moved to the empty frame is rejected, and so is a tampered record histogram. +- **Receipt.** The receipt values are reproduced. + +## Reproduce + +```sh +python3 -I -B research/bit-revision3-levers-seed03/verify.py # ~8 s; PASS_BIT_REVISION3_LEVERS (RESULT.json byte-identical) +python3 -I -B -m unittest discover -s research/bit-revision3-levers-seed03 -p test_package.py +python3.12 scripts/research_package.py --package research/bit-revision3-levers-seed03 +``` + +## Scope and what is not claimed + +- **A relaxation, not a construction.** A "pass" row is an upper target that any real mechanism must + meet with its full paid budget. It is not a construction. +- **Premises of the fail rows.** They hold under the coverage law, the in-window child shapes, the + idle cap and the copy charge carried as rank-7 copies. O2 also depends on format-limits section D's + floors, which are argued there and given the crossing lemma. +- **Rank-16 children** are stated as being beyond the current stage windows, h = 8 for bit and + h = 9 for complex, as in format-limits (Win). A changed window is a different architecture. +- **Inherited conditions.** All-size/compiler, hosting, precision/tape, analytic-transfer and + PR589 H1–H5 conditions are inherited and untouched. + +## Overlap and credit + +**Overlap** + +- **#1240** (Douglas Colkitt / Mister-Meeseeks): the complex local-word ceiling and `levers.py`. + This package is the bit-side analogue in independent code and reproduces #1240's complex ceiling. +- **#1272** (Mister-Meeseeks): director revision 3. Its levers are quantified here for the bit side, + and its combined lever is located relative to the stage window. +- **#1293** (navinor): the a < D/E diagnostic and the bit screening extremum, reconciled above. +- **`research/format-limits`**: the format ceiling X* (section A), the scope multipliers (A.7) and + the helper floors (section D, cited as premises). +- **#974** (avirazza): the interface budget and bit headroom, including COPY deletion alone, which is complementary. +- **#1023** (ours) and **#1281** (mightyOil): width-7 hosting relaxations. Both ignore stage windows, + and the widths here are local-shape widths only. +- **#1194, #1311, #1179, #1253 and #1128**: these saturate the card's helper-interface question. +- **Discussion #1317** (bitplane): an active claim on the register-model card. + +**Credit** + +- DreamingOfClouds (PR589) and eumemic (PR555): the bit supplier. +- DaysSky and the PR510/PR442 template and hosting lineage. +- The format-limits authors. +- Douglas Colkitt (#1240, #1272) and navinor (#1293). + +Prepared by Sagar Thakrar (thakrarsagar) with substantial AI assistance from Claude (Anthropic) via +Claude Code. Parallel read-only scout and judge subagents proposed and ranked this question. New +material is Apache-2.0. + +## Open next questions + +1. **Does the idle-rank cap change with halving depth?** Every verdict is reported at the + halving-guard cap 45. + - First step: re-derive the guard for halving depths 2 and 3 from `global_k.py` and re-run the + surface. +2. **Can a bit centre-path-sharing mechanism keep every data register a single rank-7 climb?** The + shipped-shape rows show how much the ideal-data rows assume. + - First step: replay a two-call shared-centre toy on a small E8 sub-word. +3. **What would a rank-16 local window cost?** On both sides, the 1/99 combinations need children + beyond today's windows. + - First step: price a window-16 stage in format-limits' (Win)/(Dfc) accounting, including its + invoice. diff --git a/research/bit-revision3-levers-seed03/RESULT.json b/research/bit-revision3-levers-seed03/RESULT.json new file mode 100644 index 0000000000..e733358b59 --- /dev/null +++ b/research/bit-revision3-levers-seed03/RESULT.json @@ -0,0 +1,581 @@ +{ + "O1": { + "format_limits_bit_X_star": "6.0005e-3 (research/format-limits section A, stronger axioms)", + "helper_free_ceiling_bracket": [ + "74705045347/10995116277760", + "18676261337/2748779069440" + ], + "helper_free_ceiling_cap45": "0.006794384294", + "statement": "copy charge 63 per call, no helpers, every data register one rank-7 climb, idle at cap R", + "verdicts": { + "45": "fail", + "63": "fail" + } + }, + "O2": { + "floors": { + "sink_only": 212, + "strict": 138 + }, + "max_helpers_by_width": { + "2": 229, + "4": 148, + "6": 118, + "7": 110, + "8": 104 + }, + "statement": "copy charge 63/2 per call (centre path shared by two calls), every data register one rank-7 climb, helpers one climb of rank = width, idle at the cap 45; floors from research/format-limits section D (argued premises)", + "widths_meeting_sink_only_floor": [ + 2 + ], + "widths_meeting_strict_floor": [ + 4, + 2 + ] + }, + "binding": { + "assembly": "research/community-frontier1094-audit/ASSEMBLY.json", + "assembly_sha256": "1122cb3a575f8c788345fc1bf4c108ac7c3250fb81a5988671f5eb04b3ab3045", + "expected": "research/e8-bit-p111-tuned/tune/EXPECTED.json", + "expected_sha256": "b9f0e5ca038abe837b0007c8fe006f366a6f02009244ac57705a8a200e2301f4", + "record": "certificates/selected-result.json", + "word": "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz", + "word_sha256": "e3e301e62bc2b41dbf1ceac0acf3d35824ebeab1848c5a2142d4577b109da52f" + }, + "cap_curve": [ + { + "at_1_over_99": "fail", + "idle_cap": 42, + "lever": "PR589 bit word, ideal idle packing", + "root": "0.001947467559", + "root_hi": "334572379/171798691840", + "root_lo": "4282526451/2199023255552" + }, + { + "at_1_over_99": "fail", + "idle_cap": 45, + "lever": "PR589 bit word, ideal idle packing", + "root": "0.001955918756", + "root_hi": "2150555415/1099511627776", + "root_lo": "21505554149/10995116277760" + }, + { + "at_1_over_99": "fail", + "idle_cap": 63, + "lever": "PR589 bit word, ideal idle packing", + "note": "beyond the halving guard; robustness only", + "root": "0.001998187918", + "root_hi": "1098515425/549755813888", + "root_lo": "21970308499/10995116277760" + } + ], + "complex_crosscheck": { + "copy_charge": 64, + "idle_cap": 51, + "m": 73, + "rows": [ + { + "at_1_over_99": "fail", + "lever": "complex word ceiling (#1240)", + "multiplier": "1", + "root": "0.001690054109", + "root_hi": "9291170723/5497558138880", + "root_lo": "3716468289/2199023255552" + }, + { + "at_1_over_99": "fail", + "lever": "centre free", + "multiplier": "2.803", + "root": "0.00473765347", + "root_hi": "52091050787/10995116277760", + "root_lo": "26045525393/5497558138880" + }, + { + "at_1_over_99": "fail", + "lever": "centre free + rank-9 children (window h = 9)", + "multiplier": "4.809", + "root": "0.008127712728", + "root_hi": "89365146513/10995116277760", + "root_lo": "5585321657/687194767360" + }, + { + "at_1_over_99": "pass", + "lever": "centre free + rank-16 children (beyond the window)", + "multiplier": "6.514", + "root": "0.01100842544", + "root_hi": "121038917721/10995116277760", + "root_lo": "3025972943/274877906944" + } + ], + "w": "896/9" + }, + "helper_width": [ + { + "copy_charge": "0", + "helper_width": 8, + "idle_cap": 45, + "max_helpers": 332, + "next": "fail" + }, + { + "copy_charge": "0", + "helper_width": 8, + "idle_cap": 63, + "max_helpers": 372, + "next": "fail" + }, + { + "copy_charge": "0", + "helper_width": 7, + "idle_cap": 45, + "max_helpers": 352, + "next": "fail" + }, + { + "copy_charge": "0", + "helper_width": 7, + "idle_cap": 63, + "max_helpers": 399, + "next": "fail" + }, + { + "copy_charge": "0", + "helper_width": 6, + "idle_cap": 45, + "max_helpers": 379, + "next": "fail" + }, + { + "copy_charge": "0", + "helper_width": 6, + "idle_cap": 63, + "max_helpers": 435, + "next": "fail" + }, + { + "copy_charge": "0", + "helper_width": 4, + "idle_cap": 45, + "max_helpers": 472, + "next": "fail" + }, + { + "copy_charge": "0", + "helper_width": 4, + "idle_cap": 63, + "max_helpers": 555, + "next": "fail" + }, + { + "copy_charge": "0", + "helper_width": 2, + "idle_cap": 45, + "max_helpers": 731, + "next": "fail" + }, + { + "copy_charge": "0", + "helper_width": 2, + "idle_cap": 63, + "max_helpers": 885, + "next": "fail" + }, + { + "copy_charge": "63/2", + "helper_width": 8, + "idle_cap": 45, + "max_helpers": 104, + "next": "fail" + }, + { + "copy_charge": "63/2", + "helper_width": 8, + "idle_cap": 63, + "max_helpers": 181, + "next": "fail" + }, + { + "copy_charge": "63/2", + "helper_width": 7, + "idle_cap": 45, + "max_helpers": 110, + "next": "fail" + }, + { + "copy_charge": "63/2", + "helper_width": 7, + "idle_cap": 63, + "max_helpers": 194, + "next": "fail" + }, + { + "copy_charge": "63/2", + "helper_width": 6, + "idle_cap": 45, + "max_helpers": 118, + "next": "fail" + }, + { + "copy_charge": "63/2", + "helper_width": 6, + "idle_cap": 63, + "max_helpers": 212, + "next": "fail" + }, + { + "copy_charge": "63/2", + "helper_width": 4, + "idle_cap": 45, + "max_helpers": 148, + "next": "fail" + }, + { + "copy_charge": "63/2", + "helper_width": 4, + "idle_cap": 63, + "max_helpers": 270, + "next": "fail" + }, + { + "copy_charge": "63/2", + "helper_width": 2, + "idle_cap": 45, + "max_helpers": 229, + "next": "fail" + }, + { + "copy_charge": "63/2", + "helper_width": 2, + "idle_cap": 63, + "max_helpers": 431, + "next": "fail" + } + ], + "joint_surface": [ + { + "copy_charge": "0", + "ideal_data_width8_cap45": { + "max_helpers": 332, + "next": "fail" + }, + "ideal_data_width8_cap63": { + "max_helpers": 372, + "next": "fail" + }, + "shipped_data_width8_cap45": { + "max_helpers": 215, + "next": "fail" + }, + "shipped_data_width8_cap63": { + "max_helpers": 274, + "next": "fail" + } + }, + { + "copy_charge": "7", + "ideal_data_width8_cap45": { + "max_helpers": 281, + "next": "fail" + }, + "ideal_data_width8_cap63": { + "max_helpers": 330, + "next": "fail" + }, + "shipped_data_width8_cap45": { + "max_helpers": 164, + "next": "fail" + }, + "shipped_data_width8_cap63": { + "max_helpers": 232, + "next": "fail" + } + }, + { + "copy_charge": "14", + "ideal_data_width8_cap45": { + "max_helpers": 230, + "next": "fail" + }, + "ideal_data_width8_cap63": { + "max_helpers": 287, + "next": "fail" + }, + "shipped_data_width8_cap45": { + "max_helpers": 113, + "next": "fail" + }, + "shipped_data_width8_cap63": { + "max_helpers": 189, + "next": "fail" + } + }, + { + "copy_charge": "21", + "ideal_data_width8_cap45": { + "max_helpers": 180, + "next": "fail" + }, + "ideal_data_width8_cap63": { + "max_helpers": 245, + "next": "fail" + }, + "shipped_data_width8_cap45": { + "max_helpers": 63, + "next": "fail" + }, + "shipped_data_width8_cap63": { + "max_helpers": 147, + "next": "fail" + } + }, + { + "copy_charge": "28", + "ideal_data_width8_cap45": { + "max_helpers": 129, + "next": "fail" + }, + "ideal_data_width8_cap63": { + "max_helpers": 202, + "next": "fail" + }, + "shipped_data_width8_cap45": { + "max_helpers": 12, + "next": "fail" + }, + "shipped_data_width8_cap63": { + "max_helpers": 104, + "next": "fail" + } + }, + { + "copy_charge": "63/2", + "ideal_data_width8_cap45": { + "max_helpers": 104, + "next": "fail" + }, + "ideal_data_width8_cap63": { + "max_helpers": 181, + "next": "fail" + }, + "shipped_data_width8_cap45": null, + "shipped_data_width8_cap63": { + "max_helpers": 83, + "next": "fail" + } + }, + { + "copy_charge": "35", + "ideal_data_width8_cap45": { + "max_helpers": 78, + "next": "fail" + }, + "ideal_data_width8_cap63": { + "max_helpers": 160, + "next": "fail" + }, + "shipped_data_width8_cap45": null, + "shipped_data_width8_cap63": { + "max_helpers": 62, + "next": "fail" + } + }, + { + "copy_charge": "42", + "ideal_data_width8_cap45": { + "max_helpers": 28, + "next": "fail" + }, + "ideal_data_width8_cap63": { + "max_helpers": 117, + "next": "fail" + }, + "shipped_data_width8_cap45": null, + "shipped_data_width8_cap63": { + "max_helpers": 19, + "next": "fail" + } + }, + { + "copy_charge": "49", + "ideal_data_width8_cap45": null, + "ideal_data_width8_cap63": { + "max_helpers": 75, + "next": "fail" + }, + "shipped_data_width8_cap45": null, + "shipped_data_width8_cap63": null + }, + { + "copy_charge": "56", + "ideal_data_width8_cap45": null, + "ideal_data_width8_cap63": { + "max_helpers": 32, + "next": "fail" + }, + "shipped_data_width8_cap45": null, + "shipped_data_width8_cap63": null + }, + { + "copy_charge": "63", + "ideal_data_width8_cap45": null, + "ideal_data_width8_cap63": null, + "shipped_data_width8_cap45": null, + "shipped_data_width8_cap63": null + } + ], + "levers": [ + { + "at_1_over_99": "fail", + "idle_cap": 45, + "lever": "PR589 bit word, ideal idle packing (packing ceiling)", + "multiplier": "1", + "root": "0.001955918756", + "root_hi": "2150555415/1099511627776", + "root_lo": "21505554149/10995116277760" + }, + { + "at_1_over_99": "fail", + "idle_cap": 45, + "lever": "centre path free (no rank-7 copies, copy charge 0)", + "multiplier": "2.771", + "root": "0.005419644435", + "root_hi": "59589620749/10995116277760", + "root_lo": "14897405187/2748779069440" + }, + { + "at_1_over_99": "fail", + "idle_cap": 45, + "lever": "centre path shared by two calls (copies and charge halved)", + "multiplier": "1.885", + "root": "0.003686367065", + "root_hi": "20266017259/5497558138880", + "root_lo": "40532034517/10995116277760" + }, + { + "at_1_over_99": "fail", + "idle_cap": 45, + "lever": "two unpaid coordinates per family", + "multiplier": "3.738", + "root": "0.007312036734", + "root_hi": "80396694121/10995116277760", + "root_lo": "2009917353/274877906944" + }, + { + "at_1_over_99": "fail", + "idle_cap": 45, + "lever": "rank-8 children (local mass at rank 8 = window h)", + "multiplier": "1.642", + "root": "0.003211353255", + "root_hi": "8827300613/2748779069440", + "root_lo": "35309202451/10995116277760" + }, + { + "at_1_over_99": "fail", + "idle_cap": 45, + "lever": "rank-16 children (beyond the window h = 8)", + "multiplier": "2.419", + "root": "0.004730915412", + "root_hi": "13004241263/2748779069440", + "root_lo": "52016965051/10995116277760" + }, + { + "at_1_over_99": "fail", + "idle_cap": 45, + "lever": "centre free + rank-8 children", + "multiplier": "4.57", + "root": "0.008938289238", + "root_hi": "49138764749/5497558138880", + "root_lo": "98277529497/10995116277760" + }, + { + "at_1_over_99": "pass", + "idle_cap": 45, + "lever": "centre free + rank-16 children", + "multiplier": "6.732", + "root": "0.01316705483", + "root_hi": "18096662361/1374389534720", + "root_lo": "144773298887/10995116277760" + }, + { + "at_1_over_99": "pass", + "idle_cap": 45, + "lever": "centre free + two unpaid coordinates", + "multiplier": "5.501", + "root": "0.01075873179", + "root_hi": "23658701413/2199023255552", + "root_lo": "14786688383/1374389534720" + } + ], + "replay": { + "calls": 288, + "class_mass": { + "helpers": 3440, + "sources": 777, + "targets": 777, + "totals": 72 + }, + "class_split": { + "helpers": { + "1": "969", + "2": "1041", + "3": "69", + "4": "41", + "5": "1", + "6": "1", + "7": "1" + }, + "sources": { + "1": "317", + "2": "209", + "3": "10", + "4": "3" + }, + "targets": { + "1": "10", + "2": "92", + "5": "92", + "6": "10", + "7": "9" + }, + "totals": { + "1": "27", + "5": "9" + } + }, + "copies": { + "7": "9" + }, + "copy_charge_per_call": 63, + "deficit": 10272, + "deficit_identity": "D = W - 63 N", + "halving_guard_cap": 45, + "idle_children_total": { + "2": "13920", + "4": "14208", + "42": "288", + "6": "14208", + "7": "21312" + }, + "live": 28416, + "local_histogram": { + "1": "1323", + "2": "1342", + "3": "79", + "4": "44", + "5": "102", + "6": "11", + "7": "19" + }, + "local_mass": 5129, + "replicas": 32, + "stages": 9, + "v": 111, + "w": "296/3" + }, + "selected_bit_endpoint": { + "accepted": true, + "endpoint": "1733427039589844234749/1000000000000000000000000", + "next_grid_rejected": true + }, + "status": "PASS_BIT_REVISION3_LEVERS" +} diff --git a/research/bit-revision3-levers-seed03/SOURCES.json b/research/bit-revision3-levers-seed03/SOURCES.json new file mode 100644 index 0000000000..4b09371652 --- /dev/null +++ b/research/bit-revision3-levers-seed03/SOURCES.json @@ -0,0 +1,48 @@ +{ + "schema_version": 1, + "base_commit": "bce54fb3f895cbe5cd4c0eb477c3afeed100190f", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "c05fafaa25ba95b2d5af86b1800427198e3d20eb", + "sha256": "89b5928bc92c81e2647b6d702a7ad85a6795b8f44e2eb267b2ff3145d8f2b2ce" + }, + { + "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/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz", + "usage": "input", + "git_blob": "85a4499bf9e4911a705d50567a2c2ef6cf23739a", + "sha256": "e3e301e62bc2b41dbf1ceac0acf3d35824ebeab1848c5a2142d4577b109da52f" + }, + { + "path": "research/e8-bit-p111-tuned/vendor/pr510/e8-r480-nine-stage/vendor/e8-r715-eleven-stage-whole/code/global_k.py", + "usage": "input", + "git_blob": "3df12bd632f1fdba825ced57110a1fee82eb2857", + "sha256": "6368196a393ac25bb2918880e4c4bd31ed733b762c27b6873ab391cbc0c5c3c8" + }, + { + "path": "research/format-limits/README.md", + "usage": "provenance", + "git_blob": "2f7aaf5b8225717394fe6adda6b313026eaf8090", + "sha256": "0fa0d6b2df96ddc06b876c41c5fa8d2335b97f36bc8f17d1371296d23199c263" + } + ] +} diff --git a/research/bit-revision3-levers-seed03/TASK.json b/research/bit-revision3-levers-seed03/TASK.json new file mode 100644 index 0000000000..701e63682c --- /dev/null +++ b/research/bit-revision3-levers-seed03/TASK.json @@ -0,0 +1,72 @@ +{ + "schema_version": 1, + "task_id": "bit-helper-contract", + "priority_revision": 2, + "base_commit": "bce54fb3f895cbe5cd4c0eb477c3afeed100190f", + "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": [ + "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.", + "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": "Certified bit-side budgets for priority revision 3: in the coverage-law relaxation of the selected PR589 bit word (fixed local word or most favorable in-window shapes, idle mass at the halving-guard cap 45, fractional counts, no surcharge), the packing ceiling, each revision-3 lever and combination at a = 1/99, and the joint copy-charge x helper-count x helper-width surface, with scoped obstructions O1 (copy charge 63) and O2 (centre path shared by two calls against the design-free helper floors).", + "scope_change_reason": "The card's helper-interface question is saturated or claimed (semantic-D contract #1194/#1311, entrances #1179/#1253, after-B frames #1128; register-model card actively claimed in #1317), while revision 3 (#1272) quantifies its levers on the complex side only and #1293 leaves the bit word's realizability-aware ceiling open. The bit-side budget answers what any bit helper or centre-path mechanism must meet to reach the 1/99 planning target.", + "bottleneck_link": "A large kappa jump needs both suppliers to advance (bottleneck brief, priority log). This gives the bit side's quantitative targets: which levers can reach 1/99 under the coverage law, and how many helpers of which width a given copy charge leaves room for. It also shows that the combined lever of #1272 (and its bit analogue) relies on rank-16 children beyond the stage window. No kappa change.", + "budget_minutes": 180, + "stop_rule": "Stop once every lever, surface boundary and obstruction is certified with exact intervals and the positive controls reproduce the selected bit endpoint and #1240's complex ceiling; report any undecided boundary instead of claiming it.", + "outcome": "completed", + "evidence": "RESULT.json: bit word packing ceiling 0.001955918756 (cap 45); centre free x2.771, shared x1.885, two unpaid x3.738, rank-8 x1.642, rank-16 x2.419; centre free + rank-8 0.00894 < 1/99; centre free + rank-16 0.01317 and centre free + two unpaid 0.01076 pass. O1: copy charge 63 fails 1/99 at caps 42/45/63 even helper-free (ceiling 0.00679 at cap 45). O2: with the centre path shared (copy charge 31.5) at cap 45, at most 104 width-8 helpers fit (k=104 passes, 105 fails), below both floors (138 strict, 212 sink-only); only width <= 4 meets the strict floor and width 2 the sink-only floor. Complex cross-check: #1240's ceiling reproduced; #1272's combined lever gives 0.01101 with rank-16 children but 0.00813 < 1/99 inside the window (rank 9). 12 tests pass.", + "author": "Sagar Thakrar (thakrarsagar)", + "ai_assistance": "Substantial: Claude (Anthropic) via Claude Code. Parallel read-only scout and judge subagents proposed and compared four bit-track candidates; this one ranked first on value and overlap.", + "open_questions": [ + { + "question": "Is the halving-guard cap 45 the right idle-rank limit for every bit recursion depth, or can a changed halving depth admit larger idle children?", + "why_it_matters": "All verdicts are reported at cap 45 with cap 63 as a robustness bound; O1 holds at both, but surface boundaries move with the cap.", + "first_step": "Re-derive the guard from global_k.py's halving_integer_inequality for halving depths 2 and 3 and re-run the surface.", + "blocked_by": "None." + }, + { + "question": "Can a bit centre-path mechanism keep data registers as single rank-7 climbs while sharing the copy charge, or does sharing force split climbs?", + "why_it_matters": "The surface's ideal-data rows assume single climbs; the shipped-data rows show the gap is large (e.g. 104 vs none at copy charge 31.5).", + "first_step": "Construct a two-call shared-centre toy on a small E8 sub-word and replay its climbs.", + "blocked_by": "A concrete centre-sharing construction." + }, + { + "question": "Which local frame window (h) would a rank-16-children mechanism need on each side, and what does it cost in the invoice?", + "why_it_matters": "Both the bit and complex combined levers reach 1/99 only with rank-16 children beyond the current windows (h = 8 bit, h = 9 complex).", + "first_step": "Price a window-16 stage in the format-limits (Win)/(Dfc) accounting.", + "blocked_by": "None." + } + ] +} diff --git a/research/bit-revision3-levers-seed03/VERIFY.json b/research/bit-revision3-levers-seed03/VERIFY.json new file mode 100644 index 0000000000..016eb80ada --- /dev/null +++ b/research/bit-revision3-levers-seed03/VERIFY.json @@ -0,0 +1,41 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "certificates/selected-result.json", + "research/community-frontier1094-audit/ASSEMBLY.json", + "research/e8-bit-p111-tuned/tune/EXPECTED.json", + "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz", + "research/e8-bit-p111-tuned/vendor/pr510/e8-r480-nine-stage/vendor/e8-r715-eleven-stage-whole/code/global_k.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Binds selected record -> frontier1094 ASSEMBLY -> PR589 EXPECTED -> bit word and the halving guard; reproduces the selected bit endpoint (accept, next 1e-24 reject, surcharge included) with code-disjoint exact arithmetic; replays the word's local histogram, class split and coverage law; certifies the lever table, cap curve, joint helper/copy-charge surface (k passes, k+1 fails), O1/O2 and the complex cross-check; RESULT.json byte-identical." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "-m", + "unittest", + "discover", + "-s", + "{package}", + "-p", + "test_package.py" + ], + "timeout_seconds": 120, + "checks": "Interval engine sanity, endpoint and neighbour controls, the favorable-relaxation steps (merging climbs, idle at the largest rank, surcharge), coverage-law and rank guards, certified O1/O2 boundaries, replay and record tampering controls, receipt values." + } + ] +} diff --git a/research/bit-revision3-levers-seed03/levers.py b/research/bit-revision3-levers-seed03/levers.py new file mode 100644 index 0000000000..f2c4c00fc8 --- /dev/null +++ b/research/bit-revision3-levers-seed03/levers.py @@ -0,0 +1,156 @@ +# SPDX-License-Identifier: Apache-2.0 +"""Exact, standard-library tools for bit-side lever budgets (and the complex cross-check). + +Model (the coverage-law relaxation of #1240, applied to the PR589 bit supplier): + per call, the paid children are a local histogram L (rank -> count, fractional allowed) plus idle + children carrying the remaining rank mass (m - u) w + cst - mass(L) at one rank R (fractional); + the per-call bill at saving a is B(a) = (1/w) sum_r n_r (r/m)^(1-a), increasing in a. + w = live families per call, u = unpaid coordinates per family (1 today), cst = per-call copy charge. +A configuration reaches saving a iff B(a) < 1. Every number below is an exact rational interval: +ln via atanh prime chains, exp via Taylor series with a remainder bound, outward dyadic rounding. +""" +from fractions import Fraction as Q +from functools import lru_cache + +PREC = 200 + + +class Reject(Exception): + """A check failed; the argument is its label.""" + + +def need(ok, label): + if not ok: + raise Reject(label) + + +def _down(x): + return Q((x.numerator << PREC) // x.denominator, 1 << PREC) + + +def _up(x): + return -_down(-x) + + +@lru_cache(None) +def atanh(t): + s, p, k = Q(0), t, 0 + while True: + s += p / (2 * k + 1) + p *= t * t + k += 1 + tail = p / ((2 * k + 1) * (1 - t * t)) + if tail < Q(1, 1 << (PREC + 8)): + return _down(s), _up(s + tail) + + +@lru_cache(None) +def ln(k): + """Interval for ln k, k a positive integer: ln k = ln(k-1) + 2 atanh(1/(2k-1)).""" + if k == 1: + return Q(0), Q(0) + lo, hi = ln(k - 1) + a, b = atanh(Q(1, 2 * k - 1)) + return _down(lo + 2 * a), _up(hi + 2 * b) + + +def exp_iv(lo, hi): + """Interval for exp on [lo, hi] with 0 <= lo <= hi < 1.""" + def series(y, upper): + s, t, k = Q(1), Q(1), 0 + while True: + k += 1 + t = t * y / k + s += t + if t * y < Q(1, 1 << (PREC + 8)): + return _up(s + 2 * t * y / (k + 1)) if upper else _down(s) + return series(lo, False), series(hi, True) + + +def child(r, m, a): + """Interval for (r/m)^(1-a) = (r/m) exp(a ln(m/r)), integer r <= m, 0 <= a < 1.""" + lm, um = ln(m) + lr, ur = ln(r) + e = exp_iv(max(Q(0), a * (lm - ur)), a * (um - lr)) + return _down(Q(r, m) * e[0]), _up(Q(r, m) * e[1]) + + +def bill(H, m, w, a, surcharge=False): + """Interval for (1/w) sum_r n_r (r/m)^(1-a) [+ the inherited bad-residue surcharge 32 m N m^a / 1e16 / w].""" + lo = hi = Q(0) + for r, n in H.items(): + if n: + c = child(r, m, a) + lo += Q(n) * c[0] + hi += Q(n) * c[1] + if surcharge: + N = sum(Q(n) for n in H.values()) + c = child(1, m, a) # (1/m)^(1-a): 32 m^2 N c / 1e16 = 32 m N m^a / 1e16 + lo += Q(32 * m * m) * N * c[0] / 10 ** 16 + hi += Q(32 * m * m) * N * c[1] / 10 ** 16 + return _down(lo / w), _up(hi / w) + + +def relaxed(local, m, w, cst, R, unpaid=1): + """Per-call histogram: the local children plus all remaining coverage-law mass at rank R.""" + total = (m - unpaid) * Q(w) + Q(cst) + mass = sum(Q(r) * Q(n) for r, n in local.items()) + need(mass <= total, 'local mass exceeds the coverage law') + need(0 < R < m and all(0 < r < m for r in local), 'child ranks must lie in (0, m)') + H = {r: Q(n) for r, n in local.items() if n} + if total > mass: + H[R] = H.get(R, Q(0)) + (total - mass) / R + return H + + +def verdict(H, m, w, a, surcharge=False): + """'pass' (certified B(a) < 1), 'fail' (certified B(a) > 1) or 'undecided'.""" + lo, hi = bill(H, m, w, a, surcharge) + return 'pass' if hi < 1 else 'fail' if lo > 1 else 'undecided' + + +def root(H, m, w, surcharge=False, tol=Q(1, 10 ** 13), top=Q(1, 20)): + """Certified bracket [lo, hi] of the saving where B = 1: B(lo) < 1 < B(hi) certified, hi - lo <= tol.""" + lo, hi = Q(0), top + need(verdict(H, m, w, lo, surcharge) == 'pass' and verdict(H, m, w, hi, surcharge) == 'fail', 'root not bracketed') + while hi - lo > tol: + mid = (lo + hi) / 2 + v = verdict(H, m, w, mid, surcharge) + if v == 'pass': + lo = mid + elif v == 'fail': + hi = mid + else: + raise Reject('interval too wide to bisect') + return lo, hi + + +def dec(x, digits=10): + return format(float(x), '.%dg' % digits) + + +def max_count(base, extra_rank, m, w, cst, R, a, limit): + """Largest k (0..limit) such that base + k children of rank extra_rank passes at a; None if k=0 fails. + + Returns (k, verdict_k, verdict_k_plus_1) with both verdicts certified (k+1 must fail or exceed limit). + """ + def ok(k): + local = dict(base) + local[extra_rank] = local.get(extra_rank, 0) + k + try: + return verdict(relaxed(local, m, w, cst, R), m, w, a) + except Reject: + return 'fail' # exceeds the coverage law: no idle room left + if ok(0) != 'pass': + return None + lo, hi = 0, limit + while lo < hi: + mid = (lo + hi + 1) // 2 + v = ok(mid) + need(v != 'undecided', 'undecided boundary') + if v == 'pass': + lo = mid + else: + hi = mid - 1 + nxt = ok(lo + 1) if lo < limit else 'limit' + return lo, 'pass', nxt diff --git a/research/bit-revision3-levers-seed03/test_package.py b/research/bit-revision3-levers-seed03/test_package.py new file mode 100644 index 0000000000..a66bb511d6 --- /dev/null +++ b/research/bit-revision3-levers-seed03/test_package.py @@ -0,0 +1,116 @@ +# SPDX-License-Identifier: Apache-2.0 +"""Controls for the bit-side lever budgets (about 20 s). + +Run: python3 -I -B -m unittest discover -s research/bit-revision3-levers-seed03 -p test_package.py -v +""" +import copy +import json +import math +import sys +import unittest +from fractions import Fraction as Q +from pathlib import Path + +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE)) +import levers as L # noqa: E402 +import verify as V # noqa: E402 + +BINDING, ASM, EXP, WORD = V.bind() +PROFILE = {int(r): n for r, n in EXP['nine']['profile'].items()} +W = EXP['nine']['bit']['live'] +C0 = V.frac(EXP['nine']['bit_lower']) +M, w = 64, Q(296, 3) + + +class Engine(unittest.TestCase): + def test_intervals_contain_floats(self): + for k in (2, 7, 45, 64, 73): + lo, hi = L.ln(k) + self.assertTrue(lo <= Q(math.log(k)) + Q(1, 10 ** 12) and Q(math.log(k)) - Q(1, 10 ** 12) <= hi and hi - lo < Q(1, 10 ** 50)) + lo, hi = L.child(7, 64, Q(1, 99)) + self.assertTrue(lo < hi and abs(float(lo) - (7 / 64) ** (1 - 1 / 99)) < 1e-12) + + def test_selected_endpoint_and_its_neighbours(self): + self.assertEqual(L.verdict(PROFILE, M, W, C0, surcharge=True), 'pass') + self.assertEqual(L.verdict(PROFILE, M, W, C0 + Q(1, 10 ** 24), surcharge=True), 'fail') + # omitting the inherited surcharge would also accept the next grid point + self.assertEqual(L.verdict(PROFILE, M, W, C0 + Q(1, 10 ** 24), surcharge=False), 'pass') + + +class Relaxation(unittest.TestCase): + """The relaxation is favorable: each step it takes can only lower the bill.""" + + def bill_hi(self, H): + return L.bill(H, M, w, Q(1, 99))[1] + + def bill_lo(self, H): + return L.bill(H, M, w, Q(1, 99))[0] + + def test_merging_climbs_lowers_the_bill(self): + # one rank-7 climb is cheaper than a 3 + 4 split of the same register (concavity of r^(1-a)) + self.assertLess(self.bill_hi({7: 1}), self.bill_lo({3: 1, 4: 1})) + + def test_idle_mass_at_the_largest_rank_is_cheapest(self): + self.assertLess(self.bill_hi({45: 1}), self.bill_lo({42: Q(45, 42)})) + self.assertLess(self.bill_hi({63: 1}), self.bill_lo({45: Q(63, 45)})) + + def test_surcharge_only_raises_the_bill(self): + H = L.relaxed(dict(EXPECTED_LOCAL), M, w, 63, 45) + self.assertLess(L.bill(H, M, w, Q(1, 99))[1], L.bill(H, M, w, Q(1, 99), surcharge=True)[0]) + + def test_coverage_law_and_rank_guards(self): + with self.assertRaises(L.Reject): + L.relaxed({7: 10 ** 6}, M, w, 63, 45) # more local mass than the coverage law allows + with self.assertRaises(L.Reject): + L.relaxed(dict(EXPECTED_LOCAL), M, w, 63, 64) # an idle child of rank m makes the bill vacuous + self.assertEqual(max(r for r in range(1, M) if M * M > 2 * r * r), 45) + self.assertFalse(M * M > 2 * 46 * 46) + + def test_o2_boundary_is_certified(self): + base = {7: Q(222) + Q(63, 14)} + k, _, nxt = L.max_count(base, 8, M, w, Q(63, 2), 45, Q(1, 99), 600) + self.assertEqual((k, nxt), (104, 'fail')) + loc = dict(base) + loc[8] = 104 + self.assertEqual(L.verdict(L.relaxed(loc, M, w, Q(63, 2), 45), M, w, Q(1, 99)), 'pass') + loc[8] = 105 + self.assertEqual(L.verdict(L.relaxed(loc, M, w, Q(63, 2), 45), M, w, Q(1, 99)), 'fail') + + def test_o1_has_no_room_at_any_admissible_cap(self): + base = {7: Q(222) + 9} + for R in (42, 45, 63): + self.assertEqual(L.verdict(L.relaxed(base, M, w, 63, R), M, w, Q(1, 99)), 'fail') + + +class Replay(unittest.TestCase): + def test_replay_matches_the_record(self): + local, split, copies = V.replay(WORD, EXP) + self.assertEqual(sum(r * c for r, c in local.items()), 5129) + self.assertEqual(sum(r * c for r, c in (split['sources']).items()), 777) + self.assertEqual(dict(copies), {7: 9}) + + def test_tampered_gate_is_rejected(self): + word = copy.deepcopy(WORD) + gate = next(g for g in word['A'] if g[0] != word['start'][g[1]]) + gate[0] = 0 # a gate moved to the empty frame + with self.assertRaises(L.Reject): + V.replay(word, EXP) + + def test_tampered_record_histogram_is_rejected(self): + exp = copy.deepcopy(EXP) + exp['word']['local_histogram']['2'] += 1 + with self.assertRaises(L.Reject): + V.replay(WORD, exp) + + def test_receipt_is_reproduced(self): + result = json.loads((HERE / 'RESULT.json').read_text()) + self.assertEqual(result['status'], 'PASS_BIT_REVISION3_LEVERS') + self.assertEqual(result['levers'][0]['root'], '0.001955918756') + self.assertEqual(result['O2']['max_helpers_by_width']['8'], 104) + + +EXPECTED_LOCAL = {int(r): n for r, n in EXP['word']['local_histogram'].items()} + +if __name__ == '__main__': + unittest.main() diff --git a/research/bit-revision3-levers-seed03/verify.py b/research/bit-revision3-levers-seed03/verify.py new file mode 100644 index 0000000000..361a56dc43 --- /dev/null +++ b/research/bit-revision3-levers-seed03/verify.py @@ -0,0 +1,276 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Bit-side revision-3 levers: certified budgets for the selected PR589 bit supplier at a = 1/99. + +Usage: python3 -I -B research/bit-revision3-levers-seed03/verify.py [--write] + +1. Binds the selected record -> frontier1094 ASSEMBLY -> PR589 EXPECTED.json -> the bit word, and + reproduces the selected bit endpoint (accepted, next 1e-24 grid point rejected, surcharge included) + with code-disjoint exact arithmetic (levers.py). +2. Replays the bit word's frame itineraries: the local histogram, its class split (sources, targets, + helpers, retained totals, rank-7 copies) and the coverage law mass = (m-1)W + cst N, D = W - 63N. +3. Prices the revision-3 levers on the bit side in the coverage-law relaxation (fixed local word, all + idle mass at the halving-guard cap R = 45, fractional counts, no surcharge: all favorable), with + certified root brackets, multipliers and certified verdicts at a = 1/99. +4. Certifies the joint budget surface: the largest number of helpers (each one climb of rank equal to + its width) that a per-call copy charge leaves room for at a = 1/99, as k passes / k+1 fails. +5. Complex cross-check: reproduces #1240's complex word ceiling and prices #1272's combined lever + inside and beyond the complex stage window. +Expected last line: PASS_BIT_REVISION3_LEVERS +""" +import argparse +import gzip +import hashlib +import json +import sys +from collections import Counter +from fractions import Fraction as Q +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +sys.path.insert(0, str(HERE)) +from levers import Reject, dec, max_count, need, relaxed, root, verdict, bill # noqa: E402 + +RECORDS = ('certificates/selected-result.json', 'certificates/checkpoints/frontier1094.json') +ASSEMBLY = 'research/community-frontier1094-audit/ASSEMBLY.json' +EXPECTED = 'research/e8-bit-p111-tuned/tune/EXPECTED.json' +GUARD = ('research/e8-bit-p111-tuned/vendor/pr510/e8-r480-nine-stage/vendor/e8-r715-eleven-stage-whole/code/global_k.py', + 'halving_integer_inequality=[M**HD,2*max(paid)**HD]') +TARGET = Q(1, 99) +M = 64 + + +def sha(data): + return hashlib.sha256(data).hexdigest() + + +def frac(s): + return Q(s) if '/' in str(s) else Q(str(s)) + + +def bind(): + asm_raw = (ROOT / ASSEMBLY).read_bytes() + bound = None + for record in RECORDS: + p = ROOT / record + rec = json.loads(p.read_text()) if p.is_file() else {} + if rec.get('certificate') == ASSEMBLY and rec.get('certificate_sha256') == sha(asm_raw): + bound = record + break + need(bound is not None, 'B1 a record binds the frontier1094 certificate') + asm = json.loads(asm_raw) + exp_raw = (ROOT / EXPECTED).read_bytes() + need(asm['input_sha256']['package:inputs/PR589-EXPECTED.json'] == sha(exp_raw), 'B2 certificate pins the PR589 record') + exp = json.loads(exp_raw) + word_path = ROOT / 'research/e8-bit-p111-tuned' / exp['word']['file'] + word_raw = word_path.read_bytes() + need(sha(word_raw) == exp['word']['file_sha256'] and sha(gzip.decompress(word_raw)) == exp['word']['content_sha256'], + 'B3 record pins the bit word') + need(frac(asm['bit_lower']) == frac(exp['nine']['bit_lower']), 'B4 certificate bit endpoint equals the PR589 record') + guard_text = (ROOT / GUARD[0]).read_text() + need(GUARD[1] in guard_text and exp['nine']['bit']['halving_depth'] == 2, 'B5 halving guard M^2 > 2 maxchild^2') + return dict(record=bound, assembly=ASSEMBLY, assembly_sha256=sha(asm_raw), expected=EXPECTED, expected_sha256=sha(exp_raw), + word=str(word_path.relative_to(ROOT)), word_sha256=sha(word_raw)), asm, exp, json.loads(gzip.decompress(word_raw)) + + +def line_rank(vectors): + rows = [[Q(x) for x in v] for v in vectors] + rank = 0 + for c in range(len(rows[0]) if rows else 0): + piv = next((i for i in range(rank, len(rows)) if rows[i][c] != 0), None) + if piv is None: + continue + rows[rank], rows[piv] = rows[piv], rows[rank] + for i in range(len(rows)): + if i != rank and rows[i][c] != 0: + f = rows[i][c] / rows[rank][c] + rows[i] = [a - f * b for a, b in zip(rows[i], rows[rank])] + rank += 1 + return rank + + +def replay(word, exp): + """Frame itinerary of every register through D, A, B, C (start and final frames included).""" + lines = word['lines'] + dims = [line_rank([lines[i] for i in f]) if f else 0 for f in word['frames']] + v, R = word['v'], word['R'] + n = 2 * v + R + path = {r: [word['start'][r]] for r in range(n)} + for phase in ('D', 'A', 'B', 'C'): + for gate in word[phase]: + f, dst, srcs = gate[0], gate[1], gate[2] + for r in [dst] + list(srcs): + if path[r][-1] != f: + path[r].append(f) + for r in range(n): + if path[r][-1] != word['final'][r]: + path[r].append(word['final'][r]) + retained = set(word['ret']) + + def cls(r): + return 'sources' if r < v else 'targets' if r < 2 * v else 'totals' if r in retained else 'helpers' + split = {k: Counter() for k in ('sources', 'targets', 'helpers', 'totals')} + descents = 0 + for r in range(n): + for a, b in zip(path[r], path[r][1:]): + if dims[b] > dims[a]: + split[cls(r)][dims[b] - dims[a]] += 1 + elif dims[b] < dims[a]: + descents += 1 + copies = Counter(exp['word']['copy_ranks']) + local = sum(split.values(), Counter()) + copies + need(descents == 0, 'R1 every frame change is a climb') + need({str(k): c for k, c in sorted(local.items())} == exp['word']['local_histogram'], 'R2 replay equals the recorded local histogram') + need(sum(r * c for r, c in local.items()) == exp['word']['legality']['rank_mass'], 'R2 local rank mass') + return local, split, copies + + +def show(H): + return {str(r): str(n) for r, n in sorted(H.items())} + + +def main(): + ap = argparse.ArgumentParser(description=__doc__.split('\n\n')[0]) + ap.add_argument('--write', action='store_true') + a = ap.parse_args() + out = {} + binding, asm, exp, word = bind() + out['binding'] = binding + + # --- positive control: the selected bit endpoint, full profile, surcharge included + profile = {int(r): n for r, n in exp['nine']['profile'].items()} + W = exp['nine']['bit']['live'] + c0 = frac(exp['nine']['bit_lower']) + need(verdict(profile, M, W, c0, surcharge=True) == 'pass' + and verdict(profile, M, W, c0 + Q(1, 10 ** 24), surcharge=True) == 'fail', 'P1 selected bit endpoint reproduced') + out['selected_bit_endpoint'] = dict(endpoint=str(c0), accepted=True, next_grid_rejected=True) + + # --- replay and coverage law + local, split, copies = replay(word, exp) + v = word['v'] + T = W // (8 * v) + stages = 9 + N = stages * T + cst = sum(r * c for r, c in copies.items()) + w = Q(W, N) + need(W == 8 * v * T and exp['nine']['bit']['rank_mass'] == (M - 1) * W + cst * N, 'R3 coverage law mass = (m-1)W + cst N') + idle_total = Counter(profile) + idle_total.subtract({r: c * N for r, c in local.items()}) + need(all(c >= 0 for c in idle_total.values()) and max(r for r, c in idle_total.items() if c) <= exp['nine']['bit']['maxchild'], + 'R3 the profile is N local words plus idle children') + cap = max(r for r in range(1, M) if M * M > 2 * r * r) + need(cap == 45, 'B5 halving-guard cap') + out['replay'] = dict( + v=v, replicas=T, stages=stages, calls=N, live=W, w=str(w), copy_charge_per_call=cst, + local_histogram=show(local), local_mass=sum(r * c for r, c in local.items()), + class_split={k: show(c) for k, c in split.items()}, copies=show(copies), + class_mass={k: sum(r * c for r, c in s.items()) for k, s in split.items()}, + deficit=M * W - exp['nine']['bit']['rank_mass'], deficit_identity='D = W - %d N' % cst, + idle_children_total=show(+idle_total), halving_guard_cap=cap) + + # --- revision-3 levers on the bit side (fixed local word unless stated; idle at the cap) + mass = sum(r * c for r, c in local.items()) + no_copies = Counter(local) + no_copies.subtract(copies) + half_copies = {r: Q(c) - (Q(copies.get(r, 0), 2)) for r, c in local.items()} + + def lever(name, H_local, c, u=1, R=cap): + lo, hi = root(relaxed(H_local, M, w, c, R, u), M, w) + return dict(lever=name, root_lo=str(lo), root_hi=str(hi), root=dec(lo), idle_cap=R, + at_1_over_99=verdict(relaxed(H_local, M, w, c, R, u), M, w, TARGET)) + levers = [ + lever('PR589 bit word, ideal idle packing (packing ceiling)', local, cst), + lever('centre path free (no rank-7 copies, copy charge 0)', +no_copies, 0), + lever('centre path shared by two calls (copies and charge halved)', half_copies, Q(cst, 2)), + lever('two unpaid coordinates per family', local, cst, u=2), + lever('rank-8 children (local mass at rank 8 = window h)', {8: Q(mass, 8)}, cst), + lever('rank-16 children (beyond the window h = 8)', {16: Q(mass, 16)}, cst), + lever('centre free + rank-8 children', {8: Q(mass - cst, 8)}, 0), + lever('centre free + rank-16 children', {16: Q(mass - cst, 16)}, 0), + lever('centre free + two unpaid coordinates', +no_copies, 0, u=2), + ] + base = Q(levers[0]['root_lo']) + for row in levers: + row['multiplier'] = dec(Q(row['root_lo']) / base, 4) + out['levers'] = levers + out['cap_curve'] = [lever('PR589 bit word, ideal idle packing', local, cst, R=R) for R in (42, 45)] + \ + [dict(lever('PR589 bit word, ideal idle packing', local, cst, R=63), note='beyond the halving guard; robustness only')] + + # --- joint budget surface at a = 1/99: helpers (one climb of rank = width) per copy charge + data_ideal = {7: Q(2 * v)} # each data register a single rank-7 climb + data_shipped = split['sources'] + split['targets'] + surface = [] + for c in (0, 7, 14, 21, 28, Q(63, 2), 35, 42, 49, 56, 63): + base_ideal = dict(data_ideal) + base_ideal[7] = base_ideal.get(7, 0) + Q(c, 7) # the copy charge carried as rank-7 copies + base_ship = {r: Q(n) for r, n in data_shipped.items()} + base_ship[7] = base_ship.get(7, 0) + Q(c, 7) + row = dict(copy_charge=str(c)) + for label, b in (('ideal_data', base_ideal), ('shipped_data', base_ship)): + for R in (cap, 63): + res = max_count(b, 8, M, w, c, R, TARGET, 600) + row['%s_width8_cap%d' % (label, R)] = None if res is None else dict(max_helpers=res[0], next=res[2]) + surface.append(row) + widths = [] + for c in (0, Q(63, 2)): + b = dict(data_ideal) + b[7] = b.get(7, 0) + Q(c, 7) + for width in (8, 7, 6, 4, 2): + for R in (cap, 63): + res = max_count(b, width, M, w, c, R, TARGET, 2000) + widths.append(dict(copy_charge=str(c), helper_width=width, idle_cap=R, + max_helpers=None if res is None else res[0], next=None if res is None else res[2])) + out['joint_surface'] = surface + out['helper_width'] = widths + # obstruction rows, restated as certified verdicts + o1 = {R: verdict(relaxed({7: Q(2 * v) + Q(cst, 7)}, M, w, cst, R), M, w, TARGET) for R in (cap, 63)} + need(o1 == {cap: 'fail', 63: 'fail'}, 'O1 copy charge 63 cannot reach 1/99 in the relaxation') + o1_lo, o1_hi = root(relaxed({7: Q(2 * v) + Q(cst, 7)}, M, w, cst, cap), M, w) + out['O1'] = dict(statement='copy charge 63 per call, no helpers, every data register one rank-7 climb, idle at cap R', + verdicts={str(R): v_ for R, v_ in o1.items()}, helper_free_ceiling_cap45=dec(o1_lo), + helper_free_ceiling_bracket=[str(o1_lo), str(o1_hi)], + format_limits_bit_X_star='6.0005e-3 (research/format-limits section A, stronger axioms)') + # O2: centre path shared by two calls against the design-free helper floors of research/format-limits section D + floors = dict(strict=138, sink_only=212) + shared = [r for r in widths if r['copy_charge'] == str(Q(63, 2)) and r['idle_cap'] == cap] + need(next(r for r in shared if r['helper_width'] == 8)['max_helpers'] < floors['strict'], 'O2 shared centre leaves too few width-8 helpers') + out['O2'] = dict(statement='copy charge 63/2 per call (centre path shared by two calls), every data register one rank-7 climb, ' + 'helpers one climb of rank = width, idle at the cap 45; floors from research/format-limits section D (argued premises)', + floors=floors, + max_helpers_by_width={str(r['helper_width']): r['max_helpers'] for r in shared}, + widths_meeting_strict_floor=[r['helper_width'] for r in shared if r['max_helpers'] is not None and r['max_helpers'] >= floors['strict']], + widths_meeting_sink_only_floor=[r['helper_width'] for r in shared if r['max_helpers'] is not None and r['max_helpers'] >= floors['sink_only']]) + + # --- complex cross-check (#1240) and #1272's combined lever inside / beyond the window + cw = {1: 2412, 2: 418, 3: 432, 4: 142, 5: 82, 8: 8} + cmass = sum(r * n for r, n in cw.items()) + cxw, ccst, ccap = Q(896, 9), 64, max(r for r in range(1, 73) if 73 * 73 > 2 * r * r) + clo, chi = root(relaxed(cw, 73, cxw, ccst, ccap), 73, cxw) + need(Q('0.0016900541090') < chi and clo < Q('0.0016900541091'), 'X1 #1240 complex word ceiling reproduced') + rows = [] + for name, H, c in (('complex word ceiling (#1240)', cw, ccst), + ('centre free', {r: n for r, n in cw.items() if r != 8}, 0), + ('centre free + rank-9 children (window h = 9)', {9: Q(cmass - ccst, 9)}, 0), + ('centre free + rank-16 children (beyond the window)', {16: Q(cmass - ccst, 16)}, 0)): + lo, hi = root(relaxed(H, 73, cxw, c, ccap), 73, cxw) + rows.append(dict(lever=name, root_lo=str(lo), root_hi=str(hi), root=dec(lo), multiplier=dec(lo / clo, 4), + at_1_over_99=verdict(relaxed(H, 73, cxw, c, ccap), 73, cxw, TARGET))) + out['complex_crosscheck'] = dict(m=73, w=str(cxw), copy_charge=ccst, idle_cap=ccap, rows=rows) + + text = json.dumps(dict(status='PASS_BIT_REVISION3_LEVERS', **out), indent=1, sort_keys=True) + '\n' + target = HERE / 'RESULT.json' + if a.write: + target.write_text(text) + elif text != target.read_text(): + raise SystemExit('FAIL RESULT.json differs from this run') + for row in levers: + print('%-62s a = %s x%s at 1/99: %s' % (row['lever'], row['root'], row['multiplier'], row['at_1_over_99'])) + print('PASS_BIT_REVISION3_LEVERS') + + +if __name__ == '__main__': + try: + main() + except Reject as e: + raise SystemExit('FAIL ' + str(e)) From 168466b9bef73e58c68123be5c7b03b0d8352431 Mon Sep 17 00:00:00 2001 From: Sagar Thakrar Date: Wed, 14 Oct 2026 04:47:04 +0530 Subject: [PATCH 2/3] Address review: idle cap is a halving-depth premise (caps 45/50/53 under the row bounds), O2 holds at depth <= 3, correct the window overclaim and floor comparisons --- .../bit-revision3-levers-seed03/README.md | 425 ++++++++------ .../bit-revision3-levers-seed03/RESULT.json | 544 ++++++++++++++++-- .../bit-revision3-levers-seed03/TASK.json | 26 +- .../bit-revision3-levers-seed03/VERIFY.json | 4 +- .../test_package.py | 28 +- .../bit-revision3-levers-seed03/verify.py | 103 ++-- 6 files changed, 845 insertions(+), 285 deletions(-) diff --git a/research/bit-revision3-levers-seed03/README.md b/research/bit-revision3-levers-seed03/README.md index 09a05fc85f..ac65c531ff 100644 --- a/research/bit-revision3-levers-seed03/README.md +++ b/research/bit-revision3-levers-seed03/README.md @@ -1,231 +1,276 @@ # Bit-side revision-3 levers: certified budgets for the PR589 bit supplier at a = 1/99 -**Scoped obstruction plus a screening table. No new κ; the selected record is unchanged.** - -- **Track:** 00–19, bit supplier; assignment seed 3 (OS CSPRNG via Python `secrets`). +**Scoped obstructions plus a screening table. No new κ; the selected record is unchanged.** +- **Track:** 00–19 (bit supplier); assignment seed 3 (OS CSPRNG via Python `secrets`). - **Card:** `bit-helper-contract`, scope **changed** (see [TASK.json](TASK.json)). -- **Base:** `bce54fb3`. The selected record is frontier1094: κ = 0.001672660197076918, complex side binding. +- **Base:** `bce54fb3`, where the selected record is frontier1094: κ = 0.001672660197076918, with the complex side binding. ## Question -Priority revision 3 (#1272, built on #1240) aims new effort at the centre path, the rank shape and the -coverage law. It quantifies those levers for the **complex** supplier only. It also says a large -jump needs the bit side to advance, and #1293 leaves the bit word's realizability-aware ceiling -open. - -This package asks three questions about the selected PR589 bit supplier: -- Which revision-3 levers can reach the planning target a = 1/99? -- How many helpers, of what width, does a given per-call copy charge leave room for? - -## The model, and why it is favorable - -Every number is an exact rational interval, computed by [levers.py](levers.py) using only the -standard library, with no repository engine imported: -- ln uses atanh prime chains; -- exp uses a Taylor series with a remainder bound; -- rounding is outward and dyadic. - -For one call, the bill at saving a is B(a) = (1/w) Σ n_r (r/m)^(1−a). This is the bit side of the -coverage-law relaxation of #1240: - -- **Coverage law (checked).** Per call, the paid rank mass is (m − u)·w + cst. - - On the selected record, m = 64, w = 888/9 live families per call, u = 1 unpaid coordinate, and the - copy charge is cst = 63 (nine rank-7 copies). - - Then total mass = 63W + 63N = 1,808,352, and D = W − 63N = 10,272. Both equal the record (R3). - - This is the bit form of the coverage identity of #1012. -- **Children.** - - The local children are either the replayed word itself, or its most favorable in-window - shapes. In those shapes each data register is one rank-7 climb, and each helper is one climb - whose rank equals its width. - - All remaining mass goes to idle children at one rank R, with fractional counts allowed. -- **Idle cap.** R = 45, the largest rank allowed by the halving guard m² > 2·maxchild². The guard - comes from `global_k.py`'s `halving_integer_inequality=[M**HD,2*max(paid)**HD]` with the record's - `halving_depth` = 2. Cap 63 is reported as a robustness bound only, because it violates the guard. -- **Surcharge omitted.** - -Each relaxation step can only **lower** the bill: -- the cost per unit mass r^(−a)·m^(a−1) decreases in r, so idle mass is cheapest at the cap; -- r^(1−a) is subadditive, so merging a register's climbs into one climb is cheaper; -- the bill is linear in the counts, so fractional counts form a superset; -- the surcharge is a positive term. - -`test_package.py` checks each step at a = 1/99. So a certified "fail" in the relaxation rules out -every construction that satisfies the premises, and a "pass" is only an upper target. - -**Relation to the merged `research/format-limits`.** Under its accounting axioms, format-limits -section A already proves bit a ≤ X* = 6.0005·10⁻³ < 1/99. This model keeps the coverage law and the -in-window child shapes. It drops the per-stage window climb (Win), the B_K schedule (Sch), the -stage count s and slot domination. So its ceilings are weaker but cover a broader scope: -- the helper-free ceiling under O1 is 0.006794 rather than 0.0060005; -- unlike format-limits A.7's one-at-a-time multipliers, it prices **joint** budgets on the actual - PR589 word. - -## Results ([RESULT.json](RESULT.json); verdicts certified at a = 1/99, idle cap 45) - -| Lever (bit, PR589 word) | Root a (certified bracket in receipt) | × ceiling | At 1/99 | +The **proposed** priority revision 3 (open #1272, stacked on open #1240) aims effort at three +levers: the centre path, the rank shape and the coverage law. It quantifies them for the complex +supplier only, and says a large jump also needs the bit side to move. This package asks how those +levers price on the selected **PR589 bit** supplier: +- Which of them can reach the planning target a = 1/99? +- How many full-frame helpers does a given per-call copy charge leave room for? + +## The model and its premises + +Every number is an exact rational interval, computed by [levers.py](levers.py) with the standard +library only (ln by atanh prime chains, exp by Taylor with a remainder bound, outward dyadic +rounding). No repository engine is imported. + +The per-call bill at saving a is B(a) = (1/w) Σ n_r (r/m)^(1−a). This is the bit side of #1240's +coverage-law relaxation, and it rests on these premises: + +- **Coverage law (checked on the record).** Per call, the paid rank mass is (m − u)·w + cst, with + m = 64, w = 888/9 live families per call, u = 1 unpaid coordinate and a copy charge cst = 63 + (nine rank-7 copies). So mass = 63W + 63N = 1,808,352 and D = W − 63N = 10,272. + - This is format-limits (Dfc), checked there in A.4 and in our #1023. It is the bit analogue of + the coverage identity in our open #1012. +- **Local children.** Either the replayed word, or the most favorable in-window shapes: + - every data register is a single rank-7 climb (sources run 1 → 8 and targets 0 → 7, so each + climbs 7); + - every helper is a single climb of rank equal to its width. + + All remaining mass goes to idle children at one rank R, with fractional counts allowed. +- **Copy charge.** The copy charge is carried as rank-7 copies. This is a premise, not a favorable + step: format-limits (Bat) allows copies up to h = 8. The receipt shows that rank-8 carriage + changes no conclusion (O1 at cap 45: 0.006794 → 0.006805; the O2 width-8 boundary stays 104). +- **The idle cap R is a premise tied to the halving depth.** + - `global_k.py` does not cap children; it raises the halving depth HD until 2·maxchild^HD < + m^HD. HD is limited by the invoice's row-coefficient bound, row < 20161. + - The record uses HD = 2 under the PR510 bound (`assemble9.py`: row = HD·(m² + 1) + 10161 = + 18355). HD = 3 would already exceed the bound, so the record's cap is R = 45. + - The merged elementary-cover bound (`r740-hosted-eleven/code/row_bound.py`, which the PR589 + eleven-stage entry uses) admits HD ≤ 4 at this size, so R ≤ 50 (HD = 3) or R ≤ 53 (HD = 4). + - Results are therefore reported at caps 45, 50 and 53. Cap 63 is a robustness bound that neither + invoice admits. +- **Surcharge.** The surcharge is omitted. + +Each relaxation step lowers the bill: +- cost per unit mass r^(−a)·m^(a−1) decreases in r, so idle mass is cheapest at the cap; +- r^(1−a) is subadditive, so merging a register's climbs is cheaper; +- the counts enter linearly, so fractional counts form a superset; +- the surcharge is positive. + +`test_package.py` checks one instance of each step. Consequently, a certified **fail** rules out +every construction that satisfies the premises, while a **pass** is only a target that a real +mechanism must meet with its full paid budget. + +**Relation to the merged `research/format-limits`.** The scopes are complementary, not nested. +- Format-limits argues, with every number checked, that under its axioms the bit saving is at most + X(9) = 4.6072·10⁻³ at s = 9, and X* = 6.0005·10⁻³ over all s. +- This model keeps (P), (Dfc) as the coverage law, the (Bat) caps and the s = 9 data climb of 7. +- It drops (Sch) and slot domination. +- It adds the halving-depth idle cap and rank-7 copy carriage. +- Its O1 ceiling (0.006794 at cap 45) is therefore weaker than X(9), but it prices joint budgets on + the actual word. +- Format-limits A.7's star-scope multiplier (×2.79 at s = 9) is an independent check of the + centre-free row below (×2.771). + +## Results ([RESULT.json](RESULT.json); certified at a = 1/99) + +### Lever table (cap 45) + +| Lever (bit, PR589 word) | Root a (bracket in receipt) | × ceiling | At 1/99 | |---|---:|---:|---| | Word as shipped, ideal idle packing (**packing ceiling**) | 0.001955918756 | 1 | fail | | Centre path free (no rank-7 copies, cst 0) | 0.005419644435 | 2.771 | fail | | Centre path shared by two calls (cst 31.5) | 0.003686367065 | 1.885 | fail | | Two unpaid coordinates per family | 0.007312036734 | 3.738 | fail | | Rank-8 children (window h = 8) | 0.003211353255 | 1.642 | fail | -| Rank-16 children (**beyond the window**) | 0.004730915412 | 2.419 | fail | -| Centre free + rank-8 children | 0.008938289238 | 4.570 | **fail** | +| Rank-16 children (beyond the window) | 0.004730915412 | 2.419 | fail | +| Centre free + rank-8 children | 0.008938289238 | 4.570 | fail | | Centre free + rank-16 children | 0.01316705483 | 6.732 | pass | | Centre free + two unpaid coordinates | 0.01075873179 | 5.501 | pass | +| Two unpaid + ideal in-window shapes (copies kept, 439 rank-8 helpers) | 0.01179413211 | 6.030 | pass | +| Centre free + ideal data + 332 width-8 helpers (in window) | 0.01010213059 | 5.165 | pass | + +The first seven rows also fail at caps 50, 53 and 63. + +The packing ceiling **reproduces our merged #1023's width-8 free-concentration relaxation** +(0.0019559187537, cap 45), here in independent fractional-count arithmetic. #1023 already shows that +no realizable width-8 re-hosting moves the endpoint. Two related values in open #1293: +- its certified D/E value, 0.0017386, bounds the fixed full histogram; +- its screening extremum, 0.0161, ranges over all rank-mass-preserving repackings, including the + local word. + +**What the table says, and what it does not say.** +- **With the shipped local word fixed (439 helpers), centre free + in-window children fails.** + Reaching 1/99 that way needs rank-16 children or a second unpaid coordinate. +- **That is a statement about the shipped helper mass, not about the window.** + - With ideal data shapes and at most 332 width-8 helpers (cap 45), centre free reaches 1/99 + inside the window. The k = 332 / 333 boundary is certified. + - A second unpaid coordinate with in-window ideal shapes reaches 1/99 even at the full copy + charge. + - Fewer helpers or a changed coverage law can therefore substitute for a wider window. + +### O1 (copy charge 63) + +Take no helpers, every data register as a single rank-7 climb, and the nine rank-7 copies. The bill +then exceeds 1 at a = 1/99 at caps 42, 45, 50, 53 and 63: + +| Idle cap | 45 | 53 | 63 | +|---|---:|---:|---:| +| Helper-free ceiling | 0.006794 | 0.007944 | 0.009665 | + +Cap 63 leaves only a 4.3% margin. Under the premises, **no helper design, data shape or idle packing +reaches 1/99 while the bit copy charge stays at 63 per call.** + +### O2 (centre path shared by two calls, copy charge 31.5, full-frame width-8 helpers) + +The table gives the largest helper count that still reaches 1/99. Each count k is certified: k +passes and k + 1 fails. + +| Idle cap (halving depth) | 45 (HD 2, the record) | 50 (HD 3) | 53 (HD 4) | +|---|---:|---:|---:| +| Max width-8 helpers | 104 | 131 | 145 | + +The comparison uses the design-free floors of format-limits section D. They apply to full-frame +helpers in its drop-free monotone-chain model and are cited as argued premises: at least 138 strict +and at least 212 sink-only. +- **Sharing the centre path is not enough for full-frame helpers at halving depth ≤ 3**, because + 104 and 131 are both below 138. +- **At halving depth 4, which the merged elementary-cover row bound admits, the count is 145 ≥ 138**, + so the strict-floor obstruction no longer holds there. +- The sink-only floor (212) is out of reach at every admissible cap. -**Packing ceiling.** With the local word fixed, no idle repacking lifts the bit supplier above -0.0019559, which is +12.8% over the selected bit endpoint 0.0017334. The cap-42 value is 0.0019475; -the cap-63 robustness value is 0.0019982. Open #1293's certified D/E value, 0.0017386, is the bound -for the **fixed** full histogram. Its screening extremum, 0.0161, ranges over all rank-mass-preserving -repackings, including the local word. The value here sits between the two because only the idle -part moves. - -**O1 (copy charge 63).** -- Configuration: no helpers at all, every data register a single rank-7 climb, idle mass at the - cap. -- The bill exceeds 1 at a = 1/99 at caps 42, 45 and 63. At cap 45 the helper-free ceiling is - 0.006794. -- So **as long as the bit copy charge stays at 63 per call, no helper design, data shape or idle - packing reaches 1/99** under these premises. - -**O2 (centre path shared by two calls, copy charge 31.5, cap 45).** The largest helper counts that -still reach 1/99 are certified as boundaries: k passes, and k + 1 fails. - -| Helper width | 8 | 7 | 6 | 4 | 2 | -|---|---:|---:|---:|---:|---:| -| Max helpers | 104 | 110 | 118 | 148 | 229 | - -The comparison uses the design-free helper floors of format-limits section D: at least 138 (strict) -and at least 212 (sink-only targets) bit helpers. Those floors are cited as argued premises, not -re-proved here. Against them: -- **Sharing the centre path is not enough with width-8 helpers.** It leaves room for at most 104, - fewer than either floor. -- Only helpers of width ≤ 4 can meet the strict floor, and only width 2 can meet the sink-only - floor. -- At the robustness cap 63, the width-8 bound becomes 181 helpers. - -**Joint surface (width-8 helpers, cap 45).** The table gives the maximum number of helpers -(including totals) at a = 1/99 for each copy charge per call. "Ideal data" means every data register -is a single rank-7 climb; "shipped data" keeps the replayed shapes. - -| Copy charge per call | 0 | 7 | 14 | 21 | 28 | 31.5 | 35 | 42 | ≥ 49 | -|---|---:|---:|---:|---:|---:|---:|---:|---:|---:| -| Ideal data | 332 | 281 | 230 | 180 | 129 | 104 | 78 | 28 | none | -| Shipped data | 215 | 164 | 113 | 63 | 12 | none | none | none | none | - -The receipt also gives the cap-63 columns and the width sweep at copy charges 0 and 31.5. - -**The complex side and #1272.** The same code reproduces #1240's complex word ceiling, 0.0016900541090 -(m = 73, w = 896/9, cst 64, cap 51). It then prices #1272's combined lever, "centre free and rank-16": -- The combined lever gives 0.011008 (×6.514, matching #1272's 6.5×). This **requires rank-16 local - children**, larger than the complex stage window h = 9. -- Inside the window, with rank-9 children, the same combination gives **0.008128 < 1/99**. - -The bit side behaves the same way: centre free + rank-8 children gives 0.00894 < 1/99. Read either -way, **a 1/99-scale gain from these levers needs a wider local frame window, or a second unpaid -coordinate, on top of freeing the centre path.** +Narrower helpers are listed in the receipt as budget counts only. The floors are width-free for +full-frame helpers, and narrower helpers face their own (higher) cover floors, so no floor +comparison is made for them. + +### Joint surface (width-8 helpers) + +This table gives the most helpers (including totals) that still reach 1/99. Each cell shows the +three admissible caps, 45 / 50 / 53, and "none" means no helper count reaches it. + +| Copy charge per call | 0 | 7 | 14 | 21 | 28 | 31.5 | 35 | 42 | 49 | 56 | +|---|---|---|---|---|---|---|---|---|---|---| +| Ideal data | 332/346/353 | 281/298/307 | 230/250/260 | 180/203/214 | 129/155/168 | 104/131/145 | 78/107/122 | 28/59/75 | none/11/29 | none | +| Shipped data shapes | 215/236/246 | 164/188/200 | 113/140/154 | 63/92/107 | 12/45/61 | none/21/38 | none/none/15 | none | none | none | + +For shipped data ladders, format-limits D raises the full-frame floor to 222. Even with the centre +path free, the shipped-shape row stays below 222 at cap 45 (215). It exceeds 222 only at caps 50 +and 53. + +### The complex side and #1272 + +The same code reproduces #1240's complex ceiling, 0.0016900541090 (m = 73, w = 896/9, cst 64, +cap 51), and prices #1272's combined lever. + +| Complex lever | Root a | At 1/99 | +|---|---:|---| +| Centre free + rank-16 children (#1272's ×6.5) | 0.011008 | pass, but needs children beyond the stage window h = 9 | +| Centre free + rank-9 children (in window) | 0.008128 | fail | +| Centre free + two unpaid coordinates (shipped word) | 0.009410 | fail | +| Two unpaid + rank-9 children (in window) | 0.010911 | pass | + +So #1272's headline combination relies on rank-16 children. In-window alternatives exist: a second +unpaid coordinate with rank-9 shapes, or, on the bit side, fewer helpers. ## Bindings and replay -The bindings are checked in this order (B1–B5): -1. A record names the frontier1094 certificate. This is the selected record, or a checkpoint once - the frontier moves. -2. The certificate pins `PR589-EXPECTED.json` (`b9f0e5ca…`). -3. That record pins the bit word `bitE8mut-p111-tuned.json.gz` (`e3e301e6…`), the bit profile, the - endpoint and the halving depth. -4. The halving-guard source line is required verbatim. - -**Positive control (P1).** Using the full selected bit profile with the inherited surcharge, the new -code accepts the endpoint 0.001733427039589844234749 and rejects the next 1e-24 grid point. Without -the surcharge, it would also accept that next point. - -**Replay (R1–R3).** -- Every register's frame itinerary is replayed through D, A, B and C, with frame dimensions computed - as rational ranks of the E8 line sets. Every frame change is a climb. -- The local histogram equals the record: `{1:1323, 2:1342, 3:79, 4:44, 5:102, 6:11, 7:19}`, mass 5,129. -- Class split: - - sources `{1:317, 2:209, 3:10, 4:3}` and targets `{1:10, 2:92, 5:92, 6:10, 7:9}`, mass 777 each; - - 430 helpers `{1:969, 2:1041, 3:69, 4:41, 5:1, 6:1, 7:1}`, mass 3,440; - - 9 retained totals `{1:27, 5:9}`, mass 72; +**Bindings (B1–B5).** +- A record names the frontier1094 certificate: the selected record, or a checkpoint once the + frontier moves. +- The certificate pins `PR589-EXPECTED.json` (`b9f0e5ca…`). That record pins the bit word + (`e3e301e6…`), the profile, the endpoint, the halving depth and the row coefficient. +- The following source lines are required verbatim: + - the PR510 row formula and guard (`assemble9.py`); + - the elementary-cover row bound (`row_bound.py`); + - the adaptive halving depth (`global_k.py`). + +**Positive control (P1).** With the inherited surcharge, the full selected profile accepts +0.001733427039589844234749 and rejects the next 1e-24 point. Without the surcharge, the next point +would pass. + +**Replay (R1–R3).** Each register's frame itinerary is replayed through D, A, B and C, with +rational ranks of the E8 lines; every change is a climb. +- The local histogram equals the record: `{1:1323, 2:1342, 3:79, 4:44, 5:102, 6:11, 7:19}`, mass + 5,129. +- The class split: + - sources and targets, mass 777 each; + - 430 helpers, mass 3,440; + - 9 retained totals, mass 72; - 9 rank-7 copies. -- The profile is exactly 288 × the local word plus idle children `{2:13920, 4:14208, 6:14208, - 7:21312, 42:288}`. - -## Controls ([test_package.py](test_package.py), 12 tests, < 2 s) - -- **Interval engine.** It contains the float values. -- **Selected endpoint.** It is accepted, the next grid point is rejected, and omitting the surcharge - would accept the next point. -- **Favorable-relaxation steps.** - - One rank-7 climb is cheaper than a 3 + 4 split. - - Idle mass at rank 45 is cheaper than at rank 42, and rank 63 is cheaper than rank 45. - - The surcharge only raises the bill. -- **Guards.** Excess local mass is rejected by the coverage law. An idle child of rank 64 is - rejected. The cap is 45, since 46 violates the guard. -- **O1 and O2.** O1 fails at caps 42, 45 and 63. The O2 boundary is certified: 104 passes and 105 - fails. -- **Replay.** A gate moved to the empty frame is rejected, and so is a tampered record histogram. -- **Receipt.** The receipt values are reproduced. +- The profile equals 288 local words plus the idle children. + +## Controls ([test_package.py](test_package.py): 15 tests, < 2 s) + +- **Interval engine.** Its intervals contain the float values. +- **Selected endpoint and neighbours.** Includes the case without the surcharge. +- **Relaxation steps.** One instance each of merging climbs, idle mass at the largest rank, and the + surcharge. +- **Guards.** The coverage-law and rank guards hold, and the halving-depth cap table is checked: + - caps 45/50/53/55 for halving depths 2–5; + - only depth 2 is admissible under PR510; + - depths 2–4 are admissible under the elementary-cover bound. +- **O1.** It fails at every cap. +- **O2 boundaries.** 104/105 at cap 45, 131/132 at cap 50 and 145/146 at cap 53. +- **Centre free in window.** 332 helpers pass and 333 fail. +- **Tampering.** A tampered replay gate is rejected, and so is a tampered record histogram. +- **Receipt.** The receipt values are checked. ## Reproduce ```sh -python3 -I -B research/bit-revision3-levers-seed03/verify.py # ~8 s; PASS_BIT_REVISION3_LEVERS (RESULT.json byte-identical) +python3 -I -B research/bit-revision3-levers-seed03/verify.py # ~13 s; PASS_BIT_REVISION3_LEVERS (RESULT.json byte-identical) python3 -I -B -m unittest discover -s research/bit-revision3-levers-seed03 -p test_package.py python3.12 scripts/research_package.py --package research/bit-revision3-levers-seed03 ``` ## Scope and what is not claimed -- **A relaxation, not a construction.** A "pass" row is an upper target that any real mechanism must - meet with its full paid budget. It is not a construction. -- **Premises of the fail rows.** They hold under the coverage law, the in-window child shapes, the - idle cap and the copy charge carried as rank-7 copies. O2 also depends on format-limits section D's - floors, which are argued there and given the crossing lemma. -- **Rank-16 children** are stated as being beyond the current stage windows, h = 8 for bit and - h = 9 for complex, as in format-limits (Win). A changed window is a different architecture. -- **Inherited conditions.** All-size/compiler, hosting, precision/tape, analytic-transfer and - PR589 H1–H5 conditions are inherited and untouched. +- **Relaxation, not construction.** This is a relaxation, not a construction, and κ is unchanged. A + pass row is only a target. +- **Conditions on the fail rows.** + - All fail rows hold under the coverage law, the in-window child shapes, rank-7 copy carriage and + the stated idle cap. + - O2 also needs format-limits D's argued floors for full-frame helpers, and holds only at halving + depth ≤ 3. + - O1 holds at every cap, including 63. +- **Rank-16 children** lie beyond today's stage windows (h = 8 bit, h = 9 complex). Using them is a + different architecture. +- **Inherited conditions.** The inherited all-size/compiler, hosting, precision/tape, + analytic-transfer and PR589 H1–H5 conditions are untouched. ## Overlap and credit **Overlap** - -- **#1240** (Douglas Colkitt / Mister-Meeseeks): the complex local-word ceiling and `levers.py`. - This package is the bit-side analogue in independent code and reproduces #1240's complex ceiling. -- **#1272** (Mister-Meeseeks): director revision 3. Its levers are quantified here for the bit side, - and its combined lever is located relative to the stage window. -- **#1293** (navinor): the a < D/E diagnostic and the bit screening extremum, reconciled above. -- **`research/format-limits`**: the format ceiling X* (section A), the scope multipliers (A.7) and - the helper floors (section D, cited as premises). -- **#974** (avirazza): the interface budget and bit headroom, including COPY deletion alone, which is complementary. -- **#1023** (ours) and **#1281** (mightyOil): width-7 hosting relaxations. Both ignore stage windows, - and the widths here are local-shape widths only. -- **#1194, #1311, #1179, #1253 and #1128**: these saturate the card's helper-interface question. -- **Discussion #1317** (bitplane): an active claim on the register-model card. +- **#1240** (Mister-Meeseeks; prepared by Douglas Colkitt): the complex local-word ceiling and + `levers.py`. This package is the bit-side analogue, in independent code. +- **#1272**: the proposed revision 3. +- **#1293** (navinor): proof and certification of Colkitt's a < D/E diagnostic, plus a bit + screening extremum. Reconciled above. +- **Merged `research/format-limits`**: sections A, A.4, A.7 and D. +- **#974** (avirazza): PR589 interface budget and bit headroom, including COPY deletion. +- **Our merged #1023**: the packing ceiling reproduced above, plus width-7 hosting. It models + windows; only the timing of hosting is unchecked. +- **#1281** (mightyOil): partial width-7 optima. +- **The card's helper-interface question** is saturated by #1194, #1311, #1179, #1253 and #1128. +- **The register-model card** is done in PR #1333 (bitplane; claim #1317). **Credit** - -- DreamingOfClouds (PR589) and eumemic (PR555): the bit supplier. +- DreamingOfClouds (PR589, and format-limits) and eumemic (PR555): the bit supplier. - DaysSky and the PR510/PR442 template and hosting lineage. -- The format-limits authors. +- The elementary-cover row bound authors. - Douglas Colkitt (#1240, #1272) and navinor (#1293). - -Prepared by Sagar Thakrar (thakrarsagar) with substantial AI assistance from Claude (Anthropic) via -Claude Code. Parallel read-only scout and judge subagents proposed and ranked this question. New -material is Apache-2.0. +- Prepared by Sagar Thakrar (thakrarsagar) with substantial AI assistance from Claude (Anthropic) via + Claude Code. Parallel read-only scout and judge subagents ranked the question. A post-PR + adversarial review found the halving-depth error and two overclaims, all corrected here. New + material is Apache-2.0. ## Open next questions -1. **Does the idle-rank cap change with halving depth?** Every verdict is reported at the - halving-guard cap 45. - - First step: re-derive the guard for halving depths 2 and 3 from `global_k.py` and re-run the - surface. -2. **Can a bit centre-path-sharing mechanism keep every data register a single rank-7 climb?** The - shipped-shape rows show how much the ideal-data rows assume. +1. **At which halving depth does a concrete bit construction run, under which row bound?** O2 holds + at depth ≤ 3 and flips at depth 4. + - First step: price the selected profile's row coefficient under the elementary-cover bound at + depths 3 and 4, and check the other finite guards. +2. **Can a centre-path-sharing mechanism keep every data register a single rank-7 climb, with at + most 104–145 full-frame helpers?** - First step: replay a two-call shared-centre toy on a small E8 sub-word. -3. **What would a rank-16 local window cost?** On both sides, the 1/99 combinations need children - beyond today's windows. - - First step: price a window-16 stage in format-limits' (Win)/(Dfc) accounting, including its - invoice. +3. **What does each in-window alternative to rank-16 children cost?** The alternatives are a second + unpaid coordinate, or fewer helpers (≤ 332 with the centre free). + - First step: price a second unpaid coordinate in format-limits' (Dfc)/(Win) accounting, together + with its invoice. diff --git a/research/bit-revision3-levers-seed03/RESULT.json b/research/bit-revision3-levers-seed03/RESULT.json index e733358b59..5d66784e72 100644 --- a/research/bit-revision3-levers-seed03/RESULT.json +++ b/research/bit-revision3-levers-seed03/RESULT.json @@ -1,37 +1,68 @@ { "O1": { - "format_limits_bit_X_star": "6.0005e-3 (research/format-limits section A, stronger axioms)", - "helper_free_ceiling_bracket": [ - "74705045347/10995116277760", - "18676261337/2748779069440" - ], - "helper_free_ceiling_cap45": "0.006794384294", - "statement": "copy charge 63 per call, no helpers, every data register one rank-7 climb, idle at cap R", + "copies_at_rank8_ceiling": { + "45": "0.006805389536", + "63": "0.009687175715" + }, + "format_limits_bit": "X(9) = 4.6072e-3 at s = 9 and X* = 6.0005e-3 over all s (research/format-limits section A, its axioms)", + "helper_free_ceiling": { + "45": { + "bracket": [ + "74705045347/10995116277760", + "18676261337/2748779069440" + ], + "root": "0.006794384294" + }, + "53": { + "bracket": [ + "87342782769/10995116277760", + "8734278277/1099511627776" + ], + "root": "0.007943779817" + }, + "63": { + "bracket": [ + "26566576549/2748779069440", + "106266306197/10995116277760" + ], + "root": "0.009664864246" + } + }, + "statement": "copy charge 63 per call (as nine rank-7 copies), no helpers, every data register one rank-7 climb, idle at cap R", "verdicts": { + "42": "fail", "45": "fail", + "50": "fail", + "53": "fail", "63": "fail" } }, "O2": { + "by_cap": { + "45": { + "below_strict_floor": true, + "max_width8_helpers": 104, + "next": "fail" + }, + "50": { + "below_strict_floor": true, + "max_width8_helpers": 131, + "next": "fail" + }, + "53": { + "below_strict_floor": false, + "max_width8_helpers": 145, + "next": "fail" + } + }, + "copies_at_rank8_cap45": 104, "floors": { + "shipped_ladders": 222, "sink_only": 212, "strict": 138 }, - "max_helpers_by_width": { - "2": 229, - "4": 148, - "6": 118, - "7": 110, - "8": 104 - }, - "statement": "copy charge 63/2 per call (centre path shared by two calls), every data register one rank-7 climb, helpers one climb of rank = width, idle at the cap 45; floors from research/format-limits section D (argued premises)", - "widths_meeting_sink_only_floor": [ - 2 - ], - "widths_meeting_strict_floor": [ - 4, - 2 - ] + "holds_for": "halving depth 2 (cap 45, the record) and depth 3 (cap 50); fails at depth 4 (cap 53)", + "statement": "copy charge 63/2 per call (centre path shared by two calls), every data register one rank-7 climb, full-frame (width-8) helpers as one rank-8 climb, idle at cap R; floors from research/format-limits section D for full-frame helpers (argued premises)" }, "binding": { "assembly": "research/community-frontier1094-audit/ASSEMBLY.json", @@ -59,11 +90,27 @@ "root_hi": "2150555415/1099511627776", "root_lo": "21505554149/10995116277760" }, + { + "at_1_over_99": "fail", + "idle_cap": 50, + "lever": "PR589 bit word, ideal idle packing", + "root": "0.001968964606", + "root_hi": "5412248699/2748779069440", + "root_lo": "4329798959/2199023255552" + }, + { + "at_1_over_99": "fail", + "idle_cap": 53, + "lever": "PR589 bit word, ideal idle packing", + "root": "0.00197625314", + "root_hi": "5432283267/2748779069440", + "root_lo": "21729133067/10995116277760" + }, { "at_1_over_99": "fail", "idle_cap": 63, "lever": "PR589 bit word, ideal idle packing", - "note": "beyond the halving guard; robustness only", + "note": "inadmissible under both row bounds; robustness only", "root": "0.001998187918", "root_hi": "1098515425/549755813888", "root_lo": "21970308499/10995116277760" @@ -105,6 +152,22 @@ "root": "0.01100842544", "root_hi": "121038917721/10995116277760", "root_lo": "3025972943/274877906944" + }, + { + "at_1_over_99": "fail", + "lever": "centre free + two unpaid coordinates", + "multiplier": "5.568", + "root": "0.009409963999", + "root_hi": "51731824169/5497558138880", + "root_lo": "103463648337/10995116277760" + }, + { + "at_1_over_99": "pass", + "lever": "two unpaid + rank-9 children (window h = 9)", + "multiplier": "6.456", + "root": "0.01091096891", + "root_hi": "119967371843/10995116277760", + "root_lo": "59983685921/5497558138880" } ], "w": "896/9" @@ -120,8 +183,15 @@ { "copy_charge": "0", "helper_width": 8, - "idle_cap": 63, - "max_helpers": 372, + "idle_cap": 50, + "max_helpers": 346, + "next": "fail" + }, + { + "copy_charge": "0", + "helper_width": 8, + "idle_cap": 53, + "max_helpers": 353, "next": "fail" }, { @@ -134,8 +204,15 @@ { "copy_charge": "0", "helper_width": 7, - "idle_cap": 63, - "max_helpers": 399, + "idle_cap": 50, + "max_helpers": 368, + "next": "fail" + }, + { + "copy_charge": "0", + "helper_width": 7, + "idle_cap": 53, + "max_helpers": 377, "next": "fail" }, { @@ -148,8 +225,15 @@ { "copy_charge": "0", "helper_width": 6, - "idle_cap": 63, - "max_helpers": 435, + "idle_cap": 50, + "max_helpers": 398, + "next": "fail" + }, + { + "copy_charge": "0", + "helper_width": 6, + "idle_cap": 53, + "max_helpers": 408, "next": "fail" }, { @@ -162,8 +246,15 @@ { "copy_charge": "0", "helper_width": 4, - "idle_cap": 63, - "max_helpers": 555, + "idle_cap": 50, + "max_helpers": 500, + "next": "fail" + }, + { + "copy_charge": "0", + "helper_width": 4, + "idle_cap": 53, + "max_helpers": 515, "next": "fail" }, { @@ -176,8 +267,36 @@ { "copy_charge": "0", "helper_width": 2, - "idle_cap": 63, - "max_helpers": 885, + "idle_cap": 50, + "max_helpers": 783, + "next": "fail" + }, + { + "copy_charge": "0", + "helper_width": 2, + "idle_cap": 53, + "max_helpers": 810, + "next": "fail" + }, + { + "copy_charge": "0", + "helper_width": 1, + "idle_cap": 45, + "max_helpers": 1192, + "next": "fail" + }, + { + "copy_charge": "0", + "helper_width": 1, + "idle_cap": 50, + "max_helpers": 1284, + "next": "fail" + }, + { + "copy_charge": "0", + "helper_width": 1, + "idle_cap": 53, + "max_helpers": 1333, "next": "fail" }, { @@ -190,8 +309,15 @@ { "copy_charge": "63/2", "helper_width": 8, - "idle_cap": 63, - "max_helpers": 181, + "idle_cap": 50, + "max_helpers": 131, + "next": "fail" + }, + { + "copy_charge": "63/2", + "helper_width": 8, + "idle_cap": 53, + "max_helpers": 145, "next": "fail" }, { @@ -204,8 +330,15 @@ { "copy_charge": "63/2", "helper_width": 7, - "idle_cap": 63, - "max_helpers": 194, + "idle_cap": 50, + "max_helpers": 139, + "next": "fail" + }, + { + "copy_charge": "63/2", + "helper_width": 7, + "idle_cap": 53, + "max_helpers": 154, "next": "fail" }, { @@ -218,8 +351,15 @@ { "copy_charge": "63/2", "helper_width": 6, - "idle_cap": 63, - "max_helpers": 212, + "idle_cap": 50, + "max_helpers": 151, + "next": "fail" + }, + { + "copy_charge": "63/2", + "helper_width": 6, + "idle_cap": 53, + "max_helpers": 167, "next": "fail" }, { @@ -232,8 +372,15 @@ { "copy_charge": "63/2", "helper_width": 4, - "idle_cap": 63, - "max_helpers": 270, + "idle_cap": 50, + "max_helpers": 189, + "next": "fail" + }, + { + "copy_charge": "63/2", + "helper_width": 4, + "idle_cap": 53, + "max_helpers": 211, "next": "fail" }, { @@ -246,8 +393,36 @@ { "copy_charge": "63/2", "helper_width": 2, - "idle_cap": 63, - "max_helpers": 431, + "idle_cap": 50, + "max_helpers": 297, + "next": "fail" + }, + { + "copy_charge": "63/2", + "helper_width": 2, + "idle_cap": 53, + "max_helpers": 332, + "next": "fail" + }, + { + "copy_charge": "63/2", + "helper_width": 1, + "idle_cap": 45, + "max_helpers": 373, + "next": "fail" + }, + { + "copy_charge": "63/2", + "helper_width": 1, + "idle_cap": 50, + "max_helpers": 487, + "next": "fail" + }, + { + "copy_charge": "63/2", + "helper_width": 1, + "idle_cap": 53, + "max_helpers": 547, "next": "fail" } ], @@ -258,6 +433,14 @@ "max_helpers": 332, "next": "fail" }, + "ideal_data_width8_cap50": { + "max_helpers": 346, + "next": "fail" + }, + "ideal_data_width8_cap53": { + "max_helpers": 353, + "next": "fail" + }, "ideal_data_width8_cap63": { "max_helpers": 372, "next": "fail" @@ -266,6 +449,14 @@ "max_helpers": 215, "next": "fail" }, + "shipped_data_width8_cap50": { + "max_helpers": 236, + "next": "fail" + }, + "shipped_data_width8_cap53": { + "max_helpers": 246, + "next": "fail" + }, "shipped_data_width8_cap63": { "max_helpers": 274, "next": "fail" @@ -277,6 +468,14 @@ "max_helpers": 281, "next": "fail" }, + "ideal_data_width8_cap50": { + "max_helpers": 298, + "next": "fail" + }, + "ideal_data_width8_cap53": { + "max_helpers": 307, + "next": "fail" + }, "ideal_data_width8_cap63": { "max_helpers": 330, "next": "fail" @@ -285,6 +484,14 @@ "max_helpers": 164, "next": "fail" }, + "shipped_data_width8_cap50": { + "max_helpers": 188, + "next": "fail" + }, + "shipped_data_width8_cap53": { + "max_helpers": 200, + "next": "fail" + }, "shipped_data_width8_cap63": { "max_helpers": 232, "next": "fail" @@ -296,6 +503,14 @@ "max_helpers": 230, "next": "fail" }, + "ideal_data_width8_cap50": { + "max_helpers": 250, + "next": "fail" + }, + "ideal_data_width8_cap53": { + "max_helpers": 260, + "next": "fail" + }, "ideal_data_width8_cap63": { "max_helpers": 287, "next": "fail" @@ -304,6 +519,14 @@ "max_helpers": 113, "next": "fail" }, + "shipped_data_width8_cap50": { + "max_helpers": 140, + "next": "fail" + }, + "shipped_data_width8_cap53": { + "max_helpers": 154, + "next": "fail" + }, "shipped_data_width8_cap63": { "max_helpers": 189, "next": "fail" @@ -315,6 +538,14 @@ "max_helpers": 180, "next": "fail" }, + "ideal_data_width8_cap50": { + "max_helpers": 203, + "next": "fail" + }, + "ideal_data_width8_cap53": { + "max_helpers": 214, + "next": "fail" + }, "ideal_data_width8_cap63": { "max_helpers": 245, "next": "fail" @@ -323,6 +554,14 @@ "max_helpers": 63, "next": "fail" }, + "shipped_data_width8_cap50": { + "max_helpers": 92, + "next": "fail" + }, + "shipped_data_width8_cap53": { + "max_helpers": 107, + "next": "fail" + }, "shipped_data_width8_cap63": { "max_helpers": 147, "next": "fail" @@ -334,6 +573,14 @@ "max_helpers": 129, "next": "fail" }, + "ideal_data_width8_cap50": { + "max_helpers": 155, + "next": "fail" + }, + "ideal_data_width8_cap53": { + "max_helpers": 168, + "next": "fail" + }, "ideal_data_width8_cap63": { "max_helpers": 202, "next": "fail" @@ -342,6 +589,14 @@ "max_helpers": 12, "next": "fail" }, + "shipped_data_width8_cap50": { + "max_helpers": 45, + "next": "fail" + }, + "shipped_data_width8_cap53": { + "max_helpers": 61, + "next": "fail" + }, "shipped_data_width8_cap63": { "max_helpers": 104, "next": "fail" @@ -353,11 +608,27 @@ "max_helpers": 104, "next": "fail" }, + "ideal_data_width8_cap50": { + "max_helpers": 131, + "next": "fail" + }, + "ideal_data_width8_cap53": { + "max_helpers": 145, + "next": "fail" + }, "ideal_data_width8_cap63": { "max_helpers": 181, "next": "fail" }, "shipped_data_width8_cap45": null, + "shipped_data_width8_cap50": { + "max_helpers": 21, + "next": "fail" + }, + "shipped_data_width8_cap53": { + "max_helpers": 38, + "next": "fail" + }, "shipped_data_width8_cap63": { "max_helpers": 83, "next": "fail" @@ -369,11 +640,24 @@ "max_helpers": 78, "next": "fail" }, + "ideal_data_width8_cap50": { + "max_helpers": 107, + "next": "fail" + }, + "ideal_data_width8_cap53": { + "max_helpers": 122, + "next": "fail" + }, "ideal_data_width8_cap63": { "max_helpers": 160, "next": "fail" }, "shipped_data_width8_cap45": null, + "shipped_data_width8_cap50": null, + "shipped_data_width8_cap53": { + "max_helpers": 15, + "next": "fail" + }, "shipped_data_width8_cap63": { "max_helpers": 62, "next": "fail" @@ -385,11 +669,21 @@ "max_helpers": 28, "next": "fail" }, + "ideal_data_width8_cap50": { + "max_helpers": 59, + "next": "fail" + }, + "ideal_data_width8_cap53": { + "max_helpers": 75, + "next": "fail" + }, "ideal_data_width8_cap63": { "max_helpers": 117, "next": "fail" }, "shipped_data_width8_cap45": null, + "shipped_data_width8_cap50": null, + "shipped_data_width8_cap53": null, "shipped_data_width8_cap63": { "max_helpers": 19, "next": "fail" @@ -398,31 +692,141 @@ { "copy_charge": "49", "ideal_data_width8_cap45": null, + "ideal_data_width8_cap50": { + "max_helpers": 11, + "next": "fail" + }, + "ideal_data_width8_cap53": { + "max_helpers": 29, + "next": "fail" + }, "ideal_data_width8_cap63": { "max_helpers": 75, "next": "fail" }, "shipped_data_width8_cap45": null, + "shipped_data_width8_cap50": null, + "shipped_data_width8_cap53": null, "shipped_data_width8_cap63": null }, { "copy_charge": "56", "ideal_data_width8_cap45": null, + "ideal_data_width8_cap50": null, + "ideal_data_width8_cap53": null, "ideal_data_width8_cap63": { "max_helpers": 32, "next": "fail" }, "shipped_data_width8_cap45": null, + "shipped_data_width8_cap50": null, + "shipped_data_width8_cap53": null, "shipped_data_width8_cap63": null }, { "copy_charge": "63", "ideal_data_width8_cap45": null, + "ideal_data_width8_cap50": null, + "ideal_data_width8_cap53": null, "ideal_data_width8_cap63": null, "shipped_data_width8_cap45": null, + "shipped_data_width8_cap50": null, + "shipped_data_width8_cap53": null, "shipped_data_width8_cap63": null } ], + "lever_fails_at_larger_caps": { + "50": [ + { + "at_1_over_99": "fail", + "lever": "PR589 bit word, ideal idle packing (packing ceiling)" + }, + { + "at_1_over_99": "fail", + "lever": "centre path free (no rank-7 copies, copy charge 0)" + }, + { + "at_1_over_99": "fail", + "lever": "centre path shared by two calls (copies and charge halved)" + }, + { + "at_1_over_99": "fail", + "lever": "two unpaid coordinates per family" + }, + { + "at_1_over_99": "fail", + "lever": "rank-8 children (local mass at rank 8 = window h)" + }, + { + "at_1_over_99": "fail", + "lever": "rank-16 children (beyond the window h = 8)" + }, + { + "at_1_over_99": "fail", + "lever": "centre free + rank-8 children" + } + ], + "53": [ + { + "at_1_over_99": "fail", + "lever": "PR589 bit word, ideal idle packing (packing ceiling)" + }, + { + "at_1_over_99": "fail", + "lever": "centre path free (no rank-7 copies, copy charge 0)" + }, + { + "at_1_over_99": "fail", + "lever": "centre path shared by two calls (copies and charge halved)" + }, + { + "at_1_over_99": "fail", + "lever": "two unpaid coordinates per family" + }, + { + "at_1_over_99": "fail", + "lever": "rank-8 children (local mass at rank 8 = window h)" + }, + { + "at_1_over_99": "fail", + "lever": "rank-16 children (beyond the window h = 8)" + }, + { + "at_1_over_99": "fail", + "lever": "centre free + rank-8 children" + } + ], + "63": [ + { + "at_1_over_99": "fail", + "lever": "PR589 bit word, ideal idle packing (packing ceiling)" + }, + { + "at_1_over_99": "fail", + "lever": "centre path free (no rank-7 copies, copy charge 0)" + }, + { + "at_1_over_99": "fail", + "lever": "centre path shared by two calls (copies and charge halved)" + }, + { + "at_1_over_99": "fail", + "lever": "two unpaid coordinates per family" + }, + { + "at_1_over_99": "fail", + "lever": "rank-8 children (local mass at rank 8 = window h)" + }, + { + "at_1_over_99": "fail", + "lever": "rank-16 children (beyond the window h = 8)" + }, + { + "at_1_over_99": "fail", + "lever": "centre free + rank-8 children" + } + ] + }, "levers": [ { "at_1_over_99": "fail", @@ -504,6 +908,24 @@ "root": "0.01075873179", "root_hi": "23658701413/2199023255552", "root_lo": "14786688383/1374389534720" + }, + { + "at_1_over_99": "pass", + "idle_cap": 45, + "lever": "two unpaid + ideal in-window shapes (222 rank-7 data, 439 rank-8 helpers, copies kept)", + "multiplier": "6.03", + "root": "0.01179413211", + "root_hi": "129677853937/10995116277760", + "root_lo": "8104865871/687194767360" + }, + { + "at_1_over_99": "pass", + "idle_cap": 45, + "lever": "centre free + ideal data + 332 width-8 helpers (in window)", + "multiplier": "5.165", + "root": "0.01010213059", + "root_hi": "111074100463/10995116277760", + "root_lo": "55537050231/5497558138880" } ], "replay": { @@ -548,7 +970,40 @@ "copy_charge_per_call": 63, "deficit": 10272, "deficit_identity": "D = W - 63 N", - "halving_guard_cap": 45, + "halving_depths": [ + { + "elementary_cover_admissible": true, + "elementary_cover_row": 14341, + "halving_depth": 2, + "idle_cap": 45, + "pr510_admissible": true, + "pr510_row": 18355 + }, + { + "elementary_cover_admissible": true, + "elementary_cover_row": 16431, + "halving_depth": 3, + "idle_cap": 50, + "pr510_admissible": false, + "pr510_row": 22452 + }, + { + "elementary_cover_admissible": true, + "elementary_cover_row": 18521, + "halving_depth": 4, + "idle_cap": 53, + "pr510_admissible": false, + "pr510_row": 26549 + }, + { + "elementary_cover_admissible": false, + "elementary_cover_row": 20611, + "halving_depth": 5, + "idle_cap": 55, + "pr510_admissible": false, + "pr510_row": 30646 + } + ], "idle_children_total": { "2": "13920", "4": "14208", @@ -567,6 +1022,7 @@ "7": "19" }, "local_mass": 5129, + "record_idle_cap": 45, "replicas": 32, "stages": 9, "v": 111, diff --git a/research/bit-revision3-levers-seed03/TASK.json b/research/bit-revision3-levers-seed03/TASK.json index 701e63682c..c5552dbc16 100644 --- a/research/bit-revision3-levers-seed03/TASK.json +++ b/research/bit-revision3-levers-seed03/TASK.json @@ -40,32 +40,32 @@ ] }, "scope_status": "changed", - "actual_scope": "Certified bit-side budgets for priority revision 3: in the coverage-law relaxation of the selected PR589 bit word (fixed local word or most favorable in-window shapes, idle mass at the halving-guard cap 45, fractional counts, no surcharge), the packing ceiling, each revision-3 lever and combination at a = 1/99, and the joint copy-charge x helper-count x helper-width surface, with scoped obstructions O1 (copy charge 63) and O2 (centre path shared by two calls against the design-free helper floors).", - "scope_change_reason": "The card's helper-interface question is saturated or claimed (semantic-D contract #1194/#1311, entrances #1179/#1253, after-B frames #1128; register-model card actively claimed in #1317), while revision 3 (#1272) quantifies its levers on the complex side only and #1293 leaves the bit word's realizability-aware ceiling open. The bit-side budget answers what any bit helper or centre-path mechanism must meet to reach the 1/99 planning target.", - "bottleneck_link": "A large kappa jump needs both suppliers to advance (bottleneck brief, priority log). This gives the bit side's quantitative targets: which levers can reach 1/99 under the coverage law, and how many helpers of which width a given copy charge leaves room for. It also shows that the combined lever of #1272 (and its bit analogue) relies on rank-16 children beyond the stage window. No kappa change.", + "actual_scope": "Certified bit-side budgets for the proposed priority revision 3 (open #1272, stacked on open #1240): in the coverage-law relaxation of the selected PR589 bit word (fixed local word or most favorable in-window shapes, rank-7 copy carriage, idle mass at the halving-depth cap 45/50/53, fractional counts, no surcharge), each lever and combination at a = 1/99, the joint copy-charge x full-frame-helper surface, and scoped obstructions O1 (copy charge 63, every cap) and O2 (shared centre path vs the full-frame helper floor, halving depth <= 3).", + "scope_change_reason": "The card's helper-interface question is saturated (semantic-D contract #1194/#1311, entrances #1179/#1253, after-B frames #1128) and the register-model card is done in PR #1333 (claim #1317). The proposed revision 3 quantifies its levers on the complex side only; this supplies the bit-side numbers any bit centre-path or helper mechanism must meet at the 1/99 planning target. The bit packing ceiling itself reproduces our merged #1023 and is not claimed as new.", + "bottleneck_link": "A large kappa jump needs both suppliers to advance. This gives the bit side's quantitative targets: which levers reach 1/99 under the coverage law, how many full-frame helpers a given copy charge leaves room for at each admissible halving depth, and that #1272's combined lever relies on rank-16 children beyond the stage window while in-window alternatives (fewer helpers, a second unpaid coordinate) exist. No kappa change.", "budget_minutes": 180, "stop_rule": "Stop once every lever, surface boundary and obstruction is certified with exact intervals and the positive controls reproduce the selected bit endpoint and #1240's complex ceiling; report any undecided boundary instead of claiming it.", "outcome": "completed", - "evidence": "RESULT.json: bit word packing ceiling 0.001955918756 (cap 45); centre free x2.771, shared x1.885, two unpaid x3.738, rank-8 x1.642, rank-16 x2.419; centre free + rank-8 0.00894 < 1/99; centre free + rank-16 0.01317 and centre free + two unpaid 0.01076 pass. O1: copy charge 63 fails 1/99 at caps 42/45/63 even helper-free (ceiling 0.00679 at cap 45). O2: with the centre path shared (copy charge 31.5) at cap 45, at most 104 width-8 helpers fit (k=104 passes, 105 fails), below both floors (138 strict, 212 sink-only); only width <= 4 meets the strict floor and width 2 the sink-only floor. Complex cross-check: #1240's ceiling reproduced; #1272's combined lever gives 0.01101 with rank-16 children but 0.00813 < 1/99 inside the window (rank 9). 12 tests pass.", + "evidence": "RESULT.json: packing ceiling 0.001955918756 (cap 45; reproduces #1023's free concentration); levers x2.771/x1.885/x3.738/x1.642/x2.419; with the shipped local mass, centre free + rank-8 fails (0.00894) while centre free + rank-16 (0.01317) and + two unpaid (0.01076) pass; centre free with ideal data and <= 332 width-8 helpers passes in window (0.01010); two unpaid with ideal in-window shapes passes at full copy charge (0.01179). O1: copy charge 63 fails at caps 42/45/50/53/63 (ceilings 0.006794/0.007944/0.009665 at 45/53/63). O2: shared centre leaves 104/131/145 width-8 helpers at caps 45/50/53 (halving depths 2/3/4; certified k/k+1), below the strict floor 138 only at depth <= 3. Complex: #1240 reproduced; #1272's x6.5 needs rank-16; in window centre free + rank-9 0.00813 fails, two unpaid + rank-9 0.01091 passes. 15 tests pass.", "author": "Sagar Thakrar (thakrarsagar)", "ai_assistance": "Substantial: Claude (Anthropic) via Claude Code. Parallel read-only scout and judge subagents proposed and compared four bit-track candidates; this one ranked first on value and overlap.", "open_questions": [ { - "question": "Is the halving-guard cap 45 the right idle-rank limit for every bit recursion depth, or can a changed halving depth admit larger idle children?", - "why_it_matters": "All verdicts are reported at cap 45 with cap 63 as a robustness bound; O1 holds at both, but surface boundaries move with the cap.", - "first_step": "Re-derive the guard from global_k.py's halving_integer_inequality for halving depths 2 and 3 and re-run the surface.", + "question": "At which halving depth, under which row-coefficient bound, does a concrete bit construction run?", + "why_it_matters": "O2 holds at halving depth <= 3 (caps 45, 50) and flips at depth 4 (cap 53), which the merged elementary-cover row bound admits.", + "first_step": "Price the selected profile's row coefficient under the elementary-cover bound at depths 3 and 4 and check the remaining finite guards.", "blocked_by": "None." }, { - "question": "Can a bit centre-path mechanism keep data registers as single rank-7 climbs while sharing the copy charge, or does sharing force split climbs?", - "why_it_matters": "The surface's ideal-data rows assume single climbs; the shipped-data rows show the gap is large (e.g. 104 vs none at copy charge 31.5).", - "first_step": "Construct a two-call shared-centre toy on a small E8 sub-word and replay its climbs.", + "question": "Can a centre-path-sharing mechanism keep every data register a single rank-7 climb with at most 104-145 full-frame helpers?", + "why_it_matters": "The ideal-data rows assume single climbs; shipped shapes leave far less room (e.g. none at cap 45 for copy charge 31.5).", + "first_step": "Replay a two-call shared-centre toy on a small E8 sub-word.", "blocked_by": "A concrete centre-sharing construction." }, { - "question": "Which local frame window (h) would a rank-16-children mechanism need on each side, and what does it cost in the invoice?", - "why_it_matters": "Both the bit and complex combined levers reach 1/99 only with rank-16 children beyond the current windows (h = 8 bit, h = 9 complex).", - "first_step": "Price a window-16 stage in the format-limits (Win)/(Dfc) accounting.", + "question": "What do the in-window alternatives to rank-16 children cost: a second unpaid coordinate, or fewer helpers (<= 332 with the centre free)?", + "why_it_matters": "Both reach 1/99 in this relaxation inside today's windows.", + "first_step": "Price a second unpaid coordinate in format-limits' (Dfc)/(Win) accounting with its invoice.", "blocked_by": "None." } ] diff --git a/research/bit-revision3-levers-seed03/VERIFY.json b/research/bit-revision3-levers-seed03/VERIFY.json index 016eb80ada..4fe0040030 100644 --- a/research/bit-revision3-levers-seed03/VERIFY.json +++ b/research/bit-revision3-levers-seed03/VERIFY.json @@ -19,7 +19,7 @@ "{package}/verify.py" ], "timeout_seconds": 120, - "checks": "Binds selected record -> frontier1094 ASSEMBLY -> PR589 EXPECTED -> bit word and the halving guard; reproduces the selected bit endpoint (accept, next 1e-24 reject, surcharge included) with code-disjoint exact arithmetic; replays the word's local histogram, class split and coverage law; certifies the lever table, cap curve, joint helper/copy-charge surface (k passes, k+1 fails), O1/O2 and the complex cross-check; RESULT.json byte-identical." + "checks": "Binds selected record -> frontier1094 ASSEMBLY -> PR589 EXPECTED -> bit word, and the halving-depth/row-bound sources; reproduces the selected bit endpoint (surcharge included); replays the word's local histogram, class split and coverage law; tabulates admissible idle caps per halving depth; certifies the lever table, cap curve, joint full-frame helper surface (k passes, k+1 fails), O1 (all caps), O2 (holds at depth <= 3, flips at depth 4) and the complex cross-check; RESULT.json byte-identical." }, { "argv": [ @@ -35,7 +35,7 @@ "test_package.py" ], "timeout_seconds": 120, - "checks": "Interval engine sanity, endpoint and neighbour controls, the favorable-relaxation steps (merging climbs, idle at the largest rank, surcharge), coverage-law and rank guards, certified O1/O2 boundaries, replay and record tampering controls, receipt values." + "checks": "Interval engine, endpoint and neighbours, one instance of each relaxation step, coverage-law and rank guards, halving-depth cap table, O1/O2 and in-window centre-free boundaries, replay and record tampering, receipt values." } ] } diff --git a/research/bit-revision3-levers-seed03/test_package.py b/research/bit-revision3-levers-seed03/test_package.py index a66bb511d6..4edf893d7c 100644 --- a/research/bit-revision3-levers-seed03/test_package.py +++ b/research/bit-revision3-levers-seed03/test_package.py @@ -1,5 +1,5 @@ # SPDX-License-Identifier: Apache-2.0 -"""Controls for the bit-side lever budgets (about 20 s). +"""Controls for the bit-side lever budgets (< 2 s; one instance of each relaxation step, fractional counts hold by superset). Run: python3 -I -B -m unittest discover -s research/bit-revision3-levers-seed03 -p test_package.py -v """ @@ -67,6 +67,27 @@ def test_coverage_law_and_rank_guards(self): self.assertEqual(max(r for r in range(1, M) if M * M > 2 * r * r), 45) self.assertFalse(M * M > 2 * 46 * 46) + def test_halving_depth_caps_follow_the_row_bounds(self): + result = json.loads((HERE / 'RESULT.json').read_text()) + rows = {d['halving_depth']: d for d in result['replay']['halving_depths']} + self.assertEqual({k: r['idle_cap'] for k, r in rows.items()}, {2: 45, 3: 50, 4: 53, 5: 55}) + self.assertEqual([k for k, r in rows.items() if r['pr510_admissible']], [2]) + self.assertEqual([k for k, r in rows.items() if r['elementary_cover_admissible']], [2, 3, 4]) + + def test_o2_flips_at_halving_depth_four(self): + base = {7: Q(222) + Q(63, 14)} + for R, k in ((50, 131), (53, 145)): + loc = dict(base) + loc[8] = k + self.assertEqual(L.verdict(L.relaxed(loc, M, w, Q(63, 2), R), M, w, Q(1, 99)), 'pass') + loc[8] = k + 1 + self.assertEqual(L.verdict(L.relaxed(loc, M, w, Q(63, 2), R), M, w, Q(1, 99)), 'fail') + + def test_centre_free_fits_in_window_with_fewer_helpers(self): + # the joint surface, not the window, is what the centre-free lever must meet + self.assertEqual(L.verdict(L.relaxed({7: 222, 8: 332}, M, w, 0, 45), M, w, Q(1, 99)), 'pass') + self.assertEqual(L.verdict(L.relaxed({7: 222, 8: 333}, M, w, 0, 45), M, w, Q(1, 99)), 'fail') + def test_o2_boundary_is_certified(self): base = {7: Q(222) + Q(63, 14)} k, _, nxt = L.max_count(base, 8, M, w, Q(63, 2), 45, Q(1, 99), 600) @@ -79,7 +100,7 @@ def test_o2_boundary_is_certified(self): def test_o1_has_no_room_at_any_admissible_cap(self): base = {7: Q(222) + 9} - for R in (42, 45, 63): + for R in (42, 45, 50, 53, 63): self.assertEqual(L.verdict(L.relaxed(base, M, w, 63, R), M, w, Q(1, 99)), 'fail') @@ -107,7 +128,8 @@ def test_receipt_is_reproduced(self): result = json.loads((HERE / 'RESULT.json').read_text()) self.assertEqual(result['status'], 'PASS_BIT_REVISION3_LEVERS') self.assertEqual(result['levers'][0]['root'], '0.001955918756') - self.assertEqual(result['O2']['max_helpers_by_width']['8'], 104) + self.assertEqual(result['O2']['by_cap']['45']['max_width8_helpers'], 104) + self.assertEqual(result['O2']['by_cap']['53']['max_width8_helpers'], 145) EXPECTED_LOCAL = {int(r): n for r, n in EXP['word']['local_histogram'].items()} diff --git a/research/bit-revision3-levers-seed03/verify.py b/research/bit-revision3-levers-seed03/verify.py index 361a56dc43..8bf313cd3e 100644 --- a/research/bit-revision3-levers-seed03/verify.py +++ b/research/bit-revision3-levers-seed03/verify.py @@ -35,8 +35,14 @@ RECORDS = ('certificates/selected-result.json', 'certificates/checkpoints/frontier1094.json') ASSEMBLY = 'research/community-frontier1094-audit/ASSEMBLY.json' EXPECTED = 'research/e8-bit-p111-tuned/tune/EXPECTED.json' -GUARD = ('research/e8-bit-p111-tuned/vendor/pr510/e8-r480-nine-stage/vendor/e8-r715-eleven-stage-whole/code/global_k.py', - 'halving_integer_inequality=[M**HD,2*max(paid)**HD]') +# The idle-rank cap is not fixed by a guard: global_k.py raises the halving depth HD until +# 2 maxchild^HD < m^HD. HD is limited by the row-coefficient bound row < 20161 of the invoice in use. +INVOICE = ('research/e8-bit-p111-tuned/vendor/pr510/e8-r480-nine-stage/code/assemble9.py', + ['2 * max(P) ** DEPTH < m ** DEPTH', 'row = DEPTH * (m * m + 1) + 9909 + 252']) +ROW_BOUND = ('research/e8-bit-carrier-skeleton/code/hub/r740-hosted-eleven/code/row_bound.py', + ['assert m**depth>2*child**depth', 'row=depth*stock_exponent+9909+252', 'assert row<20161']) +ADAPTIVE = ('research/e8-bit-p111-tuned/vendor/pr510/e8-r480-nine-stage/vendor/e8-r715-eleven-stage-whole/code/global_k.py', + ['while not 2*max(paid)**HD 2 maxchild^2') + for path, lines in (INVOICE, ROW_BOUND, ADAPTIVE): + text = (ROOT / path).read_text() + need(all(line in text for line in lines), 'B5 halving-depth and row-bound sources: ' + path) + need(exp['nine']['bit']['halving_depth'] == 2 and exp['nine']['bit']['row_coefficient'] == 2 * (M * M + 1) + 10161, + 'B5 the record uses halving depth 2 under the PR510 row bound') return dict(record=bound, assembly=ASSEMBLY, assembly_sha256=sha(asm_raw), expected=EXPECTED, expected_sha256=sha(exp_raw), word=str(word_path.relative_to(ROOT)), word_sha256=sha(word_raw)), asm, exp, json.loads(gzip.decompress(word_raw)) @@ -160,14 +169,25 @@ def main(): need(all(c >= 0 for c in idle_total.values()) and max(r for r, c in idle_total.items() if c) <= exp['nine']['bit']['maxchild'], 'R3 the profile is N local words plus idle children') cap = max(r for r in range(1, M) if M * M > 2 * r * r) - need(cap == 45, 'B5 halving-guard cap') + need(cap == 45, 'B5 halving-depth-2 cap') + physical = exp['nine']['bit']['physical'] + overhead = next(k for k in range(64) if 3 ** k > physical) + depths = [] + for depth in range(2, 6): + dcap = max(r for r in range(1, M) if M ** depth > 2 * r ** depth) + depths.append(dict(halving_depth=depth, idle_cap=dcap, + pr510_row=depth * (M * M + 1) + 10161, pr510_admissible=depth * (M * M + 1) + 10161 < 20161, + elementary_cover_row=depth * (M * (M - 1) // 2 + M + overhead) + 10161, + elementary_cover_admissible=depth * (M * (M - 1) // 2 + M + overhead) + 10161 < 20161)) + caps = [d['idle_cap'] for d in depths if d['elementary_cover_admissible']] + need(caps == [45, 50, 53], 'B5 admissible idle caps under the merged elementary-cover row bound') out['replay'] = dict( v=v, replicas=T, stages=stages, calls=N, live=W, w=str(w), copy_charge_per_call=cst, local_histogram=show(local), local_mass=sum(r * c for r, c in local.items()), class_split={k: show(c) for k, c in split.items()}, copies=show(copies), class_mass={k: sum(r * c for r, c in s.items()) for k, s in split.items()}, deficit=M * W - exp['nine']['bit']['rank_mass'], deficit_identity='D = W - %d N' % cst, - idle_children_total=show(+idle_total), halving_guard_cap=cap) + idle_children_total=show(+idle_total), record_idle_cap=cap, halving_depths=depths) # --- revision-3 levers on the bit side (fixed local word unless stated; idle at the cap) mass = sum(r * c for r, c in local.items()) @@ -189,13 +209,20 @@ def lever(name, H_local, c, u=1, R=cap): lever('centre free + rank-8 children', {8: Q(mass - cst, 8)}, 0), lever('centre free + rank-16 children', {16: Q(mass - cst, 16)}, 0), lever('centre free + two unpaid coordinates', +no_copies, 0, u=2), + lever('two unpaid + ideal in-window shapes (222 rank-7 data, 439 rank-8 helpers, copies kept)', + {7: Q(2 * v) + 9, 8: 439}, cst, u=2), + lever('centre free + ideal data + 332 width-8 helpers (in window)', {7: Q(2 * v), 8: 332}, 0), ] base = Q(levers[0]['root_lo']) for row in levers: row['multiplier'] = dec(Q(row['root_lo']) / base, 4) out['levers'] = levers - out['cap_curve'] = [lever('PR589 bit word, ideal idle packing', local, cst, R=R) for R in (42, 45)] + \ - [dict(lever('PR589 bit word, ideal idle packing', local, cst, R=63), note='beyond the halving guard; robustness only')] + out['cap_curve'] = [lever('PR589 bit word, ideal idle packing', local, cst, R=R) for R in (42, 45, 50, 53)] + \ + [dict(lever('PR589 bit word, ideal idle packing', local, cst, R=63), note='inadmissible under both row bounds; robustness only')] + out['lever_fails_at_larger_caps'] = {str(R): [dict(lever=row['lever'], at_1_over_99=verdict( + relaxed(H_, M, w, c_, R, u_), M, w, TARGET)) for row, (H_, c_, u_) in zip(levers[:7], ( + (local, cst, 1), (+no_copies, 0, 1), (half_copies, Q(cst, 2), 1), (local, cst, 2), ({8: Q(mass, 8)}, cst, 1), + ({16: Q(mass, 16)}, cst, 1), ({8: Q(mass - cst, 8)}, 0, 1)))] for R in (50, 53, 63)} # --- joint budget surface at a = 1/99: helpers (one climb of rank = width) per copy charge data_ideal = {7: Q(2 * v)} # each data register a single rank-7 climb @@ -208,7 +235,7 @@ def lever(name, H_local, c, u=1, R=cap): base_ship[7] = base_ship.get(7, 0) + Q(c, 7) row = dict(copy_charge=str(c)) for label, b in (('ideal_data', base_ideal), ('shipped_data', base_ship)): - for R in (cap, 63): + for R in (45, 50, 53, 63): res = max_count(b, 8, M, w, c, R, TARGET, 600) row['%s_width8_cap%d' % (label, R)] = None if res is None else dict(max_helpers=res[0], next=res[2]) surface.append(row) @@ -216,31 +243,38 @@ def lever(name, H_local, c, u=1, R=cap): for c in (0, Q(63, 2)): b = dict(data_ideal) b[7] = b.get(7, 0) + Q(c, 7) - for width in (8, 7, 6, 4, 2): - for R in (cap, 63): + for width in (8, 7, 6, 4, 2, 1): + for R in (45, 50, 53): res = max_count(b, width, M, w, c, R, TARGET, 2000) widths.append(dict(copy_charge=str(c), helper_width=width, idle_cap=R, max_helpers=None if res is None else res[0], next=None if res is None else res[2])) out['joint_surface'] = surface out['helper_width'] = widths # obstruction rows, restated as certified verdicts - o1 = {R: verdict(relaxed({7: Q(2 * v) + Q(cst, 7)}, M, w, cst, R), M, w, TARGET) for R in (cap, 63)} - need(o1 == {cap: 'fail', 63: 'fail'}, 'O1 copy charge 63 cannot reach 1/99 in the relaxation') - o1_lo, o1_hi = root(relaxed({7: Q(2 * v) + Q(cst, 7)}, M, w, cst, cap), M, w) - out['O1'] = dict(statement='copy charge 63 per call, no helpers, every data register one rank-7 climb, idle at cap R', - verdicts={str(R): v_ for R, v_ in o1.items()}, helper_free_ceiling_cap45=dec(o1_lo), - helper_free_ceiling_bracket=[str(o1_lo), str(o1_hi)], - format_limits_bit_X_star='6.0005e-3 (research/format-limits section A, stronger axioms)') - # O2: centre path shared by two calls against the design-free helper floors of research/format-limits section D - floors = dict(strict=138, sink_only=212) - shared = [r for r in widths if r['copy_charge'] == str(Q(63, 2)) and r['idle_cap'] == cap] - need(next(r for r in shared if r['helper_width'] == 8)['max_helpers'] < floors['strict'], 'O2 shared centre leaves too few width-8 helpers') + o1_local = {7: Q(2 * v) + Q(cst, 7)} + o1 = {R: verdict(relaxed(o1_local, M, w, cst, R), M, w, TARGET) for R in (42, 45, 50, 53, 63)} + need(all(v_ == 'fail' for v_ in o1.values()), 'O1 copy charge 63 cannot reach 1/99 in the relaxation') + o1_roots = {R: root(relaxed(o1_local, M, w, cst, R), M, w) for R in (45, 53, 63)} + o1_rank8 = {R: dec(root(relaxed({7: Q(2 * v), 8: Q(cst, 8)}, M, w, cst, R), M, w)[0]) for R in (45, 63)} + out['O1'] = dict(statement='copy charge 63 per call (as nine rank-7 copies), no helpers, every data register one rank-7 climb, idle at cap R', + verdicts={str(R): v_ for R, v_ in o1.items()}, + helper_free_ceiling={str(R): dict(root=dec(lo), bracket=[str(lo), str(hi)]) for R, (lo, hi) in o1_roots.items()}, + copies_at_rank8_ceiling=o1_rank8, + format_limits_bit='X(9) = 4.6072e-3 at s = 9 and X* = 6.0005e-3 over all s (research/format-limits section A, its axioms)') + # O2: centre path shared by two calls, width-8 helpers, against the design-free floor for full-frame helpers + floors = dict(strict=138, sink_only=212, shipped_ladders=222) + o2 = {} + for R in (45, 50, 53): + k = max_count({7: Q(2 * v) + Q(cst, 14)}, 8, M, w, Q(cst, 2), R, TARGET, 600) + o2[str(R)] = dict(max_width8_helpers=k[0], next=k[2], below_strict_floor=k[0] < floors['strict']) + need(o2['45']['below_strict_floor'] and o2['50']['below_strict_floor'] and not o2['53']['below_strict_floor'], + 'O2 boundary: holds for halving depth <= 3, flips at depth 4') + k8 = max_count({7: Q(2 * v), 8: Q(cst, 16)}, 8, M, w, Q(cst, 2), 45, TARGET, 600) out['O2'] = dict(statement='copy charge 63/2 per call (centre path shared by two calls), every data register one rank-7 climb, ' - 'helpers one climb of rank = width, idle at the cap 45; floors from research/format-limits section D (argued premises)', - floors=floors, - max_helpers_by_width={str(r['helper_width']): r['max_helpers'] for r in shared}, - widths_meeting_strict_floor=[r['helper_width'] for r in shared if r['max_helpers'] is not None and r['max_helpers'] >= floors['strict']], - widths_meeting_sink_only_floor=[r['helper_width'] for r in shared if r['max_helpers'] is not None and r['max_helpers'] >= floors['sink_only']]) + 'full-frame (width-8) helpers as one rank-8 climb, idle at cap R; floors from research/format-limits ' + 'section D for full-frame helpers (argued premises)', + floors=floors, by_cap=o2, copies_at_rank8_cap45=k8[0], + holds_for='halving depth 2 (cap 45, the record) and depth 3 (cap 50); fails at depth 4 (cap 53)') # --- complex cross-check (#1240) and #1272's combined lever inside / beyond the window cw = {1: 2412, 2: 418, 3: 432, 4: 142, 5: 82, 8: 8} @@ -249,13 +283,16 @@ def lever(name, H_local, c, u=1, R=cap): clo, chi = root(relaxed(cw, 73, cxw, ccst, ccap), 73, cxw) need(Q('0.0016900541090') < chi and clo < Q('0.0016900541091'), 'X1 #1240 complex word ceiling reproduced') rows = [] - for name, H, c in (('complex word ceiling (#1240)', cw, ccst), - ('centre free', {r: n for r, n in cw.items() if r != 8}, 0), - ('centre free + rank-9 children (window h = 9)', {9: Q(cmass - ccst, 9)}, 0), - ('centre free + rank-16 children (beyond the window)', {16: Q(cmass - ccst, 16)}, 0)): - lo, hi = root(relaxed(H, 73, cxw, c, ccap), 73, cxw) + cases = (('complex word ceiling (#1240)', cw, ccst, 1), + ('centre free', {r: n for r, n in cw.items() if r != 8}, 0, 1), + ('centre free + rank-9 children (window h = 9)', {9: Q(cmass - ccst, 9)}, 0, 1), + ('centre free + rank-16 children (beyond the window)', {16: Q(cmass - ccst, 16)}, 0, 1), + ('centre free + two unpaid coordinates', {r: n for r, n in cw.items() if r != 8}, 0, 2), + ('two unpaid + rank-9 children (window h = 9)', {9: Q(cmass, 9)}, ccst, 2)) + for name, H, c, u_ in cases: + lo, hi = root(relaxed(H, 73, cxw, c, ccap, u_), 73, cxw) rows.append(dict(lever=name, root_lo=str(lo), root_hi=str(hi), root=dec(lo), multiplier=dec(lo / clo, 4), - at_1_over_99=verdict(relaxed(H, 73, cxw, c, ccap), 73, cxw, TARGET))) + at_1_over_99=verdict(relaxed(H, 73, cxw, c, ccap, u_), 73, cxw, TARGET))) out['complex_crosscheck'] = dict(m=73, w=str(cxw), copy_charge=ccst, idle_cap=ccap, rows=rows) text = json.dumps(dict(status='PASS_BIT_REVISION3_LEVERS', **out), indent=1, sort_keys=True) + '\n' From 5ad74a4a04d1c9264768c43762e130690918b043 Mon Sep 17 00:00:00 2001 From: Sagar Thakrar Date: Wed, 14 Oct 2026 04:47:16 +0530 Subject: [PATCH 3/3] Pin the row-bound sources read by the halving-depth binding --- research/bit-revision3-levers-seed03/SOURCES.json | 12 ++++++++++++ research/bit-revision3-levers-seed03/VERIFY.json | 2 ++ 2 files changed, 14 insertions(+) diff --git a/research/bit-revision3-levers-seed03/SOURCES.json b/research/bit-revision3-levers-seed03/SOURCES.json index 4b09371652..c4390a747b 100644 --- a/research/bit-revision3-levers-seed03/SOURCES.json +++ b/research/bit-revision3-levers-seed03/SOURCES.json @@ -20,6 +20,12 @@ "git_blob": "5fd676df060f3b450782fdf5ff5f6beb63a5eeb0", "sha256": "1122cb3a575f8c788345fc1bf4c108ac7c3250fb81a5988671f5eb04b3ab3045" }, + { + "path": "research/e8-bit-carrier-skeleton/code/hub/r740-hosted-eleven/code/row_bound.py", + "usage": "input", + "git_blob": "11d3c0d48e4ea5a02ac3b6689f3c7d36f2972eb8", + "sha256": "de4a9b9cd797e1a05da56f62cfe725c8728cea3a4aa031b7d1b0a68f869760d6" + }, { "path": "research/e8-bit-p111-tuned/tune/EXPECTED.json", "usage": "input", @@ -32,6 +38,12 @@ "git_blob": "85a4499bf9e4911a705d50567a2c2ef6cf23739a", "sha256": "e3e301e62bc2b41dbf1ceac0acf3d35824ebeab1848c5a2142d4577b109da52f" }, + { + "path": "research/e8-bit-p111-tuned/vendor/pr510/e8-r480-nine-stage/code/assemble9.py", + "usage": "input", + "git_blob": "238226c568742dd5723b03eabae564a2eaa2bda9", + "sha256": "4bf6768224a3fac81ccda26df24f3763f9a4fbc35ad62bef2888595cdae519fe" + }, { "path": "research/e8-bit-p111-tuned/vendor/pr510/e8-r480-nine-stage/vendor/e8-r715-eleven-stage-whole/code/global_k.py", "usage": "input", diff --git a/research/bit-revision3-levers-seed03/VERIFY.json b/research/bit-revision3-levers-seed03/VERIFY.json index 4fe0040030..bb1ed152ce 100644 --- a/research/bit-revision3-levers-seed03/VERIFY.json +++ b/research/bit-revision3-levers-seed03/VERIFY.json @@ -6,8 +6,10 @@ "inputs": [ "certificates/selected-result.json", "research/community-frontier1094-audit/ASSEMBLY.json", + "research/e8-bit-carrier-skeleton/code/hub/r740-hosted-eleven/code/row_bound.py", "research/e8-bit-p111-tuned/tune/EXPECTED.json", "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz", + "research/e8-bit-p111-tuned/vendor/pr510/e8-r480-nine-stage/code/assemble9.py", "research/e8-bit-p111-tuned/vendor/pr510/e8-r480-nine-stage/vendor/e8-r715-eleven-stage-whole/code/global_k.py" ], "commands": [