From 377c32061876ad04eb32da0660885035cce22ddc Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Fri, 30 Oct 2026 11:37:08 +0000 Subject: [PATCH] feat(research): prove sharp bounded-error partition threshold --- .../PROOF.md | 159 +++++++++ .../README.md | 100 ++++++ .../SOURCES.json | 36 ++ .../TASK.json | 79 +++++ .../VERIFY.json | 34 ++ .../verify.py | 334 ++++++++++++++++++ 6 files changed, 742 insertions(+) create mode 100644 research/bounded-error-partition-threshold/PROOF.md create mode 100644 research/bounded-error-partition-threshold/README.md create mode 100644 research/bounded-error-partition-threshold/SOURCES.json create mode 100644 research/bounded-error-partition-threshold/TASK.json create mode 100644 research/bounded-error-partition-threshold/VERIFY.json create mode 100644 research/bounded-error-partition-threshold/verify.py diff --git a/research/bounded-error-partition-threshold/PROOF.md b/research/bounded-error-partition-threshold/PROOF.md new file mode 100644 index 0000000000..0927c1f292 --- /dev/null +++ b/research/bounded-error-partition-threshold/PROOF.md @@ -0,0 +1,159 @@ +# Successful-input fibers preserve partition bounds above 1/q + +## Model + +Fix an alphabet A of size q>=2. A finite acyclic deterministic circuit has +W independent uniform input symbols. Each physical wire carries one symbol. +A gate applies a fixed arbitrary function to its incoming symbols and may +have several output ports. Copying uses separate physical wires. Fixed clean +constants and discarded workspace are allowed; preloaded data-dependent +advice is excluded. The topology and local functions are fixed. + +Each designated input w is demanded at one distinct designated sink rho(w). +Let S be the set of tuples on which all demands succeed, and p=|S|/q^W. +There is no correctness requirement outside S. Other independent inputs can +be fixed in the proof; include them among the demands if restoration is +required. Distinct sinks and independent designated inputs are essential. + +Vertices have rational m-by-m frames M_v. Each gate uses one common frame +on all ports. Charge every physical edge (u,v), including terminal, control +and fan-out edges, by rank_Q(M_v-M_u). Write s for their sum. Each demand +has terminal shift M_out(rho(w))-M_in(w)=I_m. No linearity or invertibility +of the scalar gates is assumed. The attaining examples are invertible. + +## 1. Successful-fiber inequality + +Choose any vertex class C. Let D be the designated inputs whose sources are +in C and required sinks are outside. Put d=|D|. Let e be the number of edges +leaving C, in fixed chronological order. Then + + p <= min(1, q^(e-d)). (1) + +Fix all inputs outside D. For a successful tuple, record its e outgoing +wire symbols. The transcript and fixed outside inputs determine every +outside vertex: simulate them in topological order, using the recorded +entry whenever a wire enters from C. Re-entry into C is allowed; no +chronological-cut hypothesis is needed. There is no extra message channel. + +Two distinct successful D tuples cannot have the same transcript. Otherwise +outside simulation gives the same distinct demanded sinks, although those +sinks must reproduce different D tuples. Thus at most q^e of the q^d D +tuples succeed for each fixed outside tuple. There are q^(W-d) outside +tuples. Counting proves (1). This is the successful-subset extension of +PR1757's zero-error outgoing-transcript argument. + +If p>1/q, then e>=d for every C. Indeed, e=d to each label class and sum: + + #{edges (u,v): ell(u)!=ell(v)} + >= #{demands w: ell(in(w))!=ell(out(rho(w)))}. (2) + +Each crossing physical edge leaves exactly one class. Each separated demand +is counted once. Re-entry and fan-out do not change this accounting. + +Suppose finitely many labelings ell_j and nonnegative weights c_j satisfy, +on every physical edge, + + sum_j c_j [ell_j(u)!=ell_j(v)] <= rank_Q(M_v-M_u). + +Multiplying (2) by c_j and summing shows that p>1/q implies + + s >= sum_w sum_j c_j + [ell_j(in(w))!=ell_j(out(rho(w)))]. (3) + +The edge inequalities are required certificates, not an assertion that all +rational rank metrics have a useful partition representation. The new +premise p>1/q replaces zero error in the credited partition implication. + +## 3. Common-flag consequence + +Assume there are one common rational offset A_0 and an invertible B over a +characteristic-zero extension K of Q such that T_v=B^-1(M_v-A_0)B is upper +triangular at every vertex. For i=1,...,m label v by (T_v)_ii. The terminal +shift I_m separates every demand in each of these m labelings. + +An upper triangular matrix has rank at least the number of its nonzero +diagonal entries: its principal submatrix on those indices has nonzero +determinant. Extending the field and conjugating preserve rational matrix +rank. Thus the m unit-weight labelings satisfy the edge inequalities in (3): + + p>1/q implies s>=Wm. (4) + +This includes nonsplit flags over K and noncommuting triangular families. +The checker uses rational triangular frames. The extension-field conclusion +rests on the written argument, not on a finite extension-field replay. + +For 0=r/m. Therefore the optimistic +normalized recursive moment is at least s/(Wm)>=1 under (4). Extra +nonnegative charges cannot create contraction. This is a scoped circuit +obstruction, not an integer-multiplication lower bound. + +## 4. Sharpness with reversible circuits and the same terminals + +For every q>=2, m>=1 and W>=2, put P=diag(1,0,...,0). Take two independent +symbols x,y and prescribe their swap. Their source frames are 0 and P. +The sink on physical wire zero demands y and has frame P+I_m. The sink on +physical wire one demands x and has frame I_m. Each demand therefore has +precisely the required identity shift. + +First use the identity circuit, with no gates. It returns (x,y), meeting +(y,x) exactly when x=y, on q of q^2 inputs. The terminal edge ranks are + + rank(P+I_m)=m, rank(I_m-P)=m-1. + +Hence p=1/q and s=2m-1. All frames are diagonal. Add W-2 untouched identity +demands with source zero and sink I_m to obtain s=Wm-1 with the same success. +This proves sharpness even with an invertible scalar map and just one rank +unit of deficit. It does not assert sharpness for each fixed topology. + +An exact swap is available with the same terminal frames. Identify the +alphabet with Z/qZ and perform + + x <- x+y; y <- x-y; x <- x-y. + +Each assignment reads the current values. The final values are (y_old,x_old) +for every q, including composite q. Each gate is invertible and has common +frame P. Each is represented as a two-input/two-output gate, retaining the +unchanged operand on an explicit output port. Entrance ranks sum to one, +internal ranks are zero, and exit ranks sum to 2m-1. Thus s=2m, or Wm with +the extra identity demands. Every physical wire is charged. + +No physical native implementation or zero-cost ordinary arithmetic is +claimed for these symbolic framed circuits. + +## 5. Independent coins and expected cost + +Condition on any fixed independent random seed. If its circuit has rank +bill strictly below the value of a valid partition certificate, (3) bounds +its success by 1/q. Average over the seed distribution. The same bound +holds. The certificate and topology may depend on the seed, and the proof +does not require finitely many seeds. For common flags the premise is +s 1/q, + E[s]=lambda Wm+(1-lambda)(Wm-1)=Wm-1+lambda < Wm. + +The exact branch costs Wm, so it violates the deficient branchwise premise. +This is a boundary counterexample, not cheaper exact computation or free +random control. Literal two-seed mixtures are checked below. Nonuniform +inputs and data-dependent coins also invalidate the uniform conditional +count and are outside the result. + +## Attribution and proof status + +Credit Jose Manuel / jmbarrancoml PR1757 for the zero-error outgoing +transcript and weighted-partition method, Navinor PR825 for common flags, +and ywz65 PR2507 for designated demands and disposable workspace. Classical +successful-subset counting retains its established status. This sharp +threshold and reversible same-terminal attainment construction were +produced by Nick Petalas. Predecessor numbers and verifiers are not replayed. +This is a written proof with bounded exact corroboration, not independent +human or formal proof-kernel review. diff --git a/research/bounded-error-partition-threshold/README.md b/research/bounded-error-partition-threshold/README.md new file mode 100644 index 0000000000..788f3e80ef --- /dev/null +++ b/research/bounded-error-partition-threshold/README.md @@ -0,0 +1,100 @@ +# A sharp bounded-error threshold for rational-frame cut certificates + +This contribution was produced by Nick Petalas. Apache-2.0. + +**Claim type: scoped proof with exact finite corroboration.** Allowing errors +does not evade a weighted partition certificate if simultaneous success is +strictly greater than `1/q`, for independent uniform inputs over an alphabet +of size `q`. Arbitrary nonlinear pointwise gates are allowed. For common-flag +rational frames, success above this threshold still requires `s >= Wm`. + +The threshold is sharp. For every `q >= 2`, `W >= 2` and `m >= 1`, an +invertible identity circuit with a prescribed swap endpoint has success +exactly `1/q` and rank mass `Wm-1`. All frames are diagonal. An exact swap +circuit costs `Wm` with the same terminal frames. + +Independent random coins preserve the obstruction when every fixed-coin +branch has the deficient budget. Expected cost alone is different: mixing +these two circuits gives success greater than `1/q` and expected cost less +than `Wm`. [PROOF.md](PROOF.md) supplies the quantifiers, successful-input +fiber argument, exact matrices and attaining gate words. + +This is an originally posed change of correctness model, motivated by Jose +Manuel / jmbarrancoml's [PR1757](https://github.com/CrocSwap/integer-mult-bounds/pull/1757). +Its zero-error results are cited, not audited or replayed. The new step is the +successful-input fiber bound, sharp threshold and distinction between +branchwise and expected budgets. Classical subset counting retains its credit. + +## Reproduce + +Use CPython 3.12 and the standard library, from the repository root: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/bounded-error-partition-threshold/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/bounded-error-partition-threshold/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/bounded-error-partition-threshold +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/bounded-error-partition-threshold --check-source-history +``` + +Any absolute CPython 3.12 path can replace this interpreter. The direct check +prints `PASS_BOUNDED_ERROR_PARTITION_THRESHOLD` in a generated JSON receipt +binding all six package files by SHA256. It writes no files and imports no +predecessor implementations. The runner prints `PASS_REGISTERED_RESEARCH_PACKAGE`. + +The new finite checks enumerate 2,002 map/demand cases and 111,744 vertex +classes across the declared binary and ternary topologies. They include +nonlinear ternary maps and count their actual successful-input fibers. They execute both attaining words, +charge every physical edge and test randomized mixtures by literal seed/input +enumeration. The 48 framed fixtures execute 1,668 input tuples. Literal random +mixtures execute another 1,668 seed/input cases. Ten invalid-contract controls +reject and five boundary controls pass. Exact counts appear in the generated +receipt. The universal result rests on the written proof, not these finite checks. + +## Limits and relation to the frontier + +This error-tolerance obstruction is a changed scope under `bit-new-register-model`, +not a new supplier, kappa or multiplication theorem. An error allowance below +`1-1/q` alone cannot open a partition-excluded mechanism. Fixed topology, +independent uniform inputs, distinct designated sinks and complete wire charging +remain essential. Input-dependent topology and uncharged data-dependent advice +are excluded. Coins are independent of inputs. The theorem concerns simultaneous +exact symbol recovery, not numerical distance or individual receiver error. + +An arbitrary rational rank metric need not admit a sufficient partition +certificate. Non-common-flag geometry is not universally excluded. Nonuniform +inputs, physical realization, native tariffs, dirty ownership, precision/tape, +stock, compiler and analytic recovery need separate work. No selected cold +replay, native replay or proof-kernel build was run. Independent human and +formal proof-kernel review are unclaimed. Selected PR6030 is unchanged. + +## Open next questions + +- For a named producer's actual nonuniform distribution, what is the maximum + mass of a successful transcript fiber? Start with that distribution and one + deficient cut. A justified distribution and its acquisition costs are missing. +- Can a proposed approximate supplier provide a useful partition certificate + and simultaneous symbol-success contract? First extract its complete graph, + endpoints and all wires. Numerical error and physical recovery remain separate. + +Structured questions and the stopping decision are in [TASK.json](TASK.json). +The work stops at this first verified threshold result. + +## Sources and verification bounds + +Base main is `2485805a6d47f36ea83ddde6327d453ac82d44dc`, priority revision eight. +[SOURCES.json](SOURCES.json) pins predecessor statements as provenance, with no +runtime scientific dependencies. Credit Navinor / PR825 for common flags, +Jose Manuel / PR1757 for outgoing transcripts and weighted partitions, and +ywz65 / PR2507 for designated demands and disposable workspace. Their retained +finite-shear and circuit lineages remain credited. The six-frame zero-error +theorem PR5944 and fixed-support Hurwitz success theorem address different +boundaries and are not targets here. + +The verifier has fixed finite domains, explicit exceptions and functions below +sixty lines. It has no recursion, subprocesses, network, generated code or input +callbacks. Warning-strict normal and optimized replay supply the available +standard-library diagnostics. Power of Ten rule three deviation: Python +allocates integers, fractions, tuples and dictionaries during verification. +Fixed domains bound live states to 125 input tuples and at most nine circuit +vertices. A fixed-allocation port is outside this bounded checker. Dimensions, +ports and tables are validated at entry. diff --git a/research/bounded-error-partition-threshold/SOURCES.json b/research/bounded-error-partition-threshold/SOURCES.json new file mode 100644 index 0000000000..f6279aacd0 --- /dev/null +++ b/research/bounded-error-partition-threshold/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "2485805a6d47f36ea83ddde6327d453ac82d44dc", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/nonlinear-frame-cut-bound/README.md", + "usage": "provenance", + "git_blob": "1fae484c0dc371afb0ec0d0c9b1f781d78dbffbb", + "sha256": "411b78a56180e835bb97e59b9845968d84ad3fb8f5658acde684e4491b3b1c3e" + }, + { + "path": "research/common-flag-frame-obstruction/README.md", + "usage": "provenance", + "git_blob": "fc38e760e0a88685b430479a2dc885590ecca327", + "sha256": "5636ffab46cf3801ac9b98ed681abbf237617f7189fa0a71aaf1883061a39cde" + }, + { + "path": "research/common-flag-disposable-workspace/PROOF.md", + "usage": "provenance", + "git_blob": "0db642e3dfb9c45180711a2ff40bed7eed316eb5", + "sha256": "5fe4e011011b59abd7e6b2004c7964655a30df000e7fb71beecb6b4435747ed5" + } + ] +} diff --git a/research/bounded-error-partition-threshold/TASK.json b/research/bounded-error-partition-threshold/TASK.json new file mode 100644 index 0000000000..80eb2f29b5 --- /dev/null +++ b/research/bounded-error-partition-threshold/TASK.json @@ -0,0 +1,79 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 8, + "base_commit": "2485805a6d47f36ea83ddde6327d453ac82d44dc", + "original_card": { + "id": "bit-new-register-model", + "question": "Can an explicitly larger or nonabelian register model escape the scoped three-register obstruction?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/bit-three-register-lower-bound/README.md", + "certificates/selected-result.json", + "research/bit-gl3-mixed-targets-length10/README.md", + "docs/research/community-efficient1000-review.md" + ], + "methods": [ + "Construct the smallest exact identity in a newly specified legal operation alphabet.", + "Derive a target-specific relaxation bound for that same explicit alphabet." + ], + "acceptance_gate": "Name the changed hypothesis, all counted roles and a uniform identity; finite column tests alone do not certify it. 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", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.", + "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse." + }, + "first_experiment": "First compare the alphabet, role count and length with the fully replayed #1974 census and #2027 mixed-root tariff. Identify a changed premise and a legal native implementation; then price one smallest completed instance before searching larger words.", + "bottleneck_link": "A small-width completed saving changes the bit primitive; a finite-address identity alone is insufficient.", + "allowed_variations": [ + "Choose a fixed larger register count or a specified nonabelian operation family." + ], + "scope_change_triggers": [ + "Remaining inside the already-excluded three-register abelian model.", + "Repeating the two-register GL3 census or a covered three-register length without changing a hypothesis; a formal group-algebra word without native conversion is a partial result." + ], + "overlap_terms": [ + "three-register", + "nonabelian", + "group algebra" + ] + }, + "scope_status": "changed", + "actual_scope": "Sharp simultaneous-success threshold for weighted rational-frame partition certificates under independent uniform finite-alphabet inputs; common-flag rank floor, reversible same-terminal attainment, and independent-coin versus expected-budget distinction.", + "scope_change_reason": "The operation model permits arbitrary pointwise nonlinear gates and errors rather than exact formal group-algebra words. This is an originally posed error-tolerance obstruction motivated by external PR1757, not a larger-group counterpart, a source audit or a selected supplier.", + "bottleneck_link": "A simultaneous error allowance below 1-1/q cannot evade a partition-excluded local primitive. This narrows approximate mechanism design while supplying no physical supplier or kappa improvement.", + "budget_minutes": 60, + "stop_rule": "Stop at the first verified threshold proof and matching reversible construction; package the scoped result without expanding to other distributions or mechanisms.", + "outcome": "completed", + "evidence": "PROOF.md and verify.py: complete approximate-map successful-fiber census, literal framed identity/swap attainments, seed/input mixture enumeration, invalid-contract and boundary controls; generated hash-bound stdout receipts.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "For a named producer with nonuniform inputs, what is the maximum mass of a successful transcript fiber?", + "why_it_matters": "A justified distribution might change the uniform error threshold.", + "first_step": "Bind one actual producer distribution and one deficient cut, then optimize its successful fibers.", + "blocked_by": "No distribution or physical acquisition cost is supplied here." + }, + { + "question": "Can an actual approximate supplier provide both a useful partition certificate and simultaneous exact symbol-success guarantee?", + "why_it_matters": "This connects the obstruction to a physical proposed mechanism.", + "first_step": "Extract its full graph, terminal demands and every charged wire.", + "blocked_by": "Numerical error, recovery, native implementation and full cost remain separate." + } + ], + "coordination": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19292052", + "claim_type": "scoped proof with exact finite corroboration", + "environment": { + "python": "3.12.15", + "implementation": "CPython", + "system": "Darwin", + "machine": "arm64", + "dependencies": "standard library only" + } +} diff --git a/research/bounded-error-partition-threshold/VERIFY.json b/research/bounded-error-partition-threshold/VERIFY.json new file mode 100644 index 0000000000..c633e145ef --- /dev/null +++ b/research/bounded-error-partition-threshold/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": 120, + "checks": "Enumerate successful fibers, exact common-flag ranks, reversible sharp witnesses, random mixtures and invalid/boundary controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Run the identical scientific checks with assertions disabled." + } + ] +} diff --git a/research/bounded-error-partition-threshold/verify.py b/research/bounded-error-partition-threshold/verify.py new file mode 100644 index 0000000000..1294852bb5 --- /dev/null +++ b/research/bounded-error-partition-threshold/verify.py @@ -0,0 +1,334 @@ +#!/usr/bin/env python3 +"""Exact successful-fiber checks for a sharp rational-frame error threshold.""" +from __future__ import annotations + +import hashlib +import itertools +import json +import sys +from fractions import Fraction +from pathlib import Path +from typing import NamedTuple + + +class Node(NamedTuple): + incoming: tuple[tuple[int, int], ...] + table: tuple[tuple[int, ...], ...] + + +def require(condition: bool, reason: str) -> None: + if not condition: + raise ValueError(reason) + + +def validate(nodes: tuple[Node, ...], q: int, width: int, + sinks: tuple[int, ...], demand: tuple[int, ...]) -> None: + require(type(q) is int and 2 <= q <= 5, 'alphabet') + require(type(width) is int and 1 <= width <= 3, 'width') + require(width <= len(nodes) <= 9, 'vertices') + require(len(sinks) == width and len(set(sinks)) == width, 'sinks') + require(sorted(demand) == list(range(width)), 'demands') + ports = [1] * width + for i, node in enumerate(nodes): + if i < width: + require(node == Node((), ()), 'source') + continue + require(0 <= len(node.incoming) <= 2, 'arity') + require(len(node.table) == q ** len(node.incoming), 'table size') + require(1 <= len(node.table[0]) <= 2, 'output width') + for row in node.table: + require(len(row) == len(node.table[0]), 'ragged table') + require(all(type(x) is int and 0 <= x < q for x in row), 'symbol') + for source, port in node.incoming: + require(type(source) is int and 0 <= source < i, 'acyclic edge') + require(type(port) is int and 0 <= port < ports[source], 'port') + ports.append(len(node.table[0])) + for sink in sinks: + require(type(sink) is int and width <= sink < len(nodes), 'sink index') + require(ports[sink] == 1, 'sink width') + require(len(nodes[sink].incoming) == 1, 'sink edge') + require(nodes[sink].table == tuple((a,) for a in range(q)), 'sink copy') + + +def evaluate(nodes: tuple[Node, ...], q: int, + inputs: tuple[int, ...]) -> tuple[tuple[int, ...], ...]: + values = [(x,) for x in inputs] + for node in nodes[len(inputs):]: + index = 0 + for source, port in node.incoming: + index = index * q + values[source][port] + values.append(node.table[index]) + return tuple(values) + + +def observations(nodes: tuple[Node, ...], q: int, width: int, + sinks: tuple[int, ...], demand: tuple[int, ...]): + validate(nodes, q, width, sinks, demand) + cases = [] + for inputs in itertools.product(range(q), repeat=width): + values = evaluate(nodes, q, inputs) + success = all(values[sink][0] == inputs[demand[j]] + for j, sink in enumerate(sinks)) + cases.append((inputs, values, success)) + return tuple(cases) + + +def check_cuts(nodes: tuple[Node, ...], q: int, width: int, + sinks: tuple[int, ...], demand: tuple[int, ...]): + cases = observations(nodes, q, width, sinks, demand) + edges = tuple((u, port, v) for v, node in enumerate(nodes) + for u, port in node.incoming) + success = sum(ok for _, _, ok in cases) + counts = {'maps': 1, 'inputs': len(cases), 'cuts': 0, 'fibers': 0, + 'deficient_cuts': 0, 'tight_deficient_cuts': 0} + for mask in range(1 << len(nodes)): + inside = tuple(bool(mask & (1 << i)) for i in range(len(nodes))) + missing = tuple(demand[j] for j, sink in enumerate(sinks) + if inside[demand[j]] and not inside[sink]) + leaving = tuple((u, port) for u, port, v in edges + if inside[u] and not inside[v]) + d, e = len(missing), len(leaving) + counts['cuts'] += 1 + require(success * q ** d <= len(cases) * q ** e, 'fiber bound') + if d > e: + counts['deficient_cuts'] += 1 + counts['tight_deficient_cuts'] += success * q ** d == len(cases) * q ** e + require(success * q <= len(cases), 'strict threshold') + if not missing: + continue + outside = tuple(i for i in range(width) if i not in missing) + fibers = {} + for inputs, values, ok in cases: + if not ok: + continue + key = (tuple(inputs[i] for i in outside), + tuple(values[u][port] for u, port in leaving)) + data = tuple(inputs[i] for i in missing) + require(key not in fibers or fibers[key] == data, 'fiber collision') + fibers[key] = data + counts['fibers'] += 1 + return counts + + +def add_counts(total: dict[str, int], update: dict[str, int]) -> None: + for key, value in update.items(): + total[key] = total.get(key, 0) + value + + +def sink(source: int, port: int, q: int) -> Node: + return Node(((source, port),), tuple((x,) for x in range(q))) + + +def parallel_maps(q: int, left: tuple[int, ...], right: tuple[int, ...]): + return (Node((), ()), Node((), ()), + Node(((0, 0),), tuple((x,) for x in left)), + Node(((1, 0),), tuple((x,) for x in right)), + sink(2, 0, q), sink(3, 0, q)) + + +def map_census() -> dict[str, int]: + total: dict[str, int] = {} + for q in (2, 3): + functions = tuple(itertools.product(range(q), repeat=q)) + for left, right in itertools.product(functions, repeat=2): + nodes = parallel_maps(q, left, right) + for demand in ((0, 1), (1, 0)): + add_counts(total, check_cuts(nodes, q, 2, (4, 5), demand)) + for left, right in itertools.product(range(16), repeat=2): + table = tuple(((left >> i) & 1, (right >> i) & 1) for i in range(4)) + nodes = (Node((), ()), Node((), ()), Node(((0, 0), (1, 0)), table), + sink(2, 0, 2), sink(2, 1, 2)) + for demand in ((0, 1), (1, 0)): + add_counts(total, check_cuts(nodes, 2, 2, (3, 4), demand)) + require(total['deficient_cuts'] > 0, 'deficient coverage') + require(total['tight_deficient_cuts'] > 0, 'sharp fiber coverage') + return total + + +def diagonal(entries: tuple[int, ...]): + return tuple(tuple(Fraction(x if i == j else 0) for j in range(len(entries))) + for i, x in enumerate(entries)) + + +def difference(left, right): + return tuple(tuple(a - b for a, b in zip(x, y)) for x, y in zip(left, right)) + + +def matrix_rank(matrix) -> int: + rows = [list(row) for row in matrix] + rank = 0 + for column in range(len(rows)): + pivot = next((i for i in range(rank, len(rows)) if rows[i][column]), None) + if pivot is None: + continue + rows[rank], rows[pivot] = rows[pivot], rows[rank] + scale = rows[rank][column] + rows[rank] = [x / scale for x in rows[rank]] + for i in range(len(rows)): + if i != rank: + multiple = rows[i][column] + rows[i] = [a - multiple * b for a, b in zip(rows[i], rows[rank])] + rank += 1 + return rank + + +def framed_bill(nodes, frames, width: int, sinks, demand) -> int: + require(len(frames) == len(nodes), 'frame count') + m = len(frames[0]) + require(1 <= m <= 3, 'address dimension') + identity = diagonal((1,) * m) + for frame in frames: + require(len(frame) == m and all(len(row) == m for row in frame), 'matrix shape') + require(all(frame[i][j] == 0 for i in range(m) for j in range(i)), 'common flag') + for j, target in enumerate(sinks): + require(difference(frames[target], frames[demand[j]]) == identity, 'terminal shift') + bill = 0 + diagonal_cuts = [0] * m + for v, node in enumerate(nodes): + for u, _ in node.incoming: + delta = difference(frames[v], frames[u]) + cost = matrix_rank(delta) + crossed = tuple(delta[i][i] != 0 for i in range(m)) + require(sum(crossed) <= cost, 'edge certificate') + for i in range(m): + diagonal_cuts[i] += crossed[i] + bill += cost + require(sum(diagonal_cuts) <= bill, 'weighted certificate') + return bill + + +def swap_fixture(q: int, width: int, m: int, exact: bool): + zero = diagonal((0,) * m) + projection = diagonal((1,) + (0,) * (m - 1)) + identity = diagonal((1,) * m) + shifted = diagonal((2,) + (1,) * (m - 1)) + nodes = [Node((), ()) for _ in range(width)] + frames = [zero, projection] + [zero] * (width - 2) + last = ((0, 0), (1, 0)) + if exact: + tables = (tuple(((a + b) % q, b) for a, b in itertools.product(range(q), repeat=2)), + tuple((a, (a - b) % q) for a, b in itertools.product(range(q), repeat=2)), + tuple(((a - b) % q, b) for a, b in itertools.product(range(q), repeat=2))) + for table in tables: + require(len(set(table)) == q * q, 'reversible gate') + nodes.append(Node(last, table)) + frames.append(projection) + last = ((len(nodes) - 1, 0), (len(nodes) - 1, 1)) + sinks = [] + for i in range(width): + source, port = last[i] if i < 2 else (i, 0) + sinks.append(len(nodes)) + nodes.append(sink(source, port, q)) + frames.append(shifted if i == 0 else identity) + demand = (1, 0) + tuple(range(2, width)) + return tuple(nodes), tuple(frames), tuple(sinks), demand + + +def attainment_census() -> dict[str, int]: + counts = {'framed_fixtures': 0, 'attainment_inputs': 0, 'random_inputs': 0} + for q, width, m in itertools.product(range(2, 6), (2, 3), range(1, 4)): + for exact in (False, True): + nodes, frames, sinks, demand = swap_fixture(q, width, m, exact) + cases = observations(nodes, q, width, sinks, demand) + correct = sum(ok for _, _, ok in cases) + require(correct == q ** (width - (not exact)), 'attaining success') + bill = framed_bill(nodes, frames, width, sinks, demand) + require(bill == width * m - (not exact), 'attaining rank') + if correct * q > len(cases): + require(bill >= width * m, 'flag threshold') + counts['framed_fixtures'] += 1 + counts['attainment_inputs'] += len(cases) + if m == 1: + add_counts(counts, check_cuts(nodes, q, width, sinks, demand)) + bad = swap_fixture(q, width, m, False) + good = swap_fixture(q, width, m, True) + successes = 0 + for chosen in (bad, good): + successes += sum(ok for _, _, ok in observations(chosen[0], q, width, chosen[2], chosen[3])) + total = 2 * q ** width + require(successes * q > total, 'expected-budget success') + bills = tuple(framed_bill(x[0], x[1], width, x[2], x[3]) for x in (bad, good)) + require(Fraction(sum(bills), 2) < width * m, 'expected-budget cost') + counts['random_inputs'] += total + return counts + + +def rejecting_controls() -> int: + nodes, frames, sinks, demand = swap_fixture(2, 2, 2, False) + changes = ( + (nodes, 1, 2, sinks, demand, 'alphabet'), + (nodes, 2, 0, sinks, demand, 'width'), + (nodes, 2, 2, (sinks[0], sinks[0]), demand, 'sinks'), + (nodes, 2, 2, sinks, (0, 0), 'demands'), + (nodes[:2] + (Node(((3, 0),), ((0,), (1,))),) + nodes[3:], + 2, 2, sinks, demand, 'acyclic edge'), + (nodes[:2] + (Node(((0, 2),), ((0,), (1,))),) + nodes[3:], + 2, 2, sinks, demand, 'port'), + (nodes[:2] + (Node(((0, 0),), ((0,),)),) + nodes[3:], + 2, 2, sinks, demand, 'table size'), + (nodes[:2] + (Node(((0, 0),), ((0,), (2,))),) + nodes[3:], + 2, 2, sinks, demand, 'symbol'), + ) + for changed, q, width, out, target, reason in changes: + try: + validate(changed, q, width, out, target) + except ValueError as error: + require(str(error) == reason, 'wrong control rejection') + else: + raise ValueError('control accepted') + for reason in ('common flag', 'terminal shift'): + changed = list(frames) + if reason == 'common flag': + changed[0] = ((Fraction(0), Fraction(0)), (Fraction(1), Fraction(0))) + else: + changed[sinks[0]] = diagonal((1, 1)) + try: + framed_bill(nodes, tuple(changed), 2, sinks, demand) + except ValueError as error: + require(str(error) == reason, 'wrong frame rejection') + else: + raise ValueError('frame control accepted') + return len(changes) + 2 + + +def boundary_controls() -> tuple[str, ...]: + nodes, frames, sinks, demand = swap_fixture(2, 2, 2, False) + cases = observations(nodes, 2, 2, sinks, demand) + bill = framed_bill(nodes, frames, 2, sinks, demand) + correct = sum(ok for _, _, ok in cases) + require(correct * 2 == len(cases) and bill < 4, 'nonstrict threshold trap') + weighted = sum((3 if a == 0 else 1) * (3 if b == 0 else 1) + for (a, b), _, ok in cases if ok) + require(weighted * 2 > 16 and bill < 4, 'biased uniformity boundary') + diagonal_cases = tuple(ok for (a, b), _, ok in cases if a == b) + require(all(diagonal_cases) and len(diagonal_cases) == 2, 'correlation boundary') + nonflag = ((Fraction(1), Fraction(1)), (Fraction(1), Fraction(1))) + require(matrix_rank(nonflag) < sum(nonflag[i][i] != 0 for i in range(2)), + 'nonflag rank boundary') + exact_nodes, exact_frames, out, target = swap_fixture(3, 2, 2, True) + changed = list(exact_frames) + changed[2] = ((Fraction(1), Fraction(1)), (Fraction(0), Fraction(0))) + changed[4] = ((Fraction(1), Fraction(-1)), (Fraction(0), Fraction(0))) + require(framed_bill(exact_nodes, tuple(changed), 2, out, target) >= 4, + 'noncommuting flag positive') + require(all(ok for _, _, ok in observations(exact_nodes, 3, 2, out, target)), + 'noncommuting flag endpoint') + return ('strict threshold', 'biased inputs', 'correlated inputs', + 'nonflag rank', 'noncommuting triangular positive') + + +def main() -> None: + require(len(sys.argv) == 1, 'unexpected arguments') + result = {'status': 'PASS_BOUNDED_ERROR_PARTITION_THRESHOLD', + 'map_census': map_census(), 'attainment': attainment_census(), + 'rejecting_controls': rejecting_controls(), + 'boundary_controls': boundary_controls()} + package = Path(__file__).resolve().parent + names = ('README.md', 'PROOF.md', 'TASK.json', 'SOURCES.json', 'VERIFY.json', 'verify.py') + result['sha256'] = {name: hashlib.sha256((package / name).read_bytes()).hexdigest() + for name in names} + print(json.dumps(result, sort_keys=True, indent=2)) + + +if __name__ == '__main__': + main()