Prove exact diagonal rank cost for every group and field (no κ)

research/all-group-diagonal-rank/PROOF.md

@@ -0,0 +1,144 @@
+# Diagonal group targets have exact scalar-rank cost
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+Claim type: scoped written algebraic proof with exact finite corroboration.
+
+## Model and statement
+
+Let K be any field and G any group, finite or infinite, with identity e.
+Work coefficientwise in the full formal group algebra K[G]. Every matrix
+has finite support. A free operation is a fixed scalar K-linear map, with
+address action [e]. Free maps may be rectangular or singular and may copy,
+reset or discard scalar registers. The schedule is finite and fixed.
+
+A paid gate on r registers is
+
+```text
+D(N,g) = I_r[e] + N([g]-[e]),  N in M_r(K), N^2=N.
+```
+
+Its scalar-rank charge is rank_K N. Rank-one call count is the same charge
+when every paid projector has rank one. Initial scalar embeddings of data
+and clean helpers, and final selections of retained outputs, are free maps.
+Arbitrary dirty inputs may also be supplied. Retained data outputs must be
+correct for every such input. Restoration of additional outputs is optional
+for the lower bound; the attaining construction restores them.
+
+**Theorem.** Suppose the retained independent data outputs implement
+diag([t_1],...,[t_m]) on their m independent data inputs. Let
+d = |{i : t_i != e}|, counting repetitions by position. Then every such
+circuit has total paid scalar rank at least d. If every nonidentity target
+label t_i is in the paid alphabet, its exact minimum scalar-rank charge
+and exact minimum rank-one call count are both d.
+
+The lower bound holds for an arbitrary paid alphabet and does not use
+idempotence. The equality statement requires the target-label availability
+just specified. It is not a word-length theorem for a restricted generating
+alphabet.
+
+This answers the four-or-more-target question in Ali Romman's
+[#5394](https://github.com/CrocSwap/integer-mult-bounds/pull/5394) for every
+group and field in its formal model. That package's arbitrary-rank,
+unit-price invocation optimum remains its ordered-subproduct cover number.
+Consequently rank-one count exceeds that invocation optimum exactly when
+the cover number is less than d. We cite the cover theorem; we do not
+re-prove or replay it.
+
+## One common scalar image space
+
+For a rectangular formal matrix M = sum_g M_g[g], define
+
+```text
+U(M) = sum_{g != e} col_K(M_g),
+c(M) = dim_K U(M).
+```
+
+All coefficient images are subspaces of the same scalar output space.
+This is a sum of subspaces, rather than a sum of the individual ranks.
+Its dimension counts repeated output directions correctly even when many
+targets have the same group label.
+
+Write epsilon(M) = sum_g M_g for augmentation. The coefficient images of
+M-epsilon(M)[e] span exactly U(M): its nonidentity coefficients are M_g,
+and its identity coefficient is -sum_{g != e} M_g.
+
+**Lemma.** For compatible rectangular formal matrices A and B,
+
+```text
+U(AB) is contained in U(A) + epsilon(A) U(B),
+c(AB) <= c(A) + c(B).
+```
+
+**Proof.** Augmentation is multiplicative, since summing every ordered
+coefficient product gives epsilon(A) epsilon(B). Thus
+
+```text
+AB-epsilon(A)epsilon(B)[e]
+  = (A-epsilon(A)[e]) B
+    + epsilon(A)[e] (B-epsilon(B)[e]).
+```
+
+Every coefficient of the first summand is a sum of scalar matrix products
+A'_g B_h, with col(A'_g) contained in U(A). Its columns therefore lie in
+U(A). Every coefficient of the second summand has columns in
+epsilon(A) U(B). Taking the sum of coefficient images proves containment.
+The image of a linear map cannot increase dimension, proving the rank
+inequality. No commutation of group labels, inverse of a free map or
+restriction on the group order was used. QED.
+
+A free scalar map has c=0. For g != e, the gate coefficients at e and g
+are I-N and N. After subtracting augmentation I, they are -N and N, so
+c(D(N,g))=rank N. For g=e the gate is identity and has c=0, which is at
+most its declared rank charge. Iterating the lemma through the entire
+rectangular circuit gives c(M) <= sum_j rank N_j.
+
+Equivalently, in matrix order write the retained data block as
+C_0 D_1 C_1 ... D_k C_k. Expand by the leftmost paid perturbation.
+The scalar image of each resulting term lies in
+col(C_0 C_1 ... C_(j-1) N_j). The sum of these k scalar spaces has dimension
+at most sum_j rank N_j and contains every nonidentity output coefficient.
+This equivalent expansion explains the transported-image test in verify.py.
+
+## Apply the bound and attain it
+
+Select the retained data-output rows and the independent data-input columns
+of the circuit. The endpoint maps in that selection are scalar, so the
+same bound applies to the resulting m-by-m matrix T. This argument allows
+arbitrary dirty workspace and arbitrary discarded garbage without assigning
+them zero cost or assuming their input values vanish.
+
+For each g != e, the coefficient T_g is diagonal, with a one in position i
+exactly when t_i=g. Its column space is the span of the corresponding
+coordinate axes. Summing over g != e gives precisely the d active axes.
+Thus c(T)=d, proving the lower bound.
+
+For the upper bound, apply one gate D(E_ii,t_i) to each active position i.
+The projectors have rank one and commute because they act on separate
+scalar registers. Their product is the required diagonal target. They
+touch no helper and restore all dirty spectators. There are exactly d
+gates and d total rank units. This also covers d=0 by the empty word. QED.
+
+## Scope and predecessor credit
+
+Ali Romman's #5394 supplies the model, cover theorem, three-label result
+and open question. The scalar coefficient-image method has precedent in
+Arham Tahir's #1919 and in the image-span reduction retained in
+research/bit-clean-workspace-compression. We claim the arbitrary-group
+application, the rectangular common-image proof and the complete answer
+to #5394's rank-one question, not invention of coefficient-span methods.
+
+Nick Petalas's older #6008 gives a representation-rank cut and proves the
+same d value for prime-exponent groups, with a coprime cyclic-character
+remark. Krzysztof Wojt's #5242 gives the mixed-target binary semilinear
+case. Those restricted consequences are prior work. No predecessor
+scientific verifier is run here. SOURCES.json pins the retained sources
+used for the argument and context.
+
+Formal coefficientwise equality is essential. A representation faithful on
+group elements can still kill nonzero linear combinations. Free
+address-dependent maps and data-dependent control are outside this model.
+The theorem prices scalar projector rank, not physical address action,
+native realization, frame conversion, precision, tape movement, hosting,
+restoration overhead or a complete supplier invoice. No new kappa or
+selected-frontier change follows. Independent human and formal proof-kernel
+review are unclaimed.

