From c92a21f9e0f1a41550ad113bd3654c92560525c8 Mon Sep 17 00:00:00 2001
From: Nick Petalas <webmasternikos@gmail.com>
Date: Tue, 3 Nov 2026 12:12:10 +0000
Subject: [PATCH 1/2] feat(research): construct uniform two-capacity
 completions

---
 research/two-capacity-uniform-codec/PROOF.md  | 168 +++++++++++++
 research/two-capacity-uniform-codec/README.md | 140 +++++++++++
 .../two-capacity-uniform-codec/SOURCES.json   |  36 +++
 research/two-capacity-uniform-codec/TASK.json | 114 +++++++++
 .../two-capacity-uniform-codec/VERIFY.json    |  32 +++
 research/two-capacity-uniform-codec/codec.py  | 161 ++++++++++++
 research/two-capacity-uniform-codec/count.py  |  73 ++++++
 research/two-capacity-uniform-codec/linear.py |  81 ++++++
 .../source/PR6539-NOTICE                      |   4 +
 .../source/PR6539-PROOF.md                    | 210 ++++++++++++++++
 research/two-capacity-uniform-codec/verify.py | 237 ++++++++++++++++++
 11 files changed, 1256 insertions(+)
 create mode 100644 research/two-capacity-uniform-codec/PROOF.md
 create mode 100644 research/two-capacity-uniform-codec/README.md
 create mode 100644 research/two-capacity-uniform-codec/SOURCES.json
 create mode 100644 research/two-capacity-uniform-codec/TASK.json
 create mode 100644 research/two-capacity-uniform-codec/VERIFY.json
 create mode 100644 research/two-capacity-uniform-codec/codec.py
 create mode 100644 research/two-capacity-uniform-codec/count.py
 create mode 100644 research/two-capacity-uniform-codec/linear.py
 create mode 100644 research/two-capacity-uniform-codec/source/PR6539-NOTICE
 create mode 100644 research/two-capacity-uniform-codec/source/PR6539-PROOF.md
 create mode 100644 research/two-capacity-uniform-codec/verify.py

