Solve exact partial-query acquisition at small codimension (no κ)

research/partial-query-optimum/ENGINEERING.md

@@ -0,0 +1,72 @@
+# Implementation bounds
+
+The exit predicate is a proved exact acquisition reduction, a bounded
+constructor and certificate checker agreeing with exhaustive subset optima,
+followed by one focused publication. The autonomous local run playbook was
+used. Build the Lever led to the reusable optimizer and certificate checker.
+Prove It Works led to literal subset and vector-set oracles and actual CLI
+replays, rather than inference from certificate self-consistency.
+
+## Code inspection
+
+The scope is optimizer.py and verify.py. All control flow is structured,
+without recursion, dynamic code generation, network access, mutable global
+caches or background tasks. Optimizer entry points validate width at most
+256, at most 4096 queries and 256 target vectors, integer costs in
+0..10^12, target inclusion in the query span, and codimension at most four.
+Booleans are rejected as integer inputs.
+
+There are at most 67 candidate subspaces. Producer span-extension layers
+number at most five and contain at most 67 canonical bases; each tries at
+most 15 new vectors. The independent checker enumerates at most 16 pivot
+sets and at most 16 free-entry assignments per set. A subspace vector set
+has at most 16 elements. Per-candidate elimination retains at most 256 rows.
+Dual construction reduces 256 ambient unit vectors. Input and certificate
+files are limited to eight million bytes. Certificates retain at most
+67*256 selected indices and dual vectors. No search-budget exhaustion is
+reported as mathematical infeasibility.
+
+The finite oracle uses at most seven queries, 128 subsets, eight vector
+values and 2187 cost assignments. The separate subspace oracle scans at
+most 32768 subsets containing zero and tests at most 256 XOR pairs each.
+CLI checks launch three serial subprocesses with 30-second timeouts, wait
+for their completion and inspect their return codes. Temporary files are
+owned by one context-managed directory and removed on every normal or
+exceptional exit. Set TMPDIR to the run's scratch directory for local replay.
+
+Explicit exception checks remain active under optimized Python. They check
+source hashes, target coverage, dual independence, eligible coverage,
+cheapest-basis exchanges, missing-target separators, complete quotient
+enumeration and the final minimum. The checker reconstructs actual vectors;
+it does not trust a reported rank or price. Malformed input rejects before
+optimization. Failed checks propagate; scientific success is never cached.
+
+All application functions fit within approximately sixty physical lines.
+Shared helpers operate on small explicit values; certificate verification
+does not call the optimizer. Both registered commands use isolated Python,
+warnings as errors and disabled bytecode writes. The direct and registered
+replays exercise the real optimizer and CLI. No external static analyzer or
+proof-kernel verification is claimed.
+
+## Managed-runtime deviation
+
+Rule: Power of Ten rule 3, allocation before steady operation.
+
+Location: optimizer.py and verify.py.
+
+Reason: CPython dynamically allocates arbitrary-precision integers, lists,
+sets and dictionaries. This exact one-shot program cannot disable runtime
+allocation while retaining its Python interface.
+
+Scope: bounded constructor, checker and finite corroboration only.
+
+Compensating control: enforced input caps, at most 67 candidate certificates,
+at most 256 rows per elimination and one current exhaustive instance. No
+unbounded queue, recursive stack or persistent cache exists.
+
+Verification: maximum-width/query-count case, maximum-codimension case,
+oversize rejection, exhaustive oracles and subprocess timeout checks.
+
+Follow-up: any native steady-operation implementation must allocate fixed
+capacity storage before taking over this interface. That implementation is
+outside this result.

research/partial-query-optimum/PROOF.md

