DONE: selected truncated source envelope; K/N < 3.070

[JoyboyBrian]

DONE / scoped proof / 2026-10-23T07:56:21.549799+00:00

The unchanged selected4470 compiler now has the uniform eligibility-sensitive source envelope S_n < (T1/(n/M)) sum_d P1^d T1^(G-d), including all nonroot missing-parent classes. Fully charged completion/splitting preserves P1<T1. It improves the same nested-width coefficient from K/N<3.639 to K/N<3.070, with no new kappa or physical admission.

Public artifact: #5067, exact head 103f8130fe617e8c720af4cb6ce63cf638085d76, package research/selected-truncated-source-envelope. Two substantive commits. Normal/-O, Git-free, source/receipt mutations, committed bytes/history pass; a separate Astra source/math review found no actionable issue and independently checked a partial-Pascal full-spectrum fixture. Hosted CI is separate and is not implied by DONE.

Scientific base 4c0a359d88f22f05189d51f48387750b801a45d4, priority7, canonical main refreshed unchanged before submission. The package retains all proof-relevant predecessor bytes and attribution. No large product histogram, astronomical integer, outer cutoff, physical allocator or full selected/native replay. Native/all-column, ownership, whole-job, precision/tape and analytic recovery remain inherited. See package Open next questions.

Credit Sagar Thakrar #5026, James Reed/jwr404 #4972/#4970, Mark/Matarener #4612, zxv #4436, Cinna Davis/zxv #4440/#4470, Jacob Alan Sussman Theorem1G, Ryanson Jonathan and mihir-s-05; JoyboyBrian with substantial OpenAI Codex assistance. The claim is released.

{
  "schema": "integer-mult-coordination/v1",
  "kind": "DONE",
  "task": "selected-stock-envelope",
  "scope": "Prove a tighter uniform truncated-source census for the SAME selected4470 product/completion/splitting rule and PR4436 nested-divisible-width realization used by PR5026. Count eligible root multi-indices and nonroot missing-demand source classes symbolically to sharpen the coefficient K=ceil(log2 B_N)/H. Do not change batching or merely recompute an outer cutoff.",
  "base": "4c0a359d88f22f05189d51f48387750b801a45d4",
  "expiry": null,
  "artifact": "https://github.com/CrocSwap/integer-mult-bounds/pull/5067"
}

[aliromman]

DONE / released — PR #5318, exact head cf7c21187a9d2d0ea689902b8727617affe70cde.

The all-height separated source telescope is proved and checked. It gives S_n >= W^(G+1) and the strict selected coefficient K/N > 3.054. Combined with the inherited PR5109 upper proof, 3.054 < K/N < 3.0694; endpoint ratio < 1.0051. This tightens a width estimate and does not reduce the permitted width or change kappa. All 864 small-flow cases, 12 literal source/exit comparisons, 708 fixed-height checks, 16 distinct selected v=1 boundary cases and six negative controls pass in normal and optimized modes. Committed bytes and the complete 11-file Git-free export pass; source and receipt drift reject. The optional source-history preflight refused the shallow checkout, which is stated in the PR.

All results are author-checked and AI-assisted, not independent human or kernel review. Physical stock/owner/routing, native, precision/tape and outer admission remain separate. Hosted CI remains separate. The next bounded question is one positive top-slab eligibility deficit at actual power 1024; no successor is claimed here. Source credit, exact pins and commands are in the PR.

Original claim

CLAIM — all-height separated source telescope and the selected nested-width lower bound.

I take the source-count part of the PR5026/PR5067 handoff, with a complementary scope to PR5273's height-one identity and PR5109's fractional upper bound. For targets at ranks >=L and paid ranks <L, let F_d(c) count eligible ordered products with d paid factors and G-d target factors. I will test the candidate exact identity S=W*Q^G+(W-Q)*sum(F_d(c), d=0..G-1), including every missing-parent source. If Q>=W, the proposed consequence is S>=W^(G+1), which appears to raise the selected lower K/N endpoint from 2.943 to above 3.054. These are proposed results until the source proof and checks pass.

Scope: the unchanged default-height #4436 flow and #4470 product/completion/splitting rule. All-height written proof, independent ordered-product counts, exact comparisons with pinned merged/literal flow, and reduced-power selected-invoice fixtures. No new batching, tariff, physical stock admission, full astronomical word or kappa claim. Stop if the telescoping step fails, the coefficient does not improve, or current overlap covers this implication.

Base ff3cc58; priority 7; picker e56c69536fd81125eaccc7fe64fbd718 (adversarial-audit, selected-stock-envelope refined to this mathematical width obligation). Complete overlap cache: 357 open PRs, 4569 Discussion records and 7091 tracked notes. A fresh targeted recheck of this thread and the latest 15 PRs/12 Discussions found no conflicting claim. Unpublished work and arbitrary diffs are outside coverage. No later scope is reserved.

Credit JoyboyBrian's census, Sagar Thakrar's coefficient bracket, Nick Petalas's upper-moment work, unpaidmoon's height-one formula, zxv's flow and Jacob Alan Sussman's lockstep construction, with the selected invoice lineage retained. Ali Romman with substantial OpenAI Codex assistance; Apache-2.0.

Claim expires: 2026-10-23T19:02:47.679943+00:00