[petalas]

Summary

For the sharp net splitting tax N(t, σ) of #6769, this proves where the best integer quotient switches as σ varies. It answers open question 2 of #6769 for every 0 < t < 1.

Claim type: scoped written proof (Lemma 1, Theorem 2, Corollary 3 and section 5 of PROOF.md) plus finite enclosure certificates for five exact t values and q ≤ 30. No new κ, no supplier admission, no selected-frontier change.

sigma     1 <-- tau_4     tau_3     tau_2     tau_1 --> infinity
best q          ... 4   |   3   |   2   |   1
at tau_m the best quotients are exactly m and m+1
window    zeta(m+1) < tau_m < zeta(m),   zeta(x) = (x - t W(x)) / (x - W(x))

• Lemma 1. For integers 1 ≤ q < q', the ratio g_σ(q) / g_σ(q') is strictly increasing in σ. A maximizing remainder is below 1, so the larger quotient is always paid at a larger R = q + s.
• Theorem 2. Each adjacent pair has exactly one tie threshold τ_q in the window above. The thresholds decrease to 1. Every positive integer is the unique best quotient on a nonempty open σ interval, so the best quotient never skips a value.
• Corollary 3. τ_m − 1 ~ (1 − t) m^(t−1). At t = 1/2, ζ(x) = 1 + 1/(√(4x+1) − 1).
• log N(t, ·) is convex with a convex kink at each τ_m.

The proof uses only facts (I1) to (I3), which PROOF.md quotes from #6769 and does not re-prove.

Evidence

Before, #6769 shows the best quotient is ⌊z⌋ or ⌈z⌉ and allows ties. After, the thresholds are unique, ordered and bracketed. Certified values at t = 1/2, with θ_m = z(τ_m) − m:

m	τ_m	θ_m
1	1.6357241325	0.405094
2	1.4383632422	0.441590
3	1.3507366418	0.457824
5	1.2642332618	0.472944
10	1.1800795463	0.485785
20	1.1233222265	0.492734
30	1.0991113903	0.495127

Reproduce from the repository root with CPython 3.12.15. The exact local interpreter is /Users/nick/git/integer-mult-bounds/.venv/bin/python3.12. The package uses the standard library only.

IMB_PYTHON=/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12
"$IMB_PYTHON" -I -W error -B research/net-split-quotient-staircase/verify.py
"$IMB_PYTHON" -I -O -W error -B research/net-split-quotient-staircase/verify.py
"$IMB_PYTHON" -B scripts/research_package.py --package research/net-split-quotient-staircase
"$IMB_PYTHON" -B scripts/research_package.py --package research/net-split-quotient-staircase --check-only
"$IMB_PYTHON" -B scripts/check_research_commit.py --package research/net-split-quotient-staircase --check-source-history --check-modes

Local results at commit 7741b65a42e6f1bb586267afe08dc1a90d25448c:

• Both direct runs print PASS_NET_SPLIT_QUOTIENT_STAIRCASE. The measured wall times are 6.74 s for normal Python and 6.38 s for optimized Python, each below its registered 300 s timeout and CI's 600 s limit. These are single executions, not benchmark estimates.
• The registered replay prints PASS_REGISTERED_RESEARCH_PACKAGE research/net-split-quotient-staircase outcome=completed. Both registered commands together take 13.36 s of wall time.
• The metadata check prints PASS_PACKAGE_METADATA_AND_PINS.
• The commit check prints PASS_RESEARCH_COMMIT_BYTES for 6 files, source history and executable modes.

What verify.py checks:

• 150 enclosure-certified pairs (t, q) with t in {1/10, 1/4, 1/2, 3/4, 9/10} and q ≤ 30. Each has a bracket of half-width at most 1e-12 around τ_q with ρ_q < 1 on the left and ρ_q > 1 on the right, the window ζ(q+1) < τ_q < ζ(q), and ζ(q+½) < τ_q. The smallest relative margin is 3.2e-14.
• 400 ratio evaluations on a grid, all increasing in σ. Also 48 envelope-slope comparisons, 12 pairs of one-sided slopes at thresholds that show the convex kink, and 261 second differences of log N.
• A float brute force over integer quotients 1 to 200 at 300 values of σ agrees with the staircase read from the thresholds.
• The t = 1/2 closed form and ζ(n(n+1)) = 1 + 1/(2n) for n ≤ 16.
• Eight rejection controls and a nearest-integer witness. At t = 1/2, σ = 1.62201395897… has z = 1.45, which rounds to 1, yet quotient 2 is strictly better (ρ_1 < 0.9925).

