[petalas]

Summary

Scoped mathematical proof with exact finite arithmetic corroboration. The two-parameter dyadic cut family in CubeJerry's #6784 has a unique best member at every height, found by an exact integer sign test. Its optimized deficit from 2n^2 is Theta(n^beta), where beta=4 log(2)/log(16/3). Combining this with the cited global envelope gives the new explicit rate 0 <= 2-E_infinity(n)/n^2 <= 6 n^(-(2-beta)) for dyadic n>=4.

cited two-parameter mass formula
  -> adjacent integer difference with one sign change
  -> unique finite optimizer and sharp within-family deficit exponent
  -> quantitative global convergence bound

The result was produced by Nick Petalas. CubeJerry's exact family formula and envelope are cited mathematical inputs, not rechecked deliverables. The predecessor proof is retained byte-for-byte at head c134aa6edc8ed6444bbf7bfcabbed8124ff26c39, with its original notice and SHA256/Git-blob binding. Retain Chafik Boukhalfa/#628, Philippe Van Velzen/#2177, ywz65/#2735, Adam Gall/#2067 and their credited transport lineage. No new kappa or selected-frontier change.

Evidence

Before, #6784 supplied an explicit family and the limiting leading constant two. After, PROOF.md gives the unique optimizer for every height and the explicit bounds n^beta/6 <= 2n^2-max K <= 6n^beta for that family. The universal claim is the written proof under the stated cited premises.

At publication head 7c92a140620e65f6c0064fe43fe62bb1a29231e3, local CPython 3.12.15 checks pass:

• 32,640 family candidates across all 255 heights from 2 through 256; 32,385 adjacent identities and unique optima.
• 514 exact rational rate brackets, covering heights 2 through 512 and 1024, 2048 and 4096. No floating-point branch or logarithm is used by the verifier.
• Five wrong-decision/formula controls, ten input rejections, and normal/optimized receipt equality. Both direct commands finish below 0.2 seconds locally, versus their 120-second caps. These durations document timeout margin, not a performance claim.
• The registered metadata check and both registered scientific commands pass. Committed-byte and declared-source-history preflight passes for all eight files.
• Standalone replay outside the repository in both modes reproduces the same generated file-hash receipt. Altering the retained source proof is rejected in both modes. No receipt is handwritten or committed.

From the repository root, reproduce with the local interpreter path below, or substitute another CPython 3.12 installation:

/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

Expected markers: PASS_DYADIC_CUT_FAMILY_OPTIMUM, PASS_REGISTERED_RESEARCH_PACKAGE, PASS_RESEARCH_COMMIT_BYTES.

Limitations and unrun obligations

The exact optimizer and sharp exponent apply inside the cited family. The global bound is one-sided quantitative convergence, not an exact global finite-height maximum or matching global deficit exponent. Only dyadic sizes and independent formal completed-leaf errors are covered. Simultaneous native rounding attainment, internal leaf errors, inverse precision, physical access/storage, a complete rounded caller, supplier admission and all five selected framework assumptions remain open. No independent human or proof-kernel review, selected cold replay, Lean or Docker run is claimed. Every registered local obligation was run.

The recorded uniform-transfer-audit card has explicitly changed scope. This is a side result for precision-envelope research, not discharge of the selected precision_tape assumption. The public source proof is retained locally, so scientific replay needs neither the pending predecessor's Git object nor network access.

Open next questions

• Can another chronological cut family improve the global deficit exponent? First derive its exact independent-channel mass and compare it with the proved limit of this family.
• What are the exact global finite-height maxima? Start with a phase recurrence retaining complete profiles and collisions, then compare every phase and readout.

Related open work

• Disprove the universal Omega cut and prove the dyadic error asymptotic (no κ) #6784 supplies the family and leading global limit. This contribution adds the family's exact finite optimizer and the quantitative rate; its transport proof is cited without replay.
• Prove the sharp joint dirty-word interval envelope (no new κ) #6770 proves a sharp envelope for one interval transport row. This contribution instead sums independent completed-leaf error channels and optimizes a cut family.
• Prove all-depth attainment of 4g-3 destination channels (no κ) #6668 proves a small-budget maximum-channel segment at n=2^g-1. Its quantity and attaining family differ from the total dyadic mass optimized here.

Live handoffs, local reservations, the complete 734-open-PR overlap snapshot, recent account PRs, main-tree README object/formula searches and targeted merged searches were checked before committing. The sparse local-note search omitted 8,770 notes; direct origin/main searches supplied the relevant merged-object check. Unpublished work, arbitrary diffs and global literature priority remain outside this lexical coverage. No extra computations were run to validate other open PRs.

Completion refresh inspected this account's nine other open PRs created since the CLAIM: #6785, #6786, #6787, #6788, #6790, #6791, #6792, #6793 and #6794. None studies this dyadic completed-leaf cut family or its total-mass deficit. No additional related-work entry or shared numerical comparison is required; the three related open contributions above remain unchanged.

CI notes

Both hosted checks passed at exact head 7c92a140620e65f6c0064fe43fe62bb1a29231e3 in run 42223418453: plan and replay (research/dyadic-cut-family-optimum). The completed checks were read once; run metadata confirms this exact head and conclusion success. The registered normal and optimized finite arithmetic replay and package metadata checks are certified by the hosted replay. The universal written proof and cited predecessor premises are not proof-kernel certified. All listed local checks also passed.

Merge Danger

Door: two-way. Blast Radius: isolated. Only the new eight-file research/dyadic-cut-family-optimum/ package is added. Shared code, frozen predecessor packages and the selected frontier are unchanged.