Sharpen the many-axis prime product bound to exp(1/3) (no κ)

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.

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"
+    }
+  ]
+}

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."
+  }
+}

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."
+    }
+  ]
+}