[petalas]

Summary

Scoped written proof with exact finite corroboration, produced by Nick Petalas. For arbitrary finite two-type nonnegative row menus, determine the sharp common contraction rate when positive reserve weights have imbalance at most B >= 1.

q_B = max {
  max_(a,b) (a+b/B),
  max_(c,d) (d+c/B),
  max_row_pairs (a+d+sqrt((a-d)^2+4bc))/2
}.

The proof supplies the entire feasible weight interval at every rate and shows that rational weights attain the optimum exactly when the optimum is rational, for rational rows and B. A new four-row example has exact law max(1/(2B),sqrt(2)/4). The reserve cap also gives the all-depth abstract relative tail bound B*q^k.

Ali Romman's #6472 supplies the independent adaptive-row contract and explicit common-ratio question. Its existing result is cited, not replayed. Older #6555 solves one uncapped fixture; its menu, identity and cutoff are not used as the main step. Classical Perron roots, positive diagonal scaling and weighted contraction retain their credit; global priority for those methods is unclaimed.

Advance CLAIM. Canonical base e545235; selected frontier unchanged.

Evidence

Before, the cited adaptive-row interface supplied valid common weights without an explicit arbitrary-menu reserve-cap optimum. After, the closed form and complete interval give an exact rational feasibility certificate.

• All 30,375 rational decisions agree with a separate normalized-polytope vertex enumeration that tests the original row inequalities and uses no row-pair determinant: 11,831 feasible and 18,544 infeasible.
• The verifier checks every delivered interval endpoint and midpoint, 455 exact transition thresholds, 387 tail prefixes and 14 rejecting controls. The universal claim rests on PROOF.md, not finite extrapolation.
• Warning-strict normal and optimized CPython 3.12.15 replays have identical generated hash-bound receipts. Registered metadata/pins and committed-byte/source-history checks pass. Each registered command was timed locally: 0.82 s normal and 0.84 s optimized, under its 120-second bound.

From the repository root:

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

Another CPython 3.12 executable can replace the host-specific path. Expected markers are PASS_BOUNDED_ADAPTIVE_RESERVES, PASS_REGISTERED_RESEARCH_PACKAGE and PASS_RESEARCH_COMMIT_BYTES. No predecessor executable, receipt or scientific census is imported.

Limitations

No actual physical supplier menu or reserve consumer is bound. Native realization, complete charges, independent row legality, compiler closure, ownership, stock, precision/tape and analytic recovery remain separate. All five selected framework assumptions remain; there is no new kappa or complete multiplication theorem. Selected cold replay, Lean, Docker, independent human and formal proof-kernel review are unclaimed.

The theorem covers arbitrary finite nonnegative real menus. The executable checks rational thresholds with at most sixteen rows per type and 64-bit input numerators/denominators. Its managed-allocation deviation and fixed replay bounds are documented. No shared source or pinned evidence changes.

Open next questions

1. Bind one complete current two-type menu and a real reserve consumer, including every child, adapter and restoration charge and the permissible B.
2. Find a useful higher-type certificate that retains all pairwise reserve constraints; the two-type interval formula does not supply that extension.

Related open work

• #7151 bounds retained backend backing with a finite-stage Bellman certificate. This result instead optimizes positive scaling under an explicit cap for abstract two-type row menus; it does not compute or reassess that physical reserve.

The completion check of this account's open PRs created after the advance CLAIM found no additional PR studying this two-type contraction or reserve-cap quantity.

Main, live PRs and claims were refreshed before committing. Distinctive reserve-cap, general-menu and formula searches found no prior delivery of this result. Sparse omitted notes, arbitrary historical diffs and unpublished work remain coverage limits.

CI notes

CI did not certify this package. At unchanged head 18cd386d47b415fcc6c6cddde9ae1ac3d1c8749e, run 43029125610, plan job 130551298799, failed in Onboarding helper tests. The log reports exactly one failure among 760 tests, with 24 skipped:

test_research_current_status.CurrentCiNavigationTests.test_current_ci_section_matches_selected_record
AssertionError: '`make frontier7000-verify`' not found
FAILED (failures=1, skipped=24)

This failure is inherited from canonical base e54523517d0f03e58352e647c403a5af3e525a57: certificates/selected-result.json specifies make frontier7000-verify, while the current section of docs/ci-verification.md still describes #6030 and make frontier6030-verify. Both base files were read directly; this PR changes only its six package files. The replay job was skipped because plan failed, so no hosted scientific replay ran.

The failed-job logs for 42905094314, 42903313790, 43023514635, 43024693032 and 43029249083 were read and each confirms the same exact failing test, missing-command assertion and one-failure/24-skipped summary across 760 tests. No unrelated CI failure is inferred.

Local normal/optimized direct checks, both registered commands, metadata/pins and committed-byte/source-history checks passed as recorded above. Those are local evidence only. The repository navigation repair remains for maintainers; no fix or retrigger commit is added here.

Merge Danger

Door: two-way. Blast radius: one isolated research package and two bounded replay commands. No shared implementation or selected-frontier files change.