From ecd0e3512ea3f108112ea4c127dd4ced2369b7a0 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Thu, 22 Oct 2026 20:21:05 +0100 Subject: [PATCH] feat(research): prove the two-call chain retiming premium --- research/depth6-chain-retiming/README.md | 177 ++++++++++++++++++ research/depth6-chain-retiming/SOURCES.json | 18 ++ research/depth6-chain-retiming/TASK.json | 106 +++++++++++ research/depth6-chain-retiming/VERIFY.json | 32 ++++ research/depth6-chain-retiming/verify.py | 195 ++++++++++++++++++++ 5 files changed, 528 insertions(+) create mode 100644 research/depth6-chain-retiming/README.md create mode 100644 research/depth6-chain-retiming/SOURCES.json create mode 100644 research/depth6-chain-retiming/TASK.json create mode 100644 research/depth6-chain-retiming/VERIFY.json create mode 100644 research/depth6-chain-retiming/verify.py diff --git a/research/depth6-chain-retiming/README.md b/research/depth6-chain-retiming/README.md new file mode 100644 index 0000000000..9bf6bc2ddf --- /dev/null +++ b/research/depth6-chain-retiming/README.md @@ -0,0 +1,177 @@ +# Two extra calls suffice for genuine depth-six chain retiming + +This contribution was produced by Nick Petalas. It answers Open next +question 2 of [#4748](https://github.com/CrocSwap/integer-mult-bounds/pull/4748): +the least number of unsigned complete calls permitting a commuting +retiming in a binary depth-six dirty chain, without any cancellation +obtainable by commuting calls, is **22**. This is exactly two above the +known 20-call minimum. + +The new result is a scoped construction and proof. Its lower bound uses +#4748's cited finite shortest-word classification at +`fc09e5b783989d769e6ae6fffeb7d23b30177c86`. This package neither imports nor +replays that classification. No new kappa or supplier admission is claimed. + +## Exact question + +Call l performs `z_l += B_l z_(l-1)`, for l=1,...,6. The source z_0 is +immutable. Every other register starts arbitrarily dirty; z_1,...,z_5 +must be restored, and the only final change is + +```text +z_6 += B_6 B_5 B_4 B_3 B_2 B_1 z_0. +``` + +The maps are arbitrary compatible linear maps over a nonzero unital ring +of characteristic two. Calls have equal unit prices. No inverse, +scaling, fused call, extra storage or other operation is allowed. + +Distinct calls i,j commute universally exactly when `|i-j|>1`. Equal +calls cancel in pairs. Call a word commutation-reduced if no sequence of +these commuting swaps can expose adjacent equal calls. This is stronger +than merely having no equal neighbors in the displayed word. It excludes +an inserted cancelling pair even when that pair has been separated by +commuting calls. A retiming means one actual adjacent swap of distinct +commuting calls, giving a different chronological word. + +## Construction and proof + +Use the two words + +```text +W = 1234656564321234565432 +V = 1236456564321234565432. +``` + +They differ by swapping calls 4 and 6 at positions 4 and 5, counted from +one. Both have count vector `(2,4,4,4,4,4)` and length 22. + +First, both are universally correct. Start with the known bridge word +`(1234565432)^2`, and replace its first `565` by `65656`. This gives W. +For two adjacent chain calls A,B in characteristic two, + +```text +ABA = BABAB. +``` + +To see the identity with arbitrary maps, write A=I+X and B=I+Y. Here +X^2=Y^2=0 and one of XY,YX is zero. Thus +`(AB)^2=I+XY+YX`; the remaining product has square zero, so `(AB)^4=I`. +Since A and B are involutions, `ABABABAB=I` implies `ABA=BABAB`. +The identity works with chronological products in either convention. +Apply it to A=call 5, B=call 6. The swap giving V preserves the operator. +The bridge construction is prior work, credited below. + +There is also a direct certificate independent of this substitution. For +every increasing interval i,...,j, count scattered occurrences of +`i(i+1)...j` in W or V. Its parity is the coefficient of +`B_j ... B_i` from the initial z_(i-1) to the final z_j. Every parity is +zero except the full interval 1,...,6, whose parity is one. This proves +correctness for arbitrary maps without assuming that maps commute. +The verifier emits all 21 integer counts for each new word. + +Second, both words are commutation-reduced. For every two consecutive +occurrences of a call i, there is a call i-1 or i+1 between them. Such a +call fails to commute with either endpoint. Label occurrences individually. +Commuting swaps preserve the relative order of every pair of +noncommuting occurrences. Therefore the intervening call stays between +the two i occurrences until a deletion occurs. A first deletion is +impossible. Each word has 16 such consecutive equal-call pairs, and the +verifier emits a blocker position for every one. This proves the +noncancellation claim for arbitrarily many commuting swaps, without +searching their equivalence class. + +Finally, 22 is minimal. Yifan Kang's Proposition 3.1 gives the known +20-call minimum. #4748's complete classification states that every +20-call schedule is a cyclic rotation of `(1234565432)^2`, and none has +an adjacent commuting pair. Every valid word has even multiplicity of +each call, because each singleton interval coefficient must vanish. +Hence length 21 is impossible. The displayed 22-call words attain the +first remaining length and are commutation-reduced. This last exclusion +of length 20 depends on #4748, rather than being a new independent proof +of its classification. + +## Verification and reproduction + +From the repository root with CPython 3.12 and the standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/depth6-chain-retiming/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -O -W error -B research/depth6-chain-retiming/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/depth6-chain-retiming +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/depth6-chain-retiming --check-source-history +``` + +Any CPython 3.12 interpreter can replace the local path. Both registered +commands run the complete new certificate. The output is a generated JSON +receipt bound to the five package files, followed by + +```text +PASS_DEPTH6_CHAIN_RETIMING calls=22 extra=2 blockers=32 scalar=16384 matrix=1792 relation=1536 controls=10 +``` + +The direct interval-count and 7-by-7 matrix checks agree. Literal dirty +replays cover every choice of six binary scalar maps and seven initial +bits for both words, for 16,384 cases. Two-coordinate replay checks 64 +deterministic six-map tuples on fourteen initial basis vectors for each +word, for 1,792 cases. The local three-call/five-call relation is checked +on all 256 pairs of binary 2-by-2 maps and six initial basis vectors, +for 1,536 comparisons. These finite checks support the written proof; +they do not prove the arbitrary-map statement by extrapolation. + +Ten rejection controls cover four incorrect endpoints, a valid but +commutation-reducible 22-call word, two smaller reducible words, an +unknown call, the wrong characteristic for the witness, and the local +relation in characteristic three. Checks use explicit exceptions and +remain enabled under optimized Python. No predecessor verifier runs. + +## Limits and implementation bounds + +The exact 22-call threshold uses the cited #4748 classification. No +independent human or formal proof-kernel review is claimed. There is no +classification of all length-22 words, all-depth theorem, other-characteristic +result, unequal-price optimum or physical supplier implementation. +Routing, native preparation, dispatch, precision, tape/storage, recursive +admission and a complete multiplication theorem remain outside scope. +The selected frontier stays unchanged. + +The standalone verifier has no recursion, subprocess, network or file +writes. Inputs are fixed words of at most 22 calls; literal state size is +at most seven two-bit registers. All loops have fixed finite bounds in +code, and every function is below 60 lines. Explicit exceptions enforce +word, map and register ranges and the mathematical invariants. Standard +Python container and integer allocation is a managed-runtime deviation +from fixed-allocation operation. Its scope is this bounded one-shot +verifier, compensated by fixed case counts and a one-MiB limit per hashed +package file. Follow up with fixed-capacity buffers only if this checker +becomes a long-lived service. Warning-strict normal and optimized replay +supply the local interpreted-language diagnostics; no separate static +type checker or compiled build is claimed. + +## Open next questions + +1. How many commutation-reduced length-22 schedules are there, and how + many commuting-equivalence classes do they form? Start with a bounded + near-shortest-path search. The present result proves existence and the + exact threshold, not a census. +2. Can the no-retiming statement at length 20 be proved structurally, + replacing the dependence on #4748's finite classification? Start with + the known minimum count vector and forced chronological dependencies. +3. Does an actual six-stage supplier consumer benefit from this extra + retiming freedom? Name its maps and charge routing, frame changes and + restoration before interpreting the abstract two-call cost as savings. + +## Credit + +Nick Petalas's #4748 supplies the exact shortest-word classification and +this open question. The original contribution here is the exact +commutation-reduced retiming threshold and its explicit witnesses. +Yifan Kang's [CNOT-Optimal Circuit Synthesis, Proposition 3.1](https://math.mit.edu/documents/rsi/2023KangY.pdf) +supplies the known directed-path minimum and bridge construction, building +on the construction attributed there to Nash et al. Nick Petalas's +#4249/#4263/#4281 supply the chain model and interval-count reduction; +Ryanson Jonathan's #4418 addresses separate depth-five residues. Ross +Richardson's #943/#934 lineage supplies the complete-call dirty connector +interface. The involution identity and the blocker argument are elementary +algebra and commutation arguments, not new general group-theoretic claims. +Apache-2.0. diff --git a/research/depth6-chain-retiming/SOURCES.json b/research/depth6-chain-retiming/SOURCES.json new file mode 100644 index 0000000000..4916cee8e5 --- /dev/null +++ b/research/depth6-chain-retiming/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "b58ad9ef4d4e861b0eaa5dba41742bdc072dca51", + "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" + } + ] +} diff --git a/research/depth6-chain-retiming/TASK.json b/research/depth6-chain-retiming/TASK.json new file mode 100644 index 0000000000..dc6c268b0f --- /dev/null +++ b/research/depth6-chain-retiming/TASK.json @@ -0,0 +1,106 @@ +{ + "schema_version": 1, + "task_id": "connector-alphabet-change", + "priority_revision": 7, + "base_commit": "b58ad9ef4d4e861b0eaa5dba41742bdc072dca51", + "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": "The exact 22-call threshold for commutation-reduced binary depth-six dirty-chain schedules admitting a nontrivial commuting retiming.", + "scope_change_reason": "Take Open next question 2 of PR4748 rather than extending a construction family. The connector alphabet stays fixed; the new quantity is the extra chronological freedom beyond the known optimum.", + "bottleneck_link": "An exact two-call premium quantifies retiming flexibility in a six-stage arbitrary-map connector. No physical consumer or recursive saving is supplied.", + "budget_minutes": 60, + "stop_rule": "Stop at the first verified exact retiming threshold. Do not enumerate length-22 classes or change depth.", + "outcome": "completed", + "evidence": "Two explicit 22-call witnesses pass direct interval counts, full matrix endpoint checks, all binary scalar dirty cases, two-coordinate controls, and blocker certificates proving no cancellation after arbitrary commuting swaps. The exact threshold cites PR4748 for the no-retiming result at length 20.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "How many commutation-reduced length-22 words and commuting-equivalence classes are there?", + "why_it_matters": "Distinguishes one exhibited retiming from the complete chronology flexibility.", + "first_step": "Bounded near-shortest-path enumeration.", + "blocked_by": "No length-22 census is supplied." + }, + { + "question": "Can the 20-call no-retiming statement be proved structurally?", + "why_it_matters": "Replaces the finite classification dependency.", + "first_step": "Derive chronological constraints from the known minimum count vector.", + "blocked_by": "The lower-bound step here cites PR4748." + }, + { + "question": "Can an actual supplier benefit from the two-call retiming premium?", + "why_it_matters": "An abstract schedule need not lower a fully paid recursive bill.", + "first_step": "Name an actual six-stage consumer and charge its full physical boundary.", + "blocked_by": "No native caller or price is supplied." + } + ], + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19131105", + "scientific_dependencies": [ + { + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/4748", + "head": "fc09e5b783989d769e6ae6fffeb7d23b30177c86", + "used_claim": "The ten shortest 20-call schedules have no adjacent commuting calls.", + "status": "Cited published finite classification, not independently rechecked here; no executable import." + }, + { + "url": "https://math.mit.edu/documents/rsi/2023KangY.pdf", + "author": "Yifan Kang", + "title": "CNOT-Optimal Circuit Synthesis", + "date": "2023-08-01", + "used_claim": "Proposition 3.1 supplies the known directed-path minimum and bridge construction." + } + ], + "coordination": { + "priority_revision": 7, + "upstream_commit": "1f87c3578ae546c8f903f7f4d83dc2e2fb99650b", + "checked_at": "2026-10-22T19:20:54.505538+00:00", + "overlap": "Entry scan: 521 open PR records and 3676 Discussion records. Pre-commit refresh: 426 open PR records at 2026-10-22T19:19:51Z and 3682 Discussion records at 2026-10-22T19:20:37Z, with complete reported pagination. Read latest handoff and relevant PR bodies; searched exact witness, reduced-retiming terms and depth-six object on canonical main and merged PRs. Local cached-note coverage is sparse; no no-match guarantee of novelty is claimed.", + "related_open_work": [ + 4748, + 1930 + ], + "preserved_branch": "research/w1-1022e-depth6-binary-chain", + "preserved_commit": "fc09e5b783989d769e6ae6fffeb7d23b30177c86", + "refresh_result": "Priority guidance, catalogue, selected record and family status are unchanged from the pinned research base. Retain the original scientific baseline; archive intake and export documentation advanced independently.", + "related_merged_work": [ + 4600 + ] + } +} diff --git a/research/depth6-chain-retiming/VERIFY.json b/research/depth6-chain-retiming/VERIFY.json new file mode 100644 index 0000000000..539691c6a3 --- /dev/null +++ b/research/depth6-chain-retiming/VERIFY.json @@ -0,0 +1,32 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Both new 22-call endpoints, integer interval coefficients, 32 blockers, 16384 scalar cases, 1792 matrix cases, 1536 local-relation cases and ten controls." + }, + { + "argv": [ + "{python}", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same complete new certificate with optimized Python. The cited shortest-word lower bound is not replayed." + } + ] +} diff --git a/research/depth6-chain-retiming/verify.py b/research/depth6-chain-retiming/verify.py new file mode 100644 index 0000000000..7cbe0c11e8 --- /dev/null +++ b/research/depth6-chain-retiming/verify.py @@ -0,0 +1,195 @@ +#!/usr/bin/env python3 +"""Check the new 22-call witnesses, without replaying the cited lower bound.""" + +from hashlib import sha256 +from itertools import product +import json +from pathlib import Path +import sys + + +PACKAGE_FILES = ("README.md", "SOURCES.json", "TASK.json", "VERIFY.json", "verify.py") +WORD = tuple(int(x) for x in "1234656564321234565432") +RETIME = WORD[:3] + (6, 4) + WORD[5:] + + +def require(condition: bool, message: str) -> None: + if not condition: + raise ValueError(message) + + +def validate_word(word: tuple[int, ...]) -> None: + require(1 <= len(word) <= 22, "word length outside the fixed certificate") + require(all(type(x) is int and 1 <= x <= 6 for x in word), "unknown call") + + +def interval_counts(word: tuple[int, ...]) -> tuple[int, ...]: + """Integer scattered-subword counts for all 21 increasing intervals.""" + validate_word(word) + answer = [] + for start in range(1, 7): + counts = [0] * 7 + counts[start - 1] = 1 + for letter in word: + if letter >= start: + counts[letter] += counts[letter - 1] + answer.extend(counts[start:]) + return tuple(answer) + + +def endpoint(word: tuple[int, ...], modulus: int = 2) -> tuple[tuple[int, ...], ...]: + validate_word(word) + require(modulus in (2, 3), "unsupported scalar control modulus") + rows = [[int(i == j) for j in range(7)] for i in range(7)] + for letter in word: + rows[letter] = [(x + y) % modulus + for x, y in zip(rows[letter], rows[letter - 1])] + return tuple(tuple(row) for row in rows) + + +def correct(word: tuple[int, ...]) -> bool: + target = tuple(tuple(int(i == j) ^ int(i == 6 and j == 0) + for j in range(7)) for i in range(7)) + counts = interval_counts(word) + expected = tuple(int(i == 1 and j == 6) + for i in range(1, 7) for j in range(i, 7)) + return tuple(x % 2 for x in counts) == expected and endpoint(word) == target + + +def blocked_pairs(word: tuple[int, ...]) -> tuple[tuple[int, int, int], ...]: + """Return one noncommuting blocker for each consecutive equal-call pair.""" + validate_word(word) + certificate = [] + for letter in range(1, 7): + positions = [i for i, x in enumerate(word) if x == letter] + for left, right in zip(positions, positions[1:]): + blockers = [i for i in range(left + 1, right) + if abs(word[i] - letter) == 1] + require(bool(blockers), "commuting moves can expose an equal-call pair") + certificate.append((left, right, blockers[0])) + return tuple(certificate) + + +def action(word: tuple[int, ...], maps: tuple[int, ...], + initial: tuple[int, ...], dimension: int) -> tuple[int, ...]: + """Literal dirty-register replay using bit-encoded linear maps.""" + validate_word(word) + require(dimension in (1, 2), "unsupported replay dimension") + limit = 1 << dimension + require(len(maps) == 6 and all(0 <= x < limit ** dimension for x in maps), + "invalid map tuple") + require(len(initial) == 7 and all(0 <= x < limit for x in initial), + "invalid initial tuple") + values = list(initial) + for letter in word: + values[letter] ^= apply_map(maps[letter - 1], values[letter - 1], dimension) + return tuple(values) + + +def apply_map(matrix: int, value: int, dimension: int) -> int: + output = 0 + for row in range(dimension): + bits = (matrix >> (row * dimension)) & ((1 << dimension) - 1) + output |= ((bits & value).bit_count() % 2) << row + return output + + +def expected_action(maps: tuple[int, ...], initial: tuple[int, ...], + dimension: int) -> tuple[int, ...]: + value = initial[0] + for matrix in maps: + value = apply_map(matrix, value, dimension) + return initial[:6] + (initial[6] ^ value,) + + +def replay_cases() -> tuple[int, int]: + scalar_count = matrix_count = 0 + for maps in product(range(2), repeat=6): + for initial in product(range(2), repeat=7): + expected = expected_action(maps, initial, 1) + for word in (WORD, RETIME): + require(action(word, maps, initial, 1) == expected, "scalar replay") + scalar_count += 1 + for seed in range(64): + maps = tuple((seed * (2 * i + 1) + i * i + 3 * (seed >> 2)) % 16 + for i in range(6)) + for coordinate in range(14): + initial = tuple((1 << (coordinate % 2)) if i == coordinate // 2 else 0 + for i in range(7)) + expected = expected_action(maps, initial, 2) + for word in (WORD, RETIME): + require(action(word, maps, initial, 2) == expected, "matrix replay") + matrix_count += 1 + return scalar_count, matrix_count + + +def local_relation() -> int: + comparisons = 0 + for first, second in product(range(16), repeat=2): + maps = (0, 0, 0, 0, first, second) + for coordinate in range(6): + initial = tuple((1 << (coordinate % 2)) if i == 4 + coordinate // 2 else 0 + for i in range(7)) + require(action((5, 6, 5), maps, initial, 2) + == action((6, 5, 6, 5, 6), maps, initial, 2), "local relation") + comparisons += 1 + return comparisons + + +def controls() -> int: + count = 0 + for bad in (WORD[:-1], WORD[1:], tuple(range(1, 7)), + WORD[:4] + (5,) + WORD[5:]): + require(not correct(bad), "bad endpoint was accepted") + count += 1 + redundant = (6, 1, 6) + tuple(int(x) for x in "2345654321234565432") + require(correct(redundant), "redundancy control must have the right endpoint") + for word in (redundant, (1, 1), (1, 3, 1)): + try: + blocked_pairs(word) + except ValueError: + count += 1 + else: + raise ValueError("reducible word was accepted") + try: + validate_word((0,)) + except ValueError: + count += 1 + else: + raise ValueError("unknown call was accepted") + require(endpoint(WORD, 3) != endpoint(RETIME, 2), "odd-characteristic control") + require(endpoint((5, 6, 5), 3) != endpoint((6, 5, 6, 5, 6), 3), + "local relation was wrongly extended to characteristic three") + return count + 2 + + +def receipt() -> dict[str, str]: + package = Path(__file__).resolve().parent + hashes = {} + for name in PACKAGE_FILES: + path = package / name + require(path.is_file() and not path.is_symlink(), "invalid package file") + require(path.stat().st_size <= 1024 * 1024, "oversized package file") + hashes[name] = sha256(path.read_bytes()).hexdigest() + return hashes + + +def main() -> None: + require(len(WORD) == len(RETIME) == 22 and WORD != RETIME, "witness shape") + require(abs(WORD[3] - WORD[4]) > 1, "retimed calls must commute") + require(correct(WORD) and correct(RETIME), "incorrect witness") + certificates = [blocked_pairs(word) for word in (WORD, RETIME)] + require(all(len(c) == 16 for c in certificates), "blocker coverage") + scalar, matrix = replay_cases() + relation = local_relation() + negative = controls() + print(json.dumps({"schema": "depth6-chain-retiming/v1", "python": sys.version, + "words": ["".join(map(str, w)) for w in (WORD, RETIME)], + "counts": [interval_counts(w) for w in (WORD, RETIME)], + "blockers": certificates, "package_sha256": receipt()}, sort_keys=True)) + print(f"PASS_DEPTH6_CHAIN_RETIMING calls=22 extra=2 blockers=32 " + f"scalar={scalar} matrix={matrix} relation={relation} controls={negative}") + + +if __name__ == "__main__": + main()