research/all-group-diagonal-rank/README.md

@@ -0,0 +1,141 @@
+# Every group diagonal has exact scalar-rank cost d
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+Claim type: scoped written algebraic proof with exact finite corroboration.
+
+In Ali Romman's [#5394](https://github.com/CrocSwap/integer-mult-bounds/pull/5394)
+formal group-gate model, let d count the nonidentity entries of a diagonal
+target, with repetitions counted by position. For every field and every
+group, finite or infinite,
+
+```text
+minimum total projector rank = minimum rank-one call count = d.
+```
+
+Equality assumes each target label is an allowed paid label. The lower
+bound needs no such assumption. Arbitrary finite scalar workspace,
+rectangular or singular free scalar maps, copying, reset and discarded
+garbage do not lower the bound. Dirty inputs may be arbitrary; the attaining
+coordinate construction restores them.
+
+[PROOF.md](PROOF.md) proves that all nonidentity coefficient images of a
+circuit lie in one scalar space of dimension at most the total paid rank.
+The diagonal target needs exactly d scalar directions. No finite group
+representation, characteristic assumption or inverse free map enters the
+proof. The lower bound even permits nonidempotent paid couplings.
+
+This closes #5394's four-or-more-target rank-one question. Its unit-price,
+arbitrary-rank invocation optimum remains the credited subproduct-cover
+number. Rank-one count exceeds that optimum exactly when the cover number
+is below d. The prime-exponent and coprime cyclic cases of Nick Petalas's
+older #6008, and the binary semilinear case of Krzysztof Wojt's #5242,
+retain their prior credit. We do not replay those results.
+
+## Reproduce
+
+From the repository root, with CPython 3.12 and the standard library:
+
+```sh
+/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
+```
+
+Another CPython 3.12 path can replace the absolute local path. The direct
+command prints `PASS_ALL_GROUP_DIAGONAL_RANK` inside a generated JSON
+receipt bound to all six package-file hashes. Both registered commands run
+the full finite corroboration. The publication check requires the committed
+package and full history. No receipt is handwritten or stored as an input.
+
+The checker constructs new circuits over C4, C6 and S3, over F2, F3 and F5.
+It checks the transported common image, the rank charge and the complete
+regular-action matrix against separate ordinary matrix multiplication.
+A literal enumeration of all row combinations independently checks every
+circuit's coefficient rank. Direct diagonal words include repeated labels,
+identity targets, the three-copy order-two target in C4, and two arbitrary
+restored dirty roles. Normal and optimized execution use explicit exceptions.
+The receipt reports the executed counts. These finite checks corroborate
+the written proof; they do not establish its universal quantifiers alone.
+
+Local CPython 3.12.15 runs pass 216 new circuits with 540 paid gates,
+561 rectangular free maps and 79 singular square free maps. All 57,024
+regular-matrix entries agree, and 133 circuits have positive coefficient
+rank. The 54 direct endpoint fixtures cover 1,512 regular basis columns,
+including 36 fixtures with repeated labels. These counts include fixture
+occurrences rather than distinct maps across the complete run.
+
+Eight controls distinguish repeated positions from distinct labels,
+unit-price invocations from rank charges, forbidden free address maps,
+free singular scalar maps, invalid idempotents, noncommutative order,
+omitted calls and characteristic-two cancellation. The fixed seeded circuits
+are probes, not an exhaustive search of circuit words.
+
+## Sources and scope
+
+Base is canonical main `e54523517d0f03e58352e647c403a5af3e525a57`, priority
+revision 8, selected #7000 unchanged. The selected source-binding baseline
+passed with `PASS_RESEARCH_BASELINE_BINDINGS_ONLY`. It was orientation only.
+[TASK.json](TASK.json) records the change from the bit-new-register-model
+card to this formal all-group side result. [SOURCES.json](SOURCES.json)
+contains provenance-only pins; the verifier has no external scientific inputs.
+
+Ali Romman #5394 supplies the model, cover theorem, triple result and open
+question. The coefficient-span method has precedent in Arham Tahir #1919
+and the retained clean-workspace image-span reduction. Preserve the group
+model lineage of Cinna Davis, JoyboyBrian and their cited register-model
+predecessors. The new contribution is the rectangular common-image proof
+and its complete arbitrary-group application, not a new general invention
+of coefficient-span methods. Predecessor scientific suites are not replayed.
+
+The advance [CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19540700)
+precedes the new verifier. Main and merged object/formula searches, open PR
+bodies, recent account work, active Discussions and local reservations were
+checked. The overlap cache covers 502 open PRs and 7,179 Discussion records;
+its local note coverage is sparse. All-main Git searches cover the relevant
+omitted README texts. These are bounded overlap checks, not proof of novelty
+against unpublished work or every historical diff.
+
+Formal coefficientwise equality, fixed schedules and scalar free maps are
+essential. A quotient address representation, free address operation or
+data-dependent control changes the model. This result prices no native
+group action, physical caller, frame conversion, source access, precision,
+tape movement, hosting or complete recursive invoice. No new kappa,
+supplier admission or selected-frontier change is claimed. Selected cold
+replay, Lean and Docker are unrun. Independent human and formal proof-kernel
+review are unclaimed.
+
+## Code constraints
+
+The standalone checker has no recursion, subprocess, network call or file
+mutation. Circuit widths are at most four, words have at most four gates,
+groups have at most six elements, and the row-space oracle has at most
+three rows and 125 combinations. Diagonal fixtures have at most seven
+registers including the two dirty roles, so regular matrices have at most
+42 rows and columns. All functions are shorter than sixty physical lines.
+Every loop ranges over these fixed domains or a collection they bound.
+
+Power of Ten rule 3 has a managed-allocation deviation for this one-shot
+CPython checker. Live state is bounded by the displayed shapes, at most
+six coefficient matrices per formal product, and one row-space set of at
+most 125 vectors. Runtime and standard-library allocation cannot be fixed
+statically. A deployment requiring allocation-free operation would need
+fixed buffers; this verifier claims no such deployment. Warning-strict
+development-mode normal and optimized checks provide runtime diagnostics.
+The rank-elimination and literal-row-space algorithms are separate.
+Source compilation and function-size inspection are part of local checks.
+
+## Open next questions
+
+Can a specified native address quotient escape this formal coefficient
+bound and still improve the complete supplier bill? Begin with one exact
+representation and a new target whose formal coefficient images collapse
+in that representation. A paid native implementation, dirty restoration,
+precision and complete caller charges remain the blockers. The current
+theorem does not price such a quotient or reserve a follow-up.
+
+For a fixed rank cap and positive invocation overhead, which subproduct
+covers minimize the full rank and invocation bill together? Begin with one
+four-target mixed-order example and retain both charges for each gate.
+The present d bound and the predecessor's invocation optimum need not be
+attained by the same word. Physical realization remains separate.

