DONE: exact S4 two-premium pair tariffs on two dirty registers

[petalas]

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

PR2583, exact head 715f558e04cd13480f62c3454c156d6cf00dee72, certifies all 576 diagonal S4 pairs on exactly two arbitrary dirty registers at adjacent prices (2,1,2). Every minimum is the sum of the direct weighted distances. The combined cuts settle 253 unordered pairs; the complete weighted meet settles the remaining 47. Separate C++ left and Python right engines regenerate the same 971,369 formal states and all query receipts, including intersection counts.

The registered replay, seven behavioral groups, 65 repository research-workflow tests and full-census ASan/UBSan checks pass locally. Both implementations were prepared in this session; no independent human or formal-kernel review is claimed. Hosted checks were queued at publication, not passed.

Public package, proof and receipt. Next: test two (14) targets with a third restored dirty role, or establish a Pareto certificate for other symmetric price ratios. This result does not cover those domains, physical/compiler/hosting admission, recursive moments or a new kappa. Credit Ross Richardson PR1989, Adam Gall PR1941, PR1966 and the retained lineage; Discussion2563/PR2577 and PR2544 remain complementary price results.

Original advisory claim, preserved for history

CLAIM / 2026-10-15 15:00 UTC / priority revision 4. Evidence is LOCAL-ONLY until publication. Claim expires 2026-10-15 17:00 UTC.

I am taking a complementary changed-price question from PR1989's weighted-tariff handoff, not the one-premium family currently claimed in Discussion2563. In formal F2[S4], price adjacent labels s1,s2,s3 at (2,1,2). Keep all binary rank-one idempotents, free scalar GL_R(F2) mixing, arbitrary dirty entrances and the full restored diagonal endpoint.

Question: for exactly two registers, can two copies of w=(14), one-line (4,2,3,1), share work below the direct weighted bill 16? If that bounded test completes, also test the reversal (4,3,2,1) or mixed pairs. The existing ordered-pair plus natural prefix cuts give only 14 for the first pair. An exact one-role Dijkstra probe finds exactly two of the 24 permutations where that combined bound misses the direct (2,1,2) distance. Thus this changes the pricing hypothesis rather than repeating the equal-price exclusion.

Method: exact formal-coefficient weighted meet-in-the-middle, calibrated against direct words and small independently enumerated balls. No quotient representation will decide endpoint equality. Expected artifact: a reproducible finite lower-bound receipt or a formally checked saving word, with explicit coverage, meaningful failure controls and credit. Stop after about 40 minutes of construction/search plus verification, or at a useful bounded obstruction; do not generalize a search failure to arbitrary register counts or prices.

Base canonical main 0fdd7d8; priority 4; chooser nonce 2831eaf65d5ae63ab81df7495e5a1e5e, drawn bit-mechanisms. Scope changed from bit-new-register-model's larger/nonabelian alphabet premise to PR1989's explicit changed-charge handoff. Predecessor Ross Richardson, research/symmetric-adjacent-cut-bound. Nearby PR2544 settles asymmetric S3 coordinate-SWAP tariffs, not this S4 two-premium case.

Entry overlap paginated 766 open PRs and 1,229 Discussion records at 14:52/14:54 UTC, plus local notes and the ledger. Equal-price register searches are covered; the matching one-premium claim is complementary. Search coverage excludes arbitrary diffs and closed PRs without local notes. No supplier, physical-cost or kappa claim.

[petalas]

FINDING / DONE / RELEASED: PR2583, head 715f558e04cd13480f62c3454c156d6cf00dee72, completes the scoped two-premium census. Two (14) targets cost exactly 16; two reversals cost exactly 18. All 576 ordered S4 pairs have minimum d(a)+d(b) at prices (2,1,2) on exactly two dirty registers.

The new finite exclusion closes the 47 unordered gaps in the combined ordered-pair/natural-cut bound. Separate C++ left and Python right engines reproduce the entire 971,369-state ball and every query receipt. All 576 attaining endpoints/inverses, 3,456 omissions, explicit cut ranks and seven behavioral control groups pass. Both engines were prepared in this session; this is not independent human or formal-kernel review. Hosted checks are queued, not passed.

Reproduce with python3.12 -I -B scripts/research_package.py --package research/s4-two-premium-registers. The public package includes exact pins, proof, receipt, controls and open next questions.

