Prove exact unequal-width query capacity on bipartite masks (no new κ)

research/bipartite-query-capacity/PROOF.md

@@ -0,0 +1,144 @@
+# Exact query dimension on bipartite masks
+
+This is a scoped algebraic theorem, not a physical supplier or a complete
+multiplication theorem. All dimensions below are integers. The field is arbitrary.
+
+## Contract and result
+
+Let G=(L disjoint-union R,E) be any finite simple bipartite graph. At vertex v
+there are d_v>=0 source coordinates and d_v target coordinates. Put D=sum_v d_v.
+A fitting matrix M has D rows and D columns, partitioned by these vertices, with
+
+    M_vv = I_(d_v),
+    M_uv = 0 if u != v and {u,v} is not an edge.
+
+Each permitted ordered block is arbitrary. Rectangular blocks, asymmetric
+opposite blocks, noncommuting coefficients and empty blocks are allowed.
+
+Define the maximum integral edge sharing
+
+    nu = max sum_(e in E) x_e,
+    x_e integer >= 0,
+    sum_(e incident to v) x_e <= d_v for every v.
+
+Define alpha_d(G) as the maximum of sum_(v in I) d_v over independent vertex
+sets I. Then, over every field F,
+
+    min_(M fits G) rank_F(M) = D - nu = alpha_d(G).       (1)
+
+Equivalently, a linear query factorization M=A B needs at least alpha_d(G)
+intermediate field coordinates, and a factorization of exactly that size exists.
+Any factorization gives rank(M)<=its intermediate dimension. Conversely a rank
+factorization exists by selecting a basis of the column space of M.
+
+The new repository statement is this complete bipartite-mask contract with
+unequal payloads. Weighted matching and cover duality are classical. We give
+the elementary proof rather than claiming a new graph-theoretic theorem.
+
+## Integral sharing equals minimum weighted vertex cover
+
+Construct a directed network with source s and sink t. Give s->u capacity d_u
+for u in L, u->v capacity D+1 for every {u,v} in E, and v->t capacity d_v for
+v in R. Start with zero flow. As long as a residual s-to-t path exists, augment
+by the smallest residual capacity along that path. Every capacity and flow stays
+integral. Each augmentation increases the flow value by at least one, and the
+value is at most D. Thus the process terminates, including when D=0.
+
+At termination let S contain the residual vertices reachable from s. There is
+no positive residual arc leaving S, and t is outside S. Therefore every original
+arc leaving S is saturated and every original arc entering S carries zero flow.
+Conservation shows that the flow value equals the capacity of this cut. Every
+flow value is at most every cut capacity, by the same conservation identity, so
+both are optimal. This proves the needed integral flow and cut statement.
+
+The cut capacity is at most D because the cut containing only s costs at most D.
+It therefore cannot cut a D+1 arc. Write P=S intersect L and Q=S intersect R.
+Every neighbor in R of P lies in Q. Consequently
+
+    C = (L minus P) union Q
+
+is a vertex cover, and the cut capacity is exactly sum_(v in C) d_v. Conversely
+a vertex cover C defines such a cut by taking P=L minus C and Q=R intersect C;
+its capacity is the cover weight. Edge flows x_e satisfy the vertex capacities,
+and every feasible integer x extends to a network flow. Hence nu is exactly the
+minimum weighted vertex-cover value.
+
+A set is independent exactly when its complement is a vertex cover. Taking
+complements gives alpha_d(G)=D-nu. Zero weights and isolated vertices need no
+special convention beyond empty sums.
+
+## Lower bound for every fitting matrix
+
+Choose an independent set I of weight alpha_d(G). The principal submatrix on
+all coordinates at vertices in I is the identity of size alpha_d(G). The
+nonedge condition forces every off-diagonal vertex block in this submatrix to
+vanish. Taking a submatrix cannot increase rank. Thus every fitting M has
+rank at least alpha_d(G), regardless of its permitted coefficients or the field.
+
+## Attainment by coordinate pairs
+
+Take optimal integral edge counts x. Allocate x_(uv) distinct, previously unused
+coordinates at u and the same number at v. Pair them across edge {u,v}. The
+vertex constraints make these allocations possible. Each unallocated coordinate
+is private. A pair contributes the matrix
+
+    [1 1]
+    [1 1]
+
+on its two coordinates, and a private coordinate contributes [1]. Put zero in
+all other positions. After a simultaneous permutation this is a direct sum of
+rank-one two-coordinate matrices and rank-one private matrices. It fits G,
+because the only off-diagonal entries join an edge and each diagonal block is
+its identity. Its rank over every field is
+
+    number of pairs + number of private coordinates
+      = nu + (D - 2 nu) = D - nu = alpha_d(G).
+
+A query for a pair is the sum of its two source coordinates, read by each of its
+two targets. A private query is its source coordinate. These give literal A,B
+with M=A B. Each receiver may subtract its neighbor contribution in the usual
+fitting-matrix interpretation; physical side-information access is a separate
+contract. The theorem only states the algebraic factorization.
+
+This proves (1). It also proves integrality: multiplying every d_v by a positive
+integer k multiplies the optimum by k. Vector payload mixing gives no rate gain
+beyond scalar coordinate pairing on this graph class. This is a dimension
+statement, not a claim that a physical pair query costs one native operation.
+
+## First example and decision
+
+For a star with center width 4 and three leaves of width 1, D=7, nu=3 and the
+exact rank is 4. The larger bipartition-side total is sharp here. On a
+path with widths (4,1,1,4), the two side totals are both 5, but the independent
+endpoint set has weight 8, nu=2, and the exact rank is 8. Merely taking the
+larger side total can therefore underprice even a connected bipartite mask.
+
+In this contract, searches for arbitrary block coefficients on a bipartite mask
+cannot beat an integral edge-sharing construction. To seek a lower algebraic
+query rate, change the graph class, the diagonal/zero contract or the type of
+encoding. Tekalign's #3362 treats the nonbipartite five-cycle and its P112
+principal core. That result is a credited model antecedent, not an input or a
+result replayed here. We do not claim a stronger full-P112 lower bound.
+
+## Finite evidence and scope
+
+The verifier has an integral residual-flow constructor and a separate exhaustive
+independent-set oracle. It expands the pair construction, checks every required
+matrix entry and computes actual ranks over GF(2), GF(3) and GF(101). A second
+finite experiment enumerates every ordered binary fitting block in its declared
+small domain, including nonsymmetric completions. These checks corroborate the
+proof; they do not replace its all-field and all-dimension arguments.
+
+The mathematical theorem has no bound on graph size or dimensions. The checker
+has explicit finite capacities. It imports no predecessor code and has no
+runtime input from another package. No claim is made about coefficient bit cost,
+nonlinear queries, native COPY tariffs, source acquisition, frames, arbitrary
+dirty-state restoration, ownership, hosting, stock, precision/tape, all-size
+compiler admission, a complete supplier or outer multiplication transfer.
+
+This contribution is produced by Nick Petalas. Credit Tekalign/#3362 for the
+unequal-payload block-fitting interface; Sagar Thakrar/#2484 and ywz65/#2471 for
+the P112 cycle setting, and the classical matching/vertex-cover and block-fitting
+methods. Cinna Davis, Adam Gall, ctoth, Philippe Van Velzen and the retained
+P112/E8/native/compiler lineage retain their predecessor credit. Apache-2.0.
+Independent human and formal proof-kernel review are unclaimed.

