Prove zero-preserving polynomial helpers cannot reduce linear call minima (no new κ)

research/polynomial-helper-profile-domination/PROOF.md

@@ -0,0 +1,109 @@
+# Zero-state extraction preserves the labelled linear interface
+
+## Contract
+
+Let K be an infinite field and R a subring of K. There are finitely many
+vector registers of a common finite dimension d. The data and dirty workspace
+vary independently over K. A specified subset of scratch registers may instead
+start at zero. Every gate has distinct source a and target b, a fixed K-linear
+operator T, a label ell, and a fixed scalar polynomial p in R[t] with p(0)=0.
+It performs one of the following operations. Powers in p are coordinatewise.
+
+    b += p(Ta),       or       b += T p(a).
+
+The source and other registers stay unchanged. Each gate is invertible by
+subtracting the same increment. No invertibility assumption on T is needed.
+The sequence, coefficients, operators, ports and labels are independent of
+input values. A label records one allowed paid operator class. Multiplication
+by any scalar in R is permitted in the linear class at that same label charge.
+The polynomial class grants its extra pointwise arithmetic for free. This is
+an optimistic operator-call model, not a physical implementation claim.
+
+The call profile n_ell counts gates of each label. Any nonnegative tariff
+sum_ell w_ell n_ell is allowed. Labels may encode rank, operator, orientation,
+ports and other fixed distinctions. There is no claim that these counts alone
+constitute the selected supplier's complete invoice.
+
+## Theorem
+
+Suppose a word in this model implements an exact linear endpoint L on every
+allowed input. Include every required dirty return and clean-scratch return in
+that endpoint. Replace each gate by
+
+    b += p'(0) T a.
+
+If p'(0)=0, delete its gate. The extracted word has the same endpoint on the
+same allowed input space. For every label, its call count is at most the
+original call count. Thus every attainable polynomial call profile is dominated
+coordinatewise by an attainable linear profile. The attainable Pareto-minimal
+profiles, and the minimum for every nonnegative tariff, are identical in the
+two classes. This holds with any finite number of clean or dirty registers.
+
+## Proof
+
+Let J be the ideal generated by all independent input coordinates in their
+polynomial ring over K. Substitute zero for the initialized clean coordinates.
+Every initial register has zero constant term. Inductively this remains true
+after each gate because T is linear and p(0)=0.
+
+Modulo J squared, a polynomial p(u) with u in J equals p'(0)u. Linear T
+commutes with taking degree one. Therefore either gate placement induces
+exactly the displayed linear shear on the degree-one parts. This proves by
+induction in chronological order that the extracted word equals the degree-one
+part of the complete original endpoint, including every workspace output.
+
+Over an infinite field, equality of polynomial functions on all independent
+inputs implies equality of their polynomials. For completeness, a univariate
+nonzero polynomial has at most its degree many roots. Induction in the number
+of variables applies that fact to the coefficient polynomials in the last
+variable. Hence an endpoint that is the linear function L has degree-one part
+L itself. This proves the endpoint statement. Equivalently the proof is the
+chain rule at the common fixed zero state.
+
+A retained gate has its old T, label, ports, placement and order. Its scalar
+p'(0) is in R. A discarded gate induces the identity on degree-one parts.
+Consequently no label count increases. Linear gates are already polynomial
+gates, proving equality of the profile minima in both directions. The same
+argument applies separately at every permitted dimension. If a fixed word
+uses a uniform operator family T_f, the single extracted word is independent
+of f, so an all-width endpoint gives an all-width extracted endpoint.
+
+## What the theorem excludes
+
+Adding zero-preserving pointwise polynomial gates to this labelled linear
+helper model cannot evade any call-profile obstruction proved for its full
+linear scalar class. This conclusion does not require a common flag, a
+commuting operator alphabet, a bound on polynomial degree, or a bound on the
+number of borrowed registers across different candidate words. Each word
+must be finite. The executable checks a bounded rational subcase.
+
+The conclusion concerns exactly the same linear output contract. A nonlinear
+output could carry different information and require a different consumer.
+No selected-word result, supplier lower bound or multiplication theorem is
+inferred here. In particular, a lower bound limited to signs or unit scalar
+coefficients cannot be used if derivatives introduce other allowed scalars.
+Representation changes and their frame, precision, scalar, movement and
+restoration costs require their own implementation argument. The theorem
+only preserves the declared operator-call labels and the algebraic returns.
+
+## Essential boundaries
+
+1. A nonzero constant can move the trajectory away from zero. For example,
+   adding 1 to a source, adding its square to a target, subtracting 1 from
+   the source, subtracting the source square from the target, and subtracting
+   1 from the target produces the exact linear endpoint target += 2 source. Differentiating each gate at zero separately would
+   miss the linear term. This word is outside the contract.
+2. Over F2, target += source squared is the linear map target += source on
+   every input, but its formal degree-one part is the identity. Thus the
+   infinite-field or polynomial-identity hypothesis matters. The same issue
+   arises on a restricted finite grid inside an infinite field.
+3. Linearizing a word never proves that its endpoint is linear. The single
+   gate target += source + source squared has the same degree-one part as
+   an addition but has a different endpoint. Exact endpoint verification is
+   a separate premise; basis-only testing is insufficient.
+4. Branching, rounded arithmetic, discontinuous bit operations and nonlinear
+   address permutations are outside these polynomial data-value gates.
+
+The degree-one quotient, chain rule and polynomial identity principle are
+classical. The contribution is their explicit labelled-profile domination
+statement for this helper contract and its bounded executable extraction.