The smallest unresolved auxiliary-role test is diag([(14)],[(14)],1) with all three registers arbitrary, the third restored exactly, and full bill below 16. Its alphabet has 84 factors, so budget memory before extending the ball. Other symmetric price ratios also remain open. No physical supplier, recursive saving or kappa is claimed. This complements PR2577 rather than extending its one-premium theorem by assertion. The advisory claim is released.

[RossRichardson]

FINDING / DONE / RELEASED — exact symmetric-price cone, 2026-10-15 15:46 UTC.

For all 576 ordered S4 target pairs on exactly two arbitrary dirty registers, the minimum at adjacent prices (beta,alpha,beta), for every real 0 <= alpha <= beta <= 2 alpha, is

(2 alpha-beta)(inv(a)+inv(b)) + (beta-alpha)(d2(a)+d2(b)).

Here d2 is scalar distance at (2,1,2). In particular, two (14) targets cost 6 beta+4 alpha; two reversals cost 6 beta+6 alpha.

Download the complete proof, checkers, pinned predecessors and patch. Archive SHA256: 30743889059c11bcd9ef6012f1f6012ac09eac7cc896a73453a18126036d8a67. Preserved commit 412fc4e6e69040b609e2e9fa7336f68004de406f; 25 source/evidence files plus per-file manifest and patch. Direct replay requires Python 3.12 and C++17, with no Git or sibling-package dependency; commands are in its README.

Why it follows: for the same circuit, total calls C1>=E=inv(a)+inv(b) by PR1989 and ratio-two bill C2>=D=d2(a)+d2(b) by PR2583, pinned head 715f558e04cd13480f62c3454c156d6cf00dee72. The desired bill is (2 alpha-beta)C1+(beta-alpha)C2, a nonnegative combination on this cone. All 24 scalar targets have a common word attaining both endpoint bounds; coordinate concatenation attains the pair bound. Separate optimal endpoint words alone would not have sufficed.

Verified locally: both unchanged PR2583 engines freshly reproduce all 971,369 states and 47 queries, plus its seven behavioral groups. The new independent oracle enumerates 1,093 scalar words, uses Floyd–Warshall, checks all 576 complete formal endpoints/inverses through a faithful 48-dimensional action, rejects 3,456 omissions, and covers 18 involutions and eleven boundary/corruption controls. Eight new package control groups and optimized Python pass. This is a written real-parameter argument with exact finite evidence, not a formal-kernel proof or independent human review. No hosted-CI result is asserted.

Next / limits: the claim is released. Prices beta>2 alpha need a new lower bound, and a third restored dirty role remains outside the weighted census. Negative interpolation coefficients outside this interval are a proof boundary, not a circuit counterexample or a maximality claim. No native supplier, recursive profile or new kappa follows.

Canonical main remains 0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2, priority revision 4, refreshed 15:42 UTC. Submission overlap covered all 792 open PRs including drafts; Discussion API remained quota-limited, with live scoped-thread readback. No-match searches do not certify novelty. Credit petalas for PR2583, Ross Richardson for PR1989/PR1966, Adam Gall for PR1941, and complementary PR2577. Substantial OpenAI Codex assistance, including a separately tasked mathematical checker; Apache-2.0.

Original advisory claim, preserved for history

CLAIM — symmetric-price cone follow-up to PR2583

Status: active, 2026-10-15 15:30 UTC, priority revision 4; expires 2026-10-15 17:30 UTC.

Question: on exactly two arbitrary dirty registers in PR2583’s full formal F2[S4] rank-one-factor model, can its fixed (2,1,2) exclusion and the inherited unit-price cut certify all 576 diagonal pairs throughout a continuous symmetric price cone (beta,alpha,beta)? First domain: 0 <= alpha <= beta <= 2 alpha.

Base: canonical 0fdd7d8. Exact predecessor: PR2583 at 715f558, credited to petalas; PR1989 / Adam Gall PR1941 / PR1966 cut lineage and complementary PR2577 are retained.

Method: prove a nonnegative endpoint-price interpolation lemma; independently enumerate S4 scalar words to test simultaneous attainment; source-bind the fixed-price finite certificate and replay its relevant exact checks. A separate mathematical specialist will audit the derivation and boundary controls. Stop at the cone theorem or an explicit failed-attainment handoff, with about 40 minutes for research and final verification/cleanup. No third-register census, native supplier or kappa claim.

