DONE: exact mixed UT3 target tariffs with arbitrary dirty workspace (PR1607)

[bbMisk]

DONE — PR1607, exact head 9d6117918025cee6a0c5b7ef30ff8d936ca0621f. Scope released.

The written coefficient-span/Sylvester proof gives sharp separate a/b tariffs for every diagonal mixture of all eight UT3 targets, with any finite restored dirty workspace and all nonzero rank-one scalar couplings. Direct formal words attain both bounds. This extends the central-only scope of PR1573 and PR1589, whose quotient and rank methods are credited. No new kappa or supplier admission is claimed.

Exact checks cover 111,151 short words and 2,336 full mixed-target fixtures; the formal and separately implemented faithful-regular engines agree on 62,848 basis columns and all 324 two-factor products. CPython 3.12 registered replay, CPython 3.14 read-only optimized relocation, 3,925 boundary mutations, model controls, corrupted-receipt rejection and source pins pass. Hosted CI is queued at handoff.

Reproduce: python3.12 scripts/research_package.py --package research/ut3-mixed-target-tariffs.

Full selected cold replay, physical/compiler/hosting/precision interfaces, analytic transfer, Lean and independent human proof review remain outside scope. The PR records the exact predecessor heads, overlap refresh and open next question. Prepared for Hanson Sun (@bbMisk) with substantial OpenAI Codex assistance; no subagents.

Original claim

CLAIM — mixed UT3 target tariffs with arbitrary restored dirty workspace

Question: in the formal F2[UT_3(F2)] register model with paid letters a=I+E01 and b=I+E12, does every diagonal mixture of the eight group elements have its direct separate-label minimum? For target g=(x,y,z), the proposed counts are x+2(1-x)z a-calls and y+2(1-y)z b-calls, summed over targets. The paid scalar alphabet includes every nonzero binary rank-one coupling, both idempotent and nilpotent; scalar GL mixing is free, and every extra role is arbitrary dirty and restored.

Base main: ebedc08. Catalogue bit-new-register-model, nonce 4aba18fcd52cd4290d0badf705c2dfc3. Predecessors: steph4n-gh PR1573 at 0b8c5a6, and Arham Tahir PR1589 at 010ec8c. Their central-only bounds and quotient/rank methods are credited; the proposed delta is heterogeneous endpoints with nonzero first-order coefficients. No predecessor executable is imported.

Method: the predecessor degree-two quotient plus Sylvester rank inequality, with full formal upper witnesses. Bounded corroboration: all two-register expanded-alphabet words through four calls, all one/two/three-target mixtures, separate faithful-regular replay, and model/dirty-input controls. This is a written all-register proof with finite corroboration, not a finite-search extrapolation. No new kappa or physical supplier is claimed.

Expected artifact: research/ut3-mixed-target-tariffs, a focused proof/checker package. Entry overlap covered 727 open PRs and 233 discussion records with complete pagination; coverage is not proof of novelty. Claim expires 2026-10-14T05:46:00Z.

Prepared for Hanson Sun (@bbMisk) with substantial OpenAI Codex assistance; no subagents or independent human proof review. Apache-2.0.