From f01a1bb3910cf27fd9ebacecaf90f503ca75e535 Mon Sep 17 00:00:00 2001 From: Aaron Wang Date: Fri, 16 Oct 2026 21:37:09 -0400 Subject: [PATCH] Register rank-shape fully charged block-climb gate screen - no new kappa Cost-alphabet hard-search reading of the drawn complex-rank-shape-decoder card, scope unchanged. Exact gate thresholds for zero-charge payload reblocking: 363 payloads and 10 rank-1 units of slack at block cap 16, 255 payloads and 14 units at cap 51; uniform restoration tax excluded under the PR1605 added-work contract; PR3066 seven-row moment replay as controls; greedy optimality certified by 600 strict merge inequalities. Package research/rank-shape-coframe-bill-seed850bc3/. Aaron Wang, with help from opencode. Apache-2.0. --- .gitattributes | 3 + .../README.md | 192 ++++++ .../RESULT.json | 532 +++++++++++++++++ .../SOURCES.json | 46 ++ .../TASK.json | 84 +++ .../VERIFY.json | 34 ++ .../sources/pr3066-RESULT.json | 142 +++++ .../verify.py | 554 ++++++++++++++++++ 8 files changed, 1587 insertions(+) create mode 100644 research/rank-shape-coframe-bill-seed850bc3/README.md create mode 100644 research/rank-shape-coframe-bill-seed850bc3/RESULT.json create mode 100644 research/rank-shape-coframe-bill-seed850bc3/SOURCES.json create mode 100644 research/rank-shape-coframe-bill-seed850bc3/TASK.json create mode 100644 research/rank-shape-coframe-bill-seed850bc3/VERIFY.json create mode 100644 research/rank-shape-coframe-bill-seed850bc3/sources/pr3066-RESULT.json create mode 100644 research/rank-shape-coframe-bill-seed850bc3/verify.py diff --git a/.gitattributes b/.gitattributes index 226044d4ce..0cf99250be 100644 --- a/.gitattributes +++ b/.gitattributes @@ -178,3 +178,6 @@ research/gmx-t74-grid24/** -text -whitespace research/global-mixed-x54-fusions-k531/** -text -whitespace research/global-mixed-x54-grid24/** -text -whitespace research/gauge44-ends7-t16/** -text -whitespace + +# Preserve the exact vendored PR3066 result bytes (frozen source pin). +research/rank-shape-coframe-bill-seed850bc3/sources/pr3066-RESULT.json -text diff --git a/research/rank-shape-coframe-bill-seed850bc3/README.md b/research/rank-shape-coframe-bill-seed850bc3/README.md new file mode 100644 index 0000000000..773631f0c3 --- /dev/null +++ b/research/rank-shape-coframe-bill-seed850bc3/README.md @@ -0,0 +1,192 @@ +# Fully charged block-climb gate screen over all payload reblockings + +**Scoped cost-alphabet result for the drawn `complex-rank-shape-decoder` card +(method 2). No physical decoder, word-level co-frame census, supplier admission +or new kappa; the selected record is unchanged.** +Agent: Aaron Wang, with help from opencode (substantial AI assistance; no model +named; no independent human review). Base commit +`d8e0f83f00191df62174b641e9fff055c357f641`, priority revision 6. + +The card asks whether a decoder can deliver the local paid mass in fewer, +larger-rank children, with copies, frames and restoration counted. After +[PR 3039](https://github.com/CrocSwap/integer-mult-bounds/pull/3039) excluded every charged +block-climb group and [PR 3066](https://github.com/CrocSwap/integer-mult-bounds/pull/3066) +showed free and charged groups can mix in a passing call, the open question is +quantitative: how much zero-charge structure does the card's +5% gate actually +require? This package answers that exactly, over **all** partitions of the +selected word's 2,412 rank-one payloads into block children, with the proved +minimum charges for copies (rank-k frame transports, PR 1429) and dirty-slot +restoration (one rank-1 save per block without owned temporaries, PR 3039). + +## Model and conventions + +The frozen PR 1240/PR 1429/PR 1605 cost alphabet: width 73, stock 896/9, +centre charge 64, old idle mass 1,646 at rank 51 (halving guard), baseline +profile `{1:2412, 2:418, 3:432, 4:142, 5:82, 8:8}`, paid mass 5,586. The +acceptance target is `a* = 21/20 * 1690054109089/10^15` (the card's +5% over +the selected packing ceiling). Two accounting conventions are reported: + +- **strict contract** (PR 1605's added-work contract, PR 3066's convention): + every added child is paid on top of the old idle bill, none receives idle + credit. This is the acceptance-relevant screen ("all copied information, + frames and restoration counted"). +- **coverage-law convention**: every added rank unit is refunded from old idle + mass (the `ceiling.py` model). Favourable to any construction. + +## What is established + +1. **Exact gate thresholds for zero-charge groups (strict contract).** A + reblocked profile passes the +5% moment gate at `a*` only if zero-charge + groups (both operand vectors already at the block frame, owned gather + slots) cover enough payloads: + + | Block cap | Minimum zero-charge coverage | Blocks | Full-coverage slack | Taxed blocks allowed at full coverage | + |---|---:|---:|---:|---:| + | 16 | 363 of 2,412 payloads | 23 | 10 rank-1 units | 10 of 151 (at least 141 zero-charge) | + | 51 | 255 of 2,412 payloads | 5 | 14 rank-1 units | 14 of 48 (at least 34 zero-charge) | + + Coverage/charged-work tradeoff (slack in rank-1 units at `a*`): cap 16 with + 363, 768, 2,412 covered payloads gives 0, 1, 10 units; cap 51 with 255, + 1,530, 2,412 gives 0, 8, 14 units. Under the coverage-law convention the + slack is 1,447 units (cap 16) and mass-law-capped 1,646 (cap 51). + +2. **The uniformly taxed family is excluded under the strict contract.** With + the PR 3039 restoration tax imposed on every block (no owned temporaries), + a taxed block of any size `k = 2..51` is strictly dearer than its `k` + payload singles at `a*` (50/50 exact enclosure inequalities). Blocking is + then counterproductive at every size, so the optimal uniformly taxed + realization is the unchanged selected word: moment + `1.000245413040243..1.000245413040244` at `a*` (fail). The taxed greedy-51 + profile is worse: its strict-contract moment is above one for **every** + `a >= 0`. This closes PR 3066's conditional sentence about a uniformly + taxed construction with exact numbers. Under the coverage-law convention + the same taxed profile would still clear the +5% ceiling gate (1.79x), so + the exclusion is a statement about the added-work contract, not about the + coverage law alone. + +3. **Charged copies are excluded too, and exceed the mass law.** One paid + rank-k transport per block is strictly dearer than the payload singles for + every `k = 2..51` at `a*` (50/50), and its rank mass is 7,998, above the + coverage law's 7,232 total, so the law rejects such profiles outright. + Every mixed transport/restoration variant screened fails the strict moment + (see `RESULT.json` `contracts`). + +4. **Exact predecessor convergence.** The 363-payload minimum coverage and the + 10-unit slack are PR 1605's independently derived rank-16 threshold and + call budget, now derived as optima of one exact gate arithmetic. PR 3066's + seven published mixed-profile moments are reproduced as controls; its five + charged pairs spend `0.001390065582957` of the `0.001395098052012` slack its + q=0 zero-charge row leaves (about 10.0 rank-1 units at the margin, matching + the budget computed here), and six pairs exceed it. + +5. **Ceiling screen (coverage law, the card's ceiling definition).** The greedy + reblocked shapes clear the +5% ceiling gate by a wide margin once their + groups are zero-charge: + + | Profile | Ceiling bracket | Ratio to selected ceiling | +5% gate | + |---|---|---:|---| + | Selected word (control) | 0.001690054109..0.0016900541091 | 1.000x | fail | + | Greedy cap-16 (150x16 + 12) | 0.002480124284..0.0024801242841 | 1.467x | pass | + | Greedy cap-51 (47x51 + 15) | 0.0030761867866..0.0030761867867 | 1.820x | pass | + | Greedy cap-51 + 48 saves | 0.0030266309503..0.0030266309504 | 1.790x | pass (relaxation) | + + The last row is the favourable coverage-law relaxation only: under the + strict contract the same profile has moment above one for every `a >= 0`. + An optimistic passing relaxation is not acceptance; the strict screens in + items 1-3 are the acceptance-relevant statements. + +6. **Certificates.** Greedy block-size optimality is exact, not heuristic: 600 + strict subadditivity inequalities (every legal merge strictly lowers cost), + 1,225 payload-monotonicity inequalities (`c(k)/k` strictly decreasing), 50 + tax-dominance and 50 transport-dominance inequalities at `a*`, and an + exhaustive small-instance check (all 918 other partitions of 24 payloads + under cap 8 are strictly dearer than greedy `[8,8,8]`). All signs are + strict enclosures from the retained PR 1240 engine, executed from + authenticated source bytes. + +## Route note (recorded obstruction) + +PR 3039's open question 1 (read the pinned t16 canonical word's per-child +operand frames and partition the payload into co-frame groups) was assessed +and killed for this session: the canonical word archives record operations and +a frame registry, but no per-child operand frame field, so deriving them needs +a separate frame-propagation pass over each child's operand spans; guessing +them would misstate the word. The thresholds above are the exact bar that pass +must clear. + +## Reproduce + +Python 3.12, standard library only, exact rational arithmetic throughout +(about 40 seconds): + +```sh +python3.12 -I -B research/rank-shape-coframe-bill-seed850bc3/verify.py +python3.12 -I -B research/rank-shape-coframe-bill-seed850bc3/verify.py --write +``` + +Expected final line: + +```text +PASS_RANK_SHAPE_COFRAME_BILL min_cover_cap16=363 slack_units_cap16=10 min_free_blocks_cap16=141 slack_units_cap51=14 min_cover_cap51=255 uniform_tax_excluded=1 no_new_kappa +``` + +`verify.py` is read-only without `--write`; it recomputes every number from the +pinned inputs and fails on receipt drift, source drift, any predecessor moment +mismatch or any undecided sign. + +## Scope and limits + +- Covered: the cost-alphabet model above, block caps 16 and 51, the PR 1429 + transport charge, the PR 3039 per-block restoration tax, both accounting + conventions, all payload partitions (greedy optimality certified). +- Not covered: word-level realizability (which of the actual 2,412 rank-one + children are co-frame with owned gather slots); physical decoder identities; + the rank-2/rank-3 step children; masked or overcomplete supports (which + would change an assumption of the eight-term all-pairs bound); any changed + coverage law, template, port count or centre path; native/hosting/precision + bills. No supplier admission and no kappa claim. +- Claims: a scoped lower bound on effective payload child rank for one fixed + support alphabet (with the proved minimum charges, blocking helps only at + zero charge), exact gate thresholds, and the strict-contract exclusion of + the uniformly taxed family. Not a lower bound on all decoders. + +## Credit + +- [PR 3039](https://github.com/CrocSwap/integer-mult-bounds/pull/3039) by Aaron Wang + (navinor, AI-assisted): the charged-group obstruction, the `k = 2` + identity classification and the restoration tax made into a lower bound. +- [PR 3066](https://github.com/CrocSwap/integer-mult-bounds/pull/3066) by Ross + Richardson (AI-assisted): the mixed-profile correction and its published + moments, replayed here as controls; its conditional uniformly-taxed sentence + is what items 2-3 close. +- [PR 1605](https://github.com/CrocSwap/integer-mult-bounds/pull/1605) by Arham Tahir + (AI-assisted): the integer block budgets, the exact target and the added-work + contract; its 363 threshold and 10-unit budget are re-derived in item 1. +- [PR 1240](https://github.com/CrocSwap/integer-mult-bounds/pull/1240) by Doug + Colkitt (AI-assisted): the cost model and the retained exact interval engine, + executed from authenticated source bytes. +- [PR 1429](https://github.com/CrocSwap/integer-mult-bounds/pull/1429) by Ali Romman + (AI-assisted): the transport-charge contract. +- [PR 679](https://github.com/CrocSwap/integer-mult-bounds/pull/679) by Greer Guthrie: + the native direct-sum/tensor-child obstruction, unchanged. + +Apache-2.0. + +## Open next questions + +- **How many of the selected word's actual 2,412 rank-one payloads are + zero-charge co-frame groups?** This decides the lever: item 1 shows at least + 363 (cap 16) or 255 (cap 51) payloads must be, with at most 10/14 taxed + blocks even at full coverage. First step: the per-child operand-frame data + pass over `t16/global/base/providers/gauge44` recorded in the route note. + Blocked by: that frame-propagation pass and the owned-slot (temporary + lifetime) analysis, neither of which exists in the archives. +- **Does a shared-call transport contract change the strict-contract + exclusion?** PR 1605 budgets ten rank-1 units per call for shared charged + work; item 3 excludes per-block charges but shared charges inside the slack + remain open. First step: declare one explicit sharing schedule and screen its + profile at `a*`. Blocked by: no such schedule is currently proposed. +- **Do the rank-2/rank-3 step children admit the same treatment?** The card + names "rank-1 to rank-3 steps"; this package covers the rank-one payload + only. First step: declare the joint replacement contract and its coverage + identity before any synthesis (PR 3039 open question 2). diff --git a/research/rank-shape-coframe-bill-seed850bc3/RESULT.json b/research/rank-shape-coframe-bill-seed850bc3/RESULT.json new file mode 100644 index 0000000000..948887d51e --- /dev/null +++ b/research/rank-shape-coframe-bill-seed850bc3/RESULT.json @@ -0,0 +1,532 @@ +{ + "baseline_profile": { + "1": 2412, + "2": 418, + "3": 432, + "4": 142, + "5": 82, + "8": 8 + }, + "budgets": { + "greedy16": { + "blocks": 151, + "max_taxed_blocks_strict_contract": 10, + "min_zero_charge_blocks_strict_contract": 141, + "slack_coverage_law_law_capped": false, + "slack_rank1_units_coverage_law": 1447, + "slack_rank1_units_strict_contract": 10, + "slack_strict_contract_law_capped": false + }, + "greedy51": { + "blocks": 48, + "max_taxed_blocks_strict_contract": 14, + "min_zero_charge_blocks_strict_contract": 34, + "slack_coverage_law_law_capped": true, + "slack_rank1_units_coverage_law": 1646, + "slack_rank1_units_strict_contract": 14, + "slack_strict_contract_law_capped": false + } + }, + "ceilings_coverage_law": [ + { + "ceiling": [ + "1690054109/1000000000000", + "16900541091/10000000000000" + ], + "gate_five_percent": "fail", + "profile": "baseline", + "ratio_to_selected_ceiling": [ + "1690054109000/1690054109089", + "1690054109100/1690054109089" + ] + }, + { + "ceiling": [ + "620031071/250000000000", + "24801242841/10000000000000" + ], + "gate_five_percent": "pass", + "profile": "greedy16", + "ratio_to_selected_ceiling": [ + "2480124284000/1690054109089", + "2480124284100/1690054109089" + ] + }, + { + "ceiling": [ + "15380933933/5000000000000", + "30761867867/10000000000000" + ], + "gate_five_percent": "pass", + "profile": "greedy51", + "ratio_to_selected_ceiling": [ + "3076186786600/1690054109089", + "3076186786700/1690054109089" + ] + }, + { + "ceiling": [ + "30266309503/10000000000000", + "236455543/78125000000" + ], + "gate_five_percent": "pass", + "profile": "greedy51_restoration_taxed", + "ratio_to_selected_ceiling": [ + "3026630950300/1690054109089", + "3026630950400/1690054109089" + ] + } + ], + "ceilings_strict_contract": [ + { + "ceiling": [ + "1690054109/1000000000000", + "16900541091/10000000000000" + ], + "profile": "baseline", + "ratio_to_selected_ceiling": [ + "1690054109000/1690054109089", + "1690054109100/1690054109089" + ] + }, + { + "ceiling": [ + "620031071/250000000000", + "24801242841/10000000000000" + ], + "profile": "greedy16", + "ratio_to_selected_ceiling": [ + "2480124284000/1690054109089", + "2480124284100/1690054109089" + ] + }, + { + "ceiling": [ + "15380933933/5000000000000", + "30761867867/10000000000000" + ], + "profile": "greedy51", + "ratio_to_selected_ceiling": [ + "3076186786600/1690054109089", + "3076186786700/1690054109089" + ] + }, + { + "ceiling": null, + "moment_at_zero": [ + "27605706480327968987711966169108933921936267063351259813722053803804357944807207/27558517238481254510809894432067722069078256350422454241390904993883324854304768", + "441691303685247503803391458705742942750980273013620157019552860860869727116961605/440936275815700072172958310913083553105252101606759267862254479902133197668876288" + ], + "profile": "greedy51_restoration_taxed", + "reason": "moment above one for every a >= 0 under the strict contract" + } + ], + "certificates": { + "merge_grid_checks": 600, + "payload_monotone_checks": 1225, + "tax_dominance_checks": 50, + "transport_dominance_checks": 50 + }, + "checks": [ + "pr3066_seven_rows_reproduced", + "merge_grid_strict", + "payload_monotone_strict", + "tax_dominance_strict", + "transport_dominance_strict", + "unchanged_baseline_fails", + "one_over_99_still_fails", + "contract_lattice_screened", + "uniform_restoration_tax_excluded", + "omitted_save_false_pass_control", + "over_law_transport_rejected", + "budget_boundaries_signed", + "min_coverage_computed", + "selected_ceiling_bracket_control", + "small_instance_greedy_strictly_minimal" + ], + "contracts": [ + { + "contract": "zero_charge", + "decision": "pass", + "moment": [ + "249651225486997/250000000000000", + "998604901947989/1000000000000000" + ], + "moment_exact": [ + "1761284505904993101156042797943406332005657811794966177895018610956680761121949195/1763745103262800288691833243652334212421008406427037071449017919608532790675505152", + "31451509034017733949215049963275113071529603782052967462411046624226442162895495/31495448272550005155211307922363110936089435829054233418732462850152371262062592" + ], + "profile": { + "12": 1, + "16": 150, + "2": 418, + "3": 432, + "4": 142, + "5": 82, + "8": 8 + }, + "rank_mass": 5586, + "shape": "greedy16" + }, + { + "contract": "restoration_tax_one_save_per_block", + "decision": "fail", + "moment": [ + "1019540971828723/1000000000000000", + "254885242957181/250000000000000" + ], + "moment_exact": [ + "1798210396638708215613500136841220911846367680254272605608927532743224240074742097/1763745103262800288691833243652334212421008406427037071449017919608532790675505152", + "1798210396638708215613500136841220911846367680254272605608927532743224240074963725/1763745103262800288691833243652334212421008406427037071449017919608532790675505152" + ], + "profile": { + "1": 151, + "12": 1, + "16": 150, + "2": 418, + "3": 432, + "4": 142, + "5": 82, + "8": 8 + }, + "rank_mass": 5737, + "shape": "greedy16" + }, + { + "contract": "one_paid_transport_per_block", + "decision": "fail", + "moment": [ + "1331386911069867/1000000000000000", + "332846727767467/250000000000000" + ], + "moment_exact": [ + "1174113572473831734255155901862878852923245676772882312920562426850571074869387033/881872551631400144345916621826167106210504203213518535724508959804266395337752576", + "1174113572473831734255155901862878852923245676772882312920562426850571074869497847/881872551631400144345916621826167106210504203213518535724508959804266395337752576" + ], + "profile": { + "12": 2, + "16": 300, + "2": 418, + "3": 432, + "4": 142, + "5": 82, + "8": 8 + }, + "rank_mass": 7998, + "shape": "greedy16" + }, + { + "contract": "transport_plus_restoration", + "decision": "fail", + "moment": [ + "676161490475301/500000000000000", + "1352322980950603/1000000000000000" + ], + "moment_exact": [ + "42592018494310331838710163261135219387271450392947697384911317419422957655206553/31495448272550005155211307922363110936089435829054233418732462850152371262062592", + "2385153035681378582967769142623572285687201222005071053555033775487685628691811699/1763745103262800288691833243652334212421008406427037071449017919608532790675505152" + ], + "profile": { + "1": 151, + "12": 2, + "16": 300, + "2": 418, + "3": 432, + "4": 142, + "5": 82, + "8": 8 + }, + "rank_mass": 8149, + "shape": "greedy16" + }, + { + "contract": "zero_charge", + "decision": "pass", + "moment": [ + "997924675428799/1000000000000000", + "623702922143/625000000000" + ], + "moment_exact": [ + "1760084759712664096308465545860964722092781368830992086477016181611477657031540031/1763745103262800288691833243652334212421008406427037071449017919608532790675505152", + "440021189928166024077116386465241180523195342207748021619254045402869414257932497/440936275815700072172958310913083553105252101606759267862254479902133197668876288" + ], + "profile": { + "15": 1, + "2": 418, + "3": 432, + "4": 142, + "5": 82, + "51": 47, + "8": 8 + }, + "rank_mass": 5586, + "shape": "greedy51" + }, + { + "contract": "restoration_tax_one_save_per_block", + "decision": "fail", + "moment": [ + "1004579849960423/1000000000000000", + "125572481245053/125000000000000" + ], + "moment_exact": [ + "1771822791204176185672425494649673992505722254169049758862894514364815981466864927/1763745103262800288691833243652334212421008406427037071449017919608532790675505152", + "442955697801044046418106373662418498126430563542262439715723628591203995366765557/440936275815700072172958310913083553105252101606759267862254479902133197668876288" + ], + "profile": { + "1": 48, + "15": 1, + "2": 418, + "3": 432, + "4": 142, + "5": 82, + "51": 47, + "8": 8 + }, + "rank_mass": 5634, + "shape": "greedy51" + }, + { + "contract": "one_paid_transport_per_block", + "decision": "fail", + "moment": [ + "1330026458031489/1000000000000000", + "133002645803149/100000000000000" + ], + "moment_exact": [ + "1172913826281502729407578649780437243010369233808908221502559997505367970778977869/881872551631400144345916621826167106210504203213518535724508959804266395337752576", + "167559118040214675629654092825776749001481319115558317357508571072195424397011445/125981793090200020620845231689452443744357743316216933674929851400609485048250368" + ], + "profile": { + "15": 2, + "2": 418, + "3": 432, + "4": 142, + "5": 82, + "51": 94, + "8": 8 + }, + "rank_mass": 7998, + "shape": "greedy51" + }, + { + "contract": "transport_plus_restoration", + "decision": "fail", + "moment": [ + "1336681632563113/1000000000000000", + "668340816281557/500000000000000" + ], + "moment_exact": [ + "1178782842027258774089558624174791878216839676477937057695499163882037132996640317/881872551631400144345916621826167106210504203213518535724508959804266395337752576", + "1178782842027258774089558624174791878216839676477937057695499163882037132996746235/881872551631400144345916621826167106210504203213518535724508959804266395337752576" + ], + "profile": { + "1": 48, + "15": 2, + "2": 418, + "3": 432, + "4": 142, + "5": 82, + "51": 94, + "8": 8 + }, + "rank_mass": 8046, + "shape": "greedy51" + } + ], + "coverage_law_total_mass": "7232", + "idle_mass": 1646, + "idle_rank": 51, + "min_zero_charge_coverage": { + "cap16": { + "blocks_coverage_law": 23, + "blocks_strict_contract": 23, + "min_payloads_covered_coverage_law": 363, + "min_payloads_covered_strict_contract": 363 + }, + "cap51": { + "blocks_coverage_law": 5, + "blocks_strict_contract": 5, + "min_payloads_covered_coverage_law": 255, + "min_payloads_covered_strict_contract": 255 + } + }, + "payload_units": 2412, + "predecessor_rows": [ + { + "charged_pairs": 0, + "decision": "pass", + "moment": [ + "249651225486997/250000000000000", + "998604901947989/1000000000000000" + ], + "moment_exact": [ + "1761284505904993101156042797943406332005657811794966177895018610956680761121949195/1763745103262800288691833243652334212421008406427037071449017919608532790675505152", + "31451509034017733949215049963275113071529603782052967462411046624226442162895495/31495448272550005155211307922363110936089435829054233418732462850152371262062592" + ] + }, + { + "charged_pairs": 1, + "decision": "pass", + "moment": [ + "998883185907233/1000000000000000", + "499441592953617/500000000000000" + ], + "moment_exact": [ + "110110957992214271771182884175600925526893293033661757323821945909516098707966811/110234068953925018043239577728270888276313025401689816965563619975533299417219072", + "1761775327875428348338926146809614808430292688538588117181151134552257579327667807/1763745103262800288691833243652334212421008406427037071449017919608532790675505152" + ] + }, + { + "charged_pairs": 2, + "decision": "pass", + "moment": [ + "499580685680233/500000000000000", + "999161371360467/1000000000000000" + ], + "moment_exact": [ + "1762265976106366494413117906060491600883565073467946746079649916378211694471008971/1763745103262800288691833243652334212421008406427037071449017919608532790675505152", + "440566494026591623603279476515122900220891268366986686519912479094552923617802027/440936275815700072172958310913083553105252101606759267862254479902133197668876288" + ] + }, + { + "charged_pairs": 3, + "decision": "pass", + "moment": [ + "31232482286021/31250000000000", + "999439433152673/1000000000000000" + ], + "moment_exact": [ + "1762756406230775652193390025924352747177434465527493478090156603840404381180467563/1763745103262800288691833243652334212421008406427037071449017919608532790675505152", + "881378203115387826096695012962176373588717232763746739045078301920202190590333503/881872551631400144345916621826167106210504203213518535724508959804266395337752576" + ] + }, + { + "charged_pairs": 4, + "decision": "pass", + "moment": [ + "499858664277061/500000000000000", + "999717328554123/1000000000000000" + ], + "moment_exact": [ + "1763246542884301185751189087190913468636426938008994032681981132269339858225312741/1763745103262800288691833243652334212421008406427037071449017919608532790675505152", + "881623271442150592875594543595456734318213469004497016340990566134669929112756245/881872551631400144345916621826167106210504203213518535724508959804266395337752576" + ] + }, + { + "charged_pairs": 5, + "decision": "pass", + "moment": [ + "15624921367671/15625000000000", + "199998993506189/200000000000000" + ], + "moment_exact": [ + "881868113635073488230837641882393939414293422830871851080288045492088940645779421/881872551631400144345916621826167106210504203213518535724508959804266395337752576", + "1763736227270146976461675283764787878828586845661743702160576090984177881291758897/1763745103262800288691833243652334212421008406427037071449017919608532790675505152" + ] + }, + { + "charged_pairs": 6, + "decision": "fail", + "moment": [ + "500135962796849/500000000000000", + "1000271925593699/1000000000000000" + ], + "moment_exact": [ + "441056177674284340594655414932448821013092045223941935705692282706692603764199895/440936275815700072172958310913083553105252101606759267862254479902133197668876288", + "63008025382040620084950773561778403001870292174848847957956040386670371966321421/62990896545100010310422615844726221872178871658108466837464925700304742524125184" + ] + } + ], + "scope": "cost-alphabet implication audit for complex-rank-shape-decoder method 2; no physical decoder, word-level co-frame census, supplier admission or new kappa", + "shapes": { + "greedy16": { + "blocks": 151, + "cap": 16, + "profile": { + "12": 1, + "16": 150, + "2": 418, + "3": 432, + "4": 142, + "5": 82, + "8": 8 + } + }, + "greedy51": { + "blocks": 48, + "cap": 51, + "profile": { + "15": 1, + "2": 418, + "3": 432, + "4": 142, + "5": 82, + "51": 47, + "8": 8 + } + } + }, + "small_instance_other_partitions": 918, + "stock": "896/9", + "target": "35491136290869/20000000000000000", + "tradeoff": [ + { + "cap": 16, + "covered_payloads": 363, + "slack_rank1_units_strict_contract": 0, + "slack_strict_contract_law_capped": false + }, + { + "cap": 16, + "covered_payloads": 768, + "slack_rank1_units_strict_contract": 1, + "slack_strict_contract_law_capped": false + }, + { + "cap": 16, + "covered_payloads": 2412, + "slack_rank1_units_strict_contract": 10, + "slack_strict_contract_law_capped": false + }, + { + "cap": 51, + "covered_payloads": 255, + "slack_rank1_units_strict_contract": 0, + "slack_strict_contract_law_capped": false + }, + { + "cap": 51, + "covered_payloads": 1530, + "slack_rank1_units_strict_contract": 8, + "slack_strict_contract_law_capped": false + }, + { + "cap": 51, + "covered_payloads": 2412, + "slack_rank1_units_strict_contract": 14, + "slack_strict_contract_law_capped": false + } + ], + "uniform_restoration_tax": { + "decision": "fail", + "moment": [ + "500122706520121/500000000000000", + "1000245413040243/1000000000000000" + ], + "moment_exact": [ + "441044487327701306085190304698423949103775939570391441834824647266867543845050087/440936275815700072172958310913083553105252101606759267862254479902133197668876288", + "882088974655402612170380609396847898207551879140782883669649294533735087690372403/881872551631400144345916621826167106210504203213518535724508959804266395337752576" + ], + "optimal_profile": { + "1": 2412, + "2": 418, + "3": 432, + "4": 142, + "5": 82, + "8": 8 + }, + "reason": "for every 2<=k<=51 at a*, k rank-one singles are strictly cheaper than one rank-k block plus one rank-one save (tax_dominance certificate); blocking without owned gather slots is counterproductive at every block size" + }, + "width": 73 +} diff --git a/research/rank-shape-coframe-bill-seed850bc3/SOURCES.json b/research/rank-shape-coframe-bill-seed850bc3/SOURCES.json new file mode 100644 index 0000000000..eda62d3412 --- /dev/null +++ b/research/rank-shape-coframe-bill-seed850bc3/SOURCES.json @@ -0,0 +1,46 @@ +{ + "schema_version": 1, + "base_commit": "d8e0f83f00191df62174b641e9fff055c357f641", + "files": [ + { + "path": "research/complex-local-word-ceiling/ceiling.py", + "usage": "input", + "git_blob": "6c0f54527d879396f689523bfde19928a9b6157c", + "sha256": "86a1432870b3b21d8454106ec9162fddc0471472d9214c590a1420f2426cedfc" + }, + { + "path": "research/complex-rank-one-block-budget/README.md", + "usage": "input", + "git_blob": "b6986916ea0557bbb9540427dced85625d7ecbb7", + "sha256": "0abb8872bc413ab875634c7d6922e4cf4f7343ed125d2d1ce089ae47dad983d7" + }, + { + "path": "research/complex-rank-one-block-budget/RESULT.json", + "usage": "input", + "git_blob": "7bff1e841d729679d4ce44df8103fab9430e2539", + "sha256": "fb7d1baaccc236a8e4eb1417dea76aefb1a423cf9c7677fbfa774b0673e333b6" + }, + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5", + "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0" + } + ], + "frozen_sources": [ + { + "head": "8aa53674536727123436d3f76adb8f5dac6ddea1", + "original_path": "research/mixed-block-climb-overhead/RESULT.json", + "git_blob": "b8de790cb591f883f9446944058b949553de20ce", + "sha256": "2b464c650e114d75238109ff082ef3abba4485a0ea1c7d4229293c4291044247", + "local_path": "sources/pr3066-RESULT.json", + "url": "https://github.com/CrocSwap/integer-mult-bounds/blob/8aa53674536727123436d3f76adb8f5dac6ddea1/research/mixed-block-climb-overhead/RESULT.json" + } + ] +} diff --git a/research/rank-shape-coframe-bill-seed850bc3/TASK.json b/research/rank-shape-coframe-bill-seed850bc3/TASK.json new file mode 100644 index 0000000000..d6d7035727 --- /dev/null +++ b/research/rank-shape-coframe-bill-seed850bc3/TASK.json @@ -0,0 +1,84 @@ +{ + "schema_version": 1, + "task_id": "complex-rank-shape-decoder", + "priority_revision": 6, + "base_commit": "d8e0f83f00191df62174b641e9fff055c357f641", + "original_card": { + "id": "complex-rank-shape-decoder", + "question": "Can a decoder deliver the local paid mass in fewer, larger-rank children (block frame climbs instead of rank-1 to rank-3 steps)?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/complex-local-word-ceiling/README.md", + "research/complex-decoder-field-extension-seed44/README.md", + "research/complex-frame-pair-decoders/README.md", + "research/selected-k8-unrestricted-ends/README.md", + "research/eisenstein-reduction-copy-floor/README.md" + ], + "methods": [ + "Find one exact small decoding identity whose frame path climbs in blocks, and price its complete per-call profile.", + "Bound the best effective child rank achievable for one fixed support alphabet, including copies, frames and restoration." + ], + "acceptance_gate": "A per-call local profile, with all copied information, frames and restoration counted, whose ceiling exceeds the selected word's by at least 5%; masked or overcomplete supports must change an assumption of the eight-term all-pairs bound. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "research/complex-local-word-ceiling/verify.py" + ], + "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING", + "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.", + "scope": "Positive control and planning budget only; this is not a new construction or full cold replay." + }, + "first_experiment": "Before any synthesis, write the candidate per-call local profile (and centre charge / unpaid coordinates if changed) and screen it with ceiling.ceiling(); reject it if even the ideal ceiling does not beat the selected word's by your stated margin. Ideal budget: rank-16 delivery is 2.31x (levers.py).", + "bottleneck_link": "Rank-1 children are about half of recursive cost; the selected word's effective child rank is about 3.9. Larger-rank delivery lowers recursive cost per unit of paid mass.", + "allowed_variations": [ + "One masked, overcomplete or block decoder family with exact labels and supports.", + "A scoped lower bound on effective rank for one alphabet.", + "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope." + ], + "scope_change_triggers": [ + "Repacking idle remainders of an unchanged word (covered by the packing ceiling).", + "Repeating the eight-term all-pairs search inside its proved scope.", + "Only changing helper terminal subspaces and monotone frames within the fixed scalar word, entrances and cleanup contract already covered by #1995/#2013.", + "Searching below C=40 in the #2017 Eisenstein binary scalar-rectangle or fixed-support block-linear additive pairing model; specify a changed premise instead. This bound does not cover every complex decoder.", + "Continuing a partial cost improvement while leaving the same unpriced consumer, restoration or central-readout obligation unresolved; refresh the family expansion decision first. Local product-retiming evidence has a narrow scope and is not a ban on changed graphs or contracts." + ], + "overlap_terms": [ + "rank shape", + "block climb", + "masked decoder", + "overcomplete", + "effective rank" + ] + }, + "scope_status": "unchanged", + "actual_scope": "Can a decoder deliver the local paid mass in fewer, larger-rank children (block frame climbs instead of rank-1 to rank-3 steps)?", + "scope_change_reason": null, + "bottleneck_link": "Rank-1 children are about half of the per-call recursive cost, so larger-rank payload delivery is the lever named by the card's bottleneck. This package prices the lever's exact gate condition: block-climb reblocking lowers the strict-contract moment only at zero charge (co-frame operands, owned gather slots), and the exact minimum zero-charge coverage and taxed-block slack turn the remaining word-level question into a quantitative bar.", + "budget_minutes": 60, + "stop_rule": "Stop after one complete contract-lattice screen at the acceptance target with exact adjacent signs, the four dominance certificates and the small-instance exhaustive check; kill with the exact obstruction if any sign is undecided. No decoder synthesis, no word census, no new construction round.", + "outcome": "completed", + "evidence": "RESULT.json: PR3066's seven published moments reproduced; greedy optimality certified by 600 strict merge inequalities and 1225 payload-monotonicity inequalities; 50/50 tax-dominance and 50/50 transport-dominance inequalities at a*; uniform restoration tax excluded (optimal taxed realization is the unchanged selected word, moment 1.000245413040243..); exact thresholds 363 payloads/10 rank-1 units at cap 16 and 255 payloads/14 units at cap 51; coverage-law ceilings 1.467x (cap 16) and 1.820x (cap 51) over the selected ceiling for the zero-charge shapes; omitted-save false-pass and over-law-mass rejection controls; 918-partition small-instance check.", + "author": "Aaron Wang, with help from opencode", + "ai_assistance": "Substantial AI assistance via opencode; no model named; no independent human or formal-kernel proof review claimed. Retained engine and all predecessor numbers are executed from authenticated source bytes.", + "open_questions": [ + { + "question": "How many of the selected word's actual 2,412 rank-one payloads are zero-charge co-frame groups with owned gather slots?", + "why_it_matters": "It decides the whole lever: at least 363 payloads (cap 16) or 255 (cap 51) must be zero-charge for the +5% gate, with at most 10/14 taxed blocks even at full coverage.", + "first_step": "The per-child operand-frame data pass over the pinned t16 word archives named in the README route note, then partition payload pairs into co-frame groups and price exactly those.", + "blocked_by": "The archives record operations and a frame registry but no per-child operand frames; deriving them needs a separate frame-propagation and temporary-lifetime pass." + }, + { + "question": "Does an explicit shared-call transport schedule beat the strict-contract per-block exclusion inside the ten rank-1-unit call budget?", + "why_it_matters": "Item 3 excludes per-block charged copies, but shared charged work inside the slack is exactly what PR1605's budget allows.", + "first_step": "Declare one sharing schedule and screen its complete profile at a* with ceiling.ceiling().", + "blocked_by": "No such schedule is currently proposed." + }, + { + "question": "What complete profile results if a block climb also replaces the rank-2/rank-3 frame-step children?", + "why_it_matters": "Those steps are the 'rank-1 to rank-3 steps' the card names; rank-one-only reblocking cannot reach a = 1/99.", + "first_step": "Declare the joint replacement contract and its coverage identity before any synthesis (PR3039 open question 2).", + "blocked_by": "The coverage identity fixes paid mass at 72w + 64 per call, so moving step mass needs a proved replacement identity." + } + ] +} diff --git a/research/rank-shape-coframe-bill-seed850bc3/VERIFY.json b/research/rank-shape-coframe-bill-seed850bc3/VERIFY.json new file mode 100644 index 0000000000..b5c9f7c0c3 --- /dev/null +++ b/research/rank-shape-coframe-bill-seed850bc3/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/complex-local-word-ceiling/ceiling.py", + "research/complex-rank-one-block-budget/README.md", + "research/complex-rank-one-block-budget/RESULT.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "PR3066 seven-row moment replay, 600 merge and 1225 payload-monotonicity certificates, 50/50 tax and transport dominance inequalities, uniform-taxed exclusion, exact threshold and budget boundaries, omitted-save and over-law-mass controls, coverage-law and strict ceilings, 918-partition small-instance check, receipt drift." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py", + "--write" + ], + "timeout_seconds": 300, + "checks": "Regenerates RESULT.json from the pinned inputs with newline LF and sorted keys (byte-stable receipt)." + } + ] +} diff --git a/research/rank-shape-coframe-bill-seed850bc3/sources/pr3066-RESULT.json b/research/rank-shape-coframe-bill-seed850bc3/sources/pr3066-RESULT.json new file mode 100644 index 0000000000..b8de790cb5 --- /dev/null +++ b/research/rank-shape-coframe-bill-seed850bc3/sources/pr3066-RESULT.json @@ -0,0 +1,142 @@ +{ + "scope": "cost-alphabet only; no physical decoder or new kappa", + "target": "35491136290869/20000000000000000", + "stock": "896/9", + "width": 73, + "idle_mass": 1646, + "idle_rank": 51, + "rows": [ + { + "charged_pairs": 0, + "profile": { + "2": 418, + "3": 432, + "4": 142, + "5": 82, + "8": 8, + "12": 1, + "16": 150 + }, + "rank_mass": 5586, + "moment": [ + "249651225486997/250000000000000", + "998604901947989/1000000000000000" + ], + "decision": "pass" + }, + { + "charged_pairs": 1, + "profile": { + "2": 420, + "3": 432, + "4": 142, + "5": 82, + "8": 8, + "10": 1, + "16": 150 + }, + "rank_mass": 5588, + "moment": [ + "998883185907233/1000000000000000", + "499441592953617/500000000000000" + ], + "decision": "pass" + }, + { + "charged_pairs": 2, + "profile": { + "2": 422, + "3": 432, + "4": 142, + "5": 82, + "8": 9, + "16": 150 + }, + "rank_mass": 5590, + "moment": [ + "499580685680233/500000000000000", + "999161371360467/1000000000000000" + ], + "decision": "pass" + }, + { + "charged_pairs": 3, + "profile": { + "2": 424, + "3": 432, + "4": 142, + "5": 82, + "6": 1, + "8": 8, + "16": 150 + }, + "rank_mass": 5592, + "moment": [ + "31232482286021/31250000000000", + "999439433152673/1000000000000000" + ], + "decision": "pass" + }, + { + "charged_pairs": 4, + "profile": { + "2": 426, + "3": 432, + "4": 143, + "5": 82, + "8": 8, + "16": 150 + }, + "rank_mass": 5594, + "moment": [ + "499858664277061/500000000000000", + "999717328554123/1000000000000000" + ], + "decision": "pass" + }, + { + "charged_pairs": 5, + "profile": { + "2": 429, + "3": 432, + "4": 142, + "5": 82, + "8": 8, + "16": 150 + }, + "rank_mass": 5596, + "moment": [ + "15624921367671/15625000000000", + "199998993506189/200000000000000" + ], + "decision": "pass" + }, + { + "charged_pairs": 6, + "profile": { + "2": 430, + "3": 432, + "4": 142, + "5": 82, + "8": 8, + "16": 150 + }, + "rank_mass": 5598, + "moment": [ + "500135962796849/500000000000000", + "1000271925593699/1000000000000000" + ], + "decision": "fail" + } + ], + "maximum_charged_pairs_in_this_family": 5, + "checks": [ + "all_seven_complete_profiles", + "mass_includes_transport", + "charged_pair_individually_loses", + "unchanged_baseline_fails", + "omitted_transport_false_pass", + "idle_refund_false_pass", + "one_over_99_still_fails" + ] +} diff --git a/research/rank-shape-coframe-bill-seed850bc3/verify.py b/research/rank-shape-coframe-bill-seed850bc3/verify.py new file mode 100644 index 0000000000..0c96e71fd4 --- /dev/null +++ b/research/rank-shape-coframe-bill-seed850bc3/verify.py @@ -0,0 +1,554 @@ +#!/usr/bin/env python3 +"""Fully charged block-climb gate screen over all rank-one payload reblockings. + +Aaron Wang, with help from opencode (substantial AI assistance). Apache-2.0. +The interval engine is Douglas Colkitt's retained PR1240 source, unchanged. + +Scope: cost-alphabet implication audit for the drawn `complex-rank-shape-decoder` +card (method 2). In the frozen PR1240/PR1429/PR1605 cost alphabet (width 73, +stock 896/9, centre charge 64, old idle mass 1646 at rank 51) we price every +partition of the selected word's 2,412 rank-one payloads into block children of +rank at most the declared cap, with copies (rank-k frame transports), frames and +dirty-slot restoration charged at the PR1605/PR3039 proved minimum, and screen +the complete per-call profiles at the card's acceptance target +a* = 21/20 * 1690054109089/10^15. No physical decoder, word-level co-frame +census, supplier admission or new kappa is claimed. +""" +import argparse +from fractions import Fraction as Q +import hashlib +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +BASE = {1: 2412, 2: 418, 3: 432, 4: 142, 5: 82, 8: 8} +PAYLOAD = 2412 +TARGET = Q(21, 20) * Q(1690054109089, 10 ** 15) +PLANNING = Q(1, 99) +BASE_CEILING = Q(1690054109089, 10 ** 15) +WIDTH, STOCK, IDLE, CAP, TOTAL = 73, Q(896, 9), 1646, 51, Q(7232) +INPUTS = { + 'research/complex-local-word-ceiling/ceiling.py', + 'research/complex-rank-one-block-budget/README.md', + 'research/complex-rank-one-block-budget/RESULT.json', +} + + +def require(ok, why): + if not ok: + raise ValueError(why) + + +def load_engine(): + pins = json.loads((HERE / 'SOURCES.json').read_text(encoding='utf-8')) + live = [v for v in pins['files'] if v['usage'] == 'input'] + require(len(live) == len(INPUTS) and {v['path'] for v in live} == INPUTS, + 'incomplete source inventory') + authenticated = {} + for v in live: + data = (ROOT / v['path']).read_bytes() + require(hashlib.sha256(data).hexdigest() == v['sha256'], + 'source drift: ' + v['path']) + authenticated[v['path']] = data + prior = json.loads(authenticated['research/complex-rank-one-block-budget/RESULT.json']) + require(prior['local_profile'] == {str(r): n for r, n in BASE.items()} and + Q(prior['target']) == TARGET and prior['idle_mass'] == IDLE and + prior['rank16_complete_max_extra_integer_rank_mass'] == 10, + 'predecessor model binding') + frozen = pins['frozen_sources'][0] + data = (HERE / frozen['local_path']).read_bytes() + require(hashlib.sha256(data).hexdigest() == frozen['sha256'], 'PR3066 source drift') + # Execute precisely the authenticated source bytes, without consulting pyc. + path = ROOT / 'research/complex-local-word-ceiling/ceiling.py' + namespace = {'__name__': 'retained_ceiling', '__file__': str(path)} + exec(compile(authenticated['research/complex-local-word-ceiling/ceiling.py'], + str(path), 'exec'), namespace) + return namespace + + +def iv_add(*terms): + lo = sum((t[0] for t in terms), Q(0)) + hi = sum((t[1] for t in terms), Q(0)) + return lo, hi + + +def iv_scale(term, count): + require(count >= 0, 'nonnegative count') + return count * term[0], count * term[1] + + +def moment_strict(hist, cost, a, idle=IDLE): + """PR1605 strict contract: added work is paid on top of the old idle bill.""" + out = [Q(0), Q(0)] + for rank, count in list(hist.items()) + [(CAP, Q(idle, CAP))]: + require(type(rank) is int and 1 <= rank <= CAP and count >= 0, 'histogram domain') + lo, hi = cost(rank, WIDTH, a) + out[0] += count * lo + out[1] += count * hi + return out[0] / STOCK, out[1] / STOCK + + +def moment_law(hist, cost, a): + """Coverage-law convention: every added rank unit is refunded from old idle.""" + paid = sum(Q(r) * Q(n) for r, n in hist.items()) + idle = TOTAL - paid + require(idle >= 0, 'local word pays more mass than the coverage law allows') + return moment_strict(hist, cost, a, idle=Q(idle)) + + +def decision(bounds): + if bounds[1] < 1: + return 'pass' + if bounds[0] > 1: + return 'fail' + raise ValueError('interval does not decide strict moment sign') + + +def decimal_bounds(bounds, digits=15): + scale = 10 ** digits + lo = (bounds[0] * scale).__floor__() + hi = (bounds[1] * scale).__ceil__() + return [str(Q(lo, scale)), str(Q(hi, scale))] + + +def exact_bounds(bounds): + return [str(bounds[0]), str(bounds[1])] + + +def pr3066_profile(charged_pairs): + hist = dict(BASE) + del hist[1] + hist[16] = hist.get(16, 0) + 150 + hist[2] = hist.get(2, 0) + 2 * charged_pairs + remainder = 12 - 2 * charged_pairs + if remainder: + hist[remainder] = hist.get(remainder, 0) + 1 + return dict(sorted(hist.items())) + + +def greedy_blocks(payload, cap): + blocks = [] + left = payload + while left > 0: + take = min(cap, left) + blocks.append(take) + left -= take + return blocks + + +def reblocked(cap, payload=PAYLOAD, saves=0, transports=0): + """BASE with `payload` rank-one children replaced by greedy blocks. + + saves and transports are charged at rank 1 and at the block rank (PR1429), + one per block unless count overridden by per-block arrays (int here).""" + blocks = greedy_blocks(payload, cap) + hist = dict(BASE) + hist[1] = hist.get(1, 0) - payload + saves + for k in blocks: + hist[k] = hist.get(k, 0) + 1 + if transports: + hist[k] = hist.get(k, 0) + transports + if hist[1] == 0: + del hist[1] + require(all(n >= 0 for n in hist.values()), 'negative count') + return dict(sorted(hist.items())) + + +def with_rank1(hist, units): + out = dict(hist) + out[1] = out.get(1, 0) + units + return dict(sorted(out.items())) + + +def strict_ceiling(hist, cost, grid=Q(1, 10 ** 13)): + lo, hi = Q(0), Q(1, 20) + require(decision(moment_strict(hist, cost, hi)) == 'fail', 'search window too small') + require(decision(moment_strict(hist, cost, lo)) == 'pass', 'no positive saving') + while hi - lo > grid: + mid = Q(int((lo + hi) / 2 / grid)) * grid + if mid <= lo: + mid = lo + grid + v = moment_strict(hist, cost, mid) + if v[1] < 1: + lo = mid + elif v[0] > 1: + hi = mid + else: + raise ValueError('enclosure too wide to separate the grid point') + return lo, hi + + +def law_ceiling(engine, hist, grid=Q(1, 10 ** 13)): + return engine['ceiling'](hist, WIDTH, 896, 9, 64, grid=grid) + + +def max_units(hist, cost, a, convention): + """Largest number of added rank-one units still passing at a (strict sign). + + Returns (units, law_capped): law_capped says the coverage law, not the + moment, stopped the budget search.""" + def dec(units): + h = with_rank1(hist, units) + try: + return decision(convention(h, cost, a)) + except ValueError as exc: + if 'coverage law' in str(exc): + return 'law_exhausted' + raise + units = 0 + while dec(units) == 'pass': + units += 1 + require(units <= 4000, 'budget search runaway') + return units - 1, dec(units) == 'law_exhausted' + + +def min_coverage(cap, cost, a, convention): + """Least payload coverage by zero-charge blocks whose profile passes at a.""" + for blocks in range(1, PAYLOAD // 2 + 2): + payload = min(blocks * cap, PAYLOAD) + hist = reblocked(cap, payload=payload) + if decision(convention(hist, cost, a)) == 'pass': + lo_b, hi_b = (blocks - 1) * cap + 1, payload + best = payload + while lo_b <= hi_b: + mid = (lo_b + hi_b) // 2 + if decision(convention(reblocked(cap, payload=mid), cost, a)) == 'pass': + best = mid + hi_b = mid - 1 + else: + lo_b = mid + 1 + return best, len(greedy_blocks(best, cap)) + raise ValueError('no passing coverage found') + + +def enumerate_partitions(total, cap): + out = [] + + def rec(left, ceiling, acc): + if left == 0: + out.append(list(acc)) + return + for k in range(min(ceiling, left), 0, -1): + acc.append(k) + rec(left - k, k, acc) + acc.pop() + + rec(total, cap, []) + return out + + +def small_instance_check(cost, a): + """Independent exhaustive check: greedy is strictly minimal at payloads=24, cap=8.""" + total, cap = 24, 8 + greedy = greedy_blocks(total, cap) + g_cost = iv_add(*[iv_scale(cost(k, WIDTH, a), 1) for k in greedy]) + others = 0 + for part in enumerate_partitions(total, cap): + if part == greedy: + continue + p_cost = iv_add(*[iv_scale(cost(k, WIDTH, a), 1) for k in part]) + require(g_cost[1] < p_cost[0], 'greedy not strictly minimal on small instance') + others += 1 + return others + + +def merge_certificate(cost, a, cap): + """Strict subadditivity on the full merge grid: merging two blocks strictly helps.""" + checks = 0 + for p in range(2, cap + 1): + for q in range(p, cap + 1): + if p + q > cap: + continue + left = iv_add(cost(p, WIDTH, a), cost(q, WIDTH, a)) + right = cost(p + q, WIDTH, a) + require(left[0] > right[1], 'merge certificate failed at %d+%d' % (p, q)) + checks += 1 + return checks + + +def monotone_certificate(cost, a, cap): + """c(k)/k strictly decreasing: larger blocks deliver payloads cheapest.""" + checks = 0 + for p in range(2, cap): + for q in range(p + 1, cap + 1): + lp, hp = cost(p, WIDTH, a) + lq, hq = cost(q, WIDTH, a) + require(lp / p > hq / q, 'payload monotonicity failed at %d,%d' % (p, q)) + checks += 1 + return checks + + +def tax_dominance_certificate(cost, a, cap): + """A restoration-taxed block is dearer than its payload singles at this a.""" + c1 = cost(1, WIDTH, a) + checks = 0 + for k in range(2, cap + 1): + taxed = iv_add(cost(k, WIDTH, a), c1) + singles = iv_scale(c1, k) + require(singles[1] < taxed[0], 'tax dominance failed at k=%d' % k) + checks += 1 + return checks + + +def transport_dominance_certificate(cost, a, cap): + """One paid transport per block is dearer than the payload singles at this a.""" + checks = 0 + for k in range(2, cap + 1): + charged = iv_scale(cost(k, WIDTH, a), 2) + singles = iv_scale(cost(1, WIDTH, a), k) + require(singles[1] < charged[0], 'transport dominance failed at k=%d' % k) + checks += 1 + return checks + + +def result(engine): + cost = engine['child_cost'] + checks = [] + + # --- predecessor replay: PR3066's seven published rows, exactly --- + frozen = json.loads((HERE / json.loads((HERE / 'SOURCES.json').read_text( + encoding='utf-8'))['frozen_sources'][0]['local_path']).read_text(encoding='utf-8')) + rows = [] + for published in frozen['rows']: + q = published['charged_pairs'] + hist = pr3066_profile(q) + require({str(r): n for r, n in hist.items()} == published['profile'], + 'PR3066 profile drift at q=%d' % q) + require(sum(r * n for r, n in hist.items()) == 5586 + 2 * q, 'paid mass') + bounds = moment_strict(hist, cost, TARGET) + require(decimal_bounds(bounds) == published['moment'], + 'PR3066 moment drift at q=%d' % q) + require(decision(bounds) == published['decision'] == + ('pass' if q <= 5 else 'fail'), 'PR3066 decision drift at q=%d' % q) + rows.append({'charged_pairs': q, 'moment': decimal_bounds(bounds), + 'moment_exact': exact_bounds(bounds), + 'decision': decision(bounds)}) + checks.append('pr3066_seven_rows_reproduced') + + # --- certificates at the acceptance target --- + merges = merge_certificate(cost, TARGET, CAP) + mono = monotone_certificate(cost, TARGET, CAP) + tax = tax_dominance_certificate(cost, TARGET, CAP) + trans = transport_dominance_certificate(cost, TARGET, CAP) + checks += ['merge_grid_strict', 'payload_monotone_strict', + 'tax_dominance_strict', 'transport_dominance_strict'] + + # --- control: baseline and planning target --- + require(decision(moment_strict(BASE, cost, TARGET)) == 'fail', 'baseline control') + require(decision(moment_strict(BASE, cost, PLANNING)) == 'fail', 'planning control') + checks += ['unchanged_baseline_fails', 'one_over_99_still_fails'] + + # --- shapes --- + g16 = reblocked(16) + g51 = reblocked(51) + require(g16 == pr3066_profile(0), 'greedy cap-16 shape must be PR3066 q=0 row') + + # --- contract lattice, strict contract (added work paid on top) --- + contracts = [] + shapes = {'greedy16': (16, g16, 151), 'greedy51': (51, g51, 48)} + for name, (capk, hist, block_count) in shapes.items(): + free_bounds = moment_strict(hist, cost, TARGET) + contracts.append({'shape': name, 'contract': 'zero_charge', + 'profile': {str(r): n for r, n in hist.items()}, + 'rank_mass': sum(r * n for r, n in hist.items()), + 'moment': decimal_bounds(free_bounds), + 'moment_exact': exact_bounds(free_bounds), + 'decision': decision(free_bounds)}) + saved = with_rank1(hist, block_count) + taxed_bounds = moment_strict(saved, cost, TARGET) + contracts.append({'shape': name, 'contract': 'restoration_tax_one_save_per_block', + 'profile': {str(r): n for r, n in saved.items()}, + 'rank_mass': sum(r * n for r, n in saved.items()), + 'moment': decimal_bounds(taxed_bounds), + 'moment_exact': exact_bounds(taxed_bounds), + 'decision': decision(taxed_bounds)}) + over = dict(hist) + for k in greedy_blocks(PAYLOAD, capk): + over[k] = over.get(k, 0) + 1 + over = dict(sorted(over.items())) + over_bounds = moment_strict(over, cost, TARGET) + contracts.append({'shape': name, 'contract': 'one_paid_transport_per_block', + 'profile': {str(r): n for r, n in over.items()}, + 'rank_mass': sum(r * n for r, n in over.items()), + 'moment': decimal_bounds(over_bounds), + 'moment_exact': exact_bounds(over_bounds), + 'decision': decision(over_bounds)}) + both = with_rank1(over, block_count) + both_bounds = moment_strict(both, cost, TARGET) + contracts.append({'shape': name, 'contract': 'transport_plus_restoration', + 'profile': {str(r): n for r, n in both.items()}, + 'rank_mass': sum(r * n for r, n in both.items()), + 'moment': decimal_bounds(both_bounds), + 'moment_exact': exact_bounds(both_bounds), + 'decision': decision(both_bounds)}) + checks.append('contract_lattice_screened') + + # --- uniform-tax optimum: taxed blocks are counterproductive, so the best + # uniformly taxed realization is the unchanged selected word --- + uniform = {'optimal_profile': {str(r): n for r, n in BASE.items()}, + 'reason': ('for every 2<=k<=51 at a*, k rank-one singles are strictly ' + 'cheaper than one rank-k block plus one rank-one save ' + '(tax_dominance certificate); blocking without owned gather ' + 'slots is counterproductive at every block size'), + 'moment': decimal_bounds(moment_strict(BASE, cost, TARGET)), + 'moment_exact': exact_bounds(moment_strict(BASE, cost, TARGET)), + 'decision': decision(moment_strict(BASE, cost, TARGET))} + require(uniform['decision'] == 'fail', 'uniform tax must be excluded at a*') + checks.append('uniform_restoration_tax_excluded') + + # --- mutation control: dropping the saves from a taxed profile must flip it --- + g51_taxed = with_rank1(g51, 48) + require(decision(moment_strict(g51_taxed, cost, TARGET)) == 'fail', + 'taxed greedy-51 must fail') + require(decision(moment_strict(g51, cost, TARGET)) == 'pass', + 'omitted-save false pass must be observable') + checks.append('omitted_save_false_pass_control') + + # --- coverage-law rejection of over-law transport masses --- + over_law = reblocked(51, transports=1) + require(sum(r * n for r, n in over_law.items()) > TOTAL, 'transport mass accounting') + try: + moment_law(over_law, cost, TARGET) + except ValueError as exc: + require('coverage law' in str(exc), 'wrong rejection reason') + else: + raise ValueError('over-law transport profile not rejected') + checks.append('over_law_transport_rejected') + + # --- budgets: exact slack in added rank-one units at a* --- + budgets = {} + for name, (capk, hist, block_count) in shapes.items(): + strict_units, strict_capped = max_units(hist, cost, TARGET, moment_strict) + law_units, law_capped = max_units(hist, cost, TARGET, moment_law) + budgets[name] = { + 'blocks': block_count, + 'slack_rank1_units_strict_contract': strict_units, + 'slack_strict_contract_law_capped': strict_capped, + 'slack_rank1_units_coverage_law': law_units, + 'slack_coverage_law_law_capped': law_capped, + 'max_taxed_blocks_strict_contract': strict_units, + 'min_zero_charge_blocks_strict_contract': block_count - strict_units, + } + require(decision(moment_strict(with_rank1(hist, strict_units), cost, TARGET)) + == 'pass', 'budget boundary pass side') + require(decision(moment_strict(with_rank1(hist, strict_units + 1), cost, TARGET)) + == 'fail', 'budget boundary fail side') + checks.append('budget_boundaries_signed') + + # --- minimal zero-charge coverage of the payloads --- + coverage = {} + for capk in (16, 51): + payload_strict, blocks_strict = min_coverage(capk, cost, TARGET, moment_strict) + payload_law, blocks_law = min_coverage(capk, cost, TARGET, moment_law) + coverage['cap%d' % capk] = { + 'min_payloads_covered_strict_contract': payload_strict, + 'blocks_strict_contract': blocks_strict, + 'min_payloads_covered_coverage_law': payload_law, + 'blocks_coverage_law': blocks_law, + } + checks.append('min_coverage_computed') + + # --- coverage/charged-work tradeoff at the strict contract --- + tradeoff = [] + for capk, payload in ((16, coverage['cap16']['min_payloads_covered_strict_contract']), + (16, 768), (16, PAYLOAD), (51, coverage['cap51']['min_payloads_covered_strict_contract']), + (51, 1530), (51, PAYLOAD)): + hist = reblocked(capk, payload=payload) + units, capped = max_units(hist, cost, TARGET, moment_strict) + tradeoff.append({'cap': capk, 'covered_payloads': payload, + 'slack_rank1_units_strict_contract': units, + 'slack_strict_contract_law_capped': capped}) + + # --- ceilings (coverage law, the card's ceiling definition) --- + ceilings = [] + law_profiles = [('baseline', BASE), ('greedy16', g16), ('greedy51', g51), + ('greedy51_restoration_taxed', g51_taxed)] + for name, hist in law_profiles: + lo, hi = law_ceiling(engine, hist) + ratio_lo = lo / BASE_CEILING + ceilings.append({'profile': name, + 'ceiling': [str(lo), str(hi)], + 'ratio_to_selected_ceiling': [str(ratio_lo), str(hi / BASE_CEILING)], + 'gate_five_percent': 'pass' if lo >= Q(21, 20) * BASE_CEILING + else ('fail' if hi < Q(21, 20) * BASE_CEILING else 'undecided')}) + base_lo, base_hi = law_ceiling(engine, BASE) + require(base_lo <= BASE_CEILING <= base_hi, 'selected ceiling bracket control') + checks.append('selected_ceiling_bracket_control') + + # --- strict-convention ceilings --- + strict_ceilings = [] + for name, hist in [('baseline', BASE), ('greedy16', g16), ('greedy51', g51), + ('greedy51_restoration_taxed', g51_taxed)]: + at_zero = moment_strict(hist, cost, Q(0)) + if decision(at_zero) == 'fail': + strict_ceilings.append({ + 'profile': name, 'ceiling': None, + 'reason': 'moment above one for every a >= 0 under the strict contract', + 'moment_at_zero': exact_bounds(at_zero)}) + continue + lo, hi = strict_ceiling(hist, cost) + strict_ceilings.append({'profile': name, 'ceiling': [str(lo), str(hi)], + 'ratio_to_selected_ceiling': [str(lo / BASE_CEILING), + str(hi / BASE_CEILING)]}) + + # --- independent small-instance check --- + others = small_instance_check(cost, TARGET) + checks.append('small_instance_greedy_strictly_minimal') + + return { + 'scope': ('cost-alphabet implication audit for complex-rank-shape-decoder ' + 'method 2; no physical decoder, word-level co-frame census, ' + 'supplier admission or new kappa'), + 'target': str(TARGET), 'stock': str(STOCK), 'width': WIDTH, + 'idle_mass': IDLE, 'idle_rank': CAP, 'coverage_law_total_mass': str(TOTAL), + 'baseline_profile': {str(r): n for r, n in BASE.items()}, + 'payload_units': PAYLOAD, + 'predecessor_rows': rows, + 'certificates': {'merge_grid_checks': merges, 'payload_monotone_checks': mono, + 'tax_dominance_checks': tax, + 'transport_dominance_checks': trans}, + 'shapes': {name: {'cap': capk, + 'profile': {str(r): n for r, n in hist.items()}, + 'blocks': block_count} + for name, (capk, hist, block_count) in shapes.items()}, + 'contracts': contracts, + 'uniform_restoration_tax': uniform, + 'budgets': budgets, + 'min_zero_charge_coverage': coverage, + 'tradeoff': tradeoff, + 'ceilings_coverage_law': ceilings, + 'ceilings_strict_contract': strict_ceilings, + 'small_instance_other_partitions': others, + 'checks': checks, + } + + +def main(): + parser = argparse.ArgumentParser() + parser.add_argument('--write', action='store_true') + args = parser.parse_args() + engine = load_engine() + expected = result(engine) + if args.write: + with open(HERE / 'RESULT.json', 'w', encoding='utf-8', newline='\n') as fh: + fh.write(json.dumps(expected, indent=2, sort_keys=True) + '\n') + else: + actual = json.loads((HERE / 'RESULT.json').read_text(encoding='utf-8')) + require(json.dumps(actual, sort_keys=True) == json.dumps(expected, sort_keys=True), + 'result receipt drift') + b16 = expected['budgets']['greedy16'] + b51 = expected['budgets']['greedy51'] + c16 = expected['min_zero_charge_coverage']['cap16'] + print('PASS_RANK_SHAPE_COFRAME_BILL ' + 'min_cover_cap16=%d slack_units_cap16=%d min_free_blocks_cap16=%d ' + 'slack_units_cap51=%d min_cover_cap51=%d uniform_tax_excluded=1 no_new_kappa' + % (c16['min_payloads_covered_strict_contract'], + b16['slack_rank1_units_strict_contract'], + b16['min_zero_charge_blocks_strict_contract'], + b51['slack_rank1_units_strict_contract'], + expected['min_zero_charge_coverage']['cap51']['min_payloads_covered_strict_contract'])) + + +if __name__ == '__main__': + main()