[aliromman]

Every triple of distinct nonidentity group labels has exact rank-one call count three over every field, even with arbitrary finite scalar workspace and fixed free scalar linear maps. This extends the earlier finite order-21 and Q8 minima beyond their register and field restrictions. It is a written theorem in the formal group-algebra model with all nonidentity labels allowed. The complete kappa calculation does not change.

The proof first gives an exact criterion for arbitrary-rank unit gates: the target labels must fit in the ordered subproducts of one paid label word, and diagonal projectors realize every such cover. Free scalar maps, including singular maps, copies, clears and changes of register dimension, cannot add a group label to the support. For three distinct labels, two calls are possible precisely for a triple {g,h,gh}. The two coefficient cuts then show that any such realization needs rank at least two in each projector. Thus rank-one count and total rank-charged cost are both exactly three; the two-call construction costs at least four rank units.

For the actual order-21 target diag([a],[a^2],[a^4]), no pair product is the remaining target, so even arbitrary-rank unit gates need three calls. For Q8, diag([i],[j],[k]) takes two rank-two gates because ij=k, while its rank-one minimum remains three with all the added scalar resources. These statements distinguish the larger resource class from the predecessor alphabets. Formal group algebra, or its faithful regular action, is required: a 14-term nonzero formal element in the order-21 group acts as zero in its faithful seven-point group representation.

The exact receipt and source pins bind the bounded checks. The primary verifier uses sparse integer group-algebra matrices. The separate replay imports no primary code and uses permutation/quaternion group encodings and regular-action columns. Both classify every distinct nonidentity triple: C7 has 12 two-call and 8 three-call cases; C7 semidirect C3 has 348 and 792; Q8 has 11 and 24. All 1195 records agree, with 121800 regular columns including two dirty registers. The primary also checks 216 full-cover constructions, 96 scalar interleavings, 96 coefficient-cut cases and 12 scope controls. These finite checks corroborate the quantified proof; they are not its unbounded premise.

With Python 3.12 and the standard library, run from the repository root:

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:

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

Registered normal/optimized CPython 3.12.13 checks and optimized CPython 3.14.7 checks pass. The committed-byte preflight and official 11-file export pass; the committed-diff planner selects only this package. Both scripts pass normal and optimized runs in a fresh Git-free export, with all 12 files including transport metadata unchanged. Seven optimized rejection runs detect a source change, a typed receipt change, a changed census count in both engines, a broken group law, a coefficient-cut sign change and a quaternion-order change. Receipt overwrite is also rejected. git diff --check passes. No predecessor full census, selected native/whole-supplier, full-history, Lean, Docker, independent human or formal-kernel replay was run for this contribution.

The unit price of a high-rank gate and free scalar maps are explicit optimistic assumptions. Physical group gates, source access, scalar work, frame conversion, precision, children, hosting and cleanup remain unpriced. The rank-one conclusion concerns three distinct nonidentity labels with an unrestricted group alphabet; it does not prove longer-word rank-one additivity, handle data-dependent control or permit free address maps. No native supplier or selected-frontier change is claimed.

Base: 1ec1119972c9aefe42525172d07b332fcff81cb4, priority revision 7. The canonical claim records the changed premise and overlap. Credit OpenAI Codex at Cinna's direction for PR #2011 and the order-21 target and census; Cinna Davis for the Q8 census and rank-one model; and JoyboyBrian for the explicit all-workspace subword-support argument, with its retained predecessor lineage. The support expansion is prior work. The new contribution is the joint-cover converse in the relaxed class, the sharp two-call rank cuts and these uniform triple consequences. No literature-priority claim is made. Ali Romman with substantial OpenAI Codex assistance; Apache-2.0.

[jwr404]

Independent review (jwr404). Base: upstream/main 1ec1119.

Replay.

• python3.12 -B scripts/research_package.py --package research/group-subproduct-cover gives PASS_REGISTERED_RESEARCH_PACKAGE … outcome=completed.
• python3 -I -O -B independent.py (CPython 3.15.1) gives PASS_INDEPENDENT_SUBPRODUCT_COVER triples=1195 regular_columns=121800.

Census, recounted from scratch. My script is about 30 lines and uses none of the package code. It encodes C7 additively, C7⋊C3 as pairs (i,j) with b^j a^i = a^(i·2^j) b^j, and Q8 as unit quaternions. A triple counts as two-call when some ordered pair of distinct members has its product as the third member. Results:

• C7: 12 two-call, 8 three-call.
• C7⋊C3: 348 two-call, 792 three-call.
• Q8: 11 two-call, 24 three-call.

The total is 20 + 1140 + 35 = 1195, matching the package, and the order-21 target (a, a², a⁴) has no such pair.

Proof (PROOF.md), checked line by line. I find no gap.

• §2 lower bound. Expanding C₀D₁C₁⋯D_kC_k gives terms whose labels are ordered subproducts, and scalar matrices only multiply coefficients. The argument needs neither invertibility nor idempotence. Restricting to the data rows and columns handles workspace and dirt, because the free maps are fixed and do not depend on the data. Upper bound: the diagonal 0/1 masks are idempotent over every field, as stated.

• §3. Two calls give support {e, g₁, g₂, g₁g₂}, so three distinct nonidentity targets force targets = {g₁, g₂, g₁g₂}. The non-degeneracy conditions are automatic: g₁ ≠ g₂ because the targets are distinct, g₂ ≠ e, and g₁g₂ ≠ e.

• §4 rank cut. I re-derived the four coefficients:

  • A_e = C₀(I−N)C₁(I−M)C₂
  • A_g = C₀NC₁(I−M)C₂
  • A_h = C₀(I−N)C₁MC₂
  • A_gh = C₀NC₁MC₂

  These give A_g + A_gh = C₀NC₁C₂ and A_h + A_gh = C₀C₁MC₂. On the data block each sum is a 0/1 diagonal with two ones, so it has rank 2 over every field. Since rank(XNY) ≤ rank N, both rank N ≥ 2 and rank M ≥ 2. The rank-charged corollary then follows. Total rank ≤ 2 leaves at most two nonzero gates, and these need rank ≥ 2 each, giving at least 4 > 2.

• §6 faithfulness example. Under x ↦ 2^j x + i, the subgroup ⟨a⟩ and the coset ⟨a⟩b each sum to the all-ones 7×7 matrix, so the 14-term difference acts as zero. Correct.

Scope. The scope statement is accurate. One relation to existing results may be worth a sentence. The §2 cover theorem with L restricted to coordinate CNOTs gives a lower bound on arbitrary-rank unit-cost gates. For the rank-one CNOT-alphabet targets (#5005, #5292, #5379), that bound is well below the exhaustive minima. For example, diag([c],[c]) at n=4 costs 12 rank-one calls, while one 6-CNOT word for c already covers both entries, so c_L ≤ 6. So the theorem does not supersede those searches, and they do not contradict it. As the PR says, the extension to four or more labels or a restricted alphabet remains open.

Verdict: correct as a scoped theorem in the stated optimistic model (unit-cost high-rank gates, free fixed scalar maps, unrestricted alphabet). No κ is claimed and none is affected.