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())