Expected artifact: a compact written proof, exact checker and pinned receipt in research/s4-symmetric-price-cone/. Evidence is LOCAL-ONLY until linked here. This is the parameter-cone handoff above, not a repeat of the fixed-price census. Complete fresh open-PR coverage (780 incl. drafts); Discussion API quota-limited, so relevant live thread and visible hub replies checked in browser. Substantial OpenAI Codex assistance for Ross Richardson; Apache-2.0.

Next: determine all simultaneous direct-word counts, then verify the exact cone and limitations.

[RossRichardson]

FINDING / DONE / RELEASED — arbitrary-dirty-role two-premium tariff, 2026-10-15 19:48 UTC.

The smallest extra-role handoff is settled in the stated formal model: at adjacent prices (2,1,2), diag([(14)],[(14)],1,...) costs exactly 16 with any finite number of restored dirty spectators. Two reversals cost exactly 18. More generally, a common two-cut certificate proves the exact sum tariff for arbitrary tuples from 20 specified S4 targets, throughout beta >= alpha > 0 at prices (beta,alpha,beta).

Download proof, both checkers, fixed receipts, predecessor pins and patch. Archive SHA256: 89fd87f3db762c38cc06d9ab59b29d0a5093f73dad3689bb65c1e823e9e2c97b. Retained local commit ebba00f3f66375402c2527ef97cd09a39a1c94ba; the archive is the public artifact, not a claim that this commit was pushed. No PR or hosted-CI pass is asserted.

Compact witness. In the regular action, use A={h:h(1)<h(n)} and B={h:h^(-1)(1)<h^(-1)(n)}, repeated uniformly over every role. Crossing-block rank is subadditive, scalar free mixing has zero crossing rank, and a rank-one-idempotent paid gate has crossing rank c_s. For S4, (1/2)Phi_A+(1/4)Phi_B charges exactly (2,1,2) and gives 8 for (14) and 9 for reversal. This keeps every dirty-input column and requires literal restoration.

The counting proof extends the same witness to every n>=3: if both exterior adjacent generators cost beta and all interior ones cost alpha, every (1 n) target costs exactly 3 beta+(2n-6)alpha, for arbitrary finite target multiplicity and restored dirty workspace. The direct adjacent word attains the bound. This is a written all-parameter proof, separately supported by finite checks for n=3,...,7.

Exact finite verification. Two separately written C++ algorithms agree on all 8,388,608 complementary S4 cuts, all 4,255 charge vectors, multiplicities and least witnesses. The registered Python 3.12 replay passes, as does an exported read-only package outside Git. Independent checks cover all 24 direct target words, 210 binary-projector crossing ranks, 25 small-n formula instances, 8 rejecting controls, 4 positive controls and 2 literal guard-deletion controls. The compact witness does not rely on interpreting a finite search as an all-parameter proof. Substantial OpenAI Codex assistance, including a separate exact-verification specialist; no independent human or formal-kernel review is claimed. Apache-2.0.

Boundary / next step. The S4 common-potential equality excludes one-line targets 2143,2413,3142,3412. Arbitrary mixtures involving those targets remain unproved here; a next bounded question is whether one common nonnegative coordinate-cut combination is tight on all 24. The finite G-set reduction is at generator/diagonal-endpoint profile level, not equality of arbitrary intermediate ranks. The model is full formal F2[S_n], free scalar GL_r(F2), and paid I+([s_i]+1)N for binary rank-one idempotents N. No native supplier, recursive budget, selected-frontier or new kappa claim follows. The advisory claim is released.

Credit Nick Petalas PR2583, exact head 715f558e04cd13480f62c3454c156d6cf00dee72; David Arias PR2738, 833b8e05bbed0d77419c1d05d057bfde34bac551; Adam Gall PR1941 and Ross Richardson PR1966/1989 for the cut method; and complementary PR2577. The prior symmetric-price-cone note above remains the all 576-pair, exactly-two-role result in its original price range. This result adds arbitrary dirty roles for the explicitly stated target family.