research/all-group-diagonal-rank/SOURCES.json

@@ -0,0 +1,54 @@
+{
+  "schema_version": 1,
+  "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "75d77b328ea02ded535e7f23aee5b1e55d0bb1a8",
+      "sha256": "154c3d30455d778fd3343b6b4851f0fa4665f0f7625b0adb3675e2bafbbf6bf1"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/bit-clean-workspace-compression/README.md",
+      "usage": "provenance",
+      "git_blob": "bd752384cc1061d912bbb49c970ba4a4d8aef00d",
+      "sha256": "ca2cc91629ccb36475cd38f9d8c13719d3b2742d96080653b545a45b5d991885"
+    },
+    {
+      "path": "research/group-subproduct-cover/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "308e63dcc668b0089b4a0c5152dda0733b01fed5",
+      "sha256": "7392dca9e7258dcdb4802a3c9f60cd8e5ccced271950a4ce2e4823f449586c00"
+    },
+    {
+      "path": "research/group-subproduct-cover/README.md",
+      "usage": "provenance",
+      "git_blob": "36faba920c546d36f3a51a026e8e84d925acf723",
+      "sha256": "b9241c29301d2d20af35fe9f09ff2b0e7e7aca0566394b8e4c7708924e59d161"
+    },
+    {
+      "path": "research/prime-exponent-rank-cut/README.md",
+      "usage": "provenance",
+      "git_blob": "a23cf9be5d5ec8b258156b7925a9349fe6bef8b3",
+      "sha256": "4e1936de8546a3ac91f58cb5176f11a2b35d7a1093814794b35622bd97347db7"
+    },
+    {
+      "path": "research/ut3-rank-bounded-block-calls/README.md",
+      "usage": "provenance",
+      "git_blob": "dc0d1bac91fcebecc9fed4e8c3d26a11acca3ef5",
+      "sha256": "822574c7040b5571d729960951425a1ad9742ae8541a2af2882733f952975b5d"
+    },
+    {
+      "path": "research/semilinear-mixed-tariff/README.md",
+      "usage": "provenance",
+      "git_blob": "dc95473ba57ec799194c33fc030f1f82dba484d2",
+      "sha256": "edecd78f1ab2661ac4115c09cd7b47d06274672f4a6a7a20202d9b5812a84c80"
+    }
+  ]
+}