Prove the all-group rank-one triple floor with free scalar workspace

research/group-subproduct-cover/PROOF.md

@@ -0,0 +1,182 @@
+# Ordered subproducts determine the relaxed gate count
+
+Ali Romman, with substantial OpenAI Codex assistance. Apache-2.0.
+
+## 1. Exact model
+
+Let K be any field and G any group, with identity e. Use the formal group
+algebra K[G]. Its basis elements [g] are linearly independent, also when
+K has positive characteristic. Matrices act on column vectors on the left.
+Products below are in matrix order; the rightmost factor acts first.
+
+A circuit has finitely many registers. Free operations are fixed matrices
+with entries in K, tensored with the identity address action [e]. They may
+change the register count, be singular, copy inputs, discard registers, or
+set registers to zero. They cannot depend on the input data or apply an
+address map. A paid gate on R registers is
+
+    D(N,g) = (I_R-N)[e] + N[g],     N in M_R(K), N^2=N.
+
+Each gate costs one, at every rank of N. The allowed group labels form an
+explicit set L. This is an optimistic relaxation of a rank-one gate model.
+In particular a rank-two projector costs one here, not two.
+
+The required data block is diag([t_1],...,[t_d]). Any extra clean or dirty
+workspace is finite. If dirt is present, the data block must be correct for
+all dirt, and the chosen upper construction leaves it unchanged. For the
+lower bound we even allow arbitrary changes to workspace. Thus a rule that
+requires restoration can only make the lower bound stronger.
+
+For a word w=(g_1,...,g_k) in L, define its ordered subproduct set
+
+    S(w) = {g_1^b_1 ... g_k^b_k : b_j in {0,1}}.
+
+This set always contains e. Define c_L(T) as the minimum k for which one
+such word has {t_1,...,t_d} contained in S(w). Set it to infinity if there
+is no such word. Repeated labels and repeated target entries are allowed.
+
+## 2. The exact cover theorem
+
+**Theorem.** In this model the minimum paid count for the diagonal target
+is c_L(T). Extra finite scalar workspace and free scalar maps do not lower
+it. A minimum cover has a construction on the data registers alone, with
+diagonal projectors and no free operations.
+
+**Lower bound.** Combine consecutive free maps. A circuit with k gates
+has a data block of
+
+    C_0 D(N_1,g_1) C_1 ... D(N_k,g_k) C_k,
+
+where the C_j are scalar matrices. Initial embeddings, final selections,
+and any zero workspace are included in the endpoint scalar maps. For dirty
+workspace, take the columns that correspond to data input. Rectangular C_j
+are permitted wherever the register count changes.
+
+Expand each paid factor into its two terms. Each summand is a scalar
+matrix times one basis element
+
+    [g_1^b_1 ... g_k^b_k].
+
+Scalar entries commute with all group-algebra entries. Matrix dimensions
+and the order of group labels are preserved in this expansion. The support
+of every output entry is therefore contained in S(w). Equal products can
+cancel, but cancellation cannot add a group label. Each target [t_i] has a
+nonzero coefficient on its own diagonal, so t_i must lie in S(w). This
+proves k >= c_L(T). Invertibility of the free maps is not needed. The same
+argument holds even without the idempotent condition on the paid N_j.
+
+**Upper bound.** For each target position i choose one mask b(i) whose
+ordered subproduct is t_i. For paid position j set
+
+    N_j = diag(b(i)_j : 1 <= i <= d).
+
+These are idempotents over every field. On data register i the j-th gate
+is [g_j] if b(i)_j=1 and [e] otherwise. The full product is [t_i]. All
+cross-register entries vanish. Extend every N_j by zero on any workspace;
+then every workspace register is restored without a read, copy or clear.
+The construction has exactly k declared gates. A zero projector can be
+deleted; if that happens in a shortest cover it contradicts minimality.
+This proves equality, including the infinite case.
+
+The expansion is the prior formal subword-support method. The result here
+uses the simultaneous target cover and supplies its converse in the stated
+arbitrary-rank unit-cost class. It does not assert a new general expansion
+identity or literature priority for subset-product methods.
+
+## 3. A sharp three-label decision
+
+Now let L=G without e, and take three distinct nonidentity target labels.
+Zero and one gate are impossible. Two gates have support contained in
+
+    {e,g,h,gh}.
+
+Thus two gates are possible exactly when the unordered target triple is
+{g,h,gh} for some ordered pair of distinct target members. The three
+nonidentity elements must be distinct; g=h or gh=e cannot cover the target.
+Conversely the cover theorem realizes this triple in two gates. In target
+order (g,h,gh), use
+
+    N_1 = diag(1,0,1),     N_2 = diag(0,1,1).
+
+If there is no such relation, three direct coordinate gates attain the
+lower bound. Therefore the exact count is either two or three. This is a
+proof for every field and group, not an extrapolation from the tables.
+
+## 4. Sharp projector ranks in a two-call realization
+
+In the two-call case the four labels e,g,h,gh are distinct. Write the data
+block as C_0 D(N,g) C_1 D(M,h) C_2. The coefficient matrices satisfy
+
+    A_g + A_gh = C_0 N C_1 C_2,
+    A_h + A_gh = C_0 C_1 M C_2.
+
+These follow by adding the two expanded terms and using (I-M)+M=I and
+(I-N)+N=I. Rectangular or singular scalar maps do not affect the identities.
+For the three-label diagonal endpoint, each left side is a diagonal matrix
+with exactly two entries equal to one, up to a data permutation. Its rank
+is two over every field. Matrix-rank subadditivity is not needed: the rank
+of a product is at most the rank of each factor. Therefore rank N >= 2
+and rank M >= 2. The diagonal construction in section 3 attains both bounds.
+
+**Corollary.** Every triple of distinct nonidentity group labels has exact
+rank-one gate count three, over every field, with arbitrary finite scalar
+workspace and fixed free scalar maps. In the unrestricted alphabet three
+direct coordinate gates attain the bound. A shorter word is either excluded
+by support or needs rank at least two in each of its two gates. If each gate
+is instead charged its projector rank, the exact total rank cost is also
+three. Zero-rank gates do nothing; total rank cost below three permits at
+most two nonzero gates and cannot implement the target. In a two-call
+implementation the total rank cost is at least four, so its smaller call
+count is not a saving under rank charging.
+
+This corollary extends both finite predecessor triple minima to arbitrary
+scalar workspace. It does not establish rank-one additivity for four or
+more target labels, repeated labels, or restricted address alphabets.
+
+## 5. Actual boundaries
+
+In G=C7 semidirect C3, use a^7=b^3=e and bab^-1=a^2. The predecessor target
+is (a,a^2,a^4). Products of two distinct members have exponents 3,5,6 modulo
+7. None is the remaining member. The exact count is three, over every
+field and with all the scalar workspace and paid projectors in section 1.
+Its direct gates have rank one. Consequently its old rank-one count three
+also survives arbitrary finite scalar workspace and free scalar maps.
+This removes those hypotheses as possible two-call escapes for this target.
+
+For Q8, i*j=k. The triple (i,j,k) therefore takes two rank-two gates here.
+The rank-cut corollary extends its earlier rank-one minimum three to all
+fields and arbitrary finite scalar workspace. The two-call rank-two result
+is not a rank-charged saving. In particular the
+symbol [-k] is a different group basis element from [k], even in F2[Q8].
+Reversing the two gate labels changes the third target to [-k].
+
+With three distinct targets, the theorem can give more than the maximum
+individual address word length. In the unrestricted alphabet each separate
+nonidentity target has word length one; the order-21 triple still costs
+three. The single-target support floor alone does not give this conclusion.
+
+## 6. Faithful action and cost limits
+
+A regular action of K[G] is faithful: apply a group-algebra element to the
+basis vector at e to recover its coefficients. For infinite groups use the
+space of finitely supported vectors. Thus the proof also applies to exact
+regular-action endpoints. A group representation that is faithful on group
+elements need not be faithful on their linear combinations.
+
+For the order-21 group, the natural action x -> 2^j*x+i on seven addresses
+is faithful as a group action. However,
+
+    sum_(i=0)^6 [a^i] - sum_(i=0)^6 [a^i b]
+
+is a nonzero formal element and acts as zero in that seven-dimensional
+permutation representation: each sum acts as the all-ones matrix. The
+regular action detects it over every field. A natural matrix check cannot
+replace the formal endpoint used by the theorem.
+
+The proved bill is an abstract gate count. Scalar maps are free by an
+explicit relaxation; physical source access, scalar maps, high-rank gates,
+frame conversion, precision, recursive children, hosting and cleanup are
+not priced. The upper construction needs no workspace, but no native
+supplier realizes these arbitrary group gates here. No complete kappa
+calculation changes. Data-dependent control, free address operations and
+unfaithful address representations are outside the theorem.

