From e2bec73e3f50e3b4e57a7a466eba2a3264d313ed Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Fri, 30 Oct 2026 18:17:22 +0000 Subject: [PATCH] feat(research): prove selected MOVE frame-phase obstruction --- .../move-frame-phase-obstruction/PROOF.md | 126 ++++++++++++++ .../move-frame-phase-obstruction/README.md | 84 +++++++++ .../move-frame-phase-obstruction/SOURCES.json | 36 ++++ .../move-frame-phase-obstruction/TASK.json | 83 +++++++++ .../move-frame-phase-obstruction/VERIFY.json | 38 +++++ .../move-frame-phase-obstruction/verify.py | 161 ++++++++++++++++++ 6 files changed, 528 insertions(+) create mode 100644 research/move-frame-phase-obstruction/PROOF.md create mode 100644 research/move-frame-phase-obstruction/README.md create mode 100644 research/move-frame-phase-obstruction/SOURCES.json create mode 100644 research/move-frame-phase-obstruction/TASK.json create mode 100644 research/move-frame-phase-obstruction/VERIFY.json create mode 100644 research/move-frame-phase-obstruction/verify.py diff --git a/research/move-frame-phase-obstruction/PROOF.md b/research/move-frame-phase-obstruction/PROOF.md new file mode 100644 index 0000000000..472b07707f --- /dev/null +++ b/research/move-frame-phase-obstruction/PROOF.md @@ -0,0 +1,126 @@ +# A three-edge obstruction to scalar frame rephasing + +This scoped proof and its exact finite certificate were produced by Nick Petalas. + +## Definitions and source + +The fixed input is the selected PR6030 word, SHA256 +`7834725d9e34ee846a9ccc615221ea81e0201613938afa185d2eda0c9a6c232f`, +at canonical main `2485805a6d47f36ea83ddde6327d453ac82d44dc`. +The retained `clifford_exact.py` constructs a unitary chart `C_a` for frame `a`. +Use ordinary matrix composition, with the rightmost matrix acting first. +The source expression `chart(a).adjoint().then(chart(b))` applies `C_a†` +first, then `C_b`, so its matrix is + + T_ab = C_b C_a†. + +The source native normal form expresses `T_ab = i^(p_ab) S_ab`, where +`p_ab` is the sum modulo four of its literal `phase` gates and `S_ab` is +that same recipe with only those gates deleted. This definition fixes every +permutation, quadratic phase, translation and Gaussian gate in `S_ab`. +It does not identify all possible recipes for an operator. + +Three used frames and three actual MOVE occurrences suffice. Indices are +zero-based, as in the JSON program. + +| Frame | Binary basis | +|---|---| +| 3 | empty | +| 2 | 35 | +| 299 | 35, 75, 400 | + +| Directed edge | Event index | Public role | Child rank | `p_ab` | +|---|---:|---:|---:|---:| +| 3 to 2 | 10338 | 259 | 1 | 1 | +| 2 to 299 | 10403 | 258 | 2 | 1 | +| 3 to 299 | 14360 | 465 | 3 | 1 | + +The events are on different roles. The theorem concerns one chart choice shared +by every occurrence of a frame. It does not assert a chronological three-event +subroutine or an actual closed walk by one role. + +## The scalar gauge theorem + +For each positive integer column multiplicity `f`, permit a separate arbitrary +unit-modulus scalar `lambda_a(f)` for each frame and replace its tensor chart by + + C'_a(f) = lambda_a(f) C_a^(tensor f). + +There exists such a frame gauge making every selected MOVE equal to its fixed +phase-deleted recipe `S_ab^(tensor f)` if and only if `4` divides `f`. +In particular, no width-one frame gauge removes all these literal phase tags. +This permits width-dependent gauges and arbitrary complex unit phases, not only +fourth roots of unity. + +**Proof.** Under a frame gauge the MOVE becomes + + T'_ab(f) = lambda_b(f) conjugate(lambda_a(f)) + i^(f p_ab) S_ab^(tensor f). + +Since `S_ab` is invertible, equality with its phase-deleted tensor recipe requires + + lambda_b(f) / lambda_a(f) = i^(-f p_ab). + +For the edges `3 to 2` and `2 to 299`, the product of the required ratios is +`i^(-2f)`. The direct edge `3 to 299` requires the same ratio to be `i^(-f)`. +Consequently `i^f = 1`, which holds exactly when `4` divides `f`. +Conversely, every literal phase gate in the retained native alphabet has an +integer exponent modulo four. If `4` divides `f`, all its tensor scalar factors +are one; the trivial gauge therefore works for every selected MOVE, without +needing a census of the remaining edges. This proves both directions. ∎ + +The argument is the classical cycle criterion for scalar edge potentials. +The new source-specific content is the three used edges with cycle residue +`p_32 + p_2,299 - p_3,299 = 1 mod 4`, and the resulting exact width criterion. + +## Operator certificate and sharpness on the triangle + +Chart cancellation gives + + T_2,299 T_3,2 = T_3,299. + +Substituting the three measured phases gives + + S_3,299† S_2,299 S_3,2 = -i I. + +The verifier checks the full-phase loop is `I` and the phase-deleted loop is +`-i I` on every one of the 512 coordinate basis vectors, using exact Gaussian +integer numerators and powers of two as denominators. Tensoring the identity +shows that the phase-deleted loop at width `f` is `(-i)^f I`. + +At width one, one residual tag among these three is necessary and sufficient. +Set `q_3=0`, `q_2=3`, `q_299=2`, with `lambda_a=i^(q_a)`. The path edges then +have zero residual phase and the direct edge has residue `3`. This attains the +one-tag minimum on this triangle only. No global minimum tag count is claimed. + +As controls, enumerating the 64 fourth-root vertex assignments gives no +solution at widths 1, 2 or 3, and four solutions at width 4. Replacing the direct +edge's phase by 2 gives four width-one solutions. Deleting the direct constraint +leaves the expected four tree solutions. Wrong loop phase and reversed sign +are rejected. These finite controls corroborate the proof, including its sign; +they are not the argument for arbitrary `f` or arbitrary unit phases. + +## Scope and predecessors + +Unpaidmoon / PR6293 identifies the selected tensor-phase scaling question and +reports the full phase census. That census is cited, not replayed or adopted as +this result. The three-edge witness here is independently compiled to establish +a new gauge obstruction. DLamdata / PR5894 records existing absolute-phase +coverage; this proof asserts no missing source check. Mark / Matarener's +PR5974 and PR5442 supply earlier all-width lift work. + +DreamingOfClouds supplied PR6030's selected word, building on PR5907, PR5827, +Ali Romman's PR5599 and their retained P104 lineage. Chafik Boukhalfa's native +channel retains the exact compiler through icekylinx's frame-sa504 package and +the independent Gaussian interpreter from Ali Romman's PR1862 and PR1931. +Rohan Arun / PR1972, Adam Gall / PR1940, Josie Elliston / PR1071, Ali Romman / +PR1125 and the retained decoder/native sources keep their original credit. +All input files remain unchanged. Apache-2.0. + +The obstruction fixes the extracted native normal forms. A different +factorization can move a scalar into other gates. Role-specific or +history-dependent charts can also change the constraint graph. No lower bound +for those mechanisms follows. No physical scalar cost, changed paid profile, +new kappa, supplier failure, selected-frontier change or complete multiplication +theorem is claimed. All five selected framework assumptions remain. +Independent human and formal proof-kernel review are unclaimed. diff --git a/research/move-frame-phase-obstruction/README.md b/research/move-frame-phase-obstruction/README.md new file mode 100644 index 0000000000..ccc7fa09d9 --- /dev/null +++ b/research/move-frame-phase-obstruction/README.md @@ -0,0 +1,84 @@ +# Selected MOVE phases cannot all be removed by frame rephasing + +A scoped proof with an exact finite certificate, produced by Nick Petalas. + +On the selected PR6030 word, the native recipes for `3 to 2`, `2 to 299` and +`3 to 299` each contain total explicit phase `i`. Their cycle residue is one +modulo four. Scalar changes to the frame charts cancel around this triangle, +so they cannot remove every explicit phase. At column multiplicity `f`, even +arbitrary width-dependent unit-complex frame gauges succeed for every selected +MOVE exactly when `4` divides `f`. The phase-deleted triangle loop is `-i I` at +width one. One residual tag is necessary and sufficient on that triangle. + +This answers a new changed-chart question prompted by unpaidmoon / PR6293, +without repeating its full phase census. It closes the particular remedy of +removing tensor-phase bookkeeping by one scalar gauge per frame. Keeping the +correct phases already works; no source correctness failure is asserted. +The [proof](PROOF.md) fixes the normal forms and gives the all-width argument. + +## Evidence and reproduction + +From the repository root, using CPython 3.12 and the standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/move-frame-phase-obstruction/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/move-frame-phase-obstruction/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/move-frame-phase-obstruction +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/move-frame-phase-obstruction --check-source-history +``` + +Another CPython 3.12 interpreter may replace that local path. The direct verifier +also works from a source export without Git. Expected markers are +`PASS_MOVE_FRAME_PHASE_OBSTRUCTION`, `PASS_REGISTERED_RESEARCH_PACKAGE` and +`PASS_RESEARCH_COMMIT_BYTES`. + +The verifier authenticates all three live sources, binds the named frames and +actual event indices, and compiles only the three witness edges. The separate +Gaussian interpreter checks their signed Pauli actions and absolute phases. +Both the full and phase-deleted loops are checked on all 512 basis states. +The 64 fourth-root gauge assignments are enumerated at each width 1 through 4. +Compatible-triangle, tree, restored-loop, wrong-phase, reversed-sign and changed +source-byte controls run in both normal and optimized Python. Output includes +a generated receipt binding the package and live input hashes. It writes no +files. Hosted CI status is recorded separately in the PR body. + +## Limitations + +The theorem fixes the recipes with literal `phase` gates removed. It does not +cover refactoring their other gates or using distinct charts by role or history. +The three edges occur on different roles; the diagnostic loop is an operator +identity, not a chronological subroutine. No whole-word native replay, selected +cold replay, physical caller, all-size implementation, Lean or Docker was run. +No new kappa or complete multiplication theorem is claimed. All five selected +framework assumptions remain. Independent human and formal proof-kernel review +are unclaimed. + +The verifier uses bounded source sizes, three nine-axis charts, 512 basis +states and 64 gauge assignments per tested width. Python and the frozen exact +interpreters allocate dynamically; these finite bounds replace a fixed-memory +implementation. Dynamic module loading is restricted to two authenticated +files. Frozen source style and its internal assertions are retained, while new +acceptance checks use exceptions and remain enabled under `-O`. No external +static analyzer was available; warning-strict execution and the registered +checks are the available diagnostics. + +## Open next questions + +Can role-specific phase charts eliminate tags while preserving every actual +common-chart ADD and COPY relation and the endpoint normalizers? Start with +these three occurrences and add the real scalar-gate compatibility constraints. +The obstruction here requires one shared phase per frame, so that larger graph +and its physical scalar bill remain open. Do not treat missing compatibility or +restoration charges as zero. + +## Credit + +The witness and gauge application were produced by Nick Petalas. The cycle +criterion and tensor-product scalar identity are classical. Credit unpaidmoon / +PR6293 for the selected tensor-phase question; DLamdata / PR5894 for existing +absolute-phase coverage; Mark / Matarener's PR5974 and PR5442 for earlier lift +work; DreamingOfClouds / PR6030 and the retained PR5907/5827/5599 word lineage; +Chafik Boukhalfa's native channel; icekylinx's retained exact compiler; and Ali +Romman's independent Gaussian interpreter from PR1862/1931. Further retained +P104 credit is in [PROOF.md](PROOF.md) and the unchanged source packages. +Apache-2.0. diff --git a/research/move-frame-phase-obstruction/SOURCES.json b/research/move-frame-phase-obstruction/SOURCES.json new file mode 100644 index 0000000000..d29fdc5ec1 --- /dev/null +++ b/research/move-frame-phase-obstruction/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/p104-helper470-twin-rung-removal/WORD.json.gz", + "usage": "input", + "git_blob": "22f9ab02d1b73ea0aa4b07ce445a14cc2602c760", + "sha256": "7834725d9e34ee846a9ccc615221ea81e0201613938afa185d2eda0c9a6c232f" + }, + { + "path": "research/p104-native-channel/vendor/clifford_exact.py", + "usage": "input", + "git_blob": "166841a037f069249f6f7f6dedb89248812f59e2", + "sha256": "2982ead07721e83358dc67c6f49c2b4c16a236a6bebdfd72f58221be1f5d0962" + }, + { + "path": "research/p104-native-channel/vendor/native_verify.py", + "usage": "input", + "git_blob": "2c209dfa9cfade3bc20ac5fc9d876b433a147f8c", + "sha256": "3049471905b47b385c88378a1a3be7a18b8858aadd035b8a6da2f4a03b470f38" + } + ] +} diff --git a/research/move-frame-phase-obstruction/TASK.json b/research/move-frame-phase-obstruction/TASK.json new file mode 100644 index 0000000000..4f564fb6cd --- /dev/null +++ b/research/move-frame-phase-obstruction/TASK.json @@ -0,0 +1,83 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 8, + "base_commit": "2485805a6d47f36ea83ddde6327d453ac82d44dc", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Can one of the selected record's five inherited assumptions be proved at its actual caller?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Choose one assumption ID (native_all_columns, owned_erasure, compiler, precision_tape, analytic_recovery), one quantified implication and exact dependency closure. Check current handoffs, including #5625 row reentry and #5707 root-prefix lowering, without treating their partial scope as the whole theorem. Prove or falsify that implication with a caller-bound argument; stop at the chosen obligation. Finite tests or root digits do not discharge an all-size statement.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "native_all_columns", + "owned_erasure", + "compiler", + "precision_tape", + "analytic_recovery" + ], + "existing_checks": [ + { + "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "refined", + "actual_scope": "Prove or refute scalar frame gauges that erase the fixed native MOVE phase tags on the selected PR6030 word, at every column multiplicity.", + "scope_change_reason": "Choose native_all_columns and allow a scalar chart phase per frame. The new result is a three-edge obstruction, not a repeat of the predecessor phase census or a discharge of the assumption.", + "bottleneck_link": "A frame gauge cannot remove the tensor-phase bookkeeping for all widths; a future native implementation must retain those factors or change its normal forms or compatibility contract.", + "budget_minutes": 60, + "stop_rule": "Stop after one exact cycle obstruction or a consistent frame potential; package the first verified result.", + "outcome": "partial", + "evidence": "PROOF.md and verify.py: cycle residue 1, ranks 1/2/3, exact -i I loop on 512 basis states, and the iff 4 divides f proof.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can role-specific phase charts eliminate tags while preserving all actual scalar-gate and endpoint compatibility?", + "why_it_matters": "That changes the shared-frame premise of this obstruction and may simplify native phase handling.", + "first_step": "Add actual ADD/COPY phase equalities around the three witness occurrences and retain boundary normalizers.", + "blocked_by": "No complete role/history compatibility graph or physical scalar bill is supplied." + } + ] +} diff --git a/research/move-frame-phase-obstruction/VERIFY.json b/research/move-frame-phase-obstruction/VERIFY.json new file mode 100644 index 0000000000..2c453ba18e --- /dev/null +++ b/research/move-frame-phase-obstruction/VERIFY.json @@ -0,0 +1,38 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/p104-helper470-twin-rung-removal/WORD.json.gz", + "research/p104-native-channel/vendor/clifford_exact.py", + "research/p104-native-channel/vendor/native_verify.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Authenticate sources; compile three edges; check every basis vector of both loops; finite gauge and fault controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Repeat all scientific acceptance and fault controls with Python assertions disabled." + } + ] +} diff --git a/research/move-frame-phase-obstruction/verify.py b/research/move-frame-phase-obstruction/verify.py new file mode 100644 index 0000000000..184bd88a55 --- /dev/null +++ b/research/move-frame-phase-obstruction/verify.py @@ -0,0 +1,161 @@ +#!/usr/bin/env python3 +"""Check the selected three-edge scalar-phase obstruction with exact arithmetic.""" + +from hashlib import sha256 +import gzip +import importlib.util +import itertools +import json +from pathlib import Path +import sys +import time + +ROOT = Path(__file__).resolve().parents[2] +PACKAGE = Path(__file__).resolve().parent +WORD = "research/p104-helper470-twin-rung-removal/WORD.json.gz" +CLIFFORD = "research/p104-native-channel/vendor/clifford_exact.py" +NATIVE = "research/p104-native-channel/vendor/native_verify.py" +INPUT_SHA256 = { + WORD: "7834725d9e34ee846a9ccc615221ea81e0201613938afa185d2eda0c9a6c232f", + CLIFFORD: "2982ead07721e83358dc67c6f49c2b4c16a236a6bebdfd72f58221be1f5d0962", + NATIVE: "3049471905b47b385c88378a1a3be7a18b8858aadd035b8a6da2f4a03b470f38", +} +FRAMES = {3: (), 2: (35,), 299: (35, 75, 400)} +EDGES = ((3, 2), (2, 299), (3, 299)) +EVENTS = (10338, 10403, 14360) + + +def need(condition, label): + if not condition: + raise ValueError(label) + + +def authenticate(raw, expected, label): + need(sha256(raw).hexdigest() == expected, label + " source bytes") + + +def reject(operation, label): + try: + operation() + except ValueError: + return + raise ValueError(label + " was accepted") + + +def load(relative, name): + spec = importlib.util.spec_from_file_location(name, ROOT / relative) + need(spec is not None and spec.loader is not None, "Module loader") + module = importlib.util.module_from_spec(spec) + sys.modules[name] = module + spec.loader.exec_module(module) + return module + + +def sources(): + manifest = json.loads((PACKAGE / "SOURCES.json").read_text()) + pins = {row["path"]: row["sha256"] for row in manifest["files"] + if row["usage"] == "input"} + need(pins == INPUT_SHA256, "Declared live source pins") + payloads = {} + for relative, expected in INPUT_SHA256.items(): + raw = (ROOT / relative).read_bytes() + need(len(raw) <= 16 * 1024 * 1024, "Bounded source input") + authenticate(raw, expected, relative) + reject(lambda: authenticate(raw + b"\n", expected, relative), "Changed source") + payloads[relative] = raw + word = json.loads(gzip.decompress(payloads[WORD])) + need(word["schema"] == "p104-accumulated-block-composition/2", "Word schema") + need(len(word["frames"]) <= 4096 and len(word["program"]) <= 100000, "Word bounds") + for frame, basis in FRAMES.items(): + need(tuple(word["frames"][frame]) == basis, "Named frame basis") + for index, (a, b) in zip(EVENTS, EDGES): + event = word["program"][index] + need(event[0] == "MOVE" and event[2:5] == [a, b, False], "Selected MOVE occurrence") + return word + + +def compile_edges(word, clifford, native): + charts = {frame: clifford.canonical_frame(9, basis) for frame, basis in FRAMES.items()} + recipes, stripped, phases, ranks = [], [], [], [] + for a, b in EDGES: + operator = charts[a].adjoint().then(charts[b]) + record, _compiled = clifford.lower_child(operator) + recipe = native.recipe(record) + expected = native.adjoint(native.frame(tuple(word["frames"][a]), 9)) + expected += native.frame(tuple(word["frames"][b]), 9) + # This checker reconstructs signed Pauli action and the absolute phase. + native.equal(recipe, expected, "Triangle edge") + phase = sum(gate[1] for gate in recipe if gate[0] == "phase") % 4 + phases.append(phase) + ranks.append(record["rank"]) + recipes.append(recipe) + stripped.append(tuple(gate for gate in recipe if gate[0] != "phase")) + need(phases == [1, 1, 1] and ranks == [1, 2, 3], "Triangle phase and rank") + return recipes, stripped, phases, ranks + + +def gauge_solutions(phases, width): + need(len(phases) == 3 and 1 <= width <= 4, "Finite gauge control domain") + solutions = [] + # Variables are q(3), q(2), q(299), each in Z/4. + for q0, q1, q2 in itertools.product(range(4), repeat=3): + residuals = ((width * phases[0] + q1 - q0) % 4, + (width * phases[1] + q2 - q1) % 4, + (width * phases[2] + q2 - q0) % 4) + if residuals == (0, 0, 0): + solutions.append((q0, q1, q2)) + return solutions + + +def controls(phases): + counts = [len(gauge_solutions(phases, width)) for width in range(1, 5)] + need(counts == [0, 0, 0, 4], "Width residue controls") + need(len(gauge_solutions([1, 1, 2], 1)) == 4, "Compatible triangle control") + # On the two-edge tree every root phase determines one solution. + tree = [(q0, (q0 - 1) % 4, (q0 - 2) % 4) for q0 in range(4)] + need(len(tree) == 4 and all((b - a + 1) % 4 == (c - b + 1) % 4 == 0 + for a, b, c in tree), "Tree control") + return counts + + +def basis_checks(native, recipes, stripped): + full_loop = recipes[0] + recipes[1] + native.adjoint(recipes[2]) + bare_loop = stripped[0] + stripped[1] + native.adjoint(stripped[2]) + restored_loop = bare_loop + (("phase", 1),) + for address in range(512): + need(native.state(full_loop, address) == ({address: (1, 0)}, 0), "Exact chart loop") + need(native.state(bare_loop, address) == ({address: (0, -1)}, 0), "Phase-free loop is -i I") + need(native.state(restored_loop) == ({0: (1, 0)}, 0), "Restored loop control") + reject(lambda: need(native.state(bare_loop) == ({0: (1, 0)}, 0), "Wrong loop"), + "Deleting the needed phase") + reject(lambda: need(native.state(bare_loop) == ({0: (0, 1)}, 0), "Wrong sign"), + "Reversed holonomy sign") + + +def main(): + start = time.perf_counter() + word = sources() + clifford = load(CLIFFORD, "phase_obstruction_clifford") + native = load(NATIVE, "phase_obstruction_native") + recipes, stripped, phases, ranks = compile_edges(word, clifford, native) + counts = controls(phases) + basis_checks(native, recipes, stripped) + files = sorted(path for path in PACKAGE.iterdir() if path.is_file()) + receipt = { + "claim_type": "scoped proof with exact finite certificate", + "input_sha256": INPUT_SHA256, + "package_sha256": {path.name: sha256(path.read_bytes()).hexdigest() for path in files}, + "edges": EDGES, "event_indices_zero_based": EVENTS, + "ranks": ranks, "edge_phases_mod4": phases, + "cycle_phase_mod4": (phases[0] + phases[1] - phases[2]) % 4, + "stripped_loop_scalar": "-i", "basis_states": 512, + "z4_gauge_solution_counts_at_widths_1_through_4": counts, + "python": sys.version.split()[0], + "elapsed_seconds": round(time.perf_counter() - start, 6), + } + print(json.dumps(receipt, sort_keys=True)) + print("PASS_MOVE_FRAME_PHASE_OBSTRUCTION edges=3 basis_states=512 cycle_phase=1") + + +if __name__ == "__main__": + main()