Prove the selected #5599 scalar instructions lift at every column mul…

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.

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.

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"
+    }
+  ]
+}

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."
+    }
+  ]
+}

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."
+    }
+  ]
+}