Prove the exact bounded-degree polynomial cost law and moments (no κ)

research/degree-bounded-polynomial-cost/PROOF.md

@@ -0,0 +1,134 @@
+# Uniform bounded-degree polynomial target costs
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+Claim type: scoped counting proof, conditional only on the cited exact
+degree/cost theorem. Finite execution corroborates the formulas below.
+No new multiplication exponent or native supplier is claimed.
+
+## Contract and predecessor input
+
+Let q be any prime power, K=F_q and R=K[t]. There are two data roles and
+no auxiliary roles. A paid factor is I+u y^T with u in R^2 and y in K^2.
+Arbitrary GL2(K) maps may occur freely anywhere in the word. Write C(M)
+for minimum paid length and D(M) for the maximum entry degree of M.
+
+The sampling measure here is uniform on
+
+    S_N = {M in GL2(K[t]) : D(M)<=N},    N>=0.
+
+Invertibility means that the determinant is a nonzero constant. Uniform
+polynomial matrices without this condition are a different measure.
+
+Nick Petalas's PR4784, exact head
+4d0a6363fe4f45dd9a769f5b74d02fc5d9061ae3, proves the following input.
+For g=|GL2(K)|=(q^2-1)(q^2-q), D>=1 and 1<=r<=D,
+
+    #{M : D(M)=D, C(M)=r}
+      = g (q+1)(q-1)^r q^(D-1) binom(D-1,r-1).
+
+There are g degree-zero targets, all of cost zero, and |S_N|=g q^(2N).
+Equivalently, conditional on positive degree D,
+
+    C-1 has distribution Binomial(D-1,(q-1)/q).
+
+Those statements and their normal-form proof are cited premises. This
+package does not audit them or rerun their matrix census. Their original
+proof text is pinned as the sole external mathematical input.
+
+## The new probability-generating function
+
+Put B(z)=q+q(q-1)z. Then the exact generating function for the present
+uniform bounded-degree measure is
+
+    G_N(z) = E[z^C]
+           = q^(-2N) [1+(q^2-1)z (B(z)^N-1)/(B(z)-1)].
+
+The quotient means the polynomial sum 1+B+...+B^(N-1). For N=0 it is
+zero. At B(z)=1 its value is N, so no pole is part of the result. All
+cost probabilities are the coefficients of this explicit polynomial.
+In particular P(C=0)=q^(-2N), and costs above N have probability zero.
+
+To prove the formula, sum the cited joint count over r at each D>=1:
+
+    g^(-1) sum_r #{M:D(M)=D,C(M)=r} z^r
+       = (q^2-1) z q^(D-1) (1+(q-1)z)^(D-1)
+       = (q^2-1) z B(z)^(D-1).
+
+Add the degree-zero contribution 1 and sum D=1,...,N. Division by
+q^(2N) gives G_N. At z=1, B(1)=q^2 and the numerator is q^(2N), which
+also confirms normalization. This is a finite polynomial identity.
+
+## Closed first and second moments
+
+Set e=q^(-2N). For every N>=0,
+
+    E[C] = (q-1)N/q + (1-e)/(q+1),
+
+    Var(C) = (q-1)N/q^2
+             + 2(q-1)N e/[q(q+1)]
+             - (1-e)(q-e)/(q+1)^2.
+
+Here is a direct derivation that accounts for the exceptional degree-zero
+case. Under the bounded-degree measure,
+
+    P(D=0)=e,
+    P(D=d)=(q^2-1)q^(2d-2-2N),    1<=d<=N.
+
+Its tail is P(D>=j)=1-q^(2j-2-2N) for 1<=j<=N. Finite geometric sums give
+
+    E[D] = N-(1-e)/(q^2-1),
+    E[D^2] = N^2-2N/(q^2-1)+(q^2+1)(1-e)/(q^2-1)^2.
+
+For example the second identity follows by summing
+(2j-1)P(D>=j). Both identities also hold at N=0.
+
+Write p=(q-1)/q. At D=d>=1 the cited binomial law gives
+
+    E[C|D=d] = pd+1/q,
+    E[C^2|D=d] = p^2 d^2+3p(1-p)d+(1-p)(1-2p).
+
+At D=0, both conditional moments are zero. Therefore the constant terms
+in these two expressions must be multiplied by 1-e when averaging.
+Substituting the displayed moments of D gives the claimed mean and
+
+    E[C^2] = (q-1)^2 N^2/q^2
+              +(q-1)(3q+1)N/[q^2(q+1)]
+              -(q-1)(1-e)/(q+1)^2.
+
+Subtracting the square of the mean gives the stated variance. This uses
+only rational finite-sum identities, so there is no limiting interchange.
+
+For N>=1, the exact-degree-N mean exceeds the new mean by exactly
+
+    1/[q(q+1)] + q^(-2N)/(q+1).
+
+Thus replacing exact-degree sampling by bounded-degree sampling changes
+even the constant term in typical cost. It does not change the alphabet,
+the cost of any particular target, or the worst-case cost N.
+
+## Evidence and scope
+
+The verifier separately forms the finite mixture from the cited joint
+count and the polynomial coefficients from the new geometric formula.
+It measures the resulting first and second moments by integer sums and
+compares them with the closed expressions. A weighted digit-string
+enumeration checks a different realization of the new mixture. This is
+not a new enumeration or independent validation of polynomial matrices.
+
+The theorem covers every prime power q and every N>=0. Finite arithmetic
+checks also use integer q that are not prime powers, solely as algebraic
+substitutions. No nonexistent finite field is claimed for those q.
+
+Uniform words, singular endpoints, more roles, restored auxiliary roles,
+other coefficient algebras and native implementations are outside scope.
+Preparation, conversion, routing, control, precision, restoration, stock
+and complete supplier costs remain unpriced. All selected framework
+assumptions retain their status. Independent human and formal proof-kernel
+review are unclaimed.
+
+PR4784's retained credit includes Nick Petalas's PR4763/4276/4243,
+Wentao Li's PR4099 following PR2513, ToikY's PR4334, and the local/semilocal
+comparisons. Nagao's polynomial-matrix presentation and degree method
+remain classical predecessor work. The new contribution is the
+bounded-degree sampling formula and its closed moments.

