Exclude finite-menu adaptivity for exact helper endpoints (no new κ)

research/finite-menu-adaptivity/PROOF.md

@@ -0,0 +1,163 @@
+# Finite-menu adaptivity for an exact linear endpoint
+
+This scoped proof was produced by Nick Petalas. The polynomial root bound,
+finite-union argument, Cartesian fiber bound and weighted matroid greedy
+method are classical. The contribution is their explicit application to the
+finite-template exact helper interface, with a bounded witness constructor
+and a rank-sensitive finite-grid certificate. No priority is claimed for
+those general mathematical methods.
+
+Sagar Thakrar / thakrarsagar's [PR1133](https://github.com/CrocSwap/integer-mult-bounds/pull/1133),
+retained `rational-lift-descent-seed95/PROOF.md`, already uses the same
+N(d-1)+1 polynomial-avoidance bound for support descent. That bound is
+credited and reused below, not claimed as new. The new application concerns
+full endpoint menus; the support-descent theorem is not replayed or audited.
+
+## Exact interface
+
+Let K be an infinite field, d,m positive integers, and T:K^d -> K^m linear.
+Fix a finite menu A_1,...,A_N of linear maps with the same domain and codomain.
+A selector s:K^d -> {1,...,N} may be arbitrary, with no computability,
+continuity or observation restriction. Its output is A_{s(x)}x. Coefficients
+inside the A_j are fixed independently of x.
+
+Every arbitrary initial helper coordinate belongs to the domain. Every
+required dirty restoration coordinate belongs to the codomain. A fixed
+program can have temporary scratch, provided its complete specified output
+is a linear function of this domain and its required initial scratch state
+is fixed. This theorem asserts no physical legality of any such program.
+
+## Finite-menu obstruction
+
+**Theorem 1.** The selector can satisfy A_{s(x)}x=Tx for every x in K^d if
+and only if A_j=T for at least one j.
+
+The reverse implication uses a constant selector. For the forward direction,
+suppose every D_j=A_j-T is nonzero and choose a nonzero row l_j of each D_j.
+The polynomial product P(x)=product_j l_j(x) is nonzero because K[x_1,...,x_d]
+is an integral domain. A nonzero polynomial over an infinite field cannot
+vanish at every point. This last fact follows by induction on the number
+of variables, using the univariate root bound for each coefficient.
+There is therefore an x with every l_j(x) nonzero. Each D_j x is nonzero,
+contradicting the selector's claimed endpoint at that x.
+
+An equivalent proof says that finitely many proper linear subspaces cannot
+cover a vector space over an infinite field. This is a classical lemma;
+its use here concerns a complete arbitrary-input endpoint, not the
+information available to a branching controller.
+
+**Cost corollary.** Fix any finite menu of globally legal programs for one
+input/output contract. Let B be any allowed set of their complete invoices,
+including physical charges already required by that contract. If a selector
+uses only entries with invoices in B and achieves T on every input, one
+fixed entry with an invoice in B already achieves T. This holds for a scalar
+budget or for several simultaneous resource bounds. It proves no new lower
+bound on the fixed programs themselves. It prevents finite-menu selection
+alone from escaping an already established fixed-menu exclusion.
+
+Apply the corollary only when the fixed entry is legal for the full input
+domain. A native operation legal only on its selected branch does not meet
+this premise. An instruction-count bound with a finite fixed-coefficient
+alphabet gives finitely many words. A paid-call bound alone does not give
+a finite menu if unbounded free arithmetic is allowed.
+
+## Explicit rational counterexample
+
+**Theorem 2.** Over Q, when every D_j is nonzero, some integer
+0 <= t <= N(d-1) makes x(t)=(1,t,t^2,...,t^(d-1)) a counterexample to every
+menu entry simultaneously. Every coordinate has magnitude at most
+max(1,[N(d-1)]^(d-1)); for d=1 take x=(1) separately.
+
+A chosen nonzero row of D_j gives a nonzero polynomial l_j(x(t)) of degree
+at most d-1. At most N(d-1) distinct integers can be roots of any of those
+N polynomials. The N(d-1)+1 tested integers contain a common nonroot.
+Testing the entire D_j x(t), rather than just that row, is also sound.
+The implementation stops at its first simultaneous counterexample. It
+uses exact rational arithmetic and does not enumerate branch predicates.
+
+The number of curve tests cannot be reduced in general for this curve and
+test order. Take d=3, N=4, T=0, with the four scalar-output rows equal to
+the coefficient vectors of (t-2j)(t-2j-1), j=0,1,2,3. Every t=0,...,7 is
+a root of some row, and t=8 is a common nonroot. The returned vector is
+(1,8,64). This sharpness example concerns general linear endpoints; it
+claims no optimality of a physical helper program or of all witness methods.
+
+## Rank-sensitive Cartesian-grid obstruction
+
+Let S_i be nonempty finite subsets of a field K and s_i=|S_i|. Here K may
+be finite. For a nonzero defect D_j of rank r_j, define
+
+    W_j = max product_{i in B} s_i,
+
+where B ranges over the r_j-element independent column bases of D_j.
+Then
+
+    |ker(D_j) intersect product_i S_i| <= product_i s_i / W_j.
+
+To prove this, fix all coordinates outside one such B. The independent
+columns in B make the remaining coordinates uniquely determined if a
+solution exists. There are product_{i outside B} s_i outside assignments.
+Choose B with the largest product to obtain the bound.
+
+The union bound now gives **Theorem 3**:
+
+    sum_j 1/W_j < 1
+
+implies that some point of the Cartesian grid defeats every menu entry,
+regardless of the selector. For equal sizes s this becomes
+sum_j s^(-r_j)<1. In particular, N entries each having defect rank at
+least r cannot cover such a grid when N<s^r. The proof also bounds the
+fraction of successful grid points by min(1,sum_j 1/W_j).
+
+The weighted basis can be found greedily: scan columns in nonincreasing
+s_i order, accepting an independent column. This is maximum-weight basis
+greedy for the column matroid with additive weights log(s_i). More directly,
+after every prefix the greedy set has the rank of that prefix. Hence its
+k-th accepted size is at least the k-th largest size of any independent
+basis, and multiplying proves the required optimum. No numerical logarithms
+are needed by the implementation. Zero-rank defects are excluded here;
+an entry with D_j=0 is already a full exact endpoint.
+
+The strict inequality is necessary. Over Q take T=I_3 and the two invertible
+shears
+
+    A_+(x,y,z)=(x,y,z+x+y),
+    A_-(x,y,z)=(x,y,z+x-y).
+
+Every point of {-1,1}^3 lies in the success set of at least one shear, but
+neither shear equals I_3. Both defects have rank one, W=2, and the sum is
+exactly one. They preserve the first two outputs even off the grid. Thus
+discarding the arbitrary dirty third output would also invalidate the
+complete-endpoint claim.
+
+## Boundaries and implications for helper research
+
+Finite fields do not satisfy Theorem 1. Over F_p the p+1 fixed invertible
+shears
+
+    (x,y,z) -> (x,y,z+x-a*y), a in F_p,
+    (x,y,z) -> (x,y,z+y)
+
+collectively implement I_3 under a suitable selector on every input. If
+y is nonzero choose a=x/y; otherwise choose the final shear. Each individual
+map is different from I_3. This example changes the field premise.
+
+Finiteness also matters over Q. The shears with every nonzero rational
+normal (a,b), changing z to z+a*x+b*y, form an infinite menu. For each
+(x,y) choose (a,b)=(y,-x), except choose (1,0) at (0,0). One shear acts
+as identity at each point, but no fixed shear is identity on all of Q^3.
+
+For a finite-template complex helper proposal, write every full leaf map
+and its required input/output coordinates before applying Theorem 1. If
+all leaves miss the endpoint, arbitrary data-dependent branching cannot
+repair that menu. Theorem 2 supplies a small exact failing input when the
+maps are rational. Theorem 3 can obstruct a bounded-grid claim even over
+finite fields. These results can stop this specific proposed escape route
+before a physical implementation campaign.
+
+Restricted reachable inputs, approximate endpoints, rounded arithmetic,
+nonlinear leaf maps, infinitely many coefficient choices, extra retained
+branch outputs and a changed consumer are outside the exact interface.
+The theorem neither excludes these alternatives nor asserts they are free.
+It does not establish the fixed maps, an actual selected P104 menu,
+compiler closure, native costs, a complete supplier or a new kappa.