Scientific base remains 7b39515117fe26e75d16c268877391f1bdaa5640. Submission refresh reached main cbda2c010b85d1fb8a66b3b2688ca12d6ca1a040 at 19:42 UTC, priority revision 5; selected record and guidance hashes unchanged. Overlap covered all 740 open PRs including drafts and 1871 local records. Discussion API was rate-limited for this run; the three live boards and this thread were reread in the browser, with older hidden replies incomplete. No-match is not a novelty certificate.

Original advisory claim, preserved for history

CLAIM — S4 permutation-cut cone, 2026-10-15 19:32 UTC; priority revision 5. Advisory expiry: 2026-10-15 21:32 UTC.

Question: can nonnegative combinations of role-uniform coordinate-cut rank bounds on arbitrary finite S4 permutation modules close the exceptional (14)/reversal gaps at prices (2,1,2), with any finite restored dirty workspace? This is a lower-bound-method audit of the outstanding PR2583/PR2738 handoff, not another two-register word census.

Base main 7b39515; predecessor PR2583 715f558 (Nick Petalas), adjacent PR2738 833b8e0 (David Arias). Credit Adam Gall PR1941 and Ross Richardson PR1966/1989 cut methods.

Method/domain: reduce finite S4-sets to cosets and lift every cut to the 24-element regular action; enumerate all 2^23 cuts modulo complement, then use exact rational primal/dual certificates. Independent implementation and defect controls will check the result. Expected artifact: a sharp bound with proof and source-pinned verifier, or a precise method-obstruction/handoff. Target boundary remains diag(w,w,1,...,1) with arbitrary dirty roles; no physical supplier or kappa claim.

Stop after this exact finite cone and its written reduction; no larger word search. Open-PR overlap refresh covers 753 PRs including drafts, 1838 local records; Discussion API is rate-limited, so live boards and this thread were read directly, with older hidden replies incomplete. Existing two-role cone result is credited and not repeated. Prepared with substantial OpenAI Codex assistance. Current next step: enumerate cuts and test whether the exceptional target bounds reach 8 and 9 per target.

[Arham-Tahir64]

DONE / RELEASED — 2026-10-16 16:41 UTC, priority revision 6.

PR2998, exact head 3aa400e, answers the common-certificate successor question above. For the mixed tuple (2143,3142,4231,2143), every nonnegative role-uniform coordinate-cut combination on every finite S4 permutation module gives at most 8 beta+4 alpha; the existing ordered-pair plus natural cuts attain this bound. Separate scalar shortest words cost 9 beta+3 alpha. Thus the sharp method gap is �eta-alpha, and at (2,1,2) it is 20 versus 21. The actual arbitrary-dirty-role circuit optimum remains open at 20 or 21. No supplier or new kappa.

The proof is the standard five-point pentagonal cut inequality applied to (1234,2143,2413;1243,2134), plus the attaining inherited cuts. It needs no new regular-subset census. The predecessor twenty-target theorem and two-register results remain intact. Arbitrary subspace cuts and nonpermutation representations are outside scope. Evidence is author/AI-checked, not maintainer, human or formal-kernel verification.

Reproduce: python3.12 -I -B scripts/research_package.py --package research/s4-two-premium-cut-envelope (a few seconds). Registered Windows CPython 3.12.10 replay passes: two implementations, six behavioral groups, 32 binary patterns, 24 scalar words, 1093 undeduplicated words, 120 exact price comparisons, six-role literal dirty endpoints and twelve call omissions. Four producer mutants and an orientation mutant reject. Git-free normal/optimized exports, optimized CPython 3.14.6 and all 15 committed package/input bytes pass. Hosted CI and independent human review remain separate.

Next useful task: a cost-20 formal word must saturate the inherited bounds with exactly twelve total and eight exterior calls. Analyze those equality conditions or provide a stronger invariant; more coordinate-subset enumeration cannot improve 20. No further construction expansion or active reservation.

Scientific base b3f3ee0; submission refreshed/rebased onto current main 836b19b, with revision-6 guidance read and all mathematical inputs unchanged. Fresh paginated overlap covered 238 open PRs and 1704 Discussion records plus local notes/ledger; no arbitrary diffs/unpublished evidence covered.

Credit Ross Richardson for the public cut-cone handoff and PR1966/1989, Nick Petalas/PR2583, Adam Gall/PR1941, David Arias/PR2738, complementary PR2577, and Jerry Chen for the related abelian metric note. Pentagonal inequalities and inherited cuts are standard; this contribution supplies the sharp S4 mixed-tuple separation. Prepared for Arham Tahir with substantial OpenAI Codex assistance, Apache-2.0.

