diff --git a/research/degree-bounded-polynomial-cost/PROOF.md b/research/degree-bounded-polynomial-cost/PROOF.md new file mode 100644 index 0000000000..106faf717f --- /dev/null +++ b/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. diff --git a/research/degree-bounded-polynomial-cost/README.md b/research/degree-bounded-polynomial-cost/README.md new file mode 100644 index 0000000000..6a145c9138 --- /dev/null +++ b/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. diff --git a/research/degree-bounded-polynomial-cost/SOURCES.json b/research/degree-bounded-polynomial-cost/SOURCES.json new file mode 100644 index 0000000000..25210688bd --- /dev/null +++ b/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" + } + ] +} diff --git a/research/degree-bounded-polynomial-cost/TASK.json b/research/degree-bounded-polynomial-cost/TASK.json new file mode 100644 index 0000000000..67a0da5bed --- /dev/null +++ b/research/degree-bounded-polynomial-cost/TASK.json @@ -0,0 +1,127 @@ +{ + "schema_version": 1, + "task_id": "scalar-to-moment", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "original_card": { + "id": "scalar-to-moment", + "question": "Can a scalar/frame rewrite improve the complete signed moment through paid jobs, productive targets, or both?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "docs/research/recursive-invoice-preflight.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "Require a legal chronological rewrite and favorable complete signed target-minus-paid moment with all extra charges. Unchanged ADD counts or unchanged paid-call counts alone decide neither success nor failure. Compiler, native and outer admission remain separate obligations.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Construct one legal source-bound rewrite and compare complete before/after P and T. Charge restoration, source windows and owned helpers. A paid call need not disappear: a legal target split or rank redistribution may win. Stop if the signed moment is unchanged or the consumer repays the gain. Do not extend a scalar-only census on ADD counts.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "signed moment", + "target split", + "rank exchange", + "scalar rewrite" + ], + "existing_checks": [ + { + "scope": "PR #3998: consecutive A2 scalar contraction", + "evidence": "research/staged544-a2-graph-rewrite/README.md", + "remaining": "A genuinely changed paid itinerary or a distinct independent audit; no default scalar-only expansion.", + "status": "author-checked", + "source_commit": "389268a6b5e0373a3125d5c6fcd6995f4ea324f5", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4019: separated A2 sites with unchanged recursive histogram", + "evidence": "research/staged544-separated-a2/README.md", + "remaining": "A genuinely changed paid itinerary or a distinct independent audit; no default scalar-only expansion.", + "status": "author-checked", + "source_commit": "f408e09df300b575235f7f77f81948071397e16d", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4112: composition audit", + "evidence": "research/staged544-a2-composition-audit/README.md", + "remaining": "A genuinely changed paid itinerary or a distinct independent audit; no default scalar-only expansion.", + "status": "author-checked", + "source_commit": "205b7380656ba4b6316a8a493b1a3c679b8f7a0e", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4152: A1858 contraction audit", + "evidence": "research/staged544-a1858-contraction-audit/README.md", + "remaining": "A genuinely changed paid itinerary or a distinct independent audit; no default scalar-only expansion.", + "status": "author-checked", + "source_commit": "caaa14cde5962adc372fdca71f63d0f29e73c8b2", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Exact probability-generating function, mean and variance for uniform invertible two-role polynomial targets of entry degree at most N over every finite field.", + "scope_change_reason": "Changes the selected scalar-to-moment suggestion to Open next question 1 of PR4784, a formal-algebra counting question. Its joint exact-degree count is a cited premise; the new result is the bounded-degree mixture and closed moments, with no native rewrite or claimed kappa gain.", + "bottleneck_link": "Formal factor counts can diagnose coefficient-algebra costs, but this sampling law is a side result. A native coefficient producer, physical consumer and complete invoice remain missing.", + "budget_minutes": 60, + "stop_rule": "Stop at the first verified generating function and moments. Package them without extending to other algebras, roles or asymptotic distribution theorems.", + "outcome": "completed", + "evidence": "PROOF.md derives the new law from the cited PR4784 theorem. verify.py checks 495 exact parameter pairs, 1980 PGF evaluations, 7362 weighted digit strings in 28 mixtures, three boundary fixtures and ten rejection controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "What quantitative normal-approximation error holds under the bounded-degree target measure?", + "why_it_matters": "Closed moments alone do not control finite-degree probability tails.", + "first_step": "Combine the geometric degree-deficit law with the cited conditional binomial distribution.", + "blocked_by": "No uniform approximation error bound is established here." + }, + { + "question": "Can a literal native interface realize the polynomial coefficient algebra at a useful complete price?", + "why_it_matters": "Abstract factor statistics do not establish supplier costs or a kappa improvement.", + "first_step": "Identify one coefficient producer and price its preparation and full consumer.", + "blocked_by": "Native conversion, routing, precision, restoration and stock costs remain unknown." + } + ], + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19370254", + "question_source": { + "pr": 4784, + "author": "petalas", + "created_at": "2026-10-22T19:56:30Z", + "head": "4d0a6363fe4f45dd9a769f5b74d02fc5d9061ae3", + "question": "Open next question 1: closed moments for uniform degree-bounded targets." + }, + "upstream_check": { + "commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "checked_at": "2026-11-03T09:15:02Z", + "priority_revision": 8, + "coverage": "Canonical main refreshed unchanged before submission. Live open/account lists, recent handoffs, active Discussions, source/model searches, main README quantity/formula searches and merged PR searches were checked. The cache covers 506 open PRs and 6507 Discussion records with complete remote pagination. Sparse local notes, arbitrary historical diffs and unpublished work remain limits." + } +} diff --git a/research/degree-bounded-polynomial-cost/VERIFY.json b/research/degree-bounded-polynomial-cost/VERIFY.json new file mode 100644 index 0000000000..ec8f73a6de --- /dev/null +++ b/research/degree-bounded-polynomial-cost/VERIFY.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/polynomial-cost-distribution/PROOF.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact bounded-degree PGF coefficients, closed moments, weighted digit mixtures, boundary cases and rejection controls." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Repeat the complete exact check with Python assertions disabled." + } + ] +} diff --git a/research/degree-bounded-polynomial-cost/verify.py b/research/degree-bounded-polynomial-cost/verify.py new file mode 100644 index 0000000000..4b813c2a25 --- /dev/null +++ b/research/degree-bounded-polynomial-cost/verify.py @@ -0,0 +1,185 @@ +#!/usr/bin/env python3 +"""Exact corroboration of the new degree-bounded sampling formulas.""" + +import hashlib +import itertools +import json +import math +import platform +from fractions import Fraction +from pathlib import Path + + +MAX_Q = 16 +MAX_N = 32 +MAX_FILE_BYTES = 262144 +SOURCE = "research/polynomial-cost-distribution/PROOF.md" +SOURCE_SHA256 = "946370455b5f64cfa1cee22eca97c19102aca3ef07f5da7f98eb1bf419bdbf9e" +FILES = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py") + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def domain(q, n): + require(type(q) is int and 2 <= q <= MAX_Q, "q outside finite check domain") + require(type(n) is int and 0 <= n <= MAX_N, "N outside finite check domain") + + +def source_mixture(q, n): + """Use the cited joint count, divided by the common free-group factor.""" + domain(q, n) + counts = [1] + [0] * n + for degree in range(1, n + 1): + for cost in range(1, degree + 1): + counts[cost] += ((q + 1) * (q - 1) ** cost * q ** (degree - 1) + * math.comb(degree - 1, cost - 1)) + return tuple(counts) + + +def geometric_counts(q, n): + """Coefficients of 1+(q^2-1)z sum_{j 0, "empty measure") + mean = Fraction(sum(k * count for k, count in enumerate(counts)), total) + second = Fraction(sum(k * k * count for k, count in enumerate(counts)), total) + return mean, second - mean * mean + + +def closed_moments(q, n): + domain(q, n) + epsilon = Fraction(1, q ** (2 * n)) + mean = Fraction((q - 1) * n, q) + (1 - epsilon) / (q + 1) + variance = (Fraction((q - 1) * n, q * q) + + Fraction(2 * (q - 1) * n, q * (q + 1)) * epsilon + - (1 - epsilon) * (q - epsilon) / (q + 1) ** 2) + return mean, variance + + +def evaluate(coefficients, value): + result = Fraction(0) + for coefficient in reversed(coefficients): + result = result * value + coefficient + return result + + +def quotient_value(q, n, value): + base = q + q * (q - 1) * value + geometric = n if base == 1 else (base ** n - 1) / (base - 1) + return (1 + (q * q - 1) * value * geometric) / q ** (2 * n) + + +def verify_formulas(): + cases = 0 + evaluations = 0 + rows = [] + for q, n in itertools.product(range(2, MAX_Q + 1), range(MAX_N + 1)): + counts = source_mixture(q, n) + require(counts == geometric_counts(q, n), "PGF coefficient mismatch") + require(sum(counts) == q ** (2 * n), "wrong bounded-degree normalization") + require(measured_moments(counts) == closed_moments(q, n), "moment mismatch") + require(closed_moments(q, n)[1] >= 0, "negative variance") + for value in (Fraction(0), Fraction(1), Fraction(-1, q), Fraction(2, 3)): + actual = evaluate(counts, value) / q ** (2 * n) + require(actual == quotient_value(q, n, value), "quotient mismatch") + evaluations += 1 + if n: + exact_degree_mean = 1 + Fraction((n - 1) * (q - 1), q) + reduction = Fraction(1, q * (q + 1)) + Fraction(1, (q + 1) * q ** (2 * n)) + require(exact_degree_mean - closed_moments(q, n)[0] == reduction, + "sampling-measure mean gap mismatch") + rows.append((q, n, counts)) + cases += 1 + digest = hashlib.sha256(json.dumps(rows, separators=(",", ":")).encode()).hexdigest() + return {"parameter_cases": cases, "pgf_evaluations": evaluations, "counts_sha256": digest} + + +def verify_digit_space(): + """Enumerate the new mixture via weighted digit strings, not matrices.""" + strings = 0 + cases = 0 + for q, n in itertools.product(range(2, 6), range(7)): + counts = [1] + [0] * n + for degree in range(1, n + 1): + weight = (q * q - 1) * q ** (degree - 1) + for digits in itertools.product(range(q), repeat=degree - 1): + cost = 1 + sum(digit != 0 for digit in digits) + counts[cost] += weight + strings += 1 + require(tuple(counts) == geometric_counts(q, n), "digit-space mismatch") + cases += 1 + return {"digit_space_cases": cases, "weighted_digit_strings": strings} + + +def verify_controls(): + rejected = 0 + for q, n in ((1, 0), (17, 0), (2, -1), (2, 33), (True, 0), (2, False)): + try: + source_mixture(q, n) + except ValueError: + rejected += 1 + else: + raise ValueError("invalid domain accepted") + counts = geometric_counts(2, 1) + require(counts == (1, 3), "degree-zero boundary changed") + require(measured_moments(counts) == (Fraction(3, 4), Fraction(3, 16)), + "degree-one bounded measure changed") + require(closed_moments(2, 0) == (0, 0), "constant targets have nonzero cost") + controls = ((measured_moments((0, 3)), closed_moments(2, 1)), + ((Fraction(1), Fraction(0)), closed_moments(2, 1)), + ((Fraction(5, 6), Fraction(3, 16)), closed_moments(2, 1)), + ((Fraction(3, 4), Fraction(1, 4)), closed_moments(2, 1))) + for counterfeit, actual in controls: + require(counterfeit != actual, "incorrect sampling formula escaped control") + rejected += 1 + return {"rejected_controls": rejected, "boundary_fixtures": 3} + + +def bounded_hash(path): + with path.open("rb") as stream: + data = stream.read(MAX_FILE_BYTES + 1) + require(len(data) <= MAX_FILE_BYTES, "source file exceeds byte bound") + return hashlib.sha256(data).hexdigest() + + +def main(): + package = Path(__file__).resolve().parent + source_hash = bounded_hash(package.parents[1] / SOURCE) + require(source_hash == SOURCE_SHA256, "cited proof bytes changed") + evidence = verify_formulas() | verify_digit_space() | verify_controls() + example = geometric_counts(2, 4) + mean, variance = measured_moments(example) + receipt = { + "status": "PASS_DEGREE_BOUNDED_POLYNOMIAL_COST", + "claim_type": "scoped counting proof with exact finite corroboration", + "python": platform.python_version(), + "evidence": evidence, + "binary_degree_four_example": { + "counts_divided_by_GL2": example, + "mean": str(mean), "variance": str(variance), + }, + "sha256": {name: bounded_hash(package / name) for name in FILES} | {SOURCE: source_hash}, + } + print(json.dumps(receipt, sort_keys=True)) + print("PASS_DEGREE_BOUNDED_POLYNOMIAL_COST no_new_kappa") + + +if __name__ == "__main__": + main()