diff --git a/research/many-axis-prime-product-loss/README.md b/research/many-axis-prime-product-loss/README.md new file mode 100644 index 0000000000..e93107c8c3 --- /dev/null +++ b/research/many-axis-prime-product-loss/README.md @@ -0,0 +1,187 @@ +# Sharp product loss in the many-axis prime band + +This contribution was produced by Nick Petalas. Apache-2.0. + +Claim type: **scoped mathematical proof with finite corroboration**. +The many-axis prime band of [ToikY's #4029](https://github.com/CrocSwap/integer-mult-bounds/pull/4029) +implies the sharper full product bound + +```text +T/S < (3d/(3d-1))^(d-1) < exp(1/3) < 349/250 < 3/2. +``` + +The last `3/2` is #4029's retained sufficient bound. The new constant +`exp(1/3)` is the least uniform upper bound implied by the band inequalities +alone. Sharpness here allows rational band points; no assertion of optimality +for prime selections is made. This neither changes the prime-supply cutoff +nor improves kappa. + +## Exact domain and proof + +Use the caller's actual axis count `D=d-1`, where integer `d>=2`. For each +axis, assume positive lengths satisfying the predecessor's half-open band + +```text +1 - 1/(3d) < s_i/t_i <= 1 - 1/(4d), +S = product_i s_i, T = product_i t_i, i=1,...,D. +``` + +The conclusion is algebraic. It applies to the predecessor's prime lengths, +either of its two target scales, and every dimension for which those lengths +have been supplied. Prime abundance, distinctness, period guards, source +production and source admission are cited premises rather than new checks. +Neither a prime-number estimate nor the cutoff `ell>=2^32` enters this proof. + +Each coordinate gives `t_i/s_i < 3d/(3d-1)`. Multiplying the `d-1` strict +inequalities proves the finite-d bound `T/S < A_d`, with + +```text +A_d = (3d/(3d-1))^(d-1). +``` + +For `x>0`, integrating `1/(1+t)` on `[0,x]` gives + +```text +x/(1+x) < log(1+x) < x. +``` + +Set `x=1/(3d-1)` and multiply by `d-1`. Then + +```text +(d-1)/(3d) < log(A_d) < (d-1)/(3d-1) < 1/3. +``` + +Exponentiation proves the dimension-uniform bound. The exact rational +corollary follows from the positive Taylor series at `1/3`: sum terms +`j=0,...,10`, then bound the tail by its first term divided by `1-1/36`. +Every later ratio is at most `1/36`. The resulting rational upper bound is +strictly below `349/250`, as the checker verifies by integer arithmetic. + +For fixed `d`, put every `s_i/t_i` arbitrarily close to the open lower +endpoint from above. This proves that `A_d` is the exact supremum under +the band assumptions. The displayed logarithmic squeeze also gives +`A_d -> exp(1/3)` as `d -> infinity`. + +For completeness, one explicit admissible rational sequence realizes the +uniform sharpness without using the excluded endpoint: + +```text +q_d = 1 - 1/(3d) + 1/(12d^2), +s_i/t_i = q_d for every one of the d-1 axes. +``` + +Its added term lies strictly between zero and the band width `1/(12d)`. +Writing `u_d=1-q_d`, integration gives +`u_d < -log(1-u_d) < u_d/(1-u_d)`. Consequently + +```text +1/3 - 5/(12d) < (d-1)*(-log(q_d)) < log(A_d) < 1/3. +``` + +Thus `q_d^(-(d-1)) -> exp(1/3)`. Every smaller proposed uniform constant +fails for some rational band tuple. The targets `t_i` may remain powers of +two in this sharpness example, since multiplication by `q_d` supplies +rational `s_i`; integer or prime `s_i` are a stronger, unproved restriction. +The elementary logarithmic inequalities are standard. The contribution is +their exact application to this caller's product-loss envelope. + +## Verification and reproduction + +The universal quantifiers follow from the proof above. The standalone +standard-library checker corroborates the new envelope using complete small +rational boxes, rational logarithm intervals, endpoint approaches, an explicit +sharpness sequence and domain controls. It imports no predecessor executable +and replays no predecessor prime or source-admission certificate. + +From the repository root, using CPython 3.12: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/many-axis-prime-product-loss/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/many-axis-prime-product-loss/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/many-axis-prime-product-loss +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/many-axis-prime-product-loss --check-source-history +``` + +Substitute another CPython 3.12 path as needed. The marker is +`PASS_MANY_AXIS_PRIME_PRODUCT_LOSS`. Stdout is a generated receipt bound to +the SHA256 of all five package files. Default replay is read-only and needs +no Git, network or external input files. Metadata validation separately +checks the historical provenance in [SOURCES.json](SOURCES.json). + +Local CPython 3.12.15 on macOS arm64 passes both registered modes. The +checker enumerates 1,364 rational boxes, 511 finite-d logarithmic envelopes, +504 endpoint approaches and sixteen sharpness-limit probes. All nine invalid +input fixtures reject, and both stated boundary counterexamples pass. +Syntax/function-size inspection and development-mode warnings also pass. + +The controls reject the open lower endpoint, out-of-band or nonpositive +lengths and an incorrect axis count. They accept the closed upper endpoint. +Using `D=d` is demonstrably unsafe: with `d=2`, the distinct prime lengths +107 and 109 both lie in the target-128 band, but +`128^2/(107*109) > 349/250 > exp(1/3)`. +The explicit sharpness sequence at `d=128` also exceeds `139/100`, rejecting +that smaller candidate constant. Runtime domain caps belong only to the +finite checker, not to the theorem. + +## Limits + +This is an elementary product estimate conditional on the displayed band. +It does not establish prime supply, improve its cutoff, execute an encoded +prime producer, lower physical costs or prove a complete multiplication +theorem. Native operations, source/target and period contracts, routing, +restoration, numerical recovery, stock, precision and tape costs remain +separate obligations. No selected cold replay, Lean or Docker was run. +Independent human and formal proof-kernel review are unclaimed. + +## Open next questions + +The structured versions are in [TASK.json](TASK.json). + +1. Is the same supremum attained asymptotically by distinct primes within the + retained two-scale domain? This would distinguish band-only sharpness from + prime-restricted sharpness. Start with a narrowing band immediately above + its lower endpoint and an explicit interval prime count; uniform abundance + in that narrower band is not supplied here. +2. Can a fully charged prime-selection policy achieve a smaller product loss + by selecting near the upper endpoint? Start with an actual caller's gap, + period and queue contracts before narrowing its selection interval. + Prime availability and the complete producer bill remain blockers. + +## Provenance and credit + +Base `a5df48c55ea806d7952b65acc9c76d878ff09b13`, priority revision 7. +The `uniform-transfer-audit` card is explicitly changed to this algebraic +side result in [TASK.json](TASK.json). The card's historical baseline command +raises `KeyError: 'bit_lower'` on the current selected certificate schema; +it is unchanged and is not evidence about this product estimate. +[Advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19144301). + +Credit ToikY #4029 for the band, actual `D=d-1` reading, source construction +and prior `3/2` bound; unpaidmoon #4142 for the encoded-guard scope; Jose +Manuel #3935 for the tensor interface; and Tekalign #4024 for the CRT source +premise. Cinna Davis, Chafik Boukhalfa, Josie Elliston, the retained source08 +authors and Harvey and van der Hoeven retain prime-selector credit. +Fiori, Kadiri and Swidinsky supply the analytic theorem used by the predecessor, +which is not used or reproved by this algebraic consequence. Frozen sources +and predecessor credit lines are unchanged. + +Overlap checks covered live open PRs, recent handoffs and active Discussions, +recent account work, main-tree README formulas and merged/all-state searches. +The sparse local notes and unpublished work are limits. The concurrent +prime-supply cutoff result in +[#5149](https://github.com/CrocSwap/integer-mult-bounds/pull/5149) concerns a +different quantity and is not extended. It lowers the sufficient prime-supply +cutoff and retains the old product bound; this result sharpens the product +bound without deriving a prime-supply cutoff. No numerical cross-check of +that contribution was run. + +Power of Ten inspection covers the one new code file. It has no recursion, +subprocesses, writes or runtime code generation; functions are under 60 lines. +All finite loops are bounded by `d<=512`, four choices on at most five axes, +eight endpoint steps, sixteen limit probes or twelve series terms. File reads +are capped at 256 KiB. Explicit exceptions preserve checks under `-O`. +Rule 3 has a managed-runtime deviation: CPython allocates integers and +containers. These fixed domains bound live algorithmic collections; runtime +allocation internals are not instrumented. A fixed-storage native rewrite is +required before allocation-prohibited use. Warning-strict normal and optimized +replays are the local diagnostics; no static type checker is configured here. diff --git a/research/many-axis-prime-product-loss/SOURCES.json b/research/many-axis-prime-product-loss/SOURCES.json new file mode 100644 index 0000000000..49848e18fe --- /dev/null +++ b/research/many-axis-prime-product-loss/SOURCES.json @@ -0,0 +1,36 @@ +{ + "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/many-axis-encoded-axis-guard/README.md", + "usage": "provenance", + "git_blob": "1907b4f1815f056a9bad313ba316df3c6aa4a03e", + "sha256": "3d51a8dd86db6b95d8387b16f86d6ad3627a415583eea23dedd82ffc65bc57af" + }, + { + "path": "research/many-axis-prime-supply/PROOF.md", + "usage": "provenance", + "git_blob": "1046c7493cf101e8cf1a43a7226a6d143e5190d1", + "sha256": "339213c572e0b1dae7028c16b371c0bdebc19e5ee5146ff9dd1e4c4570fa67e1" + }, + { + "path": "research/many-axis-prime-supply/README.md", + "usage": "provenance", + "git_blob": "f3f736734a0d209a5fb383494b2253cc8f7702e4", + "sha256": "68ba22bcf761370c9370f770ed65de0de699feccb89c9011e470e00542ae72e9" + } + ] +} diff --git a/research/many-axis-prime-product-loss/TASK.json b/research/many-axis-prime-product-loss/TASK.json new file mode 100644 index 0000000000..bf6b23e946 --- /dev/null +++ b/research/many-axis-prime-product-loss/TASK.json @@ -0,0 +1,85 @@ +{ + "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": "Sharp finite-d and dimension-uniform product-loss envelopes implied by the existing many-axis prime band.", + "scope_change_reason": "Original successor arithmetic rather than an audit: improve the retained 3/2 product bound to exp(1/3), sharp under band assumptions alone. Prime supply and caller/source checks are cited premises.", + "bottleneck_link": "A sharper source/target product ratio is a local quantitative improvement to a retained tensor interface. It does not itself remove any physical caller or selected-supplier assumption.", + "budget_minutes": 60, + "stop_rule": "Stop after the first proved product-envelope improvement; do not extend into prime-supply cutoff or producer implementation.", + "outcome": "completed", + "evidence": "Written dimension-uniform proof in README.md; standalone exact rational boxes, series bounds, endpoint and sharpness probes, and meaningful domain/counterexample controls in verify.py.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Is exp(1/3) also the supremum for distinct prime lengths in the retained two-scale domain?", + "why_it_matters": "The sharpness proof here admits rational points; prime-only selections add arithmetic restrictions.", + "first_step": "Prove abundance in a narrowing interval immediately above the existing lower band endpoint.", + "blocked_by": "A uniform explicit prime count for the narrower interval has not been derived." + }, + { + "question": "Can a fully charged selection policy near the upper band endpoint reduce the guaranteed product loss?", + "why_it_matters": "The band-only worst-case envelope does not optimize prime selection or physical setup.", + "first_step": "Pin one actual caller and its gap, period and prime-queue contracts before changing the selection interval.", + "blocked_by": "Prime availability in the chosen interval and its complete producer cost are not supplied." + } + ], + "coordination": { + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19144301", + "overlap_scope": "Live open PRs, recent handoff/active Discussion posts, recent own-account work, main README distinctive terms and merged/all-state searches; sparse local notes and unpublished work are incomplete.", + "separate_claim": "A concurrent many-axis prime-supply cutoff claim is a separate question; this package does not lower its cutoff." + } +} diff --git a/research/many-axis-prime-product-loss/VERIFY.json b/research/many-axis-prime-product-loss/VERIFY.json new file mode 100644 index 0000000000..1b9564242b --- /dev/null +++ b/research/many-axis-prime-product-loss/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": 120, + "checks": "Exact new product envelope, rational series bounds, complete small boxes, endpoint and limit probes; incorrect-domain and smaller-constant controls." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact new product envelope, rational series bounds, complete small boxes, endpoint and limit probes; incorrect-domain and smaller-constant controls." + } + ] +} diff --git a/research/many-axis-prime-product-loss/verify.py b/research/many-axis-prime-product-loss/verify.py new file mode 100644 index 0000000000..e82aea8fdf --- /dev/null +++ b/research/many-axis-prime-product-loss/verify.py @@ -0,0 +1,172 @@ +#!/usr/bin/env python3 +"""Exact finite corroboration of the prime-band product envelope. + +Produced by Nick Petalas. Apache-2.0. +The dimension-uniform argument is in README.md. No prime theorem is replayed. +""" + +from fractions import Fraction +from hashlib import sha256 +from itertools import product +import json +from math import prod +from pathlib import Path + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def dimension(d): + require(type(d) is int and 2 <= d <= 512, "finite checker requires 2<=d<=512") + + +def envelope(d): + dimension(d) + return Fraction(3 * d, 3 * d - 1) ** (d - 1) + + +def product_ratio(d, coordinates): + dimension(d) + require(len(coordinates) == d - 1, "the caller has exactly D=d-1 axes") + low, high = 1 - Fraction(1, 3 * d), 1 - Fraction(1, 4 * d) + for s, t in coordinates: + require(s > 0 and t > 0, "lengths must be positive") + require(low < s / t <= high, "point outside the half-open prime band") + return prod((t / s for s, t in coordinates), start=Fraction(1)) + + +def log_interval(x): + """Integrate the positive geometric series, with an exact tail bound.""" + require(Fraction(1) <= x <= Fraction(6, 5), "log probe outside bounded range") + z = (x - 1) / (x + 1) + lower = 2 * sum((z ** (2 * j + 1) / (2 * j + 1) for j in range(12)), + start=Fraction(0)) + tail = 2 * z**25 / (25 * (1 - z * z)) + return lower, lower + tail + + +def exp_third_interval(): + term, lower = Fraction(1), Fraction(1) + for j in range(1, 11): + term /= 3 * j + lower += term + first_omitted = term / 33 + upper = lower + first_omitted / (1 - Fraction(1, 36)) + require(lower < upper < Fraction(349, 250) < Fraction(3, 2), + "rational corollary failed") + return lower, upper + + +def check_boxes(): + count = 0 + for d in range(2, 7): + low = 1 - Fraction(1, 3 * d) + width = Fraction(1, 12 * d) + for digits in product(range(1, 5), repeat=d - 1): + coordinates = [] + log_upper = Fraction(0) + for i, digit in enumerate(digits): + t = Fraction(2 ** (3 + i % 2)) + s = t * (low + width * digit / 4) + coordinates.append((s, t)) + log_upper += log_interval(t / s)[1] + require(product_ratio(d, coordinates) < envelope(d), "box envelope failed") + require(log_upper < Fraction(1, 3), "box logarithm bound failed") + count += 1 + return count + + +def check_envelopes(): + for d in range(2, 513): + lower, upper = log_interval(Fraction(3 * d, 3 * d - 1)) + require(Fraction(d - 1, 3 * d) < (d - 1) * lower, + "lower integral bound failed") + require((d - 1) * upper < Fraction(d - 1, 3 * d - 1) < Fraction(1, 3), + "upper integral bound failed") + return 511 + + +def check_sharpness(): + finite = 0 + for d in range(2, 65): + low, width = 1 - Fraction(1, 3 * d), Fraction(1, 12 * d) + previous = Fraction(0) + for j in range(1, 9): + q = low + width / 2**j + ratio = product_ratio(d, [(q, Fraction(1))] * (d - 1)) + require(previous < ratio < envelope(d), "endpoint approach failed") + previous = ratio + finite += 1 + for j in range(1, 17): + d = 2**j + q = 1 - Fraction(1, 3 * d) + Fraction(1, 12 * d * d) + lower, upper = log_interval(1 / q) + require(Fraction(1, 3) - Fraction(5, 12 * d) < (d - 1) * lower, + "sharpness lower squeeze failed") + require((d - 1) * upper < Fraction(1, 3), "sharpness upper squeeze failed") + return finite, 16 + + +def check_controls(exp_upper): + valid = [(Fraction(7, 8), Fraction(1))] + require(product_ratio(2, valid) == Fraction(8, 7), "closed upper endpoint rejected") + invalid = [ + (1, valid), (True, valid), (513, valid), (2, []), (2, valid * 2), + (2, [(Fraction(5, 6), Fraction(1))]), + (2, [(Fraction(9, 10), Fraction(1))]), + (2, [(Fraction(-1), Fraction(1))]), + (2, [(Fraction(1), Fraction(0))]), + ] + rejected = 0 + for d, coordinates in invalid: + try: + product_ratio(d, coordinates) + except ValueError: + rejected += 1 + else: + raise ValueError("invalid fixture accepted") + # Distinct band primes, but the false D=d contract invalidates the bound. + for prime in (107, 109): + require(Fraction(5, 6) < Fraction(prime, 128) <= Fraction(7, 8), + "bad control band") + require(Fraction(128**2, 107 * 109) > exp_upper, "wrong axis count went undetected") + d = 128 + q = 1 - Fraction(1, 3 * d) + Fraction(1, 12 * d * d) + require(q ** (1 - d) > Fraction(139, 100), "smaller constant control failed") + return rejected, 2 + + +def file_hashes(): + root = Path(__file__).resolve().parent + names = ("README.md", "SOURCES.json", "TASK.json", "VERIFY.json", "verify.py") + hashes = {} + for name in names: + with (root / name).open("rb") as source: + data = source.read(262145) + require(len(data) <= 262144, "package file exceeds fixed read bound") + hashes[name] = sha256(data).hexdigest() + return hashes + + +def main(): + exp_lower, exp_upper = exp_third_interval() + boxes = check_boxes() + dimensions = check_envelopes() + approaches, limits = check_sharpness() + rejected, counterexamples = check_controls(exp_upper) + receipt = { + "marker": "PASS_MANY_AXIS_PRIME_PRODUCT_LOSS", + "rational_boxes": boxes, "envelope_dimensions": dimensions, + "endpoint_approaches": approaches, "limit_probes": limits, + "rejected_inputs": rejected, "boundary_counterexamples": counterexamples, + "exp_third_interval": [str(exp_lower), str(exp_upper)], + "package_sha256": file_hashes(), + "claim_type": "scoped proof with finite corroboration", "no_new_kappa": True, + } + print(json.dumps(receipt, sort_keys=True)) + + +if __name__ == "__main__": + main()