[krzysztofwojt]

Change and mathematical scope

PR #5202 leaves mixed normal/outside targets open in the order-21 register model. This package proves exactly one paid call per nonidentity diagonal target, for any target mixture, any finite restored dirty workspace and free binary scalar mixing. It also proves optimal-word rigidity: after scalar normalization, each paid projector is supported only on target roles of its own type; no normalized optimal factor touches a restored identity role.

The same self-contained proof covers every odd prime p in F2[C_(2^p-1) semidirect C_p] with Frobenius action. A quotient character added to the natural representation gives displacement rank p for every nonidentity label. Rank telescoping supplies the lower bound; coordinate calls attain the full formal endpoint. The p=3 all-normal theorem remains Nick Petalas's credited result, rather than a new audit claim.

Status: scoped written proof with exact finite corroboration. This is a unit-price formal algebra theorem, not a physical supplier, complete multiplication theorem or new kappa. Native realization, ownership, routing/restoration implementation, frames, precision, stock/compiler and full recursive/outer costs remain unknown. The selected frontier and frozen predecessors are unchanged.

Task and overlap

• Scientific base: fresh canonical main ec2780e8aeb1c88acaf5e9e470ef8c68e7fbbb6c, priority revision 7. Claim and canonical status #5230, handoff #1166.
• Card bit-new-register-model, scope changed to Prove the exact order-21 normal-subgroup call tariff (no new κ) #5202's released mixed-target boundary. This closes call-sharing feasibility in the stated family before any native implementation effort. The exact original card and boundaries are in TASK.json.
• Nearest predecessor: Prove the exact order-21 normal-subgroup call tariff (no new κ) #5202 at 99ed6d2fc13101cb5ec0d3b1cdc826b75bc27fc7; its natural-C7 theorem and rank representation are retained with credit. research: bound order-21 three-register orbit word #2011 at b971a6c68d6f60c2693b2057ecf3489efb75efc4 supplies the order-21 model and finite orbit census. Neither predecessor's code/census is imported or rerun as this contribution.
• Final paginated overlap on 2026-10-23 at 13:44–13:46 UTC: 308 open PRs, 4,515 closed PRs, 4,480 Discussion records, and all 6,998 notes at the publication head. Direct live PR/Discussion reads, including Handoffs and requests for independent checks #1166, Prove the exact order-21 normal-subgroup call tariff (no new κ) #5202 and DONE: exact mixed-target semilinear tariff and optimal-word rigidity (#5242) #5230, agree. No competing mixed-target semilinear result appeared. Classify fifteen-owner equality graphs with six-cycles (no new κ) #5239 only mentions our claim as an excluded, unrelated same-account investigation; its fifteen-owner graph classification is untouched. Prove the A4 eight-call floor with arbitrary dirty workspace (no new κ) #5199/Prove four-call optimum for all even S4 pairs with every odd label #5203/Prove exact seven-call minima for 360 Dic3 targets (no new κ) #5205 concern different groups/alphabets/targets. Arbitrary historical diffs and unpublished work remain coverage limits.
• Canonical main was fetched again on 2026-10-23 at 13:44 UTC: ff3cc58e370d0f678e529246f8c73e8094e18fcf. Priorities, catalogue, selected record and entry guidance did not change. Prove the exact order-21 normal-subgroup call tariff (no new κ) #5202 is now merged, with byte-identical cited proof. The scientific base and frozen evidence remain pinned; the isolated addition does not require a rebase.

Validation

Publication head: 8fbd8d3a8fdea5c9fc4cf4c529ea43ccc7570917. Local CPython 3.12.12 on macOS arm64, standard library only. Normal/optimized direct and registered checks, metadata, source-history/committed bytes and the Git-free export were rechecked on 2026-10-23 at 13:45 UTC; receipts are identical to the earlier verified export.

• Exact finite fields: every label at p=3,5,7; all representation products at p=3,5, and left/right generator products at p=7. Actual finite-field elimination checks 6,372 paid tensor factors. All 4,704 GL3/idempotent covariances pass.
• A separately implemented full-formal checker examines 328,000 ordered two-call words, without rank-based pruning. All 1,600 two-target endpoints are attained, including 672 mixed ones, with zero optimal-support/type-count violations. It also checks a valid noncoordinate optimal word.
• A five-role regular-action replay checks all 105 basis inputs with dense free maps mixing the dirty role; all 21 dirty-role basis states restore. A changed paid label causes 21 endpoint mismatches.
• Built-in controls cover omitted representation blocks, incorrect group law, higher-rank paid gates, omitted outside budget, composite degree, p=2, dropped formal terms, wrong support and wrong endpoints. Three additional temporary source mutations—omitted character, corrupted support predicate and omitted free inverse—fail in both normal and optimized modes.
• Registered normal/optimized replay, metadata/pins and exact committed-byte/source-history checks pass. Official export integrity and read-only Git-free normal/optimized replay pass with identical receipts and all seven file hashes unchanged. Export SHA256: 1e92d240a7d9072da65addf29825d4eaec690a9f818dad40ee91d22e29eca6fe.

python3.12 -I -W error -B research/semilinear-mixed-tariff/verify.py
python3.12 -I -O -W error -B research/semilinear-mixed-tariff/verify.py
python3.12 -B scripts/research_package.py --package research/semilinear-mixed-tariff
python3.12 -B scripts/check_research_commit.py --package research/semilinear-mixed-tariff --check-source-history

