Prove exact shared-map completion for nested capacities (no κ)

research/nested-late-capacity-completion/PROOF.md

@@ -0,0 +1,143 @@
+# Shared-map completion with nested late capacities
+
+This proof and construction were produced by Nick Petalas. Apache-2.0.
+
+## Contract and theorem
+
+Let V and W have the same finite dimension n over any field F. A fixed
+injective linear map h:U -> W has image U'. For i=1,...,k, let A_i be
+arbitrary subspaces of V and let C_1 <= ... <= C_k be subspaces of W.
+The requested map is an isomorphism g:V -> W extending h and satisfying
+g(A_i) <= C_i for every i. Inclusions may be equal, sources may overlap,
+and zero spaces, k=0 and n=0 are allowed.
+
+Put
+
+```
+S_i = A_1 + ... + A_i,
+u = dim U,  e_0 = 0,
+e_i = dim(U+S_i) - u,
+c_i = dim C_i,  b_i = dim(C_i intersect U').
+```
+
+Such a g exists if and only if, for every i,
+
+```
+h(U intersect S_i) <= C_i,             (compatibility)
+e_i <= c_i - b_i.                     (quotient capacity)
+```
+
+Over F_q, if these conditions hold, the exact number of requested maps is
+
+```
+product_(i=1..k) [q^(b_i (e_i-e_(i-1)))
+                 product_(j=e_(i-1)..e_i-1) (q^(c_i-b_i)-q^j)]
+  * product_(j=u+e_k..n-1) (q^n-q^j).
+```
+
+For k=0, read e_k=0. Empty products equal one. If any condition fails,
+the count is zero. The count covers distinct linear maps, without quotienting
+by basis choices or charging any physical realization cost.
+
+## Reduction to cumulative sources
+
+If g(A_j) <= C_j for j<=i, nesting gives g(A_j) <= C_i, hence
+g(S_i) <= C_i. Conversely A_i <= S_i, so the cumulative inclusions imply
+the original ones. This equivalence permits arbitrary source intersections;
+it requires nesting only on the target side.
+
+If g exists, its restriction to U intersect S_i is h and has image in C_i.
+The induced injection from (U+S_i)/U into W/U' sends the e_i-dimensional
+source into (C_i+U')/U', whose dimension is c_i-b_i. This proves necessity.
+
+## Compatible basis extension
+
+Choose a basis of U. Extend it successively to bases of U+S_i by choosing
+e_i-e_(i-1) new vectors in S_i. Such choices are possible because the
+cumulative sources form a flag. This ordered domain basis is fixed for
+the remainder of the proof and counting argument.
+
+Suppose an injective extension has already been defined on U+S_(i-1),
+and maps S_(i-1) into C_(i-1). Since S_(i-1) <= S_i,
+
+```
+(U+S_(i-1)) intersect S_i = (U intersect S_i) + S_(i-1).
+```
+
+The already prescribed image of this intersection lies in C_i, by
+compatibility and nesting. Thus extending by any images in C_i for the
+new independent domain vectors preserves the entire inclusion g(S_i)<=C_i.
+
+Work modulo U'. Images of the previous new basis vectors span an
+e_(i-1)-dimensional subspace of (C_i+U')/U'. The latter space has dimension
+c_i-b_i >= e_i. Extend these independent images to e_i independent vectors
+in this quotient, and lift each new vector to C_i. The resulting map on
+U+S_i is injective. This induction works over every field. Finally extend
+the domain and image bases to bases of V and W. It yields the required g.
+
+The bounded reference implements this same constructive choice without
+enumerating a field: an available member of a basis of C_i must lie outside
+the current image span whenever another independent image is needed.
+
+## Counting every completion
+
+Over F_q, fix the domain basis chosen above. At stage i, after a total of
+j new basis vectors have been assigned, where e_(i-1)<=j<e_i, the image
+span consists of U' plus j independent vectors that all lie in C_i.
+Its intersection with C_i therefore has dimension b_i+j. The next image
+can be any member of C_i outside that span. The exact number of choices is
+
+```
+q^c_i - q^(b_i+j) = q^b_i (q^(c_i-b_i)-q^j).
+```
+
+Multiplying these choices gives the stage factor in the theorem. Their
+number depends only on the stated dimensions, so all earlier choices
+receive exactly the same number of continuations. After the last contact,
+there are u+e_k independent assigned images. Each remaining domain basis
+vector has q^n-q^j choices when the current image span has dimension j.
+This gives the final factor.
+
+Every map has exactly one sequence of images of the fixed domain basis,
+and each allowed sequence produces exactly one map. Thus this counts all
+requested maps exactly once. No generic-position or infinite-field
+argument is used for the finite-field count.
+
+## A missed compatibility obstruction
+
+Over F_2, take V=W=F_2^3 with coordinate vectors x,y,z. Set
+
+```
+U = <x+y>,       h(x+y)=z,
+A_1=<x>,        C_1=<x>,
+A_2=<y>,        C_2=<x,y>.
+```
+
+The individual one-capacity contracts admit 4 and 12 isomorphisms,
+respectively. The first sends x to x, then y to x+z, and has four choices
+for the image of z outside their plane. The second has three nonzero
+choices in C_2 for the image of y, then fixes the image of x through h,
+and has four choices for the image of z. Yet no shared map exists:
+U <= S_2 and h(U)=<z> is not contained in C_2. This is a new joint-contract
+example, rather than a re-evaluation of PR5020's one-capacity examples.
+
+The quotient condition also detects a different missed obstruction. Take
+U=0, A_1=<x>, A_2=<y>, and C_1=C_2=<x>. Both individual contracts are
+feasible but S_2 has dimension two against a one-dimensional capacity.
+The exact reference and the separate literal GL census check both examples.
+
+## Scope and attribution
+
+Brian / JoyboyBrian's PR5020 supplies the one-capacity prescribed-map
+contract and asks for a second late capacity. The theorem above settles
+its nested-target case, and includes any finite number of nested targets.
+The proof is self-contained and does not invoke or recheck PR5020's theorem.
+Basis extension, quotient dimensions and finite-field independent-vector
+counts are classical; no general literature-priority claim is made.
+
+The unrestricted GL contract does not supply a symplectic native map,
+an absolute phase, chronological contact realization, a changed emitted
+word or a favorable complete paid/productive invoice. No helper credit,
+physical saving, new kappa, selected-frontier change or complete
+multiplication theorem follows. Nonnested targets require a different
+compatibility argument; applying this theorem to a nonnested list is invalid.

research/nested-late-capacity-completion/README.md

@@ -0,0 +1,159 @@
+# Exact shared maps for nested late capacities
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+Claim type: scoped written proof with exact finite corroboration. This
+settles the nested-target case of Brian / JoyboyBrian's
+[PR5020](https://github.com/CrocSwap/integer-mult-bounds/pull/5020),
+Open next question 2. It gives an exact feasibility criterion, construction
+and finite-field count for one prescribed injective map extended to an
+isomorphism meeting any finite list of nested late capacities. Sources
+may overlap arbitrarily and need not be nested. No new kappa is claimed.
+
+## Result and first discriminating example
+
+For h:U -> W injective, dim V=dim W=n, arbitrary sources A_i and nested
+capacities C_1 <= ... <= C_k, put
+
+```
+S_i = sum_(j<=i) A_j,    U' = h(U),    u = dim U,
+e_i = dim(U+S_i)-u,      c_i = dim C_i, b_i = dim(C_i intersect U').
+
+An invertible g extending h with g(A_i)<=C_i exists exactly when
+h(U intersect S_i)<=C_i and e_i<=c_i-b_i for every i.
+```
+
+[PROOF.md](PROOF.md) proves this over every field and counts every
+completion over F_q. Its exact count is
+
+```
+product_i q^(b_i*(e_i-e_(i-1)))
+          product_(e_(i-1)<=j<e_i) (q^(c_i-b_i)-q^j)
+  * product_(u+e_k<=j<n) (q^n-q^j),   e_0=0.
+```
+
+The count is zero when a condition fails. Empty products equal one.
+With no late constraints take e_k=0.
+
+Separate one-capacity tests miss relations between sources. In F_2^3,
+fix h(x+y)=z, request x -> <x> and y -> <x,y>. Each request alone
+admits a completion, with counts 4 and 12. Their shared contract admits
+zero because h(U intersect (A_1+A_2)) lies outside the final capacity.
+A second fixture has U=0 and two independent source lines directed into
+one common target line; it fails the cumulative quotient condition.
+
+The new step is the simultaneous cumulative-source theorem and its count.
+PR5020's one-capacity result, source-specific adapter and numbers are cited
+context and are not replayed. The investigation stops at this scoped result.
+
+## Exact evidence
+
+The independent census constructs subspaces as literal finite vector sets,
+enumerates invertible matrices by their complete vector permutations, and
+groups every possible prescribed partial injection by its literal action.
+For every source pair and nested target pair it compares the formula with
+the exact number of satisfying GL matrices. It uses no reference row reducer.
+
+| Field and dimension | Partial injections | Source/target/map cases |
+| --- | ---: | ---: |
+| F_2^0 | 1 | 1 |
+| F_2^1 | 2 | 24 |
+| F_2^2 | 16 | 4,800 |
+| F_3^2 | 81 | 43,740 |
+| F_5^2 | 625 | 840,000 |
+| F_2^3 | 512 | 8,650,752 |
+
+All 9,539,317 cases agree. Separately, 14,141 calls compare the bounded
+row-reduction reference count with literal census values; 3,119 constructor
+calls check existence, and every returned matrix is checked on complete
+vector permutations and literal source/target membership. The constructor
+also handles 112 attaining fixtures through dimension six, including empty,
+repeated and eight-stage target flags. Fourteen malformed boundary cases
+reject in both entry points. Checks use explicit exceptions under normal
+and optimized Python.
+
+Every run generates a JSON receipt with all six domain digests, counts,
+controls and SHA256 hashes of all seven package files. The verifier writes
+nothing; redirect stdout outside the checkout to retain the receipt.
+
+## Reproduce
+
+From the repository root, using CPython 3.12 and its standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/nested-late-capacity-completion/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/nested-late-capacity-completion/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/nested-late-capacity-completion
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/nested-late-capacity-completion --check-source-history
+```
+
+Any CPython 3.12 executable may replace the absolute path. Expected direct
+marker: `PASS_NESTED_LATE_CAPACITY_COMPLETION`. Both registered commands
+have 120-second limits. The direct verifier is self-contained in a Git-free
+copy of these seven files. The source README, selected record and task card
+are pinned historical provenance, not executable dependencies.
+
+## Scope, costs and credit
+
+The all-field conclusion rests on the written proof. The exhaustive
+execution covers only the six stated prime-field domains. The reference
+API accepts q in {2,3,5,7}, 0<=n<=6 and at most eight contacts; these are
+software limits, not theorem hypotheses. It requires basis tuples and
+rejects a noninjective prescribed map or nonnested targets.
+
+This is unrestricted linear-algebra completion. No actual selected-word
+contact is changed. Symplectic/native realization, absolute phases, source
+access, causal scheduling, arbitrary dirty restoration, basis preparation,
+delivery, productive target debits and the complete paid invoice remain
+open. Precision, stock, tape, compiler, outer admission and all five
+selected assumptions remain. No native build, selected scientific replay,
+Lean or Docker run was needed or performed. Independent human and formal
+proof-kernel review are unclaimed. The selected frontier is unchanged.
+
+Credit Brian / JoyboyBrian for PR5020 and the explicit second-capacity
+question; Cao Yifan / intqwq for PR4610's native-map caller; Nick Petalas
+for PR4919's different three-subspace correspondence theorem; codyw912
+for PR4735; and Cinna Davis, Dugongue, zxv, Jacob Alan Sussman and the
+retained native/compiler lineage. Basis extension and finite-field
+independent-vector counts are classical. No general literature-priority
+claim is made. Predecessor text and code are not copied or modified.
+
+The [advance CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19363406)
+records the scope. Canonical base is
+`7c49fe32c55de02c2c873655c804b16e4c3fef0a`, priority revision 8, selected
+PR6030. [TASK.json](TASK.json) records the explicit change from the
+coverage-law card to this shared-map feasibility side result. The selected
+orientation passed its metadata-only positive control. Live open/account
+PRs, recent claims, main README and merged/general-form searches were
+checked. Sparse historical notes, arbitrary diffs and unpublished work
+remain overlap-coverage limits.
+
+## Open next questions
+
+1. Extend the prescribed-map theorem to two nonnested target capacities.
+   Start with two intersecting binary planes and an oblique prescribed
+   subspace. Their coupled image choices are not decided by this flag proof.
+2. Bind a nested-capacity instance to an actual shared native operator.
+   Export every same-operator source/image condition and determine whether
+   its capacities form a flag. Phase/native realization and a complete
+   signed invoice block any claimed helper or kappa gain.
+
+The structured questions in [TASK.json](TASK.json) give first steps and
+blockers. No continuation or physical construction is reserved here.
+
+## Verifier bounds
+
+No function exceeds 60 physical lines and no call path recurses. The literal
+census has at most 25 vectors, 16 subspaces, 480 GL matrices and 66 target
+flags in a domain; it enumerates at most 625 candidate matrices. It retains
+counts as a digest rather than storing the millions of case records. The
+reference has at most six coordinates, twelve-column elimination matrices
+and eight contacts. Each package file is limited to 128 KiB when hashed.
+Warning-strict normal/optimized execution and in-memory syntax compilation
+supply diagnostics. Input failures propagate as explicit errors.
+
+Python exact integers, dataclasses, iterators and bounded collections allocate
+during execution. These are documented managed-runtime deviations from
+Power of Ten static allocation and indirect-call restrictions, not a
+constant-space physical implementation. There are no network, subprocess,
+write or persistent shared-state paths in the scientific verifier.

research/nested-late-capacity-completion/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": "research/multi-line-native-extension/README.md",
+      "usage": "provenance",
+      "git_blob": "655e6dba4e0850ad17d9947f075ad75a223884d7",
+      "sha256": "12074300d53cebd87ce4959f532c77af6a335a7f3101325e7e9f31d1473adc12"
+    }
+  ]
+}