Prove exact sign-dependent tariffs for every signed 3x3 connector target

research/signed-matrix-price-classification/README.md

@@ -0,0 +1,193 @@
+# Exact sign-dependent tariffs for every signed 3x3 connector target
+
+produced by Nick Petalas
+
+This is a **scoped proof with finite corroboration**, answering open question 1
+of [#4241](https://github.com/CrocSwap/integer-mult-bounds/pull/4241).
+The exact query bill for all 19,683 matrices in `{-1,0,1}^{3x3}`, over every
+nonzero unital coefficient ring, depends only on the active operators and
+membership in Ross Richardson's 288-member obstruction orbit. Forward and
+inverse additive calls may have arbitrary different positive complete prices.
+There is no new kappa or multiplication theorem.
+
+The new result is the transport of the sign-dependent envelope through the
+entire orbit, its combination with the support-attaining class, and the
+resulting all-target constructor. The integer classification, six integer
+repairs, canonical ring theorem and canonical sign-dependent theorem remain
+credited predecessor results, used as lemmas rather than offered as an audit.
+
+## Interface and exact formula
+
+There are seven distinct dirty arrays `x0,x1,x2,y0,y1,y2,z` over a finite free
+module over a nonzero unital ring R. The maps Ai and Bj are arbitrary R-linear
+maps and need not commute. The only operations are
+
+```text
+Bj^s: z  += s Bj(xj)
+Ai^s: yi += s Ai(z)             s in {-1,+1}.
+```
+
+Sources remain immutable, outputs are never read, and z must restore. For a
+specified M in `{-1,0,1}^{3x3}`, require `yi += sum_j Mij Ai(Bj(xj))` for every
+choice of maps and initial data. Each call restores private scratch and obeys
+its complete port and head-return contract. A negative call subtracts the
+increment, rather than inverting Ai or Bj.
+
+Let S(M) contain Bj for each nonzero column and Ai for each nonzero row.
+Let delta(M) be one on the signed/permuted orbit of
+
+```text
+C = [[1,1,1], [1,1,-1], [1,-1,0]],
+```
+
+and zero otherwise. Let `sigma_F = p_F^+ + p_F^-` and
+`mu_F = min(p_F^+, p_F^-)`, for arbitrary positive complete call prices.
+For characteristic c, define
+
+```text
+c = 0:   b_F = sigma_F;               u_F = 2 sigma_F
+c >= 2:  b_F = min(sigma_F, c mu_F);   u_F = min(2 sigma_F, c mu_F).
+```
+
+**Theorem.** The exact minimum query bill is
+
+```text
+M = 0:    0
+M != 0:   sum_{F in S(M)} b_F + delta(M) min_{F in S(M)} (u_F - b_F).
+```
+
+Every orbit member has all six operators active. In characteristic two,
+`u_F = b_F = 2 mu_F`, so membership in the integer orbit incurs no surcharge.
+The formula is uniform in composite characteristic and rings with zero
+divisors. Preparation, admission and word-dependent control costs must be
+charged separately unless already included in the fixed call prices.
+
+## Proof
+
+**Active-operator lower bound.** Write `(a_F,d_F)` for the positive/negative
+occurrence counts of F. Restoring z and eliminating the initial dirt in each
+y imply `a_F-d_F = 0` in the prime subring. Each active operator must occur,
+and cannot occur just once. Thus in characteristic zero its counts dominate
+`(1,1)`; in characteristic c >= 2 they dominate `(1,1)`, `(c,0)` or `(0,c)`.
+Every active operator therefore costs at least b_F. These necessary conditions
+follow by isolating one input and taking identity maps. Inactive operators
+have positive costs and cannot lower this sum.
+
+**Support-attaining targets.** Ross Richardson's
+[#944](https://github.com/CrocSwap/integer-mult-bounds/pull/944) proves that every
+M outside the orbit has an integer word with exactly one positive and one
+negative call of each active operator, with inactive operators omitted.
+Its coefficient identities hold over every ring. In characteristic c,
+replace a call of sign -s by c-1 consecutive calls of sign s whenever the
+unary profile has a lower price. The replacement acts identically at every
+other query boundary since `(c-1)s = -s` in R. Apply this independently to each
+active operator. The resulting word costs exactly sum b_F, attaining the lower
+bound. This also covers zero rows or columns and the empty word for M = 0.
+
+**Cost-preserving transport, the new orbit step.** Suppose
+
+```text
+M[i,j] = r_i s_j C[pi(i),rho(j)],       r_i,s_j in {-1,+1}.
+```
+
+In a word for C, replace an old A[pi(i)] call of sign t by Ai of sign r_i t,
+and an old B[rho(j)] call of sign t by Bj of sign s_j t. Prefix source
+coefficients and read coefficients acquire the indicated signs, giving M;
+restoration identities remain zero. Inverse signed permutations give a
+bijection of all valid words, in both directions, over every R.
+
+Pull back the actual prices along this bijection. A negative r_i or s_j swaps
+the corresponding two sign prices; permutations relabel them. Both sigma_F
+and mu_F survive a sign swap, and the displayed sum and minimum survive the
+operator permutation. Consequently the canonical-target theorem of
+[#4241](https://github.com/CrocSwap/integer-mult-bounds/pull/4241), namely
+`sum b_F + min(u_F-b_F)`, gives precisely the same expression for M. This proves
+the lower bound and attainability throughout the orbit, completing the proof.
+The transport is a compilation rule for the emitted queries at fixed ports;
+it requires no runtime array permutation or free frame conversion.
+
+For explicit construction, #4241 supplies an anchored word for every operator
+F with F at `(c,0)` and the other five at `(1,1)`, in characteristic c. Global
+sign reversal preserves the target and selects `(0,c)` when cheaper. Its
+integer branch uses martinxxx9's six `(2,2)` repairs from
+[#1088](https://github.com/CrocSwap/integer-mult-bounds/pull/1088).
+`optimal_word` transports the anchor for the desired physical operator and
+then makes the independent cheaper-sign conversions. These predecessor
+constructions are retained with attribution; the transported family is new.
+
+## Finite evidence and reproduction
+
+From the repository root, with CPython 3.12:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/signed-matrix-price-classification/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -O -B research/signed-matrix-price-classification/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/signed-matrix-price-classification
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/signed-matrix-price-classification --check-source-history
+```
+
+The first two commands print `PASS_SIGNED_MATRIX_PRICE_CLASSIFICATION`.
+The registered replay checks:
+
+- All 19,683 targets in characteristics 0,2,3,4,5,8, at four exact integer price
+  vectors. Each of the 472,392 words has its full dirty-action coefficients and
+  actual signed bill checked against the closed formula.
+- Every orbit target, every repeated operator, both global signs, and
+  characteristics 0,2,3,4,5,8,12,16: 27,648 transported anchors. Both action and
+  exact signed occurrence profile are checked.
+- 6,912 additional orbit words at seeded rational prices in eight
+  characteristics; 768 finite count-profile dynamic programs; 2,304 dense
+  two-coordinate dirty-array executions using noncommuting maps; and 744
+  single-query deletion controls.
+
+The support-word table instantiates #944's existing recipe so that the new
+constructor can serve the entire target domain. Its 19,395/288 partition is
+inherited, and is not claimed as a new classification or independent audit.
+The hash-pinned certificates from #944 and #1088 are the only live external
+inputs. No pending executable or source-history object is imported.
+
+Every run prints a generated receipt digest bound to all package files and
+both live inputs. To retain the generated JSON, use `--receipt /path/outside`
+with a destination outside the checkout. No receipt is handwritten or committed.
+
+Python uses managed allocation. The evidence domains fix capacity at 19,683
+support/target keys, 288 transformations and at most 1,536 queries per word.
+All loops have finite bounds; there is no recursion or subprocess. Explicit
+exceptions keep checks enabled under optimized Python. Warnings are errors.
+
+## Limits and obligations
+
+The all-ring result is a written scoped proof using the cited predecessor
+lemmas, including the unmerged canonical theorem #4241 at head
+`ec573175d36cb016661f37293dd9ee2aefb737bb`. The new proof does not independently
+establish that theorem's lemmas. Finite executions do not enumerate every ring,
+price vector or characteristic. Independent human and formal proof-kernel
+review are unclaimed. A physical consumer, complete fixed prices, routing,
+preparation, precision, supplier admission and outer multiplication transfer
+remain uninstantiated. No selected cold replay or formal build was run.
+
+## Open next questions
+
+1. Can a concrete caller use one of these optimal words with a smaller complete
+   bill than its current schedule? Pin the caller, its demanded M and the actual
+   forward/inverse prices, then charge routing and admission as well as calls.
+2. Which signed rectangular targets admit both an integer `(2,2)` repair and a
+   characteristic-c unary anchor at every operator? A first step is a 3x4
+   obstruction with those two properties; without them the same count-profile
+   lower bound need not be attainable.
+
+## Credit and provenance
+
+Ross Richardson's #944 supplies the signed interface, 19,395 support-attaining
+targets and 288-member obstruction orbit, building on #943/#934 and the
+PR889/PR628 lineage. martinxxx9's #1088 supplies six arbitrary-operator integer
+repairs. Sagar Thakrar's #1349 supplies the characteristic-three predecessor.
+Nick Petalas's #4233 supplies the characteristic transfer and #4241 the
+canonical sign-dependent envelope and six unary anchors. This contribution
+proves sign-price invariance under signed permutations and the combined
+all-target theorem, with a constructor for all targets.
+
+Base `12fa8c5c844be21bfefb38a19503fbd867a11244`, priority revision 7.
+[Claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19082890).
+Exact source pins are in [SOURCES.json](SOURCES.json); structured next steps are
+in [TASK.json](TASK.json). Apache-2.0.

research/signed-matrix-price-classification/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81",
+      "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65",
+      "sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96"
+    },
+    {
+      "path": "research/signed-connector-obstruction/CERTIFICATE.json",
+      "usage": "input",
+      "git_blob": "2d047548111241783bd977115318317f0ad23302",
+      "sha256": "2930f0ae2c77cf94eadc9f065fe8d034249e5e607b9eb4e8f581d1c60f5e763b"
+    },
+    {
+      "path": "research/weighted-signed-connector-seed58/CERTIFICATE.json",
+      "usage": "input",
+      "git_blob": "abaa49bf8b1724461ba11fa37aa1df5e73ddf7bf",
+      "sha256": "30291599facabc902e85bda418e587d7af37760875b86f88607dbf2c9f38cbeb"
+    }
+  ]
+}

research/signed-matrix-price-classification/TASK.json

@@ -0,0 +1,95 @@
+{
+  "schema_version": 1,
+  "task_id": "connector-alphabet-change",
+  "priority_revision": 7,
+  "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244",
+  "original_card": {
+    "id": "connector-alphabet-change",
+    "question": "Does one explicit extension of the connector alphabet offer a favorable completed budget?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "research/universal-connector-boundary/README.md",
+      "certificates/selected-result.json"
+    ],
+    "methods": [
+      "Construct and charge a legal extra operation on a minimal instance.",
+      "Prove a target-specific bound after adding one specified operation family."
+    ],
+    "acceptance_gate": "State which fixed-alphabet premise changes and charge its implementation; do not declare it free. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "research/universal-connector-boundary/verify.py"
+      ],
+      "expected": "PASS_UNIVERSAL_CONNECTOR_BOUNDARY",
+      "inspect": "Reproduce the 945-pairing control, then read Exact interface to list the allowed calls.",
+      "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay."
+    },
+    "first_experiment": "Add exactly one legally priced operation and test a tiny dirty-input instance before enumerating larger cases.",
+    "bottleneck_link": "A new legal connector operation could change recursive interface cost; a larger census in the same alphabet is a separate side result.",
+    "allowed_variations": [
+      "Choose one additional operation and a small source count for its first counterexample."
+    ],
+    "scope_change_triggers": [
+      "Keeping the alphabet and only increasing the source count; record this as a changed assignment.",
+      "Extending a source-count census without naming a supplier/interface decision it could change; audit #2973 pruning concerns before relying on the affected predecessor exclusions."
+    ],
+    "overlap_terms": [
+      "universal connector",
+      "source-toggle",
+      "connector alphabet"
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Exact sign-dependent query bill and an attaining constructor for all 19,683 signed 3x3 dirty-connector targets over every coefficient characteristic.",
+  "scope_change_reason": "Keeps the existing signed alphabet and extends the explicitly open target-domain question of PR4241. This is a pricing and classification side result, not the added-operation supplier experiment requested by the generic card.",
+  "bottleneck_link": "A caller with asymmetric complete forward/inverse prices can select a provably optimal word for its actual signed 3x3 demand. No concrete supplier or downstream exponent saving is asserted.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at a counterexample to price-preserving signed-permutation transport; otherwise finish after complete finite target-domain construction checks and scoped proof.",
+  "outcome": "completed",
+  "evidence": "Written all-ring transport and support-attaining proof; 472392 complete priced words over every signed 3x3 target, 27648 transported anchors, 6912 rational-price orbit words, 768 count-profile DPs, 2304 dense executions and 744 deletion controls.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Can a concrete recursive caller save complete cost using the all-target constructor?",
+      "why_it_matters": "The query optimum becomes a supplier improvement only after its caller and all other costs are supplied.",
+      "first_step": "Pin one caller, demand matrix and actual forward/inverse prices, then compare routing, admission and total schedules.",
+      "blocked_by": "No physical caller or complete prices are instantiated."
+    },
+    {
+      "question": "Which 3x4 signed obstructions admit an arbitrary-operator integer repair and finite-characteristic unary anchor?",
+      "why_it_matters": "Those two attainment properties are needed to extend this count-profile envelope beyond 3x3.",
+      "first_step": "Find one 3x4 support obstruction, then construct both kinds of repair at each active operator.",
+      "blocked_by": "No general rectangular support or repair classification is claimed."
+    }
+  ],
+  "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19082890",
+  "predecessor_theorems": [
+    {
+      "pr": 4241,
+      "head": "ec573175d36cb016661f37293dd9ee2aefb737bb",
+      "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/4241",
+      "scope": "Canonical sign-dependent envelope and six anchors; used as a theorem, not independently audited. The six templates are restated in verify.py.",
+      "readme_sha256": "365483c2b4409d4f51f28cbed736e51ec13df6303b81387768b640c59b59cea2"
+    },
+    {
+      "pr": 4233,
+      "head": "d56d43c726dddc37a97a5dabf9d13ef861394133",
+      "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/4233",
+      "scope": "Canonical coefficient-ring transfer, through PR4241."
+    }
+  ],
+  "upstream_checkpoint": {
+    "commit": "12fa8c5c844be21bfefb38a19503fbd867a11244",
+    "priority_revision": 7,
+    "checked_at_utc": "2026-10-20T21:57:38Z",
+    "relevant_changes": "No upstream change from the scientific base."
+  },
+  "environment": {
+    "python": "3.12.15",
+    "platform": "macOS-27.0.1-arm64-arm-64bit",
+    "dependencies": "Python standard library only"
+  }
+}

research/signed-matrix-price-classification/VERIFY.json

@@ -0,0 +1,35 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/signed-connector-obstruction/CERTIFICATE.json",
+    "research/weighted-signed-connector-seed58/CERTIFICATE.json"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 180,
+      "checks": "Complete signed target-domain priced construction, orbit anchor transport, rational prices, independent profile DP, dense dirty action and query deletion controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-W",
+        "error",
+        "-O",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 180,
+      "checks": "Repeat all scientific checks with assertions disabled; explicit invariant checks must remain effective."
+    }
+  ]
+}