Limits

• The enclosure arithmetic widens every exp and ln result by a relative 4e-70 and treats the 100-digit rounding of + − × ÷ as exact. It relies on the documented correct rounding of Decimal.exp and Decimal.ln. Every certified margin is above 1e-15, so the omitted rounding cannot change a verdict.
• The inequality θ_m < 1/2 is certified only for the 150 pairs above. It is not proved in general.
• Lemma 1 and Theorem 2 depend on (I1) to (I3) of Determine the sharp net splitting-tax coefficient (no new κ) #6769, which are quoted and not re-proved here.
• The remark about convexity in the free exponent u of Determine the sharp net splitting-tax coefficient (no new κ) #6769's test (10) is conditional on P_x being a positive moment Σ n_r r^x. I did not re-read Reduce p7 tensor power and uniform-rank exponent (41.6× and 46.38M×) #4433 or Reduce sufficient uniform-rank exponent 18.28× with net taxes and log moments #4480 for that form.
• t = 1/3 and 2/3 are not exact decimals and were not certified. Nothing here covers the full split charge of Prove the sharp direct higher-moment integer split charge (no κ) #6390.
• Hosted package replay was skipped because the repository's plan job failed; CI certified nothing for this package. Lean and Docker were not run. No independent human or proof-kernel review is claimed.
• This is a side result on a compiler coefficient. It is not a complete multiplication theorem and says nothing about any supplier.

Open next questions

1. Is θ_q < 1/2 for every 0 < t < 1 and every q ≥ 1? What is c_t in 1/2 − θ_q ~ c_t / q? The certified table has (1/2 − θ_q) q ≈ 0.15 at q = 30. A first step is to prove g(z + ½) > g(z − ½) at fixed σ. The blocker is that s_q has no closed form.
2. For the historical Conditional κ .003125804 (+5.22e-7 over #5907): remove helper 470's frame-593 rung, the twin of #5907's removal #6030 application linked from Determine the sharp net splitting-tax coefficient (no new κ) #6769, does the minimizing u of test (10) sit at a kink u = τ_m − t? A first step is to scan u over its exact moment intervals. The blocker is those moments and the moment form of P_x.
3. Is τ_m(t) increasing in t for each m? The table suggests it. A first step is to differentiate ρ_m(σ; t) = 1 in t. The blocker is the t-derivative of s_q.

The structured versions are in TASK.json.

Related open work

The earlier open/merged search for "net splitting", "splitting tax", "best quotient", "quotient staircase" and "tie threshold" found no overlapping open PR, with handoff claims read up to 2026-11-10 22:26 UTC. The merged predecessor is #6769 (CubeJerry), which supplies N and the question. Merged #6390 covers the full split charge and its q = 1 reduction, which this PR does not use.

The final own-account check listed all open PRs and compared those created after the CLAIM at 2026-11-10 22:15:02 UTC. The titles and bodies of #7132 (BIT stock-width fit), #7133 (dyadic aligned-window guard) and #7134 (odd-rectangle residual-rank floor) concern different objects and quantities. None requires a numerical comparison with this package.

CI notes

At head 7741b65a42e6f1bb586267afe08dc1a90d25448c, run 42914936342 failed in the plan job, job 130174850365, at "Onboarding helper tests". The log reports 760 tests, one failure and 24 skipped. The exact failing test is test_research_current_status.CurrentCiNavigationTests.test_current_ci_section_matches_selected_record, with AssertionError: '`make frontier7000-verify`' not found in the current section of docs/ci-verification.md.

The mismatch is already present at main/base e54523517d0f03e58352e647c403a5af3e525a57: certificates/selected-result.json names make frontier7000-verify, while that documentation section still describes #6030 and make frontier6030-verify. The selected record, CI document and failing test are unchanged by this PR; its only changed paths are the six new package files.

I also read the failed job logs for 42905094314, 42903313790, 42914704054 (#7132), 42914729845 (#7133), and 42914997118 (#7134). Each reports the same test and missing-command assertion, with one failure among 760 tests and 24 skipped.

The package replay job was skipped because plan failed. CI did not certify this package. The evidence above is local verification at the exact PR head. No CI rerun or retrigger commit was made; the repository-level mismatch is left for maintainers.

Merge danger

Door: two-way. Blast radius: one new directory, research/net-split-quotient-staircase. No shared file, selected record or frozen source changes.

Credit

This contribution was produced by Nick Petalas. CubeJerry's #6769 supplies N, the maximizer equation (3), the unimodality in q and the question. Apache-2.0.