diff --git a/research/optimal-neumann-quadratic-tail/README.md b/research/optimal-neumann-quadratic-tail/README.md new file mode 100644 index 0000000000..30c52b2af4 --- /dev/null +++ b/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. diff --git a/research/optimal-neumann-quadratic-tail/SOURCES.json b/research/optimal-neumann-quadratic-tail/SOURCES.json new file mode 100644 index 0000000000..9a11983282 --- /dev/null +++ b/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" + } + ] +} diff --git a/research/optimal-neumann-quadratic-tail/TASK.json b/research/optimal-neumann-quadratic-tail/TASK.json new file mode 100644 index 0000000000..93f16de2a6 --- /dev/null +++ b/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" + ] + } +} diff --git a/research/optimal-neumann-quadratic-tail/VERIFY.json b/research/optimal-neumann-quadratic-tail/VERIFY.json new file mode 100644 index 0000000000..d249d9038d --- /dev/null +++ b/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." + } + ] +} diff --git a/research/optimal-neumann-quadratic-tail/verify.py b/research/optimal-neumann-quadratic-tail/verify.py new file mode 100644 index 0000000000..e177ce0c1c --- /dev/null +++ b/research/optimal-neumann-quadratic-tail/verify.py @@ -0,0 +1,124 @@ +"""Exact arithmetic accompanying the all-precision Neumann tail proof. + +The uniform quantifier is proved in README.md. The finite comparisons below +check its boundary constants, polynomial identity and direct calibration cases. +Normal replay is read-only; --receipt creates a new hash-bound JSON file. +""" + +from __future__ import annotations + +import argparse +from fractions import Fraction +import hashlib +import json +from pathlib import Path +import platform + + +PACKAGE = Path(__file__).resolve().parent +FILES = ("README.md", "SOURCES.json", "TASK.json", "VERIFY.json", "verify.py") +MAX_PRECISION = 16 +MAX_COEFFICIENT = 512 + + +def require(condition: bool, message: str) -> None: + if not condition: + raise ValueError(message) + + +def tail_below_grid(precision: int, coefficient: int) -> bool: + """Compare the full scalar tail with one grid unit, using integers.""" + require(1 <= precision <= MAX_PRECISION, "precision outside calibration") + require(1 <= coefficient <= MAX_COEFFICIENT, "coefficient outside calibration") + modulus = 16 * precision + length = coefficient * precision * precision + left = 32 * precision * (modulus - 1) ** length * 2 ** (16 * precision) + right = modulus ** length + return left < right + + +def proof_constants() -> dict[str, object]: + # Coefficients are ordered by ascending powers of n. Multiplying the + # four-term binomial sum by 6(n-1)^2 gives the left polynomial. + binomial_numerator = ( + 6, + -12 - 6 - 3 - 2, + 6 + 6 + 3 + 1, + ) + claimed_numerator = (16 - 10, -32 + 9, 16) + require(binomial_numerator == claimed_numerator, "binomial identity") + require(9 * 16 - 10 > 0, "positive binomial surplus at n=16") + require(9 > 0, "binomial surplus increases with n") + require(3**14 < 2**23, "rho must be strictly less than 1/8") + require(32 * 2 == 8**2, "geometric induction base") + require(Fraction(3, 2) < 8, "geometric induction step for p>=2") + require(226 >= 224 == 14 * 16, "discarded positive truncation power") + require(2**21 * 15**226 < 16**226, "226 must pass at p=1") + require(2**21 * 15**225 > 16**225, "225 must fail at p=1") + return { + "minimum_integer_coefficient": 226, + "excluded_coefficient": 225, + "excluding_precision": 1, + "binomial_numerator_ascending": list(binomial_numerator), + "rho": str(Fraction(3**14, 2**26)), + "rho_upper_bound": "1/8", + "uniform_claim": "32p(1-1/(16p))^(226p^2) < 2^(-16p), p>=1", + } + + +def calibrate() -> dict[str, object]: + """Compare two arithmetic representations on precisely sixteen cases.""" + checked = [] + for precision in range(1, MAX_PRECISION + 1): + modulus = 16 * precision + length = 226 * precision * precision + rational_tail = 32 * precision * Fraction(modulus - 1, modulus) ** length + rational_result = rational_tail < Fraction(1, 2 ** (16 * precision)) + integer_result = tail_below_grid(precision, 226) + require(integer_result and rational_result, "direct tail comparison") + checked.append(precision) + require(not tail_below_grid(1, 225), "undersized coefficient control") + rejected = 0 + for precision, coefficient in ((0, 226), (17, 226), (1, 0), (1, 513)): + try: + tail_below_grid(precision, coefficient) + except ValueError: + rejected += 1 + require(rejected == 4, "calibration domain rejection controls") + return {"direct_precisions": checked, "rejected_domain_cases": rejected} + + +def source_hashes() -> dict[str, str]: + hashes = {} + for name in FILES: + path = PACKAGE / name + require(path.is_file() and not path.is_symlink(), "regular package file") + require(path.stat().st_size <= 1024 * 1024, "package file capacity") + hashes[name] = hashlib.sha256(path.read_bytes()).hexdigest() + return hashes + + +def main() -> None: + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--receipt", type=Path, help="create a new JSON receipt") + arguments = parser.parse_args() + result = { + "status": "PASS_OPTIMAL_NEUMANN_QUADRATIC_TAIL", + "claim_type": "scoped proof with exact finite corroboration", + "proof_constants": proof_constants(), + "calibration": calibrate(), + "sha256": source_hashes(), + "python": platform.python_version(), + "no_new_kappa": True, + } + if arguments.receipt is not None: + payload = json.dumps(result, indent=2, sort_keys=True) + "\n" + with arguments.receipt.open("x", encoding="utf-8") as handle: + written = handle.write(payload) + require(written == len(payload), "incomplete receipt write") + print("PASS_OPTIMAL_NEUMANN_QUADRATIC_TAIL coefficient=226 excluded=225 " + "direct_precisions=16 domain_controls=4 no_new_kappa") + + +if __name__ == "__main__": + main()