Research: certify all S4 two-premium two-register tariffs

research/s4-two-premium-registers/README.md

@@ -0,0 +1,188 @@
+# S4 two-premium calls do not share work across two dirty registers
+
+For adjacent labels in `S4` priced `(2,1,2)`, all **576 ordered diagonal
+pairs** have exact minimum `d(a)+d(b)` in the formal model below. Here
+`d` is the one-register weighted Cayley distance. The two-register search
+closes the cases not decided by the inherited cut bounds. This is a finite
+certificate, not an arbitrary-register theorem or a new kappa.
+
+The selected result and every frozen predecessor remain unchanged.
+
+## Model and changed hypothesis
+
+Use the full formal algebra `F2[S4]`. The paid labels are
+`s1=(12), s2=(23), s3=(34)` with respective costs `2,1,2`. A paid factor is
+
+`D_N(s_i) = I_2 + ([s_i]+1)N`,
+
+where `N` is any binary rank-one idempotent. There are six such `N`, giving
+18 paid factors. Both registers start arbitrary and must have complete
+endpoint `diag([a],[b])`, including zero off-diagonal coefficients. An
+identity target is an arbitrary dirty spectator, not a clean ancilla.
+Arbitrary scalar `GL_2(F2)` mixing is free. No extra registers, resets,
+COPYs or free address maps are allowed. Every restoration call is charged.
+
+As in Ross Richardson's [PR1989 proof](../symmetric-adjacent-cut-bound/PROOF.md),
+scalar maps can be moved to one end by conjugating `N`. Augmentation forces
+that final scalar map to be the identity. Thus the normalized paid alphabet
+covers all interleaved free scalar circuits in this model.
+
+The changed premise is the price, not a new alphabet. PR1989 proves the
+unit-price obstruction and explicitly leaves weighted prices open.
+Discussion2563 and its PR2577 address the distinct one-premium family,
+starting at `(1,2,1)`. PR2544 concerns the two-generator `S3` coordinate-SWAP tariff. This package
+uses two premium outer labels in `S4`; neither predecessor settles it.
+
+## Cut bound and the two exceptional permutations
+
+Let `c_p(w)` count `i<=p` with `w(i)>p`. In the natural permutation action,
+the cut from the first `p` coordinates to their complement has rank
+`c_p(w)`. Its charge on `s_i` is `1` for `i=p` and `0` otherwise.
+Tensoring with a rank-one scalar projector preserves that charge, and
+free scalar maps have charge zero. The subadditivity proof is exactly the
+block-rank argument credited to PR1941/PR1966/PR1989.
+
+Combine the natural cuts at `p=1,3` with PR1989's ordered-pair cut. Every
+circuit, with any finite dirty role count, has weighted cost at least
+
+`sum_j L(w_j)`, where `L(w)=inv(w)+c_1(w)+c_3(w)`.
+
+The charge of each generator is precisely `(2,1,2)`. For `S4`,
+`c_1(w)=1` iff `w(1)!=1`, and `c_3(w)=1` iff `w(4)!=4`.
+The exact 24-vertex one-role calculation gives `d(w)=L(w)` except for:
+
+| One-line permutation | `L(w)` | `d(w)` | Attaining chronological labels |
+| --- | ---: | ---: | --- |
+| `4231`, the transposition `(14)` | 7 | 8 | `1,2,3,2,1` |
+| `4321`, the reversal | 8 | 9 | `2,1,2,3,2,1` |
+
+`EXPECTED.json` contains all 24 distances and attaining words. Every graph
+edge satisfies the shortest-path dual inequality, and every word has its
+stated bill and full formal endpoint. The combined cut cannot certify the
+exact weighted tariff for these two permutations: `d=L+1`. This is a gap in
+that particular lower bound, not evidence of a sharing construction.
+
+For the other 22 permutations, the cut plus direct words already proves
+additivity for any target tuple and any finite number of restored dirty
+roles. That consequence does not require a search.
+
+## Complete two-role exclusion
+
+There are 300 unordered pairs including repetitions. The cut settles 253.
+The remaining 47 unordered pairs, or 92 ordered pairs, contain at least one
+of the exceptional permutations. Role exchange preserves the alphabet,
+prices and boundary, so checking the unordered pairs is exhaustive.
+
+Both engines construct the exact weighted ball of radius nine:
+
+| Minimum cost | 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9 |
+| --- | ---: | ---: | ---: | ---: | ---: | ---: | ---: | ---: | ---: | ---: |
+| States | 1 | 6 | 19 | 134 | 542 | 2,058 | 10,568 | 40,562 | 166,385 | 751,094 |
+
+The ball has **971,369 distinct formal states**. For each of the 47 pairs,
+the complete meet finds minimum exactly `d(a)+d(b)`, including 16 for two
+`4231` targets and 18 for two reversals. The receipt includes every query,
+its cut/direct bills and its number of ball intersections. Each query row
+is `[a,b,direct,cut,meet,hits]`; `a,b` index `permutation_order`.
+
+Why radius nine suffices: each factor costs at most two. Any word of cost
+at most 17 splits into two subwords of cost at most nine. Choose the first
+prefix of cost at least eight; it costs eight or nine. If the whole word
+costs less than eight, use the identity as the other half. Since every
+factor is an involution, every such word has form `A B^-1`, with both
+states in the ball. The producer enumerates all `B` and tests `A=T B` by
+full formal equality. Every direct pair bill is at most 18, so excluding
+all cheaper words through 17 is sufficient.
+
+The weighted layers are also exhaustive. A state of minimum cost `k` has a
+last factor of cost one or two and a shortest predecessor at cost `k-1`
+or `k-2`. The engines apply every legal factor from both relevant layers,
+discard only exact states already at smaller cost, and record all remaining
+states at cost `k`. No heuristic or quotient filter prunes the ball.
+
+## Evidence and replay
+
+```sh
+python3.12 -I -B scripts/research_package.py --package research/s4-two-premium-registers
+```
+
+The registered replay runs all three checks, about one minute on the recorded
+Linux environment with CPython 3.12.15 and GCC 14.2.0:
+
+```sh
+python3.12 -I -B research/s4-two-premium-registers/verify.py
+python3.12 -I -B research/s4-two-premium-registers/independent.py
+python3.12 -I -B research/s4-two-premium-registers/test_verify.py
+```
+
+The producer compiles `engine.cpp` in a temporary directory with strict
+warnings. A C++17 compiler is required. `verify.py --write` is the only
+receipt-regeneration command. Default replay does not change package files.
+
+The C++ producer uses four 24-bit coefficient sets, left multiplication,
+and full-key hash-table equality. The separately written Python engine
+uses packed 96-bit integers, right multiplication, its own permutation
+multiplication tables and Dijkstra distances. It imports no producer or
+predecessor implementation. Both independently regenerate the full ball
+and all 47 queries; **their complete census receipts agree**, including
+all intersection counts. These are separate implementations from the same
+session, not independent human review or proof-assistant verification.
+
+Other checks include all 576 formal endpoints and their inverses, all
+3,456 single-call omissions, 18 paid involutions, 54 explicit paid-factor
+cut ranks, 72 target cut ranks, 18 free-scalar cut ranks, exact equality of all
+702 radius-four states, every transition from that small ball against a
+literal matrix oracle, and undeduplicated word enumeration through cost
+four. Seven behavioral test groups reject corrupted scientific receipts,
+wrong order, dirty leaks, nonfaithful-representation endpoint aliases,
+invalid projectors, malformed radii and exhausted state capacity. Forcing
+hashes to one bit leaves the small ball unchanged. Optimized read-only,
+Git-free replay succeeds; changing a pinned source fails before search.
+
+Only the credited proof is a live external dependency. Its exact SHA256
+and Git blob are in `SOURCES.json`; the catalogue and selected result are
+historical provenance. No predecessor search code is imported.
+
+### Implementation limits
+
+The search radius is capped at nine, the state capacity at two million,
+and subprocesses have explicit timeouts. Capacity exhaustion fails without
+an exclusion receipt. The language/runtime allocation deviation is confined
+to these finite checkers: Python dictionaries and C++ hash nodes allocate
+during enumeration. The enforced state cap bounds live search storage;
+tables have 24 group elements, 18 calls and ten layers. There is no recursion
+or service loop. C++ tables are initialized once and read-only during search.
+The standard hash table and Python runtime allocate internally; no hard
+real-time memory guarantee is claimed. GCC strict warnings, AddressSanitizer
+and UndefinedBehaviorSanitizer pass on the full census. Python development-mode
+compilation with warnings treated as errors passes; a separate Python linter
+was unavailable in the recorded environment. A larger search requires an explicit
+capacity and memory review, not removal of the guard.
+
+## Open next questions
+
+- Does an exceptional target admit weighted sharing with a third restored
+  dirty role? The smallest first test is two `4231` targets plus an identity
+  spectator, against bill 16. A favorable word must be checked formally and
+  completely charged. The larger 84-factor alphabet and exact weighted-ball
+  memory are the blockers; the present two-role census does not settle it.
+- Does additivity persist for the symmetric price cone `(beta,alpha,beta)`
+  with `0<alpha<beta`, beyond the tested ratio two? First enumerate Pareto
+  costs by total calls and outer-label calls for the two exceptional targets.
+  One fixed weighted ball is not a complete parameter-cone certificate.
+
+These questions are recorded in `TASK.json`. No physical native conversion,
+compiler, hosting, precision/tape, recursive moment, selected-supplier cold
+replay or multiplication theorem is supplied. The bit supplier is not the
+currently binding side, and this formal tariff alone changes no kappa.
+
+## Credit
+
+Ross Richardson's PR1989 supplies the operation model, ordered-pair cut,
+free-scalar normalization, direct-construction argument and weighted-price
+handoff. Adam Gall's PR1941 and Ross Richardson's PR1966 supply the underlying
+cut method. Josie Elliston's PR1974 is a related exact-register-census
+precedent, not an input to this search. Discussion2563/PR2577 and PR2544
+are complementary changed-price investigations, not claimed as new here.
+The retained bit-supplier lineage and attribution remain in those sources.
+New work is Apache-2.0.

