Prove the selected PR6030 scalar instructions lift at every column mu…

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.

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.

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

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

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