From 26117c30f9ab47bfcbc198e0edbe54ebbd57340e Mon Sep 17 00:00:00 2001 From: Ali Romman <226877337+aliromman@users.noreply.github.com> Date: Fri, 23 Oct 2026 01:30:36 -0500 Subject: [PATCH] Certify nine-call path and star transposition minima --- research/swap-path-star-certificate/CUTS.json | 110 +++++++++++ research/swap-path-star-certificate/README.md | 176 ++++++++++++++++++ .../swap-path-star-certificate/RESULT.json | 79 ++++++++ .../swap-path-star-certificate/SOURCES.json | 30 +++ research/swap-path-star-certificate/TASK.json | 87 +++++++++ .../swap-path-star-certificate/VERIFY.json | 34 ++++ research/swap-path-star-certificate/verify.py | 165 ++++++++++++++++ 7 files changed, 681 insertions(+) create mode 100644 research/swap-path-star-certificate/CUTS.json create mode 100644 research/swap-path-star-certificate/README.md create mode 100644 research/swap-path-star-certificate/RESULT.json create mode 100644 research/swap-path-star-certificate/SOURCES.json create mode 100644 research/swap-path-star-certificate/TASK.json create mode 100644 research/swap-path-star-certificate/VERIFY.json create mode 100644 research/swap-path-star-certificate/verify.py diff --git a/research/swap-path-star-certificate/CUTS.json b/research/swap-path-star-certificate/CUTS.json new file mode 100644 index 0000000000..5583fd8e01 --- /dev/null +++ b/research/swap-path-star-certificate/CUTS.json @@ -0,0 +1,110 @@ +{ + "schema": "swap-path-star-certificate/v1", + "order": "lexicographic permutations of 0123", + "cases": [ + { + "name": "path", + "targets": [ + [ + 0, + 1 + ], + [ + 1, + 2 + ], + [ + 2, + 3 + ] + ], + "automorphisms": [ + "0123" + ], + "cuts": [ + { + "patterns": [ + "0123", + "0132", + "0312", + "0321", + "1203", + "1230", + "2013", + "2031", + "2301", + "2310", + "3102", + "3120" + ], + "weight": "1/18" + } + ], + "lower_bound": "25/3", + "minimum": 9 + }, + { + "name": "star", + "targets": [ + [ + 0, + 1 + ], + [ + 0, + 2 + ], + [ + 0, + 3 + ] + ], + "automorphisms": [ + "0123", + "0132", + "0213", + "0231", + "0312", + "0321" + ], + "cuts": [ + { + "patterns": [ + "0213", + "0231", + "0312", + "1032", + "1320", + "2013", + "2103", + "2130", + "2301", + "3012", + "3102", + "3120" + ], + "weight": "1/56" + }, + { + "patterns": [ + "0123", + "0213", + "0231", + "1023", + "1230", + "1302", + "2130", + "2301", + "2310", + "3012", + "3021", + "3102" + ], + "weight": "3/70" + } + ], + "lower_bound": "57/7", + "minimum": 9 + } + ] +} diff --git a/research/swap-path-star-certificate/README.md b/research/swap-path-star-certificate/README.md new file mode 100644 index 0000000000..410981e640 --- /dev/null +++ b/research/swap-path-star-certificate/README.md @@ -0,0 +1,176 @@ +# Exact nine-call certificates for a transposition path and star + +**Scoped formal-model proof; no new kappa.** Three target registers carrying +swaps `(01),(12),(23)`, or swaps `(01),(02),(03)`, require exactly **nine** +paid coordinate-CNOT calls. The theorem holds for every address dimension +`n>=4` and every register count `R>=3`, with arbitrary restored dirty +registers and free scalar register mixing. + +[PR #4968](https://github.com/CrocSwap/integer-mult-bounds/pull/4968) +reported numerical order-pattern bounds near 8.33 and 8.14 and a nine-call +path word. Its scratch LP certificates were not in the package. This +contribution supplies exact rational certificates and the uniform implication. +The bounds are **25/3** and **57/7**. Each exceeds eight. The result does +not claim a new numerical observation or an optimum over all cut methods. +The selected kappa remains `60403/20000000`. + +## Formal contract + +Let `G=GL_n(F2)`. Work in `M_R(F2[G])`, the formal group algebra. +A paid call is `I+([g]+1)N`, where `g` is one coordinate CNOT and `N` is a +scalar rank-one idempotent. Each such call costs one. Free `GL_R(F2)` +register maps are allowed. The target is diagonal, with the three specified +coordinate swaps on distinct registers and identity on every other register. +Every register input is arbitrary; extra registers must be restored. + +No native address representation, clean workspace, rank-two paid unit, +physical compiler, storage bill or recursive supplier is supplied here. +Natural-matrix equality is not substituted for a formal group-algebra identity. + +## Crossing-rank argument + +Use the left regular representation on `F2^G`. For a cut `A` in `G`, define + +```text +q_A(M) = rank_F2 M[A^c x registers, A x registers]. +out_A(g) = |{x in A : gx not in A}|. +``` + +Block multiplication and rank subadditivity give +`q_A(MN)<=q_A(M)+q_A(N)`. A free scalar register map has crossing rank zero. +A paid call has crossing block `P_g[A^c,A] tensor N`, hence crossing rank +`out_A(g)`, since the permutation submatrix has that rank and `rank(N)=1`. +The diagonal target has crossing rank equal to the sum of its three `out` +counts. These are formal-algebra consequences, valid for every `R`. +Positive weighted sums and averages of these inequalities remain valid. + +## Relative-order cuts + +Fix a total order on the nonzero binary vectors. For an invertible address +matrix `x`, record the relative order of its first four rows as a permutation +of `0123`. A subset `C` of the 24 patterns defines a cut in `G`. Now average +this cut inequality over every total order of the nonzero vectors. + +A CNOT writing one of these four rows replaces it by the sum of two +independent rows. This sum is nonzero and differs from all original rows. +Thus the four selected row vectors and the new vector have 120 equally +likely relative orders. This holds whether the read row is selected or is +an address spectator. A CNOT writing outside the four rows changes no pattern. +A target swap only relabels the four original rows, whose 24 orders are uniform. + +For pattern set `C`, define `g_i(C)` by counting transitions from `C` to its +complement when label `i` is deleted and inserted at one of four positions. +The unchanged position contributes zero. Define `h_ab(C)` by counting patterns +in `C` that leave `C` after labels `a,b` are exchanged. Then + +```text +average paid crossing, writing i = |G| g_i(C) / 120, +average target crossing, swap ab = |G| h_ab(C) / 24. +``` + +The first formula can also be checked by all 120 orders of five labels: +remove the new label for the input; remove the old row and rename the new +label for the output. Each changed insertion occurs once. The two positions +that give the unchanged pattern contribute zero. The verifier uses both +counting methods and compares them exactly. + +Consequently, positive cut weights with each weighted `g_i` at most one +prove the paid-call lower bound `5 sum_C weight(C) sum_targets h(C)`. +All cut sets and weights are explicit in [CUTS.json](CUTS.json). + +## The two certificates + +Each base cut has twelve patterns. The exact counts are: + +| Cut | Write counts g_0,g_1,g_2,g_3 | Sum of target h counts | Weight | +| --- | --- | --- | --- | +| Path P | 18,18,18,18 | 30 | 1/18 | +| Star A | 8,24,24,24 | 24 | 1/56 | +| Star B | 20,0,20,20 | 28 | 3/70 | + +The path cut already has equal paid loads. Its weighted target count is +`5*30/18=25/3`. + +For each star cut, average over the six permutations of the three leaf +labels `123`, with label zero fixed. This preserves the target sum and +makes each leaf load equal to the mean of its three base counts. The +weighted center load and each weighted leaf load are respectively + +```text +8/56 + 20*(3/70) = 1, +24/56 + (40/3)*(3/70) = 1. +``` + +The weighted target bound is +`5*(24/56 + 28*(3/70))=57/7`. +The verifier checks the sets, all relabelings, both count methods and all +four exact rational paid loads. The certificate has no numerical tolerance. +Neither certificate is claimed optimal within its cut family. + +The number of calls is an integer, so both lower bounds imply at least nine. +For the upper bound, implement each swap on its own register by +`CNOT(a,b), CNOT(b,a), CNOT(a,b)`. Each register entry stays a single formal +group basis element. Their product is the required swap; all other entries +are identity or zero. Thus nine calls suffice in the full formal algebra. +This proves the theorem, including arbitrary extra dirty registers and +address spectators. + +## Verification and reproduction + +Use CPython 3.12 and the standard library: + +```sh +python3.12 -B scripts/research_package.py --package research/swap-path-star-certificate +python3.12 -I -W error -O -B research/swap-path-star-certificate/verify.py +``` + +Expected markers: `PASS_REGISTERED_RESEARCH_PACKAGE` and +`PASS_SWAP_PATH_STAR_CERTIFICATE path=9 star=9 no_new_kappa`. +The normal and optimized commands recompute [RESULT.json](RESULT.json). +`--emit-receipt` emits JSON to standard output for explicit regeneration. +Normal replay writes no files and needs neither Git nor network. + +The checks cover the three base cuts, all required symmetry images, all +120 five-item orders per image, twelve formal diagonal endpoints across +`n=4,5,6` and `R=3,5`, and 108 single-call omissions. Eight certificate +controls reject changed weights, a claimed bound of nine, a wrong symmetry +orbit and an invalid pattern. The receipt binds all six source files. +The endpoint calculation uses group labels only because these particular +attaining words remain diagonal monomials; the lower bound concerns all +allowed formal words, including scalar register mixing. + +A disposable exhaustive pattern search found the certificates. No search, +C++ compiler or LP solver is needed for verification. The proof uses their +explicit counts, not search completeness or a floating point optimum. + +## Limits + +This gives exact cost for one path or star with three target registers. +It does not prove `3t` for every connected target graph, or for repeated +batches on the same four coordinates. The argument is a scoped formal-model +screen, not a native construction, a full multiplier theorem or a kappa gain. +Independent human and proof-kernel review remain open. No selected cold +replay or larger formal-word census is required or claimed. + +## Open next questions + +Can repeated path or star batches on the same four coordinates share calls? +The scaled lower bounds need not round to nine per batch. Compare a bounded +multi-batch formal word with those bounds before seeking a general additive +claim. This package has no repeated-batch optimum or construction search. + +## Credit and provenance + +Prepared for Ali Romman with substantial OpenAI Codex assistance. +New work is Apache-2.0. James Reed supplied the component-cut proof, the +numerical path/star observations and the path upper word in +[PR #4968](https://github.com/CrocSwap/integer-mult-bounds/pull/4968), and +the all-order spectator method in +[PR #4950](https://github.com/CrocSwap/integer-mult-bounds/pull/4950). +Mihir Srivastava supplied the spectator-model statement in +[PR #4939](https://github.com/CrocSwap/integer-mult-bounds/pull/4939). +Their retained notices credit Ross Richardson, commdata2338, Gareth Davidson +and the earlier register-model/cut contributors. No predecessor code is +imported. Source documents are provenance only and are pinned in +[SOURCES.json](SOURCES.json). Base: +`f259dabc7d70e0db8d6d36bfda888f008bbfecc1`, priority revision 7. diff --git a/research/swap-path-star-certificate/RESULT.json b/research/swap-path-star-certificate/RESULT.json new file mode 100644 index 0000000000..f0a7c558aa --- /dev/null +++ b/research/swap-path-star-certificate/RESULT.json @@ -0,0 +1,79 @@ +{ + "call_omission_controls": 108, + "cases": [ + { + "cuts": [ + { + "patterns": 12, + "target_count": 30, + "weight": "1/18", + "write_counts": [ + 18, + 18, + 18, + 18 + ] + } + ], + "loads": [ + "1", + "1", + "1", + "1" + ], + "lower_bound": "25/3", + "minimum": 9, + "name": "path", + "orbit_size": 1 + }, + { + "cuts": [ + { + "patterns": 12, + "target_count": 24, + "weight": "1/56", + "write_counts": [ + 8, + 24, + 24, + 24 + ] + }, + { + "patterns": 12, + "target_count": 28, + "weight": "3/70", + "write_counts": [ + 20, + 0, + 20, + 20 + ] + } + ], + "loads": [ + "1", + "1", + "1", + "1" + ], + "lower_bound": "57/7", + "minimum": 9, + "name": "star", + "orbit_size": 6 + } + ], + "certificate_controls": 8, + "formal_diagonal_endpoints": 12, + "no_new_kappa": true, + "relative_orders_per_orbit_cut": 120, + "schema": "swap-path-star-result/v1", + "source_sha256": { + "CUTS.json": "7683dd39797163b35b89b2faf694c5f2b6c9bacad4fab646d4691cf29788606b", + "README.md": "e1350a2373bf31c7a4c876bde2a8d2b74076628b339bcf9a5b80b37600d4c203", + "SOURCES.json": "ae85cc57a3d9455c633a3a6a8b6836fd92a04502bf38c13484f6c24cd95082cb", + "TASK.json": "b540b70cc3be94bd2abe68fac6c029b2e75a464c4dcfec1246176ef0422879ae", + "VERIFY.json": "0943abd3e0271ac81ebad6a433d6c465d65b8b7a6c777595a2ca9251154c4b27", + "verify.py": "41914ab0328a8df37d9930dd03312d3e9245cb36528464f9e87e14c000bec739" + } +} diff --git a/research/swap-path-star-certificate/SOURCES.json b/research/swap-path-star-certificate/SOURCES.json new file mode 100644 index 0000000000..7e3470b907 --- /dev/null +++ b/research/swap-path-star-certificate/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "f259dabc7d70e0db8d6d36bfda888f008bbfecc1", + "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/swap-component-cut/README.md", + "usage": "provenance", + "git_blob": "19eaadc4ea40e312d202c917e2f1914d98ca224a", + "sha256": "7fe7efcb948a71af664d8f7828c8f4a056de3c6c3aa2cb82e420ec6ae7bd0106" + }, + { + "path": "research/swap-row-order-cut/README.md", + "usage": "provenance", + "git_blob": "941c1eb4f2301023757c45bbe1bb767962065cd1", + "sha256": "a5e9661f5ffa504cafee1c9481f0a1072b98341f98a031a2b4d18bb8c4a9ef7c" + } + ] +} diff --git a/research/swap-path-star-certificate/TASK.json b/research/swap-path-star-certificate/TASK.json new file mode 100644 index 0000000000..1f18b14668 --- /dev/null +++ b/research/swap-path-star-certificate/TASK.json @@ -0,0 +1,87 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 7, + "base_commit": "f259dabc7d70e0db8d6d36bfda888f008bbfecc1", + "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_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read Model section 1 of the three-register bound and identify the exact excluded free operations.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "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": "Exact order-pattern cut certificates prove nine calls for one three-edge coordinate-transposition path or star, for every n>=4 and R>=3.", + "scope_change_reason": "Certify the scratch path/star observations and answer the associated multi-target handoff in PR4968; no new native construction.", + "bottleneck_link": "Exclude an eight-call formal word for two specific mixed target sets with arbitrary restored dirty registers and address spectators.", + "budget_minutes": 60, + "stop_rule": "Stop at explicit rational cut certificates, the uniform proof, attaining words and bounded checks. No general cut optimum, repeated-batch additivity or native search.", + "outcome": "completed", + "evidence": "Two finite cut certificates, independent five-item order counts, exact rational tariff sums and nine-call formal diagonal endpoints with omission controls.", + "author": "Ali Romman", + "ai_assistance": "Substantial OpenAI Codex assistance for proof, finite search, code, verification and publication. No independent human or proof-kernel review.", + "open_questions": [ + { + "question": "Can repeated path or star batches share calls?", + "why_it_matters": "The integer rounding used for one three-target batch does not prove additivity for repeated batches.", + "first_step": "Compare the scaled fractional lower bounds with an explicit multi-batch formal word.", + "blocked_by": "No repeated-batch optimality is established." + } + ], + "selection": { + "mode": "handoff-first", + "source_pr": 4968, + "source_head": "e7d050e79a6a55ecdd1706ee2855a3f3585c11e7", + "handoff": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19138026" + }, + "overlap": { + "searched_at": "2026-10-23T06:21:23.436659+00:00", + "open_prs": { + "fetched_at": "2026-10-23T06:20:22.879886+00:00", + "complete_pagination": true, + "records": 304 + }, + "discussions": { + "fetched_at": "2026-10-23T06:21:23.317485+00:00", + "complete_pagination": true, + "records": 4112 + }, + "local_notes": 76, + "total_local_notes": 6710, + "limits": "Sparse omitted notes, arbitrary diffs and unpublished work." + }, + "canonical_discussion": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1317#discussioncomment-19139461" +} diff --git a/research/swap-path-star-certificate/VERIFY.json b/research/swap-path-star-certificate/VERIFY.json new file mode 100644 index 0000000000..0e3bac85f3 --- /dev/null +++ b/research/swap-path-star-certificate/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": 30, + "checks": "Exact cut certificates, independent five-item counts, formal diagonal words and controls." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 30, + "checks": "The same checks with Python assertions disabled." + } + ] +} diff --git a/research/swap-path-star-certificate/verify.py b/research/swap-path-star-certificate/verify.py new file mode 100644 index 0000000000..3836379711 --- /dev/null +++ b/research/swap-path-star-certificate/verify.py @@ -0,0 +1,165 @@ +#!/usr/bin/env python3 +"""Check two exact cut certificates. Ali Romman with Codex assistance. + +Apache-2.0. No predecessor code or numerical solver is used. +""" +from fractions import Fraction as F +from itertools import permutations +from pathlib import Path +import hashlib +import json +import sys + +ORDERS = tuple(permutations(range(4))) + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def pattern(text): + require(type(text) is str and len(text) == 4 and set(text) == set('0123'), + 'invalid pattern') + return tuple(map(int, text)) + + +def relabel(order, mapping): + return tuple(mapping[x] for x in order) + + +def transposition(a, b): + return tuple(b if x == a else a if x == b else x for x in range(4)) + + +def counts(cut): + writes = [] + for row in range(4): + total = 0 + for order in cut: + tail = tuple(x for x in order if x != row) + total += sum(tail[:k] + (row,) + tail[k:] not in cut for k in range(4)) + writes.append(total) + swaps = {f'{a}{b}': sum(relabel(order, transposition(a, b)) not in cut for order in cut) + for a in range(4) for b in range(a+1, 4)} + return writes, swaps + + +def independent_counts(cut): + # The new row vector has label 4. Count all 120 orders directly. + writes = [0] * 4 + for order in permutations(range(5)): + before = tuple(x for x in order if x != 4) + if before not in cut: + continue + for row in range(4): + after = tuple(row if x == 4 else x for x in order if x != row) + writes[row] += after not in cut + return writes + + +def certificate(case): + targets = [tuple(edge) for edge in case['targets']] + expected_targets = {'path': [(0,1),(1,2),(2,3)], 'star': [(0,1),(0,2),(0,3)]} + require(targets == expected_targets[case['name']], 'wrong target graph') + maps = tuple(pattern(s) for s in case['automorphisms']) + required_maps = (tuple(permutations((1,2,3))) if case['name'] == 'star' else None) + expected_maps = {(0,)+p for p in required_maps} if required_maps else {(0,1,2,3)} + require(set(maps) == expected_maps and len(set(maps)) == len(maps), 'wrong symmetry orbit') + loads = [F(0)] * 4 + target = F(0) + rows = [] + for entry in case['cuts']: + base = {pattern(s) for s in entry['patterns']} + require(len(base) == len(entry['patterns']) and 0 < len(base) < 24, 'invalid cut') + weight = F(entry['weight']) + require(weight > 0, 'nonpositive cut weight') + raw, raw_swaps = counts(base) + require(raw == independent_counts(base), 'reinsertion count differs') + for mapping in maps: + require({tuple(sorted((mapping[a],mapping[b]))) for a,b in targets} + == set(targets), 'mapping changes target graph') + cut = {relabel(o, mapping) for o in base} + paid, swaps = counts(cut) + require(paid == independent_counts(cut), 'orbit count differs') + for j in range(4): + loads[j] += weight * paid[j] / len(maps) + target += 5 * weight * sum(swaps[f'{a}{b}'] for a,b in targets) / len(maps) + rows.append({'patterns': len(base), 'write_counts': raw, + 'target_count': sum(raw_swaps[f'{a}{b}'] for a,b in targets), + 'weight': str(weight)}) + require(loads == [F(1)] * 4, 'paid load is not one') + require(target == F(case['lower_bound']) and 8 < target <= 9, 'lower bound differs') + require(type(case['minimum']) is int and case['minimum'] == 9, 'wrong minimum') + return {'name': case['name'], 'cuts': rows, 'loads': list(map(str,loads)), + 'lower_bound': str(target), 'minimum': 9, 'orbit_size': len(maps)} + + +def word_check(edges, n, registers, omitted=None): + # Each register entry remains one formal group basis element. + state = [[1 << i for i in range(n)] for _ in range(registers)] + gates = [(r,i,j) for r,(a,b) in enumerate(edges) for i,j in ((a,b),(b,a),(a,b))] + for index,(r,i,j) in enumerate(gates): + if index != omitted: + state[r][i] ^= state[r][j] + expected = [[1 << i for i in range(n)] for _ in range(registers)] + for r,(a,b) in enumerate(edges): + expected[r][a], expected[r][b] = expected[r][b], expected[r][a] + return state == expected + + +def controls(cases): + rejected = 0 + for case in cases: + mutations = [] + wrong = json.loads(json.dumps(case));wrong['cuts'][0]['weight'] = str(2*F(wrong['cuts'][0]['weight']));mutations.append(wrong) + wrong = json.loads(json.dumps(case));wrong['lower_bound'] = '9';mutations.append(wrong) + wrong = json.loads(json.dumps(case));wrong['automorphisms'] = ['1023'];mutations.append(wrong) + wrong = json.loads(json.dumps(case));wrong['cuts'][0]['patterns'][0] = '0000';mutations.append(wrong) + for wrong in mutations: + try: + certificate(wrong) + except ValueError: + rejected += 1 + else: + raise ValueError('invalid certificate accepted') + return rejected + + +def evidence(): + here = Path(__file__).resolve().parent + supplied = json.loads((here/'CUTS.json').read_text(encoding='utf-8')) + require(supplied['schema'] == 'swap-path-star-certificate/v1', 'schema differs') + cases = supplied['cases'] + require([c['name'] for c in cases] == ['path','star'], 'case inventory differs') + rows = [certificate(c) for c in cases] + endpoints = omissions = 0 + for case in cases: + for n in (4,5,6): + for registers in (3,5): + require(word_check(case['targets'],n,registers), 'nine-call endpoint differs') + endpoints += 1 + for omit in range(9): + require(not word_check(case['targets'],n,registers,omit), 'call omission accepted') + omissions += 1 + result = {'schema':'swap-path-star-result/v1', 'cases':rows, 'formal_diagonal_endpoints':endpoints, + 'call_omission_controls':omissions, 'certificate_controls':controls(cases), + 'relative_orders_per_orbit_cut':120, 'no_new_kappa':True} + result['source_sha256'] = {name:hashlib.sha256((here/name).read_bytes()).hexdigest() + for name in ('README.md','CUTS.json','verify.py','TASK.json','VERIFY.json','SOURCES.json')} + return result + + +def main(): + encoded = json.dumps(evidence(),indent=2,sort_keys=True)+'\n' + if sys.argv[1:] == ['--emit-receipt']: + print(encoded,end='') + else: + require(not sys.argv[1:], 'unexpected argument') + require(Path(__file__).with_name('RESULT.json').read_text(encoding='utf-8') == encoded, + 'receipt differs') + print('PASS_SWAP_PATH_STAR_CERTIFICATE path=9 star=9 no_new_kappa') + + +if __name__ == '__main__': + main()