research/degree-bounded-polynomial-cost/README.md

@@ -0,0 +1,115 @@
+# Exact cost law for uniform bounded-degree polynomial targets
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+Scoped counting proof with exact finite corroboration. This answers Open next
+question 1 of [PR4784](https://github.com/CrocSwap/integer-mult-bounds/pull/4784).
+Its exact-degree count is a cited premise, not an audit deliverable.
+
+Choose M uniformly among GL2(F_q[t]) matrices of maximum entry degree at most
+N. Paid factors are I+u y^T with polynomial u and base-field y. GL2(F_q) maps
+are free anywhere, there are two roles, and no auxiliary role is available.
+Let C be the minimum paid cost, e=q^(-2N) and B(z)=q+q(q-1)z. The new law is
+
+```text
+E[z^C] = q^(-2N) [1+(q^2-1)z (B(z)^N-1)/(B(z)-1)],
+E[C]   = (q-1)N/q + (1-e)/(q+1),
+Var(C) = (q-1)N/q^2 + 2(q-1)Ne/[q(q+1)] - (1-e)(q-e)/(q+1)^2.
+```
+
+The quotient is the finite geometric polynomial, including its removable
+value N at B=1. The formulas hold for every prime power q and N>=0. They
+include the constant matrices, whose cost is zero. For N>=1, the bounded-
+degree mean is below the exact-degree-N mean by exactly
+`1/[q(q+1)]+q^(-2N)/(q+1)`. The individual target costs are unchanged.
+[PROOF.md](PROOF.md) supplies the finite-sum derivation.
+
+For example, q=2 and N=4 gives count weights `[1,45,102,84,24]`, divided by
+the common factor |GL2(F2)|. The mean is 597/256 and variance 51399/65536.
+The weights agree with the predecessor's existing binary bounded-degree
+census; that census is credited prior work. The new result is the closed
+law and moments for the changed sampling measure at arbitrary q and N.
+
+## Evidence and reproduction
+
+The verifier compares the cited joint-count mixture with an independently
+formed geometric polynomial for all 495 integer pairs 2<=q<=16, 0<=N<=32.
+It checks both moments by exact coefficient sums, and evaluates the PGF at
+1,980 rational points, including every removable-pole case. Non-prime-power
+q only test arithmetic identities, not finite fields.
+
+A second enumeration covers 7,362 weighted digit strings in 28 small
+mixtures, with q=2..5 and N=0..6. These are digit strings, not a fresh
+polynomial-matrix census. Three boundary fixtures and ten rejection controls
+cover invalid domains, omission of the free targets, exact-degree sampling,
+an incorrect mean and an incorrect variance. No predecessor program runs.
+
+From the repository root, using standard-library CPython 3.12:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/degree-bounded-polynomial-cost/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/degree-bounded-polynomial-cost/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/degree-bounded-polynomial-cost
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/degree-bounded-polynomial-cost --check-source-history
+```
+
+Another CPython 3.12 executable may replace the local interpreter path.
+The direct marker is `PASS_DEGREE_BOUNDED_POLYNOMIAL_COST`. The generated
+stdout receipt binds all six package files and the cited proof by SHA256.
+Replay writes no checkout files. Registered commands each have a 120-second
+limit. [VERIFY.json](VERIFY.json) declares the sole external proof input.
+
+The discovery base is canonical main
+`7c49fe32c55de02c2c873655c804b16e4c3fef0a`, priorities revision 8, selected
+PR6030. The selected source-binding orientation passed; no selected scientific
+replay ran. [TASK.json](TASK.json) changes the scalar-to-moment card to this
+formal-algebra side result and records the
+[advance CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19370254).
+Live open/account PRs, recent claims, local reservations, main formula/object
+searches and merged searches were checked. The overlap cache covers 506 open
+PRs and 6,507 Discussion records with complete remote pagination. Sparse
+local notes, arbitrary historical diffs and unpublished work remain limits.
+
+## Limits and implementation bounds
+
+The universal result uses PR4784's cited degree/cost theorem. It does not
+reprove its normal form. Uniform words, singular targets, other coefficient
+algebras, more roles and restored auxiliary roles are outside scope. Native
+preparation, conversion, routing, control, precision, restoration, stock and
+complete supplier costs remain unpriced. No new kappa, selected-frontier
+change, supplier admission or complete multiplication theorem is claimed.
+All five selected assumptions remain. Independent human and formal proof-
+kernel review are unclaimed. Lean, Docker and selected cold replay are unrun.
+
+The code has no recursion, subprocess, network, dynamic code or callbacks.
+q and N have explicit finite bounds; coefficient lists have at most 33
+entries and digit tuples at most five. At most 495 parameter records are
+retained. Seven source reads are capped at 256 KiB each. Functions fit within
+60 lines. Guards remain enabled under optimization. Warning-strict normal
+and optimized execution supplies interpreted-code diagnostics; no external
+static analyzer is claimed. Managed Python allocation is a Power of Ten
+rule 3 deviation: CPython integer arithmetic and JSON serialization allocate
+during verification. The fixed domains and file capacities bound retained
+state, and both registered runs exercise their maximum q and N. Revisit
+these capacities before expanding the domain; a fixed-storage runtime port
+would need its own arithmetic and receipt implementation.
+
+## Open next questions
+
+- Obtain a quantitative normal-approximation error for this exact bounded-
+  degree measure. Start with the geometric degree deficit and the cited
+  conditional binomial law. A uniform error estimate is not supplied here.
+- Identify one native polynomial-coefficient producer and consumer before
+  applying this formal law to a supplier. First price coefficient preparation,
+  then conversion, restoration and the complete recursive bill. Those costs
+  and the physical interface are missing.
+
+## Credit
+
+Nick Petalas's PR4784 supplies the exact-degree theorem and the explicit
+bounded-degree moment question. Its retained lineage includes PR4763/4276/4243,
+Wentao Li's PR4099 following PR2513, ToikY's PR4334 and the local/semilocal
+comparisons. Nagao's polynomial-matrix presentation and degree method remain
+classical predecessor work. [SOURCES.json](SOURCES.json) pins the unchanged
+predecessor proof. The new contribution is the bounded-degree sampling law
+and its closed moments, not a new classical normal-form theorem.

research/degree-bounded-polynomial-cost/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/polynomial-cost-distribution/PROOF.md",
+      "usage": "input",
+      "git_blob": "6a682dab6d2c5f26e2e40c1f98edad6fbcbcd327",
+      "sha256": "946370455b5f64cfa1cee22eca97c19102aca3ef07f5da7f98eb1bf419bdbf9e"
+    }
+  ]
+}