diff --git a/research/signed-duplication-tariff/README.md b/research/signed-duplication-tariff/README.md new file mode 100644 index 0000000000..3b504dee93 --- /dev/null +++ b/research/signed-duplication-tariff/README.md @@ -0,0 +1,262 @@ +# Exact tariffs for rectangular duplications of the signed obstruction + +produced by Nick Petalas + +This is a **scoped proof with finite corroboration**. For arbitrary nonempty +row and column groups, it determines every minimal call-count profile and the +exact positive, equal-by-sign query tariff of the replicated signed connector +target. The extra calls must cover a whole group. Repeating only the cheapest +individual operator can be insufficient. There is no new kappa or complete +multiplication theorem. + +The result extends the rectangular-target direction in +[#4258](https://github.com/CrocSwap/integer-mult-bounds/pull/4258), with symmetric +sign prices. It uses Ross Richardson's canonical obstruction, martinxxx9's +integer repairs, Sagar Thakrar's ternary repairs and the characteristic transfer +of [#4233](https://github.com/CrocSwap/integer-mult-bounds/pull/4233) as predecessor +results. Their results are dependencies, rather than the subject of an audit. + +## Boundary and theorem + +Let X0,X1,X2 partition the source indices and Y0,Y1,Y2 partition the output +indices. All six groups are nonempty and finite. Write G for this six-group +partition and N for its total size. Set + +```text +C = [[1,1,1], [1,1,-1], [1,-1,0]] +M[i,j] = C[a,b] when i is in Ya and j is in Xb. +``` + +The arrays xj, yi and z are distinct, initially arbitrary elements of a finite +free module over a nonzero unital ring R of characteristic c. The maps Ai and +Bj are arbitrary compatible R-linear maps. They may be singular and need not +commute. Target duplication does not identify these maps or their data. +The permitted complete calls, each charged separately, are + +```text +Bj^s: z += s Bj(xj) +Ai^s: yi += s Ai(z) s in {-1,+1}. +``` + +Sources are immutable, outputs are never read, and z must restore. The final +increment of yi is sum_j M[i,j] Ai(Bj(xj)). Each call preserves every other +data role and returns private scratch and heads. Coefficient preparation, +admission, instruction storage and control remain separately chargeable. +There are no extra connectors, frame operations or combined queries. + +For any operator F let pF > 0 be its complete call price, the same for both +signs. Define P(H) = sum of pF over operators F in group H, S = sum_F pF, and + +```text +alpha(c) = 0 if c = 2 + 1 if c = 3 + 2 if c = 0 or c >= 4. +``` + +**Theorem.** The exact minimum query bill over all finite legal words is + +```text +OPT = 2 S + alpha(c) min_{H in G} P(H). +``` + +More strongly, in characteristic three the six Pareto-minimal occurrence +vectors are `nF = 2 + 1[F in H]`, one for each group H. In characteristic zero +or at least four they are `nF = 2 + 2*1[F in H]`. In characteristic two there +is just the vector with every nF = 2. These statements count both signs +together. They do not classify all signed words attaining a vector. + +The unit-price optimum is `2N + alpha(c) min_H |H|`. When every group has two +members, the 6x6 target therefore needs exactly 24, 26 and 28 calls in +characteristics two, three and zero or at least four, respectively. + +An asymmetric group example has source group sizes 2,1,1 and output group sizes +1,1,1. Prices in that order are `(1,100,10,10,10,10,10)`. Here S = 151 and the +cheapest whole group costs 10. The characteristic-zero optimum is **322**. +Using the cheapest individual price as the surcharge would give 304, which +does not meet the transversal obstruction. + +## Proof + +### Restriction to a transversal + +Choose one operator from each group. Set every unchosen Bj to zero and ignore +every unchosen output. Delete their calls from any purported legal word. +Chosen readouts see exactly the same connector, and deletion cannot change a +chosen source or the connector restoration equation. The remaining word is a +legal canonical C program for arbitrary maps on those six selected operators. +Thus the canonical obstruction applies to every six-group transversal. + +Every operator is active because every row and column of C is nonzero. +Restoration forces the signed occurrence sum of each Bj to vanish in the +prime subring of R. Eliminating arbitrary initial z dirt forces the same for +each Ai. One occurrence cannot vanish in a nonzero unital ring. Hence every +operator occurs at least twice. + +For c >= 3, if each operator in one selected transversal occurs exactly twice, +its two signs must be opposite. A source prefix coordinate then takes values +in {0,1} or {0,-1}. Each paired readout coefficient belongs to {-1,0,1}. +These three elements have distinct images in characteristic c >= 3, as they +do in characteristic zero. A correct modular paired word for C would therefore +be an integer paired word for C. Richardson's +[#944](https://github.com/CrocSwap/integer-mult-bounds/pull/944) excludes such a +word. This is the no-aliasing transfer used in #4233; zero divisors introduce +no exception to the distinctness of these prime-subring elements. + +Consequently every transversal contains an operator with more than two calls. +For c = 3 that operator has at least three calls. For c = 0 or c >= 4 it has +at least four: a sum of three signs is one of -3,-1,1,3, none of which vanishes +in those characteristics. These are necessary conditions on every finite +word, without any word-length cutoff. + +### The whole-group step, the new lower bound + +Let E be the set of operators with more than two calls. The preceding argument +says that E meets every transversal. A subset meets every transversal of six +nonempty groups if and only if it contains one whole group. Indeed, if no +group is contained in E, choose an operator outside E in each group to get a +disjoint transversal. The reverse implication is immediate. + +Therefore some entire group H consists of operators with at least +`2 + alpha(c)` calls. Every other operator has at least two. This proves +componentwise domination of one displayed vector and the claimed weighted +lower bound. Characteristic two only needs the active-operator lower bound. + +### Batching attains every displayed profile + +For c = 0 or c >= 4, take martinxxx9's +[#1088](https://github.com/CrocSwap/integer-mult-bounds/pull/1088) integer repair +that calls the canonical operator corresponding to H four times, and every +other canonical operator twice. It is an integer identity, so it remains valid +over every R. For c = 3, use Sagar Thakrar's +[#1349](https://github.com/CrocSwap/integer-mult-bounds/pull/1349) repair with +the chosen canonical operator called three times and the others twice. + +Replace each canonical Bj call by one call, with its sign, to every source +operator in Xj. Replace each canonical Ai call by one call, with its sign, +to every output operator in Yi. Each replacement is an actual sequence of +complete calls at fixed ports. No combined query is priced as one call. +Source batches leave z with the indicated sum of independent Bj(xj) terms. +Output batches visit distinct arrays without changing z. Thus every pair of +an output and source acquires exactly C[a,b] Ai(Bj(xj)), arbitrary initial +connector dirt cancels, and z restores. This proof uses only distributivity +and additivity, so it applies to noncommuting maps over every R. + +In characteristic two, batch the following canonical twelve-call word: + +```text +B0+ B1+ B2+ A0+ A1+ B2- A2+ B1- B0- A0- A1- A2- +``` + +Its integer target is `[[1,1,1],[1,1,1],[1,1,0]]`, which equals C modulo two. +It calls every operator twice. These constructions attain every displayed +profile. The six profiles are pairwise incomparable because the groups are +disjoint and nonempty. Componentwise domination now proves the Pareto claim +and completes the exact tariff proof. + +## Finite evidence and reproduction + +From the repository root, with the standard library of CPython 3.12: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/signed-duplication-tariff/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -O -B research/signed-duplication-tariff/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/signed-duplication-tariff +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/signed-duplication-tariff --check-source-history +``` + +Any CPython 3.12 interpreter can replace the local interpreter path. The direct +checks print `PASS_SIGNED_DUPLICATION_TARIFF` with: + +- 30,618 construction cases, all six forced profiles for all 729 group-size + vectors in {1,2,3}^6, in characteristics 0,2,3,4,5,8,12. Exact formal + coefficients check every demanded pair, connector restoration and dirt. +- 2,240 optimal priced words, using uniform prices and seeded positive rational + prices for all 64 group-size vectors in {1,2}^6 in those characteristics. +- 46,656 exceptional-operator subsets over the same 64 shapes, with all 729 + shape-specific transversals. Direct subset enumeration checks the cover + equivalence, all minimal covers and the weighted minimum independently of + the closed group formula. +- 504 literal two-coordinate dirty-array executions and inverse round trips, + including independent noncommuting Ai,Bj matrices and four shapes of up to + 15 operators. Sources and connector restore exactly. +- 672 negative controls, consisting of 665 single-query deletions, the 304 + underbilling example and six invalid shape/price/characteristic inputs. + +These checks test the new replication and cover extension. They do not replay +the predecessor canonical censuses. The two predecessor certificates are live +SHA-256-pinned inputs, used for their six anchors each. No predecessor +executable is imported. The unmerged #4233 theorem is cited at +`d56d43c726dddc37a97a5dabf9d13ef861394133`; no pending Git object or executable +is needed by replay. Its elementary no-aliasing argument is given above, and +#944 remains the credited finite obstruction dependency. + +Every run generates a receipt bound to all package files and both live inputs. +Use `--receipt /path/outside/receipt.json` to save it outside the checkout. +No receipt is handwritten or committed. `VERIFY.json` registers normal and +optimized checks with warnings as errors and a 60-second limit per command. + +## Obligation ledger and limits + +The arbitrary-group-size theorem is a written scoped proof using the stated +predecessor lemmas. The finite domains corroborate it; they do not enumerate +all rings, prices or group sizes. Independent human and formal proof-kernel +review are unclaimed. + +The exact query lower bound is proved, and a literal abstract-call word +constructively attains it. Fixed complete prices are assumptions of the query +model. A physical caller with this demand, instantiated complete prices, +preparation, routing, layout, precision, stock, control and supplier admission +are unknown. Unknown costs are not zero. There is no consumer bill or claimed +recursive gain for downstream cleanup to preserve. This is a local interface +result, with no further construction campaign undertaken. No selected cold +replay, Lean build or outer multiplication transfer was run. + +The verifier is deliberately finite: group sizes are at most four, with at +most 24 operators, 96 queries per word and 144 pair coefficients. Its exhaustive +subset domain is at most 4096 subsets per shape. It has no recursion, +subprocess, dynamic code generation or network calls. Python requires managed +allocation, a deviation from Power of Ten rule 3. These fixed capacities bound +live mathematical state; the standard interpreter and JSON parser still +allocate internally. External certificate bytes come from the two hash-pinned +committed inputs. Each read is capped at 2 MiB and each metadata inventory at +16 rows. Revisit these limits before increasing evidence domains. +All functions stay under 60 lines, explicit exceptions survive optimized +Python, and warnings are errors. No repository-wide analysis configuration +is changed. + +## Open next questions + +1. What is the exact tariff if the two signs of each operator have different + prices within a duplicated group? This matters because a common batched + chronology may not attain the individually cheapest mixture of unary and + four-call profiles. Start with one duplicated canonical operator and mixed + sign preferences, retaining all other operators twice. Common-chronology + attainment and a matching lower bound are open; #4241 alone does not settle + them. +2. Which genuinely new 3x4 patterns have an exact tariff beyond row or column + replication? Such patterns can have overlapping canonical obstructions + without the complete-transversal structure used here. Start with one + specified fourth column, derive its obstruction-cover lower bound and seek + matching literal words. A general rectangular classification and a real + physical caller are absent. + +## Credit and provenance + +Ross Richardson's #944 supplies the canonical signed obstruction, interface +and paired-path reduction. martinxxx9's #1088 supplies the six integer repairs. +Sagar Thakrar's #1349 supplies the six ternary repairs. Nick Petalas's #4233 +supplies the characteristic transfer and #4258 identifies the rectangular +extension direction. This contribution supplies the transversal whole-group +lower bound, replicated attaining words and exact Pareto/tariff theorem for +arbitrary multiplicities. It claims no priority for modular cancellation or +standard batching. + +The lineage includes Richardson's #934/#943 binary connectors, CubeJerry's +#889 signed fanout contract and Chafik Boukhalfa's #628 dirty commutator and +literal inverse convention. Their predecessor credit is retained. Frozen +packages and the selected record are unchanged. Source README and notice +provenance is pinned in [SOURCES.json](SOURCES.json). + +Base `12fa8c5c844be21bfefb38a19503fbd867a11244`, priority revision 7. +[Claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19085440). +Structured scope and next questions are in [TASK.json](TASK.json). Apache-2.0. diff --git a/research/signed-duplication-tariff/SOURCES.json b/research/signed-duplication-tariff/SOURCES.json new file mode 100644 index 0000000000..8bf38f3085 --- /dev/null +++ b/research/signed-duplication-tariff/SOURCES.json @@ -0,0 +1,60 @@ +{ + "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/ternary-connector-independent-seed84/CERTIFICATE.json", + "usage": "input", + "git_blob": "6d309616c6626d50531cfb522d8227483ffbccc7", + "sha256": "a814ec93439ea36878fd1b6ebd3c19c3151b27e474ca0edc3d0a14c290d82b7c" + }, + { + "path": "research/weighted-signed-connector-seed58/CERTIFICATE.json", + "usage": "input", + "git_blob": "abaa49bf8b1724461ba11fa37aa1df5e73ddf7bf", + "sha256": "30291599facabc902e85bda418e587d7af37760875b86f88607dbf2c9f38cbeb" + }, + { + "path": "research/signed-connector-obstruction/README.md", + "usage": "provenance", + "git_blob": "f07370732c8bbe6c49b502308a657a6eb94a019e", + "sha256": "76e20674799a7b35dfb5908e7df5cab53f17482da2bfd25db576ba0000dade83" + }, + { + "path": "research/signed-connector-obstruction/NOTICE.md", + "usage": "provenance", + "git_blob": "037d5c6193921ed1b56038ac0f0d7a5f964aa091", + "sha256": "0a99079d85344f195f58472e0aca5002888c636309fb80f20d1df04c700facc3" + }, + { + "path": "research/weighted-signed-connector-seed58/README.md", + "usage": "provenance", + "git_blob": "cb3a42764fa80041c79e0419b80c3e87b6d254a2", + "sha256": "53cfd7805b48ddf8143e1120de74845d287e4806be9669e61989c0ad45b985ec" + }, + { + "path": "research/weighted-signed-connector-seed58/NOTICE.md", + "usage": "provenance", + "git_blob": "f4e763bba6c67aa14efe0247f8c530a06b9826b5", + "sha256": "fb7c34c6745dcb79bcf63dab3370ed24b2ec6f776d1bd3e1cae3905c0f4e3dd9" + }, + { + "path": "research/ternary-connector-independent-seed84/README.md", + "usage": "provenance", + "git_blob": "9e04b46a3d1299265eda0a95e7938865f1d3026a", + "sha256": "d398cb9497d68ef5ee44d30b2a4b580bd551d202db03ec7a3e1695b30f1ebc7f" + } + ] +} diff --git a/research/signed-duplication-tariff/TASK.json b/research/signed-duplication-tariff/TASK.json new file mode 100644 index 0000000000..0768bfad95 --- /dev/null +++ b/research/signed-duplication-tariff/TASK.json @@ -0,0 +1,68 @@ +{ + "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 Pareto call-count profiles and equal-by-sign tariffs for arbitrary nonempty row/column duplications of the canonical signed 3x3 obstruction, over every nonzero unital coefficient ring.", + "scope_change_reason": "The alphabet remains signed source/readout calls; the changed premise is the replicated rectangular demand. This answers the rectangular extension direction of PR4258 rather than adding an operation to the card alphabet.", + "bottleneck_link": "Scoped recursive-interface side result: whole-group surcharge replaces the canonical single-operator surcharge. No physical caller or supplier saving is asserted.", + "budget_minutes": 60, + "stop_rule": "Ship the first proved replicated-target tariff with bounded corroboration; do not extend to arbitrary rectangular targets or sign-asymmetric prices.", + "outcome": "completed", + "evidence": "Written arbitrary-multiplicity proof; 30618 literal coefficient/profile cases, 2240 priced words, 46656 cover subsets, 504 dense dirty-map round trips and 672 controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "What is the exact tariff with different forward/inverse prices within a duplicated group?", + "why_it_matters": "Individual unary and four-call optima may require incompatible common chronologies.", + "first_step": "Duplicate one canonical operator, give its members mixed sign preferences and seek attainable words with every other operator called twice.", + "blocked_by": "No common-chronology attainment theorem or matching lower bound is supplied." + }, + { + "question": "Which nonreplicated signed 3x4 patterns have a sharp obstruction-cover tariff?", + "why_it_matters": "They may contain overlapping obstructions without complete-transversal structure.", + "first_step": "Choose one fourth column, derive its projected lower bound and search for matching literal words.", + "blocked_by": "General rectangular classification and an instantiated physical caller are absent." + } + ] +} diff --git a/research/signed-duplication-tariff/VERIFY.json b/research/signed-duplication-tariff/VERIFY.json new file mode 100644 index 0000000000..6dfceb7b05 --- /dev/null +++ b/research/signed-duplication-tariff/VERIFY.json @@ -0,0 +1,35 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/ternary-connector-independent-seed84/CERTIFICATE.json", + "research/weighted-signed-connector-seed58/CERTIFICATE.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "New replicated-word coefficients and Pareto profiles; exact priced attainment; exhaustive transversal covers; literal dirty noncommuting maps and inverse; deletion and boundary controls." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "New replicated-word coefficients and Pareto profiles; exact priced attainment; exhaustive transversal covers; literal dirty noncommuting maps and inverse; deletion and boundary controls." + } + ] +} diff --git a/research/signed-duplication-tariff/verify.py b/research/signed-duplication-tariff/verify.py new file mode 100644 index 0000000000..44e118791f --- /dev/null +++ b/research/signed-duplication-tariff/verify.py @@ -0,0 +1,313 @@ +#!/usr/bin/env python3 +"""Check the new replicated-target constructor and its transversal cover.""" + +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 +C = ((1, 1, 1), (1, 1, -1), (1, -1, 0)) +CHARS = (0, 2, 3, 4, 5, 8, 12) +MAX_GROUP = 4 +MAX_OPS = 6 * MAX_GROUP +MAX_WORD = 4 * MAX_OPS +MAX_FILE_BYTES = 2 * 1024 * 1024 + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def digest(data): + return hashlib.sha256(data).hexdigest() + + +def read_bytes(path): + with path.open("rb") as stream: + data = stream.read(MAX_FILE_BYTES + 1) + require(len(data) <= MAX_FILE_BYTES, "file capacity: " + str(path)) + return data + + +def load_anchors(): + """Use predecessor constructions as inputs, without auditing their results.""" + sources = json.loads(read_bytes(PACKAGE / "SOURCES.json")) + require(len(sources["files"]) <= 16, "source inventory capacity") + anchors = {} + for row in sources["files"]: + if row["usage"] != "input": + continue + data = read_bytes(ROOT / row["path"]) + require(digest(data) == row["sha256"], "source hash: " + row["path"]) + source = json.loads(data) + if "canonical_words" in source: + anchors[3] = source["canonical_words"] + elif "witnesses" in source: + anchors[0] = source["witnesses"] + require(set(anchors) == {0, 3}, "two predecessor anchor families") + return anchors + + +def groups_for(sizes): + require(len(sizes) == 6, "six group sizes") + require(all(type(n) is int and 1 <= n <= MAX_GROUP for n in sizes), + "group size outside evidence capacity") + groups, offset = [], 0 + for size in sizes: + groups.append(tuple(range(offset, offset + size))) + offset += size + require(offset <= MAX_OPS, "operator capacity") + return tuple(groups) + + +def premium(char): + require(char == 0 or type(char) is int and 2 <= char <= 256, + "invalid characteristic") + return 0 if char == 2 else 1 if char == 3 else 2 + + +def envelope(groups, prices, char): + require(len(prices) == sum(map(len, groups)), "price shape") + require(all(p > 0 for p in prices), "positive complete prices required") + sums = tuple(sum(prices[op] for op in group) for group in groups) + return 2 * sum(prices) + premium(char) * min(sums) + + +def construct(groups, char, chosen, anchors): + require(chosen in range(6), "chosen group") + premium(char) + if char == 2: + tokens = "B0+ B1+ B2+ A0+ A1+ B2- A2+ B1- B0- A0- A1- A2-" + base = [(t[0], int(t[1]), 1 if t[2] == "+" else -1) + for t in tokens.split()] + else: + name = ("B" if chosen < 3 else "A") + str(chosen % 3) + base = anchors[3 if char == 3 else 0][name] + word = [] + for kind, index, sign in base: + group = groups[index + (3 if kind == "A" else 0)] + word.extend((op, sign) for op in group) + require(len(word) <= MAX_WORD, "word capacity") + return tuple(word) + + +def labels(groups): + return tuple(k for k, group in enumerate(groups) for _ in group) + + +def residual(word, groups, char): + """Track formal B_j x_j and A_i B_j x_j coefficients exactly.""" + nb = sum(map(len, groups[:3])) + na = sum(map(len, groups[3:])) + require(len(word) <= MAX_WORD, "word capacity") + q, dirt, matrix = [0] * nb, [0] * na, [[0] * nb for _ in range(na)] + for op, sign in word: + require(type(op) is int and 0 <= op < nb + na and sign in (-1, 1), + "invalid query") + if op < nb: + q[op] += sign + else: + i = op - nb + dirt[i] += sign + for j in range(nb): + matrix[i][j] += sign * q[j] + lab = labels(groups) + errors = q + dirt + [matrix[i][j] - C[lab[nb + i] - 3][lab[j]] + for i in range(na) for j in range(nb)] + return tuple(x % char if char else x for x in errors) + + +def count_profile(word, n): + counts = [0] * n + for op, _ in word: + counts[op] += 1 + return tuple(counts) + + +def construction_checks(anchors): + cases = 0 + for sizes in itertools.product(range(1, 4), repeat=6): + groups = groups_for(sizes) + n = sum(sizes) + for char, chosen in itertools.product(CHARS, range(6)): + word = construct(groups, char, chosen, anchors) + require(not any(residual(word, groups, char)), "replicated action") + expected = tuple(2 + premium(char) * (op in groups[chosen]) + for op in range(n)) + require(count_profile(word, n) == expected, "attaining profile") + cases += 1 + return cases + + +def priced_checks(anchors): + rng, cases = random.Random(84017), 0 + for sizes in itertools.product((1, 2), repeat=6): + groups = groups_for(sizes) + n = sum(sizes) + pricesets = [(Fraction(1),) * n] + pricesets.extend(tuple(Fraction(rng.randrange(1, 30), rng.randrange(1, 8)) + for _ in range(n)) for _ in range(4)) + for char, prices in itertools.product(CHARS, pricesets): + chosen = min(range(6), key=lambda k: sum(prices[o] for o in groups[k])) + word = construct(groups, char, chosen, anchors) + bill = sum(prices[op] for op, _ in word) + require(bill == envelope(groups, prices, char), "priced attainment") + require(not any(residual(word, groups, char)), "priced action") + cases += 1 + return cases + + +def cover_checks(): + """Enumerate subsets directly, independently of the closed cover lemma.""" + masks, transversals, cases = 0, 0, 0 + for sizes in itertools.product((1, 2), repeat=6): + groups = groups_for(sizes) + n = sum(sizes) + edges = tuple(sum(1 << op for op in choice) + for choice in itertools.product(*groups)) + group_masks = tuple(sum(1 << op for op in g) for g in groups) + prices = tuple(Fraction((7 * op + 3) % 19 + 1, op % 4 + 1) + for op in range(n)) + best, minimal = None, set() + for mask in range(1 << n): + hit = all(mask & edge for edge in edges) + whole = any(mask & g == g for g in group_masks) + require(hit == whole, "transversal equivalence") + if hit: + cost = sum(prices[o] for o in range(n) if mask & (1 << o)) + best = cost if best is None else min(best, cost) + if all(not all((mask ^ (1 << o)) & edge for edge in edges) + for o in range(n) if mask & (1 << o)): + minimal.add(mask) + masks += 1 + require(minimal == set(group_masks), "minimal cover classification") + require(best == min(sum(prices[o] for o in g) for g in groups), + "weighted cover optimum") + transversals += len(edges) + cases += 1 + return {"shapes": cases, "subsets": masks, "transversals": transversals} + + +def mv(matrix, vector): + return [sum(a * b for a, b in zip(row, vector)) for row in matrix] + + +def execute(word, nb, maps, initial, char): + state = [list(v) for v in initial] + for op, sign in word: + src, dst = (op, len(state) - 1) if op < nb else (len(state) - 1, op) + inc = mv(maps[op], state[src]) + state[dst] = [a + sign * b for a, b in zip(state[dst], inc)] + if char: + state[dst] = [a % char for a in state[dst]] + return state + + +def dense_checks(anchors): + rng, cases = random.Random(84321), 0 + shapes = ((1,) * 6, (2,) * 6, (4, 1, 2, 3, 1, 2), (1, 4, 2, 1, 3, 4)) + for sizes in shapes: + groups = groups_for(sizes) + n, nb = sum(sizes), sum(sizes[:3]) + lab = labels(groups) + for char, chosen, _ in itertools.product(CHARS, range(6), range(3)): + maps = [[[rng.randrange(-3, 4) for _ in range(2)] for _ in range(2)] + for _ in range(n)] + maps[0], maps[nb] = [[0, 1], [0, 0]], [[0, 0], [1, 0]] + require(mv(maps[0], mv(maps[nb], [1, 0])) != + mv(maps[nb], mv(maps[0], [1, 0])), "noncommuting fixture") + initial = [[rng.randrange(-5, 6) for _ in range(2)] for _ in range(n + 1)] + if char: + initial = [[a % char for a in row] for row in initial] + expected = [list(v) for v in initial] + for i in range(nb, n): + for j in range(nb): + inc = mv(maps[i], mv(maps[j], initial[j])) + coefficient = C[lab[i] - 3][lab[j]] + expected[i] = [a + coefficient * b for a, b in zip(expected[i], inc)] + if char: + expected[i] = [a % char for a in expected[i]] + word = construct(groups, char, chosen, anchors) + actual = execute(word, nb, maps, initial, char) + require(actual == expected, "literal dense dirty action") + inverse = tuple((op, -sign) for op, sign in reversed(word)) + require(execute(inverse, nb, maps, actual, char) == initial, + "literal dirty round trip") + cases += 1 + return cases + + +def failure_checks(anchors): + groups, controls = groups_for((2, 1, 1, 1, 1, 1)), 0 + for char, chosen in itertools.product(CHARS, range(6)): + word = construct(groups, char, chosen, anchors) + for position in range(len(word)): + broken = word[:position] + word[position + 1:] + require(any(residual(broken, groups, char)), "omitted query accepted") + controls += 1 + prices = (1, 100, 10, 10, 10, 10, 10) + require(envelope(groups, prices, 0) == 322, "whole-group example") + require(2 * sum(prices) + 2 * min(prices) == 304, "incorrect single surcharge") + word = construct(groups, 0, 1, anchors) + require(sum(prices[op] for op, _ in word) == 322, "literal example bill") + edge_avoiding_cheapest = sum(1 << group[-1] for group in groups) + require(not edge_avoiding_cheapest & 1, "single surcharge misses a transversal") + controls += 1 + bad_cases = ((0, 1, 1, 1, 1, 1), (5, 1, 1, 1, 1, 1), (1,) * 5) + for sizes in bad_cases: + try: + groups_for(sizes) + except ValueError: + controls += 1 + else: + raise ValueError("invalid group shape accepted") + for prices, char in (((0,) * 7, 3), ((1,) * 6, 3), ((1,) * 7, 1)): + try: + envelope(groups, prices, char) + except ValueError: + controls += 1 + else: + raise ValueError("invalid price or characteristic accepted") + return controls + + +def receipt(counts): + paths = sorted(p for p in PACKAGE.iterdir() if p.is_file()) + require(len(paths) <= 16, "package inventory capacity") + inputs = json.loads(read_bytes(PACKAGE / "VERIFY.json"))["inputs"] + require(len(inputs) == 2, "receipt input inventory") + paths.extend(ROOT / path for path in inputs) + hashes = {str(p.relative_to(ROOT)): digest(read_bytes(p)) for p in paths} + return {"status": "PASS_SIGNED_DUPLICATION_TARIFF", "counts": counts, + "sha256": hashes} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--receipt", type=Path) + args = parser.parse_args() + if args.receipt: + require(not args.receipt.resolve().is_relative_to(ROOT), + "receipt must stay outside checkout") + anchors = load_anchors() + counts = {"construction_cases": construction_checks(anchors), + "priced_cases": priced_checks(anchors), "cover": cover_checks(), + "dense_cases": dense_checks(anchors), + "negative_controls": failure_checks(anchors)} + result = receipt(counts) + payload = json.dumps(result, sort_keys=True, indent=2) + "\n" + if args.receipt: + written = args.receipt.write_text(payload) + require(written == len(payload), "incomplete receipt write") + print("PASS_SIGNED_DUPLICATION_TARIFF", json.dumps(counts, sort_keys=True)) + print("receipt_sha256", digest(payload.encode())) + + +if __name__ == "__main__": + main()