diff --git a/research/bit-inplace-retirement-seed11/CLAIM.json b/research/bit-inplace-retirement-seed11/CLAIM.json new file mode 100644 index 0000000000..f7bb74434d --- /dev/null +++ b/research/bit-inplace-retirement-seed11/CLAIM.json @@ -0,0 +1,37 @@ +{ + "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": "submitted", + "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": "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.", + "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 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." +} diff --git a/research/bit-inplace-retirement-seed11/README.md b/research/bit-inplace-retirement-seed11/README.md new file mode 100644 index 0000000000..4edfc89f4e --- /dev/null +++ b/research/bit-inplace-retirement-seed11/README.md @@ -0,0 +1,160 @@ +# 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) + = (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)`. Multiplying the integral bound by the +positive factor gives + +```text +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 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= 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()