Direct runtime is about one second, with a 60-second bound per registered command. Universal quantifiers rest on PROOF.md, not finite extrapolation. Independent human/proof-kernel review, native/selected cold replay, Lean and Docker are unrun.

Hosted CI passed for exact head 8fbd8d3a8fdea5c9fc4cf4c529ea43ccc7570917 in run 39964111143, completed 2026-10-23 at 13:53:04 UTC. plan passed in 4m07s; the sole selected package replay passed in 1m31s, including its registered normal/optimized commands. Run metadata confirms the matching head and successful conclusion. Passing CI is separate from independent scientific acceptance.

Credit

Nick Petalas #5202; Cinna Davis / 1337isnot1337 #2011 and #3893; eumemic #288 and the retained register-model lineage. Prepared by Krzysztof Wojt with substantial OpenAI Codex assistance, including bounded Luna overlap inventory and a separately implemented finite checker inspected, corrected and rerun by the primary agent. Apache-2.0. Exact source heads, the cited proof hash and baseline provenance are retained in the package.

Open next questions

The README and TASK list two unreserved questions: nonuniform normal/outside prices, starting with two normal targets and the three-outside-call relaxation; and composite degree nine, where the current single-character rank equalization fails. Neither is needed for this theorem. Physical expansion requires an explicit native contract and complete bill.

[jwr404]

Independent review (James Reed, with Claude Code). Head 8fbd8d3a8fdea5c9fc4cf4c529ea43ccc7570917.

Verdict: the proof is correct as stated. I found no gaps. This is a scoped formal-algebra theorem and does not change κ.

Proof read line by line

• Homomorphism. rho(a,j)(z) = a z^(2^j) is an F2-linear representation: rho(a,j)rho(b,k)(z) = a b^(2^j) z^(2^(j+k)), and the exponent is read mod p because z^(2^p) = z.
• Normal labels. rho(a,0) - I is multiplication by a - 1 ≠ 0, so its rank is p.
• Outside labels. The nonzero fixed points solve z^(2^j - 1) = a^(-1). Since gcd(2^j - 1, 2^p - 1) = 2^gcd(j,p) - 1 = 1, the power map permutes F^*, so there is exactly one solution. The kernel is {0, z0}, so the rank is p − 1. Primality of p is used exactly here.
• The character. chi(a,j) = zeta^j is a homomorphism. zeta exists in characteristic 2 because p is odd. Adding chi makes every displacement rank equal to p.
• Lower bound. Free scalar maps commute to the right via S D_N(g) = D_(SNS^-1)(g) S, and augmentation forces the leftover scalar to be I. Then rank(N ⊗ M) = rank M and subadditivity give L ≥ w.
• Counts. The split p c_N + (p-1) c_O ≥ p n + (p-1) m together with c_O ≥ m gives c_O = m and c_N = n at L = w.
• Rigidity.
  • Both telescoping inclusions are right: ΠA - I = Σ (A_i - I) A_(i+1)… for columns, and the mirrored expansion for rows.
  • The equal dimensions pL = pw force a direct sum, so each col(A_i - I) = x ⊗ col(R(g) - I) lies in ⊕_t e_t ⊗ col(R(g_t) - I).
  • Projecting to a role t with x_t = 1 gives the three exclusions as stated: an identity role, a normal call in an outside role (dimension p inside p − 1), and an outside call in a normal role (nonzero chi block). Rows and y are symmetric.

Independent finite check

I wrote a separate C census from the theorem statement only; none of the PR's code is used. It covers:

• G_p = Z/(2^p-1) ⋊ C_p with an explicit table and an associativity check;
• every nonidentity label and every rank-one idempotent;
• the full formal algebra.

For each target it enumerates all words of length w − 1 (expect none) and all words of length w. Every solution is checked for c_N = n, c_O = m, and x, y supported only on roles of the call's own type.

p	r	factors	target	solutions at w−1 / w	rigidity violations
3	3	560	N, O, e	0 / 2	0
3	3	560	N, N, e	0 / 2	0
3	3	560	O, O, e	0 / 2	0
3	3	560	O, e, e and e, N, e	0 / 1	0
3	3	560	N, O, O (w = 3)	0 / 6	0
3	3	560	N, N, O (w = 3)	0 / 18	0
3	2	120	N, O	0 / 2	0
3	2	120	O, O, same label (4,2)	0 / 6	0
5	2	924	N, O and O, O	0 / 2	0
5	3	4312	N, O, e	0 / 2	0

This independently corroborates the p = 5 family member and three-target cases with w = 3, which go beyond the PR's own census. The repeated-label case O, O with 6 optimal words includes non-coordinate projectors. That matches the PR's caveat that rigidity does not force coordinate projectors.

Replay

verify.py (with -I -O) prints PASS_SEMILINEAR_MIXED_TARIFF. scripts/research_package.py prints PASS_REGISTERED_RESEARCH_PACKAGE … outcome=completed. Both finish in about 3 s locally.

Optional notes

• A one-line remark would help readers who know Two coordinate 3-cycles cost twelve formal calls: exact search excludes length ≤ 11 (no new κ) #5005 and Bound two 3-cycles with a dirty third register below by eleven (no new κ) #5292 (GL3, coordinate CNOTs). Unit-price all-label alphabets with constant displacement rank make call counting tight, as here. In the restricted CNOT alphabet, displacement ranks undercount badly: a 3-cycle has rank bound 2 but costs 6. So rank telescoping alone does not transfer to that alphabet.

This review covers the stated scope only. It is not maintainer acceptance.