[petalas]

Summary

Scoped proof: for fixed descending chronological batch lists, source counts and base widths, the recursively least LCM library divides every feasible competing library at every rank. Joint enlargement of earlier libraries cannot improve a later width within the common-replication policy. This answers the joint-library part of Mihir Srivastava's merged #4507 Open next question 1.

M_n(B) = lcm_(e,q) B_e/gcd(B_e,q)
b_n = S_n M_n(b)
For every feasible B: b_n divides B_n at every rank.

The proof uses divisibility monotonicity of the local modulus and induction against an arbitrary complete library. A unique positive slack vector describes every feasible library. Increasing-rank normalization preserves all later widths and feasibility. Mere coordinatewise multiples of the minimum need not be feasible; a counterexample distinguishes the exact characterization.

This contribution is produced by Nick Petalas. Credit Mihir Srivastava #4507 for the local lemma and explicit question, Jacob Alan Sussman for the integer compiler, zxv #4436/#4483 for chronological flows, codyw912 #4638 for width bounds and arbitrary-height transfer, Cinna Davis and Ryanson Jonathan for their credited construction and flow/width lineage. No predecessor program or census is replayed. Only research/global-batch-library-minimum/ is added.

Evidence

Before: #4507 establishes the least multiplier for prescribed earlier widths and explicitly leaves joint-library optimization unresolved. After: the new induction proves a simultaneous divisibility minimum over every library in that same fixed policy.

On CPython 3.12.15, standard library only:

• 729 synthetic systems, 944,784 directly enumerated candidate libraries, 30,591 feasible libraries and 61,182 feasibility-preserving normalization steps pass. Candidate enumeration does not use the slack constructor.
• 128 larger systems and 2,048 generated libraries cover 24,576 coordinates. Slack recovery, literal whole-invocation feasibility and global divisibility pass.
• Eight semantic controls, thirteen invalid-input rejections and three capacity controls pass, including 32 ranks, 32 batches and a 1,008-bit growing-width fixture. The executable constructor's bounded slack domain is explicitly distinguished from the broader feasibility predicate.
• Warning-strict normal and optimized registered checks pass. Individually timed final checks take 1.36s and 1.33s locally, below their 120-second limits. These are replay durations, not performance improvements.
• All seven committed package files and declared source ancestry pass check_research_commit.py at 41fb7f22ac265e56f3ca31c990c8ee8582976fa4. Official export integrity and optimized read-only Git-free replay pass. Replacing LCM by product fails global divisibility; corrupting the receipt count fails the source-bound receipt comparison.

Exact reproduction from the repository root:

/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/global-batch-library-minimum
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/global-batch-library-minimum/verify.py
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/global-batch-library-minimum/verify.py
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/global-batch-library-minimum --check-source-history

Substitute another CPython 3.12 executable if necessary. The verifier reports PASS_GLOBAL_BATCH_LIBRARY_MINIMUM; the registered runner reports PASS_REGISTERED_RESEARCH_PACKAGE research/global-batch-library-minimum outcome=completed. RESULT.json is generated and bound to implementation, proof and metadata hashes.

Limitations and unrun obligations

The all-size result is a written proof with bounded computational corroboration. Fixed batch lists, fixed source counts, rank descent, fixed bases, whole invocations and one common replication per rank are hypotheses. This does not optimize different schedules, per-class replication, cross-cut pooling or arbitrary alternative suppliers. It supplies no tighter width growth order, physical routing/storage cost, new leaf exponent, supplier admission, new kappa or complete multiplication theorem. Independent human and formal proof-kernel review are unclaimed. No selected cold replay, Lean or Docker run was performed.

The current selected-source orientation command passed. The original card's historical scripts/research_baseline.py fails with KeyError: 'bit_lower' on the changed selected schema; that failure is documented, without modifying the baseline or using it as scientific evidence. The card is explicitly changed to this compiler-width side result. Canonical main remained 624de9dc66858af0945e5f8a0942488d62280d43 at the submission refresh. Selected-frontier files are unchanged.

Advance claim. Live open PRs, recent account submissions, handoff claims, distinctive main-tree README terms and merged searches were checked. Sparse cache omissions and unpublished work remain coverage limits.

Open next questions

Can independent replication of different path classes reduce productive width while preserving chronological matching and completed returns? First specify a two-class native matching and rejoin contract with coprime local moduli. That missing contract must be resolved before treating such a relaxation as a supplier construction.

Related open work

No open PR studying this same fixed chronological LCM width sequence was found in the scoped title/body search. Nearby compiler work is separate:

• Ordinary BIT saving 0.003475458 via three finite leaf backends #4814 changes finite leaf backends and sufficient compiler parameters; this proof changes neither its backend invoice nor its saving.
• Prove the exact optimal integer compiler separator (no new κ) #4873 optimizes an integer separator in sufficient compiler inequalities; it computes a different quantity, not productive batch width.
• Preserve physical PCs with compact residual-block compilation #4791 preserves physical program counters in residual-block compilation; this arithmetic library theorem supplies no physical PC or routing bound.

The pre-DONE refresh read all 71 open PRs on this account, including ten created since the CLAIM and nine other submissions. Those nine concern Hurwitz decoding success, weighted pair tours, SL2(F3) dirty workspace, localized Gaussian headers, cyclic-source root stock, nonlinear Eisenstein restrictions, four-label excess, the z4 error guard and dense-output scan cost. None studies this fixed chronological LCM width sequence or computes a competing width for these fixtures. No extra predecessor computations were run.

CI notes

Both hosted checks passed at 41fb7f22ac265e56f3ca31c990c8ee8582976fa4 in Registered research packages run 39870058859: planning in 3m02s and registered package replay in 1m25s. Run metadata confirms the matching head and successful completion. The registered replay executes both warning-strict normal and optimized commands. Local registered/direct replay, committed-byte/source-history preflight, export integrity and read-only Git-free replay also passed. Hosted replay certifies execution of the scoped automated checks, not independent human or formal proof-kernel acceptance.

Merge danger

Door: two-way. Blast radius: isolated research package. Shared code, frozen sources and the selected record are unchanged.