[petalas]

Summary

Scoped written proof with exact finite corroboration. For every h>=0, the unchanged balanced dirty word at n=2^h+1 has exact joint interval envelope floor(h^2/2)+h+3, covering all ordered ideal-leaf cuts and both orientations. Real scalar signs attain the bound. At n=17 the height-only bound 19 sharpens to the exact value 15.

unequal child sizes -> one idle depth row -> sharper six-phase upper bound
split the last leaf of the credited power-of-two witness -> matching lower bound

This answers one infinite family in CubeJerry's #6770 Open next question 1. The unequal-child proof and last-leaf extension were produced by Nick Petalas. Credit CubeJerry's inverse-prefix bound and height theorem, Arham Tahir's power-of-two scalar witness, Hanson Sun's unit-entry invariant, Charles Bethin's phase/squarefree identities, Chafik Boukhalfa's word and the retained precision/restoration lineage. Predecessor proofs are cited inputs, not audit deliverables; exact pending proof bytes and original notices are retained unchanged.

Advance CLAIM.

Evidence

Local CPython 3.12.15, standard library only:

• All 92,720 nonempty chronological intervals across both word orientations at n=17 have maximum coefficient mass 15; the first maximizing target row is at positive cuts [38,87). Complementary inverse cuts cover the reverse ordered direction.
• Exact scalar attaining rows pass at h=1..32. Literal noncommutative replay agrees with the first four compressed witnesses. Phase inequalities pass at h=1..10,000, with six contract rejections and three mathematical controls.
• Both registered commands pass, timed separately at 0.452481 and 0.456682 seconds against 120-second caps. These timings document CI timeout margin, not a performance claim. The package runner and direct verifier pass.
• Committed bytes and declared source ancestry pass at 666e561e8ee88dbf839901ba018a0e2d29c55b1f: 12 files, canonical source base 7c49fe32c55de02c2c873655c804b16e4c3fef0a. Official export integrity passes. Its read-only export runs normal and optimized with an empty PATH and identical generated hash-bound receipts.

From the repository root, another CPython 3.12 interpreter may replace the local absolute path:

/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/dirty-one-extra-factor
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -B -W error -X dev research/dirty-one-extra-factor/verify.py
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -B -W error -X dev research/dirty-one-extra-factor/verify.py
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/dirty-one-extra-factor --check-source-history

Expected markers: PASS_DIRTY_ONE_EXTRA_FACTOR, PASS_REGISTERED_RESEARCH_PACKAGE, PASS_RESEARCH_COMMIT_BYTES.

Limitations and unrun obligations

The universal statement is the written induction under the cited premises; finite checks corroborate it. It settles n=2^h+1, not every factor count. Actual rounded error support, inverse preimages, internal leaf growth, preparation, physical precision/tape costs, caller integration and all five selected assumptions remain separate. No selected cold replay, Lean, Docker, independent human review or proof-kernel verification was run. No new kappa or selected-frontier change.

Open next questions

• Determine the exact envelope for other n by retaining correlated target/scratch support in the phase recurrence. Simultaneous attainment remains open.
• Bind an actual rounded caller of this size and compare its destination-supported estimate before changing precision. The complete rounding, preparation and tape invoice remains required.

Related open work

• Prove the sharp joint dirty-word interval envelope (no new κ) #6770: supplies the cited sharp height-uniform envelope; this gives an exact fixed-length infinite subfamily left open there.
• Disprove the universal Omega cut and prove the dyadic error asymptotic (no κ) #6784: studies accumulated completed-leaf error mass over dyadic words, a different quantity from one joint interval norm.
• Optimize dyadic error cuts and prove a quantitative convergence rate (no κ) #6789: optimizes Disprove the universal Omega cut and prove the dyadic error asymptotic (no κ) #6784's accumulated-error cut family and convergence rate; no common new numerical value is compared here.
• Prove all-depth attainment of 4g-3 destination channels (no κ) #6668: counts maximum-mass destination channels at n=2^g-1; this concerns arbitrary joint disturbances at n=2^h+1.

Live PR bodies, recent handoffs, local locks, merged formula/object searches and main README searches were checked before committing. Canonical main is unchanged. These searches do not cover unpublished work or prove global novelty. No additional computations audited another PR.

Completion refresh checked the eight other account open PRs created since the advance CLAIM: #6795, #6797, #6798, #6799, #6800, #6801, #6802 and #6803. They study padding tapes, cubic shared-block classification, cube lattices, permutation rank chains, square-zero capacity, signed halves, NTT instructions and joint return thresholds. None studies the balanced-word joint interval envelope, so no additional same-object or same-quantity line or numerical comparison is required. No extra computation audited them.

CI notes

At head 666e561e8ee88dbf839901ba018a0e2d29c55b1f, both plan and replay (research/dirty-one-extra-factor) passed in GitHub Actions run 42228445179. The checks were read once after completion. The hosted registered replay passed; all registered scientific checks also passed locally. CI success is executable corroboration, not independent mathematical acceptance or a proof-kernel check.

Merge Danger

Door: two-way. Blast radius: isolated. Only research/dirty-one-extra-factor/ is added.