research/finite-menu-adaptivity/README.md

@@ -0,0 +1,114 @@
+# Finite-menu adaptivity cannot repair an exact helper endpoint
+
+Scoped mathematical obstruction, with finite exact corroboration. Over an
+infinite field, arbitrary data-dependent selection among finitely many fixed
+linear helper programs implements an exact arbitrary-input endpoint only if
+one fixed program already implements it. Every dirty input and every required
+restoration output must be part of the same contract.
+
+For N wrong rational maps on d inputs, the explicit witness constructor finds
+one input missed by every map after at most N(d-1)+1 tests of
+(1,t,...,t^(d-1)). The polynomial-avoidance bound is already used in Sagar
+Thakrar / thakrarsagar's [PR1133](https://github.com/CrocSwap/integer-mult-bounds/pull/1133)
+for support descent and is credited here. A four-map example needs all nine tests and
+returns (1,8,64). For a Cartesian grid with coordinate sizes s_i, a stronger
+rank-sensitive obstruction is
+
+    sum_j 1/W_j < 1,
+    W_j = maximum product of s_i over a column basis of A_j-T.
+
+For equal sizes s, this is sum_j s^(-rank(A_j-T)) < 1. Maximum-product bases
+use exact greedy independence tests. The grid statement holds over any field;
+the whole-space finite-menu statement requires an infinite field.
+[PROOF.md](PROOF.md) gives the proofs, cost corollary and sharpness examples.
+
+This supplies a screening rule for a proposed finite-menu escape from a
+complex helper or decoder exclusion. It does not establish an exclusion for
+any actual P104 menu. A paid-call cap alone need not make the menu finite.
+Every fixed word must also be globally legal before the cost corollary applies.
+No physical caller, complete supplier, new kappa or selected-frontier change
+is claimed. The original construction card has explicitly changed scope.
+
+## Evidence and reproduction
+
+Use CPython 3.12 and its standard library, from the repository root:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/finite-menu-adaptivity/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/finite-menu-adaptivity/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/finite-menu-adaptivity
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/finite-menu-adaptivity --check-source-history
+```
+
+Another installed CPython 3.12 may replace that executable. Expected direct
+status is `PASS_FINITE_MENU_ADAPTIVITY`. The verifier writes only stdout,
+including generated SHA256 bindings to all six package files. No receipt is
+handwritten and no predecessor executable or mathematical receipt is consumed.
+Catalogue and selected-record pins are historical provenance in SOURCES.json.
+
+The exact checks enumerate all 729 two-by-three matrices with entries in
+{-1,0,1}, all 2,187 declared weighted grids and their 11,139 output fibers.
+Rational elimination agrees with a separate determinant/permutation rank
+oracle. Exhaustive column bases confirm greedy maximum products. All 2,600
+three-element menus of nonzero ternary rows receive simultaneous witnesses;
+their success unions are enumerated on 166,400 grid points. Scope controls
+include a tight eight-point restricted grid, all 503 points of F_p^3 for
+p=2,3,5,7, an infinite-menu construction on 81 rational fixtures, preservation
+of required dirty outputs, rational coefficients and dimension one. Ten
+invalid-domain calls reject. Checks remain active with optimization enabled.
+These finite enumerations corroborate the written proof; they do not replace it.
+
+## Scope and overlap
+
+The scientific base is canonical main
+19fdb086ea96af9a9f87936a2b888e10af4ed810, priority revision 8. The
+[advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19228363)
+specifies the original question and its limits. Search covered live open PRs,
+recent account work, handoffs, active Discussions, distinctive main README and
+proof terms, and merged-PR terms. The overlap helper reported 393 open PRs and
+5,630 Discussion records with complete remote pagination. Sparse local notes
+and arbitrary code diffs were incomplete; no search proves novelty.
+
+Related work has different contracts. PR5997 bounds adaptive observation
+capacity with a cited missing-dimension premise. PR5961 counts finite-field
+minor selection. The retained centre-nonlinear-fresh-floor uses topological
+dimension for continuous or semialgebraic observations. This package concerns
+selection among fixed full endpoint maps, allows an arbitrary selector and
+supplies no observation-capacity or header-price theorem. Those results are
+context, not dependencies being replayed or verified.
+
+## Open next questions
+
+1. Apply the certificate to one actual source-bound complex helper menu.
+   Export every globally legal leaf's full endpoint and complete invoice,
+   then run the witness constructor. The missing menu and physical contract
+   block a source-specific exclusion.
+2. Bound approximate finite-menu endpoints under a physical norm and a bounded
+   magnitude domain. This could inform rounded execution, but first needs a
+   priced error tolerance and restoration contract. The exact theorem does
+   not provide either. Structured questions are in TASK.json.
+
+## Implementation limits and credit
+
+The checker has no recursion or unbounded loop. The public matrix boundary caps dimensions
+at eight, menus at 32 entries and input rational components at 64 bits.
+The witness loop has at most 225 iterations. Minor enumeration is separately
+capped at four by four, and every fixture domain is explicitly finite. All
+functions are shorter than 60 physical lines. Internal checks use exceptions.
+
+Managed-runtime allocation is a Power of Ten rule 3 deviation. Exact integers,
+fractions and bounded containers allocate during this offline checker; no
+fixed byte allocation guarantee is claimed. Input dimensions and coefficients,
+fixed fixture inventories and 120-second registered timeouts bound the work.
+Rule 9 has ten explicitly listed invalid-domain callbacks, used only by the
+negative-control loop. The call targets and lifetimes are fixed. Warning-strict
+normal and optimized execution and in-memory syntax inspection provide the
+available diagnostics; no standalone static analyzer or global CI change is
+introduced.
+
+This contribution was produced by Nick Petalas. Classical finite-union,
+polynomial-root, Cartesian-fiber and column-matroid arguments are credited
+as methods rather than new general mathematics. The contribution is the
+specified exact-interface application and its bounded certificate tools.
+New proof and code are Apache-2.0. Independent human and formal proof-kernel
+review are unclaimed.

research/finite-menu-adaptivity/SOURCES.json

@@ -0,0 +1,24 @@
+{
+  "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/rational-lift-descent-seed95/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "51775d18c09eb4b5f3b1b0be42388ac2041efa1f",
+      "sha256": "5ab2bab295bd3a2dc5202f90606235776e6354ade301edf8e23fc63344c4c15e"
+    }
+  ]
+}