Prove sharp affine native tag membership at 46 queries (no new κ)

research/affine-tag-query-minimum/PROOF.md

@@ -0,0 +1,153 @@
+# Sharp oracle cost of affine native tag membership
+
+This scoped proof was produced by Nick Petalas. Quadratic interpolation and
+binary nullspace elimination are classical. The contribution is the exact
+decision cost with unknown constant and even-linear tags, including an
+adversary for arbitrary adaptive query choices.
+
+## Statement and oracle model
+
+Fix any positive integer n, a known invertible binary matrix A, and a known
+binary offset b. The oracle returns exact values in Z/4 of a function promised
+to have the form
+
+```text
+q(x) = q0 + sum_i a_i x_i + 2 sum_(i<j) h_ij x_i x_j modulo 4,
+q0,a_i in Z/4, h_ij in F2, x in F2^n.
+```
+
+The matrix, offset and promise are available without oracle queries. Polynomial
+coefficients are not available. A query specifies any binary address and returns
+its phase exponent. Algorithms may choose later addresses from earlier answers.
+The decision must be correct on every promised oracle. The complexity is the
+worst-case number of queries of a deterministic algorithm. Neither arithmetic
+cost nor tensor-width identity testing is the quantity being optimized.
+
+Let `D|x> = i^wt(x)|x>`, `F(x)=Ax+b`, and `J_F=D P_F D^-1`. The question is
+whether there are a constant `c in Z/4` and mask `t in F2^n` such that
+
+```text
+i^q(x)|F(x)> = i^c J_F Z_t |x>    for every x.
+```
+
+The answer can be decided, and the unique c,t recovered on acceptance, with
+exactly
+
+```text
+d(n) = 1 + n + binom(n,2) = 1 + n(n+1)/2
+```
+
+queries in the worst case. Every deterministic adaptive decision algorithm
+requires at least d(n) queries. In particular d(9)=46, whereas the cube has
+512 points. This is a query count, not a measured speedup or a physical saving.
+
+## Reduction to an even-linear residual
+
+Write `r_A,b(x)=wt(Ax+b)-wt(x) modulo 4`. If row j of A has entries A_ji, then
+the parity expansion modulo four gives
+
+```text
+(Ax+b)_j = b_j + (1-2b_j) sum_i A_ji x_i
+                 - 2 sum_(i<k) A_ji A_jk x_i x_k modulo 4.
+```
+
+Terms of degree at least three have coefficients divisible by four. The sign
+of the quadratic term is immaterial modulo four. Thus r_A,b belongs to the
+same promised quadratic class. That class is closed under subtraction.
+
+Set `R=q-r_A,b`. The requested identity is exactly
+
+```text
+R(x) = c + 2(t dot x) modulo 4.
+```
+
+Since twice binary parity equals twice the ordinary sum modulo four, these
+are precisely the residual polynomials with even linear coefficients and
+zero quadratic coefficients. Every coefficient in the promised class is
+unique as a function: its constant is determined at zero, its linear
+coefficients at the unit vectors, and its doubled quadratic coefficients by
+the pair differences. The constant and mask c,t are therefore unique too.
+
+## Upper bound
+
+Query q, hence R, on zero, every unit vector e_i, and every e_i+e_j with i<j.
+There are d(n) distinct addresses. Compute
+
+```text
+c = R(0),
+delta_i = R(e_i)-c modulo 4,
+gamma_ij = R(e_i+e_j)-R(e_i)-R(e_j)+c modulo 4.
+```
+
+Accept exactly when every delta_i is even and every gamma_ij is zero. These
+are exactly the required coefficient conditions. On acceptance return
+`t_i=delta_i/2`. The polynomial promise extends these conditions to every
+address. The implementation uses equivalent pair comparisons after recovering
+t; it queries each address once.
+
+## Lower bound with arbitrary adaptive choices
+
+Run any correct deterministic algorithm on the accepted oracle `q=r_A,b`,
+whose residual R is identically zero. Suppose it stops after m<d(n) queries.
+Let S be the set of queried addresses; repeated queries do not add information.
+We construct a promised residual R* that vanishes on S but is outside the
+accepted family. Then `q*=r_A,b+R*` supplies exactly the same transcript.
+Determinism forces the same later queries and the same acceptance, which is
+incorrect. This proves the worst-case lower bound once the construction is
+given.
+
+If S does not affinely span F2^n, choose a nonzero mask v whose binary linear
+functional is constant, say k, on S. Empty S allows any nonzero v and k=0.
+Take
+
+```text
+R*(x) = (v dot x as a bit) - k modulo 4.
+```
+
+This is a promised polynomial because binary parity has the expansion
+`sum_i v_i x_i - 2 sum_(i<j) v_i v_j x_i x_j modulo 4`.
+It vanishes on S. Its parity is nonconstant, whereas the parity of every
+accepted `c+2(t dot x)` is constant. Hence it is outside the accepted family.
+
+If S does affinely span F2^n, consider binary square-free polynomials of
+degree at most two. They have dimension d(n), with basis 1, x_i, x_i x_j.
+Evaluation on S has at most |S|<d(n) rows, so its kernel contains a nonzero
+polynomial f. Full affine span implies that no nonzero affine polynomial
+vanishes on S. Consequently f has a nonzero quadratic coefficient. Set
+
+```text
+R*(x) = 2 f(x) modulo 4.
+```
+
+Twice a binary polynomial equals twice its ordinary coefficient sum modulo
+four. R* is promised, vanishes on S, and has a nonzero doubled quadratic
+coefficient. Uniqueness of the square-free coefficient representation makes
+it impossible for R* to be an accepted even-linear residual.
+
+These cases cover every S and prove the lower bound. The executable
+`adversary` constructs v or f by binary elimination, without searching
+possible adaptive algorithms. The transcript argument handles adaptivity.
+
+## Essential boundaries
+
+The quadratic promise cannot be inferred from the d(n) samples. For n=3,
+`q(x)=2 x1 x2 x3` with A=I,b=0 vanishes on every queried address but is nonzero
+at 111. It is outside the promised class. The implementation intentionally
+accepts its sampled values in a limitation control.
+
+The theorem assumes that the affine permutation is known. It does not certify
+the permutation, arbitrary serialized gate semantics, nonmonomial children,
+general tensor linear combinations, or physical routing/restoration costs.
+It does not give a lower bound for algorithms that inspect polynomial
+coefficients directly, randomized bounded-error tests, or quantum queries.
+It supplies no new kappa or complete multiplication theorem.
+
+JoyboyBrian's [PR6106 at its exact head](https://github.com/CrocSwap/integer-mult-bounds/blob/9d0126c134720258cfe685b661ce288da01008fa/research/native-affine-phase-tags/README.md)
+supplies the affine tag convention and explicitly warns that coordinate
+evaluations alone cannot establish that a general quadratic residual is
+linear. Its actual warp/inverse result is cited, not replayed here.
+ToikY's [PR4002 proof](../native-lift-phase-tags/PROOF.md) supplies the normalized
+linear lift and retains Chris R / Clear1nsight's PR3987 and the native lineage.
+Ali Romman's [native tensor criterion](../native-tensor-cutoff/PROOF.md) concerns
+fixed group-algebra identities across tensor widths, a different decision
+problem. No predecessor result is claimed as a new theorem here.