diff --git a/research/two-capacity-uniform-codec/PROOF.md b/research/two-capacity-uniform-codec/PROOF.md
new file mode 100644
index 0000000000..3bbe424ffe
--- /dev/null
+++ b/research/two-capacity-uniform-codec/PROOF.md
@@ -0,0 +1,168 @@
+# Enumerating and sampling two-capacity completions
+
+## Contract and cited premise
+
+Let V and W have dimension n over a finite field F_q. Fix an injection
+h:U→W, and arbitrary subspaces A,B of V and C,D of W. Write
+
+`G(h) = {g:V→W invertible | g|U=h, g(A)⊂C, g(B)⊂D}`.
+
+The inclusions may be equalities and neither pair needs to be nested.
+Ali Romman's [PR6539](https://github.com/CrocSwap/integer-mult-bounds/pull/6539),
+head `96c63f994af628f574c71dca0d7ed219cbfc70c2`, gives an exact formula
+N(h)=|G(h)| from a constant number of subspace calculations and at most n+1
+summands. Its proof is retained verbatim in `source/PR6539-PROOF.md`.
+The coupled feasibility and common-quotient construction are ToikY's PR6535.
+The nested count is Nick Petalas's PR6489. These are cited premises here.
+This package does not reprove their count or feasibility theorems.
+
+The new result is an explicit enumerative construction and finite-fair-bit
+sampling interface for this coupled contract. Counting-to-sampling reduction,
+lexicographic interval coding and binary entropy recycling are classical.
+No general literature-priority claim is made for those methods.
+
+## 1. A conditional partition
+
+Choose an ordered basis u_1,...,u_r of U. Extend it deterministically to a
+basis of V by greedily adding standard vectors e_1,...,e_n that increase the
+span. Denote the added vectors by x_1,...,x_m, where m=n-r. They are fixed
+before choosing any images.
+
+Suppose the images of x_1,...,x_i have been specified, giving an injection
+h_i on U_i=U+span(x_1,...,x_i). For every y in W define
+
+`w_i(y) = 0` if y belongs to h_i(U_i), and otherwise
+
+`w_i(y) = N(h_i extended by x_(i+1)↦y)`.
+
+The new source vector is independent of U_i. For y outside h_i(U_i), the
+extended prescription is again an injection, so PR6539 applies with the
+same two capacities. No capacity is discarded, split or replaced by a
+separate independent count. In particular, the prescribed-image coupling
+in the predecessor's kernel condition persists at every step.
+
+Every g in G(h_i) has exactly one value y=g(x_(i+1)), and that value lies
+outside h_i(U_i). Conversely every completion counted by that branch is a
+completion of h_i. The branches are disjoint and exhaust G(h_i). Thus
+
+`N(h_i) = sum_(y∈W) w_i(y)`.
+
+At depth m the domain is V. A prescribed invertible map has exactly one
+completion if it satisfies the capacities and zero otherwise. Every
+positive leaf therefore has weight one.
+
+## 2. Rank and unrank
+
+Order the field elements once, then order vectors y lexicographically.
+Assign each child of h_i a consecutive interval of w_i(y) integers, in
+this order, starting at zero. Zero-weight children receive empty intervals.
+The partition identity makes these intervals a partition of [0,N(h_i)).
+
+Given k in [0,N(h)), choose its containing interval, subtract that
+interval's left endpoint and continue. The residual integer is always in
+the selected child's interval. After m choices it is zero because the
+selected leaf has weight one. The fixed images on the resulting domain
+basis determine all standard columns of an invertible map satisfying the
+original prescription and both capacities. This is `unrank(k)`.
+
+Conversely, for a supplied admissible map g, follow its successive images
+g(x_1),...,g(x_m) and add every left endpoint encountered. This is `rank(g)`.
+The same interval partition is used at every level. Induction on the
+remaining depth proves
+
+`rank(unrank(k)) = k`, and `unrank(rank(g)) = g`.
+
+Consequently `unrank` is a bijection from [0,N(h)) onto G(h). A uniform rank
+gives a uniform admissible completion, including arbitrary nonnormalized
+prescribed injections. If N(h)=0, no rank or sample exists. If n=r, there
+is either no completion or exactly one; no branch is needed.
+
+The abstract statement works over every finite field with an ordered
+element representation and the cited oracle. The executable uses prime
+fields only. It does not implement extension-field arithmetic.
+
+## 3. Exact sampling with a finite fair-bit budget
+
+Put M=N(h)>0. If M=1, return rank zero without reading a bit. Otherwise
+start with an interval width v=1 and value c=0. For each supplied fair bit b,
+replace `(v,c)` by `(2v,2c+b)`. If v≥M and c<M, return c. If v≥M and c≥M,
+subtract M from both v and c and continue. If the supplied bit budget ends,
+report exhaustion. A rejected interval is recycled before another bit is
+read; no candidate matrix is constructed and rejected.
+
+For M>1, after any surviving prefix one has `0≤c<v<M`. Doubling gives
+v<2M, so at most one subtraction is needed per bit. At every depth j,
+the surviving bit prefixes are in bijection with
+
+`{0,...,r_j-1}`, where `r_j = 2^j mod M`.
+
+This follows by induction. Doubling the previous residual interval gives
+every new integer once. If its size reaches M, the first M integers accept
+one occurrence of every rank, and the residual interval has size
+`2r_(j-1) mod M`. Previously accepted prefixes contribute the same number
+of length-j extensions to every rank. Therefore, with exactly b independent
+fair bits available, every rank has exactly
+
+`(2^b-r_b)/M`
+
+successful length-b bit strings, and exactly r_b strings exhaust the budget.
+In particular,
+
+`P(exhaustion) = (2^b mod M)/2^b`,
+
+and every admissible map has probability
+
+`(1-P(exhaustion))/M`.
+
+Conditional on success, the distribution is exactly uniform whenever the
+success event has positive probability. No approximate rounding or modulo
+bias is introduced. The caller must supply independent unbiased bits; this
+is a sampling interface, not a physical random-bit generator.
+
+For an unlimited fair stream, write T for the number of bits used and
+t=ceil(log_2 M). The tail identity gives
+
+`E[T] = sum_(j≥0) (2^j mod M)/2^j < t+2`.
+
+Indeed the first t summands are at most one, and the remaining sum is
+strictly below `sum_(j≥t) M/2^j = 2M/2^t ≤ 2`.
+Exhaustion probability tends to zero. For a power of two, exactly log_2 M
+bits suffice. The executable takes at most 4,096 bits and returns exhaustion
+explicitly. The infinite-stream statement is a mathematical consequence,
+not an unbounded executable loop.
+
+## 4. Exact operation bounds and limits
+
+An encoding or decoding path has m=n-r levels and at most q^n candidate
+image vectors at each level. At most one call of the cited count oracle is
+made per candidate. Including initialization, either operation needs at most
+
+`1 + (n-r) q^n`
+
+count-oracle calls. No collection of complete matrices is generated. The
+baseline literal universe has q^(n^2) matrices. These are exact candidate
+bounds, not measured runtime comparisons or a polynomial-time sampler.
+The algorithm remains exponential in n.
+
+Our direct oracle implementation uses O(n^4) field operations for basis
+calculations and O(n^2) integer products/divisions in the formula. The
+field-operation bound allows a separate linear solve for every mapped basis
+vector. It is not a bit-complexity bound. Every count is at most
+|GL_n(F_q)|<q^(n^2), so count integers have O(n^2 log q) bits. Reconstruction
+of standard columns takes O(n^4) further field operations. The fair-bit
+recurrence uses O(b) arithmetic steps on integers smaller than 2M, followed
+by one unrank call on success.
+
+The executable enforces n≤12, prime q≤31, q^n≤4,096 and b≤4,096. It keeps
+one partial prescription and bounded row-reduction workspaces, rather than
+a tree of all completions. Python allocates managed integers and containers;
+no allocation-free execution or physical storage tariff is claimed. Functions
+use bounded loops, normal input errors and invariant checks that remain
+enabled under optimization. The finite verifier's enumerations have separate
+explicit dimension and field bounds.
+
+This is unrestricted GL construction. It does not preserve a symplectic form
+or signed phases, construct an actual native contact, price scalar basis
+changes or establish caller access, dirty restoration, physical routing,
+precision, stock, tapes, compiler or outer closure. All five selected
+framework assumptions remain. No new kappa or selected-frontier change follows.
diff --git a/research/two-capacity-uniform-codec/README.md b/research/two-capacity-uniform-codec/README.md
new file mode 100644
index 0000000000..3788a3216e
--- /dev/null
+++ b/research/two-capacity-uniform-codec/README.md
@@ -0,0 +1,140 @@
+# Exact uniform two-capacity completions
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+Claim type: a scoped written constructive proof with exact finite corroboration.
+Given an injection h:U→W over a prime field and two arbitrary simultaneous
+capacities `g(A)⊂C`, `g(B)⊂D`, this package constructs a bijection between
+integer ranks and every admissible invertible extension g. Sampling a uniform
+rank therefore constructs an exactly uniform extension. A finite fair-bit
+interface reports exhaustion explicitly and is exactly uniform conditional
+on success.
+
+The new step answers the uniform-sampling opening in
+[Ali Romman's PR6539](https://github.com/CrocSwap/integer-mult-bounds/pull/6539).
+Its exact two-capacity count is a cited premise, not a result established here.
+The construction handles overlapping, nonnested source and target spaces and
+arbitrary prescribed images. It retains the coupling in every conditional
+count. [PROOF.md](PROOF.md) gives the theorem, inverse algorithms, bit law and
+operation bounds. The self-reduction and entropy-recycling methods are
+classical; no general literature-priority claim is made.
+
+For N admissible maps and a budget of b independent fair bits, the sampler's
+exact exhaustion probability is `(2^b mod N)/2^b`. Every map has the same
+success probability. On an unlimited stream the expected bit count is below
+`ceil(log2 N)+2`, with exactly `log2 N` bits when N is a power of two.
+An encoding or decoding path uses at most `1+(n-dim U)q^n` calls to the cited
+count oracle, including initialization. It does not enumerate the `q^(n^2)`
+complete candidate matrices. This remains exponential in n; no polynomial
+runtime or measured speedup is claimed.
+
+## Exact finite evidence
+
+The new decoder and encoder agree with independently enumerated, ordered
+matrix sets on 2,118 admissible endpoints in 1,954 contracts. The full small
+part has 1,940 contracts and 1,342 endpoints. It includes every ordered pair
+of source/target subspaces and every normalized fixed rank over F2 in
+dimensions 0, 1 and 2, and F3 in dimension 1. The other 14 contracts contribute
+776 endpoints over F3/F5 in dimension 2 and F2 in dimension 3, including
+nonnormalized prescribed images, coupled capacities and empty sets.
+
+There are ten additional rank/unrank round trips in two dimension-eight
+contracts, with endpoint constraints checked directly. These are selected
+ranks, not an exhaustive dimension-eight census. Their ambient cardinalities
+are outputs of the cited oracle, not new independently enumerated counts.
+
+The bit checker exhausts 24,564 bit strings for 132 cardinality/budget pairs,
+N=1,...,12 and b=0,...,10. It checks exact equality of every output frequency
+and the exact exhaustion count. For the six binary 2×2 invertible matrices,
+all 256 eight-bit strings give 42 occurrences per matrix and four exhausted
+strings. Fourteen rejection controls exercise bad ranks, singular or illegal
+maps, nonprime fields, noncanonical vectors, resource limits and empty sampling.
+Both ordinary and optimized execution retain these checks.
+
+These checks test the new construction's output and distribution. No
+predecessor scientific suite or selected cold replay is run.
+
+## Reproduction
+
+From the repository root, using CPython 3.12 and the standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B scripts/research_package.py --package research/two-capacity-uniform-codec
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B scripts/check_research_commit.py --package research/two-capacity-uniform-codec --check-source-history
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/two-capacity-uniform-codec/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -O -B research/two-capacity-uniform-codec/verify.py
+```
+
+Another CPython 3.12 installation may replace that local interpreter path.
+Each registered scientific command has a 120-second timeout. Optional
+`--receipt /absolute/scratch/path.json` writes a generated receipt outside the
+checkout, bound to the hashes of every package file. Default replay writes
+only stdout. No hand-authored receipt is supplied.
+
+For a direct API example, put this package on the Python import path:
+
+```python
+from codec import Codec, Contract
+
+codec = Codec(Contract(2, 2, (), (((), ()), ((), ()))))
+matrix = codec.unrank(4)  # Matrices are tuples of standard column vectors.
+assert codec.rank(matrix) == 4
+matrix_or_none, bits_used = codec.sample((1, 1, 0, 0, 1, 0, 1, 1))
+```
+
+## Sources, credit and limits
+
+The immediate dependency is Ali Romman's PR6539 at
+`96c63f994af628f574c71dca0d7ed219cbfc70c2`. Its proof text and NOTICE are
+retained verbatim, authenticated by SHA256 and Git blob digests, and attributed
+in [SOURCES.json](SOURCES.json). They were obtained from that immutable public
+head. Its relative NOTICE pointers refer to the original package. This
+checkout does not contain that head as a Git object, so the generic
+source-history check authenticates the main-based provenance; it does not
+certify the external head's ancestry. The standalone verifier authenticates
+the retained external bytes. No predecessor source code is imported.
+
+Credit ToikY / PR6535 for coupled quotient feasibility, Ali Romman / PR6533
+for general simultaneous-capacity rank counts and construction, Nick Petalas /
+PR6489 for the nested count, Brian / JoyboyBrian / PR5020 for the original
+one-capacity contract, Cao Yifan / intqwq / PR4610 for the caller context,
+Nick Petalas / PR4919, codyw912 / PR4735, and the retained Cinna Davis,
+Dugongue, zxv and Jacob Alan Sussman lineage. These predecessor theorems and
+classical linear algebra are not claimed as new.
+
+The executable enforces n≤12, prime q≤31, q^n≤4,096 and at most 4,096 supplied
+bits. The abstract reduction works over every finite field with an ordered
+element representation and exact count oracle; extension fields are not
+implemented. The function can report entropy exhaustion, and an empty
+completion set is an error for sampling.
+
+Python uses managed allocation within these finite input limits. The code has
+no recursive calls, hidden random source or unbounded retry loop. Field
+inversion, arbitrary-precision integer operations and the standard dataclass
+mechanism are managed-runtime deviations from fixed-allocation low-level
+rules. Checks use ordinary exceptions and remain enabled under `-O`.
+
+This is an unrestricted GL interface. Native or symplectic realization,
+signed phase, actual contacts, physical scalar/basis costs, causal access,
+dirty restoration, precision, stock, tapes, compiler and the complete outer
+invoice remain unproved. All five selected assumptions remain. There is no
+new kappa, supplier admission, full multiplication theorem, or proof-kernel
+verification. Independent human and formal proof-kernel review are unclaimed.
+
+The publication base is canonical main
+`7c49fe32c55de02c2c873655c804b16e4c3fef0a`, priority revision 8, selected
+PR6030. `formal-interface-lemma` has changed scope to this constructive
+finite-field prerequisite. Its baseline binding command passed; this does not
+replay or strengthen the selected supplier.
+
+## Open next questions
+
+1. Can a direct sampler realize the predecessor's quotient/lift factors in
+   polynomially many field operations? Begin with the common injection and
+   its prescribed quotient discrepancy. Uniform choices of compatible lifts
+   must retain the exact branch multiplicities; a feasibility witness alone
+   does not give a uniform distribution. This would remove the q^n factor.
+2. Can one actual shared native contact use a sampled completion with a
+   favorable complete bill? Specify its exact bases and chronology first.
+   Symplectic or signed constraints, legal access and physical realization
+   are blockers; an unrestricted GL sample does not meet them automatically.
diff --git a/research/two-capacity-uniform-codec/SOURCES.json b/research/two-capacity-uniform-codec/SOURCES.json
new file mode 100644
index 0000000000..462c6d8f67
--- /dev/null
+++ b/research/two-capacity-uniform-codec/SOURCES.json
@@ -0,0 +1,36 @@
+{
+  "schema_version": 1,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a",
+      "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    }
+  ],
+  "external_sources": [
+    {
+      "local_path": "source/PR6539-PROOF.md",
+      "author": "Ali Romman",
+      "url": "https://github.com/aliromman/integer-mult-bounds/blob/96c63f994af628f574c71dca0d7ed219cbfc70c2/research/two-capacity-completion-count/PROOF.md",
+      "sha256": "66ab99f0c3b13999325523378ae3f9ade8c0341cd194cc8ad5580916bc9144c4",
+      "git_blob": "0a835ca8de78befc93e61b72d18a471a1e1df344",
+      "usage": "cited theorem and retained attribution; no source scientific replay"
+    },
+    {
+      "local_path": "source/PR6539-NOTICE",
+      "author": "Ali Romman",
+      "url": "https://github.com/aliromman/integer-mult-bounds/blob/96c63f994af628f574c71dca0d7ed219cbfc70c2/research/two-capacity-completion-count/NOTICE",
+      "sha256": "8987ad7468783ec169bb112de5231a4e22cb46a18583e52a8f6201cefac61d2c",
+      "git_blob": "50762aa4f8e901a9882bd0366a9a756887a540f8",
+      "usage": "cited theorem and retained attribution; no source scientific replay"
+    }
+  ]
+}
diff --git a/research/two-capacity-uniform-codec/TASK.json b/research/two-capacity-uniform-codec/TASK.json
new file mode 100644
index 0000000000..820f8d0328
--- /dev/null
+++ b/research/two-capacity-uniform-codec/TASK.json
@@ -0,0 +1,114 @@
+{
+  "schema_version": 1,
+  "task_id": "formal-interface-lemma",
+  "priority_revision": 8,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "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": "Exact rank/unrank bijection and finite-fair-bit uniform sampler for invertible prime-field completions with a prescribed injection and two arbitrary simultaneous capacities.",
+  "scope_change_reason": "The source PR6539 leaves uniform sampling open. This is a written constructive interface proof rather than a Lean formalization or an audit of a selected assumption.",
+  "bottleneck_link": "Side result for shared-map basis selection: converts a coupled static count into explicit completions. Physical/native/caller admission remains separate.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after the first verified enumerative construction; direct polynomial-time sampling and physical realization remain open.",
+  "outcome": "completed",
+  "evidence": "PROOF.md and verify.py; exact literal rank/unrank endpoints, finite-bit distribution census, large selected round trips and rejection controls.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Can a direct uniform sampler realize the quotient/lift factors in polynomially many field operations?",
+      "why_it_matters": "It would remove the q^n candidate-vector factor.",
+      "first_step": "Construct uniform common injections with the prescribed quotient discrepancy and track lift multiplicities.",
+      "blocked_by": "Compatible lift multiplicities must remain exact across both capacities."
+    },
+    {
+      "question": "Can an actual shared native contact use a sampled completion with a favorable full bill?",
+      "why_it_matters": "The unrestricted GL interface alone does not improve a supplier.",
+      "first_step": "Specify one exact contact, its source/target bases and legal chronological access.",
+      "blocked_by": "Symplectic/signed restrictions and physical basis, precision, storage, tape and compiler costs are unresolved."
+    }
+  ],
+  "upstream_refresh": {
+    "commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+    "priority_revision": 8,
+    "checked_at_utc": "2026-11-03T12:11:10.165020+00:00",
+    "selected_record_sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa"
+  },
+  "local_environment": {
+    "implementation": "CPython",
+    "python": "3.12.15",
+    "platform": "macOS-27.0.1-arm64-arm-64bit",
+    "machine": "arm64",
+    "interpreter": "/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12"
+  }
+}
diff --git a/research/two-capacity-uniform-codec/VERIFY.json b/research/two-capacity-uniform-codec/VERIFY.json
new file mode 100644
index 0000000000..98f032ec46
--- /dev/null
+++ b/research/two-capacity-uniform-codec/VERIFY.json
@@ -0,0 +1,32 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Exact rank/unrank against literal matrix sets, finite fair-bit frequencies and exhaustion, large selected ranks, source bindings and fourteen rejection controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-W",
+        "error",
+        "-O",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "The same complete finite verification with assertions disabled."
+    }
+  ]
+}
diff --git a/research/two-capacity-uniform-codec/codec.py b/research/two-capacity-uniform-codec/codec.py
new file mode 100644
index 0000000000..ee20440f05
--- /dev/null
+++ b/research/two-capacity-uniform-codec/codec.py
@@ -0,0 +1,161 @@
+"""Exact enumerative construction of two-capacity completions.
+
+Produced by Nick Petalas. Apache-2.0.
+"""
+
+from dataclasses import dataclass
+from itertools import product
+from math import isqrt
+
+from count import count
+from linear import apply, basis, coordinates, require
+
+
+def draw_rank(total, bits):
+    """Recycle fair bits; return (rank or None, bits consumed) on finite input."""
+    require(type(total) is int and 1 <= total < 2**4096, "Invalid sample cardinality")
+    require(type(bits) is tuple and len(bits) <= 4096
+            and all(type(bit) is int and bit in (0, 1) for bit in bits),
+            "Expected at most 4096 canonical bits")
+    if total == 1:
+        return 0, 0
+    width, value = 1, 0
+    for used, bit in enumerate(bits, 1):
+        width *= 2
+        value = 2 * value + bit
+        if width >= total:
+            if value < total:
+                return value, used
+            width -= total
+            value -= total
+        require(0 <= value < width < total, "Invalid residual uniform interval")
+    return None, len(bits)
+
+
+@dataclass(frozen=True)
+class Contract:
+    n: int
+    prime: int
+    fixed: tuple
+    capacities: tuple
+
+    def __post_init__(self):
+        require(type(self.n) is int and 0 <= self.n <= 12, "Dimension outside 0..12")
+        p = self.prime
+        require(type(p) is int and 2 <= p <= 31
+                and all(p % d for d in range(2, isqrt(p) + 1)), "Unsupported prime")
+        require(p**self.n <= 4096, "Candidate vector budget exceeds 4096")
+        require(type(self.fixed) is tuple and len(self.fixed) <= self.n,
+                "Invalid fixed injection")
+        require(type(self.capacities) is tuple and len(self.capacities) == 2,
+                "Exactly two capacities required")
+        for pair in self.fixed:
+            require(type(pair) is tuple and len(pair) == 2, "Invalid fixed pair")
+            for vector in pair:
+                self.check_vector(vector)
+        for pair in self.capacities:
+            require(type(pair) is tuple and len(pair) == 2, "Invalid capacity pair")
+            for rows in pair:
+                require(type(rows) is tuple and len(rows) <= self.n, "Invalid subspace basis")
+                for vector in rows:
+                    self.check_vector(vector)
+                require(len(basis(rows, self.n, p)) == len(rows), "Dependent capacity basis")
+        for side in range(2):
+            require(len(basis(tuple(pair[side] for pair in self.fixed), self.n, p))
+                    == len(self.fixed), "Dependent fixed injection")
+
+    def check_vector(self, vector):
+        require(type(vector) is tuple and len(vector) == self.n
+                and all(type(x) is int and 0 <= x < self.prime for x in vector),
+                "Noncanonical field vector")
+
+
+class Codec:
+    def __init__(self, contract):
+        require(type(contract) is Contract, "Expected a validated Contract")
+        self.contract = contract
+        self.count_calls = 0
+        self.total = self.weight(contract.fixed)
+        domain = tuple(x for x, _ in contract.fixed)
+        complement = []
+        for i in range(contract.n):
+            vector = tuple(int(i == j) for j in range(contract.n))
+            if len(basis(domain + tuple(complement) + (vector,), contract.n,
+                         contract.prime)) > len(domain) + len(complement):
+                complement.append(vector)
+        self.complement = tuple(complement)
+        require(len(domain) + len(self.complement) == contract.n, "Incomplete domain basis")
+
+    def weight(self, fixed):
+        self.count_calls += 1
+        c = self.contract
+        return count(c.n, c.prime, fixed, c.capacities)
+
+    def branches(self, fixed, source):
+        c = self.contract
+        images = tuple(y for _, y in fixed)
+        for vector in product(range(c.prime), repeat=c.n):
+            if len(basis(images + (vector,), c.n, c.prime)) == len(images):
+                yield vector, 0
+            else:
+                yield vector, self.weight(fixed + ((source, vector),))
+
+    def unrank(self, index):
+        require(type(index) is int and 0 <= index < self.total, "Rank outside completion set")
+        fixed = self.contract.fixed
+        for source in self.complement:
+            found = False
+            for image, weight in self.branches(fixed, source):
+                if index < weight:
+                    fixed += ((source, image),)
+                    found = True
+                    break
+                index -= weight
+            require(found, "Conditional counts do not partition parent")
+        require(index == 0, "Nonunit leaf count")
+        c = self.contract
+        domain = tuple(x for x, _ in fixed)
+        images = tuple(y for _, y in fixed)
+        columns = []
+        for i in range(c.n):
+            vector = tuple(int(i == k) for k in range(c.n))
+            coefficients = coordinates(domain, vector, c.prime)
+            columns.append(tuple(sum(a * y[j] for a, y in zip(coefficients, images)) % c.prime
+                                 for j in range(c.n)))
+        return tuple(columns)
+
+    def rank(self, columns):
+        self.check_completion(columns)
+        c, fixed, index = self.contract, self.contract.fixed, 0
+        for source in self.complement:
+            actual = apply(columns, source, c.prime)
+            found = False
+            for image, weight in self.branches(fixed, source):
+                if image == actual:
+                    require(weight > 0, "Completion has zero conditional count")
+                    fixed += ((source, image),)
+                    found = True
+                    break
+                index += weight
+            require(found, "Missing image branch")
+        require(0 <= index < self.total, "Encoded rank outside completion set")
+        return index
+
+    def check_completion(self, columns):
+        c = self.contract
+        require(type(columns) is tuple and len(columns) == c.n, "Invalid matrix columns")
+        for vector in columns:
+            c.check_vector(vector)
+        require(len(basis(columns, c.n, c.prime)) == c.n, "Singular completion")
+        require(all(apply(columns, x, c.prime) == y for x, y in c.fixed),
+                "Prescribed injection changed")
+        for source, target in c.capacities:
+            require(all(len(basis(target + (apply(columns, x, c.prime),), c.n,
+                                  c.prime)) == len(target) for x in source),
+                    "Capacity violated")
+
+    def sample(self, bits):
+        """Uniform on success for independent fair bits; report budget exhaustion."""
+        require(self.total > 0, "Cannot sample an empty completion set")
+        index, used = draw_rank(self.total, bits)
+        return (None if index is None else self.unrank(index)), used
diff --git a/research/two-capacity-uniform-codec/count.py b/research/two-capacity-uniform-codec/count.py
new file mode 100644
index 0000000000..bb606007fb
--- /dev/null
+++ b/research/two-capacity-uniform-codec/count.py
@@ -0,0 +1,73 @@
+"""Conditional count oracle from Ali Romman's PR6539, Theorem 1.
+
+This is a direct implementation of the cited formula, not a new count theorem.
+Apache-2.0.
+"""
+
+from math import prod
+
+from linear import basis, intersection, mapped, require
+
+
+def injections(n, k, prime):
+    if not 0 <= k <= n:
+        return 0
+    return prod(prime**n - prime**i for i in range(k))
+
+
+def gaussian(n, k, prime):
+    if not 0 <= k <= n:
+        return 0
+    numerator = prod(prime**(n - i) - 1 for i in range(k))
+    denominator = prod(prime**(k - i) - 1 for i in range(k))
+    require(numerator % denominator == 0, "Nonintegral Gaussian coefficient")
+    return numerator // denominator
+
+
+def formula(prime, n, u, a, b, s, c, d, t, k, ell, ec, ed, ecd):
+    if a > c or b > d or s > t or k > ell:
+        return 0
+    j, tau = a + b - s, c + d - t
+    alpha, beta, common_dimension = a - j, b - j, tau - j
+    require(0 <= k <= j and 0 <= j - k <= tau - ell,
+            "Invalid common-quotient dimensions")
+    summands = []
+    for i in range(max(0, alpha - c + tau), min(alpha, common_dimension) + 1):
+        summands.append(gaussian(common_dimension, i, prime)
+                        * gaussian(c - tau, alpha - i, prime)
+                        * prime**((common_dimension - i) * (alpha - i))
+                        * injections(alpha, alpha, prime)
+                        * injections(d - j - i, beta, prime) * prime**(i * beta))
+    return (injections(ell, k, prime) * prime**(ell * (j - k))
+            * prime**(j * (alpha + beta)) * sum(summands)
+            * prime**(ecd * j + ec * alpha + ed * beta)
+            * prod(prime**n - prime**i for i in range(u + s, n)))
+
+
+def count(n, prime, fixed, capacities):
+    """Inputs are validated by Contract; every added fixed pair is independent."""
+    domain = basis(tuple(x for x, _ in fixed), n, prime)
+    image = basis(tuple(y for _, y in fixed), n, prime)
+    require(len(domain) == len(image) == len(fixed), "Noninjective prefix")
+    (a_space, c_space), (b_space, d_space) = capacities
+    source_sum = basis(a_space + b_space, n, prime)
+    target_sum = basis(c_space + d_space, n, prime)
+    ua = intersection(domain, a_space, n, prime)
+    ub = intersection(domain, b_space, n, prime)
+    u0 = intersection(domain, source_sum, n, prime)
+    for source, target in ((ua, c_space), (ub, d_space), (u0, target_sum)):
+        if len(basis(mapped(source, fixed, n, prime) + target, n, prime)) != len(target):
+            return 0
+    ec = intersection(image, c_space, n, prime)
+    ed = intersection(image, d_space, n, prime)
+    ecd = intersection(ec, ed, n, prime)
+    z_space = basis(ec + ed, n, prime)
+    k = (len(intersection(a_space, b_space, n, prime))
+         + len(intersection(mapped(u0, fixed, n, prime), z_space, n, prime))
+         - len(ua) - len(ub))
+    return formula(prime, n, len(domain), len(a_space) - len(ua),
+                   len(b_space) - len(ub), len(source_sum) - len(u0),
+                   len(c_space) - len(ec), len(d_space) - len(ed),
+                   len(target_sum) - len(intersection(image, target_sum, n, prime)),
+                   k, len(intersection(c_space, d_space, n, prime)) - len(ecd),
+                   len(ec), len(ed), len(ecd))
diff --git a/research/two-capacity-uniform-codec/linear.py b/research/two-capacity-uniform-codec/linear.py
new file mode 100644
index 0000000000..cfe99dfe0e
--- /dev/null
+++ b/research/two-capacity-uniform-codec/linear.py
@@ -0,0 +1,81 @@
+"""Small exact prime-field linear algebra. Apache-2.0."""
+
+
+def require(condition, message):
+    if not condition:
+        raise ValueError(message)
+
+
+def reduce_system(width, equations, prime):
+    rows = [list(row) for row in equations]
+    pivots = []
+    for column in range(width):
+        pivot = next((i for i in range(len(pivots), len(rows))
+                      if rows[i][column] % prime), None)
+        if pivot is None:
+            continue
+        index = len(pivots)
+        rows[index], rows[pivot] = rows[pivot], rows[index]
+        inverse = pow(rows[index][column], -1, prime)
+        rows[index] = [x * inverse % prime for x in rows[index]]
+        for i in range(len(rows)):
+            if i != index:
+                coefficient = rows[i][column]
+                rows[i] = [(x - coefficient * y) % prime
+                           for x, y in zip(rows[i], rows[index])]
+        pivots.append(column)
+    if any(not any(row[:width]) and row[width] for row in rows):
+        return None
+    return tuple(tuple(row) for row in rows[:len(pivots)]), tuple(pivots)
+
+
+def basis(rows, n, prime):
+    reduced = reduce_system(n, [tuple(row) + (0,) for row in rows], prime)
+    return tuple(row[:n] for row in reduced[0])
+
+
+def orthogonal(rows, n, prime):
+    reduced, pivots = reduce_system(n, [tuple(row) + (0,) for row in rows], prime)
+    answer = []
+    for free in range(n):
+        if free not in pivots:
+            vector = [0] * n
+            vector[free] = 1
+            for row, pivot in zip(reduced, pivots):
+                vector[pivot] = -row[free] % prime
+            answer.append(tuple(vector))
+    return tuple(answer)
+
+
+def intersection(left, right, n, prime):
+    return orthogonal(orthogonal(left, n, prime) + orthogonal(right, n, prime),
+                      n, prime)
+
+
+def coordinates(rows, vector, prime):
+    equations = [tuple(row[i] for row in rows) + (entry,)
+                 for i, entry in enumerate(vector)]
+    result = reduce_system(len(rows), equations, prime)
+    require(result is not None, "Vector outside prescribed domain")
+    reduced, pivots = result
+    require(len(pivots) == len(rows), "Dependent prescribed domain")
+    answer = [0] * len(rows)
+    for row, pivot in zip(reduced, pivots):
+        answer[pivot] = row[-1]
+    return tuple(answer)
+
+
+def apply(columns, vector, prime):
+    return tuple(sum(x * column[i] for x, column in zip(vector, columns)) % prime
+                 for i in range(len(vector)))
+
+
+def mapped(rows, fixed, n, prime):
+    domain = tuple(pair[0] for pair in fixed)
+    images = tuple(pair[1] for pair in fixed)
+    answer = []
+    for row in rows:
+        coefficients = coordinates(domain, row, prime)
+        answer.append(tuple(sum(c * y[i] for c, y in zip(coefficients, images)) % prime
+                            for i in range(n)))
+    return basis(tuple(answer), n, prime)
diff --git a/research/two-capacity-uniform-codec/source/PR6539-NOTICE b/research/two-capacity-uniform-codec/source/PR6539-NOTICE
new file mode 100644
index 0000000000..50762aa4f8
--- /dev/null
+++ b/research/two-capacity-uniform-codec/source/PR6539-NOTICE
@@ -0,0 +1,4 @@
+New count and checks: Ali Romman with substantial OpenAI Codex assistance.
+Apache-2.0. No subagents.
+ToikY retains PR6535's quotient theorem. Nick Petalas retains PR6489's nested count.
+Read inputs/pr6535-NOTICE and inputs/pr6533-completion.py for full retained credit.
diff --git a/research/two-capacity-uniform-codec/source/PR6539-PROOF.md b/research/two-capacity-uniform-codec/source/PR6539-PROOF.md
new file mode 100644
index 0000000000..0a835ca8de
--- /dev/null
+++ b/research/two-capacity-uniform-codec/source/PR6539-PROOF.md
@@ -0,0 +1,210 @@
+# Exact finite-field count for two simultaneous capacities
+
+## Contract and prior theorem
+
+Let V and W have dimension n over F_q. Let h:U→W be an injection, with
+u=dim U and E=h(U). Require an isomorphism g:V→W such that
+
+`g|U=h`, `g(A)⊂C`, `g(B)⊂D`.
+
+All inclusions allow equality. A and B need not be nested. C and D need not
+be nested. ToikY's PR6535 gives the exact feasibility criterion and its
+quotient proof. Nick Petalas's PR6489 gives the prior nested count.
+Ali Romman's PR6533 counts arbitrary finite capacity families by an
+exponential kernel lattice. Here we count every completion for exactly two
+capacities by a sum with at most n+1 terms. These prior results retain credit.
+
+Set UA=U∩A, UB=U∩B, U0=U∩(A+B), and Z=(E∩C)+(E∩D). First require
+
+`h(UA)⊂C`, `h(UB)⊂D`, `h(U0)⊂C+D`.
+
+If any test fails, the count is zero. Define
+
+| Symbol | Dimension |
+| --- | --- |
+| a,b | dim A-dim UA, dim B-dim UB |
+| s | dim(A+B)-dim U0 |
+| c,d | dim C-dim(E∩C), dim D-dim(E∩D) |
+| t | dim(C+D)-dim(E∩(C+D)) |
+| j | a+b-s |
+| tau | c+d-t |
+| ell | dim(C∩D)-dim(E∩C∩D) |
+| k | dim(A∩B)+dim(h(U0)∩Z)-dim UA-dim UB |
+| eC,eD,eCD | dim(E∩C), dim(E∩D), dim(E∩C∩D) |
+
+If `a>c`, `b>d`, `s>t` or `k>ell`, the count is zero. For the remaining
+case put `alpha=a-j`, `beta=b-j`, and `H=tau-j`. For a valid contract the
+prior exact sequence also gives `0≤j-k≤tau-ell`, hence H≥0.
+
+Write
+
+`Inj(m,r) = product_(i=0)^(r-1) (q^m-q^i)`
+
+for the number of injections from a fixed r-dimensional space into a fixed
+m-dimensional space. It is zero if r<0 or r>m. Empty products are one.
+Write `[m choose r]_q` for the Gaussian binomial coefficient, with value zero
+outside 0≤r≤m.
+
+## Closed formula
+
+Define
+
+```text
+S = sum_i [H choose i]_q [c-tau choose alpha-i]_q
+          q^((H-i)(alpha-i)) Inj(alpha,alpha)
+          Inj(d-j-i,beta) q^(i beta),
+
+max(0,alpha-c+tau) <= i <= min(alpha,H).
+```
+
+Then the exact number of completions is
+
+```text
+Inj(ell,k) q^(ell(j-k))
+  * q^(j(alpha+beta)) S
+  * q^(eCD*j+eC*alpha+eD*beta)
+  * product_(i=u+s)^(n-1) (q^n-q^i).
+```
+
+This integer formula holds over every finite field, including nonprime fields.
+The first factor uses ker(delta), not the whole common source quotient. That
+distinction is required by the nonzero-delta example below.
+
+The formula uses at most n+1 summands and O(n^2) integer multiplications and
+exact divisions with direct Gaussian products. This statement concerns the
+formula arithmetic, not bit complexity, field-order validation or input basis
+reduction. The API checks prime-power orders; its simple trial-division check
+is not claimed optimal in log q. No subspace lattice is enumerated by the
+counting routine.
+
+## 1. Count the injective common lifts
+
+Use the source theorem's quotients
+
+`Abar=(A+U)/U`, `Bbar=(B+U)/U`, `J=Abar∩Bbar`,
+`Cbar=(C+E)/E`, `Dbar=(D+E)/E`, `T=Cbar∩Dbar`.
+
+There is an exact sequence
+
+`0→H0→T --rho--> (E∩(C+D))/Z →0`,
+
+where H0 is the image of C∩D modulo E. Its dimension is ell. The prescribed
+map induces delta:J→(E∩(C+D))/Z, with dim J=j and dim ker(delta)=k.
+Any quotient completion restricts to an injective j0:J→T satisfying
+`rho j0=delta`.
+
+Choose a fixed complement of ker(delta) in J and a fixed section of rho.
+There are Inj(ell,k) choices for j0 on ker(delta). On its j-k dimensional
+complement, each prescribed quotient vector has q^ell lifts. All those
+choices are independent. They remain independent from j0(ker(delta)), since
+delta is injective on that complement. Thus there are
+
+`Inj(ell,k) q^(ell(j-k))`
+
+injective common lifts. No basis choice is counted twice: the source basis
+and complements are fixed during this count.
+
+## 2. Extend the quotient map inside the two capacities
+
+Fix one j0 and write L=j0(J). Quotient the target capacities by L. Their
+dimensions are c-j and d-j, and their intersection has dimension H=tau-j.
+The remaining source parts have dimensions alpha and beta and have zero
+intersection. Choose the image P of the alpha-dimensional source part in
+Cbar/L, and put i=dim(P∩(T/L)).
+
+The number of such P is the classical subspace-intersection count
+
+`[H choose i]_q [c-tau choose alpha-i]_q q^((H-i)(alpha-i))`.
+
+Indeed choose its intersection in T/L, choose its projection in a fixed
+complement of T/L in Cbar/L, and choose the graph map from that projection
+to (T/L)/(P∩T/L). The graph has (H-i)(alpha-i) free field entries.
+There are Inj(alpha,alpha) isomorphisms from the fixed first source part to P.
+
+The second source part must map into Dbar/L with image disjoint from P.
+The intersection of P with Dbar/L has dimension i. An injection modulo that
+intersection has Inj(d-j-i,beta) choices. Its beta vectors have q^(i beta)
+independent lifts. Summing over i gives S.
+
+These choices specify the quotient map modulo L. Lifting the alpha+beta
+source basis vectors back through L gives q^(j(alpha+beta)) choices. This
+count depends only on dim L=j, so it is the same for every j0 in step1.
+
+## 3. Lift back through the fixed image E
+
+Fix a quotient map on (U+A+B)/U. The source theorem proves that compatible
+lifts exist; its common-lift condition is exactly what removes the paired
+representative discrepancy. The set of such lifts is an affine space.
+Differences between two lifts vanish on U and map Abar into E∩C and Bbar
+into E∩D. Their common J values must agree, so they lie in E∩C∩D.
+Choose fixed complements of J in Abar and Bbar. The independent free entries
+have dimension
+
+`eCD*j+eC*alpha+eD*beta`.
+
+Therefore this step has exactly the third power-of-q factor. Every resulting
+map on U+A+B is injective: its quotient is injective, and its kernel on U is
+zero because h is injective.
+
+## 4. Complete the ambient basis
+
+The fixed domain U+A+B now has dimension u+s and has an injective image.
+For each remaining domain basis vector, choose its image outside the span
+of all preceding image vectors. This gives the last product. Multiplying
+the four independent counts proves the formula.
+
+In particular, the formula is symmetric under exchange of (A,C) and (B,D),
+although the displayed sum treats the first source part first. This is also
+checked directly in every positive finite census case.
+
+## Discriminating examples
+
+For the source oblique example in dimension3,
+
+```text
+U=E=<e1,e2>, h=identity,
+A=<e1+e3>, B=<e3>, C=<e1,e3>, D=<e1,e2+e3>,
+```
+
+one has k=1 and ell=0. The count is zero. Each separate capacity can be
+satisfied, so separate counts cannot be multiplied.
+
+For `U=<e1-e2>`, h=identity, `A=C=<e1>` and `B=D=<e2>` in dimension2,
+delta has rank1, while k=ell=0. There is exactly one completion, the identity.
+Replacing k by j would incorrectly give zero.
+
+With no capacities the formula is the ordinary fixed-injection extension
+product. With two complementary source blocks of size r and target blocks
+of size r, each enlarged by E, the count is
+`q^(2ur) |GL_r(F_q)|^2`. With r coupled differences fixed between two target
+blocks, the constraints force the identity on both blocks; only the remaining
+ambient basis extension is free. These independent product formulas also
+check the large-dimensional cases in the receipt.
+
+## Evidence and limits
+
+The independent literal engine enumerates vector sets and complete GL actions.
+It uses the polynomial x^2+x+1 for F4 and ordinary arithmetic for prime fields.
+The full normalized census covers all fixed ranks in F2 dimensions0–3 and
+F3/F4/F5 dimension2: 287,431 contracts, including 64,525 positive counts.
+This is a count census, not just agreement of zero/nonzero decisions.
+Independent changes of source and target bases put every prescribed injection
+of a given rank in this normalized form.
+
+Seventy-eight further contracts with arbitrary prescribed images agree with
+PR6533's affine kernel-lattice rank count. Six named controls preserve the
+oblique and nonzero-delta cases over F2/F3/F5. Sixteen dimension120 formulas
+over field orders2,3,4,9 agree with separate product counts. Two literal
+48-dimensional vector contracts agree as well. Four omitted-factor controls,
+seven invalid inputs and three actual source-byte corruptions are rejected.
+
+The proof is the all-field result. Finite checks corroborate it; they do not
+replace it. The executable basis extractor uses prime fields. The scalar
+formula accepts every prime-power order, with F4 checked independently.
+The routine counts invertible completions only. It does not count every
+singular rank, sample completions, or emit a native operator.
+
+All spaces here are unrestricted linear spaces. Symplectic form, signed phase,
+causal access, dirty restoration, physical routing, scalar/basis cost, precision,
+stock, tape, compiler and outer costs remain separate. No actual selected
+contact, supplier admission, new kappa or selected-frontier change follows.
diff --git a/research/two-capacity-uniform-codec/verify.py b/research/two-capacity-uniform-codec/verify.py
new file mode 100644
index 0000000000..a9ff361c3d
--- /dev/null
+++ b/research/two-capacity-uniform-codec/verify.py
@@ -0,0 +1,237 @@
+"""Literal conformance checks for the new construction. Apache-2.0."""
+
+import argparse
+import hashlib
+import json
+from itertools import combinations, permutations, product
+from pathlib import Path
+import time
+
+from codec import Codec, Contract, draw_rank
+from linear import apply, require
+
+
+ROOT = Path(__file__).resolve().parent
+
+
+def verify_sources():
+    manifest = json.loads((ROOT / "SOURCES.json").read_text())
+    prefix = ("https://github.com/aliromman/integer-mult-bounds/blob/"
+              "96c63f994af628f574c71dca0d7ed219cbfc70c2/")
+    for row in manifest["external_sources"]:
+        require(row["url"].startswith(prefix), "Unexpected predecessor source")
+        payload = (ROOT / row["local_path"]).read_bytes()
+        require(hashlib.sha256(payload).hexdigest() == row["sha256"],
+                "Predecessor source digest mismatch")
+        blob = b"blob " + str(len(payload)).encode() + b"\0" + payload
+        require(hashlib.sha1(blob).hexdigest() == row["git_blob"],
+                "Predecessor Git blob mismatch")
+    return len(manifest["external_sources"])
+
+
+def span(rows, n, prime):
+    return frozenset(tuple(sum(a * row[j] for a, row in zip(coefficients, rows)) % prime
+                           for j in range(n))
+                     for coefficients in product(range(prime), repeat=len(rows)))
+
+
+def determinant(columns, prime):
+    n, value = len(columns), 0
+    for order in permutations(range(n)):
+        inversions = sum(order[i] > order[j] for i in range(n) for j in range(i + 1, n))
+        term = (-1)**inversions
+        for i in range(n):
+            term *= columns[i][order[i]]
+        value += term
+    return value % prime
+
+
+def invertibles(n, prime):
+    require(n <= 3 and prime**(n * n) <= 1000, "Literal matrix budget exceeded")
+    vectors = tuple(product(range(prime), repeat=n))
+    return tuple(columns for columns in product(vectors, repeat=n)
+                 if determinant(columns, prime))
+
+
+def subspaces(n, prime):
+    """Independent span-set inventory; keep the first basis for each set."""
+    require(n <= 2, "Literal subspace budget exceeded")
+    vectors = tuple(product(range(prime), repeat=n))
+    result = {}
+    for size in range(n + 1):
+        for rows in combinations(vectors, size):
+            elements = span(rows, n, prime)
+            if len(elements) == prime**size:
+                result.setdefault(elements, rows)
+    return tuple(result.values())
+
+
+def literal_completions(contract, matrices):
+    c = contract
+    result = []
+    for columns in matrices:
+        if any(apply(columns, x, c.prime) != y for x, y in c.fixed):
+            continue
+        if all(all(apply(columns, x, c.prime) in span(target, c.n, c.prime)
+                   for x in source) for source, target in c.capacities):
+            result.append(columns)
+    return result
+
+
+def check_contract(contract, matrices):
+    codec = Codec(contract)
+    expected = literal_completions(contract, matrices)
+    expected.sort(key=lambda columns: tuple(apply(columns, x, contract.prime)
+                                            for x in codec.complement))
+    require(codec.total == len(expected), "Wrong construction cardinality")
+    for index, columns in enumerate(expected):
+        before = codec.count_calls
+        require(codec.unrank(index) == columns, "Unrank disagrees with literal ordered set")
+        require(codec.count_calls - before <= len(codec.complement) * contract.prime**contract.n,
+                "Unrank exceeded the proved conditional-count bound")
+        before = codec.count_calls
+        require(codec.rank(columns) == index, "Rank disagrees with literal ordered set")
+        require(codec.count_calls - before <= len(codec.complement) * contract.prime**contract.n,
+                "Rank exceeded the proved conditional-count bound")
+    return len(expected)
+
+
+def full_small_census():
+    contracts, endpoints, positive = 0, 0, 0
+    for prime, n in ((2, 0), (2, 1), (2, 2), (3, 1)):
+        spaces, matrices = subspaces(n, prime), invertibles(n, prime)
+        standard = tuple(tuple(int(i == j) for j in range(n)) for i in range(n))
+        for fixed_rank in range(n + 1):
+            fixed = tuple((e, e) for e in standard[:fixed_rank])
+            for a, b, c, d in product(spaces, repeat=4):
+                contract = Contract(n, prime, fixed, ((a, c), (b, d)))
+                size = check_contract(contract, matrices)
+                contracts += 1
+                endpoints += size
+                positive += bool(size)
+    return {"contracts": contracts, "positive_contracts": positive,
+            "rank_unrank_endpoints": endpoints}
+
+
+def nonnormalized_and_larger():
+    contracts, endpoints = 0, 0
+    for prime, n in ((3, 2), (5, 2), (2, 3)):
+        standard = tuple(tuple(int(i == j) for j in range(n)) for i in range(n))
+        e, f = standard[:2]
+        diagonal = tuple((x + y) % prime for x, y in zip(e, f))
+        configs = [Contract(n, prime, (), (((), ()), ((), ()))),
+                   Contract(n, prime, ((diagonal, e),), (((), ()), ((), ()))),
+                   Contract(n, prime, (), (((e,), (f,)), ((f,), (e,)))),
+                   Contract(n, prime, ((diagonal, diagonal),),
+                            (((e,), (e,)), ((f,), (f,))))]
+        if n == 3:
+            z = standard[2]
+            configs.extend([Contract(n, prime, ((e, f),),
+                                     (((e, z), (e, f)), ((f, z), (f, z)))),
+                            Contract(n, prime, ((e, e), (f, f)),
+                                     (((diagonal,), (e,)), ((z,), (z,))))])
+        matrices = invertibles(n, prime)
+        for contract in configs:
+            endpoints += check_contract(contract, matrices)
+            contracts += 1
+    return {"contracts": contracts, "rank_unrank_endpoints": endpoints}
+
+
+def entropy_census():
+    cases, words, completion_samples = 0, 0, 0
+    for total in range(1, 13):
+        for budget in range(11):
+            frequencies, exhausted = [0] * total, 0
+            for bits in product((0, 1), repeat=budget):
+                index, used = draw_rank(total, bits)
+                require(0 <= used <= budget, "Invalid bit consumption")
+                if index is None:
+                    exhausted += 1
+                else:
+                    frequencies[index] += 1
+                words += 1
+            require(len(set(frequencies)) == 1, "Sampler has unequal output probabilities")
+            require(exhausted == 2**budget % total, "Wrong exact exhaustion probability")
+            cases += 1
+    codec = Codec(Contract(2, 2, (), (((), ()), ((), ()))))
+    expected = {codec.unrank(i): 0 for i in range(codec.total)}
+    for bits in product((0, 1), repeat=8):
+        columns, _ = codec.sample(bits)
+        if columns is not None:
+            expected[columns] += 1
+            completion_samples += 1
+    require(set(expected.values()) == {42}, "Completion samples are not exactly uniform")
+    return {"cardinality_budget_pairs": cases, "bit_strings": words,
+            "successful_completion_samples": completion_samples}
+
+
+def large_round_trips():
+    n, prime = 8, 2
+    standard = tuple(tuple(int(i == j) for j in range(n)) for i in range(n))
+    configs = [Contract(n, prime, (), (((), ()), ((), ()))),
+               Contract(n, prime, ((standard[0], standard[-1]),),
+                        (((standard[1],), (standard[0], standard[1])),
+                         ((standard[2],), (standard[2], standard[3]))))]
+    result = []
+    for contract in configs:
+        codec = Codec(contract)
+        indices = sorted({0, 1, codec.total // 3, codec.total // 2, codec.total - 1})
+        for index in indices:
+            columns = codec.unrank(index)
+            require(codec.rank(columns) == index, "Large exact round trip failed")
+            codec.check_completion(columns)
+        result.append({"dimension": n, "total": codec.total, "tested_ranks": indices,
+                       "count_calls": codec.count_calls})
+    return result
+
+
+def controls():
+    good = Contract(2, 2, (), (((), ()), ((), ())))
+    codec = Codec(good)
+    actions = [lambda: codec.unrank(-1), lambda: codec.unrank(codec.total),
+               lambda: codec.unrank(True), lambda: codec.rank(((0, 0), (0, 0))),
+               lambda: Contract(2, 4, (), (((), ()), ((), ()))),
+               lambda: Contract(13, 2, (), (((), ()), ((), ()))),
+               lambda: Contract(2, 2, (((1, 0), (0, 0)),), (((), ()), ((), ()))),
+               lambda: Contract(2, 2, (), ((((2, 0),), ()), ((), ()))),
+               lambda: draw_rank(0, (0,)), lambda: draw_rank(6, (2,)),
+               lambda: draw_rank(6, (0,) * 4097)]
+    constrained = Codec(Contract(2, 2, (((1, 0), (1, 0)),),
+                                 ((((0, 1),), ((0, 1),)), ((), ()))))
+    actions.append(lambda: constrained.rank(((0, 1), (1, 0))))
+    capacity = Codec(Contract(2, 2, (), ((((1, 0),), ((1, 0),)), ((), ()))))
+    actions.append(lambda: capacity.rank(((0, 1), (1, 0))))
+    empty = Codec(Contract(2, 2, (), ((((1, 0),), ()), ((), ()))))
+    require(empty.total == 0, "Empty fixture is not empty")
+    actions.append(lambda: empty.sample((0, 1)))
+    for action in actions:
+        try:
+            action()
+        except ValueError:
+            continue
+        raise ValueError("Invalid input was accepted")
+    return len(actions)
+
+
+def main():
+    parser = argparse.ArgumentParser(description=__doc__)
+    parser.add_argument("--receipt", type=Path)
+    args = parser.parse_args()
+    started = time.monotonic()
+    result = {"bound_predecessor_files": verify_sources(),
+              "small_census": full_small_census(),
+              "additional_census": nonnormalized_and_larger(),
+              "entropy_census": entropy_census(),
+              "large_round_trips": large_round_trips(), "rejection_controls": controls()}
+    result["source_sha256"] = {str(path.relative_to(ROOT)): hashlib.sha256(path.read_bytes()).hexdigest()
+                               for path in sorted(ROOT.rglob("*")) if path.is_file()}
+    if args.receipt:
+        require(not args.receipt.resolve().is_relative_to(ROOT.parent.parent),
+                "Write receipts outside the checkout")
+        args.receipt.write_text(json.dumps(result, indent=2, sort_keys=True) + "\n")
+    print(json.dumps(result, sort_keys=True))
+    print(f"PASS_TWO_CAPACITY_UNIFORM_CODEC seconds={time.monotonic() - started:.3f}")
+
+
+if __name__ == "__main__":
+    main()

From 0abcc978aa8ec083c0017ee50d7788e85f1cba1a Mon Sep 17 00:00:00 2001
From: Nick Petalas <webmasternikos@gmail.com>
Date: Tue, 3 Nov 2026 12:53:23 +0000
Subject: [PATCH 2/2] fix(research): include dimension zero in the count bound

---
 research/two-capacity-uniform-codec/PROOF.md | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/research/two-capacity-uniform-codec/PROOF.md b/research/two-capacity-uniform-codec/PROOF.md
index 3bbe424ffe..7aa94f3223 100644
--- a/research/two-capacity-uniform-codec/PROOF.md
+++ b/research/two-capacity-uniform-codec/PROOF.md
@@ -148,8 +148,12 @@ Our direct oracle implementation uses O(n^4) field operations for basis
 calculations and O(n^2) integer products/divisions in the formula. The
 field-operation bound allows a separate linear solve for every mapped basis
 vector. It is not a bit-complexity bound. Every count is at most
-|GL_n(F_q)|<q^(n^2), so count integers have O(n^2 log q) bits. Reconstruction
-of standard columns takes O(n^4) further field operations. The fair-bit
+|GL_n(F_q)|≤q^(n^2), with equality in the latter bound only at n=0, where
+there is one empty isomorphism. For n≥1 the zero matrix is singular, so the
+inequality is strict. Count integers therefore have O(1+n^2 log q) bits,
+recovering O(n^2 log q) for n≥1. At n=0, the unique rank is zero and the
+M=1 sampling case in Sections 2 and 3 already applies. Reconstruction of
+standard columns takes O(n^4) further field operations. The fair-bit
 recurrence uses O(b) arithmetic steps on integers smaller than 2M, followed
 by one unrank call on success.