diff --git a/research/pr6030-scalar-chart-lift/PROOF.md b/research/pr6030-scalar-chart-lift/PROOF.md new file mode 100644 index 0000000000..f0397934c2 --- /dev/null +++ b/research/pr6030-scalar-chart-lift/PROOF.md @@ -0,0 +1,90 @@ +# Scalar instructions of the selected PR6030 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 of that assumption on the selected caller. It is not the assumption, and it is not any of the other four. + +## 1. Proposition + +Let the selected word be `research/p104-helper470-twin-rung-removal/WORD.json.gz` on canonical main `7c49fe32c55de02c2c873655c804b16e4c3fef0a` (PR #6030, κ = 781451/250000000). Its schema is `p104-accumulated-block-composition/2`. It has 770 public registers, 29 owned registers and 22,803 events. + +Use the convention in the selected PR6030 review and in #5837: a register at an invertible 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. Equal frame indices name the same chart. + +**Proposition.** Every `SCALE`, `ADD` and `COPY` in this word acts on those logical coordinates by the same rational matrix at every integer `f ≥ 1`. + +The 3,453 `MOVE`s are not included. #5837 proved the same scalar sentence for the older selected #5599 word and stated that a different word still has to be proved on its own hypothesis. This note is that hypothesis for the word the selected record now uses. + +## 2. Lemmas + +The three identities below are the chart-algebra argument of `research/native-scalar-chart-lift/PROOF.md` (unpaidmoon, PR #5837). They do not depend on which word supplies the events. They are restated so this note can be read alone. + +Let `C` be an invertible linear operator on a finite-dimensional space `V`. Write `C^{(⊗)f}` for its `f`-fold tensor power, 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. + +## 3. Binding to the selected caller + +The chart state of the word is the following finite machine. Public registers start at `initial`. Owned registers start with no chart. `INIT` on an unowned owned-index gives that register a chart and an empty logical row. `CLEAR` on an owned register at the named chart drops both. `MOVE` from the current chart replaces it. A scalar event is accepted only when every operand's current chart equals the event's frame tag, the coefficient is a nonzero rational, and a `COPY` destination is an owned register whose logical row is empty. + +`verify.py` reimplements that machine and no endpoint arithmetic. On this word the walk accepts every event: + +| Opcode | Count | +|---|---:| +| `ADD` | 18,404 | +| `SCALE` | 861 | +| `COPY` | 23 | +| `MOVE` | 3,453 | +| `INIT` | 31 | +| `CLEAR` | 31 | + +All 29 owned indices in `770..798` occur. Register 778 is initialized three times and the other 28 once, always after a `CLEAR`, so the 31 lifetimes are serial. The peak number of simultaneously owned registers is 13. At the end no owned register remains, and every public chart equals `final`. + +Each of the 23 `COPY`s writes an empty owned row, so its logical vector is `u = 0`. Each `ADD` and each `COPY` has one common frame index on its operands, so Lemma C's obstruction is absent and Lemma B applies at every `f ≥ 1`. Each `SCALE` is Lemma A at the destination chart. That is the proposition. + +The same walk rejects a cross-chart `ADD`, a stale frame tag after `MOVE`, a zero coefficient, and a `COPY` into a nonempty owned row. Replacing the frame tag of the first `ADD` in this word is rejected. Those are finite rejection tests of the walker. + +The tensor specimens in `verify.py` check Lemma A's commutation, Lemma B's pullback and the mixed-product step on Pauli `X`, the shear `[[1,1],[0,1]]` and `[[2,3],[5,7]]` at widths 1, 2 and 3. They also check the phase trap: `(-I)` matches the width-free replay at width 2 and misses it at widths 1 and 3. Those specimens support the tensor implementation. They are not the all-`f` proof. The all-`f` proof is the induction in Lemma B together with the common-chart and empty-`COPY` census above. + +## 4. What remains + +This does not prove that a `MOVE` from chart `A` to chart `B` equals `(chart_B^{-1} chart_A)^{(⊗)f}` with the signed Pauli image and absolute phase. #6293 records the phase factor `i^{p f}` for this same word and leaves the joint lowered recipe open. Spectators, whole-job adapters and the fixed-tape tariff stay open. + +`INIT` and `CLEAR` are used only as the chart and emptiness state machine. That is not a proof of the physical erasure contract in `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. The width-1 endpoint replay in `research/p104-6030-independent-audit` checks this word's charts and empty `COPY`s as part of a different obligation. It does not state the all-`f` scalar proposition. #6522 records the `precision_tape` envelope exponent and is not this implication. + +## 5. Downstream effect + +The width-free rational rows of this word's scalar program remain the logical coordinates at every positive column multiplicity, for `SCALE`, `ADD` and `COPY` only. A later all-width claim for a `MOVE`, a native adapter or another word still has to be proved on its own hypothesis. Discharging the scalar half does not remove `native_all_columns` from the selected record. diff --git a/research/pr6030-scalar-chart-lift/README.md b/research/pr6030-scalar-chart-lift/README.md new file mode 100644 index 0000000000..0a73d45797 --- /dev/null +++ b/research/pr6030-scalar-chart-lift/README.md @@ -0,0 +1,53 @@ +# Scalar half of `native_all_columns` for the selected #6030 word + +**Scoped proof; no new κ.** Every `SCALE`, `ADD` and `COPY` in the selected PR6030 word acts by the same rational matrix at every column multiplicity `f ≥ 1`. The census is 18,404 `ADD`s, 861 `SCALE`s and 23 `COPY`s, each on one common chart. Every `COPY` writes an empty owned logical row. The 3,453 `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 invertible 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 the scalar-instruction implication on the selected PR6030 caller. 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 `7c49fe32c55de02c2c873655c804b16e4c3fef0a`, priority revision 8. Selected κ remains `781451/250000000`. + +Open-PR overlap at 2026-11-03T13:29:40Z covered 572 open PR bodies. No open PR states this census. The discussion refresh returned HTTP 502; comments on #1166 from 2026-10-24 through 2026-11-03 were read directly and do not claim these scalar events. + +This is session r92, item 5 of the ordered eligible list. The 19 October handoff index is already delivered. Later structured handoffs are excluded when the post is DONE, a later merged result answers them, or the canonical artifact is an open PR, including the H25 requests on #6321, #6326, #6328, #6332 and #6335 and the 2 November review artifacts #6355, #6357, #6359, #6360, #6361, #6376, #6378 and #6396. Unexpired claims do not cover this word's scalar events. Work already delivered by this account is excluded. The revision-8 next-decision table then supplies six rows, and unnamed catalogue cards follow. Item 5 is the all-size row. Within that row, #5837, #6293 and #6522 are different implications and were not repeated. + +The chart walk reports zero common-chart violations and 23 empty-target `COPY`s. Register 778 has three serial lifetimes; the other 28 owned registers have one. Peak simultaneous owned registers: 13. + +## Reproduce + +Python 3.12 and the standard library, from the repository root: + +```sh +python3 -B research/pr6030-scalar-chart-lift/verify.py +python3 -O -B research/pr6030-scalar-chart-lift/verify.py +python3 -B scripts/research_package.py --package research/pr6030-scalar-chart-lift --check-only +python3 -B scripts/research_package.py --package research/pr6030-scalar-chart-lift +``` + +Expected direct marker: + +```text +PASS_PR6030_SCALAR_CHART_LIFT adds=18404 scales=861 copies=23 moves=3453 inits=31 clears=31 common_chart_violations=0 copy_into_empty=23 peak_owned=13 owned_fields=29 public=770 events=22803 phase_width2_only=true no_new_kappa=true +``` + +The checker rejects a cross-chart synthetic `ADD`, a stale frame tag after `MOVE`, a zero coefficient, a `COPY` into a nonempty owned row, 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 frontier6030-verify`, the primary native replay, Lean, and any proof of `MOVE` operators. + +## Open next questions + +1. Do the 3,453 `MOVE`s of this same word equal `(chart_b^{-1} chart_a)^{(⊗)f}` as group elements, including absolute phase `i^{p f}`? #6293 records the phase factor and leaves the joint lowered recipe open. The first step is one lowered recipe with `p ≠ 0` against `U^{(⊗)f}`. Blocked because the primary native payload is not an input here. +2. Does the empty-`COPY` chart identity survive the retained tape and erasure model at width `f`? The first step is one `INIT`/`COPY`/`CLEAR` triple in that model. Blocked by `owned_erasure` and `precision_tape`, which this note does not use. + +## Credit + +The selected word is DreamingOfClouds' PR #6030. The chart convention and the scalar induction are the ones recorded for the older #5599 word in `research/native-scalar-chart-lift` (unpaidmoon, PR #5837), which explicitly leaves a different word open. #6293 (unpaidmoon) is the `MOVE` phase factor on this word, not the scalar events. The width-1 endpoint replay is `research/p104-6030-independent-audit` (JosieElliston). The selected review is `docs/research/pr-intake-evidence/pr6030-audit/PROOF-REVIEW.md`. #5442 (Mark / Matarener) is the group-algebra half for the older #5413 caller. + +Prepared by unpaidmoon with substantial Cursor Grok assistance. Apache-2.0. diff --git a/research/pr6030-scalar-chart-lift/SOURCES.json b/research/pr6030-scalar-chart-lift/SOURCES.json new file mode 100644 index 0000000000..120a707639 --- /dev/null +++ b/research/pr6030-scalar-chart-lift/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "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" + } + ] +} diff --git a/research/pr6030-scalar-chart-lift/TASK.json b/research/pr6030-scalar-chart-lift/TASK.json new file mode 100644 index 0000000000..80a520098b --- /dev/null +++ b/research/pr6030-scalar-chart-lift/TASK.json @@ -0,0 +1,89 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "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 #6030 word's SCALE, ADD and COPY instructions 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 #6030 word. MOVE operators, tape realization and the other four assumptions stay open. #5625 and #5707 remain partial interfaces of other callers. #5837 is the same implication on the older #5599 word.", + "bottleneck_link": "The selected conditional supplier still lists native_all_columns. This discharges only the scalar-instruction half on the current word, so the width-free scalar rows remain the logical coordinates at every positive column multiplicity. It does not raise kappa or remove the assumption.", + "budget_minutes": 60, + "stop_rule": "Stop after the scalar implication on this pinned word. Do not search MOVE group identities, rerun the native replay, or treat a finite width as the proof.", + "outcome": "partial", + "evidence": "PROOF.md plus PASS_PR6030_SCALAR_CHART_LIFT: 18404 ADD, 861 SCALE, 23 COPY, 3453 MOVE, 31 INIT, 31 CLEAR, zero common-chart violations, 23 empty-target COPYs, peak owned 13. 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 3453 MOVE events of this word equal (chart_b^{-1} chart_a) tensor-power f, including absolute phase i^{p f}?", + "why_it_matters": "MOVE is the remaining algebraic half of native_all_columns on this caller. The scalar half no longer carries it.", + "first_step": "Compare one lowered recipe with p != 0 against U tensor-power f, including the action on |0>.", + "blocked_by": "The primary native payload is not an input of this package. #6293 records the phase factor and leaves the joint recipe open." + }, + { + "question": "Does the empty-COPY chart identity survive the retained tape and erasure model at width f?", + "why_it_matters": "A cleared logical row is not by itself a physical erasure or a width-f storage tariff.", + "first_step": "Price one INIT/COPY/CLEAR triple in the retained tape model, including residual storage.", + "blocked_by": "owned_erasure and precision_tape. This note uses INIT and CLEAR only as a chart state machine." + } + ] +} diff --git a/research/pr6030-scalar-chart-lift/VERIFY.json b/research/pr6030-scalar-chart-lift/VERIFY.json new file mode 100644 index 0000000000..e3522516a7 --- /dev/null +++ b/research/pr6030-scalar-chart-lift/VERIFY.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/p104-helper470-twin-rung-removal/WORD.json.gz" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Common-chart census, empty COPY census, tensor specimens at widths 1-3, and rejection of a cross-chart ADD, a stale frame, a nonempty COPY and a retagged selected ADD." + }, + { + "argv": [ + "{python}", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Same census with assertions stripped. The verifier raises ValueError, so -O does not disable the checks." + } + ] +} diff --git a/research/pr6030-scalar-chart-lift/verify.py b/research/pr6030-scalar-chart-lift/verify.py new file mode 100644 index 0000000000..6a8e42ab5c --- /dev/null +++ b/research/pr6030-scalar-chart-lift/verify.py @@ -0,0 +1,296 @@ +#!/usr/bin/env python3 +"""Bind the scalar half of native_all_columns to the selected PR6030 word. + +The all-width identities are proved in PROOF.md. This program checks the +common-chart and empty-COPY hypotheses on that word, and checks the tensor +arithmetic on explicit charts. Finite widths are controls, not a substitute +for the induction. +""" + +from fractions import Fraction +from hashlib import sha256 +import gzip +import json +from pathlib import Path + + +ROOT = Path(__file__).resolve().parents[2] +WORD = ROOT / "research/p104-helper470-twin-rung-removal/WORD.json.gz" +WORD_SHA256 = "7834725d9e34ee846a9ccc615221ea81e0201613938afa185d2eda0c9a6c232f" +# Published #5599 census in research/native-scalar-chart-lift/PROOF.md. +# A swap back to that word must not satisfy this package. +OLDER_SELECTED_COUNTS = {"ADD": 21247, "SCALE": 757, "COPY": 8, "MOVE": 3447} +Q = Fraction + + +def need(ok, why): + if not ok: + raise ValueError(why) + + +def load_word(path): + payload = path.read_bytes() + need(sha256(payload).hexdigest() == WORD_SHA256, "Selected word SHA256") + word = json.loads(gzip.decompress(payload).decode("utf-8")) + need(word.get("schema") == "p104-accumulated-block-composition/2", "Word schema") + public = word.get("public") + owned = word.get("owned_fields") + need(isinstance(public, int) and isinstance(owned, int) and owned > 0, "Inventory") + need(len(word["initial"]) == public == len(word["final"]), "Boundary length") + need(isinstance(word.get("frames"), list) and word["frames"], "Frames") + need(isinstance(word.get("program"), list), "Program") + return word + + +def frame_index(value, frame_count, why): + need(isinstance(value, int) and 0 <= value < frame_count, why) + return value + + +def walk(program, initial, frame_count, owned_slots=0): + """Accept scalar events only on one common current frame. + + COPY is accepted only into an owned register whose logical row is empty. + Public rows start nonempty. An owned row is empty after INIT or CLEAR + and becomes nonempty when a nonempty source is copied or added into it. + """ + current = list(initial) + [None] * owned_slots + empty = [False] * len(initial) + [False] * owned_slots + owned = set() + counts = {op: 0 for op in ("ADD", "SCALE", "COPY", "MOVE", "INIT", "CLEAR")} + peak = 0 + initialized = set() + 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 and isinstance(event[4], bool), "MOVE shape") + source = frame_index(event[2], frame_count, "MOVE source chart") + destination = frame_index(event[3], frame_count, "MOVE destination chart") + need(current[role] == source, "MOVE leaves the recorded chart") + need((role in owned) == event[4], "MOVE ownership flag") + current[role] = destination + elif op == "INIT": + need(len(event) == 3, "INIT shape") + need(role >= len(initial) and role not in owned, "Owned init") + owned.add(role) + initialized.add(role) + peak = max(peak, len(owned)) + empty[role] = True + current[role] = frame_index(event[2], frame_count, "INIT chart") + elif op == "CLEAR": + need(len(event) == 3, "CLEAR shape") + need(role in owned, "CLEAR of an unowned register") + need(current[role] == frame_index(event[2], frame_count, "CLEAR chart"), + "CLEAR leaves the recorded chart") + owned.discard(role) + empty[role] = True + current[role] = None + else: + need(len(event) == (4 if op == "SCALE" else 5), op + " shape") + coefficient = Q(event[-2]) + frame = frame_index(event[-1], frame_count, "Scalar frame") + need(coefficient != 0, "Zero scalar coefficient") + need(current[role] == frame, "Scalar destination chart") + if op == "SCALE": + pass + else: + 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") + if op == "COPY": + need(role in owned and empty[role], "COPY into a nonempty row") + empty[role] = empty[source] + else: + need(op == "ADD", "Opcode") + empty[role] = empty[role] and empty[source] + counts[op] += 1 + need(not owned, "Owned register left open") + return counts, peak, initialized, current + + +def finish_walk(word): + counts, peak, initialized, current = walk( + word["program"], word["initial"], len(word["frames"]), word["owned_fields"]) + public = word["public"] + need(current[:public] == word["final"], "Public charts miss the published final boundary") + need(initialized == set(range(public, public + word["owned_fields"])), + "Owned inventory is not exactly the initialized registers") + return counts, peak + + +def mat_id(size): + return [[Q(i == j) for j in range(size)] for i in range(size)] + + +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)) + return (logical == replay + and scaled == scale_vec(coefficient, mat_vec(chart, vector_u)) + and mat_mul(inverse, chart) == mat_id(size)) + + +def mixed_product_step(base): + inverse = inv2(base) + left = kron(mat_mul(inverse, base), mat_mul(inverse, base)) + right = mat_mul(kron(inverse, inverse), kron(base, base)) + return mat_mul(inverse, base) == mat_id(2) and left == right == mat_id(4) + + +def cross_matches_replay(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))) + replay = add_vec(vector_u, scale_vec(coefficient, vector_v)) + return physical == 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 = {width: cross_matches_replay(phase, width, coefficient) for width in (1, 2, 3)} + need(phase_vs_replay == {1: False, 2: True, 3: False}, "Phase-chart trap did not separate widths") + pauli_vs_replay = {width: cross_matches_replay(pauli_x, width, coefficient) for width in (1, 2, 3)} + need(pauli_vs_replay == {1: False, 2: False, 3: False}, "Pauli cross-chart should miss the replay") + need(kron(pauli_x, mat_id(2)) != kron(pauli_x, pauli_x), "Width-2 Pauli power collapsed") + return phase_vs_replay + + +def expect_error(program, initial, frames, owned_slots, message): + try: + walk(program, initial, frames, owned_slots) + except ValueError as exc: + need(str(exc) == message, "Unexpected rejection: " + str(exc)) + else: + raise ValueError("Accepted an event that must fail: " + message) + + +def check_walker_controls(): + expect_error([["ADD", 0, 1, "1", 4]], [4, 5], 6, 0, "Common scalar chart") + expect_error([["MOVE", 0, 4, 5, False], ["ADD", 0, 1, "1", 4]], [4, 5], 6, 0, + "Scalar destination chart") + expect_error([["SCALE", 0, "0", 4]], [4], 6, 0, "Zero scalar coefficient") + owned_copy = [ + ["INIT", 1, 4], + ["ADD", 1, 0, "1", 4], + ["COPY", 1, 0, "1", 4], + ] + expect_error(owned_copy, [4], 6, 1, "COPY into a nonempty row") + empty_copy = [["INIT", 1, 4], ["COPY", 1, 0, "1/2", 4], ["CLEAR", 1, 4]] + counts, peak = walk(empty_copy, [4], 6, 1)[:2] + need(counts["COPY"] == 1 and peak == 1, "Empty owned COPY") + return True + + +def check_word_mutation(word): + mutated = json.loads(json.dumps(word["program"])) + index = next(i for i, event in enumerate(mutated) if event[0] == "ADD") + mutated[index][-1] = mutated[index][-1] + 1 + try: + walk(mutated, word["initial"], len(word["frames"]), word["owned_fields"]) + except ValueError: + return True + raise ValueError("Retagging the first ADD was accepted") + + +def main(): + word = load_word(WORD) + counts, peak = finish_walk(word) + need(counts["ADD"] == 18404 and counts["SCALE"] == 861 and counts["COPY"] == 23, "Scalar census") + need(counts["MOVE"] == 3453 and counts["INIT"] == 31 and counts["CLEAR"] == 31, "State-machine census") + need(sum(counts.values()) == 22803, "Event total") + need(peak == 13 and word["owned_fields"] == 29 and word["public"] == 770, "Owned peak") + need(any(counts[op] != OLDER_SELECTED_COUNTS[op] for op in OLDER_SELECTED_COUNTS), + "Census collapsed to the older #5599 word") + phase = check_specimens() + need(phase == {1: False, 2: True, 3: False}, "Specimen phase trap") + need(check_walker_controls(), "Walker controls") + need(check_word_mutation(word), "Word mutation control") + print( + "PASS_PR6030_SCALAR_CHART_LIFT" + " adds=%d scales=%d copies=%d moves=%d inits=%d clears=%d" + " common_chart_violations=0 copy_into_empty=%d peak_owned=%d" + " owned_fields=%d public=%d events=%d" + " phase_width2_only=true no_new_kappa=true" + % (counts["ADD"], counts["SCALE"], counts["COPY"], counts["MOVE"], + counts["INIT"], counts["CLEAR"], counts["COPY"], peak, + word["owned_fields"], word["public"], sum(counts.values())) + ) + + +if __name__ == "__main__": + main()