Scoped negative result: same-slot helper470 retirement raises the complete bit bill

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."
+}

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<a<1` and every
+feasible old remainder `r` in the fixed width-64 slot.
+
+## Exact replay and controls
+
+`verify.py` independently computes outward rational intervals using exact
+`Fraction` arithmetic: 24-term atanh log bounds, 32-term Taylor exponential
+bounds with explicit tails, then signed interval propagation. It checks all
+57 old remainders and separately rebuilds and prices the complete mutated
+profiles at the pinned exponent for the actual classes 2, 4, and 6. The direct
+delta formula and subtraction of the two complete profile prices enclose the
+same result.
+
+For remainders 2, 4, and 6, the complete moment increases by the following
+outward intervals; divide each integer endpoint by `10^30`:
+
+| old remainder | lower endpoint | upper endpoint |
+|---:|---:|---:|
+| 2 | `3509181979935340631634` | `3509181979935340636370` |
+| 4 | `2942545622277557042992` | `2942545622277557047728` |
+| 6 | `2590121108088020625486` | `2590121108088020630221` |
+
+The negative control omits the returned idle rank: its raw delta
+`1 + 5^(1-a) - 7^(1-a)` is negative, so that incomplete shortcut appears
+favorable. Exact call and rank-mass checks catch the omission. As a distinct
+positive control, the verifier replays PR #1256's two-slot relaxation
+`e1+e5-2e7+e_(r+8)-e_r`; its raw moment delta remains negative at all three
+actual remainder classes. This confirms that the same-slot result does not
+erase the separately priced relocation mechanism.
+
+Reproduce from the repository root with Python 3.12:
+
+```sh
+python3.12 scripts/research_package.py --package research/bit-inplace-retirement-seed11
+```
+
+Expected: `PASS_REGISTERED_RESEARCH_PACKAGE research/bit-inplace-retirement-seed11 outcome=negative-result`.
+The result certificate is [RESULT.json](RESULT.json). The registered check is
+a finite exact replay of this profile claim, not a proof of supplier
+admission, a new bit endpoint, or an asymptotic theorem.
+
+## Scope and remaining obligations
+
+The conclusion applies to the explicitly stated same-slot histogram change,
+the frozen `64,28416` profile, the pinned exponent, and the inherited moment
+formula. It does not rule out a different owner/window relocation, topology,
+helper interface, source boundary, or a change that removes other charges.
+Physical owner placement, H4 cleanup admission, native recursive replay,
+precision/tape obligations, and outer assembly remain outside this profile
+audit. PR #1256's finite circuit remains a finite construction; this note does
+not extend its interface contract.
+
+## Open next questions
+
+The next useful task is to price one concrete H4-admissible owner/window
+itinerary for helper470. It matters because a different placement or interface
+could change the complete profile even though the same-slot return is worse.
+The first step is to derive its full hosted histogram before implementing a
+compiler. Physical owner/window admission and the changed H4 cleanup contract
+remain open in PR #1256.
+
+## Credit
+
+Ali Romman's PR #1043 is credited for the earlier source-boundary helper470
+deletion and hosted invoice. The finite restoration exception, its two-slot
+relaxation, and the exact head `d6d5a994fcdcd8d04ec439ff988daa8f37b17ece`
+are from PR #1256. PR #1302 (head
+`0cc5db33b0999a7d3333383a855667f6f8cbda88`) supplies the native replay and
+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`) 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.

research/bit-inplace-retirement-seed11/RESULT.json

