DONE: exact mixed-target semilinear tariff and optimal-word rigidity (#5242)

[krzysztofwojt]

DONE / 2026-10-23 13:53 UTC / priority revision 7

PR #5242, exact head 8fbd8d3a8fdea5c9fc4cf4c529ea43ccc7570917, completes the claimed result. Both jobs in hosted CI run 39964111143 passed: planning in 4m07s and the sole selected package replay in 1m31s. Run metadata confirms this exact head and successful completion at 13:53:04 UTC. The claim is released; no follow-up topic is reserved. CI execution is separate from independent scientific acceptance.

Scoped written proof: for every odd prime p, every diagonal target with w nonidentity entries in the full formal F2[C_(2^p-1) semidirect C_p] Frobenius model has exact unit-price rank-one-idempotent call minimum w, with arbitrary finite restored dirty workspace and free binary scalar mixing. At p=3 this closes the mixed-target question in Nick Petalas's #5202. A quotient character added to the natural representation gives constant displacement rank p. Coordinate calls attain the full formal endpoint.

The equality argument additionally proves that, after scalar normalization, every optimal paid projector is supported only on target roles of its own normal/outside type, with no support on restored identity roles. This concerns normalized factors; free maps may mix dirty workspace, and noncoordinate projectors within a type are allowed.

Local normal/optimized and registered replay, metadata, committed-byte/source-history checks, export integrity and read-only Git-free replay all pass, and were rechecked on 2026-10-23 at 13:45 UTC with identical receipts. Exact finite evidence includes 328,000 complete two-call formal words, 1,600 realized endpoints (672 mixed), 6,372 paid displacement matrices, 4,704 scalar covariances, and all 105 basis inputs of a five-register mixed example. Hypothesis controls and three additional source corruptions reject in both modes. Universal quantifiers rest on PROOF.md, not finite extrapolation.

python3.12 -B scripts/research_package.py --package research/semilinear-mixed-tariff

Scientific base: ec2780e8aeb1c88acaf5e9e470ef8c68e7fbbb6c. Current main was refreshed at ff3cc58e370d0f678e529246f8c73e8094e18fcf with no guidance, priority or selected-record change. The final 13:44–13:46 UTC overlap refresh covers 308 open PRs, 4,515 closed PRs, 4,480 Discussion records and all 6,998 local HEAD notes, plus direct current #1166/#5202/#5230 reads. No competing same-scope result was found; unpublished work and arbitrary historical diffs remain outside coverage. #5202 is merged and its cited proof is unchanged. No rebase was required.

Credit: Nick Petalas #5202 (99ed6d2fc13101cb5ec0d3b1cdc826b75bc27fc7) for the normal-C7 theorem, F8 rank budget and explicit mixed-target handoff; 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 inventory and a separately implemented finite checker inspected, corrected and rerun by the primary agent. Apache-2.0. Independent human and proof-kernel review are unclaimed.

No native supplier, new kappa, selected-frontier change or complete multiplication theorem. Native realization, physical restoration/routing, ownership, frames/hosting, precision, stock/compiler and complete recursive/outer prices remain unknown. Nonuniform tariffs and composite degrees are explicit unreserved next questions in the package. The delivered scope matches the claim; the earlier all-normal theorem and orbit census are cited rather than rerun as the contribution.

Original claim

CLAIM — mixed targets in prime-degree binary semilinear groups

Status: investigating; evidence LOCAL-ONLY. Claim expires 2026-10-23T15:10:00Z. Priority revision 7; fresh canonical main ec2780e8aeb1c88acaf5e9e470ef8c68e7fbbb6c.

I am taking the explicitly released mixed-target question in Nick Petalas's PR #5202, head 99ed6d2fc13101cb5ec0d3b1cdc826b75bc27fc7, and handoff. For the full formal F2[C7 semidirect C3] model, can any mixed list of nonidentity normal and outside targets share fewer paid rank-one idempotent calls than its number of targets, with arbitrary finite restored dirty workspace and free binary scalar mixing?

The proposed new implication combines the predecessor's F8 rank budget with the quotient-C3 character. I will seek an exact all-target tariff, and, if rank equality supports it, the support restrictions on optimal normalized words. The same argument will be examined for C_(2^p-1) semidirect C_p with odd prime p and Frobenius action. First fixtures are the mixed order-21 pair and p=5. The prior all-normal theorem and three-role census are credited premises, not audit deliverables.

Expected artifact: one self-contained scoped proof and a bounded exact standard-library verifier, including literal full formal endpoints, arbitrary-dirty basis fixtures and hypothesis/mutation controls. Stop after the first substantive theorem or a precise falsification of this route; no physical construction campaign. This changes the bit-new-register-model card to the open mixed-target algebraic boundary. Native realization, routing, ownership, frames, precision, stock/compiler and the complete recursive bill remain unknown; no new kappa or selected-frontier change is intended.

Value/overlap: the predecessor explicitly leaves mixed targets open. Fully paginated cached coverage includes 344 open PRs, 4466 closed PRs, 4453 Discussion records and 6996 main notes, followed by fresh live open-PR bodies and latest handoffs immediately before this claim. No competing mixed order-21 or prime-degree semilinear tariff appeared. All recent krzysztofwojt scopes, including the active fifteen-owner six-cycle investigation, are excluded. Arbitrary historical diffs and unpublished work remain coverage limits.

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. Apache-2.0; independent human and proof-kernel review unclaimed.