Prove a shifted one-step threshold including sharp m=7 (no κ)

research/shifted-persistence-threshold/PROOF.md

@@ -0,0 +1,166 @@
+# A shifted sufficient threshold for the one-step comparison
+
+This scoped proof was produced by Nick Petalas. Apache-2.0.
+
+## Statement
+
+Let `d0,a,b` be positive integers, and put `D=d0*b`. Define
+
+```text
+T(a,D) = 1                                    if a>D,
+         max(2, ceil((3D-a)/(2a)))             if a<=D.
+```
+
+For every integer `m>=T(a,D)`,
+
+```text
+(m+1)^D < 2^a m^D.                                      (1)
+```
+
+Moreover, `T(a,D)<=ceil(27D/(17a))` for every positive integer `a,D`.
+At `(d0,a,b)=(1,1,5)` the new sufficient threshold is the exact minimum
+`7`, whereas the cited #7450 sufficient threshold is `8`. At `(1,2,5)`
+both sufficient thresholds are the exact minimum `4`.
+
+This is a new application of a classical elementary analytic inequality.
+No novelty is claimed for that inequality or for logarithmic differentiation.
+The general sufficient threshold is not claimed to be an exact minimum.
+
+## The shifted power inequality
+
+For real `x>0`, put `F(x)=(2x+1) log(1+1/x)`, using natural logarithms.
+Differentiation gives
+
+```text
+F'(x) = 2 log(1+1/x) - (2x+1)/(x(x+1)).
+```
+
+The function `t -> 1/t` is strictly convex on the positive real axis.
+On `[x,x+1]` its graph is strictly below the secant except at the endpoints.
+Integration therefore gives
+
+```text
+log(1+1/x) = integral_x^(x+1) dt/t
+          < (1/2)(1/x + 1/(x+1)).
+```
+
+Consequently `F'(x)<0`. Since `F(1)=3 log 2`, every real `x>1` satisfies
+`F(x)<3 log 2`. Exponentiating, for every integer `m>=2`,
+
+```text
+((m+1)/m)^(2m+1) < 8.                                  (2)
+```
+
+At `m=1` there is equality, not strict inequality. This endpoint is why
+the definition of `T` separates `a>D` and requires `m>=2` otherwise.
+
+## Deriving the threshold
+
+Suppose `m>=2` and `a(2m+1)>=3D`. Raise (2) to the positive integer power
+`D` and use that exponent inequality:
+
+```text
+((m+1)/m)^(D(2m+1)) < 2^(3D) <= 2^(a(2m+1)).
+```
+
+Taking a positive `(2m+1)`-st root proves (1). Its hypothesis holds when
+`m>=ceil((3D-a)/(2a))`. Thus the stated `T` works when `a<=D`.
+
+If `a>D`, then for every integer `m>=1`, `(m+1)/m<=2`, so
+`((m+1)/m)^D<=2^D<2^a`. Therefore `T=1` works in this case.
+
+All inequalities are strict where required. In particular, equality in
+`a(2m+1)>=3D` is allowed because (2) is strict for `m>=2`.
+
+## Comparison with the cited bound
+
+The predecessor #7450 supplies `ceil(27D/(17a))` as a sufficient threshold
+through a uniform binomial bound and the pair `3^17<2^27`. That predecessor
+result is a cited premise, not a replay target. The following comparison is
+also an elementary comparison of the two displayed formulas.
+
+When `a>D`, the old ceiling is at least one, so it is at least `T=1`.
+When `a<=D`, put `R=D/a>=1`. The old ceiling is at least two, and
+
+```text
+27R/17 - (3R-1)/2 = 3R/34 + 1/2 > 0.
+```
+
+Ceiling monotonicity then gives
+
+```text
+max(2, ceil((3R-1)/2)) <= ceil(27R/17).
+```
+
+Hence the new sufficient threshold never worsens that cited threshold.
+
+## The two sharp examples
+
+For `D=5,a=1`, the new value is `ceil(14/2)=7`. At its predecessor,
+
+```text
+7^5 = 16807 > 15552 = 2*6^5.
+```
+
+Thus (1) fails at `m=6`. The theorem proves (1) for every `m>=7`;
+directly, `8^5=32768<33614=2*7^5`. This makes seven the least integer
+threshold valid for all subsequent integers at this triple.
+
+For `D=5,a=2`, the new value is `ceil(13/4)=4`. At its predecessor,
+
+```text
+4^5 = 1024 > 972 = 4*3^5.
+```
+
+The theorem proves (1) for every `m>=4`; directly,
+`5^5=3125<4096=4*4^5`. Thus four remains the exact threshold.
+
+These examples do not make the general formula an exact minimum. For
+`D=10,a=1`, it gives fifteen, but (1) already holds at fourteen because
+`15^10=576650390625<578509309952=2*14^10`.
+
+## Persistence at the retained comparison
+
+Section 6 of the #7000 application review considers a fixed constant
+`C>=1`, an integer degree `d0` and positive rational slack `delta=a/b`.
+For positive `d0`, raising its comparison to the power `b` gives
+
+```text
+P(j): C^b (j+1)^D <= 2^(aj),       D=d0*b.
+```
+
+If `P(j)` holds and `j+1>=T(a,D)`, apply (1) at `m=j+1`:
+
+```text
+C^b (j+2)^D < 2^a C^b (j+1)^D <= 2^(a(j+1)).
+```
+
+Thus `P(j+1)` holds, and induction proves `P(k)` for every integer `k>=j`.
+When `d0=0`, this persistence is immediate without a threshold lemma.
+This establishes a smaller sufficient one-step region. It does not supply
+an initial `j` satisfying `P(j)`, compute any complete selected cutoff,
+or replace the other conditions in the review.
+
+## Evidence and limits
+
+The universal claims above follow from the written argument. The verifier
+corroborates (2) for `m=2..256`, and decreasing `F` at consecutive integers
+for `m=1..255` by exact cross-multiplication. It checks both threshold
+formulas for every `a,D=1..96`, and checks (1) at each new threshold and
+the next two integers. These are bounded finite checks of this new result.
+They do not replay a predecessor verifier or establish the analytic proof
+by enumeration. All arithmetic in the verifier is exact integer arithmetic.
+
+The comparison is an auxiliary threshold lemma, not a physical supplier,
+a new kappa, or a complete multiplication theorem. All five selected
+framework assumptions remain. Independent human and formal proof-kernel
+review are unclaimed.
+
+## Open next questions
+
+Can an elementary rational correction to the shifted bound remove the
+remaining sufficient-versus-necessary gap, such as fifteen versus fourteen
+at `D=10,a=1`? A first step is an explicit upper bound for
+`log(1+1/m)` with one more rational term and a proof that the resulting
+integer test is no worse. This may reduce the auxiliary persistence region;
+it does not determine the initial selected cutoff or settle physical costs.

