Construct exact uniform two-capacity completions (no κ)

research/two-capacity-uniform-codec/PROOF.md

@@ -0,0 +1,172 @@
+# 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), 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.
+
+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.

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.

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