From 74596e7b578612c4da5f10e117f430e56578151c Mon Sep 17 00:00:00 2001 From: Cinna Davis <1337isnot1337@users.noreply.github.com> Date: Tue, 13 Oct 2026 19:15:48 -0500 Subject: [PATCH 1/4] Add exact helper470 same-slot profile audit --- .../bit-inplace-retirement-seed11/CLAIM.json | 33 +++ .../bit-inplace-retirement-seed11/README.md | 152 +++++++++++ .../bit-inplace-retirement-seed11/RESULT.json | 86 ++++++ .../SOURCES.json | 42 +++ .../bit-inplace-retirement-seed11/TASK.json | 60 +++++ .../bit-inplace-retirement-seed11/VERIFY.json | 23 ++ .../bit-inplace-retirement-seed11/verify.py | 254 ++++++++++++++++++ 7 files changed, 650 insertions(+) create mode 100644 research/bit-inplace-retirement-seed11/CLAIM.json create mode 100644 research/bit-inplace-retirement-seed11/README.md create mode 100644 research/bit-inplace-retirement-seed11/RESULT.json create mode 100644 research/bit-inplace-retirement-seed11/SOURCES.json create mode 100644 research/bit-inplace-retirement-seed11/TASK.json create mode 100644 research/bit-inplace-retirement-seed11/VERIFY.json create mode 100644 research/bit-inplace-retirement-seed11/verify.py diff --git a/research/bit-inplace-retirement-seed11/CLAIM.json b/research/bit-inplace-retirement-seed11/CLAIM.json new file mode 100644 index 0000000000..1e6f96b957 --- /dev/null +++ b/research/bit-inplace-retirement-seed11/CLAIM.json @@ -0,0 +1,33 @@ +{ + "run": 3, + "assignment_seed": 11, + "track": "bit supplier", + "base_commit": "bce54fb3f895cbe5cd4c0eb477c3afeed100190f", + "started_utc": "2026-10-13T23:41:05.977699+00:00", + "planned_finish_utc": "2026-10-14T00:31:05.977699+00:00", + "verification_start_utc": "2026-10-14T00:18:35.977699+00:00", + "status": "orientation", + "previous_completed_pr": 1373, + "worktree": "/home/cinna/int-bound/sprint3-bit-seed11", + "candidate_tasks": [ + "Audit one paid recursive bit-profile mechanism after checking which stage-number and boundary classes have already been exhausted.", + "Investigate one explicit helper-mixing boundary implication beyond inherited H2, with every source access and restoration charged.", + "Investigate one precision or decoder invoice change that could alter the paid bit bill, rather than only reducing scalar ADD count." + ], + "scope_selected": true, + "required_next_action": "Inspect relevant open PR heads, active claims and closed search classes; select and locally claim one new narrow object. Keep final quarter for verification. Do not repeat quad17 or the completed GL3 branch.", + "object": "PR1256 helper470 local delta +H1+H5-H7, priced with in-place width8->7 shrink and all returned idle rank, fixed width64. All old remainders r=0..56; actual planning classes2,4,6.", + "method": "Derive exact paid histogram/call-count changes; price fixed selected exponent with two rational engines; prove a uniform concavity/power inequality rather than extrapolating finite replay.", + "deliverable": "Scoped negative result or counterexample for this complete same-slot bill, exact certificate, controls and explicit distinction from two-slot relocation and full-frame closure.", + "candidates": [ + "Helper470 in-place shrinking: complete returned-idle bill (chosen).", + "Helper470 native replay/full-frame closure (already PR1302).", + "Semantic zero-frame D application to PR1122 (already PR1311)." + ], + "predecessors": { + "1256": "d6d5a994fcdcd8d04ec439ff988daa8f37b17ece", + "1302": "0cc5db33b0999a7d3333383a855667f6f8cbda88", + "1311": "a2875c1834b9c9ef42a84eda4890d5462cc98fa5" + }, + "coordination": "No pinned sprint issue; local claim under donor fallback. Complete live semantic overlap check follows before expanded implementation." +} diff --git a/research/bit-inplace-retirement-seed11/README.md b/research/bit-inplace-retirement-seed11/README.md new file mode 100644 index 0000000000..21e826749d --- /dev/null +++ b/research/bit-inplace-retirement-seed11/README.md @@ -0,0 +1,152 @@ +# Same-slot helper470 retirement raises the complete frozen bit bill + +**Status: scoped negative result. No construction or new exponent is claimed.** + +This note completes one missing cost calculation around the finite helper470 +exception in PR #1256. It asks whether shrinking its existing width-eight slot +to width seven, then returning the freed rank to that slot's idle remainder, +improves the complete paid bit profile. The answer is no for every feasible +old remainder in the frozen width-64 interface. For the three idle classes in +the pinned selected profile, exact interval replay shows that the complete +moment bill increases, including the inherited residue surcharge. + +The question is distinct from the two-slot displacement priced in PR #1256. +That relaxation spends eight coordinates in a second slot and can lower the +raw moment at remainders 2, 4, and 6. It is also distinct from PR #1302's +native replay and full-frame closure audit, and from PR #1043's earlier +source-boundary deletion with a hosted invoice. This result only prices the +same-slot profile change. + +## Frozen inputs and complete profile + +The exact base is `bce54fb3f895cbe5cd4c0eb477c3afeed100190f`. The four live +inputs and their Git blob and SHA256 pins are in [SOURCES.json](SOURCES.json). +The verifier checks those SHA256 values, the compressed word receipt and its +uncompressed content receipt. The selected nine-stage bit endpoint is +`a = 1733427039589844234749/10^24`; it comes from the pinned `EXPECTED.json`. + +The pinned local paid histogram is +`p = {1:1323, 2:1342, 3:79, 4:44, 5:102, 6:11, 7:19}`. The frozen hosting +remainder, parsed from the pinned `fastc.py`, is +`R = {2:13920, 4:14208, 6:14208, 7:21312, 42:288}`. Thus the complete +nine-stage profile is `H = 288 p + R`, with 904896 calls, rank mass 1808352, +and deficit 10272 from `64*28416`. The moment engine prices + +```text +M(H,a) = sum_r H[r] * r * (64/r)^a / (64*28416) + + 32*64*sum_r(H[r])/(10^16*28416) * 64^a. +``` + +The second term is the inherited residue envelope in the pinned source. The +calculation takes its existing coefficient as given and charges its change +when the call count changes. + +## Same-slot delta and proof + +Shrinking the width-eight helper to seven changes its paid local profile by +`e1 + e5 - e7`. Returning one unit of unused width to an old idle remainder +`r > 0` changes that term by `e_(r+1) - e_r`. Hence + +```text +Delta_r = e1 + e5 - e7 + e_(r+1) - e_r, 1 <= r <= 56. +Delta_0 = 2 e1 + e5 - e7. +``` + +For every `0 < a < 1`, define `g_a(t)=t*(64/t)^a=64^a*t^(1-a)` for `t>0` +and `g_a(0)=0`. Dividing the raw moment change by `64^a` gives + +```text +Q_r = 1 + 5^(1-a) - 7^(1-a) + (r+1)^(1-a) - r^(1-a) + = integral_0^1 t^(-a) dt - integral_5^7 t^(-a) dt + + integral_r^(r+1) t^(-a) dt. +``` + +On `0 <= r <= 56`, the last integral is at least `57^(-a)` and the middle +integral is at most `2*5^(-a)`. Therefore + +```text +Q_r >= 1/(1-a) + 57^(-a) - 2*5^(-a) > 0. +``` + +For the strict inequality, AM-GM reduces it to +`1/(1-a) > (57/25)^a`. This follows from `-ln(1-a)>a` and +`ln(57/25)<1` (since `57/25 < 8/3 < e`). Thus the raw moment strictly +increases throughout the stated domain. For `r>0`, the complete profile adds +one call; for `r=0`, it adds two. The inherited surcharge consequently also +increases. The complete bill is strictly worse for every `0= 1, "log input must be positive") + if n == 1: + return F(0), F(0) + + def atanh_log(z): + s = F(0) + for j in range(LOG_TERMS): + s += 2 * z ** (2 * j + 1) / (2 * j + 1) + tail = 2 * z ** (2 * LOG_TERMS + 1) / ((2 * LOG_TERMS + 1) * (1 - z * z)) + return s, s + tail + + k = n.bit_length() - 1 + u = F(n, 1 << k) + z = (u - 1) / (u + 1) + ln2 = atanh_log(F(1, 3)) + lnu = atanh_log(z) + return k * ln2[0] + lnu[0], k * ln2[1] + lnu[1] + + +def exp_pos_interval(xl, xu): + """Exact positive-exponential interval; geometric tail after Taylor sum.""" + check(0 <= xl <= xu < F(1, 10), "positive exponential range") + + def bounds(x): + s = t = F(1) + for j in range(1, EXP_TERMS + 1): + t *= x / j + s += t + nxt = t * x / (EXP_TERMS + 1) + tail = nxt / (1 - x / (EXP_TERMS + 2)) + return s, s + tail + + return bounds(xl)[0], bounds(xu)[1] + + +def exp_neg_point_interval(x): + """Exact alternating-series interval for exp(-x), 0 <= x < 1/10.""" + check(0 <= x < F(1, 10), "negative exponential range") + + def partial(terms): + s = t = F(1) + for j in range(1, terms): + t *= -x / j + s += t + return s + + # For a decreasing alternating series, even term count ends below, odd above. + return partial(EXP_TERMS), partial(EXP_TERMS - 1) + + +def power_q_interval(n, alpha): + """Exact enclosure of n^(1-alpha); zero has its separate exact value.""" + if n == 0: + return F(0), F(0) + ll, lu = ln_interval(n) + lo = exp_neg_point_interval(alpha * lu)[0] + hi = exp_neg_point_interval(alpha * ll)[1] + return n * lo, n * hi + + +def add_delta(profile, delta): + ans = Counter(profile) + ans.update(delta) + return Counter({r: n for r, n in ans.items() if n}) + + +def raw_sum_interval(profile, alpha): + lo = hi = F(0) + for r, count in profile.items(): + pl, pu = power_q_interval(r, alpha) + lo += count * pl + hi += count * pu + return lo, hi + + +def moment_interval(profile, alpha): + """Parent moment engine's frozen expression with its inherited bad term.""" + lo, hi = raw_sum_interval(profile, alpha) + ln_m = ln_interval(M) + ml, mu = exp_pos_interval(alpha * ln_m[0], alpha * ln_m[1]) + calls = sum(profile.values()) + scale = F(1, M * W) + return (lo * ml * scale + BAD_SCALE * calls * ml, + hi * mu * scale + BAD_SCALE * calls * mu) + + +def signed_sum_interval(terms, alpha): + lo = hi = F(0) + for rank, coefficient in terms.items(): + pl, pu = power_q_interval(rank, alpha) + if coefficient >= 0: + lo += coefficient * pl + hi += coefficient * pu + else: + lo += coefficient * pu + hi += coefficient * pl + return lo, hi + + +def delta_for_remainder(r): + # Shrink width 8 to 7 in place, and return one rank to this idle remainder. + d = Counter({1: 1, 5: 1, 7: -1}) + d[r + 1] += 1 + if r: + d[r] -= 1 + return Counter({rank: n for rank, n in d.items() if n}) + + +def two_slot_relaxation(r): + # PR1256's distinct favorable relaxation: move width 7 between two slots. + d = Counter({1: 1, 5: 1, 7: -2, r + 8: 1, r: -1}) + return Counter({rank: n for rank, n in d.items() if n}) + + +def decimal_interval(interval): + lo, hi = interval + return [str((lo.numerator * PRINT_SCALE) // lo.denominator), + str(-((-hi.numerator * PRINT_SCALE) // hi.denominator))] + + +def load_inputs(): + raw = {} + for path, expected_sha in PINS.items(): + data = (ROOT / path).read_bytes() + check(hashlib.sha256(data).hexdigest() == expected_sha, f"SHA256 pin mismatch: {path}") + raw[path] = data + exp_path = "research/e8-bit-p111-tuned/tune/EXPECTED.json" + expected = json.loads(raw[exp_path]) + moment_src = raw["research/e8-bit-carrier-skeleton/code/hub/e8-r740-replica32/code/engines/moment.py"].decode() + check("p=F(r*n,m*W)" in moment_src and "32*m*sum(H.values())" in moment_src, + "pinned parent moment and inherited surcharge formulas") + gz_path = "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz" + word_raw = gzip.decompress(raw[gz_path]) + check(hashlib.sha256(raw[gz_path]).hexdigest() == expected["word"]["file_sha256"], "word gzip receipt") + check(hashlib.sha256(word_raw).hexdigest() == expected["word"]["content_sha256"], "word content receipt") + # The paid local histogram and global profile are both frozen source receipts. + local = {int(k): int(v) for k, v in expected["word"]["local_histogram"].items()} + profile = {int(k): int(v) for k, v in expected["nine"]["profile"].items()} + source = ast.parse(raw["research/e8-bit-p111-tuned/tune/fastc.py"].decode()) + remainder = None + for node in ast.walk(source): + if isinstance(node, ast.Assign) and any(isinstance(t, ast.Name) and t.id == "REM" for t in node.targets): + remainder = ast.literal_eval(node.value) + break + check(remainder is not None, "frozen idle remainder declaration") + rebuilt = Counter({r: REPLICAS * n for r, n in local.items()}) + rebuilt.update({int(r): int(n) for r, n in remainder.items()}) + check(dict(rebuilt) == profile, "288 * local profile + pinned remainder mismatch") + check(sum(profile.values()) == 904896, "source child count") + check(sum(r * n for r, n in profile.items()) == 1808352, "source rank mass") + check(M * W - sum(r * n for r, n in profile.items()) == 10272, "source rank deficit") + alpha = F(expected["nine"]["bit_lower"]) + check(0 < alpha < 1, "selected bit exponent domain") + return expected, profile, remainder, alpha + + +def main(): + expected, profile, remainder, alpha = load_inputs() + results = {} + for r in range(57): + uniform = Counter({1: 1, 5: 1, 7: -1}) + uniform[r + 1] += 1 + if r: + uniform[r] -= 1 + q = signed_sum_interval(uniform, alpha) + check(q[0] > 0, f"positive in-place raw moment delta r={r}") + for r in (2, 4, 6): + delta = delta_for_remainder(r) + candidate = add_delta(profile, delta) + check(sum(delta.values()) == 1, f"one added child r={r}") + check(sum(k * v for k, v in delta.items()) == 0, f"rank mass returned r={r}") + check(all(v >= 0 for v in candidate.values()), f"nonnegative candidate histogram r={r}") + base_cost = moment_interval(profile, alpha) + new_cost = moment_interval(candidate, alpha) + observed = (new_cost[0] - base_cost[1], new_cost[1] - base_cost[0]) + direct_raw = signed_sum_interval(delta, alpha) + ml = exp_pos_interval(alpha * ln_interval(M)[0], alpha * ln_interval(M)[1]) + direct = (direct_raw[0] * ml[0] / (M * W) + BAD_SCALE * ml[0], + direct_raw[1] * ml[1] / (M * W) + BAD_SCALE * ml[1]) + check(observed[0] > 0 and direct[0] > 0, f"complete paid bill increases r={r}") + check(observed[0] <= direct[1] and direct[0] <= observed[1], f"independent delta matches full-profile price r={r}") + + omitted_return = signed_sum_interval({1: 1, 5: 1, 7: -1}, alpha) + check(omitted_return[1] < 0, "negative control: omitting returned idle rank looks favorable") + relaxed = signed_sum_interval(two_slot_relaxation(r), alpha) + check(relaxed[1] < 0, f"positive control: distinct PR1256 two-slot relaxation r={r}") + + # Mutation controls: deleting the returned rank or miscounting the new child + # must violate the two exact conservation laws checked above. + bad_return = Counter(delta) + bad_return[r] -= 1 + check(sum(bad_return.values()) != sum(delta.values()), f"control catches omitted return r={r}") + bad_call = Counter(delta) + bad_call[1] -= 1 + check(sum(bad_call.values()) != sum(delta.values()), f"control catches omitted helper child r={r}") + + results[str(r)] = { + "delta_histogram": dict(sorted(delta.items())), + "calls_delta": sum(delta.values()), + "rank_mass_delta": sum(k * v for k, v in delta.items()), + "full_moment_delta_interval_scaled_1e-30": decimal_interval(observed), + "direct_formula_interval_scaled_1e-30": decimal_interval(direct), + "two_slot_relaxation_raw_delta_interval_scaled_1e-30": decimal_interval(relaxed), + } + + # Exact all-remainder argument is written out in README: the interval replay + # independently covers every integer remainder in the fixed width-64 domain. + print(json.dumps({ + "status": "PASS_SAME_SLOT_HELPER470_BILL_INCREASES", + "base_commit": "bce54fb3f895cbe5cd4c0eb477c3afeed100190f", + "selected_bit_exponent": str(alpha), + "inherited_bad_term": "32*64*N/(10^16*28416) * 64^alpha", + "pinned_idle_remainder": {str(k): int(v) for k, v in sorted(remainder.items())}, + "actual_remainder_classes": results, + "uniform_remainders_checked": 57, + "interval_method": f"exact Fraction atanh-log ({LOG_TERMS} terms), alternating/geometric Taylor exp ({EXP_TERMS} terms), signed outward intervals", + "source_profile_calls": sum(profile.values()), + "source_profile_rank_mass": sum(k*v for k,v in profile.items()), + "selected_record_bit_lower": expected["nine"]["bit_lower"], + }, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main() From cca25616db999bb8cb5be6d8c0b5a2c060080945 Mon Sep 17 00:00:00 2001 From: Cinna Davis <1337isnot1337@users.noreply.github.com> Date: Tue, 13 Oct 2026 19:17:05 -0500 Subject: [PATCH 2/4] Record helper470 audit handoff --- research/bit-inplace-retirement-seed11/CLAIM.json | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/research/bit-inplace-retirement-seed11/CLAIM.json b/research/bit-inplace-retirement-seed11/CLAIM.json index 1e6f96b957..f7bb74434d 100644 --- a/research/bit-inplace-retirement-seed11/CLAIM.json +++ b/research/bit-inplace-retirement-seed11/CLAIM.json @@ -6,7 +6,7 @@ "started_utc": "2026-10-13T23:41:05.977699+00:00", "planned_finish_utc": "2026-10-14T00:31:05.977699+00:00", "verification_start_utc": "2026-10-14T00:18:35.977699+00:00", - "status": "orientation", + "status": "submitted", "previous_completed_pr": 1373, "worktree": "/home/cinna/int-bound/sprint3-bit-seed11", "candidate_tasks": [ @@ -15,7 +15,7 @@ "Investigate one precision or decoder invoice change that could alter the paid bit bill, rather than only reducing scalar ADD count." ], "scope_selected": true, - "required_next_action": "Inspect relevant open PR heads, active claims and closed search classes; select and locally claim one new narrow object. Keep final quarter for verification. Do not repeat quad17 or the completed GL3 branch.", + "required_next_action": "Final verification: rerun the registered exact replay and refresh the PR head before handing off.", "object": "PR1256 helper470 local delta +H1+H5-H7, priced with in-place width8->7 shrink and all returned idle rank, fixed width64. All old remainders r=0..56; actual planning classes2,4,6.", "method": "Derive exact paid histogram/call-count changes; price fixed selected exponent with two rational engines; prove a uniform concavity/power inequality rather than extrapolating finite replay.", "deliverable": "Scoped negative result or counterexample for this complete same-slot bill, exact certificate, controls and explicit distinction from two-slot relocation and full-frame closure.", @@ -29,5 +29,9 @@ "1302": "0cc5db33b0999a7d3333383a855667f6f8cbda88", "1311": "a2875c1834b9c9ef42a84eda4890d5462cc98fa5" }, - "coordination": "No pinned sprint issue; local claim under donor fallback. Complete live semantic overlap check follows before expanded implementation." + "coordination": "No pinned sprint issue existed; the local claim was used. Submitted focused research note as PR #1401.", + "result": "For the frozen width-64 helper470 same-slot change, the complete bit bill strictly increases for every feasible old remainder r=0..56; exact full-profile intervals are positive at the actual classes 2,4,6. The separate PR1256 two-slot relaxation remains favorable. No new kappa.", + "result_path": "research/bit-inplace-retirement-seed11/README.md", + "result_url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1401", + "live_overlap_refresh": "865 open PRs reviewed; exact helper470 hits were PRs 1043, 1048, 1179, 1256, 1271 and 1302. PR1043 source-boundary invoice, PR1048 whole-profile pricing, PR1256 two-slot construction and PR1302 native/full-frame audit are credited and have distinct scopes." } From c4f3e9ae15bfc9c358af79bf023ae046961be499 Mon Sep 17 00:00:00 2001 From: Cinna Davis <1337isnot1337@users.noreply.github.com> Date: Tue, 13 Oct 2026 19:20:02 -0500 Subject: [PATCH 3/4] Clarify fixed-endpoint pricing scope --- research/bit-inplace-retirement-seed11/README.md | 10 ++++++---- research/bit-inplace-retirement-seed11/SOURCES.json | 6 ++++++ 2 files changed, 12 insertions(+), 4 deletions(-) diff --git a/research/bit-inplace-retirement-seed11/README.md b/research/bit-inplace-retirement-seed11/README.md index 21e826749d..a90e7d3ccd 100644 --- a/research/bit-inplace-retirement-seed11/README.md +++ b/research/bit-inplace-retirement-seed11/README.md @@ -144,9 +144,11 @@ are from PR #1256. PR #1302 (head full-frame closure audit; this note does not repeat those checks. The tuned bit word and its pipeline lineage are credited to PR #555 and its cited predecessors in the pinned source README. PR #1048 (head -`07730cd8302c378607259a9ad0efb73e0b57a2f2`) established exact pricing of the -complete paid profile and the linear objective; this work independently -replays that objective with rational intervals for this specific return-one -delta and its inherited call surcharge. Prepared by Cinna Davis +`07730cd8302c378607259a9ad0efb73e0b57a2f2`) proposed a general fixed-exponent +profile-ordering claim, which the selected review rejects with an exact +counterexample. This audit does not use that claim: it directly compares the +same frozen moment at one pinned exponent using rational intervals, including +the inherited call surcharge. The selected review is pinned as provenance in +SOURCES.json. Prepared by Cinna Davis (@1337isnot1337) with substantial OpenAI Codex assistance in source review, derivation, exact interval code, replay, and writing. New work is Apache-2.0. diff --git a/research/bit-inplace-retirement-seed11/SOURCES.json b/research/bit-inplace-retirement-seed11/SOURCES.json index 41392ad8a5..dffa9b5222 100644 --- a/research/bit-inplace-retirement-seed11/SOURCES.json +++ b/research/bit-inplace-retirement-seed11/SOURCES.json @@ -37,6 +37,12 @@ "usage": "input", "git_blob": "ec050c0139109d3033933fa137aa83a0f14fe5cc", "sha256": "ae51f1fbb22b8c8dac8aab787c798361f6aa5d4e1fefb29e43d0197899d4eab5" + }, + { + "path": "docs/research/community-batch1099-review.md", + "usage": "provenance", + "git_blob": "6cb6ec061a071a06a2d18cd4dc3e9a2b05d28099", + "sha256": "7e76d2c38e5fce30587835b7251df1430488ae4dd372611ef69a3f03f476b6cb" } ] } From 93db17f79703329cc4102d62add0f5290edd3775 Mon Sep 17 00:00:00 2001 From: Cinna Davis Date: Wed, 14 Oct 2026 02:04:23 -0500 Subject: [PATCH 4/4] Correct PR #1401 uniform integral identity and positivity bound Restore the derivative factor (1-a) in Q_r's integral representation, propagate it through the lower bound, and give the AM-GM and logarithmic strict-positivity argument. Preserve the selected-moment certificate and frozen exact replay; 57-remainder test remains unchanged. --- .../bit-inplace-retirement-seed11/README.md | 20 ++++++++++++------- 1 file changed, 13 insertions(+), 7 deletions(-) diff --git a/research/bit-inplace-retirement-seed11/README.md b/research/bit-inplace-retirement-seed11/README.md index a90e7d3ccd..4edfc89f4e 100644 --- a/research/bit-inplace-retirement-seed11/README.md +++ b/research/bit-inplace-retirement-seed11/README.md @@ -57,20 +57,26 @@ and `g_a(0)=0`. Dividing the raw moment change by `64^a` gives ```text Q_r = 1 + 5^(1-a) - 7^(1-a) + (r+1)^(1-a) - r^(1-a) - = integral_0^1 t^(-a) dt - integral_5^7 t^(-a) dt - + integral_r^(r+1) t^(-a) dt. + = (1-a) * [integral_0^1 t^(-a) dt - integral_5^7 t^(-a) dt + + integral_r^(r+1) t^(-a) dt]. ``` +The factor `1-a` is essential: the derivative of `t^(1-a)` is +`(1-a)*t^(-a)`. The integrals converge even at `r=0` because `a<1`. On `0 <= r <= 56`, the last integral is at least `57^(-a)` and the middle -integral is at most `2*5^(-a)`. Therefore +integral is at most `2*5^(-a)`. Multiplying the integral bound by the +positive factor gives ```text -Q_r >= 1/(1-a) + 57^(-a) - 2*5^(-a) > 0. +Q_r >= (1-a)*[1/(1-a) + 57^(-a) - 2*5^(-a)] + = 1 + (1-a)*(57^(-a) - 2*5^(-a)) + >= 1 - (1-a)*(57/25)^a > 0. ``` -For the strict inequality, AM-GM reduces it to -`1/(1-a) > (57/25)^a`. This follows from `-ln(1-a)>a` and -`ln(57/25)<1` (since `57/25 < 8/3 < e`). Thus the raw moment strictly +For the penultimate inequality, AM-GM gives +`2*5^(-a) <= 57^(-a) + (57/25)^a`. For the final strict inequality, +`-ln(1-a)>a` and `ln(57/25)<1` (because `57/25 < 8/3 < e`), +so `(1-a)*(57/25)^a < 1`. Thus the raw moment strictly increases throughout the stated domain. For `r>0`, the complete profile adds one call; for `r=0`, it adds two. The inherited surcharge consequently also increases. The complete bill is strictly worse for every `0