Bound shared phase-repair rank for independent groups

research/shared-phase-repair-rank/ORTOOLS-RESULT.json

@@ -0,0 +1,24 @@
+{
+  "a_endpoint": "1/400",
+  "groups": 2,
+  "lower_rounded_raw_cost": 3.986161,
+  "max_two_group_allowance": "306/160",
+  "new_kappa": null,
+  "objective_coefficients": "floor(1000000 * r^(399/400)), certified by integer-power comparisons",
+  "objective_scale": 1000000,
+  "optimal_rank_partition": {
+    "4": 1
+  },
+  "optimal_total_rank": 4,
+  "ortools_version": "9.11.4210",
+  "python": "3.10.12",
+  "rank_cap": 51,
+  "rank_per_group": 2,
+  "required_total_repair_rank": 4,
+  "rounded_lower_cost_scaled": 3986161,
+  "scope": "two independent direct-sum copies of PR3220's rank-two defect; arbitrary repair-rank partition; rank cap 51; exact correctability and routing granted for free",
+  "selected_frontier_changed": false,
+  "solver": "OR-Tools CP-SAT",
+  "status": "OPTIMAL_TWO_GROUP_RELAXATION",
+  "total_rank_below_four_control": "INFEASIBLE"
+}

research/shared-phase-repair-rank/PROOF.md

@@ -0,0 +1,83 @@
+# Shared phase-repair rank bound for independent groups
+
+## Statement
+
+Take `G >= 1` independent direct-sum copies of the exact port-zero idle-transfer defect retained from PR #3220. Each copy has a rank-two eight-stream matrix defect at character 16. Keep the original residual mass fixed. Repairs are additional caller-level phase children of integer ranks `q_j` between 1 and the outer cap 51; a rank-`q` phase child can alter at most `q` independent stream directions. Assume `0 <= a <= 1/400` and charge each child `q^(1-a)` raw moment units.
+
+Then any exact repair has total child rank at least `2G` and total raw repair cost strictly greater than `G`. The PR #3220 residual-repacking allowance is less than `153/160` per group. Therefore no such repair can pay for the repacking, even if routing, restoration and all other repair overhead are free.
+
+This statement is conditional on independent direct-sum group inputs and additive repair rank. It does not cover overlapping group inputs or corrections absorbed into the original calls.
+
+## Rank of the retained defect
+
+PR #3220's pinned proof gives the only nonzero entries of `Delta` at character 16 (zero-based indices):
+
+```text
+Delta[1,1] = -1-i
+Delta[3,1] = -1-i
+Delta[7,7] =  1-i
+```
+
+Thus only columns 1 and 7 are nonzero, so `rank_Q(i)(Delta) <= 2`. The principal minor on rows and columns `{1,7}` equals
+
+```text
+(-1-i)(1-i) = -2 != 0,
+```
+
+so its rank is exactly two. The exact source proof bytes and Git blob are pinned in `SOURCES.json` and retained under `vendor/`.
+
+For `G` independent groups, their joint defect is `Delta_G = Delta ⊕ ... ⊕ Delta`; hence `rank(Delta_G) = 2G`.
+
+## Required repair rank
+
+Insert repair phase children one at a time at arbitrary caller-level cuts. At character 16, inserting one rank-`q_j` phase child changes the full operator by
+
+```text
+S_j (U_j - I) P_j,
+```
+
+where `P_j` and `S_j` include every earlier and later operation at that cut. Since the phase child changes at most `q_j` independent stream directions, `rank(U_j-I) <= q_j`, and multiplication by surrounding matrices cannot increase rank. The difference between the unrepaired and repaired operators is the sum of these insertion differences, so rank subadditivity gives
+
+```text
+2G = rank(Delta_G) <= sum_j q_j.
+```
+
+This argument does not assume the repairs are assigned separately to each group. It permits one repair child to span several groups and grants arbitrary source access and routing. It does assume the group errors are independent direct summands and that the repair is a phase-child insertion rather than a changed original factorization.
+
+## Moment cost
+
+Let `Q = sum_j q_j`. Every repair child has rank `1 <= q_j <= 51`. For any `0 <= a <= 1/400`,
+
+```text
+q_j^(1-a) = q_j * q_j^(-a)
+          >= q_j * 51^(-a)
+          >= q_j * 51^(-1/400)
+          >  q_j / 2,
+```
+
+because `51 < 2^400`. Therefore total repair cost satisfies
+
+```text
+C = sum_j q_j^(1-a) > Q/2 >= G.
+```
+
+PR #3220 bounds the per-group repacking savings by
+
+```text
+B(a) <= 20*a*51/e <= 51/(20e) < 153/160,
+```
+
+using `e > 1 + 1 + 1/2 + 1/6 = 8/3`. Thus total available allowance is
+
+```text
+G*B(a) < 153G/160 < G < C.
+```
+
+The repair remains unaffordable even in this optimistic direct-sum shared model. For `G=2`, rank at least four is required; one rank-four child is a feasible rank-packing relaxation, but exact correctability is not asserted. The OR-Tools receipt gives a lower-rounded objective for this finite relaxed rank partition; the inequalities above prove the general result independently of the solver.
+
+## Scope limits
+
+- The retained witness is one source-bound owner-zero/port-zero defect. This proof takes two or more independent copies abstractly; it does not identify two actual T740 groups with disjoint source spaces.
+- It covers additional phase-child repairs at caller-level cuts, not changes inside opaque recursive children or new multi-stream interactions.
+- It fixes the original residual rank mass. Absorbed repairs, changed stock, changed coverage or reductions in original paid work require another complete invoice.
+- It is not a new provider moment, κ, supplier admission or selected-frontier update.

