[petalas]

Summary

Scoped written proof with exact finite corroboration, no new κ. In the rational scalar-idempotent model, t invertible data targets with a common rational flag, plus any number of clean identity helpers, require at least mt paid calls if the frame span has dimension at most m+1. Diagonal targets attain this bound with mt calls and span m.

upper-entry projection:  identity output  ->  r_X + r_Y <= U
diagonal projections:    t active outputs ->  t <= r_X + l_i, t <= r_Y + l_i
rank-one lower frames:   l_1 + l_2 <= E - U  ->  E >= 2t

This partially answers open question 1 of unpaidmoon's PR6338. The common-flag hypothesis is needed for the proof. The CLAIM asked about arbitrary invertible targets; the progress update records the narrower delivered scope. The result was produced by Nick Petalas.

Eumemic's PR288 supplies the model, Ali Romman's PR468 the normalization, projections and flag bound, PR5988 the all-dimensional support split, and unpaidmoon's PR6338 the question and non-two-support cases. Ali Romman's PR4961 already proves the stronger unrestricted-span nine-call bound for three lower-triangular 3-by-3 data targets and one returned register; that special case is not new here. PR4118 supplies a partial dirty-auxiliary span-four bound. Predecessor results are cited inputs and were not re-verified.

Evidence

Before: PR6338 leaves clean helpers in the two-support block open. After: with a common target flag, the exact rank argument handles any number of data and clean helper registers in all address dimensions.

Local CPython 3.12 checks from the repository root:

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

Both direct modes return PASS_CLEAN_HELPER_FLAG_BOUND short_words=178808 identity_words=56 cancellation_calls=6 sharp_calls=4 controls=4. They enumerate short words in one finite projected alphabet, check the scalar span inequality for each identity word, verify direct and cancellation fixtures and reject a missing cancellation. These controls do not establish the universal theorem. The registered replay and metadata check pass; each registered command ran locally in under two seconds. The committed-byte and source-history check passes at e7b08ac9ef4ea5b5517d9d325ae6aeae445d3f91. The selected baseline reports PASS_RESEARCH_BASELINE_BINDINGS_ONLY.

Limitations

The proof cites PR468, PR5988 and PR6338 for the existing normalization, support split and non-two-support cases. It does not cover targets without a common rational flag, general dirty helper exponents, frame span above m+1, interposed address maps, native implementation or a complete supplier invoice. No selected-frontier update or complete multiplication theorem is claimed. Independent human and formal proof-kernel review are unclaimed. No Lean build or selected scientific cold replay was run.

Open next questions

• Does the two-dimensional bound hold without a common rational flag? Start with two targets whose relative two-by-two matrix has irreducible quadratic characteristic polynomial; their upper projection need not have identity output.
• Can nonzero dirty helper exponents be admitted when their upper projection vanishes? Track their contributions to the diagonal ranks.

Related open work

• PR203 studies a common triangular flag for paid frames; this proof instead assumes a common flag for the data-target ratios and limits frame span.
• PR6419 accelerates the PR6338 finite verifier. It does not establish this two-support bound.
• PR3893 studies a three-register target in a finite nonabelian algebra; the present proof uses rational additive address frames.

CI notes

At head e7b08ac9ef4ea5b5517d9d325ae6aeae445d3f91, the plan job in run 41726501615 was cancelled by the workflow’s 10-minute timeout while the repository-wide Onboarding helper tests step was still running. Package selection never ran, and the replay job was skipped. Hosted CI did not certify this result. The finite checks are certified only by the local runs listed above; they do not constitute independent human or formal proof-kernel review.

Merge Danger

Door: two-way. Blast radius: isolated.

Only the new research package is added. Frozen predecessors and the selected result remain unchanged.