From c5c71fd61d06e9580673fe4d2475d5f8b4c95e01 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Fri, 23 Oct 2026 13:32:28 +0100 Subject: [PATCH] feat(research): prove exact equal-nonunit fanout tariffs --- research/equal-nonunit-fanout/README.md | 225 +++++++++++++++ research/equal-nonunit-fanout/SOURCES.json | 36 +++ research/equal-nonunit-fanout/TASK.json | 79 ++++++ research/equal-nonunit-fanout/VERIFY.json | 34 +++ research/equal-nonunit-fanout/verify.py | 312 +++++++++++++++++++++ 5 files changed, 686 insertions(+) create mode 100644 research/equal-nonunit-fanout/README.md create mode 100644 research/equal-nonunit-fanout/SOURCES.json create mode 100644 research/equal-nonunit-fanout/TASK.json create mode 100644 research/equal-nonunit-fanout/VERIFY.json create mode 100644 research/equal-nonunit-fanout/verify.py diff --git a/research/equal-nonunit-fanout/README.md b/research/equal-nonunit-fanout/README.md new file mode 100644 index 0000000000..f97c05717f --- /dev/null +++ b/research/equal-nonunit-fanout/README.md @@ -0,0 +1,225 @@ +# Exact equal-nonunit dirty-fanout tariffs + +Scoped written proof with exact finite corroboration; no new κ. +For demand `(2,2,2)` over `Z/4`, the exact destination-priced dirty-fanout +frontier consists of seven count vectors. More generally, every common +nonzero demand over a commutative unital ring has the tariff below, at every +row count and every positive stationary coefficient-independent price. + +This settles the first all-nonunit example in lee-phys's +[#5163](https://github.com/CrocSwap/integer-mult-bounds/pull/5163), whose theorem +requires a unit demand. Krzysztof Wojt's +[#5045](https://github.com/CrocSwap/integer-mult-bounds/pull/5045) already settles +two rows. The new scope is equal nonzero demands on arbitrarily many rows, +including three or more nonunit demands. The return argument and echo +construction retain their predecessor credit. + +## Contract and result + +Let R be a commutative unital ring with `1 != 0`, let `lambda != 0` in R, +and let `q,w >= 1`. There are q arbitrary independent dirty rows +`a_i in R^w` and a preserved disjoint source `p in R^w`. Require + + A_i = a_i + lambda p, for every 0 <= i < q. + +The allowed finite straight-line gates are + + P_i(beta): A_i <- A_i + beta p, price mu_i > 0; + E_ij(alpha): A_i <- A_i + alpha A_j, price c_i > 0, i != j. + +All nonzero coefficients and ordered row pairs are available. Prices are +stationary, coefficient-independent complete abstract prices. An ADD's price +depends only on its destination. Zero-coefficient gates can be deleted. +Every original dirt column must return. There are no extra rows, cleared +registers, observations, adaptive choices or free basis changes. + +For a nonempty subset S of the q rows define + + V(S) = (P_i = 1 if i in S else 0; + K_i = 0 if i in S else 2), + +where K_i counts all incoming ADDs at i. Then + + OPT = min over nonempty S [sum_(i in S) mu_i + 2 sum_(i not in S) c_i]. + +Exactly the `2^q-1` vectors V(S) form the Pareto frontier of aggregate source +and destination counts. Each vector is uniquely cheapest at some strictly +positive price vector. Equivalently, with `a_i=min(mu_i,2c_i)`, + + OPT = sum_i a_i + min_i (mu_i-a_i). + +This last expression takes O(q) arithmetic/comparison operations after the +prices are supplied. It does not price the physical implementation of a gate. +The common demand can be a nonunit or a zero divisor. No division by it is used. +For the excluded zero-demand case the empty word has optimum zero. + +For `(2,2,2)` over `Z/4`, the complete seven-term answer is + +| Source support S | Exact price | Counts `(P0,P1,P2,K0,K1,K2)` | +|---|---|---| +| `{0}` | `mu0+2c1+2c2` | `(1,0,0,0,2,2)` | +| `{1}` | `mu1+2c0+2c2` | `(0,1,0,2,0,2)` | +| `{2}` | `mu2+2c0+2c1` | `(0,0,1,2,2,0)` | +| `{0,1}` | `mu0+mu1+2c2` | `(1,1,0,0,0,2)` | +| `{0,2}` | `mu0+mu2+2c1` | `(1,0,1,0,2,0)` | +| `{1,2}` | `mu1+mu2+2c0` | `(0,1,1,2,0,0)` | +| `{0,1,2}` | `mu0+mu1+mu2` | `(1,1,1,0,0,0)` | + +At `mu=(1,9,9)` and `c=(1,1,1)`, the exact optimum is five, attained by + + E_10(-1), E_20(-1), P_0(2), E_20(1), E_10(1). + +## Proof over arbitrary ring size and row count + +Write M for the q-by-q matrix of original dirt coefficients. It starts and +ends at I. Every prefix is invertible, since P leaves M unchanged and every +E has its negated-coefficient inverse. Testing free input coordinates gives +these matrix equalities even when R has zero divisors. + +A row cannot receive exactly one nonzero ADD. If row i had its only incoming +ADD `E_ij(alpha)` at prefix M, its dirt row would change from e_i to +`e_i+alpha m_j`. No later operation into i could restore it. Thus restoration +would require `alpha m_j=0`. Multiplying on the right by the inverse prefix +matrix yields `alpha e_j=0`, so alpha=0, a contradiction. This is the credited +incoming-row return lemma of #5163 and its #3063/#4916 lineage. It counts total +arrivals, without asserting that each individual directed edge occurs twice. + +Let S be the rows receiving at least one source insertion in an arbitrary +valid word. S is nonempty, since without insertions the source column stays +zero, whereas its required endpoint is the nonzero common value lambda. +For i in S, the word pays at least mu_i. For i outside S, its source +coefficient starts at zero and must become lambda, so it receives an ADD. +The return lemma forces at least two arrivals, costing at least 2c_i. +These disjoint row bills show that the word's count vector dominates V(S) +and its price is at least the displayed minimum. Repeated insertions, +feedback, cancellation and arbitrary interleavings are covered. + +Conversely, choose any nonempty S and any r in S. For every i outside S, +prepare `E_ir(-1)`. Execute `P_r(lambda)`. Undo the preparations in reverse +order with `E_ir(1)`, then execute `P_i(lambda)` on every other i in S. +An echoed row becomes + + (a_i-a_r) + (a_r+lambda p) = a_i+lambda p. + +The chosen row and directly inserted rows also end correctly. Every dirt +column returns, and the count vector is exactly V(S). This proves attainment. +Its literal inverse reverses the gate order and negates every coefficient, +with the same abstract prices. + +Different V(S) are pairwise incomparable. Every realizable vector dominates +one of them, and every one is realizable, so they are exactly the Pareto +frontier. To expose a particular S uniquely, put c_i=1 for every row, +mu_i=1 on S and mu_i=9 elsewhere. Including a row of S reduces its local cost +from two to one; including any other row increases it from two to nine. +The unique minimizing source support is therefore S. + +Finally, for a chosen inserted root r, every other row may independently +choose its cheaper direct or echo bill a_i. This gives +`mu_r + sum_(i != r) a_i`. Minimizing over r proves the O(q) formula. + +## Exact finite evidence and reproduction + +The standalone standard-library verifier imports no predecessor code. +It checks 23,433 attaining words and their literal inverses, accounting for +298,716 formal-column executions, over `Z/n` for n=2 through 12 and the +non-chain local ring `F2[e,h]/(e^2,eh,h^2)`. Rows range from one through six; +every nonzero common demand, nonempty insertion support and allowed chosen +root is enumerated. The ring checks examine 6,595 element triples. + +For the seven `Z/4` witnesses it also enumerates all 256 scalar assignments +to the three dirt rows and the source, totaling 1,792 assignments with both +forward and inverse checks. There are 480 heterogeneous-price comparisons +and 120 separately exposed frontier vectors across the six row counts. +Seven rejecting controls and positive source-insertion/inverse controls pass. + +An independently implemented flattened-matrix interpreter certifies seven +three-row `Z/4` minima by exhaustive forward/reverse balls. For each nonempty +S use mu_i=1 on S, mu_i=9 otherwise, and c_i=1 everywhere. The attaining +cost is `6-|S|`, between three and five. Any cheaper word excludes price-nine +gates, so every remaining gate costs one. The two balls of total radius +`5-|S|` are disjoint. They contain, by source-support mask, respectively +`(299,299), (299,299), (25,381), (299,299), (25,381), (25,381), (28,28)` states. +All nonzero modular coefficients and all six ADD directions are available. +These are complete lower-cost searches, rather than an arbitrary depth cap; +they are not an enumeration of the entire affine state graph. + +From the repository root, run + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/equal-nonunit-fanout +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/equal-nonunit-fanout/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/equal-nonunit-fanout/verify.py +``` + +Expected output includes `PASS_EQUAL_NONUNIT_FANOUT`. Each run prints a generated +JSON receipt with the evidence counts and SHA256 hashes of all five package +files. No receipt is handwritten. The universal claim rests on the written +proof; finite checks corroborate the stated finite domains. Independent human +and formal proof-kernel review are unclaimed. + +## Scope, sources and overlap + +Scientific base is canonical main +`ec2780e8aeb1c88acaf5e9e470ef8c68e7fbbb6c`, priority revision 7. The historical +`bit-helper-contract` card is marked changed in TASK.json. Its native H2/K +question is replaced by #5163's explicit all-nonunit tariff handoff; the card's +original example is not replayed, because that would not answer this task. +The handoff's first working example is the `(2,2,2)` case above. + +The [advance CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19145537) +records the question before substantial work. Entry coverage included live +open PRs and this account's recent submissions, recent handoffs and active +Discussions, distinctive main README and merged-PR searches, and cached +snapshots of 314 open PRs and 4,389 Discussion records. The local cached scan +covered 151 of 6,996 note paths before widening; arbitrary diffs and unpublished +work remain unsearched. A lack of matches is not a novelty certificate. +Exact historical predecessor documents are provenance-pinned in SOURCES.json; +none is an executable input or a rechecked deliverable. + +No unequal-demand classification, general directed-edge tariff, extra dirty +workspace theorem, physical caller, complete supplier invoice, native/tape or +precision admission, selected-frontier change or multiplication theorem is +claimed. The selected κ remains 0.00302015. Lean, Docker and selected supplier +cold replay are outside this algebraic contribution and were not run. + +## Open next questions + +1. Determine the destination-priced tariff for `(e,h,e+h)` in the eight-element + square-zero ring. This is #5163's second all-nonunit example, whose demands + are not common multiples of one unit-normalized coefficient. Start with + source-support lower bounds and the generated demand ideal. The missing + multi-insertion sharing argument blocks applying this theorem. +2. Determine the all-positive directed-edge tariff for `(2,2,2)` over `Z/4`. + Destination totals lose which source supplied an arrival. Start with a price + matrix whose cheap edges form a directed cycle and an explicit restoring + word; a matching directed-cut lower bound is still missing. +3. Supply one physical caller's complete stationary tariffs. Source access, + coefficient application, routing, frame changes, precision and restoration + must all be paid before this abstract optimum implies any supplier gain. + +## Engineering constraints + +The verifier has no recursion, external imports, background processes, solver, +network access or dynamic code evaluation. Every loop has a finite domain: +12 ring fixtures of size at most 12, at most six rows, 63 source supports, +six chosen roots, at most eleven common-demand values and 80 price fixtures +per row count. Words have at most eleven gates and formal rows seven entries. +Each oracle ball has radius at most two and at most 27 gates, so at most +757 candidates are stored per ball. Python exact objects, sets, dataclasses +and JSON allocate dynamically, a managed-runtime deviation from Power-of-Ten +rule 3. Live collections and integer sizes are bounded by these fixed fixtures; +standard-library allocation internals are not audited. Functions are kept +below 60 physical lines; warning-strict normal and optimized replay is +registered. Internal checks use explicit exceptions and remain active under -O. + +## Credit + +This contribution was produced by Nick Petalas. Apache-2.0. Credit lee-phys +#5163 for the explicit `(2,2,2)` handoff and incoming-row formulation; Krzysztof +Wojt #5045 for source-count classification and nonunit two-row constructions; +Nick Petalas #4916 for the ring-valued free-module contract; Ross Richardson +#3063/#3121 for destination/edge tariffs and dirt restoration; Cinna Davis +#1944/#1968, Anthony #774, Oscar Fennell #759, Tekalign #3130 and the retained +common-source fanout lineage. The new claim is the common-nonzero-demand +arbitrary-row destination-price theorem and its exact frontier, rather than +priority for the credited return lemma or echo construction. diff --git a/research/equal-nonunit-fanout/SOURCES.json b/research/equal-nonunit-fanout/SOURCES.json new file mode 100644 index 0000000000..25e7853f18 --- /dev/null +++ b/research/equal-nonunit-fanout/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "ec2780e8aeb1c88acaf5e9e470ef8c68e7fbbb6c", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/local-ring-row-fanout/README.md", + "usage": "provenance", + "git_blob": "a65ecdb615300c6b4357eadadb52b46cfbc363ba", + "sha256": "4f167d526d889089717b9ba273bc7d048efe4ec1e02cdd91456543e7fc9703fb" + }, + { + "path": "research/two-row-nonunit-fanout/PROOF.md", + "usage": "provenance", + "git_blob": "1bd3b47624db83c45ca08fb498f2a84d814306c1", + "sha256": "d177967c73bd5e755c5f70964d5542420e23e36cad81c57452a222e50e356f77" + }, + { + "path": "research/unit-ring-dirty-fanout/README.md", + "usage": "provenance", + "git_blob": "70ce8559a0d35a5e2e9c47f0885c8042b22bb0ef", + "sha256": "70764fb3def04ba1b0a51e95cb023358fdaed5100d2440feecbaab0e85a9a5fe" + } + ] +} diff --git a/research/equal-nonunit-fanout/TASK.json b/research/equal-nonunit-fanout/TASK.json new file mode 100644 index 0000000000..3d13e15453 --- /dev/null +++ b/research/equal-nonunit-fanout/TASK.json @@ -0,0 +1,79 @@ +{ + "schema_version": 1, + "task_id": "bit-helper-contract", + "priority_revision": 7, + "base_commit": "ec2780e8aeb1c88acaf5e9e470ef8c68e7fbbb6c", + "original_card": { + "id": "bit-helper-contract", + "question": "Can one precisely specified helper-mixing word satisfy a replacement for the inherited H2/K interface?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/r439-bsection-stars-seed01/README.md", + "research/r439-copy-path-sharing-barrier/README.md" + ], + "methods": [ + "Derive a replacement interface lemma and price its implementation.", + "Seek an exact dirty-input or chronological-cut counterexample to the proposed replacement." + ], + "acceptance_gate": "A full boundary contract and paid profile; unchanged scalar counts alone are insufficient. 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/r439-bsection-stars-seed01/verify.py" + ], + "expected": "PASS_R439_BSECTION_STARS", + "inspect": "Compare the two false H2/K flags with the unchanged paid profile in its README.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Write one replacement H2/K implication for a single helper-star operation, then try to falsify it on dirty inputs.", + "bottleneck_link": "A legitimate replacement could admit a cheaper bit circuit; scalar savings alone do not alter the selected moment.", + "allowed_variations": [ + "Choose one helper-star or quartet instance; narrow to one boundary implication." + ], + "scope_change_triggers": [ + "Changing only source count or scalar addition count without an interface argument." + ], + "overlap_terms": [ + "H2_D_frame0_targets_from_helpers", + "K_equals_D", + "helper-star" + ] + }, + "scope_status": "changed", + "actual_scope": "Exact all-positive destination-priced tariff and Pareto frontier for a common nonzero demand over commutative unital rings, settling the three-row Z/4 demand (2,2,2).", + "scope_change_reason": "Take lee-phys #5163's explicit all-nonunit first-example handoff. This is an algebraic side result, replacing the historical card's native H2/K premise; its original replay would not answer this question.", + "bottleneck_link": "Exact abstract dirty-restoration prices can guide a later physical caller, but no complete supplier or selected moment is inferred.", + "budget_minutes": 60, + "stop_rule": "Stop at the first all-word lower bound with matching restoring constructions and exact finite corroboration; leave unequal demands and independent edge prices open.", + "outcome": "completed", + "evidence": "README proof; verify.py checks 23433 words, 298716 formal columns, 1792 scalar assignments, seven complete lower-cost three-row searches, 480 price comparisons, 120 exposed vectors and seven rejection controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "What is the destination-priced optimum for (e,h,e+h) over F2[e,h]/(e^2,eh,h^2)?", + "why_it_matters": "This is the next all-nonunit example in #5163 and has no common generating coefficient.", + "first_step": "Classify source-support lower bounds and the generated demand ideal before searching one price vector.", + "blocked_by": "A matching multi-insertion sharing lower bound and construction." + }, + { + "question": "What is the independently directed-edge-priced optimum for (2,2,2) over Z/4?", + "why_it_matters": "Physical directed costs need not depend only on the destination.", + "first_step": "Choose a cheap directed cycle, construct a restoring word and compare directed cuts.", + "blocked_by": "Destination arrival totals discard source information." + }, + { + "question": "Can one physical caller supply complete coefficient-independent stationary tariffs?", + "why_it_matters": "An abstract optimum alone does not establish a supplier improvement.", + "first_step": "Record source access, coefficient application, routing, frames, precision and restoration at one caller.", + "blocked_by": "Missing complete physical bill." + } + ], + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19145537", + "environment": { + "python": "CPython 3.12.15", + "platform": "macOS 27.0.1 arm64", + "dependencies": "standard library only" + } +} diff --git a/research/equal-nonunit-fanout/VERIFY.json b/research/equal-nonunit-fanout/VERIFY.json new file mode 100644 index 0000000000..81f29288b0 --- /dev/null +++ b/research/equal-nonunit-fanout/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Equal-nonzero-demand construction, inverse, full dirt columns, exact seven lower-cost searches, heterogeneous price fixtures, ring axioms and rejecting controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Equal-nonzero-demand construction, inverse, full dirt columns, exact seven lower-cost searches, heterogeneous price fixtures, ring axioms and rejecting controls." + } + ] +} diff --git a/research/equal-nonunit-fanout/verify.py b/research/equal-nonunit-fanout/verify.py new file mode 100644 index 0000000000..988344cd47 --- /dev/null +++ b/research/equal-nonunit-fanout/verify.py @@ -0,0 +1,312 @@ +#!/usr/bin/env python3 +"""Exact corroboration for the equal-demand tariff; standard library only.""" + +import hashlib +import itertools +import json +from dataclasses import dataclass +from pathlib import Path + + +class VerificationError(Exception): + """A mathematical or input-contract check failed.""" + + +def require(condition: bool, message: str) -> None: + if not condition: + raise VerificationError(message) + + +@dataclass(frozen=True) +class Ring: + size: int + square_zero: bool = False + + def add(self, x: int, y: int) -> int: + return x ^ y if self.square_zero else (x + y) % self.size + + def neg(self, x: int) -> int: + return x if self.square_zero else (-x) % self.size + + def mul(self, x: int, y: int) -> int: + if not self.square_zero: + return x * y % self.size + return ((x & 1) * (y & 1)) ^ ((x & 1) * (y & 6)) ^ ((y & 1) * (x & 6)) + + +def check_ring(ring: Ring) -> int: + require(2 <= ring.size <= 12, "ring size outside finite check domain") + require(not ring.square_zero or ring.size == 8, "invalid square-zero encoding") + triples = 0 + for x, y, z in itertools.product(range(ring.size), repeat=3): + require( + ring.add(ring.add(x, y), z) == ring.add(x, ring.add(y, z)), "additivity" + ) + require( + ring.mul(ring.mul(x, y), z) == ring.mul(x, ring.mul(y, z)), "associativity" + ) + require( + ring.mul(x, ring.add(y, z)) == ring.add(ring.mul(x, y), ring.mul(x, z)), + "distributivity", + ) + require(ring.mul(x, y) == ring.mul(y, x), "commutativity") + triples += 1 + for x in range(ring.size): + require(ring.add(x, ring.neg(x)) == 0, "additive inverse") + require(ring.mul(x, 1) == x and ring.mul(1, x) == x, "multiplicative identity") + return triples + + +def word_for(ring: Ring, q: int, demand: int, support: int, root: int) -> tuple: + require(1 <= q <= 6 and 0 < demand < ring.size, "invalid equal-demand domain") + require(0 < support < 1 << q and 0 <= root < q, "invalid source support") + require(bool(support & (1 << root)), "root is not in insertion support") + echoed = tuple(i for i in range(q) if not support & (1 << i)) + before = tuple(("E", i, root, ring.neg(1)) for i in echoed) + after = tuple(("E", i, root, 1) for i in reversed(echoed)) + direct = tuple( + ("P", i, -1, demand) for i in range(q) if i != root and support & (1 << i) + ) + return before + (("P", root, -1, demand),) + after + direct + + +def execute(ring: Ring, word: tuple, rows: tuple, source: tuple) -> tuple: + data = [list(row) for row in rows] + for kind, dest, origin, coefficient in word: + rhs = source if kind == "P" else data[origin] + data[dest] = [ + ring.add(x, ring.mul(coefficient, y)) + for x, y in zip(data[dest], rhs, strict=True) + ] + return tuple(tuple(row) for row in data) + + +def inverse(ring: Ring, word: tuple) -> tuple: + return tuple( + (kind, dest, origin, ring.neg(coefficient)) + for kind, dest, origin, coefficient in reversed(word) + ) + + +def counts(word: tuple, q: int) -> tuple: + source = [0] * q + arrivals = [0] * q + for kind, dest, _, _ in word: + if kind == "P": + source[dest] += 1 + else: + arrivals[dest] += 1 + return tuple(source + arrivals) + + +def endpoint(ring: Ring, word: tuple, q: int, demand: int) -> None: + rows = tuple(tuple(int(i == j) for j in range(q + 1)) for i in range(q)) + source = (0,) * q + (1,) + expected = tuple(row[:-1] + (demand,) for row in rows) + actual = execute(ring, word, rows, source) + require(actual == expected, "wrong full formal endpoint") + require( + execute(ring, inverse(ring, word), actual, source) == rows, "inverse failed" + ) + + +def support_vector(q: int, support: int) -> tuple: + return tuple(int(bool(support & (1 << i))) for i in range(q)) + tuple( + 0 if support & (1 << i) else 2 for i in range(q) + ) + + +def dot(left: tuple, right: tuple) -> int: + return sum(x * y for x, y in zip(left, right, strict=True)) + + +def closed_price(mu: tuple, c: tuple) -> int: + require(len(mu) == len(c) and 1 <= len(mu) <= 6, "invalid price shape") + require( + all(type(x) is int and x > 0 for x in mu + c), + "prices must be positive integers in the finite checker", + ) + local = tuple(min(x, 2 * y) for x, y in zip(mu, c, strict=True)) + return sum(local) + min(x - y for x, y in zip(mu, local, strict=True)) + + +def construction_checks() -> dict: + rings = tuple(Ring(n) for n in range(2, 13)) + (Ring(8, True),) + total = { + "ring_triples": 0, + "words": 0, + "formal_columns": 0, + "literal_assignments": 0, + } + for ring in rings: + total["ring_triples"] += check_ring(ring) + for q in range(1, 7): + for demand in range(1, ring.size): + for support in range(1, 1 << q): + for root in range(q): + if not support & (1 << root): + continue + word = word_for(ring, q, demand, support, root) + endpoint(ring, word, q, demand) + require( + counts(word, q) == support_vector(q, support), + "wrong aggregate count", + ) + total["words"] += 1 + total["formal_columns"] += 2 * (q + 1) + ring = Ring(4) + for support in range(1, 8): + root = next(i for i in range(3) if support & (1 << i)) + word = word_for(ring, 3, 2, support, root) + for dirt in itertools.product(range(4), repeat=4): + rows = tuple((x,) for x in dirt[:3]) + source = (dirt[3],) + expected = tuple(((x + 2 * dirt[3]) % 4,) for x in dirt[:3]) + actual = execute(ring, word, rows, source) + require(actual == expected, "literal endpoint failed") + require( + execute(ring, inverse(ring, word), actual, source) == rows, + "literal inverse failed", + ) + total["literal_assignments"] += 1 + return total + + +def price_checks() -> dict: + comparisons = 0 + exposed = 0 + for q in range(1, 7): + vectors = tuple(support_vector(q, s) for s in range(1, 1 << q)) + for support in range(1, 1 << q): + mu = tuple(1 if support & (1 << i) else 9 for i in range(q)) + c = (1,) * q + values = tuple(dot(v, mu + c) for v in vectors) + require( + values.count(min(values)) == 1, + "frontier vector is not uniquely exposed", + ) + require(values[support - 1] == min(values), "wrong exposed support") + require( + closed_price(mu, c) == min(values), + "closed formula disagrees with support minimum", + ) + exposed += 1 + for seed in range(80): + mu = tuple(1 + (seed * (2 * i + 1) + i * i) % 17 for i in range(q)) + c = tuple(1 + (seed * (i + 3) + 7 * i) % 13 for i in range(q)) + require( + closed_price(mu, c) == min(dot(v, mu + c) for v in vectors), + "heterogeneous tariff mismatch", + ) + comparisons += 1 + return {"price_comparisons": comparisons, "exposed_vectors": exposed} + + +def oracle_step(state: tuple, gate: tuple) -> tuple: + # Independent Z/4 interpreter on a flattened 3-by-4 affine matrix. + dest, origin, coefficient = gate + result = list(state) + for column in range(4): + value = int(column == 3) if origin == -1 else state[4 * origin + column] + result[4 * dest + column] = (state[4 * dest + column] + coefficient * value) % 4 + return tuple(result) + + +def ball(start: tuple, gates: tuple, radius: int) -> set: + require(0 <= radius <= 2 and len(gates) <= 27, "oracle bound exceeded") + seen = {start} + frontier = {start} + for _ in range(radius): + following = {oracle_step(state, gate) for state in frontier for gate in gates} + frontier = following - seen + seen.update(frontier) + require(len(seen) <= 1 + 27 + 27**2, "oracle state capacity exceeded") + return seen + + +def oracle_checks() -> dict: + identity = tuple(int(i == j) for i in range(3) for j in range(4)) + target = tuple((2 if j == 3 else int(i == j)) for i in range(3) for j in range(4)) + counts_by_support = [] + for support in range(1, 8): + # Only source prices are heterogeneous. All ADD prices are one. + # A putatively cheaper word costs <= 4, so price-nine gates cannot occur. + gates = tuple( + (i, j, a) + for i in range(3) + for j in range(-1, 3) + for a in range(1, 4) + if i != j and (j != -1 or support & (1 << i)) + ) + optimum = 6 - support.bit_count() + lower = optimum - 1 + left = ball(identity, gates, lower // 2) + right = ball(target, gates, lower - lower // 2) + require(not left.intersection(right), "a strictly cheaper complete word exists") + word = word_for(Ring(4), 3, 2, support, (support & -support).bit_length() - 1) + require(len(word) == optimum, "matching witness has wrong cost") + mu = tuple(1 if support & (1 << i) else 9 for i in range(3)) + require( + dot(counts(word, 3), mu + (1, 1, 1)) == optimum, + "oracle witness price mismatch", + ) + require(identity in ball(identity, gates, 0), "oracle zero-radius control") + require( + oracle_step(identity, gates[0]) in ball(identity, gates, 1), + "oracle planted-hit control", + ) + counts_by_support.append([support, len(left), len(right), optimum]) + return {"oracle_instances": counts_by_support} + + +def rejection_checks() -> int: + ring = Ring(4) + word = word_for(ring, 3, 2, 1, 0) + bad_words = (word[1:], word[:-1], inverse(ring, word)) + rejected = 0 + for candidate in bad_words[:2]: + try: + endpoint(ring, candidate, 3, 2) + except VerificationError: + rejected += 1 + else: + raise VerificationError("dirt corruption was accepted") + # Demand 2 is self-negative in Z/4, so its inverse is a positive control. + endpoint(ring, bad_words[2], 3, 2) + for mu, c in (((0,), (1,)), ((True,), (1,)), ((1, 2), (1,)), ((), ())): + try: + closed_price(mu, c) + except VerificationError: + rejected += 1 + else: + raise VerificationError("invalid price input was accepted") + try: + word_for(ring, 3, 0, 1, 0) + except VerificationError: + rejected += 1 + else: + raise VerificationError("zero demand was accepted in the nonzero theorem") + require(oracle_step((0,) * 12, (0, -1, 1)) != (0,) * 12, "source insertion control") + return rejected + + +def main() -> None: + result = construction_checks() | price_checks() | oracle_checks() + result["rejection_controls"] = rejection_checks() + package = Path(__file__).resolve().parent + result["sha256"] = { + name: hashlib.sha256((package / name).read_bytes()).hexdigest() + for name in ( + "README.md", + "TASK.json", + "SOURCES.json", + "VERIFY.json", + "verify.py", + ) + } + print(json.dumps(result, indent=2, sort_keys=True)) + print("PASS_EQUAL_NONUNIT_FANOUT") + + +if __name__ == "__main__": + main()