research/shared-phase-repair-rank/README.md

@@ -0,0 +1,37 @@
+# Rank cost of sharing phase repairs across independent groups
+
+**Scoped negative result; no new κ or supplier.** PR #3220 leaves cross-group repair sharing open because its per-group allowance does not charge one hypothetical repair once across multiple groups. This package checks the sharpest two-group relaxation for two independent copies of PR #3220's exact rank-two operator defect.
+
+At the live overlap refresh on 2026-10-17 18:34 UTC, the newest reported conditional κ was PR #3200's `0.001734807021726127552033`. This result does not improve that value; it tests one bounded route for lowering the repair bill.
+
+The source defect at character 16 has rank two over `Q(i)`. For two independent groups, the joint error is a direct sum of those matrices and has rank four. Any caller-level phase-child repairs must therefore carry total rank at least four, even if one repair is shared. With child rank capped at 51 and `0 ≤ a ≤ 1/400`, their total raw moment cost is strictly greater than one unit per group. PR #3220's maximum per-group residual-repacking allowance is strictly less than `153/160`; thus even this direct-sum shared repair cannot pay. The proof extends to any number of independent copies of this same defect; details are in [PROOF.md](PROOF.md).
+
+An optional OR-Tools CP-SAT model optimizes the most favorable two-group repair-rank partition while granting arbitrary routing and exact repairability. It selects one rank-4 child. Its integer objective coefficients are exact lower roundings of `r^(399/400)`, so its optimum is a lower bound on the true best repair bill. The standard-library replay independently recalculates those coefficients and verifies the finite optimum with dynamic programming; no optimizer dependency is required for that check. A separate CP-SAT control requiring total repair rank both at least four and at most three is infeasible. The short analytic inequality gives the general result.
+
+This is not a source-bound audit of two distinct T740 groups. It treats two independent direct-sum copies of the pinned PR #3220 port-zero defect and caller-level phase-child repairs. Overlapping inputs, repairs absorbed into original children, edits inside opaque recursive children, changed interactions and the full routing/stock invoice remain open. The retained PR #3220 proof is credited and copied verbatim under `vendor/`.
+
+## Reproduce
+
+The registered standard-library check verifies the pinned witness, exact Gaussian-integer rank, all-parameter cost inequality and solver receipt:
+
+```sh
+python3 scripts/research_package.py --package research/shared-phase-repair-rank --check-only
+python3.12 scripts/research_package.py --package research/shared-phase-repair-rank
+```
+
+Optional optimization, Python 3.10.12 with OR-Tools 9.11.4210:
+
+```sh
+python3.10 research/shared-phase-repair-rank/ortools_shared_repair.py
+```
+
+The OR-Tools run is outside registered CI. Its result is retained in `ORTOOLS-RESULT.json`; no optimizer dependency is required for the mathematical replay.
+
+## Open next questions
+
+- **Can this rank-additivity bound be bound to two actual T740 groups with disjoint source subspaces?** It would close the direct-sum premise for a real allocation. First select two groups, authenticate their source/stream maps and prove the joint defect has rank four. The current receipt only duplicates the source-derived port-zero defect on independent abstract inputs; no two-group routing ledger is pinned.
+- **Can a repair be absorbed into original paid children?** This package does not change original factors or deduct repair rank from the residual inventory. Follow PR #3220's source and derive one literal changed-child identity plus a complete invoice before searching.
+
+## Credit
+
+The exact source defect and per-group allowance are retained from Ross Richardson's [PR #3220](https://github.com/CrocSwap/integer-mult-bounds/pull/3220), prepared with substantial OpenAI Codex assistance. The source proof is copied verbatim; this package adds the independent-group rank argument, exact cost bound and optional OR-Tools relaxation. No independent human or proof-kernel review is claimed. New work is Apache-2.0.

