diff --git a/research/polynomial-decoder-split/PROOF.md b/research/polynomial-decoder-split/PROOF.md new file mode 100644 index 0000000000..a14396d0bf --- /dev/null +++ b/research/polynomial-decoder-split/PROOF.md @@ -0,0 +1,184 @@ +# Maximum split extraction by nested matroid intersection + +## Statement + +Let `H_0,...,H_(c-1)` be arbitrary `v` by `v` matrices over `F2`, with +`v,c >= 1`. A split consists of square nonsingular minors `H_a[U_a,W_a]` +whose original row sets are pairwise disjoint and whose original column sets +are separately pairwise disjoint. Its size is `sum_a |U_a|`. There is a +deterministic polynomial-time algorithm returning a maximum split and sets +`S,T` with + +```text +size = 2v - |S| - |T| + sum_a rank H_a[S,T]. (1) +``` + +The package implements this construction on the explicit capacity domain in +the README. This is a constructive specialization of classical induced +matroids and matroid intersection, not a new general min-max theorem. + +## The two oracle levels + +Let `X` and `Y` be row and column color copies, each indexed by `(a,i)`, and +let `H=blockdiag_a H_a`. Write `Q_X,Q_Y` for the partition matroids allowing +at most one copy of each original index. + +For a row set `A subset X`, define `A` independent in `N` when there is a +`Q_Y`-independent set `B subset Y` such that `H[A,B]` is square nonsingular. +Schrijver's [Theorem 3.3](https://ir.cwi.nl/pub/9901/9901D.pdf#page=12) +states that a matrix linking system induces a matroid in this way. The +hypotheses hold here: `Q_Y` is a finite matroid, the linking system consists +of nonsingular submatrices of a single matrix over a single field, and the +empty pair is allowed. Thus `N` is a matroid, of rank at most `v`. + +There is an explicit independence oracle for `N`. Restrict `H` to rows `A` +and regard its columns as a linear matroid `L_A`. Compute a maximum common +independent set of `L_A` and `Q_Y`. Its size is `rank_N(A)`: a common +independent column set of size `k` contains a nonsingular `k` by `k` minor +on some subset of `A`, and conversely every linked independent row subset +supplies such columns. In particular, `A` is independent precisely when +that size equals `|A|`. If `|A|>v`, the answer is immediately false. +For a set contained in one color, distinct original columns are automatic, +so ordinary row rank suffices. The executable uses this exact shortcut. +It also rejects a set immediately if its rows are dependent within any color: +those rows remain dependent in the full block diagonal matrix. + +The outer computation intersects `Q_X` with `N`. For an optimal outer set +`A`, invoke the inner computation once more to recover a column set `B` +of size `|A|` with `H[A,B]` nonsingular. In a block diagonal matrix, +nonsingularity forces equal row and column counts in every color. Otherwise +a color with more rows than columns has dependent selected rows. The +determinant then factors into nonzero color-block determinants. The two +partition conditions give the required disjointness. Conversely every split +gives a common independent outer set. Hence this extracts a maximum split. + +## The classical intersection subroutine + +For two matroids `M1,M2` on `E` and a common independent set `I`, use the +following directed exchange graph. Sources are `x outside I` for which +`I+x` is independent in `M1`, and sinks are those for which it is independent +in `M2`. An arc `y -> x`, with `y in I` and `x outside I`, tests +`I-y+x` in `M1`. An arc `x -> y` tests that exchange in `M2`. + +Breadth-first search returns a shortest source-to-sink path. Symmetric +difference with its vertex set preserves both independences and increases +size by one. This is the classical shortest augmenting-path theorem for +unweighted matroid intersection. The implementation also checks both +independences and the size increment after each augmentation. + +If no path exists, let `R` be every vertex reachable from any source. Then + +```text +|I| = rank_M1(E minus R) + rank_M2(R). (2) +``` + +For clarity, a standard span argument gives this terminal identity. Every +outside element not in `R` is spanned in `M1` by `I minus R`; otherwise it +would be a source or its fundamental circuit would give an arc from a +reachable member of `I`. Similarly each outside element of `R` is spanned +in `M2` by `I intersect R`, since it is not a sink and its entire fundamental +circuit is reachable along the `M2` arcs. These spans prove (2), because +the indicated subsets of `I` are independent. Shortest-path augmentation, +including the necessity of avoiding shortcuts, is the classical result +presented in [Goemans's notes, section 6](https://math.mit.edu/~goemans/18453S17/matroid-intersect-notes.pdf). +The code uses exactly the arc and source conventions above. + +## Recovering an original-index cut + +At outer termination, set `D=X minus R`. Equation (2) reads + +```text +P = rank_QX(D) + rank_N(X minus D), +``` + +where `P` is the maximum split size. Saturate `D` by deleting every color +copy of each original row represented in `D`. This preserves its partition +rank and can only decrease the induced rank on the complement. Every such +rank sum still upper-bounds the outer optimum by matroid weak duality, so +the sum remains exactly `P`. If `S` is the set of original rows not deleted, +we now have + +```text +P = v - |S| + rank_N(copies(S)). (3) +``` + +Run the inner intersection on all rows `copies(S)`, using `M1=L_copies(S)` +and `M2=Q_Y`. Let `R_Y` be its terminal reachable set. By (2), + +```text +rank_N(copies(S)) = rank H[copies(S),Y minus R_Y] + + rank_QY(R_Y). +``` + +Saturate `R_Y` by adding every column copy of each represented original +column. The partition rank is unchanged; the remaining matrix rank can only +decrease. Matroid weak duality again prevents strict decrease of the sum. +Writing `T` for the original columns not represented in `R_Y` gives + +```text +rank_N(copies(S)) = sum_a rank H_a[S,T] + v - |T|. +``` + +Substitution in (3) proves (1). Both saturations use whole original-index +groups. No equality between row and column cuts, or between selected row and +column indices, is assumed. + +## Independent certificate soundness + +Any split and any `S,T` satisfy the upper bound in (1). Deleting rows outside +`S` and columns outside `T` from each packed minor reduces rank by at most +the number deleted. The disjointness conditions charge each original row +and column at most once. The surviving rank is bounded by the corresponding +`H_a[S,T]` rank, and summing proves the bound. Therefore nonsingular disjoint +minors and an equal-valued cut certify optimality without trusting either +intersection routine, its matroid interpretation, or a general min-max +implementation. `certify` implements this check. The verifier independently +checks every returned certificate using permutation determinants for the +exhaustive small domain and dense binary row operations on larger fixtures. + +## Termination and resource bounds + +Put `N=cv`. Each intersection has at most `v` augmentations and one terminal +graph. A graph construction makes `O(N^2)` independence queries, stores at +most `N^2` arcs, and searches each vertex at most once. Only four specific +oracle roles occur: a row partition, the induced row oracle, a column linear +oracle, and a column partition. The inner linear rank uses at most `N` +vectors of at most `N` bits. Direct elimination costs `O(N^3)` bit operations. +An inner run therefore costs `O(N^6)` bit operations. The outer run makes +`O(N^3)` oracle calls, giving the conservative bound `O(N^9)` overall. +This bound includes graph construction and additional certificate checks; +it is an upper bound rather than a measured or optimized runtime claim. + +The outer routine computes its induced-matroid answers before constructing +each exchange graph. The graph then consults a bounded lookup table. Inner +calls therefore finish before the outer graph call begins, with no recursive +call cycle through the shared graph routine. There are at most `N(v+1)` +table entries per round, each keyed by at most `v+1` indices. The table is +discarded after the round, giving `O(N^3)` stored indices and `O(N^2)` vector +bits, plus graph/object overhead. No cache grows across rounds. The executable +checks `v<=32`, `c<=8`, and `N<=96` before any graph construction. All +iteration bounds follow from these dimensions, `capacity+1` graph rounds, +or bounded permutations/subsets in the verifier. It writes no artifacts. + +## Implementation constraints + +Power-of-Ten deviations are confined to the managed Python implementation. +Rule 3, fixed allocation, cannot hold literally because Python allocates +integers and collections during exact rank and set operations. The explicit +input capacities, no persistent cache, polynomial live-state bound and +serial oracle lifetimes and per-round table bound this allocation. A fixed-buffer implementation +would be the next step if hard memory guarantees were needed. + +Rules 8 and 9 permit the verifier's explicit local import and the four named +oracle roles plus their finite lookup adapter as documented deviations. The local import loads only +this package's `solver.py`, supports isolated `-I` execution, and is recorded +by the generated source hashes. The callbacks implement the classical +two-matroid oracle contract with no runtime registration or user-supplied +code. Replacing them with specialized duplicated routines would add scope +without changing their finite target sets. Normal and optimized warning-strict +replays exercise every target. No native compiler diagnostics apply; Python +warning-strict execution and package/source-history checks are the available +diagnostics. No unrelated shared code is changed. + +Produced by Nick Petalas. Classical results and predecessor credit are given +in the README. Independent human and formal proof-kernel review are unclaimed. diff --git a/research/polynomial-decoder-split/README.md b/research/polynomial-decoder-split/README.md new file mode 100644 index 0000000000..95f219f4de --- /dev/null +++ b/research/polynomial-decoder-split/README.md @@ -0,0 +1,103 @@ +# Constructive binary decoder splits and equal-valued cuts + +This package answers the algorithmic part of Open next question 1 in +[Charan/theon199's PR #2330](https://github.com/CrocSwap/integer-mult-bounds/pull/2330). +For supplied binary square blocks, `solve` deterministically extracts a maximum +packing of nonsingular minors with disjoint original rows and columns. It also +returns an equal-valued row/column cut. The implementation uses two nested +instances of classical unweighted matroid intersection. It does not enumerate +minor packings, cut pairs, or finite-field substitutions. + +The contribution is a constructive specialization and executable certificate +interface for this decoder problem. Matroid intersection and induced matroids +are classical results. The predecessor's min-max theorem is a cited premise, +not an audit deliverable. [PROOF.md](PROOF.md) establishes the extraction and +cut-recovery contract and a conservative polynomial bound. This is a scoped +constructive algorithm with exact finite corroboration, not a physical decoder, +proof-assistant formalization, new kappa, or complete multiplication theorem. + +For blocks `H_c` of order `v`, the output satisfies + +```text +sum_c |U_c| = 2v - |S| - |T| + sum_c rank_F2 H_c[S,T], +det_F2 H_c[U_c,W_c] = 1, +``` + +with equally sized `U_c,W_c`, pairwise disjoint `U_c`, and separately pairwise +disjoint `W_c`. Elementary weak duality makes each such output an independently +checkable optimality certificate. The empty minor has determinant one. + +## Reproduce + +From the repository root: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -I -B research/polynomial-decoder-split/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/polynomial-decoder-split +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/polynomial-decoder-split --check-source-history +``` + +The interpreter may be replaced by any CPython 3.12 interpreter. Only the +standard library is required. The verifier prints generated JSON ending in +`PASS_POLYNOMIAL_DECODER_SPLIT`, with SHA256 hashes of the package files and +literal certificates for the larger structured fixtures. It writes no files. +Registered commands run normally and with `-O`; acceptance uses explicit +exceptions in both modes. + +New finite coverage exhausts all one-, two-, and three-color binary block +tuples at width two. It checks each output against permutation determinants +and exhaustive cut minimization, independently of the solver's elimination. +Thirty specified SHA256-derived inputs at widths 3, 4, 6, 8 and 12 and nine +structured inputs at widths 8, 16 and 32 receive a separate dense-rank +certificate check. The width-three samples also receive the literal exhaustive +check. A greedy-trap example and malformed-input/certificate controls are +included. These are new extraction tests; no predecessor verifier is run. + +## Scope and dependencies + +The written construction applies to every finite binary input. The executable +accepts 1 through 8 colors, 1 through 32 rows per square block, and at most 96 +color copies per side. It rejects larger inputs before search. These are +implementation capacity bounds, not mathematical obstructions. The verifier's +exhaustive part has width two; its larger unstructured inputs are samples. + +The supplied-block interface does not extract a pairing or support sets from +the actual `tied_min` decoder, prove the universal rational decoder conjecture, +or realize a selected supplier. It supplies an exact oracle for a later +source-bound application. All selected compiler, native, hosting, precision, +tape and analytic obligations remain unchanged. No Lean or production supplier +replay was run. + +The task picker suggested `formal-interface-lemma`; `TASK.json` records the +changed scope. The concrete handoff in #2330 and the explicit instruction to +produce new work led to constructive extraction instead of a proof-assistant +binding or another audit. The cheap selected first control passed +`PASS_RESEARCH_BASELINE_BINDINGS_ONLY` on canonical main +`de5ec2e7a6074068452f45b1a191b5c72832df4a`, priority revision 8. + +## Open next questions + +1. Bind this extractor to one actual `tied_min` pairing and its row/column + supports. This would produce inspectable decoder-specific splits or cuts. + First export the binary blocks from the pinned #2162 data without importing + its search. The exact input adapter and source attribution remain to be done. +2. Extend the executable to other finite fields, retaining the same nested + intersection and cut contract. Start with prime-field elimination and + independent determinant checks. Field arithmetic and extension-field input + formats are not implemented here. + +## Credit and license + +This contribution was produced by Nick Petalas. Charan/theon199 #2330 posed +the polynomial witness-extraction question and supplied the explicit cut +contract. DreamingOfClouds #2162 supplied the decoder split formulation and +generic-rank interpretation, following the #1590/#2111 decoder model. +A. Schrijver's [Theorem 3.3](https://ir.cwi.nl/pub/9901/9901D.pdf#page=12) +supplies the classical induced-matroid theorem. The shortest augmenting-path +algorithm and its terminal rank cut are the classical matroid-intersection +method, as presented in +[Michel Goemans's notes, section 6](https://math.mit.edu/~goemans/18453S17/matroid-intersect-notes.pdf). +Their results are credited rather than claimed as new. No predecessor code or +text is copied. New files are Apache-2.0 under the repository license. + +Independent human and formal proof-kernel review are unclaimed. diff --git a/research/polynomial-decoder-split/SOURCES.json b/research/polynomial-decoder-split/SOURCES.json new file mode 100644 index 0000000000..2cd0063ad0 --- /dev/null +++ b/research/polynomial-decoder-split/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8", + "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/split-minmax-audit-seed63/PROOF.md", + "usage": "input", + "git_blob": "ad260528d07176932d760fb9f6be0c605cd09434", + "sha256": "f9f443d2299728297cb331713b15c92e6dd461f25a7bc1398aaef4b2ed2d3fe5" + }, + { + "path": "research/split-minmax-audit-seed63/README.md", + "usage": "input", + "git_blob": "1172888f2fe8a469d78561994b0a5b62325025bf", + "sha256": "5187c1d44a82586522422a84d10b6f263a38c439c92087d40ae092c44eac5149" + } + ] +} diff --git a/research/polynomial-decoder-split/TASK.json b/research/polynomial-decoder-split/TASK.json new file mode 100644 index 0000000000..186fbeeac4 --- /dev/null +++ b/research/polynomial-decoder-split/TASK.json @@ -0,0 +1,101 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 8, + "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "original_card": { + "id": "formal-interface-lemma", + "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/gate-operand-parity-lean/README.md", + "research/staged544-certified-endpoint/README.md", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Formalize a missing boundary lemma identified by the selected review.", + "Audit a formal theorem-to-certificate binding independently." + ], + "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.", + "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse." + }, + "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.", + "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.", + "allowed_variations": [ + "Narrow to one formal lemma or one theorem-to-certificate binding." + ], + "scope_change_triggers": [ + "Formalizing already-covered arithmetic and claiming the full multiplication theorem." + ], + "overlap_terms": [ + "hyperplane end", + "formal interface", + "Lean binding", + "3807", + "3857", + "4100", + "gate-operand-parity-lean", + "staged544-certified-endpoint", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #3807: scoped gate-operand parity formalization.", + "evidence": "research/gate-operand-parity-lean/README.md", + "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.", + "status": "author-checked", + "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #3857: certified real-power moment/endpoint arithmetic.", + "evidence": "research/staged544-certified-endpoint/README.md", + "remaining": "Uniform algorithmic implications, not another endpoint digit.", + "status": "author-checked", + "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4100: compact-switch formalization proposed as future validation.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Audit the statement and assumptions before a formal proof campaign.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Deterministic polynomial-time extraction of a maximum split and equal-valued cut for supplied binary color blocks, using nested matroid intersection.", + "scope_change_reason": "The explicit assignment asks for new work rather than an audit. Open next question 1 of Charan/theon199 PR2330 asks for constructive polynomial witness extraction. This is a source-specific algorithmic interface result, not a proof-assistant binding of the selected construction.", + "bottleneck_link": "Supplies constructive minor packings and exact obstructions for the rational-decoder split program; no physical decoder or complete invoice follows from this binary interface alone.", + "budget_minutes": 60, + "stop_rule": "Ship the first verified extraction algorithm and certificate contract; do not extend to actual pairing adapters, other fields or selected admission.", + "outcome": "completed", + "evidence": "Written extraction/cut proof and a rerunnable exact binary verifier; exhaustive new width-two inputs, independent larger certificates and semantic rejection controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Bind this extractor to an actual tied_min pairing and support sets.", + "why_it_matters": "Would turn a decoder-specific binary instance into a public split or obstructing cut.", + "first_step": "Export the masked binary blocks from pinned PR2162 data, with independent byte/source binding.", + "blocked_by": "The exact pairing/support adapter and provenance have not been implemented." + }, + { + "question": "Extend executable extraction to other finite fields.", + "why_it_matters": "The same combinatorial construction could serve nonbinary decoder interfaces.", + "first_step": "Implement prime-field rank and independent determinant checks under the existing oracle/certificate contract.", + "blocked_by": "Only binary bitmask arithmetic and input representation are implemented." + } + ] +} diff --git a/research/polynomial-decoder-split/VERIFY.json b/research/polynomial-decoder-split/VERIFY.json new file mode 100644 index 0000000000..95b239e514 --- /dev/null +++ b/research/polynomial-decoder-split/VERIFY.json @@ -0,0 +1,65 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/split-minmax-audit-seed63/PROOF.md", + "research/split-minmax-audit-seed63/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-I", + "-B", + "{package}/verify.py", + "exhaustive" + ], + "timeout_seconds": 300, + "checks": "Exact exhaustive extraction, independent primal/cut certificates and rejection controls" + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-I", + "-B", + "{package}/verify.py", + "sampled" + ], + "timeout_seconds": 300, + "checks": "Exact sampled extraction, independent primal/cut certificates and rejection controls" + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-I", + "-B", + "{package}/verify.py", + "fixtures" + ], + "timeout_seconds": 300, + "checks": "Exact fixtures extraction, independent primal/cut certificates and rejection controls" + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-I", + "-O", + "-B", + "{package}/verify.py", + "all" + ], + "timeout_seconds": 300, + "checks": "Complete extraction, independent primal/cut certificates and rejection controls with assertions disabled" + } + ] +} diff --git a/research/polynomial-decoder-split/solver.py b/research/polynomial-decoder-split/solver.py new file mode 100644 index 0000000000..ba94c31b64 --- /dev/null +++ b/research/polynomial-decoder-split/solver.py @@ -0,0 +1,252 @@ +"""Maximum disjoint binary minor packing with a matching rank-cut certificate. + +The algorithm specializes classical unweighted matroid intersection twice. +The decoder extraction interface follows Charan/theon199 PR2330 and +DreamingOfClouds PR2162; new construction produced by Nick Petalas. +Apache-2.0. +""" + +from collections import deque +from collections.abc import Callable, Sequence +from dataclasses import dataclass + + +Independent = Callable[[frozenset[int]], bool] +MAX_WIDTH = 32 +MAX_COLORS = 8 +MAX_COPIES = 96 + + +def require(condition: bool, message: str) -> None: + if not condition: + raise ValueError(message) + + +def rank(vectors: Sequence[int]) -> int: + """Binary rank; input vectors have at most MAX_COPIES bits.""" + pivots = [0] * MAX_COPIES + result = 0 + for vector in vectors: + for _ in range(MAX_COPIES): + if vector == 0: + break + bit = vector.bit_length() - 1 + if pivots[bit] == 0: + pivots[bit] = vector + result += 1 + break + vector ^= pivots[bit] + return result + + +def exchange_graph(n: int, chosen: frozenset[int], first: Independent, + second: Independent) -> tuple[list[list[int]], list[int], set[int]]: + """Inside -> outside uses first; outside -> inside uses second.""" + graph: list[list[int]] = [[] for _ in range(n)] + sources, sinks = [], set() + for outside in range(n): + if outside in chosen: + continue + added = chosen | {outside} + if first(added): + sources.append(outside) + if second(added): + sinks.add(outside) + for inside in sorted(chosen): + exchanged = added - {inside} + if first(exchanged): + graph[inside].append(outside) + if second(exchanged): + graph[outside].append(inside) + return graph, sources, sinks + + +def shortest_path(graph: list[list[int]], sources: list[int], + sinks: set[int]) -> tuple[frozenset[int], frozenset[int]]: + """Return a shortest augmenting path, or complete terminal reachability.""" + n = len(graph) + parents = [-2] * n + queue = deque(sources) + for source in sources: + parents[source] = -1 + for _ in range(n): + if not queue: + break + current = queue.popleft() + if current in sinks: + path = set() + for _ in range(n): + path.add(current) + current = parents[current] + if current == -1: + return frozenset(path), frozenset() + raise RuntimeError("cyclic predecessor chain") + for neighbor in graph[current]: + if parents[neighbor] == -2: + parents[neighbor] = current + queue.append(neighbor) + require(not queue, "BFS exceeded its vertex bound") + return frozenset(), frozenset(i for i in range(n) if parents[i] != -2) + + +def intersect(n: int, capacity: int, first: Independent, + second: Independent) -> tuple[frozenset[int], frozenset[int]]: + chosen: frozenset[int] = frozenset() + for _ in range(capacity + 1): + graph, sources, sinks = exchange_graph(n, chosen, first, second) + path, reachable = shortest_path(graph, sources, sinks) + if not path: + return chosen, reachable + new = chosen ^ path + require(len(new) == len(chosen) + 1, "augmentation size") + require(first(new) and second(new), "augmentation independence") + chosen = new + raise RuntimeError("matroid intersection exceeded its rank bound") + + +def outer_intersection(n: int, capacity: int, first: Independent, + second: Independent) -> tuple[frozenset[int], frozenset[int]]: + """Finish inner oracle calls before building each outer exchange graph.""" + chosen: frozenset[int] = frozenset() + for _ in range(capacity + 1): + answers = {} + for outside in range(n): + if outside in chosen: + continue + added = chosen | {outside} + answers[added] = second(added) + for inside in sorted(chosen): + exchanged = added - {inside} + answers[exchanged] = second(exchanged) + + def lookup(elements: frozenset[int]) -> bool: + return answers[elements] + + graph, sources, sinks = exchange_graph(n, chosen, first, lookup) + path, reachable = shortest_path(graph, sources, sinks) + if not path: + return chosen, reachable + new = chosen ^ path + require(len(new) == len(chosen) + 1, "outer augmentation size") + require(first(new) and second(new), "outer augmentation independence") + chosen = new + raise RuntimeError("outer intersection exceeded its rank bound") + + +def partition_independent(elements: frozenset[int], width: int) -> bool: + return len({element % width for element in elements}) == len(elements) + + +def inner(blocks: tuple[tuple[int, ...], ...], width: int, + rows: frozenset[int]) -> tuple[frozenset[int], frozenset[int]]: + """A column partition matroid intersected with restricted column rank.""" + n = width * len(blocks) + vectors = [0] * n + for position, row in enumerate(sorted(rows)): + color, original = divmod(row, width) + for column in range(width): + vectors[color * width + column] |= ( + ((blocks[color][original] >> column) & 1) << position) + + def linear(elements: frozenset[int]) -> bool: + return rank([vectors[element] for element in sorted(elements)]) == len(elements) + + def partition(elements: frozenset[int]) -> bool: + return partition_independent(elements, width) + + return intersect(n, width, linear, partition) + + +@dataclass(frozen=True) +class Certificate: + rows: tuple[tuple[int, ...], ...] + columns: tuple[tuple[int, ...], ...] + cut_rows: tuple[int, ...] + cut_columns: tuple[int, ...] + + +def validate(blocks: tuple[tuple[int, ...], ...]) -> int: + require(type(blocks) is tuple and 1 <= len(blocks) <= MAX_COLORS, + "expected one to eight tuple blocks") + require(type(blocks[0]) is tuple, "expected tuple rows") + width = len(blocks[0]) + require(1 <= width <= MAX_WIDTH and width * len(blocks) <= MAX_COPIES, + "width or total-copy capacity exceeded") + for block in blocks: + require(type(block) is tuple and len(block) == width, "nonsquare block") + require(all(type(row) is int and 0 <= row < (1 << width) for row in block), + "row is not a binary bitmask of the declared width") + return width + + +def solve(blocks: tuple[tuple[int, ...], ...]) -> Certificate: + width = validate(blocks) + n = width * len(blocks) + + def row_partition(elements: frozenset[int]) -> bool: + return partition_independent(elements, width) + + def induced(elements: frozenset[int]) -> bool: + if len(elements) > width: + return False + active_colors = 0 + for color, block in enumerate(blocks): + vectors = [block[element % width] for element in elements + if element // width == color] + if rank(vectors) != len(vectors): + return False + active_colors += bool(vectors) + if active_colors <= 1: + return True + columns, _ = inner(blocks, width, elements) + return len(columns) == len(elements) + + rows, reachable = outer_intersection(n, width, row_partition, induced) + columns, _ = inner(blocks, width, rows) + deleted_originals = {row % width for row in range(n) if row not in reachable} + cut_rows = tuple(i for i in range(width) if i not in deleted_originals) + saturated_rows = frozenset(c * width + i for c in range(len(blocks)) for i in cut_rows) + _, inner_reachable = inner(blocks, width, saturated_rows) + deleted_columns = {column % width for column in inner_reachable} + cut_columns = tuple(i for i in range(width) if i not in deleted_columns) + certificate = Certificate( + tuple(tuple(i for i in range(width) if c * width + i in rows) + for c in range(len(blocks))), + tuple(tuple(i for i in range(width) if c * width + i in columns) + for c in range(len(blocks))), cut_rows, cut_columns) + certify(blocks, certificate) + return certificate + + +def certify(blocks: tuple[tuple[int, ...], ...], certificate: Certificate) -> int: + """Check primal feasibility and equality to an elementary cut upper bound.""" + width = validate(blocks) + require(type(certificate) is Certificate, "expected Certificate") + require(type(certificate.rows) is tuple and type(certificate.columns) is tuple + and len(certificate.rows) == len(blocks) == len(certificate.columns), + "wrong color count") + used_rows, used_columns = set(), set() + for color, block in enumerate(blocks): + rows, columns = certificate.rows[color], certificate.columns[color] + require(type(rows) is tuple and type(columns) is tuple + and len(rows) <= width and len(columns) <= width, + "invalid minor dimensions") + require(len(rows) == len(columns), "nonsquare selected minor") + for subset in (rows, columns): + require(type(subset) is tuple and all(type(i) is int and 0 <= i < width for i in subset) + and len(set(subset)) == len(subset), "invalid selected indices") + require(not used_rows.intersection(rows) and not used_columns.intersection(columns), + "reused original row or column") + used_rows.update(rows) + used_columns.update(columns) + mask = sum(1 << i for i in columns) + require(rank([block[i] & mask for i in rows]) == len(rows), "singular selected minor") + for subset in (certificate.cut_rows, certificate.cut_columns): + require(type(subset) is tuple and len(subset) <= width + and all(type(i) is int and 0 <= i < width for i in subset) + and len(set(subset)) == len(subset), "invalid cut") + mask = sum(1 << i for i in certificate.cut_columns) + cut = 2 * width - len(certificate.cut_rows) - len(certificate.cut_columns) + cut += sum(rank([block[i] & mask for i in certificate.cut_rows]) for block in blocks) + require(len(used_rows) == cut, "primal/cut gap") + return cut diff --git a/research/polynomial-decoder-split/verify.py b/research/polynomial-decoder-split/verify.py new file mode 100644 index 0000000000..16a5efebed --- /dev/null +++ b/research/polynomial-decoder-split/verify.py @@ -0,0 +1,222 @@ +"""Independent finite evidence for the new extraction algorithm, not PR2330 replay.""" + +import hashlib +import importlib.util +import itertools +import json +from dataclasses import replace +from pathlib import Path +import sys +import time + + +PACKAGE = Path(__file__).resolve().parent +SPEC = importlib.util.spec_from_file_location("split_solver", PACKAGE / "solver.py") +if SPEC is None or SPEC.loader is None: + raise RuntimeError("cannot load package solver") +solver = importlib.util.module_from_spec(SPEC) +sys.modules[SPEC.name] = solver +SPEC.loader.exec_module(solver) + + +def check(condition: bool, message: str) -> None: + if not condition: + raise RuntimeError(message) + + +def subsets(width: int): + return (tuple(i for i in range(width) if mask & (1 << i)) for mask in range(1 << width)) + + +def determinant(block, rows, columns) -> int: + """Literal Leibniz formula over F2, independent of elimination.""" + value = 0 + for permutation in itertools.permutations(columns): + term = 1 + for row, column in zip(rows, permutation): + term &= (block[row] >> column) & 1 + value ^= term + return value + + +def minor_rank(block, rows, columns) -> int: + for size in range(min(len(rows), len(columns)), 0, -1): + for chosen_rows in itertools.combinations(rows, size): + for chosen_columns in itertools.combinations(columns, size): + if determinant(block, chosen_rows, chosen_columns): + return size + return 0 + + +def independent_small_check(blocks, certificate) -> int: + width = len(blocks[0]) + row_list = [i for group in certificate.rows for i in group] + col_list = [i for group in certificate.columns for i in group] + check(len(row_list) == len(set(row_list)), "literal row reuse") + check(len(col_list) == len(set(col_list)), "literal column reuse") + for block, rows, columns in zip(blocks, certificate.rows, certificate.columns): + check(len(rows) == len(columns) and determinant(block, rows, columns) == 1, + "literal determinant certificate") + returned_cut = 2 * width - len(certificate.cut_rows) - len(certificate.cut_columns) + returned_cut += sum(minor_rank(block, certificate.cut_rows, certificate.cut_columns) + for block in blocks) + check(returned_cut == len(row_list), "literal returned cut certificate") + best = 2 * width + for rows in subsets(width): + for columns in subsets(width): + value = 2 * width - len(rows) - len(columns) + value += sum(minor_rank(block, rows, columns) for block in blocks) + best = min(best, value) + check(best == len(row_list), "exhaustive cut optimum") + return best + + +def dense_rank(matrix) -> int: + """Dense row operations, separate from the solver's bit-vector rank.""" + work = [list(row) for row in matrix] + width = len(work[0]) if work else 0 + pivot_row = 0 + for column in range(width): + pivot = next((i for i in range(pivot_row, len(work)) if work[i][column]), None) + if pivot is None: + continue + work[pivot_row], work[pivot] = work[pivot], work[pivot_row] + for row in range(len(work)): + if row != pivot_row and work[row][column]: + work[row] = [a ^ b for a, b in zip(work[row], work[pivot_row])] + pivot_row += 1 + return pivot_row + + +def independent_large_check(blocks, certificate) -> int: + width = len(blocks[0]) + all_rows = [i for group in certificate.rows for i in group] + all_cols = [i for group in certificate.columns for i in group] + check(len(all_rows) == len(set(all_rows)), "dense row reuse") + check(len(all_cols) == len(set(all_cols)), "dense column reuse") + for block, rows, columns in zip(blocks, certificate.rows, certificate.columns): + matrix = [[(block[i] >> j) & 1 for j in columns] for i in rows] + check(len(rows) == len(columns) == dense_rank(matrix), "dense minor rank") + cut = 2 * width - len(certificate.cut_rows) - len(certificate.cut_columns) + for block in blocks: + matrix = [[(block[i] >> j) & 1 for j in certificate.cut_columns] + for i in certificate.cut_rows] + cut += dense_rank(matrix) + check(cut == len(all_rows), "dense primal/cut gap") + return cut + + +def exhaustive_cases() -> dict: + counts = {} + histogram = [0, 0, 0] + for colors in (1, 2, 3): + count = 0 + for encoding in range(1 << (4 * colors)): + blocks = tuple(tuple((encoding >> (4 * c + 2 * i)) & 3 for i in range(2)) + for c in range(colors)) + certificate = solver.solve(blocks) + value = independent_small_check(blocks, certificate) + if colors == 3: + histogram[value] += 1 + count += 1 + counts[str(colors)] = count + return {"width_two_cases_by_colors": counts, "three_color_optimum_histogram": histogram} + + +def larger_cases() -> list: + records = [] + for width in (3, 4, 6, 8, 12): + for index in range(6): + blocks = [] + for color in range(3): + rows = [] + for row in range(width): + payload = f"binary-split:{width}:{index}:{color}:{row}".encode() + rows.append(int.from_bytes(hashlib.sha256(payload).digest(), "big") + & ((1 << width) - 1)) + blocks.append(tuple(rows)) + blocks = tuple(blocks) + certificate = solver.solve(blocks) + optimum = independent_large_check(blocks, certificate) + if width == 3: + check(independent_small_check(blocks, certificate) == optimum, "sampled cuts") + records.append({"width": width, "index": index, "optimum": optimum}) + return records + + +def fixtures() -> list: + records = [] + for width in (8, 16, 32): + identity = tuple(1 << i for i in range(width)) + constant = tuple((1 << width) - 1 for _ in range(width)) + zero = tuple(0 for _ in range(width)) + for name, blocks, expected in ( + ("perfect", (identity, zero), width), + ("constant_rank_two", (constant, constant), 2), + ("zero", (zero, zero), 0)): + certificate = solver.solve(blocks) + optimum = independent_large_check(blocks, certificate) + check(optimum == expected, "explicit large fixture") + records.append({"name": name, "width": width, "optimum": optimum, + "certificate": certificate.__dict__}) + exchange = ((3, 3), (1, 0)) + check(independent_small_check(exchange, solver.solve(exchange)) == 2, + "greedy-trap fixture") + return records + + +def rejection_controls() -> int: + cases = [(), ((0,),) * 9, ((),), ((4, 0),), ((True,),), ((-1,),), + ((1, 0), (0,)), ([1],), ((0,) * 33,), ((0,) * 13,) * 8] + count = 0 + for blocks in cases: + try: + solver.solve(blocks) + except ValueError: + count += 1 + else: + raise RuntimeError("accepted invalid input") + blocks = ((1, 2), (0, 0)) + good = solver.solve(blocks) + wrong = [replace(good, rows=((0, 0), ())), + replace(good, columns=((0, 0), ())), + replace(good, rows=((0,), (0,)), columns=((0,), (0,))), + replace(good, rows=((0,), ()), columns=((1,), ())), + replace(good, cut_rows=(2,)), replace(good, cut_rows=(0, 0)), + replace(good, cut_columns=(-1,)), replace(good, rows=()), + replace(good, cut_rows=(), cut_columns=()), + replace(good, rows=((0,), ()), columns=((0,), ()))] + for certificate in wrong: + try: + solver.certify(blocks, certificate) + except ValueError: + count += 1 + else: + raise RuntimeError("accepted invalid certificate") + return count + + +def main() -> None: + check(len(sys.argv) <= 2, "expected at most one phase argument") + phase = sys.argv[1] if len(sys.argv) == 2 else "all" + check(phase in ("all", "exhaustive", "sampled", "fixtures"), "unknown phase") + result = {"claim_type": "constructive scoped algorithm with finite certificates", + "phase": phase} + for name, action in (("exhaustive", exhaustive_cases), ("sampled", larger_cases), + ("fixtures", fixtures)): + if phase in ("all", name): + start = time.perf_counter() + result[name] = action() + print(f"{name}: {time.perf_counter() - start:.3f}s", file=sys.stderr, flush=True) + result["rejection_controls"] = rejection_controls() + hashes = {} + for path in sorted(PACKAGE.iterdir()): + if path.is_file(): + hashes[path.name] = hashlib.sha256(path.read_bytes()).hexdigest() + result["package_sha256"] = hashes + result["status"] = "PASS_POLYNOMIAL_DECODER_SPLIT" + print(json.dumps(result, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main()