Optimize dyadic error cuts and prove a quantitative convergence rate (no κ)

research/dyadic-cut-family-optimum/PREDECESSOR.json

@@ -0,0 +1,15 @@
+{
+  "author": "CubeJerry",
+  "pr": 6784,
+  "commit": "c134aa6edc8ed6444bbf7bfcabbed8124ff26c39",
+  "url": "https://github.com/CubeJerry/integer-mult-bounds/blob/c134aa6edc8ed6444bbf7bfcabbed8124ff26c39/research/dyadic-omega-counterexample/PROOF.md",
+  "retained_path": "predecessor-proof.md",
+  "sha256": "986c4341bad842a30655ca959fdf8a13c95764f721499a5e580ad78b64dbac0c",
+  "git_blob": "e903af6bf67dfced9a235413bb6a7cdb8e08030f",
+  "used_claims": [
+    "Section 6 equation (11) global upper envelope",
+    "Section 6 equation (12) cut-family mass and chronology"
+  ],
+  "review_status": "Cited mathematical input; not independently audited here.",
+  "license": "Apache-2.0; original notice retained verbatim."
+}

research/dyadic-cut-family-optimum/PROOF.md

@@ -0,0 +1,182 @@
+# Exact optimization of the dyadic cut family
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+Independent human and formal proof-kernel review are unclaimed.
+
+## Mathematical input and claim boundary
+
+CubeJerry's [PR #6784](https://github.com/CrocSwap/integer-mult-bounds/pull/6784),
+head `c134aa6edc8ed6444bbf7bfcabbed8124ff26c39`, section 6, supplies the
+following exact mass for a chronological cut of the balanced dirty word.
+For integers `h >= 2`, `0 <= k <= h-2`, and `m=h-k-1`, it reads scratch
+`z_(m+1)` after `4^h-(4^k+2)/3` completed leaves and has total channel mass
+
+```text
+6 K_h(k) = (48*4^m-4)*4^k
+           +(-36*4^m-24*2^m+12*3^m+3)*3^k
+           +24*2^(m+k)-5.                         (1)
+```
+
+The same source proves that the global formal peak `E_h=E_infinity(2^h)`,
+over all cuts, registers and both orientations, satisfies
+
+```text
+max_k K_h(k) <= E_h <= 2*4^h-3^h.                 (2)
+```
+
+We cite (1) and (2), without rechecking their free-algebra transport proofs.
+The unchanged source proof is retained as [predecessor-proof.md](predecessor-proof.md),
+with its original attribution. [PREDECESSOR.json](PREDECESSOR.json) binds its
+exact bytes and source URL. The new proof below optimizes (1) and quantifies
+its convergence. It does not determine the global finite-height peak.
+
+## The unique optimum at every height
+
+Let `D_h(k)=2*4^h-K_h(k)`. Substituting `m=h-k-1` in (1) gives
+
+```text
+6 D_h(k) = 4*4^k + 9*4^h*(3/4)^k + 12*2^h*(3/2)^k
+           -4*3^h -3*3^k -12*2^h +5.             (3)
+```
+
+Subtract (3) at adjacent indices. For `0 <= k <= h-3`,
+
+```text
+8 [D_h(k+1)-D_h(k)] = T_h(k),
+T_h(k) = 16*4^k -3^k [3*4^(h-k)-8*2^(h-k)+8].   (4)
+```
+
+The normalized quantity
+
+```text
+T_h(k)/3^k = 16*(4/3)^k - f(2^(h-k)),
+f(t)=3t^2-8t+8,                                  (5)
+```
+
+is strictly increasing in `k`. Its first term increases. Its subtracted
+term decreases, because `f` is strictly increasing for `t >= 4`, and the
+arguments under consideration are at least eight. Thus the sign in (4)
+changes at most once, from negative to positive.
+
+There are no ties. For `k >= 1`, `T_h(k)` is one modulo three. For `k=0`
+and `h>=3`, `2^h>=8`, so `f(2^h)>=f(8)=136>16` and `T_h(0)<0`.
+For `h=2` there is only one candidate.
+
+Consequently the following rule gives the unique maximizer of (1):
+
+```text
+k_h = the first k in [0,h-3] for which T_h(k)>0;
+      use h-2 if that set is empty.
+m_h = h-k_h-1.                                   (6)
+```
+
+This is an exact integer criterion. Bisection uses at most
+`ceil(log2(h-1))` sign comparisons. The count is a comparison bound,
+not a bit-complexity or physical tape-cost claim.
+
+For example `h=11` gives `k_h=8`, `m_h=2`, cut `4^11-21846`, and readout
+`z_3`. Its mass is `7,735,559`. The `m=1` member has mass `7,716,024`.
+These values evaluate the cited formula, rather than replaying its native
+realization. The improvement inside this explicit family is `19,535`.
+
+## A sharp exponent for the family's deficit
+
+Define real constants
+
+```text
+alpha = log(4)/log(16/3),
+lambda = 4^alpha,
+beta = log_2(lambda) = 4*log(2)/log(16/3).
+```
+
+Here `beta` is about `1.656289`. For every integer `h>=2`, the optimized
+family deficit `D_h=min_k D_h(k)` satisfies
+
+```text
+lambda^h/6 <= D_h <= 6*lambda^h.                  (7)
+```
+
+Thus `D_h=Theta(lambda^h)=Theta(n^beta)` for dyadic `n=2^h`. The exponent
+is sharp within the family (1). This does not assert that the global peak
+has a deficit of this order.
+
+To prove the lower bound, put `Q=4^h*(3/4)^k`. Since `h-k>=2`,
+
+```text
+9Q >= 16*3^h,
+4*4^k-3*3^k >= 4^k,
+12*2^h*((3/2)^k-1) >= 0.
+```
+
+Equation (3) therefore implies `6D_h(k) >= 4^k+Q`.
+The two expressions `4^k` and `Q` are equal at the real index
+`k=alpha*h`, with common value `lambda^h`. One increases in `k` and
+the other decreases. Hence their maximum is always at least `lambda^h`,
+proving the lower bound in (7).
+
+For the upper bound take `k=floor(alpha*h)`. For `h>=12` this is a legal
+family index: `alpha<5/6` follows from `3^5<4^4`. Then
+
+```text
+4^k <= lambda^h,
+Q <= (4/3)*lambda^h,
+2^h*(3/2)^k <= lambda^h.
+```
+
+For the third inequality it suffices that `2*(3/2)^alpha < 4^alpha`.
+Indeed
+
+```text
+alpha*log(8/3)-log(2)
+    = log(2)*log(4/3)/log(16/3) > 0.
+```
+
+Dropping the negative terms in (3) now gives
+`6D_h(k) <= 28*lambda^h+5 <= 33*lambda^h < 36*lambda^h`.
+For the ten remaining heights `h=2,...,11`, exact evaluation of (1),(6)
+gives deficits
+
+```text
+19, 64, 209, 668, 2109, 6624, 20809, 65668, 208949, 653049.
+```
+
+Each is at most `6*3^h`. Finally `lambda>3`, since
+`log(4)^2-log(3)*log(16/3)=(log(4)-log(3))^2>0`.
+This establishes the upper bound of (7) at every height.
+
+## Quantitative consequence for the global peak
+
+Combining the cited envelope (2) with the new constructive bound (7) gives
+
+```text
+3^h <= 2*4^h-E_h <= 6*lambda^h,
+n^(log_2(3)) <= 2*n^2-E_infinity(n) <= 6*n^beta,
+0 <= 2-E_infinity(n)/n^2 <= 6*n^(-(2-beta)).        (8)
+```
+
+The last two lines apply to dyadic `n>=4`. This gives an explicit
+power-saving convergence rate where the predecessor supplied a limit.
+The lower and upper exponents for the global deficit still differ.
+No arbitrary-`n`, exact global optimum, error-budget profile, physical
+rounding realization, new multiplier or new kappa follows.
+
+## Executable evidence and remaining obligations
+
+The verifier checks the new integer optimization, adjacent identity and
+rational enclosures used for (7). It takes (1) as input and does not
+execute any predecessor verifier or reconstruct its channel polynomials.
+Its finite arithmetic checks corroborate the written proof; they do not
+replace the all-height argument. The same explicit checks run under `-O`.
+
+Python allocates integers dynamically. This is the bounded managed-runtime
+deviation to Power of Ten rule 3: height is restricted to `2..4096`, the
+exhaustive range to `2..256`, and no word of length `4^h` is materialized.
+All loops have bounds, functions are at most 60 lines, failure checks use
+explicit exceptions, and there is no recursion, dynamic code or network
+access. Warning-strict normal and optimized replay provide interpreted-code
+diagnostics; no external static analyzer is a dependency. Expanding the
+height bound requires revisiting integer resource bounds.
+
+All five selected framework assumptions remain. Independent human review,
+formal proof-kernel review, native rounding, internal leaf errors, inverse
+precision, physical storage/access and a complete selected caller are unrun.