@@ -0,0 +1,128 @@
+# Exact acquisition by quotient superspaces
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+## Contract and result
+
+Let K be a finite field of order q. Let v_1,...,v_n be vectors with
+nonnegative real acquisition costs a_i. Acquiring a subset S permits free
+linear reconstruction from its span. Let V=span(v_i), let U be a specified
+target subspace of V, and put c=dim(V)-dim(U). Costs are charged once per
+acquired index. Zero vectors, duplicates, zero costs, an empty query pool
+and U=0 are allowed.
+
+For every R<=V/U, let W_R be its inverse image under the quotient map, let
+E_R={i : v_i in W_R}, and let T_R=span(v_i : i in E_R). Compute a cheapest
+basis B_R from the indices E_R for T_R. Discard R if U is not contained
+in T_R. Then
+
+    OPT(U) = min_R sum_{i in B_R} a_i,
+
+over the retained candidates. There are exactly
+
+    N_q(c) = sum_{k=0}^c product_{j=0}^{k-1} (q^c-q^j)/(q^k-q^j)
+
+candidates. The number of weighted-basis problems depends only on target
+codimension. The empty product is one. For q=2 and c=0,1,2,3,4 the counts
+are 1,2,5,16,67. The executable covers q=2 and c<=4.
+
+This is an exact algorithm for additive acquisition. The finite-field
+restriction concerns bounded enumeration. The underlying reduction holds
+over any field if all superspaces can be considered. No polynomial bound
+in c, physical reconstruction cost or new multiplication exponent is asserted.
+
+## Proof of the reduction
+
+Every retained B_R spans U, so its acquisition is feasible and OPT(U) is at
+most its cost. Conversely, let S be an optimal feasible acquisition and put
+W=span(v_i : i in S). Since U<=W<=V, W is the inverse image of exactly one
+quotient subspace R. All indices of S belong to E_R. Therefore T_R=W:
+inclusion in W follows from eligibility, while the reverse inclusion follows
+from S. Remove dependent vectors from S to obtain a basis of W. Nonnegative
+costs ensure removal cannot increase cost. A cheapest basis B_R consequently
+costs at most S. That candidate is retained and attains OPT(U). Finiteness
+of the index set supplies an optimum, including at zero cost. There is always
+a retained candidate at W=V.
+
+The basis need not have rank dim(U). Paying for extra independent directions
+can be cheaper than buying queries entirely in U. It is also unnecessary
+that eligible queries span the entire W_R. The algorithm uses their actual
+span T_R and explicitly checks target coverage.
+
+## Counting and constructing quotient spaces
+
+The number of ordered independent k-tuples in K^c is product_j(q^c-q^j).
+Each k-dimensional subspace has exactly product_j(q^k-q^j) ordered bases.
+Division and summation prove N_q(c), the classical Gaussian binomial count.
+
+The constructor starts with the zero subspace and repeatedly adjoins every
+vector outside each current subspace. Every extension increases rank, and
+canonical reduced bases identify repetitions. Induction on rank proves
+completeness. The checker uses a different enumeration: choose all pivot
+positions, assign every permitted free entry in reduced row echelon form,
+then enumerate the resulting vector set. Unique reduced forms prove that
+it lists every quotient subspace exactly once. Both enumerations terminate
+after c rank layers. A third finite corroboration scans all vector subsets
+and tests closure under XOR for c<=4.
+
+To construct the quotient map, extend a basis of U to a basis of V and take
+the coordinate forms of the added elements. The checker accepts any c forms
+that vanish on U and map V onto K^c. Rank-nullity makes their kernel on V
+exactly U, so they parameterize the same complete superspace family. No
+favorable choice of quotient coordinates is assumed.
+
+## Checkable candidate optimality
+
+The binary certificate gives selected indices and dual forms d_j with
+d_j(v_i)=delta_ji on selected vectors. This proves independence. For every
+eligible v, the checker computes coordinates d_j(v), reconstructs v, and
+checks that every used selected index has price at most the price of v.
+The coordinates prove full eligible coverage and the absence of an improving
+single-element basis exchange.
+
+That exchange condition implies global cheapest-basis optimality. At every
+strict price threshold, all cheaper eligible vectors are spanned by cheaper
+selected vectors. Thus the selected cheap prefix has the full rank of the
+eligible cheap prefix. Every other basis contains at most that many cheap
+vectors. Summing these rank inequalities over the finite distinct prices,
+or pairing sorted basis prices, proves that every other basis costs at least
+as much. This is classical weighted linear-matroid greedy optimality,
+inherited from Ali Romman's PR5791 contract rather than a new matroid theorem.
+
+If a candidate cannot span U, its certificate supplies one target vector and
+a linear functional that is one there and zero on every eligible query.
+No eligible acquisition can obtain that target. Otherwise the checker
+reconstructs every target from the selected basis. After checking all
+quotient spaces, it checks the reported minimum. The certificate checker
+does not rerun global subset optimization.
+
+## First strict improvement and an interior necessity example
+
+For queries (1,2,3), prices (3,2,2), and target U=span(1) in F2^2, a cheapest
+whole-span basis buys 2 and 3 for four units. Both are needed to reconstruct
+the target in that basis. The new optimizer buys query 1 for three units.
+Here c=1, so only U and V are considered.
+
+For queries (1,2,3,4,7), prices (8,2,2,1,2), and target span(1) in F2^3,
+queries entirely in U cost eight. A cheapest whole-span basis costs five.
+The intermediate superspace span(1,2) has a four-unit basis (2,3), and four
+is optimal. Every query costs at least one; the sole one-unit vector is 4,
+and neither it nor any price-two vector is the target. A subset cheaper than
+four cannot span 1: XOR with the sole one-unit vector 4 sends the
+price-two vectors 2,3,7 to 6,7,3. This shows why considering only U and V is insufficient
+once c=2. No predecessor numerical result is used for either example.
+
+## Attribution and scope
+
+Ali Romman / PR5791 supplies whole-span acquisition, the partial-target
+question and its exchange certificate contract. Nick Petalas / PR5878 gives
+the earlier sharp c+1 guarantee for pruning a cheapest whole-span basis.
+The new step is the exact quotient-superspace reduction with a complete
+bounded optimizer and certificate. Quotient spaces, rank-nullity, Gaussian
+binomial counting and weighted matroid selection are classical tools.
+No literature-wide priority for enumerative optimization is claimed.
+
+This does not price XOR reconstruction, physical delivery, restoration,
+phase realization, storage or native legality. A source-to-query adapter,
+complete signed supplier invoice and all-size caller remain separate proof
+obligations. Independent human and formal proof-kernel review are unclaimed.

