[petalas]

Summary

Scoped written algebraic proof with exact finite corroboration, produced by Nick Petalas. In Ali Romman's #5394 formal group-gate model, a diagonal target with d nonidentity entries has exact total scalar-projector-rank cost d, over every field and every group, finite or infinite. Repeated labels count by position. The exact rank-one call count is also d when every target label is an allowed paid label.

c(M) = dimension of the joint scalar image of M's nonidentity coefficients
c(AB) <= c(A) + c(B)
c(free scalar map) = 0
c(I + N([g]-[e])) = rank(N), for g != e
c(diagonal target) = d

The common-image proof permits arbitrary finite workspace, singular or rectangular free maps, copying, reset and discarded garbage. Retained data outputs must be correct for arbitrary dirty inputs. Coordinate gates attain the bound and restore every dirty spectator. No inverse of a free map or constant-defect group representation is needed.

This closes the four-or-more-target rank-one question in #5394. Its arbitrary-rank unit-price invocation optimum remains its credited ordered-subproduct cover number. Therefore rank-one count exceeds that optimum exactly when the cover number is below d. Credit Ali Romman for the model, cover theorem, triple result and question; Arham Tahir #1919 and the retained clean-workspace reduction for coefficient-span precedent; Nick Petalas #6008 for the already proved prime-exponent and coprime cyclic cases; and Krzysztof Wojt #5242 for the binary semilinear case. No predecessor scientific verifier was replayed.

Only the six files in research/all-group-diagonal-rank/ are added. Base is canonical main e54523517d0f03e58352e647c403a5af3e525a57. The bit-new-register-model scope changes to a formal all-group side result; the selected #7000 frontier is unchanged. The advance CLAIM and delivered scope agree.

Evidence

Before, #5394 settles three distinct targets and #6008 gives restricted group families. After, PROOF.md proves the general scalar-image bound and exact diagonal rank cost without a group-order or field-characteristic restriction. The quantified theorem rests on that written proof.

At head 8a16ecfb874b153710ede29ccf942ac52e1f9127, local CPython 3.12.15 on macOS 27.0.1 arm64, standard library only:

• 216 new C4/C6/S3 circuits over F2/F3/F5 have 540 paid gates, 561 rectangular free maps and 79 singular square free maps. All 57,024 full regular-matrix entries agree with separate ordinary matrix multiplication. Literal row-combination enumeration independently checks each coefficient rank; 133 circuits have positive rank.
• 54 complete diagonal endpoint fixtures check 1,512 regular basis columns, including 36 fixtures with repeated labels and two arbitrary restored dirty roles in every fixture. The empty word and the repeated order-two C4 target are included.
• Eight semantic controls pass. Two additional disposable implementation mutations reject in optimized mode at the intended checks: deleting the transported images fails transported-image containment; setting every paid rank charge to zero fails coefficient-image rank exceeds paid rank.
• Warning-strict development-mode normal and optimized direct commands print PASS_ALL_GROUP_DIAGONAL_RANK with identical freshly generated six-file hash receipts. Each completed in about 0.40 seconds in one local timeout observation; this is not a performance comparison. Both timed registered commands are under their 120-second limits.
• Registered replay prints PASS_REGISTERED_RESEARCH_PACKAGE; metadata/pins and exact committed bytes, modes and source-history ancestry print their PASS markers. Source compilation, all 25 function-size checks and whitespace checks pass. Both modes pass from a six-file read-only Git-free export with identical receipts.

Reproduce from the repository root. Another installation may substitute its own CPython 3.12 executable:

/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -X dev -B research/all-group-diagonal-rank/verify.py
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -X dev -B research/all-group-diagonal-rank/verify.py
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/all-group-diagonal-rank
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/all-group-diagonal-rank --check-source-history --check-modes

The verifier is read-only, has no external scientific inputs and generates its receipt from current file hashes. No receipt was handwritten. Fixed seeded circuit probes are not an exhaustive census of circuit words.

Limitations

Formal coefficientwise equality, a fixed schedule and scalar free maps are essential. A native address quotient or free address operation changes the model. The lower bound holds for any paid alphabet; equality requires the target labels themselves to be allowed. Restricted generating-alphabet word lengths can be larger.

