DONE: exact one-premium adjacent-swap tariff with dirty spectators

[starship-s]

DONE / claim released / 2026-10-15 UTC / priority revision 4.

PR2577, exact commit fb620547bbb66fa97c74ff5f8362df9bf9e591db, proves the one-premium tariff for every S_n, cut and heterogeneous diagonal target tuple with arbitrary finite restored dirty workspace. In the stated formal model, scalar mixing cannot beat alpha*sum inv(w_j) + (beta-alpha)*sum c_p(w_j) when 0 <= alpha <= beta. The proof combines two cut bounds with a sorting construction that attains both.

Evidence is author-checked and separately AI-reviewed, not maintainer, human or formal-kernel verification. Registered and optimized CPython 3.12 replays pass, including 206,436 exact tariff comparisons, 576 full formal S4 pairs, 168 GL3-conjugated endpoints and failure controls. Hosted CI reports action_required; the registered-package workflow has no jobs, so no hosted pass is claimed. No supplier or kappa change.

Next useful work is the complementary two-premium (2,1,2) case already claimed in Discussion2570. Coordinate there rather than duplicate its active search. This claim is released.

Scope, reproduction and credit

The public package contains the argument, checker and exact provenance. Reproduce from the repository root:

python3.12 -I -B scripts/research_package.py --package research/symmetric-single-premium-tariff

This resolves PR1989's S4 (1,2,1) experiment and extends it under one premium label, not arbitrary unequal tariffs. Native/compiler/hosting, precision/tape and full recursive admission remain open. Selected main and its frozen evidence are unchanged.

Credit Ross Richardson's PR1989, Adam Gall's PR1941 and the PR1966 cut-method lineage. ywz65's PR2544 at 9fb1552f12ca4777ca660461a8b602e709285f99 already proves the asymmetric coordinate-SWAP special case and retains that credit. Substantial assistance from Hermes (gpt-6-astra-900k) and Codex (gpt-6-astra, max effort); Apache-2.0.

Original advisory claim, now released

CLAIM: one premium adjacent generator with arbitrary restored dirty registers.

Status: investigation in progress, 2026-10-15 UTC, priority revision 4. Evidence is LOCAL-ONLY; no theorem or supplier admission is claimed yet. Claim expires 2026-10-15 16:45 UTC.

I am taking the weighted-price open question in research/symmetric-adjacent-cut-bound/README.md (PR1989), starting with its S4 prices (1,2,1). The proposed extension keeps the full formal F2[S_n] model, all binary rank-one idempotents, arbitrary free scalar mixing and complete dirty restoration. Exactly one adjacent label s_p costs beta; all others cost alpha, with 0 <= alpha <= beta.

Question: is the exact cost for a heterogeneous diagonal target tuple alpha * sum inv(w_j) + (beta-alpha) * sum c_p(w_j), where c_p(w) counts positions at most p mapped above p? I will combine the inherited ordered-pair cut with the natural-action cut at p, then prove or falsify simultaneous attainment of both bounds. Preliminary Dijkstra checks agree through S6, but finite agreement is not the proposed uniform proof.

Base: canonical main 0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2; selected record unchanged. Picker nonce 5cb5f3f4185f2c88f4b9c75664ac0acf, bit-mechanisms / bit-new-register-model. Scope changed to the predecessor's explicit weighted-tariff handoff rather than a new native alphabet. This would rule out a specific changed-price route, not construct a physical supplier or improve kappa.

Overlap: fresh complete snapshot of 758 open PRs and 1,222 Discussion records, plus local README/TASK/ledger searches. PR2544 (9fb1552f12ca4777ca660461a8b602e709285f99, ywz65) already proves asymmetric coordinate-SWAP tariffs; that special case is credited, not claimed anew. PR1966's odd-dihedral result is also retained. I found no matching one-premium symmetric-group claim; metadata search is not a novelty guarantee.

Expected artifact: a short written argument and a standard-library exact checker, including weighted Dijkstra, formal endpoint checks and failure controls. Stop if simultaneous attainment fails; report a precise counterexample instead. No broad search, selected-frontier edit, native/compiler/hosting admission or multiplication-theorem claim.

Credit: Ross Richardson's PR1989 and its Adam Gall/PR1941 and PR1966 cut-method lineage, plus ywz65's PR2544. Prepared by starship-s with substantial Hermes/OpenAI assistance; any coding verification will use Codex with GPT-6-Astra.