research/shared-phase-repair-rank/SOURCES.json

@@ -0,0 +1,47 @@
+{
+  "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"
+    }
+  ],
+  "retained_sources": [
+    {
+      "local_path": "vendor/PR3220-PROOF.md",
+      "source_pr": 3220,
+      "head": "4aa4bd8d53a2bb80fa0c7d6f634c078b33965113",
+      "upstream_path": "research/idle-additive-repair-budget/PROOF.md",
+      "sha256": "dc796d5ef8adb5eb44ff953023b62efe74b3f41bd4eb411230e8c1611a097aac",
+      "git_blob": "83d199cff8d1102b8e73b144da3361e4978637d5"
+    }
+  ],
+  "context": {
+    "related_pr": "https://github.com/CrocSwap/integer-mult-bounds/pull/3220",
+    "canonical_discussion": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1167#discussioncomment-19002478",
+    "overlap_refresh": {
+      "open_prs_fetched_at": "2026-10-17T18:33:50Z",
+      "open_prs": 274,
+      "discussions_fetched_at": "2026-10-17T18:34:23Z",
+      "discussion_records": 2011,
+      "complete_pagination": true,
+      "warnings": []
+    },
+    "latest_reported_conditional_kappa": {
+      "pr": 3200,
+      "value": "0.001734807021726127552033",
+      "observed_at": "2026-10-17T18:33:50Z",
+      "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/3200"
+    },
+    "note": "The final overlap query returned no remote PR or Discussion matches. Local-only matches included this package and an unrelated readme. This package checks the independent direct-sum rank model left open by PR3220; it does not instantiate two real replica/port groups or audit their routing, overlapping sources, stock or full invoice."
+  }
+}

research/shared-phase-repair-rank/TASK.json