@@ -0,0 +1,86 @@
+{
+  "actual_remainder_classes": {
+    "2": {
+      "calls_delta": 1,
+      "delta_histogram": {
+        "1": 1,
+        "2": -1,
+        "3": 1,
+        "5": 1,
+        "7": -1
+      },
+      "direct_formula_interval_scaled_1e-30": [
+        "3509181979935340634001",
+        "3509181979935340634002"
+      ],
+      "full_moment_delta_interval_scaled_1e-30": [
+        "3509181979935340631634",
+        "3509181979935340636370"
+      ],
+      "rank_mass_delta": 0,
+      "two_slot_relaxation_raw_delta_interval_scaled_1e-30": [
+        "-4218511589072501683499826231",
+        "-4218511589072501683499803028"
+      ]
+    },
+    "4": {
+      "calls_delta": 1,
+      "delta_histogram": {
+        "1": 1,
+        "4": -1,
+        "5": 2,
+        "7": -1
+      },
+      "direct_formula_interval_scaled_1e-30": [
+        "2942545622277557045359",
+        "2942545622277557045360"
+      ],
+      "full_moment_delta_interval_scaled_1e-30": [
+        "2942545622277557042992",
+        "2942545622277557047728"
+      ],
+      "rank_mass_delta": 0,
+      "two_slot_relaxation_raw_delta_interval_scaled_1e-30": [
+        "-8763094305235481033659073902",
+        "-8763094305235481033659046724"
+      ]
+    },
+    "6": {
+      "calls_delta": 1,
+      "delta_histogram": {
+        "1": 1,
+        "5": 1,
+        "6": -1
+      },
+      "direct_formula_interval_scaled_1e-30": [
+        "2590121108088020627853",
+        "2590121108088020627854"
+      ],
+      "full_moment_delta_interval_scaled_1e-30": [
+        "2590121108088020625486",
+        "2590121108088020630221"
+      ],
+      "rank_mass_delta": 0,
+      "two_slot_relaxation_raw_delta_interval_scaled_1e-30": [
+        "-12077948998316473013168471918",
+        "-12077948998316473013168441432"
+      ]
+    }
+  },
+  "base_commit": "bce54fb3f895cbe5cd4c0eb477c3afeed100190f",
+  "inherited_bad_term": "32*64*N/(10^16*28416) * 64^alpha",
+  "interval_method": "exact Fraction atanh-log (24 terms), alternating/geometric Taylor exp (32 terms), signed outward intervals",
+  "pinned_idle_remainder": {
+    "2": 13920,
+    "4": 14208,
+    "42": 288,
+    "6": 14208,
+    "7": 21312
+  },
+  "selected_bit_exponent": "1733427039589844234749/1000000000000000000000000",
+  "selected_record_bit_lower": "1733427039589844234749/1000000000000000000000000",
+  "source_profile_calls": 904896,
+  "source_profile_rank_mass": 1808352,
+  "status": "PASS_SAME_SLOT_HELPER470_BILL_INCREASES",
+  "uniform_remainders_checked": 57
+}

research/bit-inplace-retirement-seed11/SOURCES.json

@@ -0,0 +1,48 @@
+{
+  "schema_version": 1,
+  "base_commit": "bce54fb3f895cbe5cd4c0eb477c3afeed100190f",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11",
+      "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "c05fafaa25ba95b2d5af86b1800427198e3d20eb",
+      "sha256": "89b5928bc92c81e2647b6d702a7ad85a6795b8f44e2eb267b2ff3145d8f2b2ce"
+    },
+    {
+      "path": "research/e8-bit-carrier-skeleton/code/hub/e8-r740-replica32/code/engines/moment.py",
+      "usage": "input",
+      "git_blob": "7d697cb45203fe72d97037403d6da41f71f3b7fd",
+      "sha256": "81cbc864e106418fc7854322746f72180cb8110ff39f74450a3b8d55a82c1482"
+    },
+    {
+      "path": "research/e8-bit-p111-tuned/tune/EXPECTED.json",
+      "usage": "input",
+      "git_blob": "e293ddc557742637f9f679f083a1a282d87b1b13",
+      "sha256": "b9f0e5ca038abe837b0007c8fe006f366a6f02009244ac57705a8a200e2301f4"
+    },
+    {
+      "path": "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz",
+      "usage": "input",
+      "git_blob": "85a4499bf9e4911a705d50567a2c2ef6cf23739a",
+      "sha256": "e3e301e62bc2b41dbf1ceac0acf3d35824ebeab1848c5a2142d4577b109da52f"
+    },
+    {
+      "path": "research/e8-bit-p111-tuned/tune/fastc.py",
+      "usage": "input",
+      "git_blob": "ec050c0139109d3033933fa137aa83a0f14fe5cc",
+      "sha256": "ae51f1fbb22b8c8dac8aab787c798361f6aa5d4e1fefb29e43d0197899d4eab5"
+    },
+    {
+      "path": "docs/research/community-batch1099-review.md",
+      "usage": "provenance",
+      "git_blob": "6cb6ec061a071a06a2d18cd4dc3e9a2b05d28099",
+      "sha256": "7e76d2c38e5fce30587835b7251df1430488ae4dd372611ef69a3f03f476b6cb"
+    }
+  ]
+}

