Prove sharp adaptive higher-rank minor choice bounds (no new κ)

research/common-prefix-minor-frontier/PROOF.md

@@ -0,0 +1,134 @@
+# Sharp adaptive choice among higher-rank tests with shared columns
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+## Contract and theorem
+
+Let F be any finite field of order q. Fix integers 1 <= k < m and let
+t=m-k+1 >= 2. Let G be uniform in GL_m(F), and let U be its first k rows.
+Write U=[C B], where C consists of the first k-1 columns and B has t columns.
+For each nonzero v in F^t define the rank-k determinant test
+
+    d_v(U) = det [C, Bv].
+
+Multiplying v by a nonzero scalar does not change its zero set. A nonempty
+family contains at most M projectively distinct vectors, fixed before inspecting
+G. A selector may inspect the entire G and choose any member of that family.
+It fails precisely when its chosen determinant vanishes. These are actual
+k-column tests after a fixed invertible input chart for each v. Each v extends
+the first k-1 coordinate vectors to an independent k-tuple. They need not all
+be coordinate minors in one common chart.
+
+Put
+
+    D = product_{j=0}^{k-1} (q^m-q^j),
+    R = product_{j=0}^{k-2} (q^k-q^j),
+    A = R q^(kt-2) (q-1) / D.
+
+An empty product equals one. For every integer M>=1, the maximum failure
+probability over such families and selectors is exactly
+
+    P*(q,m,k,M) = 1 - A max(q+1-M, 0).                 (1)
+
+In particular q+1 candidates suffice for failure on every matrix. This is
+a sharp result for this shared-column family. It is not a bound for arbitrary
+rank-k minors, arbitrary matrix distributions or current-dependent families.
+
+## 1. The top frame is uniform
+
+There are D full-row-rank k-by-m matrices. Choose the rows in order. After
+j independent rows, q^j vectors are forbidden for the next row. Every such
+matrix U has exactly
+
+    product_{j=k}^{m-1} (q^m-q^j)
+
+invertible completions to G, independent of U. Thus U is uniform on those D
+matrices. Giving the selector access to the remaining rows changes neither
+the set on which some candidate fails nor its probability. A selector that
+chooses the first failing candidate whenever one exists attains that union.
+
+## 2. Separate the common failure from the quotient test
+
+If rank C < k-1, every d_v vanishes. If rank C=k-1, the quotient F^k/im C
+is one-dimensional. Choose an arbitrary isomorphism of that quotient with F.
+The quotient of B is a row z in F^t, and
+
+    d_v(U)=0  if and only if  z dot v=0.
+
+Full row rank of U forces z nonzero. For each fixed full-rank C, every
+nonzero z has exactly q^((k-1)t) lifts B. This number does not depend on z,
+so z is uniform on F^t minus zero conditional on C. Choosing a different
+quotient coordinate scales z and leaves all its zero tests unchanged.
+
+There are R possible full-rank C. Therefore the probability gamma of an
+independent shared prefix is
+
+    gamma = R q^((k-1)t) (q^t-1) / D.                (2)
+
+The common-prefix deficiency contributes 1-gamma before any adaptive
+choice. No independence between the candidate failure events is assumed.
+
+## 3. The remaining union is sharp
+
+This is the one-linear-minor geometry cited from ywz65's #2601. The short
+argument is included to make the new reduction self-contained. A nonzero v
+defines a hyperplane in F^t. For s distinct such hyperplanes, the first has
+q^(t-1) points and each further one adds at most q^(t-1)-q^(t-2), because
+its intersection with the first already has q^(t-2) points. Consequently,
+for 1<=s<=q+1, their union on nonzero z has fraction at most
+
+    b_s = [q^(t-2)(1+s(q-1))-1] / (q^t-1).        (3)
+
+Equality holds for any s members of the pencil with normals
+
+    (1,a,0,...,0) for a in F, and (0,1,0,...,0).
+
+Their pairwise intersections are all the same codimension-two subspace,
+and their parts outside that subspace are disjoint. All q+1 members cover
+F^t. Extra budget cannot improve on probability one.
+
+Every candidate family has unconditional failure at most
+
+    (1-gamma) + gamma b_M
+
+until saturation, with the same pencil attaining the bound simultaneously
+for every full-rank C. Substituting (2) and (3) and cancelling q^t-1 gives
+(1), since
+
+    1-b_M = q^(t-2)(q-1)(q+1-M)/(q^t-1).
+
+This proves the theorem for every finite field, including extension fields.
+The finite verifier corroborates small cases; it does not supply these
+unbounded quantifiers.
+
+## 4. A concrete higher-rank boundary
+
+At q=2, m=3, k=2 there are 42 full-row-rank top frames. Six have a zero
+shared column. Formula (1) gives failure probabilities 3/7, 5/7 and 1 for
+budgets one, two and three. In particular two candidates give 5/7, whereas
+twice the single-test rate is 6/7 and the conditional linear-only rate is
+2/3. The common failure event must be counted once, and cannot be omitted.
+Every frame has four GL_3(F_2) completions, so the corresponding literal
+invertible-matrix counts are 72, 120 and 168 out of 168.
+
+At q=3, m=3, k=2 the rates are 4/13, 7/13, 10/13 and 1. These are examples
+of the theorem's new shared-column contract, not measurements of the
+selected stopped producer.
+
+## Scope and credit
+
+The original step is the higher-rank shared-prefix reduction, its exact
+common-deficiency term, and the resulting sharp formula (1). ywz65's
+PR #2601 supplies the bounded-choice interface, projective-pencil formula
+and higher-rank-intersection question. Adam Gall's PR #2097 supplies the
+fresh-row versus current-dependent-selection boundary, with its retained
+three-stage-cover, eumemic source527, Rohan Arun, Jeremy Kothe and PR589
+lineage. Matrix completion counts and projective pencils are classical.
+No general literature-priority claim is made for these counting methods.
+
+No actual selected candidate family, eligible-prime proof, current-field
+transcript, physical selector, routing, dirty restoration, complete paid
+invoice or all-size supplier is supplied. The selected five framework
+assumptions remain. This is a scoped written proof with finite exact
+corroboration, with no new kappa or complete multiplication theorem.
+Independent human and formal proof-kernel review are unclaimed.