research/group-subproduct-cover/README.md

@@ -0,0 +1,161 @@
+# Exact subproduct covers with arbitrary scalar workspace
+
+**Written formal-model theorem; no new kappa.** For any field and group,
+the paid count for a diagonal tuple of group labels equals its minimum
+ordered-subproduct cover, in the arbitrary-rank unit-gate model below.
+Extra finite workspace and arbitrary free scalar maps cannot lower this
+count. Diagonal projectors attain every cover without workspace.
+
+For three distinct nonidentity labels, with every nonidentity group element
+allowed as a paid label, the exact count is two if the triple is `{g,h,gh}`
+for some ordered pair. It is three otherwise.
+
+The actual order-21 target `diag([a],[a^2],[a^4])` still costs three. Unlike
+the earlier finite census, this conclusion allows every field, any finite
+scalar workspace, singular free scalar maps, and paid projectors of any
+rank. The old rank-one minimum three therefore also survives those free
+scalar resources. In contrast, the Q8 target `diag([i],[j],[k])` takes two
+rank-two gates here. Its old rank-one minimum does not transfer to this
+larger gate class.
+
+[PROOF.md](PROOF.md) gives the quantified theorem, converse construction,
+resource boundary and two examples. [RESULT.json](RESULT.json) holds the
+recomputed finite receipt; [SOURCES.json](SOURCES.json) pins the three
+predecessor notices and the historical assignment. The finite tables support
+the written proof; they do not establish its unbounded quantifiers alone.
+
+A coefficient-rank argument also proves that any two-call realization of a
+three-label target needs rank at least two in **each** projector. Therefore
+every triple of distinct nonidentity labels has exact rank-one call count
+three, over every field and with arbitrary finite free scalar workspace.
+Its exact rank-charged cost is also three. The two-call construction costs
+at least four rank units.
+
+## Model and complete scope
+
+Work in the formal group algebra `K[G]`. A paid gate is
+`D(N,g)=(I-N)[e]+N[g]`, with `N^2=N`. Its cost is one at every rank of N.
+Free maps are fixed scalar linear maps, with no address action. They may
+change dimension, copy, clear or discard registers. Data-dependent control
+and free address operations are outside this class. Group labels are formal
+basis elements; a regular action preserves the theorem, but an arbitrary
+natural representation need not preserve it.
+
+For a paid word `(g1,...,gk)` in matrix order, all endpoint support lies in
+`{g1^b1 ... gk^bk : bj in {0,1}}`. This is the inherited support method.
+The new exact criterion requires one such set to contain all target labels.
+Conversely, choose one mask for each target and put those bits on the
+projector diagonals. This realizes all targets at once. Additional dirty
+registers remain untouched. Arbitrary-rank unit cost is an explicit
+optimistic relaxation, not an uncharged physical implementation.
+
+The proved bill is only this abstract count. Physical group gates, scalar
+maps, source reads, frame changes, precision, recursive children, hosting
+and cleanup remain unpriced. The three direct order-21 gates use rank-one
+projectors, but no native supplier is supplied. The complete multiplication
+exponent and selected frontier are unchanged.
+
+## Exact finite evidence
+
+Two implementations classify every unordered triple of distinct nonidentity
+labels in each listed group. They agree on each triple, not only the totals.
+
+| Group | Triples | Minimum two | Minimum three | Regular columns, including two dirty roles |
+|---|---:|---:|---:|---:|
+| C7 | 20 | 12 | 8 | 700 |
+| C7 semidirect C3 | 1140 | 348 | 792 | 119700 |
+| Q8 | 35 | 11 | 24 | 1400 |
+
+The primary uses group multiplication tables and sparse integer group-algebra
+matrices. It checks all 1195 constructed endpoints over the integers, so
+those identities reduce to every field. It also checks 216 complete covers
+from three-letter C7 words and 96 scalar interleavings over F2, F3 and F5,
+including rectangular endpoint maps, singular free maps and dense rank-two
+projectors. Another 96 cases check the two coefficient-cut identities and
+rank bounds with singular free maps over the same three fields.
+
+The separate implementation imports no primary code. It obtains C7 and the
+order-21 group from permutations of seven points, Q8 from signed quaternion
+multiplication, and the triple criterion from ordered pairs inside each
+triple. It then checks all 121800 columns of the **regular** action, including
+two independent dirty registers. The seven-point action is used to encode
+group elements, not to accept formal linear combinations.
+
+Twelve in-verifier controls cover rank-two Q8 construction, reversed order,
+group versus scalar signs, dirty return, omitted or changed gates, dirty
+endpoint changes, uncovered targets, invalid projectors, empty/repeated
+targets and a natural-action alias. That alias has 14 nonzero formal terms
+but vanishes in the faithful seven-point group representation. This shows
+why faithfulness on group elements is not enough for a group-algebra test.
+
+## Reproduce
+
+Python 3.12 and the standard library, from the repository root:
+
+```sh
+python3 -B scripts/research_package.py --package research/group-subproduct-cover
+python3 -I -O -B research/group-subproduct-cover/verify.py
+python3 -I -O -B research/group-subproduct-cover/independent.py
+```
+
+Expected final markers:
+
+```text
+PASS_GROUP_SUBPRODUCT_COVER triples=1195 order21_min=3 q8_relaxed_min=2 controls=12 no_new_kappa
+PASS_INDEPENDENT_SUBPRODUCT_COVER triples=1195 regular_columns=121800 no_new_kappa
+```
+
+Both scripts are read-only by default and use no network or Git. The primary
+checks live source bytes by SHA256 and Git blob digest. Receipt comparison
+preserves JSON types. The optional `--write-receipt` creates a missing receipt
+and refuses overwrite. Exported source files must remain at their declared
+repository-relative paths. The registered runner checks provenance separately.
+
+No predecessor circuit census, selected native/full supplier, full-history,
+Lean, Docker, independent human or formal-kernel verification is claimed.
+The selected source-bound baseline passed at the base; that is not admission.
+
+## Current priorities, overlap and credit
+
+Base `1ec1119972c9aefe42525172d07b332fcff81cb4`, priority revision 7. The
+`bit-new-register-model` scope changes the projector rank, field and free
+workspace premises. This is a bounded structural screen, not a larger search
+inside the old 560-operation alphabet. The complete cost boundary above is
+its family decision: finish the exact criterion and stop; unknown physical
+costs do not become zero.
+
+The [canonical claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1167#discussioncomment-19154784)
+records the premise change and stop rule. The preclaim overlap scan covers
+338 open PRs, 4677 Discussion records and all 7267 base HEAD notes, with
+complete pagination at 21:17–21:18 UTC on 2026-10-23. Exact joint-cover and
+ordered-subproduct terms, the order-21 scope, and the nearby scalar-workspace
+proofs were checked. This is text coverage, not proof of novelty or a scan
+of unpublished branches and all diffs.
+
+Credit the following material predecessors:
+
+- OpenAI Codex at Cinna's direction: [PR #2011](https://github.com/CrocSwap/integer-mult-bounds/pull/2011)
+  and its [order-21 source](https://github.com/CrocSwap/integer-mult-bounds/blob/1ec1119972c9aefe42525172d07b332fcff81cb4/research/bit-semidir21-orbit-seed8f89/README.md)
+  supply the target, group and original finite rank-one minimum.
+- Cinna Davis: the [Q8 source](https://github.com/CrocSwap/integer-mult-bounds/blob/1ec1119972c9aefe42525172d07b332fcff81cb4/research/bit-q8-three-register-two-call-seed189ad74/README.md)
+  supplies the rank-one comparison and its operation boundary.
+- JoyboyBrian: the [three-cycle source](https://github.com/CrocSwap/integer-mult-bounds/blob/1ec1119972c9aefe42525172d07b332fcff81cb4/research/three-cycle-address-floor/README.md)
+  gives the explicit all-workspace formal subword-support argument. Its
+  single-cycle CNOT theorem and retained contributor lineage remain prior work.
+
+The new contribution is the simultaneous cover converse in this relaxed
+class, the all-field workspace extension for the actual order-21 target,
+the sharp two-call projector-rank bound, and the independent complete triple
+classification. It does not claim
+invention of group-algebra support expansion or literature priority.
+Prepared by Ali Romman with substantial OpenAI Codex assistance. Apache-2.0.
+
+## Open next questions
+
+For four or more distinct targets, when does rank-one cost exceed the relaxed
+subproduct-cover cost after arbitrary finite scalar workspace is allowed?
+First specify one target and group, then derive coefficient cuts that remain
+valid when ordered subproducts collide. The two-call rank proof relies on
+four distinct labels and does not establish a longer-word invariant. A larger
+census alone would not close the unbounded workspace question. Physical gate
+realization and a complete supplier cost remain separate missing work.

research/group-subproduct-cover/RESULT.json

@@ -0,0 +1,50 @@
+{
+  "actual_order21_minimum": 3,
+  "controls": [
+    "dirty_return",
+    "Q8_rank_two",
+    "Q8_reversed_order",
+    "group_sign",
+    "deleted_gate",
+    "changed_label",
+    "dirty_mutation",
+    "uncovered_target",
+    "non_idempotent",
+    "natural_alias",
+    "empty_cover",
+    "repeated_target"
+  ],
+  "full_cover_constructions": 216,
+  "groups": {
+    "C7": {
+      "records_sha256": "4eb44c0f7642c4ec5160b62e8d2683f38cd68f9ece3f393e4772f06d67bc7ce1",
+      "regular_columns": 700,
+      "three_calls": 8,
+      "triples": 20,
+      "two_calls": 12
+    },
+    "C7:C3": {
+      "records_sha256": "40182c48a10dfbd5913ad4a286cbbbe0d15416ffcf208c8e3849c886c607de0a",
+      "regular_columns": 119700,
+      "three_calls": 792,
+      "triples": 1140,
+      "two_calls": 348
+    },
+    "Q8": {
+      "records_sha256": "0cb3e996f8f6a9f308dd9b2990fce39c67590a7bbd2939d5c11cf7acf4cfb313",
+      "regular_columns": 1400,
+      "three_calls": 24,
+      "triples": 35,
+      "two_calls": 11
+    }
+  },
+  "integer_formal_endpoints": 1195,
+  "q8_relaxed_minimum": 2,
+  "rank_cut_cases": 96,
+  "rank_one_triple_minimum": 3,
+  "scalar_interleavings": 96,
+  "schema": "group-subproduct-cover/1",
+  "scope": "Written all-field/all-group cover proof; finite replay corroborates it; no new kappa",
+  "source_inputs": 3,
+  "two_call_projector_rank_floor": 2
+}