research/bipartite-query-capacity/README.md

@@ -0,0 +1,107 @@
+# Exact unequal-payload query capacity for bipartite masks
+
+For every finite bipartite permitted-read graph G, every nonnegative integer
+payload vector d and every coefficient field, the exact minimum fitting-matrix
+rank is
+
+    total payload - maximum integral edge sharing
+      = maximum independent-set payload weight.
+
+This is a scoped proof about linear query dimension. Arbitrary rectangular,
+nonsymmetric and noncommuting permitted blocks cannot beat coordinate pairing.
+It gives no physical supplier, new kappa or selected-frontier change.
+[PROOF.md](PROOF.md) gives the full contract, all-field proof and construction.
+
+The three-leaf star with widths (4,1,1,1) has exact query dimension 4. The path
+with widths (4,1,1,4) has dimension 8, although each bipartition side has total
+width 5. Thus even the larger side total can understate the required capacity.
+Integral coordinate sharing attains both answers.
+
+## Contribution and credit
+
+This contribution is produced by Nick Petalas. It extends the unequal-payload
+block-fitting interface of [Tekalign's #3362](https://github.com/CrocSwap/integer-mult-bounds/pull/3362)
+to the bipartite graph class. The predecessor's nonbipartite C5 result and P112
+numbers are cited without replay or audit. Classical weighted matching,
+vertex-cover duality and block-fitting methods are credited; no new general
+graph-theoretic method or literature priority is claimed.
+
+Credit Sagar Thakrar/#2484, ywz65/#2471, Cinna Davis, Adam Gall, ctoth,
+Philippe Van Velzen and the retained P112/E8/native/compiler lineage.
+[SOURCES.json](SOURCES.json) binds the historical model and base by exact bytes.
+There are no external scientific runtime inputs. Apache-2.0.
+Independent human and formal proof-kernel review are unclaimed.
+
+## Reproduction and evidence
+
+From the repository root, using standard-library CPython 3.12:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/bipartite-query-capacity/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -O -W error -B research/bipartite-query-capacity/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/bipartite-query-capacity
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/bipartite-query-capacity --check-source-history
+```
+
+Substitute an installed Python 3.12 path on another host. The verifier prints
+`PASS_BIPARTITE_QUERY_CAPACITY` after its JSON receipt. An optional
+`--receipt /absolute/external/new-file.json` saves the generated receipt with
+SHA256 of all six package files. It refuses an existing destination or a path
+inside the checkout. Default verification writes nothing.
+
+The replay checks 15,552 weighted cases and 46,656 constructed field ranks.
+The separate binary enumeration has 1,297 mask/width/matrix cases, including
+repetitions across zero-width masks. Thirteen controls and fixtures pass.
+
+The weighted domain is every one of the 64 bipartite masks on fixed parts of
+sizes 2 and 3, with every width vector in {0,1,2}^5. For each recipe an independent
+subset enumerator finds the maximum independent weight. The verifier checks
+all entries of its expanded matrix and its rank over GF(2), GF(3) and GF(101).
+A separate loop enumerates every directed binary fitting matrix on fixed parts
+of sizes 2 and 2 for every binary width vector, allowing asymmetric blocks.
+Input rejection, false fitting matrices, the unequal star, the path example and
+a 4096-bit compressed capacity fixture are also checked.
+
+These are finite corroborations of the written proof. The generic metadata
+runner also checks provenance. It is not mathematical acceptance by a reviewer.
+
+## Scope and family decision
+
+The `complex-rank-shape-decoder` card changes to a side result about exact
+query capacity. A coefficient search on this graph class cannot improve on the
+proved pairing recipe. Stop at that obstruction. No dependent physical
+construction round is proposed.
+
+Source access, actual COPY tariffs, frames, dirty restoration, ownership, hosting,
+stock, precision/tape, all-size compilation, native realization and complete
+supplier/outer transfer remain unproved. A dimension-optimal factorization does
+not supply their costs. Nonlinear encoders and nonbipartite masks are outside
+the theorem. No selected cold replay, Lean or Docker run is needed or claimed.
+
+## Engineering constraints
+
+Build the Lever supplies a deterministic constructor and verifier. Prove It
+Works requires literal fitting entries and actual field ranks, including every
+small directed binary completion. Power of Ten bounds the implementation to
+at most 14 vertices, 49 edges, 4096-bit widths and 16 dense coordinates. The
+scientific driver fixes smaller domains. Residual BFS scans at most V vertices;
+Edmonds-Karp uses at most V^3+1 attempts and each path has at most V arcs.
+Functions stay below 60 physical lines. All contracts use explicit exceptions
+and remain active under optimization. Python's managed allocation is a bounded
+rule-3 deviation; allocator internals are not inspected. The proof itself is
+unbounded in graph size and dimensions. No metaprogramming, recursion or dynamic
+imports are used. Warning-strict normal and optimized runs are registered.
+Local Ruff 0.17.1
+checks E,F,I,B,UP,SIM,RUF,C4,PIE,PERF,PTH,RET and formatting without suppressions.
+The registered scientific replay needs only the Python standard library.
+
+## Open next questions
+
+Can one named triangle-free nonbipartite mask support a block query rate below
+its integral coordinate-sharing optimum? Start with an exact fitting identity and price every
+required read. The present theorem offers no candidate or native contract.
+
+Can an attaining pair-query factorization fit a fully charged native consumer?
+Start with one literal caller and include neighbor reads, frame conversions,
+helper restoration and target writes. Physical acquisition and all-size
+admission are the blockers. Neither question is reserved by this package.

research/bipartite-query-capacity/SOURCES.json

@@ -0,0 +1,36 @@
+{
+  "schema_version": 1,
+  "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395",
+      "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602",
+      "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72"
+    },
+    {
+      "path": "research/unequal-cycle-payloads/README.md",
+      "usage": "provenance",
+      "git_blob": "8e1e01bb308b7a9147847446a7070b0c7bb9f354",
+      "sha256": "834cd8c46c3893962afe96bdf13eccf21f698fcf26e8fe0ac3c9efd1cea1e4c4"
+    },
+    {
+      "path": "research/unequal-cycle-payloads/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "e407a81af930a1b218f899f244edb303547f3d5c",
+      "sha256": "684d0281bd0308a6c3eeea602b0d6ac4e35a66a0ff740e3aeb6d5d2309805753"
+    }
+  ],
+  "predecessor": {
+    "pr": 3362,
+    "author": "Tekalign",
+    "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/3362",
+    "role": "bibliographic model antecedent; no executable or mathematical result is a runtime dependency"
+  }
+}