research/s4-two-premium-registers/SOURCES.json

@@ -0,0 +1,24 @@
+{
+  "schema_version": 1,
+  "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11",
+      "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "e8870e5917057d59b730eb14721a778639eca050",
+      "sha256": "d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7"
+    },
+    {
+      "path": "research/symmetric-adjacent-cut-bound/PROOF.md",
+      "usage": "input",
+      "git_blob": "30dad3856246c9cef3b8014ee967dd545f3a092d",
+      "sha256": "008be68867a8e85f4e18455d206e03f20aebfc28e9f08efba576180e7e1edc50"
+    }
+  ]
+}

research/s4-two-premium-registers/TASK.json

@@ -0,0 +1,107 @@
+{
+  "schema_version": 1,
+  "task_id": "bit-new-register-model",
+  "priority_revision": 4,
+  "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2",
+  "original_card": {
+    "id": "bit-new-register-model",
+    "question": "Can an explicitly larger or nonabelian register model escape the scoped three-register obstruction?",
+    "starting_points": [
+      "research/bit-three-register-lower-bound/README.md",
+      "certificates/selected-result.json",
+      "research/bit-gl3-mixed-targets-length10/README.md",
+      "docs/research/community-efficient1000-review.md"
+    ],
+    "methods": [
+      "Construct the smallest exact identity in a newly specified legal operation alphabet.",
+      "Derive a target-specific relaxation bound for that same explicit alphabet."
+    ],
+    "acceptance_gate": "Name the changed hypothesis, all counted roles and a uniform identity; finite column tests alone do not certify it.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read Model section 1 of the three-register bound and identify the exact excluded free operations.",
+      "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay."
+    },
+    "first_experiment": "First compare the alphabet, role count and length with the fully replayed #1974 census and #2027 mixed-root tariff. Identify a changed premise and a legal native implementation; then price one smallest completed instance before searching larger words.",
+    "bottleneck_link": "A small-width completed saving changes the bit primitive; a finite-address identity alone is insufficient.",
+    "allowed_variations": [
+      "Choose a fixed larger register count or a specified nonabelian operation family."
+    ],
+    "scope_change_triggers": [
+      "Remaining inside the already-excluded three-register abelian model.",
+      "Repeating the two-register GL3 census or a covered three-register length without changing a hypothesis; a formal group-algebra word without native conversion is a partial result."
+    ],
+    "overlap_terms": [
+      "three-register",
+      "nonabelian",
+      "group algebra"
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Exact weighted minimum for all 576 ordered diagonal S4 target pairs on exactly two arbitrary dirty registers, with adjacent labels priced (2,1,2), all binary rank-one idempotents and free scalar GL2 mixing.",
+  "scope_change_reason": "The drawn larger/nonabelian-model questions and semantic helper interface have extensive existing coverage. Follow PR1989's explicit weighted-price handoff instead. Two premium outer labels differ from Discussion2563's live one-premium investigation and PR2544's S3 tariff. This changes prices rather than the address alphabet and is a formal-model side result, not a native supplier advance.",
+  "bottleneck_link": "Tests whether changed paid-call prices permit register sharing after the unit-price exclusion. A finite formal saving would still need a native realization and complete recursive invoice. The exact exclusion here changes no primitive moment or kappa.",
+  "budget_minutes": 60,
+  "stop_rule": "Complete the 47 unordered cut-gap pairs by a radius-nine weighted meet, or stop at two million states, 120 seconds per native subprocess, or the 60-minute session budget. Do not raise capacities or infer an arbitrary-register obstruction from failure.",
+  "outcome": "negative-result",
+  "evidence": "EXPECTED.json binds all 24 direct tariffs, 576 arbitrary-dirty endpoints/inverses, 3456 omission controls and the complete 971369-state census. Separate left/C++ and right/Python engines regenerate every layer and every one of 47 query receipts identically. Seven behavioral groups include full small-ball equality, literal transition checks, capacity/hash/receipt faults and optimized Git-free source-bound replay.",
+  "author": "Nick Petalas",
+  "ai_assistance": "No independent human or formal-kernel review is claimed; both implementations were prepared in the same session.",
+  "selection_nonce": "2831eaf65d5ae63ab81df7495e5a1e5e",
+  "coordination": "https://github.com/CrocSwap/integer-mult-bounds/discussions/2570",
+  "optimistic_cost_budget": "The inherited combined cut gives 14 for two (14) targets against direct bill 16, and 16 for two reversal targets against direct bill 18. Exact search closes these gaps at the direct bills, including every other pair.",
+  "predecessor_credit": [
+    "Ross Richardson PR1989, weighted-price question, formal alphabet, normalization and ordered-pair cut",
+    "Adam Gall PR1941 and Ross Richardson PR1966, subadditive cut-rank method",
+    "Josie Elliston PR1974, related exact register-census precedent, not imported",
+    "Discussion2563/PR2577 and PR2544, complementary one-premium/S3 price investigations, not reclaimed"
+  ],
+  "entry_overlap": {
+    "open_prs": 766,
+    "prs_checked_at_utc": "2026-10-15T14:52:29.542645+00:00",
+    "discussion_records": 1229,
+    "discussions_checked_at_utc": "2026-10-15T14:54:31.007904+00:00",
+    "complete_pagination": true,
+    "queries": ["--task bit-helper-contract", "--task bit-new-register-model", "weighted", "weighted adjacent; multiple premium; weighted symmetric; nonuniform tariffs"],
+    "limits": "Also searched local README/TASK notes and the PR ledger. No arbitrary diffs; closed PRs only through retained local notes. No match is not novelty evidence. The matching one-premium claim is complementary."
+  },
+  "submission_freshness": {
+    "canonical_main": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2",
+    "priority_revision": 4,
+    "selected_record_sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32",
+    "main_checked_at_utc": "2026-10-15T15:20:01Z",
+    "open_prs": 776,
+    "prs_checked_at_utc": "2026-10-15T15:14:36.113476+00:00",
+    "discussion_records": 1238,
+    "discussions_checked_at_utc": "2026-10-15T15:16:51.208914+00:00",
+    "complete_pagination": true,
+    "warnings": [],
+    "relevant_change": "Canonical main, priority and selected record unchanged. Discussion2563 completed as PR2577 and explicitly points the complementary two-premium question to Discussion2570. Continue this scoped census; no scientific input migration is needed.",
+    "complementary_heads": {
+      "2544": "9fb1552f12ca4777ca660461a8b602e709285f99",
+      "2577": "fb620547bbb66fa97c74ff5f8362df9bf9e591db"
+    },
+    "coverage_limits": "Queries: two-premium; (2,1,2); S4 weighted. Local notes and ledger also searched. No arbitrary diffs or complete closed-PR coverage. No match is not a novelty certificate."
+  },
+  "environment": "Linux x86_64; CPython 3.12.15; GCC 14.2.0; standard-library Python and C++17 only",
+  "verification_limits": "Exact formal S4 model and fixed (2,1,2) tariffs only. No extra dirty role in the finite exclusion, native conversion, hosting, precision/tape, recursive profile, selected cold replay, human review or proof-assistant verification.",
+  "open_questions": [
+    {
+      "question": "Can a third restored dirty role enable weighted sharing for two exceptional S4 targets?",
+      "why_it_matters": "The cut gap is closed only on two roles; arbitrary auxiliary coupling is outside this finite exclusion.",
+      "first_step": "Test diag([(14)],[(14)],1) at prices (2,1,2), against direct bill 16, with complete formal equality and a fully charged restored endpoint.",
+      "blocked_by": "The three-role alphabet has 84 factors and the weighted ball requires a new memory/capacity budget."
+    },
+    {
+      "question": "Does additivity hold throughout the symmetric price cone (beta,alpha,beta), 0<alpha<beta?",
+      "why_it_matters": "One ratio-two exclusion is not a uniform weighted tariff theorem.",
+      "first_step": "Enumerate the Pareto costs in total calls and outer-label calls for the two exceptional target classes.",
+      "blocked_by": "A fixed weighted radius does not bound every potentially competitive word throughout the price cone."
+    }
+  ]
+}