research/common-prefix-minor-frontier/README.md

@@ -0,0 +1,137 @@
+# Sharp adaptive choice among higher-rank minors with shared columns
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+Claim type: scoped proof with exact finite corroboration. For a uniform
+G in GL_m(F_q), let U be its first k rows, where 1<=k<m, and write U=[C B]
+with k-1 shared columns C and t=m-k+1 remaining columns B. A candidate
+v in F_q^t tests whether det[C,Bv]=0. Candidates are fixed before G is seen;
+a selector may inspect all of G. Projectively equal candidates count once.
+
+The sharp maximum failure probability with at most M>=1 candidates is
+
+```text
+1 - A max(q+1-M, 0),
+A = q^(kt-2) (q-1) product_{j=0}^{k-2}(q^k-q^j)
+    / product_{j=0}^{k-1}(q^m-q^j).
+```
+
+A projective pencil attains it over every finite field. At q=2,m=3,k=2,
+the rates for one, two and three choices are 3/7, 5/7 and 1. This resolves
+a concrete family in the higher-rank-intersection direction of ywz65's
+[PR #2601](https://github.com/CrocSwap/integer-mult-bounds/pull/2601),
+Open next question 2. Its linear-minor theorem is cited, not re-audited.
+The new step is the exact common-column deficiency term and its combination
+with the quotient test. [PROOF.md](PROOF.md) gives the all-field argument.
+
+These determinant tests correspond to fixed input charts that share their
+first k-1 columns. They need not be coordinate minors in one common chart.
+The result does not identify the selected caller's actual bad varieties,
+construct a physical selector, improve kappa or change the selected frontier.
+
+## Exact evidence
+
+The verifier enumerates every full-row-rank matrix and every nonempty
+projective candidate family in five domains. Gaussian elimination selects
+the full-row-rank frames; the permutation determinant expansion evaluates
+every candidate. It computes each family's literal union count and maximizes
+over all families within each budget, rather than assuming pencil optimality.
+
+```text
+q  m  k    full-row-rank frames   candidate families   deficient prefixes
+2  3  2             42                    7                     6
+3  3  2            624                   15                    48
+4  3  2           3780                   31                   180
+2  4  2            210                  127                    42
+2  4  3           2520                    7                   504
+```
+
+That is 7,176 frames and 187 families across the five domains. F_4 uses
+F_2[x]/(x^2+x+1), not arithmetic modulo four. Separate literal GL_3 censuses
+cover all 168 binary and 11,232 ternary invertible matrices and compare
+complete candidate-failure-mask frequencies with their top-frame fibers.
+There are seven rejected formula-domain calls and seven semantic comparisons.
+All acceptance checks use explicit exceptions and stay active under -O.
+
+## Reproduce
+
+From the repository root, with the CPython 3.12 standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/common-prefix-minor-frontier/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/common-prefix-minor-frontier/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/common-prefix-minor-frontier
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/common-prefix-minor-frontier --check-source-history
+```
+
+Another CPython 3.12 path can replace the absolute interpreter path. The
+verifier writes nothing and emits JSON with `PASS_COMMON_PREFIX_MINOR_FRONTIER`,
+the enumerated results and SHA256 hashes of all six package files. Redirect
+stdout outside the checkout to retain a generated receipt. Both registered
+commands have 60-second limits. Local warning-strict ordinary and optimized
+checks, metadata and publication-byte/source-history checks are required.
+Hosted CI status is recorded separately in the PR body.
+
+The direct verifier also runs from a Git-free copy of this package. Exact
+source pins are historical provenance only. No predecessor executable is
+imported, and there are no external live inputs.
+
+## Limits and attribution
+
+The all-finite-field quantifier follows from the written proof. The exhaustive
+checks cover only the five stated domains. Arbitrary higher-rank minor families,
+nonuniform matrices, current-dependent candidate preparation and a fully charged
+selected caller remain outside scope. Physical reads, routes, restoration,
+transcript emission, eligible-prime arguments and all five selected framework
+assumptions remain open. No native, Lean, Docker or selected scientific cold
+replay was run. Independent human and formal proof-kernel review are unclaimed.
+
+Credit ywz65's #2601 for the question, bounded-choice interface and sharp
+linear-minor pencil bound. Credit Adam Gall's #2097 for the fresh-row versus
+adaptive-selection boundary, with the retained three-stage-cover, eumemic
+source527, Rohan Arun, Jeremy Kothe and PR589 lineage. Finite-field matrix
+completion counts and projective pencils are classical; no general literature
+priority is claimed for those methods. No predecessor text or code is copied.
+
+Canonical base is `19fdb086ea96af9a9f87936a2b888e10af4ed810`, priority revision 8.
+The task picker suggested `replay-runtime`. [TASK.json](TASK.json) explicitly
+changes it to this algebraic counting side result because the assignment
+requires an original result rather than an audit. The selected orientation
+passed `PASS_RESEARCH_BASELINE_BINDINGS_ONLY`; it is metadata orientation,
+not scientific evidence for this theorem.
+
+The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19221368)
+reserves this exact shared-column question. Live account PRs, current open
+PRs and Discussions, merged-PR searches and tracked-main README searches
+were checked. The overlap snapshot had 341 open PRs and 5,519 Discussion
+records with complete remote pagination. Its local sparse coverage was
+incomplete, so direct Git searches supplemented it. Unpublished work and
+arbitrary code diffs are outside those checks.
+
+## Open next questions
+
+1. Does an actual stopped-cover caller expose a fixed candidate family of
+   this shared-column form? First export its exact input charts and field
+   distribution. Such an adapter, eligible-prime coverage, a complete current-
+   field transcript and the physical selector bill are missing.
+2. What is the sharp bound when only k-2 columns are shared? The quotient
+   then has dimension two, and failure is a two-column determinant rather
+   than a hyperplane. Start with one specified two-plane candidate family
+   over F_2 and its literal GL distribution. Its intersection geometry is
+   not covered by the one-dimensional reduction here.
+
+## Verifier bounds
+
+The verifier has no recursion, subprocesses, network use or write path.
+Every matrix enumeration has at most 19,683 candidates; matrices have at
+most four columns and three rows. Permutation determinants have at most
+six terms. Candidate sets have at most seven projective points and 127
+nonempty families. Functions are below 60 physical lines. Package reads
+are bounded to 256 KiB each. Warning-strict normal and optimized execution
+and in-memory syntax inspection supply diagnostics.
+
+Python exact integers, lists and runtime calls allocate during this bounded
+offline check. These are managed-runtime deviations from Power of Ten static
+allocation and indirect-call restrictions. All call targets are fixed,
+collections have the stated bounds, and there is no persistent shared state.
+Larger executable domains require new capacity bounds before use.

research/common-prefix-minor-frontier/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8",
+      "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/bounded-row-choice/README.md",
+      "usage": "provenance",
+      "git_blob": "883ff97ee8eda15816ca36fcfb1d556670f12e76",
+      "sha256": "733053426538d3f1370fd48dfc3a3d4ce1fb5504d9322435541a5480fd60c912"
+    },
+    {
+      "path": "research/bounded-row-choice/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "1ea461858a08bcfc570d7810bde1e29869c69810",
+      "sha256": "3eea3e95cf606ee5ab305678b24b1b31d15b2acb816fb604c2285da74d4ca83a"
+    }
+  ]
+}