diff --git a/research/p104-all-pair-consumer-budget/PREDECESSORS.json b/research/p104-all-pair-consumer-budget/PREDECESSORS.json new file mode 100644 index 0000000000..9761b1b02b --- /dev/null +++ b/research/p104-all-pair-consumer-budget/PREDECESSORS.json @@ -0,0 +1,41 @@ +{ + "schema_version": 1, + "files": [ + { + "pr": 2458, + "commit": "3170afd2fc13a990bfe28f5ab6421bcda4ffd0f6", + "upstream_path": "research/p104-two-target-native/inputs/CIRCUIT.json", + "path": "inputs/PR2458-CIRCUIT.json.gz", + "git_blob": "17b0a10eafaf6e6c0db78690f01dc48505c63a4d", + "raw_sha256": "c34d94128decc426e7528302ab2570967293a1b293f184fdd89fd376addd61f9", + "stored_sha256": "b8c4777fc4a8415f528a2f3ec247ec729ed70dfb218226e9f5f5ce8a61fff5fc" + }, + { + "pr": 2458, + "commit": "3170afd2fc13a990bfe28f5ab6421bcda4ffd0f6", + "upstream_path": "research/p104-two-target-native/README.md", + "path": "inputs/PR2458-README.md", + "git_blob": "979be231f8e5994e8be3bcac178c09775120c5c5", + "raw_sha256": "a9aacd624c17ec6ba97583d866a1833c5f027866d1eeb181cc8b2ada48b7ec08", + "stored_sha256": "a9aacd624c17ec6ba97583d866a1833c5f027866d1eeb181cc8b2ada48b7ec08" + }, + { + "pr": 2712, + "commit": "afa5d6649460dcdb93489babd74f0ee9d01a4911", + "upstream_path": "research/p104-shared-chart-retiming/WORD.json", + "path": "inputs/PR2712-WORD.json.gz", + "git_blob": "e071eb090efe6a7a98db70c594d1081c1530272c", + "raw_sha256": "f395a54f747eea8dd5d54b0959a6ab4bfa8c5bed6447c9dd2586f2f68b0eed74", + "stored_sha256": "4023ee4cd24bca368fbabb7e356859dc83917d89e2b623b474388ccac970a323" + }, + { + "pr": 2712, + "commit": "afa5d6649460dcdb93489babd74f0ee9d01a4911", + "upstream_path": "research/p104-shared-chart-retiming/README.md", + "path": "inputs/PR2712-README.md", + "git_blob": "a1890be765dc7a266d9cb4816f1ca04acb57eb70", + "raw_sha256": "2435c9fe9adbcde892840975d9875fc0e36c9211330f851a53a256dddaaa6493", + "stored_sha256": "2435c9fe9adbcde892840975d9875fc0e36c9211330f851a53a256dddaaa6493" + } + ] +} diff --git a/research/p104-all-pair-consumer-budget/README.md b/research/p104-all-pair-consumer-budget/README.md new file mode 100644 index 0000000000..9af6b04642 --- /dev/null +++ b/research/p104-all-pair-consumer-budget/README.md @@ -0,0 +1,217 @@ +# An all-pair-count screen for the current P104 forward and dual + +Scoped conditional obstruction. No supplier admission or new kappa. + +The pinned PR2458 forward and PR2712 physical dual cannot meet the selected +saving in the paired-chain coverage model below, for **any integer pair count +`p >= 1`**, even with 416 rank units forgiven per dual and the other 102 forward +corrections supplied free. Any finite number of fully paid auxiliary banks +also fails. The selected frontier and predecessor files are unchanged. + +This extends Jose Manuel / `jmbarrancoml`'s +[four-pair Discussion calculation](https://github.com/CrocSwap/integer-mult-bounds/discussions/2619#discussioncomment-18955566). +It is not another local fusion or endpoint-rank result. The new step covers +all pair counts with the actual changing width `m=16p+9`, rather than +extrapolating the four-pair width 73. + +## Exact contract and evidence + +Fix these local positive-child profiles, independently recounted from the +retained transport events using exact binary elimination: + +| Rank | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | Rank mass | +| --- | ---: | ---: | ---: | ---: | ---: | ---: | ---: | ---: | ---: | +| PR2458 forward F | 1216 | 74 | 86 | 104 | 48 | 42 | 68 | 8 | 3070 | +| PR2712 dual D | 1498 | 60 | 74 | 92 | 58 | 56 | 92 | 8 | 3542 | +| Optimistic dual D* | 1082 | 60 | 74 | 92 | 58 | 56 | 92 | 8 | 3126 | + +Exact source heads: + +- PR2458, ywz65, `3170afd2fc13a990bfe28f5ab6421bcda4ffd0f6`. +- PR2712, ywz65, `afa5d6649460dcdb93489babd74f0ee9d01a4911`. + +`PREDECESSORS.json` binds the retained data and original README notices to +SHA256 and original Git blobs. `SOURCES.json` binds live inputs and historical +assignment provenance. No predecessor Python is imported or executed. The +checker also recounts net endpoint progress as 2312 original plus 702 added +forward units and 3014 dual units. Crediting those units to global coverage +is conditional. Native correctness and complete forward/dual boundaries +remain inherited, not newly verified here. The forward count combines the original PR1972 word retained +by PR1991 with PR2458's two insertion lists; this is an invoice recount, not a +new chronology or native proof. + +The conditional consumer has, per replica: + +- `p+1` forward calls, `p` dual calls, `m=16p+9` and `W=208p` live data families. +- One unpaid coordinate per live data family. +- At most `C=104*8+104*8+150*9=3014` units of persistent endpoint progress per + call. We grant that entire amount to every call, including descending paths + and the discounted dual, without requiring an actual compatible owner map. +- With `B_aux>=0` fully paid auxiliary banks, residual coverage at least + `I_B=max(0,(m-1)W+m*B_aux-(2p+1)C)`. Without banks write `I=I_0`. + We grant residual children rank `m`, above the retained halving guard. +- Every other obligation free, including missing forward corrections, scalar + and monomial work, allocation, movement, precision and restoration overhead. + +The template formulas come from Dominik Scholz's retained `larger-gain` model +and the explicitly conditional P104 substitution in +[`p104-terminal-correction-floor`](../p104-terminal-correction-floor/README.md). +This is not a claim that its coverage law, inventory or owner windows have +been realized for these nonmonotone words. A consumer with extra unpaid +coordinates, different coverage, different call multiplicities, shared work +that changes the profiles, or different endpoint progress is outside the +result. Costs cannot simply be removed while retaining endpoint credit from +a different contract. + +## Proof + +Write `a0=836330098538459/500000000000000000`, the selected kappa. Testing at +this smaller value favors the candidate: the retained transfer requires a +primitive saving strictly larger than kappa, and each child cost is +nondecreasing in the saving. + +For `0= (m-1)W+m*B_aux-(2p+1)C` directly. It gives paid-plus-idle +mass at least `m*(W+B_aux)+56-40p`, a strict **16-unit** excess at `p=1`. +Since `(r/m)^(1-a)>=r/m`, this rejects every nonnegative saving. The stronger +4066-unit zero-bank margin must not be reused unchanged after adding banks. + +For `p>=2`, `I=3328*(p-2)^2+8948*(p-2)+1570>=0`. The zero-bank +paid-plus-idle mass is + +``` +sum_r n_r(p)*r + I = mW + 56 - 40p. +``` + +Use `exp(x)>=1+x` to get + +``` +M_p,0(a0) >= 1 + [56-40p + a0*L_p] / (mW), +L_p = sum_r n_r(p)*r*log(m/r). +``` + +The executable uses only rational lower bounds for these logarithms. For +`x>=1`, put `t=(x-1)/(x+1)`. Integrating the finite geometric series for +`1/(1-t^2)` gives + +``` +log(x) >= 2*sum_{j=0}^{127} t^(2j+1)/(2j+1). +``` + +It rounds this sum down to six decimal places. No floating-point sign decision +or numerical root enters acceptance. + +For each of `p=2,3,4,5,6,7`, substituting these bounds makes the excess +numerator strictly greater than **46**. For every `p>=8`, `m>=137`, so use the +single fixed table of lower bounds for `log(137/r)`. It gives + +``` +56-40p+a0*L_p >= A*p+B, +A > 2/3, B > 76. +``` + +The exact certified values are +`A=6793028173440143209107/10000000000000000000000` and +`B=19117566126860375528272583/250000000000000000000000`. +They prove the entire infinite tail, not a sampled large-p range. +Consequently `M_p,0(a0)>1` for every positive integer p, and the same holds +at any required primitive saving `a>=a0` below one. + +For `p>=2`, nonnegative `I` gives `I_B=I+m*B_aux`. The same positive +excess numerator is therefore divided by `m*(W+B_aux)`, rather than `mW`. +It remains strictly positive for every finite `B_aux`. The clamped `p=1` +case was handled separately above. Banks receive no unpaid-coordinate +credit; granting that credit changes the contract. + +## Reproduce + +Standard-library Python 3.12 or later, from the repository root: + +```sh +python3 -I -B research/p104-all-pair-consumer-budget/verify.py +python3 -I -O -B research/p104-all-pair-consumer-budget/test_verify.py +python3 scripts/research_package.py --package research/p104-all-pair-consumer-budget +``` + +Expected marker: `PASS_P104_ALL_PAIR_CONSUMER_BUDGET all_p>=1 finite=6 tail_from=8 no_new_kappa`. +The normal verifier is read-only and compares its complete recomputed receipt +with `RESULT.json`. Only explicit `--write` replaces that receipt. +Tests exercise the credited p=4 profile as a positive fixture, lower-saving +non-rejection, wrong mass/rank/nesting, duplicate JSON keys, source and receipt +corruption, optimized Git-free replay and equivalent gzip recompression. +A separate set-span census checks all 3584 transport occurrences without +using the primary elimination routine. + +Local validation passes on CPython 3.12.15 through the registered hook and +CPython 3.13.5 with optimized execution. All 11 package tests pass. The 70 +research-workflow tests pass with two skips. Ruff `E,F,I,UP,B` diagnostics +pass. No hosted-CI or independent human review is claimed. + +## Expansion decision and limitations + +Pause extensions that only change pair count, repack idle coverage or add +fully paid banks to these exact profiles under this exact consumer. Local +native and fusion contributions remain useful. Reopen with a source-bound +changed profile or consumer and a new complete coverage/cost ledger. + +This does not bound every P104 decoder, interleaved correction, changed +producer/consumer or multiplication algorithm. No native cold replay, +all-size proof, physical owner/routing construction, precision/tape admission, +selected-supplier replay or formal-kernel check is claimed. + +Python allocates managed integers and fractions during this bounded check. +JSON payloads are capped at 2 MB; each word has at most 6000 events, each frame +uses at most 18 nine-bit vectors, and each logarithm uses exactly 128 terms. +The all-p proof uses six base cases and one tail, not an unbounded loop. +Source JSON contains varying event shapes, so its parsed representation is +dynamic; rank/frame and source bindings validate the proof-relevant boundary. + +## Open next questions + +Can a changed P104 consumer provide enough additional unpaid-coordinate or +endpoint-progress credit without repaying it in restoration? First write its +actual boundary and replace `I` above with a justified coverage law. The +blocker is a compatible physical consumer, not another optimizer seed. + +Can a changed complete local profile escape this screen? First recount both +directions, including all missing corrections, then replace F and D in the +same optimistic screen. The current words correct only two forward rows; +finishing the other rows at unchanged cost was merely a favorable assumption. + +## Credit + +Jose Manuel / `jmbarrancoml` supplied the p=4 screen and 416-unit discount +argument in Discussion2619. ywz65 supplied PR2458's native binding, PR2497 and +PR2586's physical-dual lineage, and PR2712's retiming. commdata2338 supplied +PR2662's endpoint fusion; Nick Petalas supplied PR2550's complementary-frame +method. Ross Richardson / PR2445 supplied the two-target correction. + +Retain Chafik Boukhalfa / PR1991, Rohan Arun / PR1972, Adam Gall / PR1940, +Josie Elliston / PR1071, Ali Romman / PR1125 and PR1862, icekylinx and the +retained geometry/compiler lineage. Dominik Scholz supplied the larger-gain +stage template; Sagar Thakrar / PR1012 supplied the coverage context; Douglas +Colkitt supplied the selected-word ceiling context. Original notices remain +in the retained predecessor READMEs. The selected construction's complete +attribution remains in its selected review. + +New all-p theorem, checker and tests by Nick Petalas. Apache-2.0. diff --git a/research/p104-all-pair-consumer-budget/RESULT.json b/research/p104-all-pair-consumer-budget/RESULT.json new file mode 100644 index 0000000000..25eef898c2 --- /dev/null +++ b/research/p104-all-pair-consumer-budget/RESULT.json @@ -0,0 +1,83 @@ +{ + "benchmark_kappa": "836330098538459/500000000000000000", + "dual_profile": { + "1": 1498, + "2": 60, + "3": 74, + "4": 92, + "5": 58, + "6": 56, + "7": 92, + "8": 8 + }, + "forgiven_dual_rank_units": 416, + "forward_profile": { + "1": 1216, + "2": 74, + "3": 86, + "4": 104, + "5": 48, + "6": 42, + "7": 68, + "8": 8 + }, + "granted_progress_per_call": 3014, + "proof": { + "finite": [ + { + "excess_numerator_lower": "2333928965018189409912569/50000000000000000000000", + "idle_mass": 1570, + "pairs": 2, + "width": 41 + }, + { + "excess_numerator_lower": "11702659768827381992505383/250000000000000000000000", + "idle_mass": 13846, + "pairs": 3, + "width": 57 + }, + { + "excess_numerator_lower": "12486665269682362309858421/250000000000000000000000", + "idle_mass": 32778, + "pairs": 4, + "width": 73 + }, + { + "excess_numerator_lower": "173126800715354667969069/3125000000000000000000", + "idle_mass": 58366, + "pairs": 5, + "width": 89 + }, + { + "excess_numerator_lower": "1568390379493440705385457/25000000000000000000000", + "idle_mass": 90610, + "pairs": 6, + "width": 105 + }, + { + "excess_numerator_lower": "1791153457249179052469097/25000000000000000000000", + "idle_mass": 129510, + "pairs": 7, + "width": 121 + } + ], + "p1_any_paid_banks_mass_excess_lower": 16, + "p1_mass_excess": 4066, + "tail_from_pairs": 8, + "tail_intercept_lower": "19117566126860375528272583/250000000000000000000000", + "tail_log_lower": { + "1": "614347/125000", + "2": "2113383/500000", + "3": "3821367/1000000", + "4": "1766843/500000", + "5": "3310543/1000000", + "6": "3128221/1000000", + "7": "297407/100000", + "8": "2840539/1000000" + }, + "tail_slope_lower": "6793028173440143209107/10000000000000000000000" + }, + "schema_version": 1, + "scope": "Conditional paired-chain coverage; all integer p>=1 and finite fully paid banks. No supplier or new kappa.", + "status": "PASS_P104_ALL_PAIR_CONSUMER_BUDGET" +} diff --git a/research/p104-all-pair-consumer-budget/SOURCES.json b/research/p104-all-pair-consumer-budget/SOURCES.json new file mode 100644 index 0000000000..8bd7849b0a --- /dev/null +++ b/research/p104-all-pair-consumer-budget/SOURCES.json @@ -0,0 +1,48 @@ +{ + "schema_version": 1, + "base_commit": "0374b3e6a532dac112813523d605288c416418c1", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "889b95d936746df124872133ae1e7cc339adcb92", + "sha256": "7d185cd8c2af35988d638d969748ad7b670f902606444dbfc748e4402c340df6" + }, + { + "path": "research/community-frontier1094-audit/ASSEMBLY.json", + "usage": "input", + "git_blob": "5fd676df060f3b450782fdf5ff5f6beb63a5eeb0", + "sha256": "1122cb3a575f8c788345fc1bf4c108ac7c3250fb81a5988671f5eb04b3ab3045" + }, + { + "path": "research/larger-gain/geometry/stage_relaxation.py", + "usage": "input", + "git_blob": "59240fe6c9bc124f0b3fab623969be0b5f7c2f7c", + "sha256": "3cbb7c80c6b1b7b5a5e1f1287f2ab37304814c7f89c2b3b4a980c943c260d9d8" + }, + { + "path": "research/larger-gain/stages/screen_stages.py", + "usage": "input", + "git_blob": "a3ee742bcf6dc319a1211fbd2359a53114cfbb56", + "sha256": "406f46288b31add60ee49ad616e721ce0a18e5eb72b7b9a7dd8664466a4dd8db" + }, + { + "path": "research/p104-terminal-correction-floor/README.md", + "usage": "input", + "git_blob": "d32e168d4ea54fe821247a5847726aec62862b96", + "sha256": "7138488bbdaf3abf6fd924bb1a8589e5ab613a8fb051df498719344ce7e62b0d" + }, + { + "path": "research/p104-native-channel/inputs/LOWRANK-WITNESS.json", + "usage": "input", + "git_blob": "86beaf424e9f0f800ae3a62797d94ec9386b7706", + "sha256": "0f541bef7f19fdeffd67157684e9f03d785f42c89973632f508fc1a0452b580e" + } + ] +} diff --git a/research/p104-all-pair-consumer-budget/TASK.json b/research/p104-all-pair-consumer-budget/TASK.json new file mode 100644 index 0000000000..276339a810 --- /dev/null +++ b/research/p104-all-pair-consumer-budget/TASK.json @@ -0,0 +1,88 @@ +{ + "schema_version": 1, + "task_id": "p104-side-correction", + "priority_revision": 5, + "base_commit": "0374b3e6a532dac112813523d605288c416418c1", + "original_card": { + "id": "p104-side-correction", + "question": "Which unresolved physical correction, endpoint transport or hosting obligation in a pinned P104 follow-up can be closed or decisively rejected?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/p104-native-channel/README.md", + "research/p104-native-channel/PROOF.md", + "docs/research/community-efficient1000-review.md" + ], + "methods": [ + "Construct one side-correction word at an explicit chronological cut with the needed frames still available.", + "Derive a lower bound on the side correction and hosting costs that decides whether this channel can beat the selected budget." + ], + "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_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read the P104 row in research-family-status.md and its exact pending source heads before choosing a task. #1991 is the reviewed channel; #2586 is a pending physical dual with explicit added transport costs, not an admitted supplier.", + "scope": "Source-bound orientation only. Read the named package and review before relying on its local evidence; this command is not its replay or supplier admission." + }, + "first_experiment": "Check live claims, pin the chosen follow-up and reproduce only the evidence needed for one unresolved obligation. Compare its complete correction/transport/hosting invoice with the target budget; test legal chronological access. Do not rebuild #1991 or assume #2586 has solved global admission.", + "bottleneck_link": "Completing an already realized changed channel tests a concrete construction opportunity, instead of refining the incumbent packing. A positive local result still needs global and all-size admission.", + "allowed_variations": [ + "One correction factorization, one chronological cut, or one explicit hosting obstruction.", + "A changed correction schedule with an updated full bill and native frame contract." + ], + "scope_change_triggers": [ + "Recompiling the already certified low-rank channel without closing a new obligation.", + "Treating a pending ancestor, local histogram or unpriced side correction as an admitted global supplier.", + "Repeating a correction or physical conversion already supplied by a pending follow-up without adding independent coverage or a different unresolved obligation." + ], + "overlap_terms": [ + "P104", + "I-G/2", + "side correction", + "native channel", + "1972", + "1991", + "2586", + "endpoint transport", + "physical dual", + "relay composition" + ] + }, + "scope_status": "refined", + "actual_scope": "Prove or falsify an all-pair-count conditional budget obstruction for PR2458 forward and PR2712 dual profiles in the retained paired-chain template, granting 416 free dual rank units and all missing corrections free.", + "scope_change_reason": "The current handoff is complete-consumer affordability. Jose Manuel's four-pair Discussion screen leaves whether changing pair count and caller width escapes it unresolved. This audit covers every integer pair count, not another local endpoint fusion.", + "bottleneck_link": "Decide whether changing the stage count or adding fully paid banks can make these exact partial P104 profiles competitive under the named coverage law, before further dependent construction.", + "budget_minutes": 60, + "stop_rule": "Stop after a source-bound proof for every p>=1 and meaningful controls, a failed inequality, or a prior all-p result; do not extend the local word or change the consumer contract.", + "outcome": "negative-result", + "outcome_detail": "Conditional all-p obstruction, including every finite number of fully paid banks. No supplier or kappa change.", + "evidence": "README.md proof, RESULT.json exact bounds, verify.py independent invoice recount and six finite cases plus an affine infinite tail, test_verify.py behavioral controls.", + "author": "Nick Petalas", + "ai_assistance": "No independent human review or formal-kernel validation is claimed.", + "scope_key": "P104/PR2458-PR2712/all-paired-chain-widths/optimistic-consumer-moment", + "predecessor_heads": {"2458": "3170afd2fc13a990bfe28f5ab6421bcda4ffd0f6", "2712": "afa5d6649460dcdb93489babd74f0ee9d01a4911"}, + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/2619#discussioncomment-18956430", + "predecessor_finding": "https://github.com/CrocSwap/integer-mult-bounds/discussions/2619#discussioncomment-18955566", + "task_selection": {"nonce": "196b9ea8ccc276b723cff7a17d43810f", "track": "complex-mechanisms", "choice": "p104-side-correction", "method": "Derive a lower bound on correction and hosting costs deciding whether the pinned channel can beat the selected budget."}, + "family_decision": "Pause this exact profile/coverage/template expansion: no pair count or finite fully paid-bank addition can help. Reopen with a changed profile, paid-work sharing or a changed consumer with a justified replacement coverage law.", + "obligation_ledger": {"proved": ["Literal local transport invoice recount", "Conditional moment lower bound for every p>=1", "416-unit rank-discount domination", "Finite fully paid banks cannot repair the strict deficit"], "constructive_upper_bounds": [], "unknown": ["Actual physical coverage and compatible owners", "Native realization of remaining 102 corrections", "Physical precision and tape realization", "All-size admission"], "favorable_grants": ["All missing corrections free without changing endpoint progress", "3014 progress units per call", "416 rank units free per dual", "Idle ranks allowed to equal full caller width", "Other nonnegative implementation costs omitted"]}, + "freshness": {"upstream_commit": "7b39515117fe26e75d16c268877391f1bdaa5640", "priority_revision": 5, "checked_at_utc": "2026-10-15T19:21:17Z", "open_pr_snapshot_utc": "2026-10-15T19:17:19.484244+00:00", "discussion_snapshot_utc": "2026-10-15T19:19:25.594251+00:00", "coverage": "751 open PRs and 1368 Discussion records, complete pagination. Metadata and local notes only, not arbitrary diffs or a novelty guarantee.", "compatibility": "Canonical main advanced through unrelated retained research/review updates. Guidance, priority revision, selected record, package runner and every live source are byte-identical to the scientific base. PR2458 and PR2712 heads remain unchanged. Targeted all-term searches distinguish the credited p=4 finding, local fusion budgets and monotone-history relaxations."}, + "validation": {"registered_python": "CPython 3.12.15", "optimized_python": "CPython 3.13.5", "package_tests": 11, "research_workflow_tests": 70, "research_workflow_skips": 2, "diagnostics": "ruff check --select E,F,I,UP,B", "review": "Separate local mathematical and source-binding passes; no subagent tool is exposed. The p=1 auxiliary-bank clamp was corrected and its boundary is covered by literal tests. No independent human, hosted-CI or formal-kernel validation is claimed."}, + "open_questions": [ + { + "question": "Can a changed consumer provide additional unpaid-coordinate or endpoint-progress credit without repaying it in restoration?", + "why_it_matters": "Changing pair count and fully paid bank capacity alone cannot make these profiles competitive.", + "first_step": "Specify actual physical entry/exit boundaries and derive a replacement coverage law before another profile optimization.", + "blocked_by": "No compatible physical consumer or revised progress/coverage proof is supplied." + }, + { + "question": "Can a complete changed forward and dual profile escape this screen?", + "why_it_matters": "Current forward words correct only two rows, and even granting the other corrections free fails this template.", + "first_step": "Recount both directions with every changed correction and restoration cost, then repeat the favorable consumer screen.", + "blocked_by": "The exact new completed word and boundary contract are not available." + } + ] +} diff --git a/research/p104-all-pair-consumer-budget/VERIFY.json b/research/p104-all-pair-consumer-budget/VERIFY.json new file mode 100644 index 0000000000..3acd0cb66c --- /dev/null +++ b/research/p104-all-pair-consumer-budget/VERIFY.json @@ -0,0 +1,31 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/community-frontier1094-audit/ASSEMBLY.json", + "research/larger-gain/geometry/stage_relaxation.py", + "research/larger-gain/stages/screen_stages.py", + "research/p104-terminal-correction-floor/README.md", + "research/p104-native-channel/inputs/LOWRANK-WITNESS.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Source-bound transport profiles, selected benchmark, six exact finite bounds and affine infinite-tail certificate." + }, + { + "argv": ["{python}", "-I", "-O", "-B", "{package}/test_verify.py"], + "timeout_seconds": 120, + "checks": "Literal p=4 fixture, logarithm and rank controls, weaker-saving non-rejection, optimized Git-free CLI, recompression and malformed source/receipt controls." + } + ] +} diff --git a/research/p104-all-pair-consumer-budget/inputs/PR2458-CIRCUIT.json.gz b/research/p104-all-pair-consumer-budget/inputs/PR2458-CIRCUIT.json.gz new file mode 100644 index 0000000000..6e915105c8 Binary files /dev/null and b/research/p104-all-pair-consumer-budget/inputs/PR2458-CIRCUIT.json.gz differ diff --git a/research/p104-all-pair-consumer-budget/inputs/PR2458-README.md b/research/p104-all-pair-consumer-budget/inputs/PR2458-README.md new file mode 100644 index 0000000000..979be231f8 --- /dev/null +++ b/research/p104-all-pair-consumer-budget/inputs/PR2458-README.md @@ -0,0 +1,149 @@ +# Native binding for the P104 two-target correction + +PR2445's correction of **Y0 and Y1** now has a finite native Clifford +certificate for all **236 added transport occurrences**. Its **161 distinct +frame pairs** are absent from the original channel's 740-pair certificate. +Every pair has an exact forward recipe and an exact adjoint recipe, including +global phase, with the inherited positive-child rank. A separately written +checker composes the forward recipes with the retained native channel and +checks every one of **128,164 boundary coefficients over 358 arbitrary inputs**. + +This closes the finite forward native-binding handoff in +[PR2445](https://github.com/CrocSwap/integer-mult-bounds/pull/2445), exact head +`6def43ad673b91dbd491389964d1dcd059bf2ac2`. The two-target construction and +78-lifetime minimum belong to that predecessor. No new helper minimum, complete +supplier, global recursive invoice, all-size proof or kappa is claimed here. + +## Exact covered operator + +Fix the nine-bit physical label isometry and canonical chart representatives +`Gamma_W` from [PR1991's retained channel](../p104-native-channel/README.md). +For every register r, maintain `physical_r = Gamma_W(r) logical_r`. +A transport A to B is exactly `Gamma_B Gamma_A^-1`; a scalar ADD or COPY uses +one identical current chart on both operands. The checker binds exact +representatives, not just equal binary spans. + +For a logical boundary matrix S, induction gives the physical block map + +`physical_r(final) = sum_s S[r,s] Gamma_final(r) Gamma_initial(s)^-1 physical_s(initial)`. + +The source and target intrinsic endpoint adapters are unchanged and rechecked. +The forward scalar matrix is checked entry by entry: Y0 and Y1 acquire their +matching source, the other 102 targets acquire the original G/2 row, all 104 +sources restore logically, and all **150 arbitrary dirty helpers** restore +logically. This includes the original 72 and the 78 added helpers. Their +physical arrays change with the prescribed endpoint charts: in particular, +an added helper starts at ZERO and finishes at FULL. Logical restoration does +not assert bytewise or physical-array equality across that change. + +The original eight private-copy lifetimes are retained. Their inherited +owned-copy discard contract is used explicitly; the checker does not pretend +the live copy was reversibly returned to zero. + +The independent native interpreter checks all 18 signed Pauli images and the +complete exact Gaussian-dyadic image of basis zero for each of the **322 +forward/adjoint recipes**. Equal Pauli conjugations determine a Clifford up +to scalar phase, and equality on this nonzero state fixes that phase. Thus +the comparison establishes each complete 512-dimensional operator, rather +than a sampled input test. [REVIEW.md](REVIEW.md) states the proof and reuse +boundary. This is finite exact computation plus a written composition argument, +not a formal proof-kernel result. + +**The adjoint recipes cover individual transports only.** They do not execute +or certify the inverse transpose of the complete program with COPY/discard. +The complete backward interface remains a separate obligation. + +## Accounting + +The newly compiled pairs do not alter the predecessor's literal word or costs. + +| Added quantity | Exact value | +| --- | ---: | +| Nested transport occurrences | 236 | +| Distinct directed frame pairs | 161 | +| Forward plus adjoint native recipes | 322 | +| Added profile | 142 H1 + 16 H2 + 18 H6 + 60 H7 | +| Added boundary rank mass | 702 | +| Added scalar ADDs / helper lifetimes | 440 / 78 | + +The full forward word has 4,734 events, 1,646 transport occurrences and rank +mass 3,070. Every native recipe contains one positive Fourier-type child of +its declared rank and two rank-zero Gaussian monomial adapters. Rank-zero +adapters still perform address/phase work. This table is a finite operator and +local rank invoice; it does not price physical scalar lowering, adapter routing, +recursive owners, idle/residual children, tape, approximate arithmetic or the +all-size compiler. Boundary rank progress is not automatically recursive excess. + +## Reproduce + +Python 3.12, standard library. Default verification reads fixed evidence and +never generates a missing certificate. It imports no producer or Clifford +compiler. The optional regeneration runs the credited compiler in temporary +storage and compares the **complete decompressed mathematical payload**. + +```sh +python3.12 -I -O -B research/p104-two-target-native/verify.py --regenerate +python3.12 -I -O -B research/p104-two-target-native/test_verify.py +python3.12 -B scripts/research_package.py --package research/p104-two-target-native +``` + +Expected marker: `PASS_P104_TWO_TARGET_NATIVE no_new_kappa`. +The new checker requires ten semantic fault controls and accepts two equivalent +presentations. The behavioral suite checks missing evidence, source drift, +malformed receipts, exclusive output, a Git-free read-only export and a changed +gzip header. It also removes only the exact-phase predicate in memory and +requires the phase control suite to fail, establishing defect sensitivity. + +[RESULT.json](RESULT.json) is the fixed exact receipt. +[SOURCES.json](SOURCES.json) pins every runtime input by Git blob and SHA256. +The literal predecessor circuit is the only vendored data; the existing native +channel, compiler and independent interpreter remain unchanged in their own +package. All required inputs are declared in [VERIFY.json](VERIFY.json), so a +Git-free export consists of this package and those six runtime files at their +listed relative paths. `--out` accepts only a new file. The separate explicit +`--emit-initial-result --out PATH` option is for authoring, not default checking. + +The inherited native checker is replayed, not claimed as a new independent +implementation. It proves all inherited transport operators via signed Pauli +and exact phase checks; this package does not rerun its optional 4,096 private +basis-column enumeration. No selected-frontier cold replay, hosted CI result, +human review or proof-assistant verification is claimed by these local checks. + +## Sources, credit and scope + +Scientific base: `0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2`, priority revision 4. +The selected record is unchanged, SHA256 +`10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32`. +The literal PR2445 circuit SHA256 is +`c34d94128decc426e7528302ab2570967293a1b293f184fdd89fd376addd61f9`. +Fresh overlap and the changed catalogue scope are recorded in [TASK.json](TASK.json). + +Credit Ross Richardson / PR2445 for the complete two-target logical word and +sharing proof; commdata2338 / PR2393 for the one-target acquisition proof and +sharing handoff; Hiroki Kumazaki / PR2353 and Philippe Van Velzen for the relay +model. Chafik Boukhalfa / PR1991 supplies native channel lowering and the +physical label binding, Rohan Arun / PR1972 the original scalar/frame channel, +Adam Gall / PR1940 its schedule, Josie Elliston / PR1071 the fixture, and Ali +Romman / PR1125 and PR1862 the retained geometry/native interpreter lineage. +The exact compiler is retained through icekylinx / PR531 and the +PR523/514/507/425/433 ancestry. Original notices remain under +`research/p104-native-channel/notices/`; no predecessor file is modified. + +Prepared for Ross Richardson with substantial OpenAI Codex assistance in +implementation, derivation and writing, including a separate mathematical +specialist who wrote the new native-binding/forward checker without importing +the producer. No blind or independent human review is claimed. New material +and the retained literal circuit are Apache-2.0. + +## Open next questions + +First specify and emit the complete dual program under its actual private-copy +contract, then check scalar direction, chart adapters and every private lifetime. +Transport adjoints alone do not settle this. + +For a full correction, name a third target and test collector rank and chronology +before extending the word. The other 102 corrections, actual global hosting and +idle/residual invoice, physical scalar/address costs, precision/tape and all-size +admission remain the gates to any supplier or exponent claim. Structured first +steps and blockers are in TASK.json; this package closes only its fixed finite +forward native-binding question. diff --git a/research/p104-all-pair-consumer-budget/inputs/PR2712-README.md b/research/p104-all-pair-consumer-budget/inputs/PR2712-README.md new file mode 100644 index 0000000000..a1890be765 --- /dev/null +++ b/research/p104-all-pair-consumer-budget/inputs/PR2712-README.md @@ -0,0 +1,89 @@ +# P104 shared-chart retiming + +This source-bound construction crosses two early ADD stars in the pending +[PR2662](https://github.com/CrocSwap/integer-mult-bounds/pull/2662) word by +moving **both operands** to a common earlier chart. It retains every ADD +coefficient, all 358 independent input/output fields and all dirty-helper +restoration. Four direct positive children replace four pairs of transports: + +| Quantity | PR2662 | This word | +| --- | ---: | ---: | +| Positive transports | 1,942 | 1,938 | +| Total events | 5,270 | 5,266 | +| Rank mass | 3,542 | 3,542 | +| Scalar ADDs | 3,104 | 3,104 | +| Restored dirty helpers | 150 | 150 | +| Owned zero/zero-erase lifetimes | 8 | 8 | + +The changes are two `H1+H1 -> H2`, one `H1+H4 -> H5` and one +`H1+H6 -> H7`. The local child sum strictly decreases for every exponent +`0 46 for r in proof["finite"]) + ) + self.assertEqual(proof["tail_from_pairs"], 8) + self.assertGreater(Q(proof["tail_slope_lower"]), Q(2, 3)) + self.assertGreater(Q(proof["tail_intercept_lower"]), 76) + + def test_paid_bank_clamping_boundary(self): + proof = VERIFY.prove(VERIFY.FORWARD, VERIFY.DUAL) + self.assertEqual(proof["p1_any_paid_banks_mass_excess_lower"], 16) + for banks, expected_excess in [ + (0, 4066), + (161, 41), + (162, 16), + (163, 16), + (10**12, 16), + ]: + idle = max(0, -4050 + 25 * banks) + self.assertEqual(9266 + idle - 25 * (208 + banks), expected_excess) + for pairs in range(2, 8): + width, roles = 16 * pairs + 9, 208 * pairs + for banks in (0, 1, 1000): + idle = (width - 1) * roles + width * banks - (2 * pairs + 1) * 3014 + paid = (pairs + 1) * 3070 + pairs * 3126 + self.assertEqual(paid + idle - width * (roles + banks), 56 - 40 * pairs) + + def test_exact_log_and_discount_fixtures(self): + self.assertEqual(VERIFY.log_lower(Q(1)), 0) + self.assertEqual(VERIFY.log_lower(Q(2)), Q(693147, 1_000_000)) + self.assertEqual(VERIFY.log_lower(Q(137)), Q(614347, 125000)) + # Independently enclose every integer-rank deletion at saving 1/2. + # The README proves all savings; this is a finite fixture of that lemma. + scale = 1_000_000 + for rank in range(1, 9): + root_floor = isqrt(rank * scale * scale) + root_ceil = root_floor + (root_floor * root_floor != rank * scale * scale) + for delta in range(1, rank + 1): + rest_floor = isqrt((rank - delta) * scale * scale) + self.assertLessEqual(Q(root_ceil - rest_floor, scale), delta) + with self.assertRaisesRegex(ValueError, "discount bound"): + VERIFY.discounted(VERIFY.DUAL, 2000) + with self.assertRaisesRegex(ValueError, "log domain"): + VERIFY.log_lower(Q(138)) + + def test_semantic_rejections(self): + understated = dict(VERIFY.DUAL) + understated[1] -= 1 + with self.assertRaisesRegex(ValueError, "source masses"): + VERIFY.prove(VERIFY.FORWARD, understated) + base_slope, base_intercept = VERIFY.coefficients( + VERIFY.FORWARD, VERIFY.discounted(VERIFY.DUAL), 41 + ) + self.assertLess(-24 + Q(1, 10000) * (2 * base_slope + base_intercept), 0) + with self.assertRaisesRegex(ValueError, "finite p=2"): + VERIFY.prove(VERIFY.FORWARD, VERIFY.DUAL, Q(1, 10000)) + with self.assertRaisesRegex(ValueError, "saving domain"): + VERIFY.prove(VERIFY.FORWARD, VERIFY.DUAL, Q(0)) + with self.assertRaisesRegex(ValueError, "transport rank"): + VERIFY.transport_profile([["transport", "r", [], [1, 2], 1]]) + with self.assertRaisesRegex(ValueError, "nonnested"): + VERIFY.transport_profile([["transport", "r", [1], [2], 1]]) + slope, _ = VERIFY.coefficients( + VERIFY.FORWARD, VERIFY.discounted(VERIFY.DUAL), 73 + ) + self.assertLess(VERIFY.KAPPA * slope - 40, 0) + self.assertEqual( + VERIFY.transport_profile([["transport", "r", [3, 1], [2, 1, 4], 1]]), + {1: 1}, + ) + + +class ArtifactControls(unittest.TestCase): + """Run the public optimized CLI from a Git-free export, including faults.""" + + def setUp(self): + self.temp = tempfile.TemporaryDirectory() + self.addCleanup(self.temp.cleanup) + self.root = Path(self.temp.name) + self.package = self.root / "research/p104-all-pair-consumer-budget" + shutil.copytree( + PACKAGE, self.package, ignore=shutil.ignore_patterns("__pycache__") + ) + sources = json.loads((PACKAGE / "SOURCES.json").read_text()) + for row in sources["files"]: + if row["usage"] == "input": + destination = self.root / row["path"] + destination.parent.mkdir(parents=True, exist_ok=True) + shutil.copyfile(VERIFY.ROOT / row["path"], destination) + + def cli(self): + return subprocess.run( + [sys.executable, "-I", "-O", "-B", str(self.package / "verify.py")], + cwd=self.root, + text=True, + capture_output=True, + timeout=30, + check=False, + ) + + def test_git_free_positive_and_recompression(self): + result = self.cli() + self.assertEqual(result.returncode, 0, result.stderr) + self.assertIn("PASS_P104_ALL_PAIR_CONSUMER_BUDGET", result.stdout) + path = self.package / "inputs/PR2712-WORD.json.gz" + raw = gzip.decompress(path.read_bytes()) + path.write_bytes(gzip.compress(raw, compresslevel=1, mtime=123456789)) + result = self.cli() + self.assertEqual(result.returncode, 0, result.stderr) + + def test_changed_source_rejects(self): + path = self.package / "inputs/PR2458-CIRCUIT.json.gz" + data = json.loads(gzip.decompress(path.read_bytes())) + data["source_witness_sha256"] = "0" * 64 + path.write_bytes(gzip.compress(json.dumps(data).encode())) + result = self.cli() + self.assertNotEqual(result.returncode, 0) + self.assertIn("PR2458-CIRCUIT", result.stderr) + + def test_changed_receipt_rejects(self): + path = self.package / "RESULT.json" + data = json.loads(path.read_text()) + data["proof"]["tail_from_pairs"] = 9 + path.write_text(json.dumps(data)) + result = self.cli() + self.assertNotEqual(result.returncode, 0) + self.assertIn("receipt mismatch", result.stderr) + + def test_typed_receipt_rejects(self): + path = self.package / "RESULT.json" + data = json.loads(path.read_text()) + data["schema_version"] = True + path.write_text(json.dumps(data)) + result = self.cli() + self.assertNotEqual(result.returncode, 0) + self.assertIn("receipt mismatch", result.stderr) + + def test_duplicate_key_rejects(self): + path = self.package / "RESULT.json" + path.write_text('{"schema_version":1,"schema_version":2}') + result = self.cli() + self.assertNotEqual(result.returncode, 0) + self.assertIn("duplicate key", result.stderr) + + +if __name__ == "__main__": + unittest.main() diff --git a/research/p104-all-pair-consumer-budget/verify.py b/research/p104-all-pair-consumer-budget/verify.py new file mode 100644 index 0000000000..5bc000b367 --- /dev/null +++ b/research/p104-all-pair-consumer-budget/verify.py @@ -0,0 +1,271 @@ +#!/usr/bin/env python3 +"""Exact conditional P104 consumer screen for every positive pair count.""" + +import argparse +import gzip +import hashlib +import json +from collections import Counter +from fractions import Fraction as Q +from pathlib import Path + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] +KAPPA = Q(836330098538459, 500000000000000000) +FORWARD = {1: 1216, 2: 74, 3: 86, 4: 104, 5: 48, 6: 42, 7: 68, 8: 8} +DUAL = {1: 1498, 2: 60, 3: 74, 4: 92, 5: 58, 6: 56, 7: 92, 8: 8} +PROGRESS = 104 * 8 + 104 * 8 + 150 * 9 +MAX_JSON_BYTES = 2_000_000 + + +def require(condition, message): + """Keep proof checks enabled under Python -O.""" + if not condition: + raise ValueError(message) + + +def unique_object(pairs): + """Reject duplicate JSON keys rather than silently accepting a last value.""" + result = {} + for key, value in pairs: + require(key not in result, f"duplicate key: {key}") + result[key] = value + return result + + +def load_json(path, compressed=False): + """Read bounded JSON, including bounded decompression of retained words.""" + require(path.stat().st_size <= MAX_JSON_BYTES, f"oversized input: {path}") + opener = gzip.open if compressed else open + with opener(path, "rb") as stream: + raw = stream.read(MAX_JSON_BYTES + 1) + require(len(raw) <= MAX_JSON_BYTES, f"oversized payload: {path}") + return json.loads(raw, object_pairs_hook=unique_object), raw + + +def authenticate(): + """Authenticate live sources and original retained Git blobs without Git.""" + sources, _ = load_json(PACKAGE / "SOURCES.json") + require(len(sources["files"]) <= 8, "live source inventory bound") + for row in sources["files"]: + if row["usage"] == "input": + path = ROOT / row["path"] + require(path.stat().st_size <= MAX_JSON_BYTES, "live input size") + raw = path.read_bytes() + require(hashlib.sha256(raw).hexdigest() == row["sha256"], row["path"]) + predecessors, _ = load_json(PACKAGE / "PREDECESSORS.json") + require(len(predecessors["files"]) == 4, "predecessor inventory") + for row in predecessors["files"]: + path = PACKAGE / row["path"] + require(path.stat().st_size <= MAX_JSON_BYTES, "predecessor container size") + opener = gzip.open if path.suffix == ".gz" else open + with opener(path, "rb") as stream: + raw = stream.read(MAX_JSON_BYTES + 1) + require(len(raw) <= MAX_JSON_BYTES, "predecessor payload size") + require(hashlib.sha256(raw).hexdigest() == row["raw_sha256"], row["path"]) + blob = b"blob " + str(len(raw)).encode() + b"\0" + raw + require( + hashlib.sha1(blob, usedforsecurity=False).hexdigest() == row["git_blob"], + "original Git blob", + ) + + +def binary_rank(vectors): + """Eliminate at most eighteen vectors in the fixed nine-bit label space.""" + require(len(vectors) <= 18, "frame vector bound") + pivots = [0] * 9 + for value in vectors: + require(type(value) is int and 0 < value < 512, "binary frame vector") + for bit in range(8, -1, -1): + if value & (1 << bit): + if pivots[bit]: + value ^= pivots[bit] + else: + pivots[bit] = value + break + return sum(value != 0 for value in pivots) + + +def transport_profile(events): + """Recount nested-frame ranks, not just the declared rank field.""" + require(len(events) <= 6000, "event bound") + profile = Counter() + for event in events: + if event[0] != "transport": + continue + require(len(event) == 5, "transport shape") + before, after, declared = event[2:] + left, right = binary_rank(before), binary_rank(after) + require(binary_rank(before + after) == max(left, right), "nonnested transport") + rank = abs(right - left) + require( + type(declared) is int and rank == declared and 1 <= rank <= 8, + "transport rank", + ) + profile[rank] += 1 + return dict(sorted(profile.items())) + + +def endpoint_progress(document): + """Recount net persistent frame progress, without admitting owner hosting.""" + initial, final = document["initial_frames"], document["final_frames"] + require(initial.keys() == final.keys(), "persistent endpoint inventory") + require(len(initial) <= 358, "persistent role bound") + return sum(binary_rank(frame) for frame in final.values()) - sum( + binary_rank(frame) for frame in initial.values() + ) + + +def source_profiles(): + """Retain predecessor native correctness; independently recount its invoice.""" + core, raw = load_json( + ROOT / "research/p104-native-channel/inputs/LOWRANK-WITNESS.json" + ) + correction, _ = load_json( + PACKAGE / "inputs/PR2458-CIRCUIT.json.gz", compressed=True + ) + dual, _ = load_json(PACKAGE / "inputs/PR2712-WORD.json.gz", compressed=True) + require( + hashlib.sha256(raw).hexdigest() == correction["source_witness_sha256"], + "core binding", + ) + added = correction["insertions"] + require(len(added) == 2, "two forward insertion cuts") + forward = Counter(transport_profile(core["program"])) + for insertion in added: + forward.update(transport_profile(insertion["events"])) + require(dict(forward) == FORWARD, "forward profile") + require(transport_profile(dual["program"]) == DUAL, "dual profile") + require( + not core["initial_frames"].keys() & correction["initial_frames"].keys(), + "disjoint added forward roles", + ) + require( + endpoint_progress(core) + endpoint_progress(correction) == PROGRESS, + "forward endpoint progress", + ) + require(endpoint_progress(dual) == PROGRESS, "dual endpoint progress") + return dict(sorted(forward.items())), dict(DUAL) + + +def log_lower(value): + """128-term positive atanh sum, rounded down to six decimal places.""" + require(type(value) is Q and Q(1) <= value <= Q(137), "log domain") + require(value.denominator <= 8, "log denominator bound") + t = (value - 1) / (value + 1) + term, total = t, Q(0) + for index in range(128): + total += 2 * term / (2 * index + 1) + term *= t * t + return Q((total * 1_000_000).__floor__(), 1_000_000) + + +def mass(profile): + return sum(rank * count for rank, count in profile.items()) + + +def discounted(dual, units=416): + """Removing H1 grants at least any integer-rank deletion of the same mass.""" + require(type(units) is int and 0 <= units <= dual[1], "discount bound") + result = dict(dual) + result[1] -= units + return result + + +def coefficients(forward, dual, width): + """L(p) >= A*p+B once the caller width is at least this fixed width.""" + logs = {rank: log_lower(Q(width, rank)) for rank in range(1, 9)} + slope = sum((forward[r] + dual[r]) * r * logs[r] for r in logs) + intercept = sum(forward[r] * r * logs[r] for r in logs) + return slope, intercept + + +def prove(forward, dual, rate=KAPPA): + """Finite base cases and an affine infinite tail, never a large-p census.""" + require(type(rate) is Q and Q(0) < rate < Q(1), "saving domain") + relaxed = discounted(dual) + require(mass(forward) == 3070 and mass(relaxed) == 3126, "source masses") + # All p have mass excess 56-40p before clamping negative idle to zero. + require(mass(forward) - PROGRESS == 56, "mass intercept") + require(mass(forward) + mass(relaxed) - 2 * PROGRESS - 208 == -40, "mass slope") + p1_excess = 2 * mass(forward) + mass(relaxed) - 25 * 208 + require(p1_excess == 4066, "p=1 without banks mass test") + # I_B >= (m-1)W+mB-(2p+1)C gives excess 56-40p even when clamped. + p1_bank_excess = 2 * mass(forward) + mass(relaxed) - 3 * PROGRESS - 208 + require(p1_bank_excess == 16, "p=1 arbitrary fully paid banks mass test") + finite = [] + for pairs in range(2, 8): + width, roles = 16 * pairs + 9, 208 * pairs + idle = (width - 1) * roles - (2 * pairs + 1) * PROGRESS + require(idle >= 0, "nonnegative idle base case") + slope, intercept = coefficients(forward, relaxed, width) + numerator = 56 - 40 * pairs + rate * (slope * pairs + intercept) + require( + numerator > 46, f"finite p={pairs} does not reject by the stated margin" + ) + finite.append( + { + "pairs": pairs, + "width": width, + "idle_mass": idle, + "excess_numerator_lower": str(numerator), + } + ) + slope, intercept = coefficients(forward, relaxed, 137) + tail_slope, tail_intercept = rate * slope - 40, 56 + rate * intercept + require(tail_slope > Q(2, 3) and tail_intercept > 76, "infinite-tail positivity") + return { + "p1_mass_excess": p1_excess, + "p1_any_paid_banks_mass_excess_lower": p1_bank_excess, + "finite": finite, + "tail_from_pairs": 8, + "tail_slope_lower": str(tail_slope), + "tail_intercept_lower": str(tail_intercept), + "tail_log_lower": {str(r): str(log_lower(Q(137, r))) for r in range(1, 9)}, + } + + +def run(): + authenticate() + forward, dual = source_profiles() + assembly, _ = load_json( + ROOT / "research/community-frontier1094-audit/ASSEMBLY.json" + ) + require(Q(assembly["kappa"]) == KAPPA, "selected benchmark binding") + result = prove(forward, dual) + return { + "schema_version": 1, + "status": "PASS_P104_ALL_PAIR_CONSUMER_BUDGET", + "benchmark_kappa": str(KAPPA), + "forward_profile": forward, + "dual_profile": dual, + "forgiven_dual_rank_units": 416, + "granted_progress_per_call": PROGRESS, + "proof": result, + "scope": ( + "Conditional paired-chain coverage; all integer p>=1 and finite fully " + "paid banks. No supplier or new kappa." + ), + } + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument( + "--write", action="store_true", help="replace this package's RESULT.json" + ) + args = parser.parse_args() + result = run() + encoded = json.dumps(result, indent=2, sort_keys=True) + "\n" + if args.write: + written = (PACKAGE / "RESULT.json").write_text(encoded) + require(written == len(encoded), "incomplete receipt write") + else: + expected, _ = load_json(PACKAGE / "RESULT.json") + expected_encoding = json.dumps(expected, indent=2, sort_keys=True) + "\n" + require(encoded == expected_encoding, "receipt mismatch") + print(result["status"] + " all_p>=1 finite=6 tail_from=8 no_new_kappa") + + +if __name__ == "__main__": + main()