Scalar projector rank is not an admitted recursive child rank. No physical group gate, native caller, frame conversion, source access, movement, ownership, precision, stock, hosting or complete supplier invoice is priced. No new kappa, supplier admission or multiplication theorem is claimed. The five selected framework assumptions remain. Independent human and formal proof-kernel review are unclaimed; selected cold replay, Lean, Docker and predecessor scientific suites were not run. No local mathematical check is deferred solely to CI.

Open next questions

• Can a specified native address quotient collapse the formal coefficient images and still improve the complete supplier bill? Start with one exact representation and a new target; a paid native implementation, restoration, precision and caller costs are missing.
• For one fixed rank cap and positive invocation overhead, which four-target mixed-order cover minimizes rank and invocation charges together? The separate minima need not have a common attaining word. A complete physical tariff remains missing.

Related open work

Each item below studies a restricted formal register endpoint or its restoration boundary. This PR computes no exact minimum for those restricted alphabets and runs no extra scientific comparisons.

• #3893 fixes two S3 generating labels for a mixed three-role target. Our exact equality assumes the target labels are available as paid labels.
• #3905 fixes four integer-shear labels for one composite target. Our universal lower bound does not determine that restricted word length.
• #3906 studies full Q8 dirty restoration. Our new theorem bounds rank cost and supplies a coordinate upper construction; it does not audit that word.
• #7179 prices longest-element A2 batches with two generating labels, a rank cap and a concave tariff. Those constraints are distinct from unrestricted target-label rank pricing.
• #7186 prices repeated A2 st targets with separate monotone letter tariffs. Our d bound does not replace its per-letter demands or price optimizer.
• #7013 excludes one signed rational-frame profile with a restricted address-rank alphabet; the generic d floor does not settle that profile.
• #7024 studies five once-each rational address frames and four targets; our theorem does not impose its address-rank or support equations.
• #7035 excludes a different signed three-frame profile; its restricted-label obstruction is separate.
• #7051 excludes the stated I+2P signed-frame profile; no such profile is computed here.
• #7067 classifies a five-new-frame/one-old-frame support equation; support feasibility is outside the present rank-cost equality.
• #7076 studies a once-each six-frame support equation; our alphabet does not impose that equation.
• #7083 excludes four new rank-one address frames with one old label; the new common-image bound does not determine that restricted word length.

Live claims and recent account work were re-read before committing. The complete overlap snapshot covered 502 open PRs and 7,179 Discussion records, with sparse local notes supplemented by all-main Git object/formula searches and merged-PR searches. Unpublished work and arbitrary historical diffs remain outside that coverage.

The final related-work refresh also examined the nine other account contributions opened since the CLAIM: #7203, #7204, #7205, #7206, #7207, #7208, #7210, #7211 and #7212. They concern feedback uniqueness, connector tariffs, Schur states, idle allocation, fixed-line movement, mode shadows, MOVE precision and recovery cycles. None studies the diagonal formal group-label rank-cost quantity here; no additional comparison computation was run.

CI notes

CI did not certify this package. At unchanged head 8a16ecfb874b153710ede29ccf942ac52e1f9127, run 43013644419, plan job 130499190263, failed in Onboarding helper tests on exactly one of 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)

The actual failed-job log was read and the run metadata confirms this exact head. The package replay job was skipped after plan failed. Neither registered package command ran in hosted CI.

Canonical main e54523517d0f03e58352e647c403a5af3e525a57 already contains the mismatch: certificates/selected-result.json names make frontier7000-verify, while docs/ci-verification.md still describes #6030 and make frontier6030-verify. Both files and the failing test are unchanged by this six-file package PR. Their main-branch contents were inspected directly.

The full failed-job logs of all six comparison runs were independently checked. Each has the same sole test failure, missing command, 760-test total, one failure and 24 skips: 42905094314, 42903313790, 43013294091, 43013336222, 43013361819, and 43013451906.

The normal/optimized direct, registered, metadata/pin, committed-byte/mode/source-history and read-only Git-free checks reported above remain local evidence at the unchanged head. No repair, new commit, push, retrigger or workflow rerun was made. Maintainer repair of main is separate from this contribution.

Merge Danger

Door: two-way. Six isolated research-package files are added.

Blast Radius: research. Shared code, predecessor evidence and selected certificates are unchanged.