From 7741b65a42e6f1bb586267afe08dc1a90d25448c Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 10 Nov 2026 22:27:08 +0000 Subject: [PATCH] feat(research): prove the staircase of best net-split quotients For the sharp net splitting tax of #6769, the ratio of two optimized quotient values is strictly monotone in sigma. Each adjacent pair has one tie threshold inside an explicit window, the thresholds decrease to 1, and every positive integer is the unique best quotient on an open sigma interval. Written proof plus enclosure-certified thresholds for five exact t and q up to 30. The half-window inequality theta < 1/2 is a finite observation only. No new kappa and no selected-frontier change. --- .../net-split-quotient-staircase/PROOF.md | 205 +++++++++ .../net-split-quotient-staircase/README.md | 146 ++++++ .../net-split-quotient-staircase/SOURCES.json | 30 ++ .../net-split-quotient-staircase/TASK.json | 95 ++++ .../net-split-quotient-staircase/VERIFY.json | 34 ++ .../net-split-quotient-staircase/verify.py | 425 ++++++++++++++++++ 6 files changed, 935 insertions(+) create mode 100644 research/net-split-quotient-staircase/PROOF.md create mode 100644 research/net-split-quotient-staircase/README.md create mode 100644 research/net-split-quotient-staircase/SOURCES.json create mode 100644 research/net-split-quotient-staircase/TASK.json create mode 100644 research/net-split-quotient-staircase/VERIFY.json create mode 100644 research/net-split-quotient-staircase/verify.py diff --git a/research/net-split-quotient-staircase/PROOF.md b/research/net-split-quotient-staircase/PROOF.md new file mode 100644 index 0000000000..40c9223027 --- /dev/null +++ b/research/net-split-quotient-staircase/PROOF.md @@ -0,0 +1,205 @@ +# The best-quotient staircase of the sharp net splitting tax + +This proof was produced by Nick Petalas. Apache-2.0. + +It answers the open question of CubeJerry's +[PR #6769](https://github.com/CrocSwap/integer-mult-bounds/pull/6769) +(`research/sharp-net-splitting-tax`): how the best integer quotient moves as +sigma varies. Sections 2 to 5 are written proofs. They use only the facts +(I1) to (I3) of section 0, which are quoted from #6769 and not re-proved here. + +## 0. Setting and quoted facts + +Fix `0 < t < 1`. For real `q > 0`, `sigma >= 1` and `0 <= s <= 1` put + +``` +A_q(s) = q + s^t - (q+s)^t, +F_q(s; sigma) = A_q(s) / (q+s)^sigma, +g_sigma(q) = max_{0<=s<=1} F_q(s; sigma). +``` + +Let `a = t^(1/(1-t))`, so `a^(1-t) = t` and `t a^(t-1) = 1`, and let +`W(x) = (x+a)^t - a^t` for `x > 0`. + +Quoted from #6769 (`PROOF.md` sections 2 to 4): + +* **(I1)** For every real `q > 0` and `sigma >= 1`, `F_q(.; sigma)` has a unique + maximizer `s_q(sigma)` on `[0,1]`, and it lies in `(0,1)`. It is the root of + `H_q(s) = t q s^(t-1) + (t-sigma) s^t - sigma q + (sigma-t)(q+s)^t`. +* **(I2)** For `sigma > 1` the equation `(sigma-t) W(z) = (sigma-1) z` has a + unique positive root `z = z(sigma)`. The map `q -> g_sigma(q)` is strictly + increasing on `(0, z]` and strictly decreasing on `[z, infinity)`. +* **(I3)** `N(t,sigma) = max_{q integer >= 1} g_sigma(q)`, and the integer + maximizers lie in `{max(1, floor z), max(1, ceil z)}`. + +**(I4)** (proved here) For an integer `q >= 1` and `0 < s < 1`, `A_q(s) > 0`. +Indeed `s^t > s`, so `A_q(s) > x - x^t >= 0` with `x = q + s >= 1`. Hence +`F_q(s; sigma) > 0` and `g_sigma(q) > 0`. + +## 1. The window function zeta + +Since `W(0) = 0` and `W'(x) = t (x+a)^(t-1) < t a^(t-1) = 1`, we have +`0 < W(x) < x`; and `W` is strictly concave, so `W(x)/x` decreases strictly +from `W'(0) = 1` to `0`. Define, for `x > 0`, + +``` +zeta(x) = (x - t W(x)) / (x - W(x)) = 1 + (1-t) / (x/W(x) - 1). +``` + +**Lemma 0.** `zeta` is a continuous strictly decreasing bijection from +`(0, infinity)` onto `(1, infinity)`, and `z(sigma) = zeta^(-1)(sigma)`. + +*Proof.* `x/W(x)` increases strictly from 1 to infinity, so `x/W - 1` +increases strictly from 0 to infinity and `zeta` decreases strictly from +infinity to 1. The equation of (I2) reads `sigma (W - x) = t W - x`, that is +`sigma = zeta(x)`. By (I2) it has exactly one positive root `z(sigma)`. QED + +For `t = 1/2`: `a = 1/4`, and with `w = sqrt(x + 1/4)` one gets +`x - W = (w - 1/2)^2` and `zeta(x) = w/(w - 1/2) = 1 + 1/(sqrt(4x+1) - 1)`. +In particular `zeta(n(n+1)) = 1 + 1/(2n)`, the #6769 family. + +## 2. The ratio of two quotients is monotone in sigma + +**Lemma 1.** Let `q < q'` be integers with `q >= 1`, and `1 < sigma_1 < sigma_2`. +Then + +``` +g_{sigma_2}(q) / g_{sigma_2}(q') > g_{sigma_1}(q) / g_{sigma_1}(q'). +``` + +*Proof.* Put `Delta = sigma_2 - sigma_1 > 0`, `s = s_q(sigma_1)` and +`s' = s_{q'}(sigma_2)`; both lie in `(0,1)` by (I1). For any `s0`, +`F_r(s0; sigma_2) = F_r(s0; sigma_1) (r + s0)^(-Delta)`. Therefore + +``` +g_{sigma_2}(q) >= F_q(s; sigma_2) = g_{sigma_1}(q) (q+s)^(-Delta), +g_{sigma_2}(q') = F_{q'}(s'; sigma_2) = F_{q'}(s'; sigma_1) (q'+s')^(-Delta) + <= g_{sigma_1}(q') (q'+s')^(-Delta). +``` + +All quantities are positive by (I4). Dividing, + +``` +g_{sigma_2}(q)/g_{sigma_2}(q') >= [g_{sigma_1}(q)/g_{sigma_1}(q')] ((q'+s')/(q+s))^Delta. +``` + +Now `q' + s' > q' >= q + 1 > q + s`, because `s' > 0` and `s < 1`. The base of +the power exceeds 1 and `Delta > 0`, so the inequality is strict. QED + +The proof does not use uniqueness of the maximizers beyond their location in +`(0,1)`, and it is an envelope argument: the larger quotient is always paid +at a larger `R = q + s`, so a larger sigma hurts it more. + +## 3. The staircase + +For an integer `q >= 1` put `rho_q(sigma) = g_sigma(q) / g_sigma(q+1)`. The +function `sigma -> g_sigma(q)` is continuous, being a maximum over the compact +interval `[0,1]` of functions continuous in `(s, sigma)`. Hence `rho_q` is +continuous and positive on `(1, infinity)`. + +**Theorem 2.** Fix `0 < t < 1`. + +1. For every integer `q >= 1` there is exactly one `tau_q > 1` with + `rho_q(tau_q) = 1`. Moreover `rho_q < 1` for `sigma < tau_q`, + `rho_q > 1` for `sigma > tau_q`, and + `zeta(q+1) < tau_q < zeta(q)`. +2. `tau_1 > tau_2 > ...` and `tau_q -> 1`. +3. With `tau_0 = +infinity`: for every integer `m >= 1` and every + `tau_m < sigma < tau_{m-1}`, the unique best integer quotient at `sigma` is + `m`. At `sigma = tau_m` the best quotients are exactly `m` and `m + 1`. + Equivalently, away from the thresholds the best quotient is + `1 + #{ m >= 1 : tau_m > sigma }`. +4. Hence the best quotient is nonincreasing in sigma, it jumps by exactly one + at each `tau_m`, and every positive integer is the unique best quotient on + a nonempty open interval of sigma. For `tau_m <= sigma <= tau_{m-1}`, + `N(t, sigma) = g_sigma(m)`. + +*Proof.* (1) By Lemma 1 (with `q' = q + 1`) `rho_q` is strictly increasing, so +it takes the value 1 at most once. At `sigma = zeta(q+1)` we have +`z = q + 1` (Lemma 0), and by (I2) `g(q) < g(q+1)`, so `rho_q < 1`. At +`sigma = zeta(q)` we have `z = q`, and `g(q+1) < g(q)`, so `rho_q > 1`. By the +intermediate value theorem the root `tau_q` exists and lies strictly between +`zeta(q+1)` and `zeta(q)`, with the stated signs on either side. + +(2) By (1) and Lemma 0, `tau_{q+1} < zeta(q+1) < tau_q`. Also +`1 < tau_q < zeta(q) -> 1`. + +(3) Let `sigma > 1` and `z = z(sigma)`. + +* If `z <= 1`, that is `sigma >= zeta(1) > tau_1`, the candidate set of (I3) + is `{1}`; the best quotient is 1 and the formula gives 1. +* If `z = m` is an integer, then `sigma = zeta(m)` and `tau_m < zeta(m) < tau_{m-1}` + by (1); by (I2) `m` is the unique best, matching the formula. +* If `m < z < m + 1` for an integer `m >= 1`, then + `zeta(m+1) < sigma < zeta(m)` and by (I3) the best quotients lie in + `{m, m+1}`. By (1), `m` is strictly better iff `sigma > tau_m`, `m + 1` is + strictly better iff `sigma < tau_m`, and they tie iff `sigma = tau_m`. Since + `tau_{m+1} < zeta(m+1)` and `zeta(m) < tau_{m-1}`, the sigma between + `tau_m` and `zeta(m)` lie in `(tau_m, tau_{m-1})` with best quotient `m`, + and those between `zeta(m+1)` and `tau_m` lie in `(tau_{m+1}, tau_m)` with + best quotient `m + 1`. + +These cases cover every `sigma > 1`, and the tie sets are as stated. + +(4) is a restatement: the intervals `(tau_m, tau_{m-1})` are nonempty by (2). QED + +**Corollary 3 (rate).** As `x -> infinity`, `W(x) = x^t (1 + O(x^(-t)))`, hence +`zeta(x) - 1 = (1-t) W/(x-W) ~ (1-t) x^(t-1)`. Since `zeta(m+1) < tau_m < zeta(m)`, + +``` +tau_m - 1 ~ (1-t) m^(t-1) (m -> infinity), +``` + +and the best quotient grows like `((1-t)/(sigma-1))^(1/(1-t))` as sigma +decreases to 1. For `t = 1/2` this is `1/(4 (sigma-1)^2)`, and the exact window +is `1 + 1/(sqrt(4m+5) - 1) < tau_m < 1 + 1/(sqrt(4m+1) - 1)`. + +## 4. Where in the window the tie sits + +Write `theta_m = z(tau_m) - m`; by Theorem 2 (1), `0 < theta_m < 1`. The +nearest-integer rule would correspond to `theta_m = 1/2`. The finite +certificates of `verify.py` show `theta_m < 1/2` for each certified pair +(`t` in {1/10, 1/4, 1/2, 3/4, 9/10}, `m <= 30`); the sampled values of +`theta_m` increase toward `1/2`. They also give concrete witnesses that rounding +`z` to the nearest integer is not the best-quotient rule (at `t = 1/2`, +`z = 1.45` rounds to 1 but quotient 2 is strictly better). **This is not +proved for all `t` and `m`.** It is an open question in the package README. + +## 5. Log-convexity and kinks + +`log g_sigma(m) = max_s [ log A_m(s) - sigma log(m+s) ]` is a maximum of affine +functions of sigma, so it is convex; by Theorem 2 only finitely many `m` +matter near any sigma, so `log N(t, .) = max_m log g_.(m)` is convex on +`(1, infinity)`. Each branch is strictly decreasing, since `m + s > 1`. + +By the implicit function theorem (the same sign computation as (5) of #6769, +with `sigma` in place of `q`), `s_m(sigma)` is `C^1`, and the envelope theorem +gives `d/dsigma log g_sigma(m) = - log R_m(sigma)` with `R_m = m + s_m(sigma)`. +At `sigma = tau_m` the branches `m + 1` (to the left) and `m` (to the right) +meet, with slopes `-log R_{m+1}` and `-log R_m`. Since +`R_{m+1} > m + 1 > R_m`, the slope jumps up by `log(R_{m+1}/R_m) > 0`, and +`R_{m+1}/R_m < (m+2)/m`. So `N(t, .)` is real analytic between consecutive +thresholds and has a genuine convex kink at every `tau_m`; the kinks +accumulate only at `sigma = 1`. `verify.py` spot-checks the slope formula +numerically. + +**Remark (conditional, for users of the strictification test).** In the +complete sufficient test (10) of #6769 section 6, with `t`, `v`, the bases and +the histograms fixed, the only summand that depends on `u >= 1 - t` is +`N(t, t+u) gamma(u)^v` with `gamma(u) = P_{t+u} / (c^u T_t)`. If `P_x` is a +positive moment `sum n_r r^x` (the form of the paid moments in #4433 and #4480, +which this package did not re-read), it is log-convex in `u` by Holder's +inequality, `c^(-uv)` is log-linear, and `N(t, t+u)` is log-convex by the +paragraph above. A product of log-convex functions is log-convex, and a +log-convex function is convex. Then the left side of (10) is a convex function +of `u`, any local minimizer is global, the minimizers form an interval, and a +minimizer can sit at a kink `u = tau_m - t`, where a stationary-point solver +would not find it. Whether a real inventory has its optimum at a kink is open. + +## 6. What is and is not claimed + +Proved (written): Lemma 0, Lemma 1, Theorem 2, Corollary 3 and the section 5 +statements, from (I1) to (I3) of #6769. Finite certificates (`verify.py`): the +tie bracket, window and `theta < 1/2` for 150 `(t, m)` pairs, with enclosure +arithmetic described in `README.md`. Not proved: `theta_m < 1/2` for all +`t` and `m`; any statement about an actual supplier. diff --git a/research/net-split-quotient-staircase/README.md b/research/net-split-quotient-staircase/README.md new file mode 100644 index 0000000000..62d71d4acb --- /dev/null +++ b/research/net-split-quotient-staircase/README.md @@ -0,0 +1,146 @@ +# The best-quotient staircase of the sharp net splitting tax + +This contribution was produced by Nick Petalas. Apache-2.0. + +**Scoped written proof with finite enclosure certificates; no new κ, no +supplier admission, no selected-frontier change.** + +CubeJerry's merged [PR #6769](https://github.com/CrocSwap/integer-mult-bounds/pull/6769) +(`research/sharp-net-splitting-tax`) shows that for `0 < t < 1` and `σ > 1` the +sharp net-tax coefficient `N(t,σ)` is attained at `⌊z⌋` or `⌈z⌉`, where `z` +solves its equation (2). It allows ties, assumes no rounding rule, and lists as +open how the best integer quotient moves as `σ` varies. This package answers +that question for every `t`, with a proof that uses only the facts (I1) to (I3) +quoted from #6769. + +## Result + +Write `g_σ(q)` for the optimized value of quotient `q` (the maximum over the +remainder of `F_q`), `a = t^(1/(1-t))`, `W(x) = (x+a)^t − a^t` and + + ζ(x) = (x − tW(x)) / (x − W(x)). + +`ζ` is a closed-form, strictly decreasing bijection `(0,∞) → (1,∞)`, and +`z(σ) = ζ⁻¹(σ)` (PROOF.md section 1). For `t = 1/2`, +`ζ(x) = 1 + 1/(√(4x+1) − 1)`, so `ζ(n(n+1)) = 1 + 1/(2n)`: the #6769 family. + +1. **Ratio monotonicity** (Lemma 1). For integers `1 ≤ q < q'`, the ratio + `g_σ(q)/g_σ(q')` is strictly increasing in `σ`. The reason is an envelope + argument: a maximizing remainder is below 1, so the larger quotient is paid at + a larger `R = q + s`, and a larger `σ` hurts it more. +2. **Staircase** (Theorem 2). Each adjacent pair has exactly one tie threshold + `τ_q`, with `ζ(q+1) < τ_q < ζ(q)`. The thresholds satisfy + `τ_1 > τ_2 > … → 1`. For `τ_m < σ < τ_{m−1}` (`τ_0 = ∞`) the unique best + quotient is `m`; at `σ = τ_m` the best quotients are exactly `m` and `m+1`. + So the best quotient is nonincreasing, jumps by exactly one, and **every + positive integer is the unique best quotient on a nonempty open interval of + `σ`**. #6769's family `σ = 1 + 1/(2n)` only meets the pronic values `n(n+1)`. +3. **Rate** (Corollary 3). `τ_m − 1 ~ (1−t) m^(t−1)`, and the best quotient grows + like `((1−t)/(σ−1))^(1/(1−t))` as `σ ↓ 1`; for `t = 1/2` this is + `1/(4(σ−1)²)`. +4. **Shape of `N`** (PROOF.md section 5). `log N(t,·)` is convex and strictly + decreasing on `(1,∞)`, real analytic between thresholds, with a genuine convex + kink at every `τ_m` whose slope jump is `log(R_{m+1}/R_m) ∈ (0, log((m+2)/m))`. + Conditionally on the moment form of `P_x` in #4433/#4480, the left side of + #6769's strictification test (10) is therefore convex in the free exponent + `u`, and its minimizer can sit at a kink (a conditional remark, not a result + about any inventory). + +### Certified thresholds + +For `t ∈ {1/10, 1/4, 1/2, 3/4, 9/10}` and `q ≤ 30`, `verify.py` certifies a +bracket of half-width at most `1e-12` around `τ_q` (150 pairs), by enclosure +arithmetic with `ρ_q < 1` at its left end and `ρ_q > 1` at its right end. The +thresholds, with `θ_q = z(τ_q) − q`: + +| q | τ_q, t = 1/4 | τ_q, t = 1/2 | τ_q, t = 3/4 | θ_q, t = 1/2 | +|---:|---:|---:|---:|---:| +| 1 | 1.4002422608 | 1.6357241325 | 1.8327404694 | 0.405094 | +| 2 | 1.2664553196 | 1.4383632422 | 1.5936908896 | 0.441590 | +| 3 | 1.2074139740 | 1.3507366418 | 1.4876063709 | 0.457824 | +| 5 | 1.1496759204 | 1.2642332618 | 1.3826780029 | 0.472944 | +| 10 | 1.0947642169 | 1.1800795463 | 1.2796676654 | 0.485785 | +| 20 | 1.0593088063 | 1.1233222265 | 1.2085870533 | 0.492734 | +| 30 | 1.0449137612 | 1.0991113903 | 1.1773611067 | 0.495127 | + +All 150 pairs also certify the window `ζ(q+1) < τ_q < ζ(q)` and +`ζ(q+½) < τ_q`, that is `θ_q < 1/2`. **The inequality `θ_q < 1/2` is a finite +observation, not a theorem**; it is the first open question below. It shows that +rounding `z` to the nearest integer is not the best-quotient rule: at `t = 1/2`, +`σ = 1.62201395897…` has `z = 1.45`, which rounds to 1, yet quotient 2 is +strictly better (certified, `ρ_1 < 0.9925`). + +## Reproduce + +Python 3.12, standard library only, from the repository root: + +```sh +python3.12 -I -W error -B research/net-split-quotient-staircase/verify.py +python3.12 -I -O -W error -B research/net-split-quotient-staircase/verify.py +python3.12 -B scripts/research_package.py --package research/net-split-quotient-staircase +python3.12 -B scripts/check_research_commit.py --package research/net-split-quotient-staircase --check-source-history +``` + +The direct commands print a JSON receipt ending in +`PASS_NET_SPLIT_QUOTIENT_STAIRCASE`; each takes about 10 to 25 seconds. They read +and write no files. The checks are: + +- **A.** The `t = 1/2` closed form of `ζ` and `ζ(n(n+1)) = 1 + 1/(2n)` for + `n ≤ 16`. +- **B.** 400 ratio evaluations on a grid (`t` in five values, eight quotient + pairs, ten `σ`): the ratio increases. 48 envelope-slope comparisons against + `−log(q + s_q)`, 12 one-sided slope pairs at thresholds showing the convex + kink, and 261 second differences of `log N`. +- **C.** The 150 enclosure-certified brackets, windows and `θ < 1/2` tests. + Enclosures widen every `exp`/`ln` result by a relative `4e-70` and treat the + 100-digit rounding of `+ − × ÷` as exact. The smallest certified relative + margin is `3.2e-14`, so that omitted rounding (relative `1e-98`) cannot change a + verdict. The enclosure relies on the documented correct rounding of + `Decimal.exp` and `Decimal.ln`. The maximizing remainder is bracketed by a + certified sign change of `H_q`, and the upper bound on `g` uses that bracket. +- **D.** A float brute force over integer quotients `1..200` at 300 values of `σ` + (five `t`, 60 each, `z ≤ 35`) agrees with the staircase read from the + thresholds. +- **E.** Eight rejection controls (the false claim `τ_q < ζ(q+½)` and a bracket + outside its window fail the enclosure test for `t = 1/2`, `q ∈ {1,2,5,12}`), + the nearest-integer witness at `t = 1/2` and `t = 1/4`, and a control that the + inverse ratio is decreasing. + +## Scope and limits + +- **Claim type.** Lemma 1 and Theorem 2 are written proofs, from (I1) to (I3) of + #6769, which are quoted and not re-proved. The tie brackets, windows and + `θ < 1/2` are finite certificates at the listed `(t, q)`; the brute force and + the slope checks are float corroboration. This is not a complete multiplication + theorem and not a statement about any supplier. +- No new κ and no selected-frontier change. The five selected framework + assumptions are untouched. +- `t` ranges over five exact decimals; `t = 1/3` and `2/3` are not exact decimals + and were not certified. Nothing here covers the full split charge of #6390. +- No independent human or proof-kernel review is claimed. + +## Open next questions + +The structured versions are in [TASK.json](TASK.json). + +1. **Half-window.** Is `θ_q < 1/2` for every `0 < t < 1` and every `q ≥ 1`, and + what is `c_t` in `1/2 − θ_q ~ c_t/q`? The certified table has + `(1/2 − θ_q) q ≈ 0.15` at `q = 30`. First step: prove `g(z+½) > g(z−½)` at + fixed `σ`, for example by comparing `F_{q+1}` at the remainder `s_q` with + `g(q)` at `z = q + ½`. Blocker: no closed form for `s_q`. +2. **Kinks in the strictification test.** For the selected #6030 joint + application linked from #6769, does the minimizing `u` of test (10) sit at a + threshold `u = τ_m − t`? First step: scan `u` over its exact moment intervals. + Blocker: those exact moments and the moment form of `P_x`. +3. **Monotone in `t`.** Is `τ_m(t)` increasing in `t` for each `m`? The table + suggests it. First step: differentiate `ρ_m(σ; t) = 1` in `t`. Blocker: the + `t`-derivative of `s_q`. + +These are suggestions, not reservations or novelty guarantees. + +## Credit + +CubeJerry's #6769 supplies the coefficient `N`, the maximizer equation (3), the +unimodality in `q` and the question; it is quoted, not replayed. The envelope +argument and `ζ` are new here. Source pins are in [SOURCES.json](SOURCES.json), +and the scope record is in [TASK.json](TASK.json). diff --git a/research/net-split-quotient-staircase/SOURCES.json b/research/net-split-quotient-staircase/SOURCES.json new file mode 100644 index 0000000000..eed17d1e04 --- /dev/null +++ b/research/net-split-quotient-staircase/SOURCES.json @@ -0,0 +1,30 @@ +{ + "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": "research/sharp-net-splitting-tax/PROOF.md", + "usage": "provenance", + "git_blob": "d49a79b19c791eafbc009fd9fdab17bd3e0d8e2e", + "sha256": "984b5e2d253bce7e5782fd55c8d35343a0e6e6c13544204dd9df3941257ff364" + }, + { + "path": "research/sharp-net-splitting-tax/README.md", + "usage": "provenance", + "git_blob": "a9437232e76cceae07ac9d696eed236e46e8f7c7", + "sha256": "c6437fd6e086add6632ea14f9b7adf7f0747dff489ee539931db1fa0dbc1ef94" + } + ] +} diff --git a/research/net-split-quotient-staircase/TASK.json b/research/net-split-quotient-staircase/TASK.json new file mode 100644 index 0000000000..e128a676e0 --- /dev/null +++ b/research/net-split-quotient-staircase/TASK.json @@ -0,0 +1,95 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 8, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Can one of the selected record's five inherited assumptions be proved at its actual caller?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "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_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Choose one assumption ID (native_all_columns, owned_erasure, compiler, precision_tape, analytic_recovery), one quantified implication and exact dependency closure. Check current handoffs, including #5625 row reentry and #5707 root-prefix lowering, without treating their partial scope as the whole theorem. Prove or falsify that implication with a caller-bound argument; stop at the chosen obligation. Finite tests or root digits do not discharge an all-size statement.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "native_all_columns", + "owned_erasure", + "compiler", + "precision_tape", + "analytic_recovery" + ], + "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": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Characterize where the best integer quotient of the sharp net splitting tax N(t,sigma) switches as sigma varies: unique tie thresholds between adjacent quotients, their order and window, and the resulting staircase, for every 0=1, and what is the constant c_t in 1/2 - theta_q ~ c_t/q?", + "why_it_matters": "It would turn the window zeta(q+1) < tau_q < zeta(q) into a half-window and prove that rounding z to the nearest integer never overshoots the best quotient. The package certifies theta_q < 1/2 for 150 pairs only.", + "first_step": "Show g(z+1/2) > g(z-1/2) at fixed sigma, for example by proving the left slope of log g exceeds the right slope at equal distance from z, or by comparing F_{q+1} at the remainder s_q with g(q) at z = q + 1/2.", + "blocked_by": "No closed form for s_q or g; the comparison needs third-order information on the implicit maximizer." + }, + { + "question": "For the selected #6030 joint application of #6769, does the minimizing u of the strictification test (10) sit at a kink u = tau_m - t of N(t,t+u)?", + "why_it_matters": "If P_x is a positive moment sum n_r r^x, the left side of (10) is convex in u with convex kinks (PROOF.md section 5, conditional remark). A solver that looks only for stationary points of one branch could then miss the optimum.", + "first_step": "Read the joint application linked from #6769, scan u over its exact directed moment intervals, and report whether the minimum lies at a threshold.", + "blocked_by": "The exact directed moments of that application, the moment form of P_x in #4433/#4480, and the complete outer consumer." + }, + { + "question": "Is tau_m(t) increasing in t for each fixed m?", + "why_it_matters": "The certified table suggests it, which would make the first switch point monotone in the exponent.", + "first_step": "Differentiate rho_m(sigma; t) = 1 implicitly in t, using the envelope formula for the sigma-slope.", + "blocked_by": "Needs the t-derivative of the maximizing remainder s_q, which has no closed form." + } + ] +} diff --git a/research/net-split-quotient-staircase/VERIFY.json b/research/net-split-quotient-staircase/VERIFY.json new file mode 100644 index 0000000000..510265553d --- /dev/null +++ b/research/net-split-quotient-staircase/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": 300, + "checks": "Ratio monotonicity grid, envelope slopes and kinks, enclosure-certified tie brackets for 150 (t,q) pairs with window and theta<1/2 tests, float brute-force staircase, and rejection controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "Same checks under optimized Python; no assert-dependent acceptance." + } + ] +} diff --git a/research/net-split-quotient-staircase/verify.py b/research/net-split-quotient-staircase/verify.py new file mode 100644 index 0000000000..e4ecda7de3 --- /dev/null +++ b/research/net-split-quotient-staircase/verify.py @@ -0,0 +1,425 @@ +#!/usr/bin/env python3 +"""Verifier for the best-quotient staircase of the sharp net splitting tax. + +Standard library only; no files are read or written. Every check prints into +one JSON receipt and the command exits nonzero on the first failure. + +Notation (see PROOF.md). For 01 and a real q>0, + F_q(s) = (q + s^t - (q+s)^t) / (q+s)^sigma (0 <= s <= 1), + g_sigma(q) = max_s F_q(s), + H_q(s) = t q s^(t-1) + (t-sigma) s^t - sigma q + (sigma-t)(q+s)^t, + a = t^(1/(1-t)), W(x) = (x+a)^t - a^t, + zeta(x) = (x - t W(x)) / (x - W(x)). +The unique maximizing remainder s_q solves H_q(s)=0 (published in PR #6769). +For integer q>=1 the tie threshold tau_q is the unique sigma with +g_sigma(q) = g_sigma(q+1). + +Checks + A. exact t=1/2 closed form of zeta and the #6769 attaining family; + B. float grid: the ratio g_sigma(q)/g_sigma(q') increases in sigma; the + envelope slope -log(q+s_q), the convex kinks at the thresholds and the + convexity of log N in sigma agree with finite differences; + C. enclosure table: for five rational t and q<=Q, a tiny sigma interval + around tau_q with rho_q<1 at its left end and rho_q>1 at its right end, + the window zeta(q+1) < tau_q < zeta(q), and zeta(q+1/2) < tau_q; + D. float brute force: the best integer quotient over 1..Qmax matches the + staircase read from the thresholds; + E. rejection controls: the false claims tau_q < zeta(q+1/2), and tau_q + outside its window, fail the enclosure test, and a nearest-integer + witness is certified. + +The enclosure arithmetic widens every exp/ln result by a relative 4e-70 and +treats the 100-digit rounding of + - * / as exact. Every inequality it +certifies has a relative margin above 1e-15 (reported in the receipt), so the +omitted rounding (relative 1e-98) cannot change a verdict. It relies on the +documented correct rounding of Decimal.exp and Decimal.ln. +""" + +import json +import math +import sys +from decimal import Decimal, getcontext + +getcontext().prec = 100 +D = Decimal +MARGIN = D("4e-70") + +T_LIST = ["0.1", "0.25", "0.5", "0.75", "0.9"] +Q_MAX_TABLE = 30 +FLOAT_Q_MAX = 200 + + +class Fail(Exception): + pass + + +def need(cond, msg): + if not cond: + raise Fail(msg) + + +# ---------------------------------------------------------------- floats +def f_h(t, sig, q, s): + return (t * q * s ** (t - 1) + (t - sig) * s**t - sig * q + + (sig - t) * (q + s) ** t) + + +def f_s(t, sig, q): + lo, hi = 1e-18, 1.0 + for _ in range(120): + mid = 0.5 * (lo + hi) + if f_h(t, sig, q, mid) > 0: + lo = mid + else: + hi = mid + return 0.5 * (lo + hi) + + +def f_g(t, sig, q): + s = f_s(t, sig, q) + return (q + s**t - (q + s) ** t) / (q + s) ** sig + + +def f_zeta(t, x): + a = t ** (1.0 / (1.0 - t)) + w = (x + a) ** t - a**t + return (x - t * w) / (x - w) + + +def f_z_of_sigma(t, sig): + a = t ** (1.0 / (1.0 - t)) + lo, hi = 1e-9, 1e13 + for _ in range(400): + mid = 0.5 * (lo + hi) + if (sig - t) * ((mid + a) ** t - a**t) - (sig - 1) * mid > 0: + lo = mid + else: + hi = mid + return 0.5 * (lo + hi) + + +def f_tau(t, q): + lo, hi = f_zeta(t, q + 1), f_zeta(t, q) + for _ in range(120): + mid = 0.5 * (lo + hi) + if f_g(t, mid, q) > f_g(t, mid, q + 1): + hi = mid + else: + lo = mid + return 0.5 * (lo + hi) + + +# ------------------------------------------------------- enclosures (Decimal) +def pw(x, e): + """Enclosure of x**e for Decimals x>0 and e.""" + v = (e * x.ln()).exp() + m = v * MARGIN + return (v - m, v + m) + + +def h_enc(t, q, sig, s): + """Interval for H_q(s) at an exact Decimal s in (0,1).""" + p1 = pw(s, t - 1) + p2 = pw(s, t) + p3 = pw(q + s, t) + c1 = t * q + c2 = t - sig + c4 = sig - t + lo = c1 * p1[0] + c2 * p2[1] - sig * q + c4 * p3[0] + hi = c1 * p1[1] + c2 * p2[0] - sig * q + c4 * p3[1] + return (lo, hi) + + +def h_mid(t, q, sig, s): + return (t * q * (((t - 1) * s.ln()).exp()) + (t - sig) * ((t * s.ln()).exp()) + - sig * q + (sig - t) * ((t * (q + s).ln()).exp())) + + +def dh_mid(t, q, sig, s): + return (-t * (1 - t) * q * (((t - 2) * s.ln()).exp()) + + t * (sig - t) * ((((t - 1) * (q + s).ln()).exp()) + - (((t - 1) * s.ln()).exp()))) + + +def s_hat(t, q, sig): + s = D(repr(f_s(float(t), float(sig), q))) + for _ in range(7): + s = s - h_mid(t, q, sig, s) / dh_mid(t, q, sig, s) + return s + + +def g_enc(t, q, sig): + """Rigorous (lo, hi) for g_sigma(q), q a positive integer.""" + s = s_hat(t, q, sig) + need(D(0) < s < D(1), "maximizer outside (0,1)") + for w in (D("1e-40"), D("1e-30"), D("1e-20"), D("1e-12")): + s1, s2 = s - w, s + w + if (h_enc(t, q, sig, s1)[0] > 0) and (h_enc(t, q, sig, s2)[1] < 0): + break + else: + raise Fail("could not certify a sign change of H bracketing s_q") + x = q + s + num_lo = q + pw(s, t)[0] - pw(x, t)[1] + need(num_lo > 0, "numerator lower bound not positive") + g_lo = num_lo / pw(x, sig)[1] + num_hi = q + pw(s2, t)[1] - pw(q + s1, t)[0] + g_hi = num_hi / pw(q + s1, sig)[0] + need(g_lo <= g_hi, "inverted enclosure of g") + return (g_lo, g_hi) + + +def rho_enc(t, q, sig): + a = g_enc(t, q, sig) + b = g_enc(t, q + 1, sig) + return (a[0] / b[1], a[1] / b[0]) + + +def a_enc(t): + return pw(t, D(1) / (D(1) - t)) + + +def zeta_enc(t, x): + a = a_enc(t) + p_lo = pw(x + a[0], t)[0] + p_hi = pw(x + a[1], t)[1] + at_lo = pw(a[0], t)[0] + at_hi = pw(a[1], t)[1] + w_lo, w_hi = p_lo - at_hi, p_hi - at_lo + den_lo, den_hi = x - w_hi, x - w_lo + need(den_lo > 0, "x - W(x) not positive") + num_lo, num_hi = x - t * w_hi, x - t * w_lo + return (num_lo / den_hi, num_hi / den_lo) + + +def dec(x, digits=16): + return D(format(x, "." + str(digits) + "f")) + + +# --------------------------------------------------------------------- A +def check_a(): + # t = 1/2: zeta(x) = 1 + 1/(sqrt(4x+1) - 1) (closed form), and the #6769 + # family z = n(n+1) at sigma = 1 + 1/(2n). + half = D("0.5") + worst = D(0) + for n in range(1, 17): + x = D(n * (n + 1)) + z = zeta_enc(half, x) + exact = D(1) + D(1) / (D(2 * n)) + need(z[0] - D("1e-60") <= exact <= z[1] + D("1e-60"), + "zeta(n(n+1)) != 1+1/(2n) at t=1/2, n=%d" % n) + worst = max(worst, z[1] - z[0]) + for x in (D("1.45"), D("2.5"), D("7.25"), D("30.5")): + closed = D(1) + D(1) / ((D(4) * x + D(1)).sqrt() - D(1)) + z = zeta_enc(half, x) + need(z[0] - D("1e-60") <= closed <= z[1] + D("1e-60"), + "t=1/2 closed form of zeta fails at x=%s" % x) + return {"family_n": 16, "max_enclosure_width": "%.3e" % float(worst)} + + +# --------------------------------------------------------------------- B +def check_b(): + ts = [0.1, 0.25, 0.5, 0.75, 0.9] + pairs = [(1, 2), (1, 3), (2, 3), (3, 4), (5, 9), (10, 11), (30, 31), (7, 40)] + sigmas = [1.001, 1.01, 1.05, 1.1, 1.3, 1.5, 2.0, 3.0, 5.0, 9.0] + n = 0 + for t in ts: + for q, qp in pairs: + prev = None + for sig in sigmas: + r = f_g(t, sig, q) / f_g(t, sig, qp) + if prev is not None: + need(r > prev, "ratio not increasing t=%s q=%d q'=%d" % (t, q, qp)) + prev = r + n += 1 + return {"ratio_evaluations": n} + + +def check_b2(): + """Envelope slope: d/dsigma log g_sigma(q) = -log(q + s_q) (PROOF.md, section 5).""" + n = 0 + worst = 0.0 + for t in (0.1, 0.5, 0.9): + for q in (1, 2, 7, 25): + for sig in (1.05, 1.3, 2.0, 4.0): + h = 1e-5 + num = math.log(f_g(t, sig + h, q)) - math.log(f_g(t, sig - h, q)) + slope = num / (2 * h) + exact = -math.log(q + f_s(t, sig, q)) + err = abs(slope - exact) + worst = max(worst, err) + need(err < 1e-7, "envelope slope mismatch t=%s q=%d sigma=%s" % (t, q, sig)) + n += 1 + # one-sided slopes at a tie: left branch q+1, right branch q (convex kink) + kinks = 0 + for t in (0.1, 0.5, 0.9): + for q in (1, 2, 3, 6): + tau = f_tau(t, q) + h = 1e-6 + + def log_n(sig): + return max(math.log(f_g(t, sig, k)) for k in range(1, 40)) + + right = (log_n(tau + 2 * h) - log_n(tau + h)) / h + left = (log_n(tau - h) - log_n(tau - 2 * h)) / h + exp_right = -math.log(q + f_s(t, tau, q)) + exp_left = -math.log(q + 1 + f_s(t, tau, q + 1)) + need(abs(right - exp_right) < 2e-4, "right slope mismatch at tau t=%s q=%d" % (t, q)) + need(abs(left - exp_left) < 2e-4, "left slope mismatch at tau t=%s q=%d" % (t, q)) + need(right - left > 1e-3, "no convex kink at tau t=%s q=%d" % (t, q)) + kinks += 1 + # log N is convex in sigma: second differences are nonnegative + convex_pts = 0 + for t in (0.1, 0.25, 0.5, 0.75, 0.9): + h = 1e-3 + + def log_n2(sig): + return max(math.log(f_g(t, sig, k)) for k in range(1, 80)) + + sig = f_zeta(t, 60.0) + while sig < 3.0: + d2 = log_n2(sig + h) - 2 * log_n2(sig) + log_n2(sig - h) + need(d2 > -1e-11, "log N not convex at t=%s sigma=%.5f" % (t, sig)) + convex_pts += 1 + sig += 0.037 + return {"slope_checks": n, "max_abs_error": "%.2e" % worst, + "kinks_checked": kinks, "convexity_points": convex_pts} + + +# --------------------------------------------------------------------- C +def certify_pair(t_str, q): + t = D(t_str) + tf = float(t) + tau = f_tau(tf, q) + for delta in (1e-12, 1e-11, 1e-10, 1e-9, 1e-8): + s_lo, s_hi = dec(tau - delta), dec(tau + delta) + r_lo = rho_enc(t, q, s_lo) + r_hi = rho_enc(t, q, s_hi) + if r_lo[1] < 1 < r_hi[0]: + break + else: + raise Fail("no certified tie bracket for t=%s q=%d" % (t_str, q)) + z_up = zeta_enc(t, D(q)) + z_dn = zeta_enc(t, D(q + 1)) + z_half = zeta_enc(t, D(q) + D("0.5")) + window = (z_dn[1] < s_lo) and (s_hi < z_up[0]) + below_half = z_half[1] < s_lo + margins = [float(1 - r_lo[1]), float(r_hi[0] - 1), + float((s_lo - z_dn[1]) / s_lo), float((z_up[0] - s_hi) / s_hi), + float((s_lo - z_half[1]) / s_lo)] + return {"t": t_str, "q": q, "tau": tau, "delta": delta, "window": window, + "below_half": below_half, "margins": margins, "s_lo": s_lo, + "s_hi": s_hi} + + +def check_c(): + rows = [] + min_margin = 1.0 + max_delta = 0.0 + for t_str in T_LIST: + for q in range(1, Q_MAX_TABLE + 1): + r = certify_pair(t_str, q) + need(r["window"], "window failed t=%s q=%d" % (t_str, q)) + need(r["below_half"], "zeta(q+1/2) < tau_q failed t=%s q=%d" % (t_str, q)) + min_margin = min(min_margin, min(r["margins"])) + max_delta = max(max_delta, r["delta"]) + rows.append(r) + taus = [r["tau"] for r in rows if r["t"] == t_str] + need(all(a > b for a, b in zip(taus, taus[1:])), "tau_q not decreasing t=%s" % t_str) + need(min_margin > 1e-15, "certified margin too small") + table = {} + for t_str in T_LIST: + table[t_str] = { + str(r["q"]): "%.10f" % r["tau"] + for r in rows + if r["t"] == t_str and q_in(r["q"]) + } + offsets = {} + for t_str in T_LIST: + tf = float(D(t_str)) + offsets[t_str] = { + str(r["q"]): round(f_z_of_sigma(tf, r["tau"]) - r["q"], 6) + for r in rows + if r["t"] == t_str and q_in(r["q"]) + } + return {"pairs_certified": len(rows), "min_relative_margin": "%.3e" % min_margin, + "max_bracket_half_width": max_delta, "tau": table, "theta": offsets} + + +def q_in(q): + return q in (1, 2, 3, 5, 10, 20, 30) + + +# --------------------------------------------------------------------- D +def check_d(): + checked = 0 + for t in (0.1, 0.25, 0.5, 0.75, 0.9): + qcap = 40 + taus = {m: f_tau(t, m) for m in range(1, qcap + 1)} + top = f_zeta(t, qcap - 5) + lo_sig = f_zeta(t, 0.4) + grid = [top + (lo_sig - top) * (k + 0.5) / 60.0 for k in range(60)] + for sig in grid: + gs = [f_g(t, sig, q) for q in range(1, FLOAT_Q_MAX + 1)] + best = max(range(len(gs)), key=lambda i: gs[i]) + 1 + predicted = 1 + sum(1 for m in range(1, qcap + 1) if taus[m] > sig) + need(best == predicted, + "staircase mismatch t=%s sigma=%.9f best=%d predicted=%d" + % (t, sig, best, predicted)) + checked += 1 + return {"sigma_points": checked, "q_range": FLOAT_Q_MAX} + + +# --------------------------------------------------------------------- E +def check_e(): + out = {} + # (1) the false claim "tie at z >= q+1/2" must fail the enclosure test + t = D("0.5") + bad = 0 + for q in (1, 2, 5, 12): + r = certify_pair("0.5", q) + false_claim = r["s_hi"] < zeta_enc(t, D(q) + D("0.5"))[0] + need(not false_claim, "false 'tie before z=q+1/2 is wrong' claim passed") + outside = r["s_hi"] < zeta_enc(t, D(q + 1))[0] or r["s_lo"] > zeta_enc(t, D(q))[1] + need(not outside, "bracket outside its window") + bad += 2 + out["rejected_false_claims"] = bad + # (2) nearest-integer witness: z = 1.45 rounds to 1, but quotient 2 is + # strictly better at that sigma (t = 1/2 and t = 1/4). + wit = {} + for t_str in ("0.5", "0.25"): + tt = D(t_str) + z = zeta_enc(tt, D("1.45")) + sig = dec(float((z[0] + z[1]) / 2)) + r = rho_enc(tt, 1, sig) + need(r[1] < 1, "nearest-integer witness failed t=%s" % t_str) + wit[t_str] = {"sigma": str(sig), "rho_upper": "%.6f" % float(r[1])} + out["nearest_integer_witness_z_1.45"] = wit + # (3) a mutated rho (the smaller quotient given the larger remainder cap) + # would not be increasing: the ratio g(q+1)/g(q) is decreasing. + t = 0.5 + vals = [f_g(t, s, 2) / f_g(t, s, 1) for s in (1.2, 1.5, 2.0, 3.0)] + need(all(a > b for a, b in zip(vals, vals[1:])), "inverse ratio control failed") + out["inverse_ratio_decreasing"] = True + return out + + +def main(): + receipt = {"status": "FAIL"} + try: + receipt["A_closed_forms"] = check_a() + receipt["B_ratio_grid"] = check_b() + receipt["B2_envelope_slope"] = check_b2() + receipt["C_enclosure_table"] = check_c() + receipt["D_staircase_bruteforce"] = check_d() + receipt["E_controls"] = check_e() + receipt["status"] = "PASS_NET_SPLIT_QUOTIENT_STAIRCASE" + except Fail as exc: + receipt["failure"] = str(exc) + print(json.dumps(receipt, indent=1, sort_keys=True)) + return 1 + print(json.dumps(receipt, indent=1, sort_keys=True)) + return 0 + + +if __name__ == "__main__": + sys.exit(main())