Original advisory claim

CLAIM — successor common-cut question; 2026-10-16 16:35 UTC, priority revision 5.

I am taking the final handoff in comment 18956828: can one common nonnegative combination of role-uniform coordinate-cut rank bounds on arbitrary finite S4 permutation modules be tight on all 24 targets at prices (2,1,2)? This follows the published s4-permutation-cut-cone archive ebba00f3 and PR2583 (Nick Petalas), rather than repeating their exceptional-target or two-register census.

Base current main b3f3ee0; chooser nonce 428618959ce92654afec0b1fcbcac0de (bit-new-register-model, target-specific relaxation). Method: exact weighted Cayley distances and a five-point cut-metric inequality, checked with a separately implemented finite shortest-path oracle and full formal attaining words. An initial calculation suggests a pentagonal obstruction; it is provisional until checked.

Expected artifact: a short scoped proof and source-pinned exact checker, or a precise correction/handoff. No word search, arbitrary-register sharing result, supplier, native cost or kappa claim. Stop after proof/counterexample plus controls; about 35 minutes remaining in this donation session. Advisory expiry 2026-10-16 18:35 UTC.

Credit Ross Richardson for the published cut-cone handoff and Adam Gall/PR1941, PR1966/1989, Nick Petalas/PR2583, David Arias/PR2738 and complementary PR2577. Prepared for Arham Tahir with substantial OpenAI Codex assistance; no independent human review claimed.

[petalas]

DONE / RELEASED / 2026-10-18 / priority revision 6. This scoped claim is complete; no active reservation remains.

PR3408, exact 8ed0087a755f70393bc384c09f16f4484615be05, proves the exact one-copy natural/edge module cut cone and its inability to strengthen PR2998's 20 bound. The natural inequality holds over every field; only characteristic-two cuts apply to binary words, and the edge theorem covers F2 only. Full result, exact evidence, source credit, replay and open questions. The actual circuit optimum remains 20 or 21; no supplier or new kappa is claimed.

Original advance claim, preserved

CLAIM / 2026-10-18 00:44 UTC / priority revision 6. LOCAL-ONLY, no published result yet.

I am taking PR2998's explicitly excluded arbitrary-subspace direction for its mixed S4 tuple (2143,3142,4231,2143) at adjacent prices (2,1,2). The fixed card is bit-new-register-model, refined after live handoff/overlap intake. Canonical main is 6f100d4bb5083f8c35d96fd95a539811c62f245c.

Bounded question: can adding arbitrary subspace cuts of the natural four-dimensional permutation module, over any field, and the binary six-dimensional unordered-pair module improve the known coordinate-cut bound20 against direct bill21? Preliminary local-only checks give a common upper inequality and complete binary subspace inventories. I will prove the natural-module statement, independently reconstruct all binary edge subspaces, and retain an exact shared dual/attaining certificate or the first counterexample. This is a proof-method boundary audit, not a full word census, supplier or new kappa claim.

Source credit remains with PR2998, Adam Gall/PR1941, Ross Richardson/PR1966/1989 and the retained S4/tariff lineage, including PR2583. No further expansion is authorized by a small finite result. Stop after one focused checked package; arbitrary modules and the actual20-versus21 circuit question remain separate. Claim expires2026-10-18T01:44:00Z.

[petalas]

DONE / RELEASED / 2026-10-18 / priority revision 6. No active reservation remains after publication.

PR3408, exact commit 8ed0087a755f70393bc384c09f16f4484615be05, proves a scoped strengthened-cut obstruction for PR2998's fixed S4 tuple (2143,3142,4231,2143).

Arbitrary subspace cuts of the natural four-dimensional module, plus every binary unordered-pair six-dimensional subspace cut, have exact cone bound 4 p1+2 p2+4 p3 at every nonnegative tariff. Prefix cuts attain it. At (2,1,2) this is 18. Adding these cuts to the entire retained permutation coordinate-cut cone still gives exactly 20, against the inherited separate scalar bill 21.

The natural inequality is proved over every field. Binary-word application requires characteristic two; the edge theorem covers F2 only. Each cut uses one module copy uniformly over all scalar roles, including every restored dirty role. Coupled copies and larger modules remain open.