research/partial-query-optimum/README.md

@@ -0,0 +1,117 @@
+# Exact partial-query acquisition at small codimension
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+Claim type: scoped written proof and constructive optimizer with exact finite
+corroboration. Independent human and formal proof-kernel review are unclaimed.
+
+A target subspace U need not require the entire query span V. The new exact
+reduction considers every superspace of U through V/U, buys a cheapest basis
+of the queries eligible in that superspace, and takes the cheapest candidate
+that spans U. For a finite field of order q and c=dim(V)-dim(U), the number
+of candidates is the sum of the Gaussian binomial coefficients [c choose k]_q.
+It depends on target codimension. For binary c=0,1,2,3,4, the exact counts
+are 1,2,5,16,67. [PROOF.md](PROOF.md) proves the reduction for every finite
+field and arbitrary finite query pools with nonnegative costs.
+
+The executable handles binary width through 256, at most 4096 queries and
+256 target vectors, codimension through four, and integer prices through
+10^12. Zero prices, duplicate/zero queries and empty targets are included.
+The checker proves candidate independence, full eligible coverage and
+cheapest-basis exchange optimality, or checks a missing-target separator.
+An independent RREF enumeration checks that no quotient space was omitted.
+The constructor uses span extension. Neither executes predecessor code.
+
+For queries 1,2,3 with prices 3,2,2 and target 1, whole-span basis pruning
+pays four; the new optimum is three. At codimension two, an intermediate
+superspace can beat both the target space and the whole space. The proof
+gives a five-query example with respective optima eight, four and five.
+These are acquisition prices in a declared algebraic relaxation.
+
+## Reproduce
+
+From the repository root, with the standard library and CPython 3.12:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/partial-query-optimum/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/partial-query-optimum/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/partial-query-optimum
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/partial-query-optimum --check-source-history
+```
+
+Set TMPDIR to an existing private external scratch directory for the three
+short CLI subprocess checks. Another CPython 3.12 path may replace the local
+path. The scientific marker is PASS_PARTIAL_QUERY_OPTIMUM. Each replay
+prints a generated receipt bound to all eight package files by SHA256 and
+writes no persistent artifact. The registered runner executes both modes.
+
+For a new problem, write JSON with exactly these keys:
+
+```json
+{"width":2,"vectors":[1,2,3],"costs":[3,2,2],"targets":[1]}
+```
+
+Run `python3.12 -I -B research/partial-query-optimum/optimizer.py problem.json`
+and save stdout as certificate.json outside the checkout. Check that file
+with the same command followed by `--check certificate.json`. The minimum
+is three. Vectors are binary coordinate bitmasks encoded as JSON integers.
+The target must lie in the query span; unsupported domains reject explicitly.
+The certificate records all candidate bases, quotient forms and the winner.
+
+## Evidence and limits
+
+The complete finite replay compares every weighted seven-vector pool with
+prices in 0,1,2 against every target subspace of F2^3. A second complete
+family includes duplicate and zero queries. Its oracle enumerates purchased
+index subsets and literal XOR spans, without Gaussian elimination. Three
+independent quotient enumerators, malformed-input and certificate controls,
+maximum width/query count and codimension, and actual CLI production/checking
+are also exercised. The replay checks 36,207 exhaustive optima and 147,258 candidate bases,
+nine corrupted certificates, ten invalid problems and three CLI runs.
+The receipt reports these exact enumerated counts.
+
+The written argument establishes the quantified theorem. Finite evidence
+corroborates the bounded implementation. [ENGINEERING.md](ENGINEERING.md)
+states resource bounds and the managed-runtime allocation deviation.
+
+Linear reconstruction is free only in this acquisition model. XOR cost,
+physical delivery, phases, borrowed-state restoration, owned storage, native
+legality, precision, compiler closure and the full supplier/outer bill remain
+separate. No native, selected cold, Lean or Docker replay, new kappa,
+selected-frontier change or complete multiplication theorem is claimed.
+
+## Sources and overlap
+
+Ali Romman / [PR5791](https://github.com/CrocSwap/integer-mult-bounds/pull/5791)
+poses partial-target acquisition separately from its whole-span optimum.
+Its retained [guide](../../docs/research/binary-query-basis.md) is pinned as
+an authenticated documentary input, without executing its implementation.
+Nick Petalas / [PR5878](https://github.com/CrocSwap/integer-mult-bounds/pull/5878)
+gives the earlier sharp c+1 approximation guarantee for pruning any cheapest
+whole-span basis. That result is cited context, not replayed or audited.
+Classical quotient spaces, rank-nullity, Gaussian binomial counting and
+weighted linear-matroid greedy selection retain their credit. The new step
+is the exact small-codimension reduction and its certificate implementation;
+no literature-wide priority for enumerative optimization is claimed.
+
+The base is 7c49fe32c55de02c2c873655c804b16e4c3fef0a, priority revision eight.
+[SOURCES.json](SOURCES.json) pins the original card and selected record as
+historical provenance. [TASK.json](TASK.json) explicitly changes the formal
+interface card to this algebraic side result. The binding-only selected
+baseline passed; no selected scientific replay is inferred.
+
+The [advance CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19376723)
+followed live open-PR, recent-account, main README, merged-PR and handoff
+searches. Distinctive terms included partial-query acquisition, quotient
+subspaces, superspaces, codimension, Gaussian binomial and target-aware
+acquisition. Cached overlap has sparse local coverage; explicit Git searches
+covered main READMEs for those terms. This does not cover arbitrary historical
+diffs or unpublished work and is not a novelty certificate. No predecessor
+package or credit line is changed.
+
+## Open next questions
+
+Can one actual native helper caller satisfy this additive acquisition contract
+with an affordable reconstruction bill? Pin its query pool and target space,
+then price the winning acquisition, reconstruction, delivery, storage and
+restoration together. Missing source binding and physical tariffs block a
+supplier or kappa claim. The structured question is in TASK.json.

research/partial-query-optimum/SOURCES.json

@@ -0,0 +1,24 @@
+{
+  "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"
+    },
+    {
+      "path": "docs/research/binary-query-basis.md",
+      "usage": "input",
+      "git_blob": "291bce46071c77b76b17ddfc3571df676b95c529",
+      "sha256": "cd60665849910830381a6a5b0c8f0d10b4bc9e54d50286eeacaf200fffd6f660"
+    }
+  ]
+}