research/affine-tag-query-minimum/README.md

@@ -0,0 +1,126 @@
+# Sharp affine native tag membership with 46 queries on nine axes
+
+This scoped proof and executable certificate were produced by Nick Petalas.
+For a known binary affine permutation on n axes and a phase promised to be
+quadratic over Z/4 with even mixed coefficients, deciding membership in the
+normalized affine tag family requires exactly
+
+```text
+d(n) = 1 + n + binom(n,2) = 1 + n(n+1)/2
+```
+
+exact phase evaluations in the worst case. The lower bound covers every
+deterministic adaptive decision algorithm, even though the constant phase
+and even-linear tag are free unknowns. A matching test queries zero, the
+unit vectors, and the pair sums. On nine axes it uses 46 evaluations; the
+cube contains 512 addresses. This is an optimal oracle query count, not a
+measured speedup, physical saving, new supplier or new kappa.
+
+[PROOF.md](PROOF.md) states the complete oracle contract and proves both
+bounds. The reusable `certify` function in [verify.py](verify.py) returns the
+unique constant and mask, or raises `ValueError` on a nonmember. `adversary`
+constructs an invalid residual agreeing with zero on any insufficient query
+set. The implementation supports 1 through 64 axes; the written theorem
+covers every positive dimension.
+
+## Why this boundary matters
+
+JoyboyBrian's [PR6106](https://github.com/CrocSwap/integer-mult-bounds/pull/6106)
+extends normalized native tags to affine maps and notes that coordinate
+evaluations alone do not establish that a general quadratic residual is
+linear. This package supplies a complete test for that question and proves
+its sharp black-box cost. It does not replay the predecessor's warp, inverse,
+512-column census, or calibration results.
+
+The reduction subtracts the known phase `wt(Ax+b)-wt(x)`. The remaining
+polynomial must have even linear coefficients and zero mixed coefficients.
+For a shorter test, an affinely deficient query set misses an odd-parity
+residual. A full-span query set with fewer than d(n) points misses twice a
+nonzero quadratic polynomial. These explicit impostors prove the adaptive
+lower bound by following the accepted oracle's transcript.
+
+## Evidence and reproduction
+
+From the repository root, with CPython 3.12 and the standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -I -B research/affine-tag-query-minimum/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -I -O -B research/affine-tag-query-minimum/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/affine-tag-query-minimum
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/affine-tag-query-minimum --check-source-history
+```
+
+Any CPython 3.12 path can replace the local interpreter path. The verifier
+prints `PASS_AFFINE_TAG_QUERY_MINIMUM` in a generated JSON receipt bound to
+all six package files. It writes no files and imports no predecessor code.
+
+The complete finite checks enumerate 2,192 promised phases through three
+axes and compare membership with literal cube values and every possible
+tag. They also enumerate all 58,916 insufficient distinct query subsets
+through four axes, construct an impostor for each, and check both its zero
+transcript and its nonmembership by literal values. Thirty-six affine
+constructions cover dimensions 1,2,3,4,5,9,16,32,64, with full cube comparisons
+through five axes and exact queried-address comparisons thereafter.
+Fourteen malformed-input/nonmember controls reject; a separate cubic control
+shows why the polynomial promise is necessary. These finite checks support
+the written proof and do not replace it.
+
+## Scope and engineering limits
+
+The known affine permutation, exact phase oracle and structural quadratic
+promise are hypotheses. For an arbitrary function, an unqueried cubic can
+pass this test. The lower bound does not apply when coefficients may be read
+directly, or to bounded-error randomized or quantum queries. A serialized
+native circuit still needs a proof that its action has the promised form.
+No complete tensor identity, physical caller, dirty restoration, precision,
+tape bound, supplier invoice or multiplication theorem is certified here.
+No selected cold replay, Lean, Docker, independent human review or formal
+proof-kernel acceptance is claimed.
+
+All executable loops have finite bounds. Public membership queries validate
+1 <= n <= 64 and affine invertibility before calling the oracle, and use at
+most 2,081 calls. Binary elimination uses at most 2,081 rows and columns;
+literal enumeration is restricted to at most four axes. Managed Python
+allocation and the standard frozen dataclass are documented departures from
+static-allocation and no-generation rules. Their retained data sizes are
+bounded by these limits; the oracle's internal time and memory are outside
+the query contract. Functions stay below 60 physical lines, use explicit
+checks under optimized execution, and propagate failures. Warning-strict
+normal and optimized runs are the registered diagnostics.
+
+## Sources and overlap
+
+The exact affine convention is credited to
+[PR6106 head 9d0126c](https://github.com/CrocSwap/integer-mult-bounds/blob/9d0126c134720258cfe685b661ce288da01008fa/research/native-affine-phase-tags/README.md).
+It is explanatory provenance, not an executable input or an unmerged source
+dependency. The proof defines the entire problem locally.
+ToikY's [PR4002](https://github.com/CrocSwap/integer-mult-bounds/pull/4002)
+supplies normalized linear lifts and retains Chris R / Clear1nsight's
+PR3987, Dugongue PR3945/3929, dataisfire PR3734, Cinna Davis PR2226 and the
+native/compiler lineage. Ali Romman's
+[PR5369](https://github.com/CrocSwap/integer-mult-bounds/pull/5369)
+decides fixed group-algebra identities across tensor widths; that different
+problem is not reduced to this membership test. Classical interpolation
+and binary linear algebra are not claimed as new methods.
+
+Before the advance claim, current main and merged PRs were searched for
+quadratic membership, affine phase tags, phase probes and interpolation,
+including general-dimension forms. The cached overlap snapshot covered 407
+open PRs and 5,816 Discussion records with complete remote pagination; its
+sparse local notes omitted 8,272 paths, so main was searched directly too.
+These are bounded overlap checks, not a proof of global novelty. The
+[advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19246894)
+records the changed card scope. The selected frontier is unchanged.
+
+## Open next questions
+
+- Bind this test to one serializer whose quadratic phase and affine
+  permutation are structurally authenticated. First expose its exact phase
+  oracle and polynomial induction, then price its complete caller. Arbitrary
+  circuit membership and physical delivery are still missing.
+- Determine the optimal bounded-error randomized query cost for this same
+  promise problem. First specify error probability and one-sided versus
+  two-sided rejection. The deterministic transcript lower bound does not
+  settle that problem.
+
+Apache-2.0. The scoped proof, checker and adversary were produced by Nick Petalas.

research/affine-tag-query-minimum/SOURCES.json

@@ -0,0 +1,18 @@
+{
+  "schema_version": 1,
+  "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419",
+  "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"
+    }
+  ]
+}