Prove sharp all-precision Neumann truncation at 226p² (no new κ)

research/optimal-neumann-quadratic-tail/README.md

@@ -0,0 +1,145 @@
+# The sharp all-precision quadratic Neumann truncation is 226 p²
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+**Claim type: scoped proof with exact finite corroboration. No new κ.**
+
+For every integer `p >= 1`, set `g = 1/(16p)` and `J = 226p²`. Then
+
+```text
+2(1-g)^J/g = 32p (1-1/(16p))^(226p²) < 2^(-16p).
+```
+
+Moreover, **226 is the smallest nonnegative integer coefficient** that works
+in `J = c p²` simultaneously for every positive integer precision. The
+coefficient 225 fails at `p = 1`.
+
+Jose Manuel's [PR #3851](https://github.com/CrocSwap/integer-mult-bounds/pull/3851)
+uses `J = 512p²` in the normalized Gaussian core. Its proof bounds the
+difference between the global inverse and a principal-window inverse by
+the scalar tail above and imposes margins larger than `Jw`.
+James Reed's [PR #3864](https://github.com/CrocSwap/integer-mult-bounds/pull/3864)
+checks the 512 coefficient for precisions 101 through 200 and at precision 1.
+Those source results are cited, not replayed as this contribution. The new
+step is the smaller truncation prescription, its all-precision proof and its
+exact optimality within this integer quadratic family.
+
+## Proof
+
+At `p = 1`, the two exact integer comparisons are
+
+```text
+2^21 * 15^226 < 16^226,
+2^21 * 15^225 > 16^225.
+```
+
+Thus 226 succeeds and 225 fails. The tail decreases strictly with the
+coefficient, so every nonnegative integer coefficient below 226 also fails
+at precision 1. This proves the required lower bound without a search over
+coefficients.
+
+For the uniform upper bound at `p >= 2`, put `n = 16p`. The first four
+terms in the binomial expansion give
+
+```text
+(1 - 1/n)^(-n) = (1 + 1/(n-1))^n
+  >= 1 + n/(n-1) + n/(2(n-1)) + n(n-2)/(6(n-1)^2)
+   = 8/3 + (9n-10)/(6(n-1)^2)
+   > 8/3.
+```
+
+This uses only the integer binomial theorem and positivity, since `n >= 32`.
+Consequently `(1-1/(16p))^(16p) < 3/8`. As `226p² >= 224p²`,
+
+```text
+32p (1-1/(16p))^(226p²) * 2^(16p)
+  < 32p [(3/8)^14 * 2^16]^p
+   = 32p (3^14/2^26)^p
+   < 32p / 8^p
+  <= 1.
+```
+
+The second strict inequality is the integer comparison `3^14 < 2^23`.
+The final inequality follows by induction. At `p = 2`, `32p = 8^p = 64`.
+For each `p >= 2`, the ratio of consecutive values of `32p/8^p` is
+`(p+1)/(8p) <= 3/16 < 1`. Together with the precision-1 comparison, this
+proves the upper bound for every positive integer precision.
+
+The uniform quantifier comes from this argument. The sixteen direct
+comparisons in the verifier are finite corroboration, not its proof.
+
+## Consequence and limits
+
+Whenever the inherited caller supplies the same contraction `g = 1/(16p)`
+and the same prefactor `2/g`, 226p² terms suffice for its stated tail budget.
+In the locality argument, a bandwidth-w path of length below J stays inside
+the retained window under a margin larger than Jw. This scalar result permits
+that argument to use `226p²w` in place of `512p²w`, subject to all its other
+hypotheses. No caller code or production-domain predicate is changed here.
+
+The result does not establish the contraction, the inverse-norm hypotheses,
+rounded arithmetic error, physical evaluation cost, complete outer tensor or
+integer recovery. The production core starts at `p >= 101`, so the global
+optimality witness at `p = 1` does not establish optimality restricted to its
+production domain. A nonquadratic prescription may be smaller. No independent
+human or formal proof-kernel review, complete multiplication theorem or
+selected-frontier change is claimed.
+
+## Reproduce
+
+From the repository root, using Python 3.12 and the standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/optimal-neumann-quadratic-tail/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/optimal-neumann-quadratic-tail/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/optimal-neumann-quadratic-tail
+```
+
+Expected output includes
+`PASS_OPTIMAL_NEUMANN_QUADRATIC_TAIL coefficient=226 excluded=225 direct_precisions=16 domain_controls=4 no_new_kappa`.
+The verifier checks both precision-1 integers, the polynomial identity in
+the binomial proof, the induction constants, and the full tail at each
+precision 1 through 16 by both integer and rational arithmetic. It rejects
+four out-of-domain calibration calls and confirms that coefficient 225 fails.
+Checks use explicit exceptions and remain enabled under optimized Python.
+
+Normal replay writes nothing. `verify.py --receipt /absolute/new/path.json`
+creates a receipt with the result, interpreter version and SHA256 hashes of
+all five package files. It refuses an occupied output. Receipts and logs
+belong outside the checkout. No hand-written receipt is supplied.
+
+All [source pins](SOURCES.json) are historical provenance. The new proof and
+verifier import no predecessor executable and have no external live inputs.
+The [task record](TASK.json) records the scope change from proof audit to an
+original truncation improvement, overlap coverage and local validation.
+
+## Open next questions
+
+1. What is the least quadratic integer coefficient when only `p >= 101`
+   is required? The precision-1 obstruction disappears. First prove a
+   monotonicity bound for the normalized logarithmic tail on that domain,
+   then check its actual integer boundary. This is separate from the
+   all-positive-precision optimum proved here.
+2. Can the production caller use the smaller window margins while preserving
+   every setup, rounding, routing and ownership obligation? First trace each
+   occurrence of J in the exact PR3851 caller and retain its full error sum.
+   The present scalar theorem does not supply that integration.
+
+## Predecessor credit and coordination
+
+Jose Manuel, `jmbarrancoml`, supplies the physical Gaussian core, the global
+and principal inverse comparison, the `1/(16p)` contraction and the original
+512p² prescription. His retained Chafik Boukhalfa, RaD project, Mason Hale,
+Dugongue and upstream FFT/Gaussian lineage keeps its credit in the unchanged
+source. James Reed, `jwr404`, supplies the finite-range tail package.
+Classical binomial and geometric-series inequalities are used here; no claim
+of priority for those general methods is made.
+
+The canonical [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19144249)
+states the same scalar question. Base main is
+`a5df48c55ea806d7952b65acc9c76d878ff09b13`, priority revision 7.
+Live PR and Discussion searches, merged-PR searches and tracked README
+searches found no same-question result at the claim checkpoint. Sparse
+working-note cache coverage is incomplete; the direct Git search covers
+tracked README files. Unpublished work and arbitrary code diffs are outside
+these overlap checks.

research/optimal-neumann-quadratic-tail/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "a5df48c55ea806d7952b65acc9c76d878ff09b13",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395",
+      "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602",
+      "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72"
+    },
+    {
+      "path": "research/neumann-tail-bound/README.md",
+      "usage": "provenance",
+      "git_blob": "c2b1bd90e0f6f029d71594ec95786ad5566adae3",
+      "sha256": "785d290e2255cf7203d1cc9b09b2adeca96318adaed6606f880598acbee40a44"
+    },
+    {
+      "path": "research/physical-gaussian-core/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "883c8d4a6f0eead888fb3532b60db41596940889",
+      "sha256": "e909026dd3f455c35ff28210a0c4ffa232ad8d7633174e481094fd09e2469d7a"
+    }
+  ]
+}

research/optimal-neumann-quadratic-tail/TASK.json

@@ -0,0 +1,117 @@
+{
+  "schema_version": 1,
+  "task_id": "uniform-transfer-audit",
+  "priority_revision": 7,
+  "base_commit": "a5df48c55ea806d7952b65acc9c76d878ff09b13",
+  "original_card": {
+    "id": "uniform-transfer-audit",
+    "question": "Does one quantified step of the proposed #4100 all-size construction hold at its actual caller?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "research/unconditional-batched-crt/README.md"
+    ],
+    "methods": [
+      "Prove one missing implication with explicit quantified hypotheses.",
+      "Find an exact counterexample at the claimed interface boundary."
+    ],
+    "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read PROOF.md and AUDIT.md in #4100. Select one distinct obligation: CRT total repair, native/free-algebra lifting, precision/conditioning, or complete fixed-tape cost. This is an author-submitted proof, not an accepted unconditional theorem.",
+      "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately."
+    },
+    "first_experiment": "Check live handoffs; name one proposition, its caller, quantified domain and dependency closure. Independently prove the implication or exhibit a precise gap/counterexample. Prioritize CRT.md total repair or COMPLEX.md free-algebra lift only if unclaimed. Stop at the chosen obligation; do not substitute finite samples or root arithmetic for an all-size proof, or launch the complete package by default.",
+    "bottleneck_link": "Finite supplier improvements are useful only under the retained transfer obligations.",
+    "allowed_variations": [
+      "One CRT repair, native lift, precision/conditioning or tape-cost proposition, with its exact caller."
+    ],
+    "scope_change_triggers": [
+      "Replacing a quantified obligation with another finite smoke test.",
+      "Treating archive intake, an author PASS receipt or a finite composed fixture as discharge of the universal hypotheses."
+    ],
+    "overlap_terms": [
+      "uniform transfer",
+      "all-size",
+      "precision",
+      "4100",
+      "unconditional-batched-crt"
+    ],
+    "existing_checks": [
+      {
+        "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.",
+        "evidence": "research/unconditional-batched-crt/README.md",
+        "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.",
+        "status": "author-checked",
+        "source_commit": "337d04939571a637aeab54a0f58f54fde811663a",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      }
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Prove the smallest nonnegative integer coefficient c in J=c p^2 that makes 32p(1-1/(16p))^J < 2^(-16p) for every integer p>=1.",
+  "scope_change_reason": "The assignment asks for original research, not verification of a predecessor. Replace the generic all-size proof audit with a new sharp scalar truncation improvement for PR3851, citing PR3864 rather than replaying it.",
+  "bottleneck_link": "The same scalar locality-error budget permits a smaller truncation and corresponding sufficient path margin, conditional on the inherited contraction and caller hypotheses. This is a local precision result, not supplier admission.",
+  "budget_minutes": 60,
+  "stop_rule": "Ship the first proved truncation improvement with exact optimality in its stated family. Do not extend to production-domain optimization or integrate the physical caller.",
+  "outcome": "completed",
+  "evidence": "README.md proves all-positive-precision sufficiency of coefficient 226 and excludes every smaller integer using precision 1. verify.py checks exact proof constants, sixteen full-tail cases in two arithmetic representations and four domain rejections.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "What is the least integer quadratic coefficient when only p>=101 is required?",
+      "why_it_matters": "The production domain omits the precision-1 obstruction that determines the all-positive-precision optimum.",
+      "first_step": "Prove monotonicity of the normalized logarithmic tail on the production domain, then determine its integer boundary.",
+      "blocked_by": "No production-domain optimization is included."
+    },
+    {
+      "question": "Can the exact PR3851 caller use the smaller J and window margins while preserving its complete error and ownership contracts?",
+      "why_it_matters": "A scalar tail improvement does not automatically change an executable Gaussian core.",
+      "first_step": "Trace every occurrence of J in the exact production caller and retain its full setup, rounding and locality error ledger.",
+      "blocked_by": "Caller integration and physical replay are outside this contribution."
+    }
+  ],
+  "upstream_checkpoint": {
+    "commit": "a5df48c55ea806d7952b65acc9c76d878ff09b13",
+    "priority_revision": 7,
+    "checked_at_utc": "2026-10-23T10:51:08Z"
+  },
+  "coordination": {
+    "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19144249",
+    "reservation": "uniform-transfer-audit-optimal-quadratic-neumann-tail",
+    "overlap": "Live open PRs and recent handoffs, all 117 same-account PRs created in the previous 24 hours, complete cached open-PR/Discussion pagination, merged-PR keyword searches and direct tracked README searches. Sparse cached local coverage and unpublished work remain incomplete.",
+    "predecessors": [
+      3851,
+      3864
+    ]
+  },
+  "engineering": {
+    "playbook": "Autonomous local run",
+    "principles": [
+      "Build the Lever: retain a bounded standalone exact verifier.",
+      "Prove It Works: run the actual package, direct and optimized commands, then committed-byte/history preflight."
+    ],
+    "power_of_ten": "No recursion; fixed loops of 16, 4 and 5 iterations; every function below 60 lines; explicit exceptions remain active under -O. Managed Python allocation is a documented deviation: calibration precision <=16, coefficient <=512, at most 131072 exponent, integer operands under 2 Mi bits; each source file <=1 MiB. No external runtime dependencies or dynamic code evaluation."
+  },
+  "validation": {
+    "python": "3.12.15",
+    "platform": "macOS-27.0.1-arm64-arm-64bit",
+    "direct_normal_seconds": 0.08,
+    "direct_optimized_seconds": 0.09,
+    "registered_package_seconds": 0.41,
+    "status": "normal, optimized, registered metadata and both manifest commands passed locally",
+    "unrun": [
+      "Gaussian caller integration and physical replay",
+      "upstream native/all-column replay",
+      "complete outer tensor and exact recovery",
+      "Lean and Docker",
+      "hosted CI pending"
+    ]
+  }
+}

research/optimal-neumann-quadratic-tail/VERIFY.json

@@ -0,0 +1,34 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "Exact integer endpoint, polynomial binomial identity, uniform induction constants, sixteen direct comparisons and rejection controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "Repeat all checks with optimized Python; no proof check relies on assertions."
+    }
+  ]
+}