research/bit-inplace-retirement-seed11/TASK.json

@@ -0,0 +1,60 @@
+{
+  "schema_version": 1,
+  "task_id": "scalar-to-moment",
+  "priority_revision": 2,
+  "base_commit": "bce54fb3f895cbe5cd4c0eb477c3afeed100190f",
+  "original_card": {
+    "id": "scalar-to-moment",
+    "question": "Can one known scalar simplification be converted into an actual paid-profile improvement?",
+    "starting_points": [
+      "research/r439-bsection-stars-seed01/README.md",
+      "certificates/selected-result.json"
+    ],
+    "methods": [
+      "Derive the changed legal frame itinerary and exact child histogram.",
+      "Prove a scoped obstruction showing why that scalar gain cannot change the paid contract."
+    ],
+    "acceptance_gate": "An unchanged histogram is not a kappa gain; record any separate runtime or proof benefit explicitly.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "research/r439-bsection-stars-seed01/verify.py"
+      ],
+      "expected": "PASS_R439_BSECTION_STARS",
+      "inspect": "Observe that the positive control improves scalar counts while retaining the paid histogram.",
+      "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay."
+    },
+    "first_experiment": "Choose one simplification and derive the complete changed frame itinerary, or prove why it cannot change the histogram.",
+    "bottleneck_link": "A legal change to the histogram, not addition count alone, is the bridge to an exponent gain.",
+    "allowed_variations": [
+      "One existing scalar simplification and one proposed frame-path change."
+    ],
+    "scope_change_triggers": [
+      "Submitting only another scalar count as completion of a paid-profile task."
+    ],
+    "overlap_terms": [
+      "scalar simplification",
+      "paid profile",
+      "R439"
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Does the complete width-64 paid bit bill improve when PR1256 helper470 shrinks in place from width eight to seven and returns one rank to the same idle remainder?",
+  "scope_change_reason": "The scalar-to-moment card led to a live paid-profile audit. The selected object is PR1256 helper470; this task isolates the unpriced same-slot return of its freed rank after checking the concurrent native closure and earlier hosted source-boundary result.",
+  "bottleneck_link": "A favorable local scalar or child-count edit only helps the conditional bit exponent if the complete paid profile and inherited per-call envelope improve.",
+  "budget_minutes": 50,
+  "stop_rule": "Derive the complete same-slot histogram for every feasible old remainder in a width-64 slot, then exactly price the actual pinned remainder classes at the selected bit exponent. Stop if the full bill is non-improving; do not build a new native supplier for a rejected profile.",
+  "outcome": "negative-result",
+  "evidence": "For every a in (0,1) and integer old remainder r in 0..56, the raw moment change is strictly positive by the integral lower bound in README.md; the inherited surcharge also rises because calls increase by one (two at r=0). Exact rational interval replay checks all 57 remainders and computes full-profile intervals for the actual classes 2,4,6.",
+  "author": "Cinna Davis (@1337isnot1337)",
+  "ai_assistance": "Substantial OpenAI Codex assistance in repository and PR review, mathematical derivation, exact interval implementation, replay, and writing.",
+  "open_questions": [
+    {
+      "question": "Can a different helper470 owner/window relocation or interface change preserve the useful retirement while satisfying H4 and the full physical allocation?",
+      "why_it_matters": "The rejected same-slot return does not price a different stage placement or remove other profile charges; those changes could alter the complete moment.",
+      "first_step": "Choose one concrete H4-admissible owner/window itinerary and derive its complete hosted histogram before implementing a compiler.",
+      "blocked_by": "The current finite PR1256 evidence leaves physical owner/window admission and the changed H4 cleanup contract open."
+    }
+  ]
+}