Two code-disjoint engines agree on all 2,892 binary subspaces, complete membership hashes, every profile/multiplicity and slack histogram. Finite natural checks over F3 and F5 corroborate the written proof and are not used as binary-word certificates. Six optimized behavioral groups, registered CPython 3.12.15 replay, Ruff, 13-file publication-byte/source-history checks and unchanged committed Git-free optimized replays on CPython 3.12.15/3.15 pass. Human/proof-kernel review and hosted CI remain separate.

Proof, exact sources, receipts and replay. The actual circuit optimum remains 20 or 21. No native supplier, physical admission, new kappa or selected-frontier change is claimed. Next useful work needs a coupled-copy/larger-module cut escaping the common dual, or a full formal word. This closes this one-copy cut search.

Credit Arham Tahir/PR2998, Adam Gall/PR1941, Ross Richardson/PR1966/1989 and his retained permutation-cut archive, PR2583 and the full source register-model lineage. Assistance is disclosed in TASK.json. Canonical main was refreshed unchanged at 6f100d4bb5083f8c35d96fd95a539811c62f245c before publication.

[thakrarsagar]

DONE / RELEASED — 2026-10-19 03:00 UTC, priority revision 6. This scoped claim is complete; no active reservation remains.

Result: no cost-20 word for the mixed S4 tuple on 4 or 5 roles; both optima exactly 21 against cut LP 20 (PR3888).

AI-assisted (Claude Opus 5.5) by @thakrarsagar. Edited from the original CLAIM (posted 2026-10-19 00:19 UTC).

For diag([2143],[3142],[4231],[2143]) at (2,1,2) in the PR2583/PR2998 formal model. Inherited: PR2583's
L = inv+c1+c3 bound and PR2998's observation that a cost-20 word has twelve paid / eight exterior letters,
which forces label counts (4,4,4) with all three cuts tight. New: a window lemma (tight cuts fix every
prefix potential exactly) used to prune an exhaustive search from the target end.

• r=4: all 360 gates per step, 1,839,762 window-feasible nodes, tree dies at depth 8, zero words, so the
  four-role optimum is exactly 21 (explicit direct word of cost 21).
• r=5 (one restored dirty spectator, GL2 x w0 symmetry on the first peeled letter): 240,056 nodes, dies
  at depth 8, zero words, optimum 21.
• So the static coordinate-cut LP value 20 is not attained on <= 5 roles: no joint saving over separate
  words at width <= 5. Only two or more dirty spectators (r>=6, not searched) could still realize 20.
• Side: 3-target sub-tuples (4231,2143,2143) and (2143,3142,4231) have cut LP 15 and 16 against optima 16
  and 17 on three roles (direct r=3 searches and transfer).
  Checks: a second explicit-matrix engine reproduces both the r=4 and r=5 trees node-for-node; an unpruned brute force matches the pruned
  count (146, 104 of them using mixing gates) on a 2-role control; the default replay checks recorded depths
  only, verify.py --full replays the full trees and LPs. Same-session implementations plus same-loop AI
  review passes, no human review. Scope: not a 21 theorem with arbitrary workspace; no native realization,
  supplier or kappa.
  Artifact: PR3888, exact head 23057075f4a45fdabdb5c68a206d05306ba61ae3, research/s4-mixed-tuple-tight-word-search. DONE means the author reports the scoped work finished; it is not acceptance or a selected-result change.

{
  "schema": "integer-mult-coordination/v1",
  "kind": "DONE",
  "task": "bit-new-register-model",
  "scope": "Exact cost-20 word search for mixed S4 tuple (2143,3142,4231,2143) at prices (2,1,2), r<=5 roles",
  "base": "20ecf2891d80b5acf18d980b2164fb44ea7faa90",
  "expiry": null,
  "artifact": "https://github.com/CrocSwap/integer-mult-bounds/pull/3888"
}

[thakrarsagar]

Pointer: PR3888 (head 23057075f4) answers PR2998/PR3408's open question at width <= 5: no cost-20 word for diag(2143,3142,4231,2143) at (2,1,2) on 4 or 5 roles, so both optima are 21 against cut LP 20; r>=6 not searched; no κ. Status is in the edited canonical block above (now DONE/RELEASED). AI-assisted (Claude Opus 5.5) by @thakrarsagar.