diff --git a/research/dyadic-helper-basis-completion/PROOF.md b/research/dyadic-helper-basis-completion/PROOF.md new file mode 100644 index 0000000000..8c51201534 --- /dev/null +++ b/research/dyadic-helper-basis-completion/PROOF.md @@ -0,0 +1,77 @@ +# Complete dyadic basis construction + +Let D = Z[1/2]. Let a be a row and b a column in D^n, with a b = 1. +For any index p there is an invertible R over D such that a R = e_p^T +and R e_p = b. The compiler emits R as ordinary ADDs with coefficients +in D and SCALEs by units of D. All operations use the same physical chart. +This is an application of the Euclidean algorithm, not a new theorem about +principal ideal domains. Nick Petalas used Euclidean row preparation in +[PR5115](https://github.com/CrocSwap/integer-mult-bounds/pull/5115) +for a single-hub shear. Here both the row and column are prescribed. + +First clear all denominators of a by a common power of two, d. Each +column scaling is invertible over D. Apply the integer Euclidean algorithm +to coordinate p and each other coordinate. An ADD and a swap perform +one division step. The nonzero pivot becomes the gcd g of the integer +coordinates, up to sign. Because a b = 1, every odd prime divisor of g +would divide 1 in D. Thus g has no odd prime divisor. It is a unit in D. +A final unit scaling gives a P = e_p^T. Each operation used to construct +P is invertible over D. The loop terminates because each Euclidean +remainder has smaller absolute value than its divisor. + +Set c = P^-1 b. Then c_p = a b = 1. The shear + +```text +S = I + (c - e_p) e_p^T +``` + +is a product of ADDs on rows other than p. It satisfies S e_p = c and +e_p^T S = e_p^T. Set R = P S. Then + +```text +a R = e_p^T, R e_p = b. +``` + +Execution order is S followed by the reverse order of the right factors +of P. The compiler records this order explicitly. Its inverse uses the +reverse instruction list, with negative ADD coefficients and inverse +SCALE coefficients. No odd division, extra field, native MOVE or owned +zero is required. Scalar coefficients remain outside the tensor power. +Thus the identity holds for whole fields at every positive tensor width. + +The pinned PR5602 constructor requires some a_i to be a dyadic unit. +That condition is sufficient but unnecessary. For example, + +```text +a = (3, 5), b = (2, -1)^T, +R = [[2, 5], [-1, -3]], det(R) = -1. +``` + +Both identities hold. Neither entry of a is a unit. More generally, +completeness depends on the ideal generated by the row, not on any one +entry. The supplied b proves that this ideal is D. A rational pair whose +coefficients have odd denominators is outside this arithmetic contract. + +## Exact caller boundary and limits + +The two uses in PR5602 are the input/output helper basis and the common +cut basis. Its handoff proof needs only the two displayed identities, +invertibility and common charts. This compiler supplies those algebraic +requirements for all dyadic dual pairs. It does not find the prefix/suffix +kernels, prove that a cut exists, change a frame or add a productive target. +The source's nine witnesses supply 18 concrete interfaces. The verifier +checks all 18 with a separate dense matrix interpreter. + +An emitted ADD with a large coefficient is not free. A consumer must +check the source's coefficient bound, total scalar allowance, prefix growth, +operation count and fixed-tape costs before installation. This package does +not replace the source constructor or rerun its physical caller, native +phases, compiler or outer proof. It does not increase complete kappa or +change the selected frontier. The five inherited assumptions stay open. + +The finite tests corroborate the algorithm and find implementation errors. +The argument above establishes the all-input statement. Neither the tests +nor this paper proof are proof-assistant or independent human acceptance. + +Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. +Credit the PR5599/5602 helper handoff and all retained P104 predecessors. diff --git a/research/dyadic-helper-basis-completion/README.md b/research/dyadic-helper-basis-completion/README.md new file mode 100644 index 0000000000..595d586859 --- /dev/null +++ b/research/dyadic-helper-basis-completion/README.md @@ -0,0 +1,67 @@ +# Complete the dyadic helper-basis constructor + +This enabling algorithm removes the unit-entry restriction in the +[PR5602](https://github.com/CrocSwap/integer-mult-bounds/pull/5602) helper +basis constructor. For every dyadic row a and column b with a b = 1, +[basis.py](basis.py) emits ADD and unit SCALE operations for R with +`a R = e_p^T` and `R e_p = b`. The pair `(3,5)` and `(2,-1)` is legal +but has no unit row entry. The old sufficient test rejects it. + +The [proof](PROOF.md) gives the complete construction. The +[replay](verify.py) uses a separate dense matrix interpreter and checks all +18 basis interfaces from the source's nine handoffs. It also checks every +integer dual pair in `[-5,5]^2` at both pivots: 616 compilations, including +16 primitive pairs omitted by the old test. Another 96 presentations cover +dimensions 1 through 12 and dyadic fractions. Five invalid-input controls +and an operation-sign control reject their defects. [RESULT.json](RESULT.json) +is the exact receipt. [SOURCES.json](SOURCES.json) pins all consumed inputs. + +This is a complete constructor for one algebraic interface. It does not +find a new physical helper channel. Complete kappa is unchanged. Consumers +must charge the emitted scalar operations and recheck growth, operation +count, native maps, ownership, the physical caller and the full invoice. +The complete selected replay was not run: orientation read the selected +record and its promotion proof; its sparse source closure is not present. + +## Reproduce + +Python 3.12 and the standard library suffice. From the repository root: + +```sh +python3 -B scripts/research_package.py --package research/dyadic-helper-basis-completion +``` + +Normal and optimized commands must print `PASS_DYADIC_HELPER_BASIS_COMPLETION`. +The launcher must print `PASS_REGISTERED_RESEARCH_PACKAGE`. The scientific +checker does not call Git or the network. Export the package with its three +declared source files. A source hash mismatch fails before the checks. + +## Scope and credit + +Base: canonical main `d7633ce230196a1d5d061347de7a0fd8be512ed6`, priority 7. +The three source files equal PR5602 head +`6c224aa720203c4f4615e6538d8038a275387db8`. The +[claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/5125#discussioncomment-19184390) +is separate from the active different-carrier and word-reassociation searches. +Remote overlap pagination was complete at 22:17 UTC; local notes are sparse. +No exhaustive novelty claim is made. + +Ali Romman's [PR5599](https://github.com/CrocSwap/integer-mult-bounds/pull/5599) +and PR5602 supply the helper handoff, source witnesses and compiler interface. +Nick Petalas's [PR5115](https://github.com/CrocSwap/integer-mult-bounds/pull/5115) +already uses Euclidean row preparation for a different single-hub shear +contract. Its [proof](https://github.com/CrocSwap/integer-mult-bounds/blob/391355b8e537b82cedabd45af509177496e7a7a6/research/dyadic-rankone-borrowing/README.md) +is related prior work. The present interface prescribes both a row and a +column. It does not claim row preparation as new. The Euclidean method is standard. The P104/native/controller/compiler lineage +retains its source credit; it is not re-proved here. New implementation, +interface proof and checks: Ali Romman with substantial OpenAI Codex assistance. +Apache-2.0. No independent human or formal-kernel acceptance is claimed. + +## Open next questions + +Use the complete constructor in the current cut search only after checking +live overlap. First test whether a previously rejected dual pair gives a +new physical target. Then charge the emitted scalar work and growth and +rerun the complete caller. Feasibility over the dyadic ring is distinct +from feasibility over the rational field. An exact pairing-ideal test can +prevent searches from relying on an unavailable odd inverse. diff --git a/research/dyadic-helper-basis-completion/RESULT.json b/research/dyadic-helper-basis-completion/RESULT.json new file mode 100644 index 0000000000..ee1d4fa877 --- /dev/null +++ b/research/dyadic-helper-basis-completion/RESULT.json @@ -0,0 +1,124 @@ +{ + "counterexample_operations": [ + [ + "SCALE", + 1, + 1, + "-1" + ], + [ + "ADD", + 0, + 1, + "1" + ], + [ + "ADD", + 1, + 0, + "-1" + ], + [ + "ADD", + 0, + 1, + "1" + ], + [ + "ADD", + 1, + 0, + "-2" + ], + [ + "SCALE", + 1, + 1, + "-1" + ], + [ + "ADD", + 0, + 1, + "1" + ], + [ + "ADD", + 1, + 0, + "-1" + ], + [ + "ADD", + 0, + 1, + "1" + ], + [ + "ADD", + 1, + 0, + "-1" + ], + [ + "SCALE", + 1, + 1, + "-1" + ], + [ + "ADD", + 0, + 1, + "1" + ], + [ + "ADD", + 1, + 0, + "-1" + ], + [ + "ADD", + 0, + 1, + "1" + ], + [ + "ADD", + 1, + 0, + "-1" + ], + [ + "SCALE", + 1, + 1, + "-1" + ], + [ + "ADD", + 0, + 1, + "1" + ], + [ + "ADD", + 1, + 0, + "-1" + ], + [ + "ADD", + 0, + 1, + "1" + ] + ], + "exhaustive_compilations": 616, + "larger_presentations": 96, + "omitted_primitive_pairs": 16, + "rejected_inputs": 5, + "sign_control": true, + "source_interfaces": 18 +} diff --git a/research/dyadic-helper-basis-completion/SOURCES.json b/research/dyadic-helper-basis-completion/SOURCES.json new file mode 100644 index 0000000000..88def2abcc --- /dev/null +++ b/research/dyadic-helper-basis-completion/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "d7633ce230196a1d5d061347de7a0fd8be512ed6", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "fc3d4ba105e1f097d0d7d051a308281e86ab1446", + "sha256": "66974efdced4083c00025f97d95d83909a226cdf801edb9301c195c6641f6903" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/p104-coupled-helper-bases/PROOF.md", + "usage": "input", + "git_blob": "168733f6c486d689e58de15c6c34ce1b5ae6b12d", + "sha256": "d9049aa75f065c3c21b0f55246c433c643584bca8969f2f382a83c425c4a2927" + }, + { + "path": "research/p104-coupled-helper-bases/WITNESS.json", + "usage": "input", + "git_blob": "8073b3c9772a4a7c94e07d613c2f5c45b1c650fc", + "sha256": "e4dfc526453eb9d232772ffdb587fff1923e247341405aee031318b0fb9cb638" + }, + { + "path": "research/p104-coupled-helper-bases/construct.py", + "usage": "input", + "git_blob": "ef5936ca89d6502d7f6af1ce6903d8500c117401", + "sha256": "2360066b0a1390c60a86d9788ada1504478e7e48bbfe3fcdf27a5563379fc001" + } + ] +} diff --git a/research/dyadic-helper-basis-completion/TASK.json b/research/dyadic-helper-basis-completion/TASK.json new file mode 100644 index 0000000000..55dbc13771 --- /dev/null +++ b/research/dyadic-helper-basis-completion/TASK.json @@ -0,0 +1,100 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 7, + "base_commit": "d7633ce230196a1d5d061347de7a0fd8be512ed6", + "original_card": { + "id": "formal-interface-lemma", + "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/gate-operand-parity-lean/README.md", + "research/staged544-certified-endpoint/README.md", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Formalize a missing boundary lemma identified by the selected review.", + "Audit a formal theorem-to-certificate binding independently." + ], + "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Inventory the gate-operand parity lemma (#3807) and certified endpoint arithmetic (#3857). Neither is a full multiplication proof. For #4100, audit the compact-switch statement and its hypotheses before formalizing it.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.", + "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.", + "allowed_variations": [ + "Narrow to one formal lemma or one theorem-to-certificate binding." + ], + "scope_change_triggers": [ + "Formalizing already-covered arithmetic and claiming the full multiplication theorem." + ], + "overlap_terms": [ + "hyperplane end", + "formal interface", + "Lean binding", + "3807", + "3857", + "4100", + "gate-operand-parity-lean", + "staged544-certified-endpoint", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #3807: scoped gate-operand parity formalization.", + "evidence": "research/gate-operand-parity-lean/README.md", + "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.", + "status": "author-checked", + "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #3857: certified real-power moment/endpoint arithmetic.", + "evidence": "research/staged544-certified-endpoint/README.md", + "remaining": "Uniform algorithmic implications, not another endpoint digit.", + "status": "author-checked", + "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4100: compact-switch formalization proposed as future validation.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Audit the statement and assumptions before a formal proof campaign.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Complete ADD and dyadic-unit SCALE construction for the dual helper-basis interface in PR5602.", + "scope_change_reason": "A constructive paper proof and exact executable interface replace the generic formalization assignment. No proof-assistant claim is made.", + "bottleneck_link": "The old unit-entry test omits legal dyadic helper bases. Completing it removes an artificial restriction on productive helper channels.", + "budget_minutes": 60, + "stop_rule": "Prove the full dual-pair interface and check all 18 pinned basis witnesses, exhaustive small pairs and rejecting controls; do not claim a new caller.", + "outcome": "completed", + "evidence": "PROOF.md, RESULT.json, verify.py", + "author": "Ali Romman with substantial OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance in the proof, implementation, checks and prose.", + "open_questions": [ + { + "question": "Does a newly admitted dyadic pair give an additional physical helper target?", + "why_it_matters": "A new target can improve the complete signed moment.", + "first_step": "Recheck live claims, then test rejected source cut pairs and price all scalar operations.", + "blocked_by": "Actual frame, input and output support; complete caller, growth and compiler checks." + } + ], + "coordination": { + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/5125#discussioncomment-19184390", + "remote_checked_at": "2026-10-25T22:17:55Z", + "local_coverage": "sparse" + } +} diff --git a/research/dyadic-helper-basis-completion/VERIFY.json b/research/dyadic-helper-basis-completion/VERIFY.json new file mode 100644 index 0000000000..98e62b239c --- /dev/null +++ b/research/dyadic-helper-basis-completion/VERIFY.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/p104-coupled-helper-bases/PROOF.md", + "research/p104-coupled-helper-bases/WITNESS.json", + "research/p104-coupled-helper-bases/construct.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Source hashes, all 18 pinned basis interfaces, complete small dual-pair census, dense inverse identities and invalid-input controls." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "-O", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Source hashes, all 18 pinned basis interfaces, complete small dual-pair census, dense inverse identities and invalid-input controls." + } + ] +} diff --git a/research/dyadic-helper-basis-completion/basis.py b/research/dyadic-helper-basis-completion/basis.py new file mode 100644 index 0000000000..6b2bcbbb7c --- /dev/null +++ b/research/dyadic-helper-basis-completion/basis.py @@ -0,0 +1,83 @@ +"""Compile a dual dyadic pair to ADD and unit SCALE operations. + +Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. +""" +from fractions import Fraction as Q + + +def need(test, message): + if not test: + raise ValueError(message) + + +def dyadic(q): + return q.denominator & (q.denominator - 1) == 0 + + +def unit(q): + n = abs(q.numerator) + return n > 0 and n & (n - 1) == 0 and dyadic(q) + + +def inverse(ops): + return [(op, r, s, 1 / c if op == 'SCALE' else -c) + for op, r, s, c in reversed(ops)] + + +def apply(ops, vector): + out = list(map(Q, vector)) + for op, r, s, c in ops: + if op == 'ADD': + out[r] += c * out[s] + else: + need(op == 'SCALE', 'Known operation') + out[r] *= c + return out + + +def compile_basis(a, b, pivot): + """Return R with a R = e_p^T and R e_p = b, in execution order.""" + a, b = list(map(Q, a)), list(map(Q, b)) + n = len(a) + need(n == len(b) and 0 <= pivot < n, 'Matching nonempty vectors and pivot') + need(all(dyadic(q) for q in a + b), 'Dyadic input coefficients') + need(sum(x * y for x, y in zip(a, b)) == 1, 'Dual pairing equals one') + current, right = a[:], [] + + def emit(op, r, s, c): + c = Q(c) + if (op == 'ADD' and not c) or (op == 'SCALE' and c == 1): + return + right.append((op, r, s, c)) + if op == 'ADD': + current[s] += c * current[r] + else: + current[r] *= c + + def swap(r, s): + emit('ADD', r, s, 1) + emit('ADD', s, r, -1) + emit('ADD', r, s, 1) + emit('SCALE', s, s, -1) + + denominator = max(q.denominator for q in a) + for r in range(n): + emit('SCALE', r, r, denominator) + for s in range(n): + if s == pivot: + continue + while current[s]: + quotient = current[pivot] // current[s] + emit('ADD', s, pivot, -quotient) + swap(pivot, s) + need(unit(current[pivot]), 'Primitive row over the dyadic ring') + emit('SCALE', pivot, pivot, 1 / current[pivot]) + target = [Q(i == pivot) for i in range(n)] + need(current == target, 'Euclidean row reduction') + + # If P is the right product, c = P^-1 b and c[p] = 1. + c = apply(inverse(list(reversed(right))), b) + need(c[pivot] == 1, 'Normalized column pivot') + shear = [('ADD', r, pivot, value) for r, value in enumerate(c) + if r != pivot and value] + return shear + list(reversed(right)) diff --git a/research/dyadic-helper-basis-completion/verify.py b/research/dyadic-helper-basis-completion/verify.py new file mode 100644 index 0000000000..bdd87f6ffa --- /dev/null +++ b/research/dyadic-helper-basis-completion/verify.py @@ -0,0 +1,122 @@ +"""Check the complete basis compiler and the pinned caller witnesses. + +Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. +""" +import hashlib +import itertools +import json +from pathlib import Path +from fractions import Fraction as Q +from random import Random +from basis import compile_basis, inverse, apply, dyadic, unit, need + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] + + +def matrix(ops, n): + rows = [[Q(i == j) for j in range(n)] for i in range(n)] + for op, r, s, c in ops: + need(0 <= r < n and 0 <= s < n and dyadic(c), 'Legal operand') + if op == 'ADD': + need(r != s, 'Distinct ADD operands') + rows[r] = [x + c*y for x, y in zip(rows[r], rows[s])] + else: + need(op == 'SCALE' and unit(c), 'Unit SCALE') + rows[r] = [c*x for x in rows[r]] + return rows + + +def check(a, b, p): + a, b = list(map(Q, a)), list(map(Q, b)) + ops = compile_basis(a, b, p) + n = len(a) + r, inv = matrix(ops, n), matrix(inverse(ops), n) + need([sum(a[i]*r[i][j] for i in range(n)) for j in range(n)] == + [Q(j == p) for j in range(n)], 'Row identity') + need([r[i][p] for i in range(n)] == b, 'Column identity') + for i in range(n): + for j in range(n): + need(sum(r[i][k]*inv[k][j] for k in range(n)) == (i == j), + 'Independent dense inverse') + return ops + + +def main(): + sources = json.loads((HERE/'SOURCES.json').read_text()) + inputs = [x for x in sources['files'] if x['usage'] == 'input'] + for source in inputs: + data = (ROOT/source['path']).read_bytes() + need(hashlib.sha256(data).hexdigest() == source['sha256'], 'Pinned source bytes') + source = ROOT/'research/p104-coupled-helper-bases' + need("q = next((h for h in sorted(a) if unit(a[h])), None)" in + (source/'construct.py').read_text(), 'Source unit-entry restriction') + + source_cases = 0 + for step in json.loads((source/'WITNESS.json').read_text())['steps']: + if step['kind'] != 'coupled_handoff': + continue + for left, right in [('v', 'u'), ('source_functional', 'output_direction')]: + a, b = dict(step[left]), dict(step[right]) + keys = sorted(set(a) | set(b) | {step['pivot']}) + av, bv = [Q(a.get(i, 0)) for i in keys], [Q(b.get(i, 0)) for i in keys] + pair = sum(x*y for x, y in zip(av, bv)) + need(unit(pair), 'Source pairing') + check([q/pair for q in av], bv, keys.index(step['pivot'])) + source_cases += 1 + need(source_cases == 18, 'All nine source handoffs, at both boundaries') + + cases, no_unit = 0, 0 + for a in itertools.product(range(-5, 6), repeat=2): + for b in itertools.product(range(-5, 6), repeat=2): + if sum(x*y for x, y in zip(a, b)) != 1: + continue + no_unit += not any(unit(Q(q)) for q in a) + for p in range(2): + check(a, b, p) + cases += 1 + check([3, 5], [2, -1], 0) + need(no_unit > 0, 'Old restriction omits legal pairs') + + rng, larger = Random(20261025), 0 + for n in range(1, 13): + for trial in range(8): + p = trial % n + ops = [] + for _ in range(2*n): + if n > 1 and rng.randrange(3): + r, s = rng.sample(range(n), 2) + ops.append(('ADD', r, s, Q(rng.choice([-5, -3, 1, 3, 5]), 2**rng.randrange(3)))) + else: + r = rng.randrange(n) + ops.append(('SCALE', r, r, Q(rng.choice([-2, -1, 1, 2]), 2**rng.randrange(3)))) + r, ri = matrix(ops, n), matrix(inverse(ops), n) + check(ri[p], [r[i][p] for i in range(n)], p) + larger += 1 + + rejected = 0 + for a, b, p in [([3, 5], [1, 1], 0), ([Q(1, 3)], [3], 0), + ([3], [Q(1, 3)], 0), ([1], [1], 1), ([1, 0], [1], 0)]: + try: + compile_basis(a, b, p) + except ValueError: + rejected += 1 + else: + raise ValueError('Invalid basis accepted') + good = compile_basis([3, 5], [2, -1], 0) + bad = good[:] + op, r, s, c = bad[-1] + bad[-1] = (op, r, s, -c) + need(matrix(bad, 2) != matrix(good, 2), 'Sign mutation changes the output') + need(apply(good, [1, 0]) == [2, -1], 'Literal counterexample channel') + result = dict(source_interfaces=source_cases, exhaustive_compilations=cases, + omitted_primitive_pairs=no_unit, larger_presentations=larger, + rejected_inputs=rejected, sign_control=True, + counterexample_operations=[[op,r,s,str(c)] for op,r,s,c in good]) + need(result == json.loads((HERE/"RESULT.json").read_text()), "Committed receipt") + print(json.dumps(result, sort_keys=True)) + print('PASS_DYADIC_HELPER_BASIS_COMPLETION') + + +if __name__ == '__main__': + main()