research/dyadic-cut-family-optimum/README.md

@@ -0,0 +1,115 @@
+# The exact best cut in the dyadic two-parameter family
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+Independent human and formal proof-kernel review are unclaimed.
+
+This scoped proof gives the unique best member of CubeJerry's
+[PR #6784](https://github.com/CrocSwap/integer-mult-bounds/pull/6784)
+cut family at every fixed height. It also sharpens the predecessor's
+leading asymptotic to an explicit convergence rate. No new kappa is claimed.
+
+For height `h>=2`, write `m=h-k-1` with `0<=k<=h-2`. The family reads
+scratch `z_(m+1)` at completed-leaf cut `4^h-(4^k+2)/3`. Its mass `K_h(k)`
+is equation (12) of the cited predecessor, treated as a mathematical input.
+The new adjacent-difference identity is
+
+```text
+8 * [K_h(k)-K_h(k+1)]
+    = 16*4^k - 3^k*(3*4^(h-k)-8*2^(h-k)+8).
+```
+
+After division by `3^k` this expression strictly increases and never
+vanishes. The first positive value gives the unique optimum; if there
+is none, use `k=h-2`. Exact integer bisection finds it using logarithmically
+many comparisons in `h`.
+
+Let `D_h=2*4^h-max_k K_h(k)`, and
+`beta=4*log(2)/log(16/3)`, about `1.656289`. The new proof establishes
+
+```text
+(2^h)^beta / 6 <= D_h <= 6*(2^h)^beta.
+```
+
+The exponent is sharp inside this family. For the global formal peak,
+the source's envelope consequently gives the new quantitative statement
+
+```text
+0 <= 2-E_infinity(n)/n^2 <= 6*n^(-(2-beta))
+```
+
+for every dyadic `n>=4`. No matching global deficit exponent or exact global
+maximizer is asserted. [PROOF.md](PROOF.md) proves the optimizer, the bounds,
+the finite exceptional heights and the stated distinction.
+
+## Evidence and reproduction
+
+From the repository root, with CPython 3.12 and its standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -X dev -W error -B research/dyadic-cut-family-optimum/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -X dev -W error -O -B research/dyadic-cut-family-optimum/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/dyadic-cut-family-optimum
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/dyadic-cut-family-optimum --check-source-history
+```
+
+An equivalent CPython 3.12 interpreter path works elsewhere. Expected markers
+are `PASS_DYADIC_CUT_FAMILY_OPTIMUM`, `PASS_REGISTERED_RESEARCH_PACKAGE`, and
+`PASS_RESEARCH_COMMIT_BYTES`. The verifier prints a generated receipt bound to
+all eight package files and writes nothing into the checkout.
+
+The finite arithmetic checks enumerate every family member at heights
+`2..256`, check the adjacent identity and unique optimum, and check rational
+rate enclosures through height 512 and at 1024, 2048 and 4096. Exact integer
+powers bracket the logarithmic balance, so no floating-point decision is used.
+The new `h=11` optimum is `k=8,m=2`, with mass `7,735,559`. Five wrong-decision
+and formula controls and ten invalid-input rejections must pass in both modes.
+These corroborate the new written proof. They do not replay predecessor
+channel words or validate the predecessor's theorem.
+
+## Source boundary, credit and limitations
+
+The immediate mathematical input is CubeJerry's PR #6784, exact head
+`c134aa6edc8ed6444bbf7bfcabbed8124ff26c39`, PROOF section 6, equations
+(11), (12) and the family construction. Its unchanged proof is retained in
+[predecessor-proof.md](predecessor-proof.md), including its original notice.
+[PREDECESSOR.json](PREDECESSOR.json) records the public URL, head and byte
+hash. No unavailable side-branch Git object is required for replay.
+
+Retained mathematical credit goes to Chafik Boukhalfa's balanced dirty word
+in #628, Philippe Van Velzen's prefix/exit and inverse lemmas in #2177,
+ywz65's support recurrences in #2735, Adam Gall's endpoint channel counts in
+#2067, and their credited predecessors, including woklerx, Charles Bethin,
+Arham Tahir and Hanson Sun. Their transport results are cited, not audited.
+The new contribution is optimization of the stated two-parameter mass and
+its quantitative rate.
+
+This is a formal free-algebra result for independent completed-leaf errors
+on the unchanged balanced word. It does not prove simultaneous physical
+rounding attainment, internal-leaf error behavior, non-dyadic bounds, a
+complete error-budget profile, a native operator realization, precision/tape
+costs or supplier admission. All five selected assumptions remain, and the
+selected frontier is unchanged. No full selected replay, proof-kernel check
+or independent human review is claimed.
+
+The original `uniform-transfer-audit` card is recorded as changed scope in
+[TASK.json](TASK.json). This is a side result relevant to precision envelopes,
+not discharge of the selected `precision_tape` assumption.
+
+## Related open work
+
+- #6784 is the immediate predecessor. It gives the family and global leading
+  limit; this package adds its exact finite optimizer and a quantitative rate.
+- #6770 studies total mass of one interval transport row; this package sums
+  distinct completed-leaf error channels and optimizes one cut family.
+- #6668 attains a small-error-budget channel segment for `n=2^g-1`; it does
+  not supply the total mass or optimizer studied here for `n=2^h`.
+
+## Open next questions
+
+1. Can another chronological cut family improve the exponent `beta` for the
+   global deficit? First derive its exact independent-channel total and
+   compare it to the proved `Theta(n^beta)` limit of this family. The existing
+   global lower exponent `log_2(3)` does not settle this.
+2. Determine exact global finite-height maxima. Start with a phase recurrence
+   preserving collisions and complete profiles, then compare every phase
+   with the optimized family here. A mass-only relaxation is insufficient.

research/dyadic-cut-family-optimum/SOURCES.json

@@ -0,0 +1,18 @@
+{
+  "schema_version": 1,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a",
+      "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    }
+  ]
+}