From 74c353a2df322ffc0273d538450f6505b76c76e7 Mon Sep 17 00:00:00 2001 From: zxv Date: Wed, 28 Oct 2026 01:14:39 -0400 Subject: [PATCH] Bound one-cut helper delivery against the selected P104 invoice --- .../PREDECESSOR.json | 10 + research/dyadic-cut-delivery-budget/PROOF.md | 128 ++++++++++++ research/dyadic-cut-delivery-budget/README.md | 30 +++ .../dyadic-cut-delivery-budget/RESULT.json | 60 ++++++ .../dyadic-cut-delivery-budget/SOURCES.json | 42 ++++ research/dyadic-cut-delivery-budget/TASK.json | 129 ++++++++++++ .../dyadic-cut-delivery-budget/VERIFY.json | 35 ++++ .../predecessor/PR6064-README.md | 188 ++++++++++++++++++ research/dyadic-cut-delivery-budget/verify.py | 147 ++++++++++++++ 9 files changed, 769 insertions(+) create mode 100644 research/dyadic-cut-delivery-budget/PREDECESSOR.json create mode 100644 research/dyadic-cut-delivery-budget/PROOF.md create mode 100644 research/dyadic-cut-delivery-budget/README.md create mode 100644 research/dyadic-cut-delivery-budget/RESULT.json create mode 100644 research/dyadic-cut-delivery-budget/SOURCES.json create mode 100644 research/dyadic-cut-delivery-budget/TASK.json create mode 100644 research/dyadic-cut-delivery-budget/VERIFY.json create mode 100644 research/dyadic-cut-delivery-budget/predecessor/PR6064-README.md create mode 100644 research/dyadic-cut-delivery-budget/verify.py diff --git a/research/dyadic-cut-delivery-budget/PREDECESSOR.json b/research/dyadic-cut-delivery-budget/PREDECESSOR.json new file mode 100644 index 0000000000..19f778aa7f --- /dev/null +++ b/research/dyadic-cut-delivery-budget/PREDECESSOR.json @@ -0,0 +1,10 @@ +{ + "source_pr": "https://github.com/CrocSwap/integer-mult-bounds/pull/6064", + "head": "5fd1fdedddf32307db31416958a1f03a8a67aa16", + "path": "research/dyadic-cut-enlargement/README.md", + "retained_path": "predecessor/PR6064-README.md", + "sha256": "0cb8510368768ba3428d41ed5133e03a29901d065f1b0da9000c032e610a0ad5", + "author": "https://github.com/zxv", + "license": "Apache-2.0", + "usage": "Unmodified pending predecessor proof and statement; retained bytes, no foreign Git history required." +} diff --git a/research/dyadic-cut-delivery-budget/PROOF.md b/research/dyadic-cut-delivery-budget/PROOF.md new file mode 100644 index 0000000000..e7bdd0dd54 --- /dev/null +++ b/research/dyadic-cut-delivery-budget/PROOF.md @@ -0,0 +1,128 @@ +# A one-cut delivery price screen for the PR6064 opportunity + +This is a scoped invoice obstruction, not a universal bound on helper changes. +It uses the exact selected PR6030 bill and answers a particular application of +[PR6064](https://github.com/CrocSwap/integer-mult-bounds/pull/6064). + +## Contract + +Keep the existing complete targets and paid jobs. At one fixed cut per LOCAL, +add d eligible coordinates. Suppose the native realization satisfies PR6064's +fixed-prefix/full-module hypotheses and makes at most 2d **additional binary +helper splits** available per LOCAL. Each split replaces a rank-h helper by +independent rank-a and rank-(h-a) targets, with 1 <= a < h <= 9. Existing paid +jobs and all other target credits stay unchanged. Charge at least d new paid +jobs of positive integer rank in the **entire** assembly, not d per LOCAL. + +These conditions are explicit. In particular, a bound on a module's capacity +increase is not automatically a bound on every changed supplier's productive +targets. The old realized channels must be retained, one additional unit must +produce at most one binary split, and old unused or previously incompatible +channels must not be relabelled as a new capacity increase. A different prefix, +changed boundary, multi-cut reuse, additional carrier targets, or joint delivery +of several coordinates by one paid job requires a new bill. + +PR6064 proves that adjoining d coordinates increases the full dyadic pairing +capacity by at most 2d. Its proof and attaining matrix are retained verbatim in +predecessor/PR6064-README.md with the exact source head/hash in PREDECESSOR.json. +The implication above is the declared realization contract, not an admission +of that scalar example as a native P104 supplier. + +## Whole-interval price + +Write k for the proposed saving, p=1-k, and M(k) for the old complete raw +target moment minus the old complete paid moment. We examine the whole interval + + 781451/250000000 <= k <= 17/5000. + +The lower endpoint is selected kappa .003125804. The upper endpoint is the +unchanged admitted BIT saving .0034. The exact source contains 18 LOCALs and +no helper rank above 9. By concavity, + + a^p + (h-a)^p - h^p <= h^p (2^k - 1) + <= 9 (2^k - 1). + +Since log(2)<7/10 and exp(x)<=1/(1-x) for 0<=x<1, + + total extra target credit <= 2 d * 18 * 9 * (7k/10)/(1-7k/10) + <= d * 12852/16627 + < .773 d. + +Each positive-rank paid job costs at least 1 at p>0. Therefore the changed +moment is at most M(k) - d*(3775/16627). This grants free scalar basis changes, +normalization, routing, restoration and every other unchanged obligation. Any +additional fees can only hurt this comparison. + +It remains to check the small slack between the selected rounded claim and +the raw crossing. The verifier independently reconstructs the complete signed +profile from PR6030's source-bound RESULT.json. Exact rational logarithm and +Taylor bounds give + + M(.003125804) < 13/200, + M'(k) < -234000 for every 0 <= k <= .0034. + +Consequently, for every integer d>=1 and every k in the stated interval, + + changed moment < 13/200 - d*(3775/16627) + <= -538849/3325400 + < -.162. + +Thus this route cannot even retain the selected saving. It cannot increase +kappa under the unchanged BIT and declared one-cut delivery contract. This is +a necessary raw-budget failure; compiler, tail and outer checks cannot rescue +a negative raw moment. + +## Rational certificates without a sampling grid + +For q in [1,2], z=(q-1)/(q+1) belongs to [0,1/3]. The first 32 terms of +2 sum z^(2j+1)/(2j+1) give a lower bound for log(q); the remaining tail is at +most 2 z^65/(65(1-z^2)). Range reduction gives bounds L_r<=log(r)<=U_r. + +For x>=0, P3(x)<=exp(-x)<=P2(x), where + + P2(x)=1-x+x^2/2, P3(x)=P2(x)-x^3/6. + +Both polynomials decrease on the certified x interval [0,1/50]. At the lower +kappa endpoint, sum T_r r P2(k L_r) - sum P_r r P3(k U_r) bounds M from above. +For the derivative, r^(1-k)<=r and r^(1-k)>=r(1-k log r) give the uniform upper +bound + + sum P_r r U_r - sum T_r r L_r (1-(17/5000) U_r). + +All arithmetic is rational. No finite grid is substituted for an interval +claim, addressing the failure mode in PR6049. + +## Existing eligible coordinates on the selected word + +Separately, the unmodified full-subspace census of +[Matarener](https://github.com/Matarener)'s +[PR5994](https://github.com/CrocSwap/integer-mult-bounds/pull/5994) is applied +to the selected PR6030 word. It considers **every role already at the cut +chart**, not only helpers in the boundary group. At 8,734 evaluations across +69 groups and 562 helpers, it finds no pure helper split: six two-sided group +classes have zero cut pairing. The more permissive boundary-support screen +also finds none (1,590 zero cut pairings and 11 zero boundary pairings). + +An enlargement by coordinates already in these complete chart banks is a +restriction of a tested domain and therefore cannot bypass that exclusion. +This last statement concerns PR5599's pure-prefix/pure-suffix split contract; +it does not exclude PR5718 corrections or changed scalar programs. It is not +used to silently identify a rational census with PR6064's dyadic capacity. + +The census implementation and its criterion belong to PR5994. The contribution +here is the current-word receipt and its applicability to the proposed free +eligibility route, alongside the new whole-interval delivery budget. + +## Limits + +This does not price a productive carrier, multi-coordinate paid transport, +different recursive boundary, multi-cut lifetime, changed paid trajectory, +new BIT cap or other helper architecture. It is not a complete multiplier, +native admission, global P104 ceiling, independent human review or formal proof +kernel check. The five selected framework assumptions remain. + +Prepared by [zxv](https://github.com/zxv), with substantial OpenAI Codex assistance. +Credit [Ali Romman](https://github.com/aliromman)'s cut and P104 lineage, +[DreamingOfClouds](https://github.com/DreamingOfClouds)'s PR6030 word/bill, +[Matarener](https://github.com/Matarener)'s full-subspace census, and the retained +source authors. Apache-2.0. diff --git a/research/dyadic-cut-delivery-budget/README.md b/research/dyadic-cut-delivery-budget/README.md new file mode 100644 index 0000000000..181a12ab7d --- /dev/null +++ b/research/dyadic-cut-delivery-budget/README.md @@ -0,0 +1,30 @@ +# P104 single-cut enlargements cannot fund one paid delivery per added coordinate + +Applying [PR6064](https://github.com/CrocSwap/integer-mult-bounds/pull/6064)'s two-channels-per-added-coordinate opportunity to the selected P104 invoice requires a cheaper delivery contract. Under the explicit single-cut realization contract in [PROOF.md](PROOF.md), all additional binary helper splits earn less than **.773 per added coordinate**, even granting 18 LOCAL invocations and charging only one new rank-one call in the entire assembly. That call costs at least one. The route cannot retain selected kappa .003125804, throughout the unchanged BIT range up to .0034. No new kappa is claimed. + +The theorem assumes at most two additional binary helper splits per added coordinate per LOCAL, ranks at most nine, unchanged other targets/paid jobs, and at least one new paid job per added coordinate globally. PR6064's capacity theorem alone does not establish that every supplier realization satisfies this target-count contract. Productive carriers, shared multi-coordinate transport, multi-cut reuse and changed prefixes/boundaries remain outside this exclusion. + +The free-delivery alternative was also checked on the actual selected PR6030 word. The unmodified full-subspace census from [Matarener](https://github.com/Matarener)'s [PR5994](https://github.com/CrocSwap/integer-mult-bounds/pull/5994) already grants every role present at a chart. Both exact group and relaxed boundary supports have zero pure helper splits at all 8,734 evaluated cuts. An added eligible role already in one of those full banks cannot help within that pure split contract. This is an application of the predecessor's algorithm, with its credit retained. + +## Significance for researchers + +The sharp algebraic two-for-one gain in PR6064 is not enough to fund individually paid coordinate delivery in the current assembly. A useful successor should change the delivery/credit contract before growing the scalar fixture. Exact rational bounds cover the entire kappa interval; they do not use a grid that could miss the crossing behavior identified in [PR6049](https://github.com/CrocSwap/integer-mult-bounds/pull/6049). + +## Reproduce + +```sh +python3.12 -B scripts/research_package.py --package research/dyadic-cut-delivery-budget +python3.12 -B scripts/check_research_commit.py --package research/dyadic-cut-delivery-budget +``` + +Normal and optimized commands use the standard library. They authenticate the selected result/word and frozen census, prove rational margin/derivative bounds, recompute both complete cut screens, and check positive, orthogonality and changed-contract controls. RESULT.json is compared with the full recomputation. The current-word census reuses the original engine and is not an independent engine audit or full selected/native/outer replay. + +## Open next questions + +Can one paid transport deliver at least two newly eligible coordinates, or can an existing paid trajectory provide a coordinate at no extra recursive cost? Start with one exact native chart/time/lifetime and the complete signed bill. The one-call-per-coordinate hypothesis would change; this certificate does not rule out that case. + +Can a newly productive carrier or a changed multi-cut continuation earn enough additional credit? First give the independent target, unchanged dirty endpoints and all native/restoration fees. Those credits cannot be inferred from capacity. + +## Credit and limitations + +Prepared by [zxv](https://github.com/zxv), with substantial OpenAI Codex assistance. Credit [Ali Romman](https://github.com/aliromman)'s dyadic cut/P104 work, [Matarener](https://github.com/Matarener)'s source census, [DreamingOfClouds](https://github.com/DreamingOfClouds)'s selected PR6030 word and invoice, [Nick Petalas](https://github.com/petalas)'s related carrier-price [PR6033](https://github.com/CrocSwap/integer-mult-bounds/pull/6033), and their retained predecessors. The pending PR6064 statement is preserved byte-for-byte with its source head and SHA256; no unavailable foreign commit is required. Apache-2.0. No new native construction, supplier admission, global P104 barrier, selected change, independent human review, proof assistant or full multiplier is claimed. The five framework assumptions remain. diff --git a/research/dyadic-cut-delivery-budget/RESULT.json b/research/dyadic-cut-delivery-budget/RESULT.json new file mode 100644 index 0000000000..d50582ab24 --- /dev/null +++ b/research/dyadic-cut-delivery-budget/RESULT.json @@ -0,0 +1,60 @@ +{ + "admitted_bit": "17/5000", + "charged_margin_upper_at_d_one": "-538849/3325400", + "controls": { + "binary_splits": 36, + "free_delivery_outside_exclusion": true, + "rejected_contracts": [ + "extra_paid_job", + "new_rank_ten_target", + "changed_local_multiplicity", + "changed_bit_cap" + ], + "shared_delivery_outside_exclusion": true, + "sharp_two_channel_border": true + }, + "credit_upper_per_added_coordinate": "12852/16627", + "current_kappa": "781451/250000000", + "derivative_upper": "-234000", + "interval": [ + "781451/250000000", + "17/5000" + ], + "local_calls": 18, + "max_helper_rank": 9, + "old_margin_upper": "13/200", + "selected_full_chart_census": { + "boundary": { + "classes": 1601, + "classes_sha256": "f3462dcbe8ca4a7ac8a07d55faa5c05073a35c8cc9eb653fcba741fda2180b78", + "counts": { + "evaluations": 8734, + "groups": 69, + "helpers": 562, + "kind_F1zero": 1590, + "kind_F2zero": 11, + "no_pure_prefix": 5382, + "no_pure_suffix": 1751, + "witnesses": 0 + } + }, + "group": { + "classes": 6, + "classes_sha256": "22b3f7d4140204e627174e7111fa8752108a012e6f8dd9603f0f4c991fb0815a", + "counts": { + "evaluations": 8734, + "groups": 69, + "helpers": 562, + "kind_F1zero": 6, + "no_pure_prefix": 7280, + "no_pure_suffix": 1448, + "witnesses": 0 + } + } + }, + "source_counts": [ + 13444, + 66834 + ], + "status": "PASS_DYADIC_CUT_DELIVERY_BUDGET" +} diff --git a/research/dyadic-cut-delivery-budget/SOURCES.json b/research/dyadic-cut-delivery-budget/SOURCES.json new file mode 100644 index 0000000000..9a547ea20f --- /dev/null +++ b/research/dyadic-cut-delivery-budget/SOURCES.json @@ -0,0 +1,42 @@ +{ + "schema_version": 1, + "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/dyadic-helper-channel-capacity/PROOF.md", + "usage": "input", + "git_blob": "c97a6edce3070414c81f0ef6e6c099ebb17f3a90", + "sha256": "b258a217f2cd0fc48461285fe8ae24de26b0c5963668d9d8f0955fc6e759e929" + }, + { + "path": "research/p104-helper-split-exhaustion/splitcensus.py", + "usage": "input", + "git_blob": "74727424f75adf75bd9061a7473e6cce2f520097", + "sha256": "c3bc8cfc14ab8fdbe600f06401119c7a7b6c5fe8dc460b6b1933cda7ef4bf1dd" + }, + { + "path": "research/p104-helper470-twin-rung-removal/RESULT.json", + "usage": "input", + "git_blob": "e4a03118d585fb80c9ac932281b528ac394ccc5f", + "sha256": "84fcbe2a0b64307b5703c363408042bdd91555b0419509aa50daa43b3b1924ad" + }, + { + "path": "research/p104-helper470-twin-rung-removal/WORD.json.gz", + "usage": "input", + "git_blob": "22f9ab02d1b73ea0aa4b07ce445a14cc2602c760", + "sha256": "7834725d9e34ee846a9ccc615221ea81e0201613938afa185d2eda0c9a6c232f" + } + ] +} diff --git a/research/dyadic-cut-delivery-budget/TASK.json b/research/dyadic-cut-delivery-budget/TASK.json new file mode 100644 index 0000000000..86b493b4db --- /dev/null +++ b/research/dyadic-cut-delivery-budget/TASK.json @@ -0,0 +1,129 @@ +{ + "schema_version": 1, + "task_id": "p104-side-correction", + "priority_revision": 8, + "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419", + "original_card": { + "id": "p104-side-correction", + "question": "Can joint helper bases and a legal causal split improve the complete P104 productive/paid invoice?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "research/p104-helper-subspace-splits/README.md", + "research/dyadic-helper-channel-capacity/README.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "An exact arbitrary-input identity, source/target frame availability and restoration at the chosen cut, plus the complete channel+correction+idle/hosting bill or an explicit favorable bound. The native channel alone is not a supplier. 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", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Start with the selected #5599 emitted word and review pending #5718 distinct input/output bases plus #5717/#5719 coverage before claiming work. Pick one uncovered source word, helper group and cut region. Prove the arbitrary-input relation and legal entry/exit corrections, then compare full target and paid profiles. Reject if completion, owned lifetimes or consumer costs repay the gain. A static pairing rank alone is not a physical split.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "P104", + "helper basis", + "helper split", + "5718", + "dyadic capacity" + ], + "existing_checks": [ + { + "scope": "PR #4133: literal-slot defect", + "evidence": "research/p104-literal-slot-defect/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "88666f1dee93fbd85b31fd5d6f91a219e111b5f4", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4136: uniform commutation gap", + "evidence": "research/p104-uniform-commutation-gap/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "281ce601a8be9db470de630759179c23e1dfaa88", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4140: uniform encoding gap", + "evidence": "research/p104-uniform-encoding-gap/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "de25c6525aa866962309df5d107b32d55e6e5628", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4153: source-chart shortcut exhausts its optimistic allowance", + "evidence": "research/p104-source-chart-shortcut/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "9123241fea53df77e51ffe30d9aca1625d4bf3a8", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4154: fiber-tag seam mismatch", + "evidence": "research/p104-fiber-tag-seam/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "4ffcdaee5d6255a9cea1fe53a5424435068089d0", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "refined", + "actual_scope": "Apply the PR6064 fixed-cut opportunity to a declared two-channel binary-split delivery contract on the selected PR6030 complete invoice, including the available-role pure-split screen.", + "scope_change_reason": "Assigned follow-up to recent zxv PRs, starting with PR6064. The source fixture alone does not supply a native delivery contract.", + "bottleneck_link": "Screens whether the two-for-one capacity gain can fund additional paid delivery before constructing a supplier.", + "budget_minutes": 30, + "stop_rule": "Stop at a whole-interval invoice decision and actual selected-word full-bank screen; do not infer a universal bound for other delivery, target or multi-cut contracts.", + "outcome": "negative-result", + "evidence": "PROOF.md; RESULT.json; exact rational interval bounds and unmodified source census.", + "author": "zxv", + "ai_assistance": "Substantial OpenAI Codex assistance; no subagents or independent human/formal review.", + "open_questions": [ + { + "question": "Can one paid job deliver multiple eligible coordinates or an existing trajectory supply one?", + "why_it_matters": "Changes the losing one-job-per-coordinate contract.", + "first_step": "Pin one native chart/time/lifetime and its full signed invoice.", + "blocked_by": "No physical delivery/credit construction supplied." + }, + { + "question": "Can productive carrier targets or a changed multi-cut program fund delivery?", + "why_it_matters": "Such credits are outside the fixed one-cut binary-split screen.", + "first_step": "Specify independent targets, scalar endpoint and all native/restoration fees.", + "blocked_by": "Changed consumer and complete bill required." + } + ], + "freshness": { + "canonical_main": "721c03822c421b7f7fcbb2598993b947c4d88419", + "priority_revision": 8, + "checked_utc": "2026-10-28T05:14:00Z", + "overlap": "341 open PR bodies and 5724 discussion records; complete remote pagination. Sparse local notes and unpublished work remain limits. Own PR6064 is the starting point; PR5994 is its source-word dependency check." + } +} diff --git a/research/dyadic-cut-delivery-budget/VERIFY.json b/research/dyadic-cut-delivery-budget/VERIFY.json new file mode 100644 index 0000000000..3b69fdcc75 --- /dev/null +++ b/research/dyadic-cut-delivery-budget/VERIFY.json @@ -0,0 +1,35 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/dyadic-helper-channel-capacity/PROOF.md", + "research/p104-helper-split-exhaustion/splitcensus.py", + "research/p104-helper470-twin-rung-removal/RESULT.json", + "research/p104-helper470-twin-rung-removal/WORD.json.gz" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Rational interval budget, both complete cut screens, positive and changed-contract controls" + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Same checks under optimization" + } + ] +} diff --git a/research/dyadic-cut-delivery-budget/predecessor/PR6064-README.md b/research/dyadic-cut-delivery-budget/predecessor/PR6064-README.md new file mode 100644 index 0000000000..312b56bc97 --- /dev/null +++ b/research/dyadic-cut-delivery-budget/predecessor/PR6064-README.md @@ -0,0 +1,188 @@ +# One extra cut coordinate can restore two dyadic helper channels + +In the fixed-prefix dyadic helper interface of +[Ali Romman](https://github.com/aliromman)'s +[PR #5615](https://github.com/CrocSwap/integer-mult-bounds/pull/5615), enlarging +the eligible cut by $d$ scalar coordinates changes its unit-channel capacity by +at most $2d$. The bound is sharp for every positive integer $d$. +One added coordinate can therefore unlock **two** channels, not just one. + +The attaining example is source-relative: the exact three-coordinate causal +fixture already present in #5615 has capacity zero on its restricted two-coordinate +cut and capacity two when its third coordinate becomes eligible. No prefix, +suffix or helper target is changed. Its complete arbitrary-dirty identity word +costs 12 signed scalar ADDs. Repeating independent blocks attains the $2d$ gain +with $d$ extra eligible coordinates and a full cost of $12d$ ADDs. + +This is a scoped cut-module theorem and calibration construction, not a native +P104 realization, productive-target split, selected-frontier change or new κ. +Eligibility is a changed contract; permitting the third coordinate at a physical +common chart and delivering its channels remain separate obligations. + +## Fixed contract and sharp bound + +Let $D=\mathbb{Z}[1/2]$. Keep the prefix $A$, suffix $B$, helper input/output +support $G$, and complete endpoint fixed. Let $E$ be the dyadic row module +whose prefix image has support in $G$, and let $H$ be the corresponding suffix +column module. For eligible coordinate supports $F\subseteq F'$, define + +$$ +L=F\cap E,\qquad L'=F'\cap E, +\qquad R=F\cap H,\qquad R'=F'\cap H. +$$ + +The row/column copies of a coordinate module are identified in this notation. +Suppose $F'/F$ has rank $d$. With full dyadic bases, form the old and new +pairings $K$ and $K'$. Let $c(K)$ be the largest $t$ for which dyadic matrices +$X,Y$ satisfy $XKY=I_t$. Then + +$$ +\boxed{0\leq c(K')-c(K)\leq2d.} +$$ + +**Proof.** The quotient $L'/L$ injects into $F'/F$: its kernel consists precisely +of those eligible rows already in $F$. It is therefore a free $D$-module of rank +$a\leq d$. The short exact sequence splits, so every full basis of $L$ extends +to one of $L'$. Likewise a full basis of $R$ extends by $b\leq d$ columns. +Thus compatible choices of full bases put $K$ in the upper-left block of $K'$. + +Padding old $X,Y$ with zeros shows $c(K')\geq c(K)$. By #5615's single-cut +criterion, some odd prime $p$ attains $c(K)$ as the rank of $K$ modulo $p$. +Adding $a$ rows and $b$ columns can raise rank by at most $a+b$. Consequently + +$$ +c(K')\leq r_p(K')\leq r_p(K)+a+b\leq c(K)+2d, +$$ + +where $r_p$ denotes rank modulo $p$. This proves the bound. The argument does +not require the added channels to be simple tensors or to use coordinate bases +inside the eligible modules. ∎ + +The proof requires a **fixed** prefix, suffix, helper support and embedding of +the old cut into the new one. A different program or helper endpoint need not +contain the old pairing block. The theorem then supplies no capacity bound. + +## Exact source fixture: zero becomes two + +The retained fixture has prefix and inverse suffix + +$$ +A=\begin{pmatrix}1&0&1\\0&1&2\\1&2&6\end{pmatrix}, +\qquad +B=\begin{pmatrix}2&2&-1\\2&5&-2\\-1&-2&1\end{pmatrix}. +$$ + +Take helper support $G$ on the first two original coordinates. On the old cut +$F$, also supported on the first two physical coordinates, the full eligible +row and column bases are both $(-2,1)$. Their pairing is $[5]$, with rational +rank one but zero dyadic unit capacity: reduction modulo five has rank zero. + +Now allow the third physical coordinate, so $F'$ is the whole ambient space. +Full eligible bases are the first two rows of $B$ and the first two columns +of $A$. Their pairing is $I_2$, since $BA=I_3$. The new capacity is exactly two. +These are full module bases: invertibility over $D$ identifies them with all +helper-supported rows and columns. No clean-input assumption is used. In bases +that extend the old ones, the enlarged pairing is + +$$ +K'=\begin{pmatrix}5&-2\\-2&1\end{pmatrix}, +\qquad 5\cdot1-(-2)^2=1. +$$ + +Its old upper-left block is still $[5]$, while the whole block is a unit. + +The exact prefix, in current-value semantics, is + +```text +x0 += z +x1 += z +x1 += z +z += x0 +z += x1 +z += x1 +``` + +The suffix executes these instructions in reverse order with minus signs. +All three independent dirty inputs are restored. The complete word has 12 +signed ADDs and uses the same three coordinates before and after changing the +eligible support. No allocation or basis conversion is silently added to this +calibration word. Realizing the changed eligibility and channel delivery in a +native supplier is not provided or priced as zero. + +For $d$ independent blocks, the old pairing is $5I_d$ and the enlarged pairing +is $I_{2d}$. Adding all $d$ third coordinates therefore attains the bound $2d$. +If only $s$ third coordinates become eligible, the exact capacity is $2s$. +This also gives every intermediate even gain in the family. + +## A necessary size for a nonproduct rescue + +[Nick Petalas](https://github.com/petalas)'s +[PR #5882](https://github.com/CrocSwap/integer-mult-bounds/pull/5882) proves that +an algebraic repeated pairing $K$ has tensor capacity $c(K)^f$ and rational +rank $r(K)^f$. Suppose an actual product cut has this exact pairing. Any +fixed-prefix enlargement that raises its capacity to at least $r(K)^f$ must add + +$$ +d\geq\left\lceil\frac{r(K)^f-c(K)^f}{2}\right\rceil +$$ + +eligible scalar coordinates. This follows by applying the sharp bound to the +whole tensor cut. It does not assume that the enlarged cut itself factors. +This is a coordinate-availability requirement, not a paid-job or storage tariff: +newly eligible coordinates may already exist. Their native charts, timing and +delivery still require a separate source-bound bill. + +## Evidence and reproduction + +``` +python3.12 -B scripts/research_package.py --package research/dyadic-cut-enlargement +python3.12 -B scripts/check_research_commit.py --package research/dyadic-cut-enlargement +``` + +The verifier authenticates the unchanged #5615 kernel/capacity source and the +#5882 proof. It reconstructs every ADD of the scalar words, solves the complete row/column eligibility constraints with the retained kernel +routine, and checks all partial support +enlargements of one through six independent blocks. It verifies literal full +unit-block witnesses and modular upper bounds, including odd and dyadic-scaled +coefficient controls. A separate small bordered-matrix census corroborates the +rank bound. Wrong cut supports, a nonsaturated basis, false one-channel gain +bounds and a changed prefix are rejected. Normal and optimized replays use +explicit checks and write no package files. + +Canonical main was refreshed on 2026-10-28 UTC at +721c03822c421b7f7fcbb2598993b947c4d88419, priority 8. The navigation repair +from [PR #6050](https://github.com/CrocSwap/integer-mult-bounds/pull/6050) is +included; frozen packages and the selected record are unchanged. No selected +cold replay ran. The optional full-history preflight is unavailable in this +shallow checkout; all declared pins use its reachable base. + +## Significance for researchers + +A zero-capacity restricted cut need not remain useless after one legal support +change. Conversely, each extra eligible coordinate can recover at most two +channels while the program is fixed. This supplies a sharp optimistic resource +screen for nonproduct support changes beyond +[PR #6054](https://github.com/CrocSwap/integer-mult-bounds/pull/6054)'s product-cut +obstruction. It does not grant the physical common-chart or consumer contract. + +## Open next questions + +Can one actual native helper cut make an outside coordinate eligible at a paid +cost that its additional channels can fund? First extract the fixed prefix, +suffix and complete support embedding, then prove legal chart/timing and delivery. +The scalar fixture alone does not supply those conditions. + +Can changed prefixes or helper endpoints beat the fixed-program two-per-coordinate +bound at a favorable complete invoice? First name the changed map and preserve +all independent dirty inputs. Such changes lie outside this theorem. + +## Credit + +Prepared by [zxv](https://github.com/zxv) with substantial OpenAI Codex assistance. +[Ali Romman](https://github.com/aliromman) supplies the single-cut theorem, +source fixture and unchanged saturated-kernel code in #5615. +[Nick Petalas](https://github.com/petalas) supplies #5882's tensor formula. +Their methods and prior attribution remain intact. Module splitting over a PID +and bordered-matrix rank bounds are classical. The contribution is their sharp +fixed-cut enlargement implication and the source-relative attaining family. +No independent human or proof-assistant review is claimed. Apache-2.0. diff --git a/research/dyadic-cut-delivery-budget/verify.py b/research/dyadic-cut-delivery-budget/verify.py new file mode 100644 index 0000000000..aea086372d --- /dev/null +++ b/research/dyadic-cut-delivery-budget/verify.py @@ -0,0 +1,147 @@ +"""Exact one-cut delivery budget. zxv, with OpenAI Codex assistance. Apache-2.0.""" +from fractions import Fraction as Q +from hashlib import sha256 +from pathlib import Path +import gzip +import importlib.util +import json +from copy import deepcopy + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +RESULT = 'research/p104-helper470-twin-rung-removal/RESULT.json' +WORD = 'research/p104-helper470-twin-rung-removal/WORD.json.gz' + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def log_bounds(q, terms=32): + """2 atanh(z), with 0 <= z <= 1/3 and an exact geometric tail.""" + q = Q(q) + need(1 <= q <= 2, 'range-reduced logarithm') + z = (q-1)/(q+1) + low = 2*sum((z**(2*j+1)/Q(2*j+1) for j in range(terms)), Q(0)) + tail = 2*z**(2*terms+1)/(Q(2*terms+1)*(1-z*z)) + return low, low+tail + + +def integer_log(r): + k = r.bit_length()-1 + a, b = log_bounds(Q(r, 1 << k)) + c, d = log_bounds(2) + return a+k*c, b+k*d + + +def p2(x): + return 1-x+x*x/2 + + +def p3(x): + return p2(x)-x*x*x/6 + + +def budget(record): + c = record['complete_cost'] + target = {int(r): n for r, n in c['targets'].items()} + paid = {int(r): n for r, n in c['paid'].items()} + n = c['full_forward_calls'] + h = max(map(int, record['local']['helpers'])) + lo, hi = Q(c['kappa']), Q(c['ordinary_BIT']['admitted']) + need(n == 18 and h == 9 and lo == Q(781451,250000000) and hi == Q(17,5000), + 'source-bound contract') + need(sum(target.values()) == c['productive_fields'] == 13444 and + sum(paid.values()) == c['paid_calls'] == 66834, 'complete inventory counts') + need(sum(r*v for r,v in target.items())-sum(r*v for r,v in paid.items()) == 760, + 'complete rank-mass surplus') + logs = {r: integer_log(r) for r in set(target)|set(paid)} + need(all(0 <= hi*b < Q(1,50) for a,b in logs.values()), 'Taylor interval') + old_upper = sum(v*r*p2(lo*logs[r][0]) for r,v in target.items()) - sum( + v*r*p3(lo*logs[r][1]) for r,v in paid.items()) + derivative_upper = sum(v*r*logs[r][1] for r,v in paid.items()) - sum( + v*r*logs[r][0]*(1-hi*logs[r][1]) for r,v in target.items()) + need(old_upper < Q(13,200), 'old raw margin upper bound') + need(derivative_upper < -234000, 'whole-interval decreasing raw margin') + need(log_bounds(2)[1] < Q(7,10), 'rational logarithm bound') + per_coordinate = 2*n*h*(Q(7,10)*hi)/(1-Q(7,10)*hi) + need(per_coordinate == Q(12852,16627) < Q(773,1000), 'two-channel credit envelope') + final_upper = Q(13,200)+per_coordinate-1 + need(final_upper < -Q(162,1000), 'one charged coordinate fails at every allowed kappa') + return dict(local_calls=n, max_helper_rank=h, admitted_bit=str(hi), current_kappa=str(lo), + old_margin_upper='13/200', derivative_upper='-234000', + credit_upper_per_added_coordinate=str(per_coordinate), + charged_margin_upper_at_d_one=str(final_upper), + interval=[str(lo), str(hi)], source_counts=[13444,66834]) + + +def controls(record): + count = 0 + for r in range(2,10): + for a in range(1,r): + need(4*a*(r-a) <= r*r, 'binary split Jensen control') + count += 1 + need(5*1-(-2)*(-2) == 1, 'PR6064 sharp bordering fixture') + need(Q(12852,16627) > 0, 'free-coordinate contract is not excluded') + need(2*Q(12852,16627) > 1, 'shared delivery escapes this price screen') + rejected = [] + for name, change in ( + ('extra_paid_job', lambda r: r['complete_cost']['paid'].__setitem__('1',41503)), + ('new_rank_ten_target', lambda r: r['local']['helpers'].__setitem__('10',1)), + ('changed_local_multiplicity', lambda r: r['complete_cost'].__setitem__('full_forward_calls',19)), + ('changed_bit_cap', lambda r: r['complete_cost']['ordinary_BIT'].__setitem__('admitted','1/200'))): + damaged = deepcopy(record) + change(damaged) + try: + budget(damaged) + except ValueError: + rejected.append(name) + else: + raise ValueError('changed contract accepted: '+name) + return dict(binary_splits=count, sharp_two_channel_border=True, + free_delivery_outside_exclusion=True, shared_delivery_outside_exclusion=True, + rejected_contracts=rejected) + + +def calculate(): + for pin in json.loads((HERE/'SOURCES.json').read_text())['files']: + if pin['usage'] == 'input': + need(sha256((ROOT/pin['path']).read_bytes()).hexdigest() == pin['sha256'], + 'source bytes: '+pin['path']) + old = json.loads((HERE/'PREDECESSOR.json').read_text()) + need(sha256((HERE/old['retained_path']).read_bytes()).hexdigest() == old['sha256'], + 'retained PR6064 bytes') + record = json.loads((ROOT/RESULT).read_text()) + result = budget(record) + path = ROOT/'research/p104-helper-split-exhaustion/splitcensus.py' + spec = importlib.util.spec_from_file_location('retained_matarener_census', path) + census = importlib.util.module_from_spec(spec) + spec.loader.exec_module(census) + word = json.loads(gzip.decompress((ROOT/WORD).read_bytes())) + receipts = {} + for mode in ('group','boundary'): + counts, records = census.census(word, in_support=mode, out_support=mode) + need(counts['evaluations'] == 8734 and counts['groups'] == 69 and + counts['helpers'] == 562 and counts['witnesses'] == 0, 'selected census contract') + need(all(r['kind'] in ('F1zero','F2zero') for r in records), 'explicit orthogonality exclusions') + receipts[mode] = dict(counts=counts, classes=len(records), + classes_sha256=sha256(json.dumps(records,sort_keys=True, + separators=(',',':')).encode()).hexdigest()) + v = {0:Q(1)} + need(census.decide([(v,v)],[(v,v)])[0] == 'witness', 'synthetic legal cut') + need(census.decide([(v,v)],[({1:Q(1)},v)])[0] == 'F1zero', 'orthogonal cut') + need(census.decide([(v,v)],[(v,{1:Q(1)})])[0] == 'F2zero', 'boundary mismatch') + result.update(status='PASS_DYADIC_CUT_DELIVERY_BUDGET', + selected_full_chart_census=receipts, controls=controls(record)) + return result + + +def main(): + result = calculate() + need(result == json.loads((HERE/'RESULT.json').read_text()), 'committed receipt') + print(json.dumps(result,sort_keys=True)) + + +if __name__ == '__main__': + main()