From 637106d1abd87416960502d3368b99f0edc7dacd Mon Sep 17 00:00:00 2001 From: Matarener Date: Sat, 17 Oct 2026 23:42:57 +0300 Subject: [PATCH 1/2] Independently re-solve PR2979 fixed-capacity stage caps and price each stage-one group alone Co-Authored-By: Claude Opus 5.5 (1M context) --- research/rank7-stage-cap-resolve/README.md | 112 ++++ research/rank7-stage-cap-resolve/RESULT.json | 557 ++++++++++++++++++ research/rank7-stage-cap-resolve/SOURCES.json | 36 ++ research/rank7-stage-cap-resolve/TASK.json | 66 +++ research/rank7-stage-cap-resolve/VERIFY.json | 25 + research/rank7-stage-cap-resolve/capsolve.py | 279 +++++++++ research/rank7-stage-cap-resolve/run.py | 162 +++++ research/rank7-stage-cap-resolve/verify.py | 22 + 8 files changed, 1259 insertions(+) create mode 100644 research/rank7-stage-cap-resolve/README.md create mode 100644 research/rank7-stage-cap-resolve/RESULT.json create mode 100644 research/rank7-stage-cap-resolve/SOURCES.json create mode 100644 research/rank7-stage-cap-resolve/TASK.json create mode 100644 research/rank7-stage-cap-resolve/VERIFY.json create mode 100644 research/rank7-stage-cap-resolve/capsolve.py create mode 100644 research/rank7-stage-cap-resolve/run.py create mode 100644 research/rank7-stage-cap-resolve/verify.py diff --git a/research/rank7-stage-cap-resolve/README.md b/research/rank7-stage-cap-resolve/README.md new file mode 100644 index 0000000000..397276eb64 --- /dev/null +++ b/research/rank7-stage-cap-resolve/README.md @@ -0,0 +1,112 @@ +# Independent re-solve of PR #2979's fixed-capacity stage caps + +**Partial positive audit. No new κ, no supplier admission.** The selected +result stays κ = 0.001672660197076918. + +[PR #2979](https://github.com/CrocSwap/integer-mult-bounds/pull/2979) +(head `be191346`) certifies its fixed-capacity packing caps from stored optimal +bases. This package re-solves the same relaxation **without any stored basis**: +its own pattern enumeration, its own two-phase simplex (numpy floats, Bland's +rule) to locate a basis, then an exact Fractions inverse and `mpmath.iv` +interval enclosures for the root and every reduced cost. No code from the +audited package is imported or run. The relaxation model is re-implemented from +its docstring (`tools/relax.py`), so this check shares the model, not the code. + +## Result + +All four shipped brackets are reproduced exactly on the 10⁻²⁵ grid, with the same +idle histograms: + +| words | cap (lower, 10⁻²⁵ grid) | patterns | basis identical to shipped | +|---|---|---:|---| +| parent (PR #2942) | 0.0017228172707428495209099 | 1,163 | no (alternative optimum) | +| stage 1 | 0.0017262265796413098725813 | 2,551 | yes | +| stage 2 | 0.0017278107473204236839366 | 2,551 | no (alternative optimum) | +| final | 0.001729035764875516181444 | 2,551 | no (alternative optimum) | + +Three optimal bases differ from the shipped ones but give the same idle profile +and root, so the LP is degenerate there. The cap does not depend on the choice. + +**New coverage: each stage-one group is priced alone with a certified cap.** +The source's single-versus-joint argument uses an approximate width guide of +2,091,300 units per freed width unit, which [the frame audit](../rank7-joint-frame-audit/README.md) +notes is not a certified tariff. Here each group's change is applied alone to +the parent words and the cap is re-solved. Local deltas come from the frame audit's +`RESULT.json`; width changes come from #2979's README. + +| change on the parent | certified cap | vs parent cap | +|---|---|---:| +| V45 (4 helpers 8→7) | 0.001723368262870964843035 | +5.510e-7 | +| A (331 8→7; 450, 451, 508, 509 7→6) | 0.001723827833046096748741 | +1.0106e-6 | +| B (299 8→7; 448, 449, 484, 485 7→6) | same as A | +1.0106e-6 | +| C (452, 453, 532, 533 7→6) | 0.001723233298297402658193 | +4.160e-7 | +| D (454, 455, 556, 557 7→6) | same as C | +4.160e-7 | +| V45 edits, k = 0 lowered | 0.001720993847503899547275 | −1.8234e-6 | +| V45, k = 1 | 0.001721586837582425406796 | −1.2304e-6 | +| V45, k = 2 | 0.001722180236554225593479 | −6.370e-7 | +| V45, k = 3 | 0.001722774044842483001525 | −4.32e-8 | +| V45, k = 4 | equals the V45 row | +5.510e-7 | + +So each group raises the fixed-capacity cap by itself. For V45 only the full joint +lowering does so, and each of 1, 2 or 3 lowered endpoints lowers the cap. The +signs agree with the source's guide margins (−53,141, −27,770, −2,399, +22,972). +The five group gains sum to 3.4042e-6 against a joint stage-one rise of +3.4093e-6, so the groups are nearly additive under the cap as well. This answers +the open question in [rank7-v45-shipped-invoice](../rank7-v45-shipped-invoice/README.md): +the cap rise is attributable to each group, V45 included, within this relaxation. + +## Controls + +`RESULT.json` records five checks: + +- one basis column replaced (singular); +- the stage-2 basis applied to stage-1 inputs (infeasible); +- a feasible basis that is optimal at b = 1/2 (rejected by the reduced-cost sign); +- one extra rank-1 child (rejected by the rank-mass identity, 65,088 per replica); +- the stage-2 local profile with the final inventory, which gives a strictly lower cap. + +The inputs are authenticated by SHA256 before use. + +## Scope and limits + +This is the **fixed-inventory fractional relaxation** only. It ignores source +windows, per-call family exclusion and integrality, so a cap rise is an upper +bound on what a chronological fill can reach, not a realized saving. The group +controls fix the parent's other words and the source-declared width changes. +They use the frame audit's checked local deltas and do not re-derive frames. +The model's bin shape (`{8:672, 16:448, 32:448, 48:448}` per replica, one idle +child per bin) is the source's and is not re-justified here. Native/phase, +physical storage, precision, the literal T74 allocation and the outer release +remain unverified by this package. + +## Reproduce + +From the repository root, with numpy and mpmath (via sympy): + +```sh +python3.12 -B research/rank7-stage-cap-resolve/verify.py +python3 scripts/research_package.py --package research/rank7-stage-cap-resolve --check-only +``` + +`verify.py` recomputes everything (about 20 s) and requires byte-equal agreement +with `RESULT.json`. `python -B research/rank7-stage-cap-resolve/run.py` prints it. + +## Open next questions + +Does PR #2987's chronological owner and packing evidence attain these caps for the +stage-one words, or is part of each group's rise unreachable once windows and +family exclusions apply? This decides whether the certified cap rise becomes a +supplier saving. A first step is to price a chronological fill of the stage-one +inventory against the stage-one cap. Native/phase, storage and precision bindings +still block admission. Another lowering census is not justified by this result. + +## Credit + +Marius-Paul Dumitrean (#2979, #2942) supplied the construction, words and +relaxation model. Jeremy Kothe (#2957 rewrites and frame/cleanup lineage), Mason +Hale (#2917) and Jeremy Diviney (#2908) supplied the extraction chain. Nick +Petalas's independent frame audit supplied the checked group deltas used here. +Ross Richardson's #2960/#2974/#2987 audits and the retained relaxation lineage +(PR2857/PR2930) keep their credit. New check written by Claude (Anthropic) via +Claude Code, in a session donated by Mark. Apache-2.0. No human or formal review +is claimed. diff --git a/research/rank7-stage-cap-resolve/RESULT.json b/research/rank7-stage-cap-resolve/RESULT.json new file mode 100644 index 0000000000..29e4fd9c51 --- /dev/null +++ b/research/rank7-stage-cap-resolve/RESULT.json @@ -0,0 +1,557 @@ +{ + "controls": { + "extra_rank1_child": "stage-1 local profile with one extra rank-1 child: rejected (rank-mass identity 72*896 + 64*9 per replica)", + "feasible_basis_optimal_at_b_half": "feasible stage-1 basis optimal at b = 1/2, not at the cap: rejected (reduced cost not positive at hi for pattern (16, (0, 0, 0, 0, 2, 0), 0))", + "stage2_basis_on_stage1_inputs": "stage-2 optimal basis certified against stage-1 inputs: rejected (basic solution infeasible)", + "stage2_local_with_final_inventory": "lower cap 17278107473204236839367/10000000000000000000000000 < 432258941218879045361/250000000000000000000000", + "swapped_basis_column": "stage-1 basis with one column replaced: rejected (singular basis)" + }, + "inputs_sha256": { + "RELAX-CAP.json": "b272680de5842f7fd5f442cd0aeadfd317fe6af266ddee1a1e0738a919ba856e", + "RELAX-STAGES.json": "0e5ec700a191b668ba3d4b6d675f5c047d264b9a5109fc55fa92961b3fcb7d68", + "rank7-joint-frame-audit/RESULT.json": "994c11f0126f17ecbd0b8392d8904ad58aaede25c4c2347d3f35de6f839b2503" + }, + "ladder": { + "final": { + "basis": [ + { + "capacity": 8, + "count_per_replica": "672", + "widths": [ + 8 + ] + }, + { + "capacity": 16, + "count_per_replica": "448", + "widths": [ + 9, + 7 + ] + }, + { + "capacity": 32, + "count_per_replica": "35/4", + "widths": [ + 8, + 8, + 8, + 8 + ] + }, + { + "capacity": 32, + "count_per_replica": "20", + "widths": [ + 9, + 8, + 8, + 7 + ] + }, + { + "capacity": 32, + "count_per_replica": "144", + "widths": [ + 9, + 9, + 8, + 6 + ] + }, + { + "capacity": 32, + "count_per_replica": "93/4", + "widths": [ + 9, + 9, + 9 + ] + }, + { + "capacity": 32, + "count_per_replica": "234", + "widths": [ + 9, + 9, + 9, + 4 + ] + }, + { + "capacity": 32, + "count_per_replica": "18", + "widths": [ + 9, + 9, + 9, + 5 + ] + }, + { + "capacity": 48, + "count_per_replica": "7619/20", + "widths": [] + }, + { + "capacity": 48, + "count_per_replica": "1341/20", + "widths": [ + 9, + 9, + 9, + 9, + 9 + ] + } + ], + "cap_lower": "432258941218879045361/250000000000000000000000", + "cap_upper": "17290357648755161814441/10000000000000000000000000", + "idle_per_replica": { + "1": "234", + "3": "1341/20", + "48": "7619/20", + "5": "93/4" + }, + "matches_shipped_bracket": true, + "matches_shipped_idle": true, + "patterns": 2551, + "patterns_match": true, + "same_basis_as_shipped": false, + "tight_patterns": 12 + }, + "parent": { + "basis": [ + { + "capacity": 8, + "count_per_replica": "672", + "widths": [ + 8 + ] + }, + { + "capacity": 16, + "count_per_replica": "448", + "widths": [ + 9, + 7 + ] + }, + { + "capacity": 32, + "count_per_replica": "2", + "widths": [ + 8, + 8, + 8, + 8 + ] + }, + { + "capacity": 32, + "count_per_replica": "110", + "widths": [ + 9, + 8, + 8, + 7 + ] + }, + { + "capacity": 32, + "count_per_replica": "84", + "widths": [ + 9, + 9, + 9 + ] + }, + { + "capacity": 32, + "count_per_replica": "234", + "widths": [ + 9, + 9, + 9, + 4 + ] + }, + { + "capacity": 32, + "count_per_replica": "18", + "widths": [ + 9, + 9, + 9, + 5 + ] + }, + { + "capacity": 48, + "count_per_replica": "1844/5", + "widths": [] + }, + { + "capacity": 48, + "count_per_replica": "396/5", + "widths": [ + 9, + 9, + 9, + 9, + 9 + ] + } + ], + "cap_lower": "17228172707428495209099/10000000000000000000000000", + "cap_upper": "172281727074284952091/100000000000000000000000", + "idle_per_replica": { + "1": "234", + "3": "396/5", + "48": "1844/5", + "5": "84" + }, + "matches_shipped_bracket": true, + "matches_shipped_idle": true, + "patterns": 1163, + "patterns_match": true, + "same_basis_as_shipped": false, + "tight_patterns": 11 + }, + "stage1": { + "basis": [ + { + "capacity": 8, + "count_per_replica": "672", + "widths": [ + 8 + ] + }, + { + "capacity": 16, + "count_per_replica": "448", + "widths": [ + 9, + 7 + ] + }, + { + "capacity": 32, + "count_per_replica": "15", + "widths": [ + 9, + 8, + 8, + 7 + ] + }, + { + "capacity": 32, + "count_per_replica": "5/2", + "widths": [ + 9, + 9, + 7, + 7 + ] + }, + { + "capacity": 32, + "count_per_replica": "144", + "widths": [ + 9, + 9, + 8, + 6 + ] + }, + { + "capacity": 32, + "count_per_replica": "69/2", + "widths": [ + 9, + 9, + 9 + ] + }, + { + "capacity": 32, + "count_per_replica": "234", + "widths": [ + 9, + 9, + 9, + 4 + ] + }, + { + "capacity": 32, + "count_per_replica": "18", + "widths": [ + 9, + 9, + 9, + 5 + ] + }, + { + "capacity": 48, + "count_per_replica": "3787/10", + "widths": [] + }, + { + "capacity": 48, + "count_per_replica": "693/10", + "widths": [ + 9, + 9, + 9, + 9, + 9 + ] + } + ], + "cap_lower": "17262265796413098725813/10000000000000000000000000", + "cap_upper": "8631132898206549362907/5000000000000000000000000", + "idle_per_replica": { + "1": "234", + "3": "693/10", + "48": "3787/10", + "5": "69/2" + }, + "matches_shipped_bracket": true, + "matches_shipped_idle": true, + "patterns": 2551, + "patterns_match": true, + "same_basis_as_shipped": true, + "tight_patterns": 12 + }, + "stage2": { + "basis": [ + { + "capacity": 8, + "count_per_replica": "672", + "widths": [ + 8 + ] + }, + { + "capacity": 16, + "count_per_replica": "448", + "widths": [ + 9, + 7 + ] + }, + { + "capacity": 32, + "count_per_replica": "35/4", + "widths": [ + 8, + 8, + 8, + 8 + ] + }, + { + "capacity": 32, + "count_per_replica": "20", + "widths": [ + 9, + 8, + 8, + 7 + ] + }, + { + "capacity": 32, + "count_per_replica": "144", + "widths": [ + 9, + 9, + 8, + 6 + ] + }, + { + "capacity": 32, + "count_per_replica": "93/4", + "widths": [ + 9, + 9, + 9 + ] + }, + { + "capacity": 32, + "count_per_replica": "234", + "widths": [ + 9, + 9, + 9, + 4 + ] + }, + { + "capacity": 32, + "count_per_replica": "18", + "widths": [ + 9, + 9, + 9, + 5 + ] + }, + { + "capacity": 48, + "count_per_replica": "7619/20", + "widths": [] + }, + { + "capacity": 48, + "count_per_replica": "1341/20", + "widths": [ + 9, + 9, + 9, + 9, + 9 + ] + } + ], + "cap_lower": "8639053736602118419683/5000000000000000000000000", + "cap_upper": "17278107473204236839367/10000000000000000000000000", + "idle_per_replica": { + "1": "234", + "3": "1341/20", + "48": "7619/20", + "5": "93/4" + }, + "matches_shipped_bracket": true, + "matches_shipped_idle": true, + "patterns": 2551, + "patterns_match": true, + "same_basis_as_shipped": false, + "tight_patterns": 12 + } + }, + "stage1_groups_alone_on_parent": { + "A": { + "cap_lower": "1077392395653810467963/625000000000000000000000", + "cap_upper": "17238278330460967487409/10000000000000000000000000", + "gain_over_parent_cap_float": 1.0105623032472278e-06, + "local_delta": { + "1": -1, + "2": 20, + "3": -14, + "4": 2, + "5": -2 + }, + "raises_parent_cap": true, + "width_delta": { + "6": 4, + "7": -3, + "8": -1 + } + }, + "B": { + "cap_lower": "1077392395653810467963/625000000000000000000000", + "cap_upper": "17238278330460967487409/10000000000000000000000000", + "gain_over_parent_cap_float": 1.0105623032472278e-06, + "local_delta": { + "1": -1, + "2": 20, + "3": -14, + "4": 2, + "5": -2 + }, + "raises_parent_cap": true, + "width_delta": { + "6": 4, + "7": -3, + "8": -1 + } + }, + "C": { + "cap_lower": "17232332982974026581929/10000000000000000000000000", + "cap_upper": "1723233298297402658193/1000000000000000000000000", + "gain_over_parent_cap_float": 4.1602755455313726e-07, + "local_delta": { + "2": 20, + "3": -14, + "4": 2, + "5": -2 + }, + "raises_parent_cap": true, + "width_delta": { + "6": 4, + "7": -4 + } + }, + "D": { + "cap_lower": "17232332982974026581929/10000000000000000000000000", + "cap_upper": "1723233298297402658193/1000000000000000000000000", + "gain_over_parent_cap_float": 4.1602755455313726e-07, + "local_delta": { + "2": 20, + "3": -14, + "4": 2, + "5": -2 + }, + "raises_parent_cap": true, + "width_delta": { + "6": 4, + "7": -4 + } + }, + "V45": { + "cap_lower": "3446736525741929686071/2000000000000000000000000", + "cap_upper": "4308420657177412107589/2500000000000000000000000", + "gain_over_parent_cap_float": 5.509921281153221e-07, + "local_delta": { + "1": -2, + "2": 10, + "3": 6, + "4": -10 + }, + "raises_parent_cap": true, + "width_delta": { + "7": 4, + "8": -4 + } + } + }, + "status": "PASS_INDEPENDENT_CAP_RESOLVE", + "v45_endpoint_subsets_on_parent": { + "0": { + "cap_lower": "3441987695007799094551/2000000000000000000000000", + "cap_upper": "4302484618759748868189/2500000000000000000000000", + "gain_over_parent_cap_float": -1.8234232389499737e-06, + "raises_parent_cap": false + }, + "1": { + "cap_lower": "17215868375824254067961/10000000000000000000000000", + "cap_upper": "8607934187912127033981/5000000000000000000000000", + "gain_over_parent_cap_float": -1.2304331604241142e-06, + "raises_parent_cap": false + }, + "2": { + "cap_lower": "4305450591385563983697/2500000000000000000000000", + "cap_upper": "17221802365542255934789/10000000000000000000000000", + "gain_over_parent_cap_float": -6.370341886239275e-07, + "raises_parent_cap": false + }, + "3": { + "cap_lower": "4306935112106207503813/2500000000000000000000000", + "cap_upper": "17227740448424830015253/10000000000000000000000000", + "gain_over_parent_cap_float": -4.322590036651938e-08, + "raises_parent_cap": false + }, + "4": { + "cap_lower": "3446736525741929686071/2000000000000000000000000", + "cap_upper": "4308420657177412107589/2500000000000000000000000", + "gain_over_parent_cap_float": 5.509921281153221e-07, + "raises_parent_cap": true + } + } +} diff --git a/research/rank7-stage-cap-resolve/SOURCES.json b/research/rank7-stage-cap-resolve/SOURCES.json new file mode 100644 index 0000000000..72e2941a8c --- /dev/null +++ b/research/rank7-stage-cap-resolve/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "463113d675af7410ac91d53a4fed51ec6494eb9a", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5", + "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0" + }, + { + "path": "research/rank7-joint-endframes/certificates/RELAX-CAP.json", + "usage": "input", + "git_blob": "14de38f85eedf4a96500173576184a439348328c", + "sha256": "b272680de5842f7fd5f442cd0aeadfd317fe6af266ddee1a1e0738a919ba856e" + }, + { + "path": "research/rank7-joint-endframes/certificates/RELAX-STAGES.json", + "usage": "input", + "git_blob": "04f87e783b2e2b6d3ac44dd3270c0e62a1cc1173", + "sha256": "0e5ec700a191b668ba3d4b6d675f5c047d264b9a5109fc55fa92961b3fcb7d68" + }, + { + "path": "research/rank7-joint-frame-audit/RESULT.json", + "usage": "input", + "git_blob": "ed620a2bc20de9327280371e00429e8b0b7db97e", + "sha256": "994c11f0126f17ecbd0b8392d8904ad58aaede25c4c2347d3f35de6f839b2503" + } + ] +} diff --git a/research/rank7-stage-cap-resolve/TASK.json b/research/rank7-stage-cap-resolve/TASK.json new file mode 100644 index 0000000000..cd2131f12e --- /dev/null +++ b/research/rank7-stage-cap-resolve/TASK.json @@ -0,0 +1,66 @@ +{ + "schema_version": 1, + "task_id": "independent-moment", + "priority_revision": 6, + "base_commit": "463113d675af7410ac91d53a4fed51ec6494eb9a", + "original_card": { + "id": "independent-moment", + "question": "Does one changed supplier or assembly claim lack a source-bound independent check of a specific new implication?", + "starting_points": [ + "certificates/selected-result.json", + "research/rank7-joint-endframes/README.md", + "docs/research/research-family-status.md" + ], + "methods": [ + "Independently reconstruct a coordinated frame/circuit change and its single-change control, then derive the complete rank and physical ledger.", + "Implement certified moment inequalities through a different exact enclosure method." + ], + "acceptance_gate": "Demonstrate independence, source binding, positive cases and semantic failure controls. Name the existing checks and the missing coverage. More digits or another equivalent evaluation of an unchanged root is not by itself new verification coverage.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read #2979 joint rank-7 end-frame proposal and the revision-6 evidence status. Its claimed kappa is not selected. Compare coordinated changes with the losing single-change controls and locate the complete physical ledger; an aggregate moment alone does not validate the mechanism.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Prioritize a bounded independent audit of #2979: reconstruct one joint group and its single-lowering control, check the declared frames/chronology, then trace changed children, idle widths and cleanup buffers into the complete invoice and both supplier caps. Choose one still-missing implication after checking existing audits. Stop with exact unresolved dependencies if full admission exceeds the session; do not launch a new lowering census on an unvalidated premise or substitute extra root digits for mechanism checking.", + "bottleneck_link": "Independent pricing prevents unsupported frontier claims and can reveal genuine accounting slack.", + "allowed_variations": [ + "Reconstruct either a source ledger or a numeric enclosure with a different method." + ], + "scope_change_triggers": [ + "Importing the primary function and calling its output independent verification.", + "Promoting #2979 from merged source archive to validated supplier solely from author PASS receipts or aggregate pricing." + ], + "overlap_terms": [ + "independent moment", + "rank histogram", + "exact enclosure", + "2979", + "rank7 joint endframes", + "paired extraction", + "joint lowering" + ] + }, + "scope_status": "changed", + "actual_scope": "Independently re-solve, without a stored basis, the fixed-capacity packing-relaxation caps of PR #2979's parent and three stage words, and certify the cap of each stage-one group and each V45 endpoint subset alone on the parent words.", + "scope_change_reason": "The local frame accounting (PR2993 lineage), V45 native endpoint/event bindings and packing cut are already independently checked; the shipped-invoice audit left 're-solving one stage basis' open and noted that the cap rise was not shown to be forced by the V45 margin. This narrows the card to that missing implication.", + "bottleneck_link": "Replaces the source's approximate 2,091,300-unit width guide with certified fixed-inventory caps for every stage-one group and single-lowering control, so the joint-lowering mechanism is checked under the source's own relaxation rather than a surrogate price.", + "budget_minutes": 60, + "stop_rule": "Stop at matching (or contradicting) the four shipped cap brackets and the group/subset controls; do not search new lowerings or a literal allocation.", + "outcome": "partial", + "evidence": "verify.py recomputes RESULT.json: all four cap brackets equal the shipped certificates exactly on the 1e-25 grid, with identical idle histograms; 3 of 4 optimal bases are alternative (degenerate) optima. Each of V45, A, B, C, D raises the parent cap alone; V45 with 1-3 lowered endpoints lowers it and only k=4 raises it. Five rejection controls.", + "author": "Claude (AI), session donated by Mark", + "ai_assistance": "Written and run entirely by Claude (Anthropic) via Claude Code, in a session donated by Mark; no independent human review.", + "open_questions": [ + { + "question": "Does PR2987's chronological owner/packing evidence attain these relaxation caps for the stage-one words, or is part of the cap rise unreachable chronologically?", + "why_it_matters": "The relaxation ignores source windows, per-call family collisions and integrality; only a chronological fill turns a cap rise into a supplier saving.", + "first_step": "Price the literal T74 allocation's idle children against the stage-one cap with a chronological fill that keeps stage-one inventory.", + "blocked_by": "Native/phase, physical storage and precision bindings of #2979 remain unverified." + } + ] +} diff --git a/research/rank7-stage-cap-resolve/VERIFY.json b/research/rank7-stage-cap-resolve/VERIFY.json new file mode 100644 index 0000000000..85fe2dfae3 --- /dev/null +++ b/research/rank7-stage-cap-resolve/VERIFY.json @@ -0,0 +1,25 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [ + "numpy==2.2.6", + "sympy==1.14.0" + ], + "inputs": [ + "research/rank7-joint-endframes/certificates/RELAX-CAP.json", + "research/rank7-joint-endframes/certificates/RELAX-STAGES.json", + "research/rank7-joint-frame-audit/RESULT.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "four shipped cap brackets re-solved without a stored basis; five group caps and five V45 subset caps on the parent; five rejection controls; byte equality with RESULT.json" + } + ] +} diff --git a/research/rank7-stage-cap-resolve/capsolve.py b/research/rank7-stage-cap-resolve/capsolve.py new file mode 100644 index 0000000000..08df2478e5 --- /dev/null +++ b/research/rank7-stage-cap-resolve/capsolve.py @@ -0,0 +1,279 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Independent re-solve of the fixed-capacity packing relaxation caps of PR #2979. + +Nothing from the audited package is imported. The model is re-implemented from +its written description (research/rank7-joint-endframes/tools/relax.py docstring): + + per replica: bins {8: 672, 16: 448, 32: 448, 48: 448}; 9 calls; live width 896; + a pattern is a multiset of helper widths of total <= capacity, paying one idle + child of rank capacity - used (rank 0 pays nothing); + LP(b) = min sum_p x_p H(r_p, b) subject to: per capacity, sum x_p = bins[c]; + per width w, sum n_w(p) x_p = 9 * inventory[w]; x >= 0; + H(r, b) = r * (73 / r) ** b; M(b) = (9 * sum_r local_r H(r, b) + LP(b)) / (73 * 896); + cap = the root of M(b) = 1 (M is increasing because every H(r, .) is). + +Method, all different from the source's: + * patterns by recursive multiset enumeration (not a product of count ranges); + * the optimal basis is located by this file's own dense two-phase simplex + (numpy float64, Bland's rule) inside a bisection on b; no scipy, no stored basis; + * certification: the basis is inverted exactly with Fractions by this file's own + Gauss-Jordan elimination; the root of the basic profile and all reduced costs + are enclosed with mpmath interval arithmetic (mpmath.iv), not with the source's + atanh/Taylor series. +The cap bracket is (lo, hi) on the 10^-25 grid: the basic solution is feasible, so +M(lo) <= M_xB(lo) < 1 gives cap > lo; all reduced costs >= 0 at hi make xB optimal +there, so M(hi) = M_xB(hi) > 1 gives cap < hi. +""" +from fractions import Fraction as Q +import mpmath +import numpy as np + +BINS = {8: 672, 16: 448, 32: 448, 48: 448} +CALLS = 9 +LIVE = 896 +BASE = 73 +GRID = 10 ** 25 +iv = mpmath.iv +iv.dps = 70 + + +def need(cond, msg): + if not cond: + raise ValueError(msg) + + +def multisets(widths, room): + """All multisets (as count tuples aligned with widths) of total width <= room.""" + if not widths: + yield () + return + w, rest = widths[0], widths[1:] + for n in range(room // w + 1): + for tail in multisets(rest, room - n * w): + yield (n,) + tail + + +def catalogue(widths): + pats = [] + for cap in sorted(BINS): + for counts in multisets(widths, cap): + used = sum(w * n for w, n in zip(widths, counts)) + pats.append((cap, counts, cap - used)) + return pats + + +def column(p, caps, widths): + cap, counts, _ = p + return [1 if c == cap else 0 for c in caps] + list(counts) + + +def rhs_of(inventory, caps, widths): + return [BINS[c] for c in caps] + [CALLS * Q(inventory[w]) for w in widths] + + +def hfloat(r, b): + return 0.0 if r == 0 else r * (BASE / r) ** b + + +def simplex(A, rhs, cost, eps=1e-9, max_iter=20000): + """Two-phase dense simplex for min c.x, A x = rhs >= 0, x >= 0. Returns basis indices.""" + m, n = A.shape + T = np.zeros((m + 1, n + m + 1)) + T[:m, :n] = A + T[:m, n:n + m] = np.eye(m) + T[:m, -1] = rhs + basis = list(range(n, n + m)) + + def run(obj, allowed): + T[m, :] = 0.0 + T[m, :len(obj)] = obj + for i, j in enumerate(basis): + if T[m, j] != 0.0: + T[m, :] -= T[m, j] * T[i, :] + for _ in range(max_iter): + red = T[m, :allowed] + cand = np.nonzero(red < -eps)[0] + if cand.size == 0: + return + j = int(cand[0]) # Bland: smallest entering index + col = T[:m, j] + pos = col > eps + need(pos.any(), 'unbounded LP') + ratios = np.full(m, np.inf) + ratios[pos] = T[:m, -1][pos] / col[pos] + best = ratios.min() + ties = [i for i in range(m) if ratios[i] <= best + 1e-12 * max(1.0, best)] + i = min(ties, key=lambda k: basis[k]) # Bland: smallest leaving index + T[i, :] /= T[i, j] + for k in range(m + 1): + if k != i and T[k, j] != 0.0: + T[k, :] -= T[k, j] * T[i, :] + basis[i] = j + raise ValueError('simplex iteration limit') + + run(np.concatenate([np.zeros(n), np.ones(m)]), n + m) + need(-T[m, -1] < 1e-7 * max(1.0, float(np.abs(rhs).sum())), 'LP infeasible') + for i, j in enumerate(basis): # drive out remaining (degenerate) artificials + if j >= n: + nz = [k for k in range(n) if abs(T[i, k]) > 1e-9 and k not in basis] + if nz: + k = nz[0] + T[i, :] /= T[i, k] + for r in range(m + 1): + if r != i: + T[r, :] -= T[r, k] * T[i, :] + basis[i] = k + need(all(j < n for j in basis), 'redundant constraint row (artificial left in basis)') + run(np.asarray(cost, dtype=float), n) + return sorted(basis) + + +def float_lp(pats, A, rhs, b): + cost = [hfloat(r, b) for _, _, r in pats] + basis = simplex(A, rhs, cost) + xB = np.linalg.solve(A[:, basis], rhs) + return sum(cost[j] * x for j, x in zip(basis, xB)), basis + + +def moment_float(local, val, b): + return (CALLS * sum(n * hfloat(r, b) for r, n in local.items()) + val) / (BASE * LIVE) + + +def exact_inverse(M): + n = len(M) + aug = [[Q(v) for v in row] + [Q(int(i == j)) for j in range(n)] for i, row in enumerate(M)] + for c in range(n): + piv = next((r for r in range(c, n) if aug[r][c] != 0), None) + need(piv is not None, 'singular basis') + aug[c], aug[piv] = aug[piv], aug[c] + p = aug[c][c] + aug[c] = [v / p for v in aug[c]] + for r in range(n): + if r != c and aug[r][c] != 0: + f = aug[r][c] + aug[r] = [a - f * bv for a, bv in zip(aug[r], aug[c])] + return [row[n:] for row in aug] + + +def h_iv(r, b): + if r == 0: + return iv.mpf(0) + return iv.mpf(r) * iv.exp(frac_iv(Q(b)) * iv.log(iv.mpf(BASE) / r)) + + +def frac_iv(q): + return iv.mpf(q.numerator) / q.denominator + + +def moment_iv(profile, b): + s = iv.mpf(0) + for r, n in profile.items(): + if n: + s += frac_iv(Q(n)) * h_iv(r, b) + return s / (BASE * LIVE) + + +def grid_root(profile, start): + """Consecutive grid points (lo, hi) with M(lo) < 1 < M(hi), certified by intervals.""" + def side(k): + v = moment_iv(profile, Q(k, GRID)) + if v.b < 1: + return -1 + if v.a > 1: + return 1 + raise ValueError('interval precision exhausted') + lo, hi = 0, GRID // 100 # the root lies in (0, 1/100]; the float estimate is not trusted + need(side(lo) < 0 < side(hi), 'root outside (0, 1/100]') + while hi - lo > 1: + mid = (lo + hi) // 2 + if side(mid) < 0: + lo = mid + else: + hi = mid + return Q(lo, GRID), Q(hi, GRID) + + +def solve_cap(local, inventory): + local = {int(r): int(n) for r, n in local.items() if int(n)} + inventory = {int(w): int(n) for w, n in inventory.items() if int(n)} + widths = sorted(inventory) + caps = sorted(BINS) + pats = catalogue(widths) + rhs = rhs_of(inventory, caps, widths) + A = np.array([column(p, caps, widths) for p in pats], dtype=float).T + rhs_f = np.array([float(v) for v in rhs]) + lo, hi = 0.0015, 0.0020 + need(moment_float(local, float_lp(pats, A, rhs_f, lo)[0], lo) < 1, 'lower start') + need(moment_float(local, float_lp(pats, A, rhs_f, hi)[0], hi) > 1, 'upper start') + for _ in range(55): + mid = (lo + hi) / 2 + if moment_float(local, float_lp(pats, A, rhs_f, mid)[0], mid) < 1: + lo = mid + else: + hi = mid + bstar = (lo + hi) / 2 + basis = float_lp(pats, A, rhs_f, bstar)[1] + return certify(local, inventory, pats, caps, widths, rhs, basis, bstar) + + +def certify(local, inventory, pats, caps, widths, rhs, basis, bstar): + m = len(rhs) + need(len(basis) == m and len(set(basis)) == m, 'basis size') + cols = [column(pats[j], caps, widths) for j in basis] + B = [[cols[k][i] for k in range(m)] for i in range(m)] + Binv = exact_inverse(B) + xB = [sum(Binv[k][i] * rhs[i] for i in range(m)) for k in range(m)] + need(all(v >= 0 for v in xB), 'basic solution infeasible') + profile = {r: Q(CALLS * n) for r, n in local.items()} + idle = {} + for j, x in zip(basis, xB): + r = pats[j][2] + if r and x: + idle[r] = idle.get(r, 0) + x + profile[r] = profile.get(r, 0) + x + total = sum(r * n for r, n in profile.items()) + need(total == 65088, 'rank-mass identity 72*896 + 64*9 per replica') + lo, hi = grid_root(profile, bstar) + # dual y^T = c_B^T B^-1, kept symbolic: y_i = sum_k Binv[k][i] * H(r_k) + Y = [{} for _ in range(m)] + for k, j in enumerate(basis): + r = pats[j][2] + if r: + for i in range(m): + if Binv[k][i]: + Y[i][r] = Y[i].get(r, 0) + Binv[k][i] + Hhi = {} + tight = strict = 0 + min_red = None + for p in pats: + a = column(p, caps, widths) + coeff = {p[2]: Q(1)} if p[2] else {} + for i, ai in enumerate(a): + if ai: + for r, v in Y[i].items(): + coeff[r] = coeff.get(r, 0) - ai * v + coeff = {r: v for r, v in coeff.items() if v} + if not coeff: + tight += 1 + continue + red = iv.mpf(0) + for r, v in coeff.items(): + if r not in Hhi: + Hhi[r] = h_iv(r, hi) + red += frac_iv(v) * Hhi[r] + need(red.a > 0, 'reduced cost not positive at hi for pattern %r' % (p,)) + strict += 1 + min_red = red.a if min_red is None else min(min_red, red.a) + basis_out = [] + for j, x in zip(basis, xB): + cap, counts, r = pats[j] + ws = [w for w, n in zip(widths, counts) for _ in range(n)] + basis_out.append({'capacity': cap, 'widths': sorted(ws, reverse=True), 'count_per_replica': str(x)}) + return { + 'cap_lower': str(lo), 'cap_upper': str(hi), 'patterns': len(pats), 'tight_patterns': tight, + 'strict_patterns': strict, 'min_reduced_cost_lower': mpmath.nstr(mpmath.mpf(min_red), 12), + 'idle_per_replica': {str(r): str(n) for r, n in sorted(idle.items())}, + 'rank_mass_per_replica': str(total), 'basis': sorted(basis_out, key=lambda e: (e['capacity'], e['widths'])), + 'float_root': repr(bstar), + } diff --git a/research/rank7-stage-cap-resolve/run.py b/research/rank7-stage-cap-resolve/run.py new file mode 100644 index 0000000000..0cb5b50415 --- /dev/null +++ b/research/rank7-stage-cap-resolve/run.py @@ -0,0 +1,162 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Re-solve PR #2979's four fixed-capacity caps and price each stage-one group alone. + +Inputs are read as data only (JSON); no code of the audited package is imported. +Prints RESULT JSON on stdout. +""" +import gzip, hashlib, json, sys +from fractions import Fraction as Q +from pathlib import Path +import capsolve as C + +HERE = Path(__file__).resolve().parent +SRC = HERE.parent / 'rank7-joint-endframes' +AUDIT = HERE.parent / 'rank7-joint-frame-audit' + + +def read(path): + raw = path.read_bytes() + return json.loads(gzip.decompress(raw) if raw[:2] == b'\x1f\x8b' else raw), hashlib.sha256(raw).hexdigest() + + +def add(base, delta): + out = {int(k): int(v) for k, v in base.items()} + for k, v in delta.items(): + out[int(k)] = out.get(int(k), 0) + int(v) + C.need(out[int(k)] >= 0, 'negative count') + return {k: v for k, v in out.items() if v} + + +def basis_key(entries): + return sorted((e['capacity'], tuple(sorted(e['widths'])), Q(e['count_per_replica'])) for e in entries) + + +def setup(cert): + local = {int(r): int(n) for r, n in cert['local_per_call'].items()} + inv = {int(w): int(n) for w, n in cert['inventory_per_call'].items()} + widths = sorted(inv) + caps = sorted(C.BINS) + pats = C.catalogue(widths) + return local, inv, pats, caps, widths, C.rhs_of(inv, caps, widths) + + +def index_of(pats, widths, entry): + counts = tuple(entry['widths'].count(w) for w in widths) + return next(j for j, p in enumerate(pats) if p[0] == entry['capacity'] and p[1] == counts) + + +def expect_reject(label, fn): + try: + fn() + except ValueError as error: + return '%s: rejected (%s)' % (label, str(error)[:90]) + raise AssertionError('control accepted: ' + label) + + +def rejections(shipped): + out = {} + s1 = shipped['stage1'] + local, inv, pats, caps, widths, rhs = setup(s1) + basis = sorted(index_of(pats, widths, e) for e in s1['basis_patterns']) + bstar = float(Q(s1['cap_lower'])) + C.certify(local, inv, pats, caps, widths, rhs, basis, bstar) # positive control + swapped = [j for j in basis if j != basis[3]] + [next(j for j in range(len(pats)) if j not in basis and pats[j][0] == 32)] + out['swapped_basis_column'] = expect_reject('stage-1 basis with one column replaced', lambda: C.certify(local, inv, pats, caps, widths, rhs, sorted(swapped), bstar)) + s2 = shipped['stage2'] + l2, inv2, pats2, caps2, widths2, rhs2 = setup(s2) + b2 = sorted(index_of(pats2, widths2, e) for e in s2['basis_patterns']) + out['stage2_basis_on_stage1_inputs'] = expect_reject('stage-2 optimal basis certified against stage-1 inputs', lambda: C.certify(local, inv, pats, caps, widths, rhs, b2, bstar)) + A = C.np.array([C.column(p, caps, widths) for p in pats], dtype=float).T + suboptimal = C.float_lp(pats, A, C.np.array([float(v) for v in rhs]), 0.5)[1] + out['feasible_basis_optimal_at_b_half'] = expect_reject('feasible stage-1 basis optimal at b = 1/2, not at the cap', lambda: C.certify(local, inv, pats, caps, widths, rhs, suboptimal, 0)) + bad = dict(s1['local_per_call']); bad['1'] = bad['1'] + 1 + out['extra_rank1_child'] = expect_reject('stage-1 local profile with one extra rank-1 child', lambda: C.solve_cap(bad, s1['inventory_per_call'])) + stale = C.solve_cap(shipped['stage2']['local_per_call'], shipped['final']['inventory_per_call']) + C.need(Q(stale['cap_upper']) < Q(shipped['final']['cap_lower']), 'stage-2 local with final inventory must give a lower cap') + out['stage2_local_with_final_inventory'] = 'lower cap %s < %s' % (stale['cap_upper'], shipped['final']['cap_lower']) + return out + + +PINS = { + 'RELAX-STAGES.json': '0e5ec700a191b668ba3d4b6d675f5c047d264b9a5109fc55fa92961b3fcb7d68', + 'RELAX-CAP.json': 'b272680de5842f7fd5f442cd0aeadfd317fe6af266ddee1a1e0738a919ba856e', + 'rank7-joint-frame-audit/RESULT.json': '994c11f0126f17ecbd0b8392d8904ad58aaede25c4c2347d3f35de6f839b2503', +} + + +def compute(): + stages, h_st = read(SRC / 'certificates/RELAX-STAGES.json') + final, h_cap = read(SRC / 'certificates/RELAX-CAP.json') + audit, h_audit = read(AUDIT / 'RESULT.json') + shipped = {'parent': stages['parent'], 'stage1': stages['stage1'], 'stage2': stages['stage2'], 'final': final} + # bind the stage inputs to the separately implemented frame audit (PR2993 lineage) + prov = audit['providers']['base'] + C.need({int(k): v for k, v in prov['parent']['profile'].items()} == {int(k): v for k, v in shipped['parent']['local_per_call'].items()}, 'parent local') + C.need({int(k): v for k, v in prov['stage_one']['profile'].items()} == {int(k): v for k, v in shipped['stage1']['local_per_call'].items()}, 'stage1 local') + C.need({int(k): v for k, v in prov['final']['profile'].items()} == {int(k): v for k, v in shipped['final']['local_per_call'].items()}, 'final local') + ladder = {} + for name, cert in shipped.items(): + r = C.solve_cap(cert['local_per_call'], cert['inventory_per_call']) + ladder[name] = { + 'cap_lower': r['cap_lower'], 'cap_upper': r['cap_upper'], 'patterns': r['patterns'], + 'tight_patterns': r['tight_patterns'], 'idle_per_replica': r['idle_per_replica'], + 'matches_shipped_bracket': Q(r['cap_lower']) == Q(cert['cap_lower']) and Q(r['cap_upper']) == Q(cert['cap_upper']), + 'matches_shipped_idle': r['idle_per_replica'] == cert['idle_per_replica'], + 'same_basis_as_shipped': basis_key(r['basis']) == basis_key(cert['basis_patterns']), + 'patterns_match': r['patterns'] == cert['patterns'], 'basis': r['basis'], + } + names = list(ladder) + for a, b in zip(names, names[1:]): + C.need(Q(ladder[a]['cap_upper']) < Q(ladder[b]['cap_lower']), 'ladder rises %s -> %s' % (a, b)) + parent_local = shipped['parent']['local_per_call'] + parent_inv = shipped['parent']['inventory_per_call'] + parent_lo = Q(ladder['parent']['cap_lower']) + parent_hi = Q(ladder['parent']['cap_upper']) + # groups of stage one, alone on the parent: local deltas from the independent frame audit, + # width changes from #2979's README (V45: four 8->7; A, B: one 8->7, four 7->6; C, D: four 7->6) + widths = {'V45': {8: -4, 7: 4}, 'A': {8: -1, 7: -3, 6: 4}, 'B': {8: -1, 7: -3, 6: 4}, + 'C': {7: -4, 6: 4}, 'D': {7: -4, 6: 4}} + groups = {} + tot_l, tot_w = {}, {} + for g, dw in widths.items(): + dl = prov['groups'][g]['profile_delta'] + C.need(prov['groups'][g]['profile_delta'] == audit['providers']['extra']['groups'][g]['profile_delta'], 'providers agree') + for k, v in dl.items(): + tot_l[int(k)] = tot_l.get(int(k), 0) + v + for k, v in dw.items(): + tot_w[k] = tot_w.get(k, 0) + v + r = C.solve_cap(add(parent_local, dl), add(parent_inv, dw)) + groups[g] = {'local_delta': dl, 'width_delta': {str(k): v for k, v in dw.items()}, + 'cap_lower': r['cap_lower'], 'cap_upper': r['cap_upper'], + 'raises_parent_cap': Q(r['cap_lower']) > parent_hi, + 'gain_over_parent_cap_float': float((Q(r['cap_lower']) + Q(r['cap_upper'])) / 2 - (parent_lo + parent_hi) / 2)} + C.need(add(parent_local, tot_l) == {int(k): v for k, v in shipped['stage1']['local_per_call'].items()}, 'groups sum to stage1 local') + C.need(add(parent_inv, tot_w) == {int(k): v for k, v in shipped['stage1']['inventory_per_call'].items()}, 'groups sum to stage1 inventory') + # V45 endpoint subsets: Delta(k) = (2-k) H1 + 10 H2 + 6 H3 - 10 H4, k of four helpers 8 -> 7 + subsets = {} + for k in range(5): + dl = {1: 2 - k, 2: 10, 3: 6, 4: -10} + r = C.solve_cap(add(parent_local, dl), add(parent_inv, {8: -k, 7: k})) + subsets[str(k)] = {'cap_lower': r['cap_lower'], 'cap_upper': r['cap_upper'], + 'raises_parent_cap': Q(r['cap_lower']) > parent_hi, + 'gain_over_parent_cap_float': float((Q(r['cap_lower']) + Q(r['cap_upper'])) / 2 - (parent_lo + parent_hi) / 2)} + C.need(subsets['4']['cap_lower'] == groups['V45']['cap_lower'], 'k=4 is the V45 group') + for name, h in (('RELAX-STAGES.json', h_st), ('RELAX-CAP.json', h_cap), ('rank7-joint-frame-audit/RESULT.json', h_audit)): + C.need(PINS[name] == h, 'input bytes differ from pin: ' + name) + controls = rejections(shipped) + out = { + 'status': 'PASS_INDEPENDENT_CAP_RESOLVE', + 'controls': controls, + 'inputs_sha256': {'RELAX-STAGES.json': h_st, 'RELAX-CAP.json': h_cap, 'rank7-joint-frame-audit/RESULT.json': h_audit}, + 'ladder': ladder, 'stage1_groups_alone_on_parent': groups, 'v45_endpoint_subsets_on_parent': subsets, + } + return out + + +def main(): + print(json.dumps(compute(), indent=1, sort_keys=True)) + + +if __name__ == '__main__': + main() diff --git a/research/rank7-stage-cap-resolve/verify.py b/research/rank7-stage-cap-resolve/verify.py new file mode 100644 index 0000000000..9d28cc5b3e --- /dev/null +++ b/research/rank7-stage-cap-resolve/verify.py @@ -0,0 +1,22 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Recompute every cap, group control and rejection, and compare with the committed RESULT.json.""" +import json, sys +from pathlib import Path +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE)) +import run + + +def main(): + got = run.compute() + want = json.loads((HERE / 'RESULT.json').read_text(encoding='utf-8')) + run.C.need(got == want, 'recomputed result differs from RESULT.json') + run.C.need(all(v['matches_shipped_bracket'] and v['matches_shipped_idle'] for v in got['ladder'].values()), 'ladder') + run.C.need(all(v['raises_parent_cap'] for v in got['stage1_groups_alone_on_parent'].values()), 'groups') + run.C.need([v['raises_parent_cap'] for _, v in sorted(got['v45_endpoint_subsets_on_parent'].items())] == [False] * 4 + [True], 'subsets') + print('PASS_INDEPENDENT_STAGE_CAP_RESOLVE caps=4 matched groups=5 raise_alone v45_subsets=only_k4 controls=%d no_new_kappa' % len(got['controls'])) + + +if __name__ == '__main__': + main() From a30d6fabb6ea22f964b7e1e072901916e602154e Mon Sep 17 00:00:00 2001 From: Matarener Date: Sat, 17 Oct 2026 23:45:54 +0300 Subject: [PATCH 2/2] Note complementary overlap with PR3237 Co-Authored-By: Claude Opus 5.5 (1M context) --- research/rank7-stage-cap-resolve/README.md | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/research/rank7-stage-cap-resolve/README.md b/research/rank7-stage-cap-resolve/README.md index 397276eb64..4925897594 100644 --- a/research/rank7-stage-cap-resolve/README.md +++ b/research/rank7-stage-cap-resolve/README.md @@ -55,6 +55,12 @@ The five group gains sum to 3.4042e-6 against a joint stage-one rise of the open question in [rank7-v45-shipped-invoice](../rank7-v45-shipped-invoice/README.md): the cap rise is attributable to each group, V45 included, within this relaxation. +Nearest parallel work: [PR #3237](https://github.com/CrocSwap/integer-mult-bounds/pull/3237) +(commdata2338, head `9881b9d5`, open) certifies that widening V45 endpoints on +the **final** words fails the complete budget. This package instead prices the +original **stage-one** groups and subsets on the parent words and re-solves all +four shipped caps; the two are complementary and neither imports the other. + ## Controls `RESULT.json` records five checks: