[petalas]

Result

Scoped written proof with an exact finite check. No new κ, no supplier change, selected frontier unchanged.

Model: the abelian scalar-idempotent register model (eumemic's PR #288 §1.2, as stated by Ali Romman's PR #468), with m x m rational rank-one frames, W registers and invertible targets. In every address dimension m, a paid-frame span of dimension at most m + 1 forces at least mW calls for invertible lower-triangular targets. PR #468 proves this only at m = 3 (its span-four lemma). The direct word attains mW.

After Cauchy–Binet normalization, the span is diag + t·uv^T. Let K = supp u ∩ supp v:

Case	Argument	Targets
span <= m	PR #468 low-span lemma (cited)	any invertible
`	K	>= 3`
`	K	<= 1`
`	K	= 2`

PR #468's step needs full support of u, v, and its component bound needs blocks of size at most two. Neither holds in dimension four or more once frames have zero coordinates. This PR replaces both steps with the |K| split.

Package: research/span-lemma-every-dimension (README, PROOF.md, verify.py).

Evidence and reproduction

From the repository root:

~/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/span-lemma-every-dimension/verify.py
~/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/span-lemma-every-dimension/verify.py
~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/span-lemma-every-dimension
~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/span-lemma-every-dimension --check-source-history

Local results (CPython 3.12.15, macOS arm64): both verifier runs print PASS_SPAN_LEMMA_EVERY_DIMENSION in 0.37 s. The package check prints PASS_REGISTERED_RESEARCH_PACKAGE ... outcome=completed. The commit check prints PASS_RESEARCH_COMMIT_BYTES.

The verifier checks:

• The support classification for every pair of nonempty supports with m <= 7. For |K| >= 3, each index has the minor witnesses. The only nontrivial strongly connected component is K when |K| >= 2. The graph is acyclic when |K| <= 1.
• The minor identity, as a polynomial identity.
• An exact integer rank-one grid at m = 3, 4, 5: 434,845 matrices and zero off-line rank-one elements.
• Two controls: the rank detector, and an explicit off-line rank-one element at |K| = 2 (u = v = (1,1,0), D = diag(2,2,0), t = -1), which shows that Lemma C fails there.

Limitations

• The |K| = 2 case relies on PR Prove nine calls are necessary for three abelian bit registers #468's block flag argument and its lower-triangular target hypothesis, which is cited and not rechecked.
• Not covered: span m + 2 or more, extra clean or dirty registers, free address maps between paid calls, nonabelian models, and native conversion.
• The finite grid is a control. The theorem rests on the written proof. Independent human review and proof-kernel review are unclaimed.

Open next questions

1. Does |K| = 2 still force mW for non-triangular invertible targets? Start at m = 2 with full-support u, v.
2. Does span m + 2 force mW for m >= 4? Classify the joint support graph of the two extra frames.
3. Do clean or dirty extra registers change the span-(m+1) bound in dimension m?

Related open work

No open PR studies the general-dimension span lemma. Open register-model PRs (for example #3893, an S3 three-register rank bound, and #5963, C3 inverse targets) use different alphabets or targets. This PR computes no number they report.

This account's open PRs opened since the claim (#5989 two-guard reciprocal, #5990 fused two-root readout, #5992 pooled R437 carrier moment) study different objects. None computes a quantity this PR computes.

Credit

Produced by Nick Petalas. Model: eumemic, PR #288. Low-span lemma, span-four lemma at m = 3, projection tools and block flag argument: Ali Romman, PR #468. Common triangular-flag obstruction: huxint, PR #203. Claim: #1166 (comment)

CI notes

Both hosted checks passed for head 206f637a74cbaab165c736fe94f6ff556dda880a: plan and replay (research/span-lemma-every-dimension), run https://github.com/CrocSwap/integer-mult-bounds/actions/runs/40571244245