Construct maximum binary decoder splits with matching cuts (no κ)

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.

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.

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"
+    }
+  ]
+}