From 8b37cd3d519365bbfe7404eccfba2262d970c6af Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 27 Oct 2026 12:04:13 +0000 Subject: [PATCH] feat(research): prove sharp Newton residual prefix cutoff --- .../newton-residual-prefix-floor/PROOF.md | 190 +++++++++++++++ .../newton-residual-prefix-floor/README.md | 134 ++++++++++ .../newton-residual-prefix-floor/SOURCES.json | 35 +++ .../newton-residual-prefix-floor/TASK.json | 129 ++++++++++ .../newton-residual-prefix-floor/VERIFY.json | 38 +++ .../newton-residual-prefix-floor/verify.py | 229 ++++++++++++++++++ 6 files changed, 755 insertions(+) create mode 100644 research/newton-residual-prefix-floor/PROOF.md create mode 100644 research/newton-residual-prefix-floor/README.md create mode 100644 research/newton-residual-prefix-floor/SOURCES.json create mode 100644 research/newton-residual-prefix-floor/TASK.json create mode 100644 research/newton-residual-prefix-floor/VERIFY.json create mode 100644 research/newton-residual-prefix-floor/verify.py diff --git a/research/newton-residual-prefix-floor/PROOF.md b/research/newton-residual-prefix-floor/PROOF.md new file mode 100644 index 0000000000..03a2710fba --- /dev/null +++ b/research/newton-residual-prefix-floor/PROOF.md @@ -0,0 +1,190 @@ +# A sharp full-precision prefix cutoff for Gaussian Newton residuals + +This scoped proof concerns the literal valuation-pruned Walsh gather in +[Ali Romman's PR #5825](https://github.com/CrocSwap/integer-mult-bounds/pull/5825), +at `baea91d8c0044a0036006bdd3b4d7bce3d6cf783`. That package states the +degree-zero prefix obstruction. The new step here covers every positive +degree, identifies the exact uniform cutoff and needs no assumption on the +bulk's precision or cost. The construction and creation-precision contract +come from David Ganz / Dugongue's #5815 and #5813, as cited by #5825. +Their implementations and numerical results are not replayed here. + +## Contract and theorem + +Let pi = 1+i, n >= 1, N = 2^n, 0 <= R < n, 0 <= a <= n-R and p >= 0. +The exponent p is an integer. Use the integer-valued generalized binomial +polynomials, including at negative arguments, and put + +```text +g(j) = i^a sum_{h=0}^R (i-1)^h binom(j-a,h), +d_j = i^j - g(j), +e_j = d_j / pi^(R+1), +Q = p+2n-R-1. +``` + +The source's Newton residual theorem supplies the integral e_j. Lemma 1 +below also proves that integrality directly. A Walsh leaf lambda has weight +j and beta_lambda = v_pi(e_j), with v_pi(0) = infinity. Its prescribed +creation demand is q_lambda = max(0,Q-beta_lambda). An absent leaf has +demand zero. Every prefix must be created with at least the largest demand +of its descendants. This is the named max-descendant precision contract, +not a lower bound for every circuit computing the same operator. + +For a nonempty prefix v at depth d, its literal child-array ADD incidence +mass is 2^(n-d) q_v. Thus the gather ADD precision mass is at least + +```text +M >= 2^n (n-R-1) (p+2n-R-1). (1) +``` + +More precisely, **every prefix at every depth 1 <= d <= n-R-1 must have +q_v >= Q**. At depth n-R there is a prefix with demand exactly zero, for +every permitted a. Consequently n-R-1 is the exact last depth through +which every prefix is uniformly forced to Q. When n-R-1 = 0, the assertion +about nonempty forced levels and the lower bound are empty, as they should be. +The root still has demand Q whenever Q > 0. + +The result is independent of the fixed order of the axes. A prefix of +weight w always has possible completion weights w,w+1,...,w+n-d, regardless +of that order. A node-dependent axis order that still fixes one fresh axis +at each step has the same property and the same full binary tree counts. + +## Lemma 1: the first surviving digit + +For every integer t and every R >= 0, + +```text +i^t - sum_{h=0}^R (i-1)^h binom(t,h) + = (i-1)^(R+1) binom(t,R+1) mod pi^(R+2). (2) +``` + +For t >= 0, this is the ordinary binomial expansion with terms of higher +degree omitted. For t < 0, work in Z[i]/(pi^(R+2)). The element u=i-1=i*pi +is nilpotent there. The finite geometric series gives the inverse of 1+u. +Raising that inverse to the positive integer -t gives the generalized +binomial expansion through degree R+1. Equivalently, the identity holds +in Z[[u]] for every integer power of 1+u, and substitution of the nilpotent +u removes every term of degree at least R+2. This justifies negative +offsets without an analytic convergence premise. + +All terms omitted after degree R are divisible by pi^(R+1), so e_j is +integral. Dividing (2) by pi^(R+1), and multiplying by i^a, gives + +```text +e_j = i^(a+R+1) binom(j-a,R+1) mod pi. +``` + +The residue field Z[i]/(pi) is F2, and every power of i maps to one. +Therefore + +```text +v_pi(e_j) = 0 iff binom(j-a,R+1) is odd. (3) +``` + +This is an exact criterion. It does not estimate higher valuations. + +## Lemma 2: no long gap in odd generalized binomials + +Fix k >= 1. The kth forward difference of binom(t,k) is one. In integer +form, for every t in Z, + +```text +sum_{r=0}^k (-1)^(k-r) binom(k,r) binom(t+r,k) = 1. (4) +``` + +Pascal's identity gives Delta binom(t,k) = binom(t,k-1) for every integer t. +Applying it k times proves (4). If every binom(t+r,k) in this window were +even, its left side would be even, a contradiction. Thus **every k+1 +consecutive integer arguments contain an odd value**. The run of k zeros +at t=0,...,k-1 shows that this window length is sharp. + +For a prefix at depth d <= n-R-1, the unprocessed count m=n-d is at least +R+1. Its completion weights contain at least R+2 consecutive values. +Apply Lemma 2 with k=R+1 and t=w-a. Lemma 1 supplies a descendant with +beta=0, hence creation demand Q. This proves the forced-level assertion. + +At each such depth, there are 2^d prefixes. Each has child-array length +2^(n-d), so that depth alone contributes at least NQ. Summing the +n-R-1 nonempty forced levels proves (1). A schedule that overallocates +precision can only increase this lower bound. + +## Sharp cutoff + +At depth d=n-R choose any prefix of weight a; this is possible because +0 <= a <= d. Its completion weights are exactly a,a+1,...,a+R. For +0 <= t <= R, the binomial expansion terminates by degree R, so d_(a+t)=0. +Every descendant is absent and this prefix's minimum demand is zero. +This proves sharpness of the full-precision depth, not attainment of the +total mass lower bound (1). Later nonzero prefixes may add substantial mass. + +## Exact full-precision counts at later levels + +The same first-digit criterion supplies an independent finite check of every +later prefix. Set k=R+1 and L=2^s, where s is the bit length of k. For every +integer t, + +```text +binom(t,k) is odd iff ((t mod L) AND k) = k. (5) +``` + +In F2[z]/(z^(k+1)), the identity (1+z)^L=1 holds because L>k. +Thus the coefficient of z^k in (1+z)^t depends only on t mod L, also for +negative t. Expanding a nonnegative residue in binary gives a product of +factors 1+z^(2^b). The z^k coefficient is one exactly when every set bit of +k is available in that residue. This proves (5) without assuming a +nonnegative offset. + +At depth d with m=n-d, the exact number of minimum-demand prefixes at Q is + +```text +F_d = sum_{w=0}^d binom(d,w) + * 1{ there exists u in {0,...,m} with + (((w+u-a) mod L) AND k) = k }. (6) +``` + +For Q>0, beta=0 is exactly the condition q_lambda=Q, so (6) counts +full-precision prefixes, rather than merely live prefixes. This formula +is used only as corroboration and a reusable exact count; it does not +claim that all live coefficients have valuation zero. + +## A low-degree obstruction even with a free bulk + +For n >= 4 and 1 <= R <= floor(n/2)-1, the forced-level count is at least +n/2 and Q >= p+n. Hence the residual gather alone satisfies + +```text +M >= (n/2) 2^n (p+n). (7) +``` + +At p=Theta(n) this is Omega(2^n n^2) ADD precision mass, even if the bulk +and every other operation are free. More generally, n-R-1 >= epsilon*n +gives the same conclusion for fixed positive epsilon. This strengthens +the applicable low-degree part of #5825's cost obstruction by dropping +its uniform-bulk-precision premise. It makes no statement about the +high-degree heterogeneous bulk or the cost of a different residual graph. + +The metered ADD precision model is not by itself a physical bit-time +theorem. Changes to the graph, arithmetic representation, divisibility +handling, normalization, or creation-demand contract can evade this +obstruction. No bound on arbitrary Gaussian algorithms, shared responses, +native suppliers or finite networks follows. All five selected framework +assumptions remain open at their existing scope. No new kappa is claimed. + +## Evidence and credit + +The proof above is the all-size argument. The standalone verifier constructs +Gaussian residual coefficients from their falling-factorial definition, +performs every division exactly and compares the first surviving digit with +(5). Its positive-degree census checks all offsets, including negative +j-a. It separately checks (4), enumerates every binary prefix in its tree +domain, compares (6), checks (1) and (7), and constructs the sharp zero +prefix. Eight underprecision profiles must be rejected. Finite checks +corroborate the proof; they are not formal proof-kernel acceptance. + +This contribution was produced by Nick Petalas. Credit Ali Romman #5825 +for the degree-zero obstruction and explicit metered graph, David Ganz / +Dugongue #5815 for the valuation-pruned residual and #5813 for its Gaussian +spectral predecessor. Their retained native, precision, ownership and +compiler contributors keep their predecessor credit. Generalized binomial +identities, finite differences and binary coefficient parity are classical +facts. No novelty is claimed for those facts separately. diff --git a/research/newton-residual-prefix-floor/README.md b/research/newton-residual-prefix-floor/README.md new file mode 100644 index 0000000000..abd64db9d6 --- /dev/null +++ b/research/newton-residual-prefix-floor/README.md @@ -0,0 +1,134 @@ +# Sharp full-precision depth for Gaussian Newton residuals + +For the degree-R consecutive-interval Gaussian Newton residual, every +Walsh prefix through depth **n-R-1** needs full creation precision +Q=p+2n-R-1 under the max-descendant demand contract. The cutoff is sharp +for every interpolation offset. At depth n-R a prefix lies entirely in +the zero residual band and needs no creation precision. + +The resulting residual-gather ADD precision mass is at least + +```text +2^n (n-R-1) (p+2n-R-1). +``` + +This is a **scoped written proof with finite corroboration**. It extends +Ali Romman's [PR #5825](https://github.com/CrocSwap/integer-mult-bounds/pull/5825) +degree-zero obstruction to arbitrary positive degree. The new argument +uses the first surviving Gaussian digit and a finite-difference identity. +The exact full-precision prefix count at every depth is also given in +[PROOF.md](PROOF.md), including negative Newton offsets and arbitrary +axis order. Classical binomial identities are not claimed as new. + +For n >= 4 and 1 <= R <= floor(n/2)-1, the residual alone costs at least +(n/2) 2^n (p+n). At p=Theta(n) this is Omega(2^n n^2), even granting a +free bulk. This removes the predecessor's uniform-bulk-precision premise +in that low-degree range. It is an ADD precision statement about the +named graph, not a physical bit-time or arbitrary-circuit lower bound. + +## Evidence + +The self-contained [verifier](verify.py) imports no predecessor code and +runs no predecessor fixture. Its complete fixed domains are: + +- Positive-degree Gaussian coefficients for 2 <= n <= 24, every + 1 <= R < n, every 0 <= a <= n-R and every 0 <= j <= n. There are + 49,726 coefficients, including 14,950 negative offsets, 2,576 zero-band + witnesses and 29,900 consecutive unit-containing windows. +- All binary prefixes for 2 <= n <= 10, every positive R and permitted a, + and p in {0,1,3}. There are 630 trees and 551,700 literal prefixes. + Each tree checks the sharp cutoff; 336 also meet the low-degree corollary. +- 16,448 signed-argument binomial parity cases and 4,128 exact + finite-difference windows. Eight separately lowered forced-prefix + precision profiles must be rejected. + +For n=8, R=3, a=2 and p=3, the exact gather mass is 21,540, while the +new forced-level lower bound is 15,360. The theorem claims sharpness of +the cutoff, not equality in that total mass bound. + +Each direct run prints `PASS_NEWTON_RESIDUAL_PREFIX_FLOOR` and a generated +receipt binding the six package files by SHA256. The written proof supplies +the universal argument; finite enumeration is corroboration. No receipt +is handwritten or committed. No generated files are written by the verifier. + +## Reproduce + +From the repository root, with CPython 3.12 and no third-party packages: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -X dev -I -B research/newton-residual-prefix-floor/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -X dev -I -O -B research/newton-residual-prefix-floor/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/newton-residual-prefix-floor +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/newton-residual-prefix-floor --check-source-history +``` + +The last command checks a committed package. The two registered commands +repeat the complete domain in normal and optimized modes with warnings +as errors and development diagnostics. They each have a 120-second timeout. +The interpreter path is the local reproduction path; another clean CPython +3.12 installation can replace it. Git-free direct replay needs only these +six files. Historical catalogue and selected-record pins require full Git +history for metadata validation, not for the mathematical verifier. + +## Limits + +The contract fixes the residual definition, its normalization, literal +Walsh-prefix graph and max-descendant creation demands. It permits exact +coefficient-valuation pruning. A changed graph, representation, integral +dependency treatment or demand contract is outside the theorem. The +near-full-degree heterogeneous bulk remains unresolved. No physical caller, +native implementation, storage/restoration protocol, complete bit-time tariff, +new kappa or complete multiplication theorem is supplied. The selected +frontier and its five assumptions are unchanged. Independent human and +formal proof-kernel review are unclaimed. + +The original `p104-side-correction` card is explicitly changed to this +component obstruction in [TASK.json](TASK.json). [SOURCES.json](SOURCES.json) +pins the original card and selected record as provenance and gives exact +cited predecessor heads. External citations are context, not replay inputs. +No unmerged source object is required by the scientific verifier. + +## Open next questions + +1. Can a changed residual graph exploit integral Walsh dependencies to beat + max-descendant creation demands? This is a possible escape from the + obstruction. Start with an explicit arbitrary-input graph and exact + quotient/precision map. A replacement graph and complete invoice are missing. +2. Does a heterogeneous high-degree Newton bulk retain an obstruction when + n-R is sublinear? The residual bound then loses its n-scale factor. + Start with backward precision demands on a named falling-factor graph, + including coefficient valuations. No such bulk lower bound is proved here. + +These questions and their blockers are recorded in TASK.json. No follow-up +is reserved by this contribution. + +## Implementation constraints + +The verifier uses explicit runtime checks, so optimization disables none +of its mathematical obligations. All loops have fixed census bounds; +there is no recursion, dynamic import, evaluation or concurrent work. +Every function has fewer than 60 physical lines. The largest tree has +2,048 integer entries. Only one tree and its eight sequential rejection +mutants are processed at a time. Gaussian valuations reject coefficient +norms exceeding a 1,024-bit resource bound. No physical address or machine +allocation guarantee is claimed for Python objects. + +Rule 3 deviation, verify.py: CPython necessarily allocates integer and +container objects during exact arithmetic. Fixed census sizes, a bounded +tree and coefficient height bound constrain the live mathematical data; +normal and optimized checks exercise the whole domain. Runtime-internal +allocation is not measured. A future native implementation would need its +own capacity and allocation accounting. Rules about C preprocessing and +raw pointer dereferencing have no direct Python mechanism here; the code +uses ordinary direct calls and shallow immutable integer-pair values. +Warning-strict development-mode execution is the available diagnostic gate. + +## Credit + +This contribution was produced by Nick Petalas. Credit Ali Romman #5825 +for the explicit residual graph, precision contract and degree-zero theorem; +David Ganz / Dugongue #5815 for the valuation-pruned residual construction +and #5813 for its Gaussian spectral predecessor; and their retained native, +precision, ownership and compiler contributors. The new contribution is +the positive-degree prefix cutoff, sharpness proof and residual-only +low-degree obstruction. New work is Apache-2.0. diff --git a/research/newton-residual-prefix-floor/SOURCES.json b/research/newton-residual-prefix-floor/SOURCES.json new file mode 100644 index 0000000000..081b7c6ab7 --- /dev/null +++ b/research/newton-residual-prefix-floor/SOURCES.json @@ -0,0 +1,35 @@ +{ + "schema_version": 1, + "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "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" + } + ], + "cited_predecessors": [ + { + "pr": 5825, + "author": "Ali Romman", + "head": "baea91d8c0044a0036006bdd3b4d7bce3d6cf783", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/5825", + "scope": "Degree-zero prefix theorem and explicit residual-tree demand/cost contract. Citation only; no imported code or scientific replay." + }, + { + "pr": 5815, + "author": "David Ganz / Dugongue", + "head": "f0fcda576df410dc15cd5b8183d4f74d284eba2b", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/5815", + "scope": "Valuation-pruned Gaussian residual construction cited by PR5825. Citation only; no imported code or scientific replay." + } + ], + "source_contract": "The theorem, definitions and verifier are self-contained. External predecessor citations identify attribution and context; they are not execution inputs or Git-history pins. No pending predecessor commit is required for replay." +} diff --git a/research/newton-residual-prefix-floor/TASK.json b/research/newton-residual-prefix-floor/TASK.json new file mode 100644 index 0000000000..13e54263a8 --- /dev/null +++ b/research/newton-residual-prefix-floor/TASK.json @@ -0,0 +1,129 @@ +{ + "schema_version": 1, + "task_id": "p104-side-correction", + "priority_revision": 8, + "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "original_card": { + "id": "p104-side-correction", + "question": "Can joint helper bases and a legal causal split improve the complete P104 productive/paid invoice?", + "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", + "research/p104-helper-subspace-splits/README.md", + "research/dyadic-helper-channel-capacity/README.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": "An exact arbitrary-input identity, source/target frame availability and restoration at the chosen cut, plus the complete channel+correction+idle/hosting bill or an explicit favorable bound. The native channel alone is not a supplier. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "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": "Start with the selected #5599 emitted word and review pending #5718 distinct input/output bases plus #5717/#5719 coverage before claiming work. Pick one uncovered source word, helper group and cut region. Prove the arbitrary-input relation and legal entry/exit corrections, then compare full target and paid profiles. Reject if completion, owned lifetimes or consumer costs repay the gain. A static pairing rank alone is not a physical split.", + "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": [ + "P104", + "helper basis", + "helper split", + "5718", + "dyadic capacity" + ], + "existing_checks": [ + { + "scope": "PR #4133: literal-slot defect", + "evidence": "research/p104-literal-slot-defect/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "88666f1dee93fbd85b31fd5d6f91a219e111b5f4", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4136: uniform commutation gap", + "evidence": "research/p104-uniform-commutation-gap/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "281ce601a8be9db470de630759179c23e1dfaa88", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4140: uniform encoding gap", + "evidence": "research/p104-uniform-encoding-gap/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "de25c6525aa866962309df5d107b32d55e6e5628", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4153: source-chart shortcut exhausts its optimistic allowance", + "evidence": "research/p104-source-chart-shortcut/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "9123241fea53df77e51ffe30d9aca1625d4bf3a8", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4154: fiber-tag seam mismatch", + "evidence": "research/p104-fiber-tag-seam/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "4ffcdaee5d6255a9cea1fe53a5424435068089d0", + "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": "Prove the sharp n-R-1 full-precision prefix cutoff for the degree-R consecutive-interval Gaussian Newton residual and the resulting residual-only ADD precision lower bound.", + "scope_change_reason": "This takes the precision-schedule boundary in Ali Romman PR5825 instead of optimizing a physical P104 helper cut. It is a scoped component obstruction, with no supplier or kappa claim.", + "bottleneck_link": "The low-degree residual alone retains input-bit-length times log-input-length ADD precision mass in this explicit graph, even if heterogeneous bulk work is free. A changed residual representation or graph is required for this route to escape.", + "budget_minutes": 60, + "stop_rule": "Ship the first verified extension of the degree-zero predecessor, with no further construction campaign.", + "outcome": "completed", + "evidence": "PROOF.md gives the all-size argument; verify.py emits exact positive-degree coefficient and binary-prefix censuses plus a SHA256-bound receipt.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can a changed residual graph exploit integral Walsh dependencies to beat the max-descendant creation-precision contract?", + "why_it_matters": "The present obstruction depends on that contract and does not exclude a factored or different representation.", + "first_step": "Give one explicit arbitrary-input residual graph and its exact quotient/precision map before searching larger intervals.", + "blocked_by": "No replacement graph or complete arithmetic invoice is supplied." + }, + { + "question": "Does the high-degree heterogeneous Newton bulk retain an all-interval obstruction when n-R is sublinear?", + "why_it_matters": "The residual-only bound loses its n-scale factor near R=n; the uniform-bulk assumption from PR5825 is not removed there.", + "first_step": "Name the bulk arithmetic graph and derive backward precision demands for each falling-factor update, including coefficient valuations.", + "blocked_by": "This package proves only a residual-tree bound; no high-degree bulk lower bound is claimed." + } + ], + "coordination": { + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19216153", + "checked_main": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "priority_revision": 8, + "overlap_limits": "Live PR bodies and handoffs plus distinct main/merged searches were checked. Cached local overlap covers only 200 of 7845 HEAD notes; absence is not a novelty certificate." + } +} diff --git a/research/newton-residual-prefix-floor/VERIFY.json b/research/newton-residual-prefix-floor/VERIFY.json new file mode 100644 index 0000000000..997102645e --- /dev/null +++ b/research/newton-residual-prefix-floor/VERIFY.json @@ -0,0 +1,38 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-X", + "dev", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "New positive-degree parity, finite-difference window, exact coefficient, literal-prefix and sharp-cutoff checks; eight underprecision rejection controls; generated package SHA256 receipt." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-X", + "dev", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Repeat the complete fixed domain with optimization; all mathematical checks remain active." + } + ] +} diff --git a/research/newton-residual-prefix-floor/verify.py b/research/newton-residual-prefix-floor/verify.py new file mode 100644 index 0000000000..7a0db1b973 --- /dev/null +++ b/research/newton-residual-prefix-floor/verify.py @@ -0,0 +1,229 @@ +#!/usr/bin/env python3 +"""Exact corroboration of the positive-degree Newton residual prefix theorem.""" + +import hashlib +import json +import math +import platform +import sys +from pathlib import Path + +Pair = tuple[int, int] +PHASES: tuple[Pair, ...] = ((1, 0), (0, 1), (-1, 0), (0, -1)) +PACKAGE_FILES = ( + "PROOF.md", "README.md", "SOURCES.json", "TASK.json", "VERIFY.json", "verify.py" +) + + +def require(condition: bool, message: str) -> None: + if not condition: + raise RuntimeError(message) + + +def choose(t: int, k: int) -> int: + """Integer falling-factorial definition, including negative upper indices.""" + require(0 <= k <= 64 and abs(t) <= 256, "binomial domain exceeded") + value = 1 + for h in range(1, k + 1): + numerator = value * (t - h + 1) + require(numerator % h == 0, "nonintegral generalized binomial") + value = numerator // h + return value + + +def multiply(z: Pair, w: Pair) -> Pair: + return (z[0] * w[0] - z[1] * w[1], z[0] * w[1] + z[1] * w[0]) + + +def divide_pi(z: Pair) -> Pair: + require((z[0] + z[1]) % 2 == 0, "Gaussian quotient is not integral") + return ((z[0] + z[1]) // 2, (z[1] - z[0]) // 2) + + +def residual(n: int, a: int, degree: int, j: int) -> Pair: + require(2 <= n <= 24 and 1 <= degree < n, "positive-degree domain exceeded") + require(0 <= a <= n - degree and 0 <= j <= n, "invalid weight or offset") + total, power = (0, 0), (1, 0) + for h in range(degree + 1): + coefficient = choose(j - a, h) + total = (total[0] + coefficient * power[0], + total[1] + coefficient * power[1]) + power = multiply(power, (-1, 1)) + total = multiply(PHASES[a % 4], total) + phase = PHASES[j % 4] + value = (phase[0] - total[0], phase[1] - total[1]) + for _ in range(degree + 1): + value = divide_pi(value) + return value + + +def valuation(z: Pair) -> int | None: + if z == (0, 0): + return None + norm = z[0] * z[0] + z[1] * z[1] + limit = norm.bit_length() + require(limit <= 1024, "coefficient height bound exceeded") + for exponent in range(limit): + if (z[0] + z[1]) % 2: + return exponent + z = divide_pi(z) + raise RuntimeError("valuation iteration bound exhausted") + + +def demand_tree(coefficients: list[Pair], n: int, q: int) -> list[int]: + require(2 <= n <= 10 and 0 < q <= 32, "tree resource bound exceeded") + require(len(coefficients) == n + 1, "coefficient count mismatch") + size = 1 << n + tree = [0] * (2 * size) + betas = [valuation(z) for z in coefficients] + for label in range(size): + beta = betas[label.bit_count()] + tree[size + label] = 0 if beta is None else max(0, q - beta) + for node in range(size - 1, 0, -1): + tree[node] = max(tree[2 * node], tree[2 * node + 1]) + return tree + + +def check_prefixes(tree: list[int], n: int, a: int, degree: int, q: int) -> dict: + """Compare every literal prefix with a separate binomial-parity oracle.""" + size = 1 << n + require(len(tree) == 2 * size, "tree size mismatch") + visited, mass, full = 0, 0, 0 + k = degree + 1 + period = 1 << k.bit_length() + for depth in range(1, n + 1): + remaining = n - depth + level_full = 0 + for bits in range(1 << depth): + weight = bits.bit_count() + expected = any((((weight + u - a) % period) & k) == k + for u in range(remaining + 1)) + actual = tree[(1 << depth) + bits] + require((actual == q) == expected, "full-precision prefix mismatch") + if depth <= n - degree - 1: + require(actual == q, "forced prefix lost full precision") + visited += 1 + level_full += actual == q + mass += (1 << remaining) * actual + weighted = sum(math.comb(depth, w) for w in range(depth + 1) + if any((((w + u - a) % period) & k) == k + for u in range(remaining + 1))) + require(level_full == weighted, "weighted full-prefix count mismatch") + full += level_full + sharp_node = (1 << (n - degree)) + (1 << a) - 1 + require(tree[sharp_node] == 0, "sharp zero-band prefix is live") + lower = size * (n - degree - 1) * q + require(mass >= lower, "gather lower bound failed") + return {"prefixes": visited, "full_prefixes": full, + "mass": mass, "lower_bound": lower} + + +def check_binomial_lemmas() -> dict: + parity_cases, difference_cases = 0, 0 + for k in range(1, 65): + period = 1 << k.bit_length() + for t in range(-128, 129): + expected = int(((t % period) & k) == k) + require(choose(t, k) % 2 == expected, "binary parity lemma failed") + parity_cases += 1 + for k in range(1, 33): + for t in range(-64, 65): + difference = sum((-1) ** (k - r) * math.comb(k, r) * choose(t + r, k) + for r in range(k + 1)) + require(difference == 1, "finite-difference no-gap lemma failed") + difference_cases += 1 + return {"binary_parity_cases": parity_cases, + "finite_difference_windows": difference_cases} + + +def check_coefficients() -> dict: + cases, negative, sharp, windows = 0, 0, 0, 0 + for n in range(2, 25): + for degree in range(1, n): + for a in range(n - degree + 1): + coefficients = [residual(n, a, degree, j) for j in range(n + 1)] + for j, z in enumerate(coefficients): + unit = (z[0] + z[1]) % 2 + require(unit == choose(j - a, degree + 1) % 2, + "first surviving Gaussian digit mismatch") + cases += 1 + negative += j < a + require(all(z == (0, 0) for z in coefficients[a:a + degree + 1]), + "sharp interpolation band is not zero") + sharp += 1 + for start in range(n - degree): + interval = coefficients[start:start + degree + 2] + require(any((z[0] + z[1]) % 2 for z in interval), + "R+2 consecutive weights contain no unit") + windows += 1 + return {"gaussian_coefficients": cases, "negative_offsets": negative, + "sharp_zero_bands": sharp, "unit_windows": windows} + + +def check_trees() -> dict: + profiles, prefixes, sharp, low_degree = 0, 0, 0, 0 + fixture = None + for n in range(2, 11): + for degree in range(1, n): + for a in range(n - degree + 1): + coefficients = [residual(n, a, degree, j) for j in range(n + 1)] + for p in (0, 1, 3): + q = p + 2 * n - degree - 1 + tree = demand_tree(coefficients, n, q) + result = check_prefixes(tree, n, a, degree, q) + profiles += 1 + prefixes += result["prefixes"] + sharp += 1 + if n >= 4 and degree <= n // 2 - 1: + require(2 * result["mass"] >= n * (1 << n) * (p + n), + "free-bulk low-degree corollary failed") + low_degree += 1 + if (n, degree, a, p) == (8, 3, 2, 3): + fixture = {"n": n, "R": degree, "a": a, "p": p, + "Q": q, **result} + require(fixture is not None, "missing positive-degree fixture") + return {"tree_profiles": profiles, "literal_prefixes": prefixes, + "sharp_cutoff_witnesses": sharp, "free_bulk_cases": low_degree, + "fixture": fixture} + + +def check_rejections() -> int: + n, degree, a, q = 6, 2, 1, 9 + tree = demand_tree([residual(n, a, degree, j) for j in range(n + 1)], n, q) + # The first eight depth-three nodes are all forced to Q by the theorem. + rejected = 0 + for node in range(8, 16): + mutant = tree.copy() + mutant[node] -= 1 + try: + check_prefixes(mutant, n, a, degree, q) + except RuntimeError as error: + require(str(error) == "full-precision prefix mismatch", + "mutant rejected for an unexpected reason") + rejected += 1 + else: + raise RuntimeError("underprecision mutant accepted") + return rejected + + +def main() -> None: + require(sys.version_info >= (3, 12), "Python 3.12 or later is required") + result = {"status": "PASS_NEWTON_RESIDUAL_PREFIX_FLOOR", + "claim_type": "scoped written proof with finite corroboration", + "lemmas": check_binomial_lemmas(), + "coefficients": check_coefficients(), + "trees": check_trees(), "rejected_underprecision_profiles": check_rejections()} + package = Path(__file__).resolve().parent + hashes = {} + for name in PACKAGE_FILES: + data = (package / name).read_bytes() + require(len(data) <= 16 * 1024 * 1024, "package file size limit exceeded") + hashes[name] = hashlib.sha256(data).hexdigest() + result["receipt"] = {"package_sha256": hashes, "python": platform.python_version(), + "implementation": platform.python_implementation(), + "optimized": bool(sys.flags.optimize)} + print(json.dumps(result, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main()