research/shifted-persistence-threshold/README.md

@@ -0,0 +1,119 @@
+# A shifted persistence threshold that includes the missing seven-step case
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+Claim type: scoped written proof with exact finite corroboration. For
+positive integers `d0,a,b`, set `D=d0*b` and
+
+```text
+T = 1                              if a>D,
+    max(2,ceil((3D-a)/(2a)))        otherwise.
+```
+
+For every integer `m>=T`, `(m+1)^D < 2^a m^D`. The new `T` is never larger
+than `ceil(27D/(17a))`, the sufficient threshold in unpaidmoon's
+[PR #7450](https://github.com/CrocSwap/integer-mult-bounds/pull/7450).
+At `(d0,a,b)=(1,1,5)` it lowers eight to the sharp seven. At `(1,2,5)`
+the sharp four is preserved. The proof uses the classical decreasing
+function `(2x+1) log(1+1/x)`. The threshold application is the new result.
+
+[PROOF.md](PROOF.md) gives the complete argument, the exact endpoint
+exception at `m=1`, and the persistence implication. The general sufficient
+threshold is not an exact minimum. For example it gives fifteen at
+`D=10,a=1`, where fourteen already works.
+
+## Source and scope
+
+This answers Open next question 1 of unpaidmoon #7450 at
+`f9b9057f9befe744df7f6b58b61b53e77001af1f` using an `m`-dependent inequality,
+instead of refining another pair `3^p<2^q` under its uniform bound. Its
+power-pair census and persistence construction are cited, not audited or
+replayed. The question is the source; the classical convexity argument is
+self-contained. No predecessor code or data is needed to run this verifier.
+
+The retained comparison is section 6 of
+[the #7000 application review](../../docs/research/pr-intake-evidence/pr7000-application/PROOF-REVIEW.md).
+[SOURCES.json](SOURCES.json) pins that historical context, the selected
+record and the originating card at canonical base
+`e54523517d0f03e58352e647c403a5af3e525a57`. These are provenance, not live
+mathematical inputs. The source PR is external context with its exact head
+and URL recorded in [TASK.json](TASK.json).
+
+Card `uniform-transfer-audit` has changed scope to this auxiliary lemma.
+It reduces a sufficient persistence region relevant to the effective
+cutoff discussion. It neither constructs the initial successful index nor
+discharges `precision_tape` or another framework assumption. Selected
+`kappa=363005817/100000000000` is unchanged.
+
+## Reproduce
+
+Use CPython 3.12 and the standard library, from the repository root:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/shifted-persistence-threshold/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -O -W error -B research/shifted-persistence-threshold/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/shifted-persistence-threshold
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/shifted-persistence-threshold --check-source-history
+```
+
+On another machine, substitute its CPython 3.12 executable. The direct
+verifier emits `PASS_SHIFTED_PERSISTENCE_THRESHOLD` in a JSON receipt
+containing all six package-file SHA256 hashes and the exact enumerated
+counts. Redirect it outside the checkout to retain a generated receipt.
+No handwritten receipt or generated replay output is committed.
+
+The bounded checks cover 255 shifted-power cases, 255 consecutive decreases,
+9,216 parameter pairs and 27,648 one-step evaluations. In that parameter
+rectangle, 4,753 threshold pairs strictly improve. Nine semantic controls
+cover both sharp examples, strict equality, the `m=1` branch, a
+sufficient-versus-necessary distinction and an overstrong slope. Eight
+invalid parameter pairs must fail with the exact declared reason. Optimized
+execution keeps every check active because checks do not rely on `assert`.
+
+No selected cold replay, predecessor scientific suite, Lean or Docker run
+is needed for this local theorem. No hosted CI success is claimed here.
+
+## Verification design
+
+`verify.py` has a fixed finite workload, no recursion, subprocesses,
+network calls, file writes or dynamic dispatch. All functions are shorter
+than sixty lines. Positive-integer arguments are validated at the threshold
+boundary; all result checks raise explicit errors even under `-O`.
+
+Power of Ten rule 3 has a managed-runtime deviation in `verify.py`: CPython
+allocates arbitrary-precision integers during execution. The finite ranges
+bound each power-product operand below `2^10240`, and the verifier retains
+only one case at a time plus six source hashes. The registered commands
+exercise that complete bounded workload. If these ranges become configurable,
+the change must introduce explicit input and memory caps. Python has no
+compiler warning mode; both registered commands use `-W error`. The package
+does not alter shared diagnostics or repository CI configuration. Ruff and
+Mypy are unavailable on the local PATH; in-memory compilation and the
+warning-strict registered replays are the available Python diagnostics.
+
+## Related open work
+
+- [#7450](https://github.com/CrocSwap/integer-mult-bounds/pull/7450), unpaidmoon,
+  supplies the `27/17` bound and explicitly asks about the missing `m=7`
+  case. This proof includes that case and retains the same sharp four.
+- [#7286](https://github.com/CrocSwap/integer-mult-bounds/pull/7286), unpaidmoon,
+  tightens a monomial record count used elsewhere in the same review.
+  Its count and elimination model are independent of this one-step inequality.
+
+## Open next questions
+
+The final section of [PROOF.md](PROOF.md) asks for a sharper elementary
+correction where this sufficient bound exceeds the true threshold. Its
+first example is `D=10,a=1`; no external blocker is required to begin.
+Physical implementation, complete cutoffs, supplier admission and all five
+framework assumptions remain separate obligations.
+
+## Credit
+
+Credit unpaidmoon #7450 for the source question, the prior `27/17` threshold
+and its retained persistence-note lineage at
+`8e0124415604b89a1cfc842cb6dc6da96ea87ac5`. Credit Douglas Colkitt's retained
+#7000 application review for the effective-cutoff comparison. The convexity,
+logarithm and induction arguments are classical. The shifted
+threshold, its application and its exact verifier were produced by Nick
+Petalas. Independent human and formal proof-kernel review are unclaimed.

research/shifted-persistence-threshold/SOURCES.json

@@ -0,0 +1,24 @@
+{
+  "schema_version": 1,
+  "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "75d77b328ea02ded535e7f23aee5b1e55d0bb1a8",
+      "sha256": "154c3d30455d778fd3343b6b4851f0fa4665f0f7625b0adb3675e2bafbbf6bf1"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "docs/research/pr-intake-evidence/pr7000-application/PROOF-REVIEW.md",
+      "usage": "provenance",
+      "git_blob": "3dd1af2285e597676725e85ad4f65e7ad326d695",
+      "sha256": "4501502c2ceb9759b20372435fe4beb51082c5a5e2910c1fd5dbe6edca415055"
+    }
+  ]
+}