@@ -0,0 +1,73 @@
+{
+  "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": "Independent exact-rank and cost audit of the two-group shared-repair relaxation left open by PR3220: direct-sum two copies of its port-zero rank-two phase defect, lower-bound the aggregate rank of caller-level phase-child repairs, and compare their best possible capped-rank bill with the per-group idle-repacking allowance.",
+  "scope_change_reason": "The current independent-moment card's #2979 scope does not cover the user's assigned idle-axis research. PR3220 explicitly leaves cross-group shared repairs open. This bounded follow-up changes the object to the source-pinned rank-two defect and the method to exact direct-sum rank plus an optional OR-Tools rank-packing optimum; it does not audit or claim a full supplier.",
+  "bottleneck_link": "A shared correction can reverse the idle-axis no-go only if sharing lowers its charged rank cost below the per-group moment allowance. For independent groups the source defect ranks add, forcing at least two repair-rank units per group even under globally shared packaging.",
+  "budget_minutes": 60,
+  "stop_rule": "Authenticate PR3220's exact port-zero defect witness; prove its Q(i)-rank is two; derive the direct-sum rank and cap-51 cost lower bound for any number of independent copies; screen the two-copy integer rank partition with OR-Tools using exact floored power coefficients and a total-rank-below-four infeasibility control. Stop without generalizing to overlapping real T740 groups, absorbed repairs or changed interactions.",
+  "outcome": "negative-result",
+  "evidence": "vendor/PR3220-PROOF.md is retained byte-for-byte from PR3220 head 4aa4bd8d53a2bb80fa0c7d6f634c078b33965113 (blob 83d199cff8d1102b8e73b144da3361e4978637d5; SHA256 dc796d5e…a097aac). verify.py reconstructs the sparse 8x8 Gaussian-integer defect and checks its rank-two minor, direct-sum rank four, the strict all-a bound repair cost/G>1 versus allowance/G<153/160, and independently verifies the exact lower-rounded CP-SAT optimum by dynamic programming. The optional OR-Tools 9.11.4210 model returns the rank-4 partition with rounded lower cost 3.986161; the total-rank-below-four consistency control is infeasible. The live overlap snapshot recorded PR #3200's conditional κ `0.001734807021726127552033` as the newest κ-bearing open PR title; the result does not improve it. Live overlap at 2026-10-17T18:34:23Z covered 274 open PRs and 2,011 Discussion records with complete pagination, no warnings and no remote phrase matches. No actual pair of distinct T740 groups, new κ, supplier admission or frontier update is claimed.",
+  "author": "OpenAI Codex",
+  "ai_assistance": "OpenAI Codex wrote the independent rank/cost verifier and optional OR-Tools CP-SAT partition model. OR-Tools used Python 3.10.12 / version 9.11.4210. PR3220's retained source proof and attribution are unchanged. No independent human or proof-kernel review is claimed.",
+  "open_questions": [
+    {
+      "question": "Can the direct-sum rank bound be attached to two actual T740 replica/port groups with disjoint source subspaces?",
+      "why_it_matters": "That would determine whether the algebraic shared-repair bound applies to a real portion of the published allocation rather than to independent copies of one source defect.",
+      "first_step": "Select two concrete groups, authenticate their source/stream maps and repair cut, then compute the exact joint dirty-input operator and prove its defect has rank four before pricing routing and stock.",
+      "blocked_by": "This package pins one group witness and forms an abstract direct sum; it does not bind two distinct groups or establish their physical source independence."
+    },
+    {
+      "question": "Can an operator-failing idle transfer be repaired by changing original paid children rather than adding correction rank?",
+      "why_it_matters": "Absorption can evade an additive repair-rank lower bound and may change the recursive-moment invoice.",
+      "first_step": "Use PR3220's named transfer and provide one literal modified-child identity, preserving arbitrary dirty inputs, with a complete before/after rank and stock ledger.",
+      "blocked_by": "No changed factorization or source-bound replacement invoice is constructed here."
+    }
+  ],
+  "canonical_discussion": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1167#discussioncomment-19002478"
+}

research/shared-phase-repair-rank/VERIFY.json

@@ -0,0 +1,18 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Pinned PR3220 witness bytes; exact Gaussian-integer rank two; direct-sum rank four; all-parameter repair-cost versus residual allowance; exact integer-power objective floors and independent dynamic-programming verification of the two-group packing optimum and below-four infeasibility receipt."
+    }
+  ]
+}