research/polynomial-helper-profile-domination/README.md

@@ -0,0 +1,111 @@
+# Polynomial helper gates cannot reduce the labelled linear call minimum
+
+This contribution was produced by Nick Petalas.
+
+**Scoped proof with finite exact corroboration; no new kappa.** Grant each
+paid linear-operator call a free, fixed coordinatewise polynomial before or
+after it. Require every polynomial to fix zero. For an exact linear endpoint
+over an infinite field, this extension has exactly the same Pareto-minimal
+labelled operator-call profiles as the linear model, with every required dirty
+and clean return included. Any finite number of workspace registers is allowed.
+
+The extraction is explicit:
+
+    b += p(Ta)  or  b += T p(a)   becomes   b += p'(0) T a.
+
+A zero derivative deletes that call. Every other call retains its operator,
+ports, label and chronological position. Scalar multiplication by p'(0) must
+be permitted in the comparison's linear class. [PROOF.md](PROOF.md) proves the
+statement with the degree-one quotient, gives its uniform-family corollary,
+and spells out the necessary assumptions. Classical polynomial linearization
+is the method; the new step is the declared helper-interface profile theorem
+and executable extraction, without any claim of literature priority.
+
+This rejects one proposed escape route from a linear call lower bound even
+when polynomial arithmetic is granted free. It does not exclude arbitrary
+nonlinear computation. Nonzero constant gates, branching, finite-grid or
+rounded execution, nonlinear address permutations, and changed output
+contracts need separate analysis. Actual scalar, frame, native, movement,
+precision, stock and compiler costs are not equated by this theorem. The
+selected supplier and frontier are unchanged.
+
+## Exact evidence and reproduction
+
+The rational implementation in [compiler.py](compiler.py) has a bounded,
+validated immutable input contract. It extracts the linear word; it does not
+certify the premise that the original endpoint is linear. The checker uses
+complete sparse multivariate polynomial expansion to certify that premise
+on its fixtures, including every dirty coordinate. A separate dual-number
+interpreter corroborates extraction. Literal rational execution checks the
+same directions against the known target. The receipt is generated and bound
+to SHA256 hashes of all seven source/metadata files.
+
+The finite corpus has 145 exact linear-endpoint fixtures and 1,029 directions
+for each of dual-number and numerical comparison, plus 14 controls. It includes
+singular and nonsymmetric operators, rational coefficients, both polynomial
+placements, clean and dirty borrowed registers, exact inverses, and successive
+blocks with noncommuting operators. The five-gate dirty echo's illustrative
+profile changes from `T:3, read:2` to `T:2, read:2`. These labels denote abstract
+operator classes, not measured Fourier ranks or selected-word jobs.
+
+From the worktree root:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/polynomial-helper-profile-domination/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/polynomial-helper-profile-domination
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/polynomial-helper-profile-domination --check-source-history
+```
+
+A portable checkout can use any CPython 3.12 interpreter in those commands.
+The registered checks run normal and optimized modes with warnings as errors.
+No predecessor mathematical replay, supplier admission, Lean build, Docker
+run or complete multiplier is required or claimed. Independent human and
+formal proof-kernel review are unclaimed.
+
+## Relation to previous work
+
+Jose Manuel / jmbarrancoml's [#1757](https://github.com/CrocSwap/integer-mult-bounds/pull/1757)
+proves a cut obstruction for arbitrary deterministic finite-alphabet gates
+under frame conditions. The present theorem uses a different infinite-field
+polynomial model, has no common-flag premise, and preserves call labels.
+Chris R / Clear1nsight's [#3992](https://github.com/CrocSwap/integer-mult-bounds/pull/3992)
+uses a generic Jacobian or transcendence-degree bound for a typed Toom-only
+boundary. It does not extract a chronological word or compare call profiles.
+Both results are cited premises/context, not audit targets or new claims here.
+The finite-menu adaptivity investigation claimed in #1166 concerns branch
+selection among linear maps and is separate from this fixed nonlinear word.
+No predecessor code is copied or executed. Exact context pins are in
+[SOURCES.json](SOURCES.json), alongside the current card and selected record.
+
+## Open next questions
+
+- Can nonzero constant trajectories produce a genuinely cheaper complete
+  complex helper word? First account for preparation, constants, the varying
+  coordinate derivatives, retained outputs and restoration. The explicit
+  translated-square counterexample only shows why this proof does not apply.
+- Can a physical finite-grid polynomial or bit-operation mechanism save calls
+  while meeting the selected source's precision and all-input requirements?
+  First specify that grid and the exact nonlinear consumer; the F2 square
+  control shows why a formal derivative is not a certificate on a finite grid.
+
+These are reopening conditions, not an implementation campaign. TASK.json
+records the changed card, stopping rule and remaining obligations.
+
+## Verification bounds
+
+The extractor accepts at most eight roles of width four, 32 gates and scalar
+polynomials of degree four. Input numerators and denominators are at most
+1,024 in magnitude. Rational evaluation rejects intermediates exceeding
+4,096 bits. The finite symbolic checker caps each polynomial at 512 monomials
+and total degree 16. It uses no recursion or generated code. Every function
+is below 60 physical lines. Explicit runtime checks remain active under `-O`.
+
+Python's Fraction arithmetic, dictionaries, tuples and standard dataclass
+construction allocate dynamically. This is a managed-runtime deviation from
+Power of Ten rule 3, restricted to this finite checker/extractor. The input,
+term, degree and scalar bounds constrain live state and reject exhaustion.
+The small fixture corpus is checked in both modes. A fixed-capacity backend
+would be needed if this extractor became a production bounded-memory service;
+no such service or physical memory tariff is claimed. Warning-strict replay
+and an AST syntax/function-length check are the available diagnostics; no
+separate static type checker is a package dependency.

research/polynomial-helper-profile-domination/RESULT.json

@@ -0,0 +1,26 @@
+{
+  "claim_type": "scoped proof with finite exact corroboration",
+  "controls": 14,
+  "dirty_echo_profile": {
+    "after": {
+      "T": 2,
+      "read": 2
+    },
+    "before": {
+      "T": 3,
+      "read": 2
+    }
+  },
+  "dual_and_numeric_directions_each": 1029,
+  "linear_endpoint_fixtures": 145,
+  "source_sha256": {
+    "PROOF.md": "187fc5788d0a033c89c16f0a8b0255cd1f3754d5abb84c786de0fdc4be8a207d",
+    "README.md": "198a63ce6e68f927fef96f8f7114d7ac78d6cc5bdb17c15b7c1069f6e7829a02",
+    "SOURCES.json": "01247337000ae4a51c606345c88d912f7e274f1919ced8309e28d659b90fab4c",
+    "TASK.json": "4cebe6ad9d98bb7d5298f165dec4d611ba797ac289ab81439e11dc7922e3da2b",
+    "VERIFY.json": "bdfa25ef3e90f2328bf1623bf1b011706e085d2a31085775a6e1cbe9a0892605",
+    "compiler.py": "47a7aecb033ef80ae83fe0465117420f807d60e1e4ad3e2baabebdb53dfaba6a",
+    "verify.py": "8ea1457cb1152e834b13a16c5c8fda9e9cf099a10c17bc5d42e620480025d386"
+  },
+  "status": "PASS_POLYNOMIAL_HELPER_PROFILE_DOMINATION"
+}

research/polynomial-helper-profile-domination/SOURCES.json

@@ -0,0 +1,36 @@
+{
+  "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": "docs/research/current-priorities.md",
+      "usage": "provenance",
+      "git_blob": "6f5d40d13d8f3bdc12ce7954c8c3eb4ab1f8be91",
+      "sha256": "70f61c8d140ae6e892f2b8f065bba4eae3e76f7a8f55f632fd4e2f9f34039bdc"
+    },
+    {
+      "path": "research/nonlinear-frame-cut-bound/README.md",
+      "usage": "provenance",
+      "git_blob": "1fae484c0dc371afb0ec0d0c9b1f781d78dbffbb",
+      "sha256": "411b78a56180e835bb97e59b9845968d84ad3fb8f5658acde684e4491b3b1c3e"
+    },
+    {
+      "path": "research/selected-toom3-typed-block/README.md",
+      "usage": "provenance",
+      "git_blob": "ad87055215a158817ff90f7599c012cf7a69cf3d",
+      "sha256": "259a0d675673adb0a5005cbd939029c013acf58b238d18ae216996505293a3a2"
+    }
+  ]
+}