diff --git a/research/signed-matrix-price-classification/README.md b/research/signed-matrix-price-classification/README.md new file mode 100644 index 0000000000..e19e55cc74 --- /dev/null +++ b/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. diff --git a/research/signed-matrix-price-classification/SOURCES.json b/research/signed-matrix-price-classification/SOURCES.json new file mode 100644 index 0000000000..39ebc1b59c --- /dev/null +++ b/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" + } + ] +} diff --git a/research/signed-matrix-price-classification/TASK.json b/research/signed-matrix-price-classification/TASK.json new file mode 100644 index 0000000000..b19123b09e --- /dev/null +++ b/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" + } +} diff --git a/research/signed-matrix-price-classification/VERIFY.json b/research/signed-matrix-price-classification/VERIFY.json new file mode 100644 index 0000000000..c3e00f2f1b --- /dev/null +++ b/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." + } + ] +} diff --git a/research/signed-matrix-price-classification/verify.py b/research/signed-matrix-price-classification/verify.py new file mode 100644 index 0000000000..4e843dad5a --- /dev/null +++ b/research/signed-matrix-price-classification/verify.py @@ -0,0 +1,337 @@ +#!/usr/bin/env python3 +"""Construct optimal priced words for the complete signed 3-by-3 domain.""" + +import argparse +import hashlib +import itertools +import json +import random +from fractions import Fraction +from pathlib import Path + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parent.parent +TARGET = (1, 1, 1, 1, 1, -1, 1, -1, 0) +NAMES = ("B0", "B1", "B2", "A0", "A1", "A2") +CHARS = (0, 2, 3, 4, 5, 8) +MAX_CHAR = 256 +MAX_WORD = 6 * MAX_CHAR + +# Restated from Nick Petalas's PR4241, head ec573175d36cb016661f37293dd9ee2aefb737bb. +# A starred token means c-2 consecutive copies. These are predecessor words. +TEMPLATES = ( + "B1- A1- A2+ B2- A0- B1+ B0+ A1+ B2+ A0+ B0+* A2- B0+", + "B1+ A0+ B1+* A2+ B0- A1- B1+ A2- B2- A0- B0+ A1+ B2+", + "A2- B1- B2+ A1- B2+* A0- B0+ B2+ A2+ B1+ A1+ A0+ B0-", + "A0+* B2+ A0+ A1- B2- B1+ A2- B0+ A0+ A1+ B1- A2+ B0-", + "A1+ B2+ A1+* B0+ A2+ B1+ A1+ A0+ B0- A2- B2- B1- A0-", + "A2+ A1- B2- A0- B0+ B1+ A1+ B2+ A2+ A0+ B0- A2+* B1-", +) + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def sha(data): + return hashlib.sha256(data).hexdigest() + + +def inputs(): + manifest = json.loads((PACKAGE / "SOURCES.json").read_text()) + result = {} + for row in manifest["files"]: + if row["usage"] == "input": + data = (ROOT / row["path"]).read_bytes() + require(sha(data) == row["sha256"], "source hash: " + row["path"]) + result[row["path"]] = json.loads(data) + require(len(result) == 2, "two live predecessor inputs") + return result + + +def active(matrix): + columns = tuple(j for j in range(3) if any(matrix[3*i+j] for i in range(3))) + rows = tuple(3+i for i in range(3) if any(matrix[3*i:3*i+3])) + return columns + rows + + +def action(word): + """Exact coefficients, sufficient for arbitrary noncommuting maps.""" + require(len(word) <= MAX_WORD, "word capacity") + q, dirt, matrix = [0]*3, [0]*3, [0]*9 + for op, sign in word: + require(op in range(6) and sign in (-1, 1), "query domain") + if op < 3: + q[op] += sign + else: + i = op - 3 + dirt[i] += sign + for j in range(3): + matrix[3*i+j] += sign*q[j] + return q + dirt + matrix + + +def correct(word, matrix, char): + residual = action(word) + residual[6:] = [a-b for a, b in zip(residual[6:], matrix)] + return all((x % char if char else x) == 0 for x in residual) + + +def profile(word): + counts = [[0, 0] for _ in range(6)] + for op, sign in word: + counts[op][sign < 0] += 1 + return tuple(tuple(pair) for pair in counts) + + +def orbit(): + """Return one explicit signed-permutation map for each orbit target.""" + result = {} + signs = tuple(itertools.product((-1, 1), repeat=3)) + for rows, cols in itertools.product(itertools.permutations(range(3)), repeat=2): + for rs, cs in itertools.product(signs, repeat=2): + matrix = tuple(rs[i]*cs[j]*TARGET[3*rows[i]+cols[j]] + for i in range(3) for j in range(3)) + mapping = tuple((cols.index(j), cs[cols.index(j)]) for j in range(3)) + mapping += tuple((3+rows.index(i), rs[rows.index(i)]) for i in range(3)) + result.setdefault(matrix, mapping) + require(len(result) == 288, "orbit cardinality") + return result + + +def transform(word, mapping): + return tuple((mapping[op][0], sign*mapping[op][1]) for op, sign in word) + + +def readout_word(path, pairs, matrix): + word = [] + needed = active(matrix) + for slot in range(7): + for i, (minus, plus) in enumerate(pairs): + if i+3 in needed: + if minus == slot: + word.append((i+3, -1)) + if plus == slot: + word.append((i+3, 1)) + if slot < 6 and path[slot][0] in needed: + word.append(path[slot]) + return tuple(word) + + +def support_words(): + """Instantiate PR944's support-word recipe; no exclusion is re-proved.""" + result = {} + moves = tuple((j, s) for j in range(3) for s in (-1, 1)) + for path in itertools.permutations(moves): + q, vertices = [0]*3, [(0, 0, 0)] + for j, sign in path: + q[j] += sign + vertices.append(tuple(q)) + pairs = {} + for minus, plus in itertools.product(range(7), repeat=2): + row = tuple(a-b for a, b in zip(vertices[plus], vertices[minus])) + pairs.setdefault(row, (minus, plus)) + for rows in itertools.product(pairs, repeat=3): + matrix = rows[0] + rows[1] + rows[2] + if matrix not in result: + result[matrix] = readout_word(path, [pairs[r] for r in rows], matrix) + require(len(result) == 19395, "PR944 support-word coverage") + return result + + +def template(op, char): + word = [] + for token in TEMPLATES[op].split(): + query = (NAMES.index(token[:2]), 1 if token[2] == "+" else -1) + word.extend([query] * (char-2 if token.endswith("*") else 1)) + return tuple(word) + + +def envelope(matrix, prices, char, obstructed): + operators = active(matrix) + if not operators: + return 0 + sigma = [prices[2*k] + prices[2*k+1] for k in operators] + mu = [min(prices[2*k:2*k+2]) for k in operators] + b = [min(s, char*m) if char else s for s, m in zip(sigma, mu)] + u = [min(2*s, char*m) if char else 2*s for s, m in zip(sigma, mu)] + return sum(b) + (min(v-w for v, w in zip(u, b)) if obstructed else 0) + + +def optimal_word(matrix, prices, char, support, transforms, repairs): + """Price-aware orbit transport followed by local sign conversion.""" + if matrix in support: + base = support[matrix] + else: + mapping = transforms[matrix] + sigma = [prices[2*k]+prices[2*k+1] for k in range(6)] + mu = [min(prices[2*k:2*k+2]) for k in range(6)] + cheap = [k for k in range(6) if char and char*mu[k] <= sigma[k]] + extra = [min(2*s, char*m)-s if char else s for s, m in zip(sigma, mu)] + chosen = cheap[0] if cheap else min(range(6), key=extra.__getitem__) + old = next(k for k in range(6) if mapping[k][0] == chosen) + if char and (cheap or char*mu[chosen] < 2*sigma[chosen]): + base = transform(template(old, char), mapping) + keep = 1 if prices[2*chosen] <= prices[2*chosen+1] else -1 + if mapping[old][1] != keep: + base = tuple((op, -s) for op, s in base) + else: + base = transform(repairs[old], mapping) + counts = profile(base) + result = [] + for op, sign in base: + plus, minus = prices[2*op:2*op+2] + if char and counts[op] == (1, 1) and char*min(plus, minus) <= plus+minus: + keep = 1 if plus <= minus else -1 + result.extend([(op, keep)] * (1 if sign == keep else char-1)) + else: + result.append((op, sign)) + require(len(result) <= MAX_WORD, "constructed word capacity") + return tuple(result) + + +def checked_case(matrix, prices, char, support, transforms, repairs): + word = optimal_word(matrix, prices, char, support, transforms, repairs) + require(correct(word, matrix, char), "constructed dirty action") + bill = sum(prices[2*op+(sign < 0)] for op, sign in word) + expected = envelope(matrix, prices, char, matrix in transforms) + require(bill == expected, "constructed bill differs from closed envelope") + return word + + +def transport_checks(transforms, repairs): + cases = 0 + for matrix, mapping in transforms.items(): + require(sorted(op for op, _ in mapping) == list(range(6)), "operator permutation") + for old, char, flip in itertools.product(range(6), (0, 2, 3, 4, 5, 8, 12, 16), (-1, 1)): + base = template(old, char) if char else repairs[old] + word = transform(tuple((op, sign*flip) for op, sign in base), mapping) + require(correct(word, matrix, char), "transported anchor action") + expected = [(1, 1)]*6 + new, sign = mapping[old] + expected[new] = ((char, 0) if sign*flip == 1 else (0, char)) if char else (2, 2) + require(profile(word) == tuple(expected), "transported anchor profile") + cases += 1 + return cases + + +def related_values(): + unit = [envelope(TARGET, (1,)*12, c, True) for c in (0, 2, 3, 4, 5, 8)] + asymmetric = [envelope(TARGET, (1, 3)*6, c, True) for c in (0, 3, 4, 5, 8)] + require(unit == [14, 12, 13, 14, 14, 14], "PR4233 equal-sign specialization") + require(asymmetric == [28, 18, 24, 25, 28], "PR4241 canonical specialization") + return {"PR4233_unit": unit, "PR4241_asymmetric": asymmetric} + + +def count_profile_bound(matrix, prices, char, obstructed): + """Independent finite DP over legal per-operator plus/minus counts.""" + costs = {False: 0} + bound = max(4, 2*char) + for op in active(matrix): + choices = {} + for plus, minus in itertools.product(range(bound+1), repeat=2): + diff = plus-minus + if plus+minus < 2 or (diff % char if char else diff) != 0: + continue + raised = (plus, minus) != (1, 1) + price = plus*prices[2*op] + minus*prices[2*op+1] + choices[raised] = min(choices.get(raised, price), price) + updated = {} + for old, value in costs.items(): + for raised, price in choices.items(): + flag = old or raised + updated[flag] = min(updated.get(flag, value+price), value+price) + costs = updated + return costs[True] if obstructed and char != 2 else min(costs.values()) + + +def dense(word, matrix, char, seed): + """Independent literal 2-coordinate, noncommuting dirty-array execution.""" + a = (((1, 2), (0, 1)), ((0, 1), (-1, 3)), ((2, 0), (1, -1))) + b = (((1, 0), (1, 1)), ((3, -1), (2, 0)), ((0, 2), (1, 1))) + initial = [[((seed+3)*(2*i+1)+j*j) % 11 - 5 for j in range(2)] for i in range(7)] + state = [row[:] for row in initial] + expected = [row[:] for row in initial] + for i, j in itertools.product(range(3), repeat=2): + bx = [sum(b[j][r][s]*initial[j][s] for s in range(2)) for r in range(2)] + for r in range(2): + expected[i+3][r] += matrix[3*i+j]*sum(a[i][r][s]*bx[s] for s in range(2)) + for op, sign in word: + source, target, linear = (op, 6, b[op]) if op < 3 else (6, op, a[op-3]) + increment = [sum(linear[r][s]*state[source][s] for s in range(2)) for r in range(2)] + for r in range(2): + state[target][r] += sign*increment[r] + residual = [state[i][j]-expected[i][j] for i in range(7) for j in range(2)] + require(all((v % char if char else v) == 0 for v in residual), "dense dirty replay") + + +def evidence(support, transforms, repairs): + matrices = tuple(itertools.product((-1, 0, 1), repeat=9)) + require(set(support).isdisjoint(transforms), "classification partition") + require(set(support) | set(transforms) == set(matrices), "full target domain") + vectors = ((1,)*12, (1, 3)*6, tuple(range(1, 13)), (3, 1, 1, 7, 4, 2, 2, 9, 6, 1, 5, 3)) + cases = 0 + for matrix, char, prices in itertools.product(matrices, CHARS, vectors): + checked_case(matrix, prices, char, support, transforms, repairs) + cases += 1 + dense_cases = random_cases = dp_cases = controls = 0 + rng = random.Random(4241) + samples = [matrices[0], matrices[-1], (0,)*9, TARGET] + samples += [matrices[rng.randrange(len(matrices))] for _ in range(28)] + for case in range(24): + prices = tuple(Fraction(rng.randrange(1, 20), rng.randrange(1, 8)) for _ in range(12)) + char = (0, 2, 3, 4, 5, 8, 12, 16)[case % 8] + for matrix in transforms: + checked_case(matrix, prices, char, support, transforms, repairs) + random_cases += 1 + for matrix in samples: + word = checked_case(matrix, prices, char, support, transforms, repairs) + for seed in range(3): + dense(word, matrix, char, seed) + dense_cases += 1 + require(count_profile_bound(matrix, prices, char, matrix in transforms) + == envelope(matrix, prices, char, matrix in transforms), "profile DP") + dp_cases += 1 + if word: + require(not correct(word[:-1], matrix, char), "deleted last query control") + controls += 1 + return {"targets": len(matrices), "orbit": len(transforms), "priced_words": cases, + "rational_orbit_words": random_cases, "profile_dp": dp_cases, + "dense_cases": dense_cases, "deletion_controls": controls} + + +def receipt(counts): + files = {p.name: sha(p.read_bytes()) for p in sorted(PACKAGE.iterdir()) if p.is_file()} + manifest = json.loads((PACKAGE / "SOURCES.json").read_text()) + live = {r["path"]: sha((ROOT/r["path"]).read_bytes()) + for r in manifest["files"] if r["usage"] == "input"} + return {"schema_version": 1, "counts": counts, "package_sha256": files, + "input_sha256": live} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--receipt", type=Path, help="write generated source-bound JSON outside checkout") + args = parser.parse_args() + if args.receipt: + require(not args.receipt.resolve().is_relative_to(ROOT), "receipt must be outside checkout") + data = inputs() + source = data["research/weighted-signed-connector-seed58/CERTIFICATE.json"] + repairs = tuple(tuple((NAMES.index(k+str(i)), s) for k, i, s in source["witnesses"][name]) + for name in NAMES) + transforms, support = orbit(), support_words() + listed = data["research/signed-connector-obstruction/CERTIFICATE.json"]["obstructed_patterns"] + require(set(transforms) == {tuple(v for row in m for v in row) for m in listed}, "orbit input") + counts = evidence(support, transforms, repairs) + counts["transported_anchors"] = transport_checks(transforms, repairs) + counts["related_values"] = related_values() + result = receipt(counts) + if args.receipt: + args.receipt.write_text(json.dumps(result, indent=2, sort_keys=True)+"\n") + print("PASS_SIGNED_MATRIX_PRICE_CLASSIFICATION " + json.dumps(counts, sort_keys=True)) + print("GENERATED_RECEIPT_SHA256 " + sha(json.dumps(result, sort_keys=True).encode())) + + +if __name__ == "__main__": + main()