From 764e7bd6d615d92019445bec92e2a473af021878 Mon Sep 17 00:00:00 2001 From: Cursor Agent Date: Tue, 27 Oct 2026 04:22:45 +0000 Subject: [PATCH] Prove the selected #5599 scalar instructions lift at every column multiplicity. The common-chart ADD, SCALE and COPY events of the helper-subspace word, including the 342 events added to the PR5565 word, act by an f-independent rational matrix. A chart difference of -I matches the width-free replay at even widths and misses it at odd widths. MOVE operators remain open. Prepared by unpaidmoon with substantial Cursor Grok assistance. Co-authored-by: unpaidmoon --- research/native-scalar-chart-lift/PROOF.md | 71 +++++ research/native-scalar-chart-lift/README.md | 50 +++ .../native-scalar-chart-lift/SOURCES.json | 30 ++ research/native-scalar-chart-lift/TASK.json | 83 +++++ research/native-scalar-chart-lift/VERIFY.json | 31 ++ research/native-scalar-chart-lift/verify.py | 287 ++++++++++++++++++ 6 files changed, 552 insertions(+) create mode 100644 research/native-scalar-chart-lift/PROOF.md create mode 100644 research/native-scalar-chart-lift/README.md create mode 100644 research/native-scalar-chart-lift/SOURCES.json create mode 100644 research/native-scalar-chart-lift/TASK.json create mode 100644 research/native-scalar-chart-lift/VERIFY.json create mode 100644 research/native-scalar-chart-lift/verify.py diff --git a/research/native-scalar-chart-lift/PROOF.md b/research/native-scalar-chart-lift/PROOF.md new file mode 100644 index 0000000000..af346b4f48 --- /dev/null +++ b/research/native-scalar-chart-lift/PROOF.md @@ -0,0 +1,71 @@ +# Scalar instructions of the selected word lift at every column multiplicity + +Prepared by unpaidmoon with substantial Cursor Grok assistance. Apache-2.0. +No new κ. Assumption ID: `native_all_columns`. This is one implication, not that assumption and not the other four. + +## 1. Proposition + +Let the selected word be `research/p104-helper-subspace-splits/WORD.json.gz` on canonical main `de5ec2e7a6074068452f45b1a191b5c72832df4a` (PR #5599, κ = 62009/20000000). Evaluate it by the convention in the selected review and in #5442: a register at chart `C` stores logical coordinates `u`, the physical vector at column multiplicity `f ≥ 1` is `C^{(⊗)f} u`, and a scalar coefficient stays outside the tensor power. + +**Proposition.** Every `SCALE`, `ADD` and `COPY` in that word acts on those logical coordinates by the same rational matrix at every integer `f ≥ 1`. The 342 events added to the pinned PR5565 word are 300 `ADD`s and 42 `SCALE`s, so they are included. The 3,447 `MOVE`s are not. + +The selected author proof states the corresponding sentence for the three basis changes. The maintainer review still lists universal native implementation at every positive column multiplicity as assumption `native_all_columns`. The argument below discharges only the scalar-instruction part of that sentence. It does not rerun the finite endpoint replay and does not treat a finite width as the proof. + +## 2. Lemmas + +Let `C` be an invertible linear operator on a finite-dimensional space `V`. Write `C^{(⊗)f}` for its `f`-fold tensor power on `V^{(⊗)f}`, and write `(C^{(⊗)f})^{-1} = (C^{-1})^{(⊗)f}`. + +**Lemma A (scale).** For every scalar `q` and every `f ≥ 1`, + +```text +C^{(⊗)f}(q u) = q C^{(⊗)f} u. +``` + +*Proof.* A scalar factors through every linear map, hence through each tensor factor and through their product. ∎ + +**Lemma B (common chart).** If both operands are logical coordinates of the same chart `C`, physical addition and return to that chart are + +```text +(C^{(⊗)f})^{-1}(C^{(⊗)f} u + q C^{(⊗)f} v) = u + q v. +``` + +`COPY` of `q v` into a zero logical register is the same identity with `u = 0`. + +*Proof.* `(C^{-1})^{(⊗)1} C^{(⊗)1} = I`. If it holds at `f`, the mixed-product identity `(A⊗B)(C⊗D) = (AC)⊗(BD)` gives + +```text +(C^{-1})^{(⊗)(f+1)} C^{(⊗)(f+1)} + = ((C^{-1})^{(⊗)f} C^{(⊗)f}) ⊗ (C^{-1} C) = I. +``` + +The scalar `q` then passes through that inverse. ∎ + +**Lemma C (distinct charts).** If the destination chart is `C_R` and the source chart is `C_S`, the same reading is + +```text +u + q (C_R^{-1} C_S)^{(⊗)f} v. +``` + +This equals `u + q v` for every `f ≥ 1` and all vectors if and only if `C_R^{-1} C_S = I`. The "only if" is the case `f = 1`. The "if" is Lemma B. + +*Phase trap.* If `C_R^{-1} C_S = -I`, the correction is `(-1)^f`. The width-free update `u + q v` is therefore right for every even `f` and wrong for every odd `f`. Agreement at width 2 does not imply agreement at width 1 or width 3. A finite-width sample cannot replace the common-chart hypothesis. + +`verify.py` checks Lemma A and Lemma B on three invertible charts (Pauli `X`, the shear `[[1,1],[0,1]]`, and `[[2,3],[5,7]]`) at widths 1, 2 and 3, and checks the mixed-product step on each chart. It checks the phase trap for `q = -1/2` and `v = e_0`: widths 1 and 3 miss the width-free replay, and width 2 hits it. Pauli `X` misses the replay at all three widths, and `X⊗X` is distinct from `X⊗I`. These specimens support the tensor implementation. The all-`f` statement is the induction above. + +## 3. Binding to the selected caller + +`local.py` in the selected package accepts a scalar event only when its frame tag equals the current chart of every operand. `MOVE` replaces that current chart; `INIT` and `CLEAR` set or drop it. `verify.py` reimplements that chart rule and no other acceptance test. + +On the selected word the walk accepts every event and counts 21,247 `ADD`, 757 `SCALE`, 8 `COPY` and 3,447 `MOVE`. The chart list is identical to `inputs/PR5565-WORD.json.gz`. Relative to that word the opcode delta is `+300 ADD`, `+42 SCALE`, and zero `MOVE`, `INIT`, `COPY` or `CLEAR` (25,133 events to 25,475; 735 public fields to 748). The thirteen helper splits therefore added only instructions covered by Lemmas A and B. The same chart indices denote the same operators before and after those splits. + +A synthetic `ADD` whose operands are at charts 4 and 5 is rejected. An `ADD` that still carries the pre-`MOVE` frame is rejected. Adding one to the frame tag of the first selected `ADD` is rejected. Those controls are finite rejection tests of the walker. They are not the all-width proof. + +## 4. What remains + +This does not prove that a `MOVE` from chart `A` to chart `B` equals `(chart_B^{-1} chart_A)^{(⊗)f}` on the tape, with the signed Pauli image and absolute phase. The selected `native` checker compares width-1 recipes. #5442 (Matarener) proves the group-algebra half of `native_all_columns` for the older #5413 caller, which does not contain these scalar bases and is not this word. + +Spectators, whole-job adapters and fixed-tape tariffs stay open. `owned_erasure`, `compiler`, `precision_tape` and `analytic_recovery` are untouched. Dyadic denominator bounds are a precision obligation and are not re-audited here. No outer row, admitted BIT budget or selected κ changes. #5625 (CRT row reentry) and #5707 (root-prefix lowering) are partial interfaces of other callers; neither is this implication. + +## 5. Downstream effect + +The width-free rational rows already used for this word's scalar program remain the logical coordinates at every positive column multiplicity, for `SCALE`, `ADD` and `COPY` only. Any later all-width claim for a `MOVE`, a native adapter or a different word still has to be proved on its own hypothesis. diff --git a/research/native-scalar-chart-lift/README.md b/research/native-scalar-chart-lift/README.md new file mode 100644 index 0000000000..402eeb1a5b --- /dev/null +++ b/research/native-scalar-chart-lift/README.md @@ -0,0 +1,50 @@ +# Scalar half of `native_all_columns` for the selected #5599 word + +**Scoped proof; no new κ.** Every `SCALE`, `ADD` and `COPY` in the selected helper-subspace word acts by the same rational matrix at every column multiplicity `f ≥ 1`. The 342 events added to the pinned PR5565 word are 300 `ADD`s and 42 `SCALE`s, so the thirteen helper splits sit inside that class. The 3,447 `MOVE`s stay inside assumption `native_all_columns`. + +The proof is [PROOF.md](PROOF.md). The width-free cancellation + +```text +(C^{(⊗)f})^{-1}(C^{(⊗)f} u + q C^{(⊗)f} v) = u + q v +``` + +is an induction on `f` for one common chart `C`. If the charts differ by `-I`, the correction is `(-1)^f`: width 2 matches the width-free replay and widths 1 and 3 do not. A finite width does not discharge the statement. + +## Scope and evidence + +Original card: `uniform-transfer-audit`, refined to assumption ID `native_all_columns` and this scalar implication. The actual question, the reason for the refinement and the stop rule are in [TASK.json](TASK.json). Pins are in [SOURCES.json](SOURCES.json). Base commit `de5ec2e7a6074068452f45b1a191b5c72832df4a`, priority revision 8. Selected κ remains `62009/20000000`. + +The chart walk on the selected word reports zero common-chart violations: 21,247 `ADD`, 757 `SCALE`, 8 `COPY`, 3,447 `MOVE`. The chart list matches the PR5565 word. Opcode delta `+300 ADD +42 SCALE +0 MOVE`. + +## Reproduce + +Python 3.12 and the standard library, from the repository root: + +```sh +python3 -B research/native-scalar-chart-lift/verify.py +python3 -O -B research/native-scalar-chart-lift/verify.py +python3 -B scripts/research_package.py --package research/native-scalar-chart-lift --check-only +python3 -B scripts/research_package.py --package research/native-scalar-chart-lift +``` + +Expected direct marker: + +```text +PASS_NATIVE_SCALAR_CHART_LIFT adds=21247 scales=757 copies=8 moves=3447 common_chart_violations=0 split_delta_add=300 split_delta_scale=42 split_delta_move=0 +``` + +The checker also rejects a cross-chart synthetic `ADD`, a stale frame tag after `MOVE`, and a one-step retag of the first selected `ADD`. It checks Pauli `X`, a shear and `[[2,3],[5,7]]` at widths 1, 2 and 3. Those widths are controls on the tensor code. The all-`f` argument is the induction in [PROOF.md](PROOF.md). + +Not run: `make frontier5599-verify`, native Clifford replay, Lean, and any proof of `MOVE` operators. + +## Open next questions + +Can the 3,447 retained `MOVE` chart changes of this same word be lifted by `g ↦ g^{(⊗)f}` with absolute phase, as group identities rather than width-1 recipe checks? + +That is the remaining algebraic content of `native_all_columns` for the selected caller. Scalar instructions no longer carry it. The smallest step is to census one distinct `(source frame, destination frame)` pair through the pinned `clifford_exact` canonical frames and apply the #5442 lifting lemma, including the action on `|0>`. The selected `native` checker only compares width-1 signed Pauli recipes. A passing census would still leave spectators, whole-job adapters and the fixed-tape tariff open. + +## Credit + +The selected word and the common-chart sentence are Ali Romman's PR #5599, using Pierre-Loic Doulcet / hexapode's PR #5565 word and the caller lineage credited in `research/p104-helper-subspace-splits/README.md`. The selected review is `docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md`. The convention that a scalar coefficient stays outside the tensor power is the one used by #5442 and stated for the older #4610 admission in `research/final4610-independent-admission`. #5442 (Mark / Matarener) proves the group-algebra half of `native_all_columns` for the older #5413 caller; it does not contain these scalar bases. #5625 and #5707 are different partial interfaces and are not reused as a proof of this implication. + +Prepared by unpaidmoon with substantial Cursor Grok assistance. Apache-2.0. diff --git a/research/native-scalar-chart-lift/SOURCES.json b/research/native-scalar-chart-lift/SOURCES.json new file mode 100644 index 0000000000..74f5045cfa --- /dev/null +++ b/research/native-scalar-chart-lift/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8", + "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/p104-helper-subspace-splits/WORD.json.gz", + "usage": "input", + "git_blob": "e325091e3051afe37a2d9c82f85afe9028510edb", + "sha256": "bbb072bced5824a8d9094c49be2fc51fbfdd05fb2b7dab8106e1275053075099" + }, + { + "path": "research/p104-helper-subspace-splits/inputs/PR5565-WORD.json.gz", + "usage": "input", + "git_blob": "4ebe6fcb7adf319bf6b247cf23d89eb1ca4cd914", + "sha256": "3d62828f53e654e3db218bf4611a47aed4a677d48043713dc004db0f8a32990d" + } + ] +} diff --git a/research/native-scalar-chart-lift/TASK.json b/research/native-scalar-chart-lift/TASK.json new file mode 100644 index 0000000000..5758e114f0 --- /dev/null +++ b/research/native-scalar-chart-lift/TASK.json @@ -0,0 +1,83 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 8, + "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "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": "Do the selected #5599 word's SCALE, ADD and COPY instructions, including the 342 scalar events added to the pinned PR5565 word, act by one f-independent rational matrix at every column multiplicity f >= 1?", + "scope_change_reason": "The card asks for one assumption ID and one quantified implication at the actual caller. This package takes native_all_columns and only the scalar-instruction implication for the selected #5599 word. MOVE operators, tape realization and the other four assumptions stay open. #5625 and #5707 remain partial interfaces of other callers.", + "bottleneck_link": "Side result; no new kappa. It discharges the scalar half of native_all_columns for the binding complex word. Admitted BIT and the other four framework assumptions still block an unconditional exponent.", + "budget_minutes": 60, + "stop_rule": "Stop when the common-chart scalar implication is proved for this word, or when the chart walk finds a cross-chart scalar event. Do not census MOVE operators or rerun frontier5599-verify.", + "outcome": "partial", + "evidence": "PROOF.md plus PASS_NATIVE_SCALAR_CHART_LIFT: 21247 ADD, 757 SCALE, 8 COPY, 3447 MOVE, zero common-chart violations, split delta +300 ADD +42 SCALE +0 MOVE. The phase-chart trap matches the width-free replay at width 2 and misses it at widths 1 and 3.", + "author": "unpaidmoon", + "ai_assistance": "Cursor Grok 4.7 provided substantial assistance with the proof, verifier and packaging.", + "open_questions": [ + { + "question": "Do the 3447 retained MOVE chart changes of this selected word lift by g -> g tensor f with absolute phase, as group identities rather than width-1 recipe checks?", + "why_it_matters": "Those moves are the remaining algebraic content of native_all_columns for the selected caller. The scalar instructions proved here do not discharge them.", + "first_step": "Census one distinct (source frame, destination frame) pair in WORD.json.gz through the pinned clifford_exact canonical frames and apply the #5442 lifting lemma, including the action on |0>.", + "blocked_by": "The selected native checker compares width-1 signed Pauli recipes only. A passing group-algebra census would still leave spectators, whole-job adapters and the fixed-tape tariff open." + } + ] +} diff --git a/research/native-scalar-chart-lift/VERIFY.json b/research/native-scalar-chart-lift/VERIFY.json new file mode 100644 index 0000000000..1270d8df8f --- /dev/null +++ b/research/native-scalar-chart-lift/VERIFY.json @@ -0,0 +1,31 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/p104-helper-subspace-splits/WORD.json.gz", + "research/p104-helper-subspace-splits/inputs/PR5565-WORD.json.gz" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Selected-word common-chart census, PR5565 scalar split delta, phase-chart width trap, and synthetic cross-chart rejection." + }, + { + "argv": [ + "{python}", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Same certificate with assert stripping; the checker uses explicit exceptions rather than assert." + } + ] +} diff --git a/research/native-scalar-chart-lift/verify.py b/research/native-scalar-chart-lift/verify.py new file mode 100644 index 0000000000..07d2c1787d --- /dev/null +++ b/research/native-scalar-chart-lift/verify.py @@ -0,0 +1,287 @@ +#!/usr/bin/env python3 +"""Scalar half of native_all_columns for the selected #5599 word. + +The all-width identities are proved in PROOF.md. This program binds that +proof to the selected word and checks the tensor arithmetic on explicit charts. +Finite widths are controls, not a substitute for the common-chart hypothesis. +""" + +from fractions import Fraction +from hashlib import sha256 +import gzip +import json +from pathlib import Path + + +ROOT = Path(__file__).resolve().parents[2] +SELECTED = ROOT / "research/p104-helper-subspace-splits/WORD.json.gz" +PREVIOUS = ROOT / "research/p104-helper-subspace-splits/inputs/PR5565-WORD.json.gz" +Q = Fraction + + +def need(ok, why): + if not ok: + raise ValueError(why) + + +def load_word(path): + with gzip.open(path, "rb") as handle: + word = json.loads(handle.read().decode("utf-8")) + need(word.get("schema") == "p104-productive-source/1", "Unexpected word schema") + need(isinstance(word.get("public"), int), "Public inventory") + need(len(word["initial"]) == word["public"] == len(word["final"]), "Boundary length") + need(isinstance(word.get("program"), list), "Program") + return word + + +def walk(program, initial, owned_slots=0): + """Return scalar-op counts after requiring one common current frame.""" + current = list(initial) + [None] * owned_slots + counts = {op: 0 for op in ("ADD", "SCALE", "COPY", "MOVE", "INIT", "CLEAR")} + for event in program: + need(isinstance(event, list) and event, "Event shape") + op = event[0] + need(op in counts, "Unexpected opcode " + str(op)) + role = event[1] + need(isinstance(role, int) and 0 <= role < len(current), "Role index") + if op == "MOVE": + need(len(event) == 5, "MOVE shape") + source, destination = event[2], event[3] + need(current[role] == source, "MOVE leaves the recorded chart") + current[role] = destination + elif op == "INIT": + need(len(event) == 3, "INIT shape") + current[role] = event[2] + elif op == "CLEAR": + need(len(event) == 3, "CLEAR shape") + need(current[role] == event[2], "CLEAR leaves the recorded chart") + current[role] = None + else: + need(len(event) == (4 if op == "SCALE" else 5), op + " shape") + coefficient, frame = Q(event[-2]), event[-1] + need(coefficient != 0, "Zero scalar coefficient") + need(isinstance(frame, int), "Frame tag") + need(current[role] == frame, "Scalar destination chart") + if op != "SCALE": + source = event[2] + need(isinstance(source, int) and source != role, "Scalar source role") + need(0 <= source < len(current), "Scalar source index") + need(current[source] == frame, "Common scalar chart") + counts[op] += 1 + return counts + + +def mat_id(n): + return [[Q(i == j) for j in range(n)] for i in range(n)] + + +def mat_mul(left, right): + rows, mid, cols = len(left), len(right), len(right[0]) + out = [[Q(0) for _ in range(cols)] for _ in range(rows)] + for i in range(rows): + for k in range(mid): + if left[i][k] == 0: + continue + for j in range(cols): + out[i][j] += left[i][k] * right[k][j] + return out + + +def mat_vec(matrix, vector): + return [sum(matrix[i][j] * vector[j] for j in range(len(vector))) for i in range(len(matrix))] + + +def kron(left, right): + n, m = len(left), len(left[0]) + p, q = len(right), len(right[0]) + out = [[Q(0) for _ in range(m * q)] for _ in range(n * p)] + for i in range(n): + for j in range(m): + for k in range(p): + for ell in range(q): + out[i * p + k][j * q + ell] = left[i][j] * right[k][ell] + return out + + +def tensor_pow(matrix, width): + out = [[Q(1)]] + for _ in range(width): + out = kron(out, matrix) + return out + + +def inv2(matrix): + determinant = matrix[0][0] * matrix[1][1] - matrix[0][1] * matrix[1][0] + need(determinant != 0, "Singular specimen chart") + return [[matrix[1][1] / determinant, -matrix[0][1] / determinant], + [-matrix[1][0] / determinant, matrix[0][0] / determinant]] + + +def add_vec(left, right): + return [a + b for a, b in zip(left, right)] + + +def scale_vec(coefficient, vector): + return [coefficient * entry for entry in vector] + + +def common_pullback(base, width, coefficient): + chart = tensor_pow(base, width) + inverse = tensor_pow(inv2(base), width) + size = len(chart) + vector_u = [Q(index + 1) for index in range(size)] + vector_v = [Q(1 if index % 2 == 0 else -3) for index in range(size)] + physical = add_vec(mat_vec(chart, vector_u), scale_vec(coefficient, mat_vec(chart, vector_v))) + logical = mat_vec(inverse, physical) + replay = add_vec(vector_u, scale_vec(coefficient, vector_v)) + scaled = mat_vec(chart, scale_vec(coefficient, vector_u)) + scale_commutes = scaled == scale_vec(coefficient, mat_vec(chart, vector_u)) + inverse_cancels = mat_mul(inverse, chart) == mat_id(size) + return logical == replay and scale_commutes and inverse_cancels + + +def mixed_product_step(base): + """(A⊗B)(C⊗D) = (AC)⊗(BD) on this chart and its inverse, the induction step.""" + inverse = inv2(base) + left = kron(mat_mul(inverse, base), mat_mul(inverse, base)) + right = mat_mul(kron(inverse, inverse), kron(base, base)) + one_factor = mat_mul(inverse, base) == mat_id(2) + return one_factor and left == right == mat_id(4) + + +def cross_chart(source_base, width, coefficient): + size = 2 ** width + destination = mat_id(size) + source = tensor_pow(source_base, width) + vector_u = [Q(2) for _ in range(size)] + vector_v = [Q(1)] + [Q(0)] * (size - 1) + physical = add_vec(mat_vec(destination, vector_u), + scale_vec(coefficient, mat_vec(source, vector_v))) + # Destination is the identity, so the logical vector is the physical sum. + logical = physical + replay = add_vec(vector_u, scale_vec(coefficient, vector_v)) + return logical, replay + + +def check_specimens(): + coefficient = Q(-1, 2) + pauli_x = [[Q(0), Q(1)], [Q(1), Q(0)]] + shear = [[Q(1), Q(1)], [Q(0), Q(1)]] + generic = [[Q(2), Q(3)], [Q(5), Q(7)]] + phase = [[Q(-1), Q(0)], [Q(0), Q(-1)]] + for base in (pauli_x, shear, generic): + need(mixed_product_step(base), "Tensor induction step failed") + for width in (1, 2, 3): + need(common_pullback(base, width, coefficient), + "Common-chart pullback failed at width " + str(width)) + phase_vs_replay = {} + for width in (1, 2, 3): + logical, replay = cross_chart(phase, width, coefficient) + phase_vs_replay[width] = logical == replay + # (-I)^{⊗f} = (-1)^f I, so a width-2 test accidentally matches the + # width-free replay while widths 1 and 3 do not. + need(phase_vs_replay == {1: False, 2: True, 3: False}, + "Phase-chart trap did not separate widths") + x_vs_replay = {} + for width in (1, 2, 3): + logical, replay = cross_chart(pauli_x, width, coefficient) + x_vs_replay[width] = logical == replay + need(x_vs_replay == {1: False, 2: False, 3: False}, "Pauli cross-chart should miss the replay") + first_factor = kron(pauli_x, mat_id(2)) + both_factors = kron(pauli_x, pauli_x) + need(first_factor != both_factors, "Width-2 Pauli power collapsed") + return {"phase_width_equals_replay": phase_vs_replay, + "pauli_x_width_equals_replay": x_vs_replay, + "widths_checked": [1, 2, 3], + "coefficient": str(coefficient)} + + +def check_walker_controls(): + initial = [4, 4] + need(walk([["ADD", 0, 1, "1", 4], ["SCALE", 0, "-1", 4]], initial)["ADD"] == 1, + "Synthetic common-chart block") + try: + walk([["ADD", 0, 1, "1", 4]], [4, 5]) + except ValueError as exc: + need(str(exc) == "Common scalar chart", "Cross-chart diagnostic") + else: + raise ValueError("Cross-chart ADD was accepted") + moved = [["MOVE", 0, 4, 7, False], ["ADD", 0, 1, "1", 7]] + need(walk(moved, [4, 7])["MOVE"] == 1, "Chart follows MOVE") + try: + walk([["MOVE", 0, 4, 7, False], ["ADD", 0, 1, "1", 4]], [4, 7]) + except ValueError as exc: + need(str(exc) == "Scalar destination chart", "Stale frame after MOVE") + else: + raise ValueError("Stale frame tag was accepted") + return {"synthetic_cross_chart_rejected": True, "stale_frame_rejected": True} + + +def opcode_counts(word): + counts = {} + for event in word["program"]: + counts[event[0]] = counts.get(event[0], 0) + 1 + return counts + + +def bind_words(): + selected = load_word(SELECTED) + previous = load_word(PREVIOUS) + need(selected["frames"] == previous["frames"], "Split changed the chart list") + frame_bytes = json.dumps(selected["frames"], separators=(",", ":")).encode() + walked = walk(selected["program"], selected["initial"], owned_slots=8) + counted = opcode_counts(selected) + for op, count in walked.items(): + need(counted.get(op, 0) == count, "Walk dropped an event") + previous_counts = opcode_counts(previous) + expected_previous = {"ADD": 20947, "MOVE": 3447, "SCALE": 715, "INIT": 8, "COPY": 8, "CLEAR": 8} + expected_selected = {"ADD": 21247, "MOVE": 3447, "SCALE": 757, "INIT": 8, "COPY": 8, "CLEAR": 8} + need(previous_counts == expected_previous, "PR5565 opcode census") + need(counted == expected_selected, "Selected opcode census") + need(previous["public"] == 735 and selected["public"] == 748, "Public-field delta") + need(len(previous["program"]) == 25133 and len(selected["program"]) == 25475, "Event delta") + mutated = json.loads(json.dumps(selected["program"])) + for event in mutated: + if event[0] == "ADD": + event[-1] = event[-1] + 1 + break + else: + raise ValueError("Selected word has no ADD") + try: + walk(mutated, selected["initial"], owned_slots=8) + except ValueError: + mutated_rejected = True + else: + raise ValueError("Retagged ADD was accepted") + return {"adds": counted["ADD"], "scales": counted["SCALE"], "copies": counted["COPY"], + "moves": counted["MOVE"], "common_chart_violations": 0, + "split_delta_add": counted["ADD"] - previous_counts["ADD"], + "split_delta_scale": counted["SCALE"] - previous_counts["SCALE"], + "split_delta_move": counted["MOVE"] - previous_counts["MOVE"], + "split_delta_events": len(selected["program"]) - len(previous["program"]), + "public_delta": selected["public"] - previous["public"], + "frames_sha256": sha256(frame_bytes).hexdigest(), + "tag_mutation_rejected": mutated_rejected} + + +def main(): + binding = bind_words() + specimens = check_specimens() + controls = check_walker_controls() + need(binding["split_delta_add"] == 300 and binding["split_delta_scale"] == 42 + and binding["split_delta_move"] == 0 and binding["split_delta_events"] == 342 + and binding["public_delta"] == 13, "Split delta left the scalar class") + need(controls["synthetic_cross_chart_rejected"] and binding["tag_mutation_rejected"], + "Failure controls") + print("PASS_NATIVE_SCALAR_CHART_LIFT" + " adds={adds} scales={scales} copies={copies} moves={moves}" + " common_chart_violations={common_chart_violations}" + " split_delta_add={split_delta_add} split_delta_scale={split_delta_scale}" + " split_delta_move={split_delta_move}".format(**binding)) + print("controls " + json.dumps({"specimens": specimens, "walker": controls, + "frames_sha256": binding["frames_sha256"]}, + sort_keys=True)) + + +if __name__ == "__main__": + main()