From 8ec29a31efaaa99b4f7823c2d9db2142a4c810c3 Mon Sep 17 00:00:00 2001 From: Gonzalo-Mier Date: Sat, 17 Oct 2026 20:33:42 +0200 Subject: [PATCH] Bound shared phase-repair rank for independent groups --- .../ORTOOLS-RESULT.json | 24 +++ research/shared-phase-repair-rank/PROOF.md | 83 ++++++++ research/shared-phase-repair-rank/README.md | 37 ++++ .../shared-phase-repair-rank/SOURCES.json | 47 +++++ research/shared-phase-repair-rank/TASK.json | 73 +++++++ research/shared-phase-repair-rank/VERIFY.json | 18 ++ .../ortools_shared_repair.py | 105 ++++++++++ .../vendor/PR3220-PROOF.md | 184 ++++++++++++++++++ research/shared-phase-repair-rank/verify.py | 133 +++++++++++++ 9 files changed, 704 insertions(+) create mode 100644 research/shared-phase-repair-rank/ORTOOLS-RESULT.json create mode 100644 research/shared-phase-repair-rank/PROOF.md create mode 100644 research/shared-phase-repair-rank/README.md create mode 100644 research/shared-phase-repair-rank/SOURCES.json create mode 100644 research/shared-phase-repair-rank/TASK.json create mode 100644 research/shared-phase-repair-rank/VERIFY.json create mode 100644 research/shared-phase-repair-rank/ortools_shared_repair.py create mode 100644 research/shared-phase-repair-rank/vendor/PR3220-PROOF.md create mode 100644 research/shared-phase-repair-rank/verify.py diff --git a/research/shared-phase-repair-rank/ORTOOLS-RESULT.json b/research/shared-phase-repair-rank/ORTOOLS-RESULT.json new file mode 100644 index 0000000000..c4f1a666c6 --- /dev/null +++ b/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" +} diff --git a/research/shared-phase-repair-rank/PROOF.md b/research/shared-phase-repair-rank/PROOF.md new file mode 100644 index 0000000000..e9c1d3a559 --- /dev/null +++ b/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. diff --git a/research/shared-phase-repair-rank/README.md b/research/shared-phase-repair-rank/README.md new file mode 100644 index 0000000000..d394f5a5d5 --- /dev/null +++ b/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. diff --git a/research/shared-phase-repair-rank/SOURCES.json b/research/shared-phase-repair-rank/SOURCES.json new file mode 100644 index 0000000000..2d9b719de0 --- /dev/null +++ b/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." + } +} diff --git a/research/shared-phase-repair-rank/TASK.json b/research/shared-phase-repair-rank/TASK.json new file mode 100644 index 0000000000..a027b2d0eb --- /dev/null +++ b/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" +} diff --git a/research/shared-phase-repair-rank/VERIFY.json b/research/shared-phase-repair-rank/VERIFY.json new file mode 100644 index 0000000000..e7cafad85b --- /dev/null +++ b/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." + } + ] +} diff --git a/research/shared-phase-repair-rank/ortools_shared_repair.py b/research/shared-phase-repair-rank/ortools_shared_repair.py new file mode 100644 index 0000000000..5bd050759b --- /dev/null +++ b/research/shared-phase-repair-rank/ortools_shared_repair.py @@ -0,0 +1,105 @@ +#!/usr/bin/env python3 +"""OR-Tools lower-cost screen for shared repair rank across two groups. + +This deliberately grants any rank partition the ability to repair both +independent defects. Exact coefficient floors make the CP-SAT objective a lower +bound on the actual raw cost at a = 1/400. +""" +from __future__ import annotations + +import argparse +import json +import sys +from pathlib import Path + +from ortools.sat.python import cp_model +import ortools + +PACKAGE = Path(__file__).resolve().parent +SCALE = 1_000_000 +GROUPS = 2 +REQUIRED_RANK = 4 +RANK_CAP = 51 + + +def floor_scaled_power(rank: int) -> int: + """Return floor(SCALE * rank^(399/400)) by exact integer comparisons.""" + target = SCALE**400 * rank**399 + lo, hi = 0, SCALE * rank + 1 + while lo + 1 < hi: + mid = (lo + hi) // 2 + if mid**400 <= target: + lo = mid + else: + hi = mid + return lo + + +def solve() -> dict: + model = cp_model.CpModel() + count = {r: model.NewIntVar(0, REQUIRED_RANK, f"num_rank_{r}") + for r in range(1, RANK_CAP + 1)} + total_rank = sum(r * count[r] for r in count) + lower_cost = sum(floor_scaled_power(r) * count[r] for r in count) + model.Add(total_rank >= REQUIRED_RANK) + model.Minimize(lower_cost) + + solver = cp_model.CpSolver() + solver.parameters.max_time_in_seconds = 30.0 + solver.parameters.num_search_workers = 1 + solver.parameters.random_seed = 0 + status = solver.Solve(model) + if status != cp_model.OPTIMAL: + raise RuntimeError(f"two-group screen did not optimize: {solver.StatusName(status)}") + partition = {str(r): solver.Value(count[r]) for r in count if solver.Value(count[r])} + + control = cp_model.CpModel() + control_count = {r: control.NewIntVar(0, REQUIRED_RANK, f"control_num_rank_{r}") + for r in range(1, RANK_CAP + 1)} + control.Add(sum(r * control_count[r] for r in control_count) >= REQUIRED_RANK) + control.Add(sum(r * control_count[r] for r in control_count) <= REQUIRED_RANK - 1) + control_solver = cp_model.CpSolver() + control_solver.parameters.num_search_workers = 1 + control_solver.parameters.random_seed = 0 + control_status = control_solver.Solve(control) + + objective_value = solver.Value(lower_cost) + return { + "status": "OPTIMAL_TWO_GROUP_RELAXATION", + "solver": "OR-Tools CP-SAT", + "ortools_version": ortools.__version__, + "python": sys.version.split()[0], + "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", + "groups": GROUPS, + "rank_per_group": 2, + "required_total_repair_rank": REQUIRED_RANK, + "rank_cap": RANK_CAP, + "a_endpoint": "1/400", + "objective_scale": SCALE, + "objective_coefficients": "floor(1000000 * r^(399/400)), certified by integer-power comparisons", + "optimal_rank_partition": partition, + "optimal_total_rank": sum(int(r) * n for r, n in partition.items()), + "rounded_lower_cost_scaled": objective_value, + "lower_rounded_raw_cost": objective_value / SCALE, + "max_two_group_allowance": "306/160", + "total_rank_below_four_control": control_solver.StatusName(control_status), + "selected_frontier_changed": False, + "new_kappa": None, + } + + +def main() -> None: + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--output", type=Path, default=PACKAGE / "ORTOOLS-RESULT.json") + args = parser.parse_args() + result = solve() + args.output.write_text(json.dumps(result, indent=2, sort_keys=True) + "\n") + print(json.dumps({k: result[k] for k in ( + "status", "groups", "required_total_repair_rank", "optimal_rank_partition", + "lower_rounded_raw_cost", "max_two_group_allowance", "total_rank_below_four_control", + "ortools_version", + )} | {"output": str(args.output)}, sort_keys=True)) + + +if __name__ == "__main__": + main() diff --git a/research/shared-phase-repair-rank/vendor/PR3220-PROOF.md b/research/shared-phase-repair-rank/vendor/PR3220-PROOF.md new file mode 100644 index 0000000000..83d199cff8 --- /dev/null +++ b/research/shared-phase-repair-rank/vendor/PR3220-PROOF.md @@ -0,0 +1,184 @@ +# An additive repair cannot pay for one idle-group consolidation + +This is a scoped negative result for a concrete changed interface: retain the +original local and hosted calls, reassign the existing idle axes, and repair the +changed physical operator using additional recursive phase children. The +correction is charged **beyond the fixed original residual rank mass**. It is +not a proof against changing or absorbing work into the original calls. + +## 1. The exact comparison model + +Let `0 <= a <= 1/400`, `p=1-a`. The raw cost of a rank-`r` recursive child is +`r^p`, with `0^p=0`. Normalized cost is `(r/73)^p`. The same positive stock +division and all other invoice terms are held fixed on both sides. + +One original replica/port group has at most twenty residual slots of integer +ranks `0 <= r_i <= 51`. Let `M=sum r_i` and `A=sum r_i^p`. The candidate +redistributes exactly this same residual mass into ranks at most 51. To give it +every advantage, permit even nonnegative real counts and real ranks: write +`A'=sum_j w_j s_j^p`, with `0 <= s_j <= 51`, `w_j >= 0`, and +`sum_j w_j s_j=M`. Any actual reassignment is included in this relaxation. + +In addition, charge at least one actual repair child, of integer rank `q>=1` +and full multiplicity one. With several repairs let their raw cost be +`C=sum_l q_l^p`. We grant the repair exact arbitrary-input correctness and no +other overhead; in particular this favorable screen gives it free movement, +adapters and restoration. It does not construct such a free implementation. + +The original local and hosted profile, stock, widths and normalization remain +fixed. Enlarging banks, changing original children, crediting repair rank against +residual mass, or sharing one repair across several groups requires a different +invoice. Nonnegative extra costs under the fixed invoice only worsen the result. + +## 2. An all-parameter allowance bound + +For every positive `s <= 51`, `s^p=s*s^(-a) >= s*51^(-a)`. Hence + +``` +A' >= M*51^(-a), +A-A' <= B(a) := sum_i (r_i^p-r_i*51^(-a)). +``` + +Rank zero contributes zero. For integer `1 <= r <= 51`, put +`t=a*ln(51/r) >= 0`. Since `1-exp(-t) <= t` and `r^p <= r`, + +``` +r^p-r*51^(-a) + = r^p*(1-exp(-t)) + <= a*r^p*ln(51/r) + <= a*r*ln(51/r) + <= a*51/e. +``` + +The last inequality follows by differentiating `x*ln(51/x)`: its maximum over +positive `x` is `51/e`, attained at `x=51/e`. The exponential series gives +`e > 1+1+1/2+1/6 = 8/3`. Therefore, for `0= 1-B(a) > 7/160 > 0. +``` + +At `a=0`, both residual profiles cost exactly `M`; the repair costs at least +one, which also proves the strict stated margin. The normalized increase is +greater than `(7/160)*73^(-p)`, followed by any unchanged stock division. +Thus this additive repair cannot improve the fixed-stock recursive moment +inequality anywhere in the stated interval. This does not claim a new root, +a new kappa, or rejection of another supplier interface. + +This is a written proof for every real `a` in the interval and every profile +in the declared model. The finite rational endpoint calculation is a control, +not the proof of the whole interval. No formal proof kernel has checked it. + +## 3. Binding the source geometry and the proposed repair + +The source base is `463113d675af7410ac91d53a4fed51ec6494eb9a`. +The unchanged DATA-PHASES recipes contain twenty idle positions at every one +of 112 ports, with full ranks only `0,8,16,32,48`. A valid hosted prefix removes +axes from these bases, so its residuals have at most twenty slots and ranks at +most 48. The retained halving guard permits new residual rank at most 51: +`2*51^2=5202 < 73^2=5329 <= 2*52^2=5408`. + +The verifier authenticates all 2,717,280 decoded T740 fill rows through the +retained PR3148 payload hash, then reconstructs actual residual inventories for +owner replica zero at all 112 ports. Its actual endpoint allowance at `a=1/400` +is below the more permissive analytic bound. The generic twenty-slot theorem +also applies to any other valid residual partition meeting its premises; this +package does not independently rerun hosting/native/owner admission for all +other replicas or certify those partitions by a new full controller replay. + +Crucially, the source coverage tool defines `idle_mass=total_mass-local_mass`. +The theorem above is **not** an allowance to insert a repair into that coverage +law and also reduce `M`. Here the repaired proposal is the literal one: assign +each original residual axis once, then insert correction operators in addition. +Its reassigned residual mass is still exactly `M`. All correction children are +extra to that mass. A controller that instead eliminates other existing paid +work has changed this hypothesis and must be priced separately. + +## 4. A physical operator witness and the sharp insertion count + +Use PR3148 owner replica zero, port zero. Move axis `v=16` from child 10 to +child 12, as in a component of the pinned PR3184 star. The donor and receiver +residual ranks change `48,48 -> 47,49`. The axis is in the donor residual and +is orthogonal to the receiver's full basis. The total rank mass and group axis +multiset are unchanged. + +On the translation character `x=16` in `F2^73`, the canonical-cover baseline +eight-stream operator is `i I_8`. With zero-based indices the reassigned operator differs +from it at exactly + +``` +Delta[1,1] = -1-i, +Delta[3,1] = -1-i, +Delta[7,7] = 1-i. +``` + +The submatrix on rows and columns `{1,7}` has determinant `-2`, and the only +nonzero columns are 1 and 7. Thus its rank over `Q(i)` is exactly two. +These are operator identities on arbitrary inputs, including dirty streams; +no zero-state promise is used. The global phase is retained in `i I_8`. + +An inserted single-stream phase child of any axis rank has, at a fixed +character, an eight-stream action `D=I+(z-1)e_s e_s^T`. If the retained prefix +and suffix are `A,B`, adding it changes the operator by +`B(D-I)A`, of rank at most one. At any cut this cannot equal the required +rank-two correction. Therefore at least two such insertions are necessary at +caller-level cuts in this exact retained-interaction example. It does not +cover edits inside an opaque recursive child's helper-coupled implementation. +The claim concerns completed +Fourier-diagonal single-stream phase insertions; it does not treat new +multi-stream interactions or an unpriced bundled decoder as one such child. + +Two rank-one calls suffice algebraically: insert `C_v` next to the donor's +reduced residual phase and `C_v^-1` next to the receiver's enlarged phase. +Here `C_v` has eigenvalue `i^(x dot v)` at character `x`, so `C_v^4=I` exactly. +The donor phase is restored and the receiver's extra factor is cancelled. +This restores each affected original factor and hence the entire operator +for all `2^73` characters, including global phase. It simply repays and +reverts the transfer; it does not achieve a cheaper supplier. + +The identity `C_v^2=X_v` also gives `C_v^-1=C_v X_v`. Thus the inverse is one +rank-one selected child plus the explicit rank-zero translation `X_v`, whose +movement is granted free in the favorable comparison of section 1. The +interpreter represents the inverse by three forward phase exponents to test +the same identity. The invoice charges one rank-one child and grants the +translation free, rather than charging three forward calls. No repeated-axis +list in this test is accepted as an orthonormal +residual basis. For the algebraic repair, the generous budget theorem already +loses with one added child, before charging its necessary second insertion. + +## 5. Controls and precise reopening conditions + +The source-bound replay rejects a wrong inverse, omission of either repair, +and acceptance based only on the unchanged axis multiset. A positive +single-insertion control has difference rank one. The retained interpreter is +reused; a separate specialist implementation independently checked the exact +operator witness. These are AI-assisted checks, not independent human review. + +The independent integer-root routine encloses every `r^(399/400)`, `r=0..51`, +using exact integer-power bisection. It certifies the endpoint single-slot +maximizer `r=19` and four **positive relaxed-invoice** controls outside the +model: 22 original slots, half an actual repair call, one repair shared across +two groups, and repair rank deducted from original residual mass. These +relaxations are not claimed to realize correct operators. They demonstrate +why those hypotheses cannot be dropped from this budget argument. + +The bounded investigation stops here. A constructive route can reopen it by +absorbing corrections into existing calls, replacing original interactions, +providing an actual shared repair across groups, changing the coverage/rank +contract, or studying another saving interval. Each needs a new complete +invoice and arbitrary-input restoration proof. This result supplies none of +those interfaces and establishes no general barrier to a larger kappa. + +Credit: the source construction and physical-stream objection remain with +Rohan Arun, Jeremy Diviney, dcharb78, Marius-Paul Dumitrean, Jeremy Kothe, +Gonzalo-Mier, Gareth Davidson, Nick Petalas, Tekalign and the retained +word/native/geometry lineage. This scoped repair allowance and its exact +application were prepared by Ross Richardson with substantial OpenAI Codex +assistance and independent mathematical-specialist implementations. +New material is Apache-2.0; retained sources are unchanged. diff --git a/research/shared-phase-repair-rank/verify.py b/research/shared-phase-repair-rank/verify.py new file mode 100644 index 0000000000..0f85c367df --- /dev/null +++ b/research/shared-phase-repair-rank/verify.py @@ -0,0 +1,133 @@ +#!/usr/bin/env python3 +"""Exact rank and cost check for shared repairs of independent phase defects.""" +from __future__ import annotations + +import hashlib +import json +from pathlib import Path + +PACKAGE = Path(__file__).resolve().parent +PROOF_PATH = PACKAGE / "vendor/PR3220-PROOF.md" +PROOF_SHA256 = "dc796d5ef8adb5eb44ff953023b62efe74b3f41bd4eb411230e8c1611a097aac" +SCALE = 1_000_000 +RANK_CAP = 51 + + +def floor_scaled_power(rank: int) -> int: + """Exact floor(SCALE * rank**(399/400)) using integer powers only.""" + target = SCALE**400 * rank**399 + lo, hi = 0, SCALE * rank + 1 + while lo + 1 < hi: + mid = (lo + hi) // 2 + if mid**400 <= target: + lo = mid + else: + hi = mid + return lo + + +def exact_packing_optimum() -> tuple[int, list[int]]: + """Independently solve the CP-SAT rank-count domain by exact DP.""" + # CP-SAT has one count variable per rank 1..51, each with domain 0..4. + states: dict[int, tuple[int, list[int]]] = {0: (0, [])} + for rank in range(1, RANK_CAP + 1): + unit_cost = floor_scaled_power(rank) + next_states: dict[int, tuple[int, list[int]]] = {} + for old_rank, (old_cost, old_counts) in states.items(): + for count in range(5): + total_rank = old_rank + count * rank + total_cost = old_cost + count * unit_cost + candidate = (total_cost, old_counts + [count]) + if (total_rank not in next_states + or total_cost < next_states[total_rank][0]): + next_states[total_rank] = candidate + states = next_states + best_rank, (best_cost, best_counts) = min( + ((rank, item) for rank, item in states.items() if rank >= 4), + key=lambda entry: entry[1][0], + ) + partition = [rank for rank, count in enumerate(best_counts, start=1) + for _ in range(count)] + assert sum(partition) == best_rank + return best_cost, partition + + +def multiply(x: tuple[int, int], y: tuple[int, int]) -> tuple[int, int]: + a, b = x + c, d = y + return a * c - b * d, a * d + b * c + + +def subtract(x: tuple[int, int], y: tuple[int, int]) -> tuple[int, int]: + return x[0] - y[0], x[1] - y[1] + + +def main() -> None: + proof = PROOF_PATH.read_bytes() + actual_sha256 = hashlib.sha256(proof).hexdigest() + assert actual_sha256 == PROOF_SHA256, actual_sha256 + source = proof.decode("utf-8") + for line in ( + "from it at exactly\n", + "Delta[1,1] = -1-i,", + "Delta[3,1] = -1-i,", + "Delta[7,7] = 1-i.", + "nonzero columns are 1 and 7.", + "The submatrix on rows and columns `{1,7}` has determinant `-2`", + ): + assert line in source, line + + # Exact sparse 8x8 defect over Z[i]. The only nonzero columns are 1 and 7. + delta = [[(0, 0) for _ in range(8)] for _ in range(8)] + delta[1][1] = (-1, -1) + delta[3][1] = (-1, -1) + delta[7][7] = (1, -1) + nonzero_columns = {j for j in range(8) if any(delta[i][j] != (0, 0) for i in range(8))} + assert nonzero_columns == {1, 7} + # The {1,7} principal minor is (-1-i)(1-i) = -2, so rank is at least 2. + minor = subtract(multiply(delta[1][1], delta[7][7]), multiply(delta[1][7], delta[7][1])) + assert minor == (-2, 0), minor + defect_rank = 2 + + # B(a) <= 20*a*51/e. On a <= 1/400 and e > 8/3, + # B(a) < 51/(20*(8/3)) = 153/160. + assert 51 * 3 * 160 == 153 * 20 * 8 + allowance_numerator, allowance_denominator = 153, 160 + assert allowance_numerator < allowance_denominator + + # For each repair child q <= 51 and 0 <= a <= 1/400: + # q^(1-a) >= q*51^(-a) >= q*51^(-1/400) > q/2, + # since 51 < 2^400. Total inserted rank is at least rank(Delta). + rank_cap = 51 + assert rank_cap < 2**400 + + # Check the CP-SAT lower-rounded receipt without importing OR-Tools. + result = json.loads((PACKAGE / "ORTOOLS-RESULT.json").read_text()) + assert result["status"] == "OPTIMAL_TWO_GROUP_RELAXATION" + assert result["groups"] == 2 + assert result["required_total_repair_rank"] == defect_rank * result["groups"] == 4 + assert result["rank_cap"] == rank_cap + assert result["optimal_rank_partition"] == {"4": 1} + assert result["total_rank_below_four_control"] == "INFEASIBLE" + lower_cost_scaled = result["rounded_lower_cost_scaled"] + objective_scale = result["objective_scale"] + exact_optimum, exact_partition = exact_packing_optimum() + assert lower_cost_scaled == exact_optimum == 3_986_161 + assert exact_partition == [4] + assert objective_scale == SCALE + assert lower_cost_scaled * allowance_denominator > ( + objective_scale * allowance_numerator * result["groups"] + ) + + # General G-copy conclusion: correction cost > G; allowance < 153G/160. + assert allowance_denominator - allowance_numerator == 7 + print( + "PASS_SHARED_PHASE_REPAIR_RANK_BOUND " + f"source_rank={defect_rank} two_group_rank>=4 " + f"exact_packing_floor={lower_cost_scaled}/{objective_scale} " + "general_repair_cost_per_group>1 allowance_per_group<153/160" + ) + + +if __name__ == "__main__": + main()