Prove scalar frame gauges cannot remove selected MOVE phases (no κ)

research/move-frame-phase-obstruction/PROOF.md

@@ -0,0 +1,126 @@
+# A three-edge obstruction to scalar frame rephasing
+
+This scoped proof and its exact finite certificate were produced by Nick Petalas.
+
+## Definitions and source
+
+The fixed input is the selected PR6030 word, SHA256
+`7834725d9e34ee846a9ccc615221ea81e0201613938afa185d2eda0c9a6c232f`,
+at canonical main `2485805a6d47f36ea83ddde6327d453ac82d44dc`.
+The retained `clifford_exact.py` constructs a unitary chart `C_a` for frame `a`.
+Use ordinary matrix composition, with the rightmost matrix acting first.
+The source expression `chart(a).adjoint().then(chart(b))` applies `C_a†`
+first, then `C_b`, so its matrix is
+
+    T_ab = C_b C_a†.
+
+The source native normal form expresses `T_ab = i^(p_ab) S_ab`, where
+`p_ab` is the sum modulo four of its literal `phase` gates and `S_ab` is
+that same recipe with only those gates deleted. This definition fixes every
+permutation, quadratic phase, translation and Gaussian gate in `S_ab`.
+It does not identify all possible recipes for an operator.
+
+Three used frames and three actual MOVE occurrences suffice. Indices are
+zero-based, as in the JSON program.
+
+| Frame | Binary basis |
+|---|---|
+| 3 | empty |
+| 2 | 35 |
+| 299 | 35, 75, 400 |
+
+| Directed edge | Event index | Public role | Child rank | `p_ab` |
+|---|---:|---:|---:|---:|
+| 3 to 2 | 10338 | 259 | 1 | 1 |
+| 2 to 299 | 10403 | 258 | 2 | 1 |
+| 3 to 299 | 14360 | 465 | 3 | 1 |
+
+The events are on different roles. The theorem concerns one chart choice shared
+by every occurrence of a frame. It does not assert a chronological three-event
+subroutine or an actual closed walk by one role.
+
+## The scalar gauge theorem
+
+For each positive integer column multiplicity `f`, permit a separate arbitrary
+unit-modulus scalar `lambda_a(f)` for each frame and replace its tensor chart by
+
+    C'_a(f) = lambda_a(f) C_a^(tensor f).
+
+There exists such a frame gauge making every selected MOVE equal to its fixed
+phase-deleted recipe `S_ab^(tensor f)` if and only if `4` divides `f`.
+In particular, no width-one frame gauge removes all these literal phase tags.
+This permits width-dependent gauges and arbitrary complex unit phases, not only
+fourth roots of unity.
+
+**Proof.** Under a frame gauge the MOVE becomes
+
+    T'_ab(f) = lambda_b(f) conjugate(lambda_a(f))
+                i^(f p_ab) S_ab^(tensor f).
+
+Since `S_ab` is invertible, equality with its phase-deleted tensor recipe requires
+
+    lambda_b(f) / lambda_a(f) = i^(-f p_ab).
+
+For the edges `3 to 2` and `2 to 299`, the product of the required ratios is
+`i^(-2f)`. The direct edge `3 to 299` requires the same ratio to be `i^(-f)`.
+Consequently `i^f = 1`, which holds exactly when `4` divides `f`.
+Conversely, every literal phase gate in the retained native alphabet has an
+integer exponent modulo four. If `4` divides `f`, all its tensor scalar factors
+are one; the trivial gauge therefore works for every selected MOVE, without
+needing a census of the remaining edges. This proves both directions. ∎
+
+The argument is the classical cycle criterion for scalar edge potentials.
+The new source-specific content is the three used edges with cycle residue
+`p_32 + p_2,299 - p_3,299 = 1 mod 4`, and the resulting exact width criterion.
+
+## Operator certificate and sharpness on the triangle
+
+Chart cancellation gives
+
+    T_2,299 T_3,2 = T_3,299.
+
+Substituting the three measured phases gives
+
+    S_3,299† S_2,299 S_3,2 = -i I.
+
+The verifier checks the full-phase loop is `I` and the phase-deleted loop is
+`-i I` on every one of the 512 coordinate basis vectors, using exact Gaussian
+integer numerators and powers of two as denominators. Tensoring the identity
+shows that the phase-deleted loop at width `f` is `(-i)^f I`.
+
+At width one, one residual tag among these three is necessary and sufficient.
+Set `q_3=0`, `q_2=3`, `q_299=2`, with `lambda_a=i^(q_a)`. The path edges then
+have zero residual phase and the direct edge has residue `3`. This attains the
+one-tag minimum on this triangle only. No global minimum tag count is claimed.
+
+As controls, enumerating the 64 fourth-root vertex assignments gives no
+solution at widths 1, 2 or 3, and four solutions at width 4. Replacing the direct
+edge's phase by 2 gives four width-one solutions. Deleting the direct constraint
+leaves the expected four tree solutions. Wrong loop phase and reversed sign
+are rejected. These finite controls corroborate the proof, including its sign;
+they are not the argument for arbitrary `f` or arbitrary unit phases.
+
+## Scope and predecessors
+
+Unpaidmoon / PR6293 identifies the selected tensor-phase scaling question and
+reports the full phase census. That census is cited, not replayed or adopted as
+this result. The three-edge witness here is independently compiled to establish
+a new gauge obstruction. DLamdata / PR5894 records existing absolute-phase
+coverage; this proof asserts no missing source check. Mark / Matarener's
+PR5974 and PR5442 supply earlier all-width lift work.
+
+DreamingOfClouds supplied PR6030's selected word, building on PR5907, PR5827,
+Ali Romman's PR5599 and their retained P104 lineage. Chafik Boukhalfa's native
+channel retains the exact compiler through icekylinx's frame-sa504 package and
+the independent Gaussian interpreter from Ali Romman's PR1862 and PR1931.
+Rohan Arun / PR1972, Adam Gall / PR1940, Josie Elliston / PR1071, Ali Romman /
+PR1125 and the retained decoder/native sources keep their original credit.
+All input files remain unchanged. Apache-2.0.
+
+The obstruction fixes the extracted native normal forms. A different
+factorization can move a scalar into other gates. Role-specific or
+history-dependent charts can also change the constraint graph. No lower bound
+for those mechanisms follows. No physical scalar cost, changed paid profile,
+new kappa, supplier failure, selected-frontier change or complete multiplication
+theorem is claimed. All five selected framework assumptions remain.
+Independent human and formal proof-kernel review are unclaimed.

research/move-frame-phase-obstruction/README.md

@@ -0,0 +1,84 @@
+# Selected MOVE phases cannot all be removed by frame rephasing
+
+A scoped proof with an exact finite certificate, produced by Nick Petalas.
+
+On the selected PR6030 word, the native recipes for `3 to 2`, `2 to 299` and
+`3 to 299` each contain total explicit phase `i`. Their cycle residue is one
+modulo four. Scalar changes to the frame charts cancel around this triangle,
+so they cannot remove every explicit phase. At column multiplicity `f`, even
+arbitrary width-dependent unit-complex frame gauges succeed for every selected
+MOVE exactly when `4` divides `f`. The phase-deleted triangle loop is `-i I` at
+width one. One residual tag is necessary and sufficient on that triangle.
+
+This answers a new changed-chart question prompted by unpaidmoon / PR6293,
+without repeating its full phase census. It closes the particular remedy of
+removing tensor-phase bookkeeping by one scalar gauge per frame. Keeping the
+correct phases already works; no source correctness failure is asserted.
+The [proof](PROOF.md) fixes the normal forms and gives the all-width argument.
+
+## Evidence and reproduction
+
+From the repository root, using CPython 3.12 and the standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/move-frame-phase-obstruction/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/move-frame-phase-obstruction/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/move-frame-phase-obstruction
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/move-frame-phase-obstruction --check-source-history
+```
+
+Another CPython 3.12 interpreter may replace that local path. The direct verifier
+also works from a source export without Git. Expected markers are
+`PASS_MOVE_FRAME_PHASE_OBSTRUCTION`, `PASS_REGISTERED_RESEARCH_PACKAGE` and
+`PASS_RESEARCH_COMMIT_BYTES`.
+
+The verifier authenticates all three live sources, binds the named frames and
+actual event indices, and compiles only the three witness edges. The separate
+Gaussian interpreter checks their signed Pauli actions and absolute phases.
+Both the full and phase-deleted loops are checked on all 512 basis states.
+The 64 fourth-root gauge assignments are enumerated at each width 1 through 4.
+Compatible-triangle, tree, restored-loop, wrong-phase, reversed-sign and changed
+source-byte controls run in both normal and optimized Python. Output includes
+a generated receipt binding the package and live input hashes. It writes no
+files. Hosted CI status is recorded separately in the PR body.
+
+## Limitations
+
+The theorem fixes the recipes with literal `phase` gates removed. It does not
+cover refactoring their other gates or using distinct charts by role or history.
+The three edges occur on different roles; the diagnostic loop is an operator
+identity, not a chronological subroutine. No whole-word native replay, selected
+cold replay, physical caller, all-size implementation, Lean or Docker was run.
+No new kappa or complete multiplication theorem is claimed. All five selected
+framework assumptions remain. Independent human and formal proof-kernel review
+are unclaimed.
+
+The verifier uses bounded source sizes, three nine-axis charts, 512 basis
+states and 64 gauge assignments per tested width. Python and the frozen exact
+interpreters allocate dynamically; these finite bounds replace a fixed-memory
+implementation. Dynamic module loading is restricted to two authenticated
+files. Frozen source style and its internal assertions are retained, while new
+acceptance checks use exceptions and remain enabled under `-O`. No external
+static analyzer was available; warning-strict execution and the registered
+checks are the available diagnostics.
+
+## Open next questions
+
+Can role-specific phase charts eliminate tags while preserving every actual
+common-chart ADD and COPY relation and the endpoint normalizers? Start with
+these three occurrences and add the real scalar-gate compatibility constraints.
+The obstruction here requires one shared phase per frame, so that larger graph
+and its physical scalar bill remain open. Do not treat missing compatibility or
+restoration charges as zero.
+
+## Credit
+
+The witness and gauge application were produced by Nick Petalas. The cycle
+criterion and tensor-product scalar identity are classical. Credit unpaidmoon /
+PR6293 for the selected tensor-phase question; DLamdata / PR5894 for existing
+absolute-phase coverage; Mark / Matarener's PR5974 and PR5442 for earlier lift
+work; DreamingOfClouds / PR6030 and the retained PR5907/5827/5599 word lineage;
+Chafik Boukhalfa's native channel; icekylinx's retained exact compiler; and Ali
+Romman's independent Gaussian interpreter from PR1862/1931. Further retained
+P104 credit is in [PROOF.md](PROOF.md) and the unchanged source packages.
+Apache-2.0.

research/move-frame-phase-obstruction/SOURCES.json

@@ -0,0 +1,36 @@
+{
+  "schema_version": 1,
+  "base_commit": "2485805a6d47f36ea83ddde6327d453ac82d44dc",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a",
+      "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/p104-helper470-twin-rung-removal/WORD.json.gz",
+      "usage": "input",
+      "git_blob": "22f9ab02d1b73ea0aa4b07ce445a14cc2602c760",
+      "sha256": "7834725d9e34ee846a9ccc615221ea81e0201613938afa185d2eda0c9a6c232f"
+    },
+    {
+      "path": "research/p104-native-channel/vendor/clifford_exact.py",
+      "usage": "input",
+      "git_blob": "166841a037f069249f6f7f6dedb89248812f59e2",
+      "sha256": "2982ead07721e83358dc67c6f49c2b4c16a236a6bebdfd72f58221be1f5d0962"
+    },
+    {
+      "path": "research/p104-native-channel/vendor/native_verify.py",
+      "usage": "input",
+      "git_blob": "2c209dfa9cfade3bc20ac5fc9d876b433a147f8c",
+      "sha256": "3049471905b47b385c88378a1a3be7a18b8858aadd035b8a6da2f4a03b470f38"
+    }
+  ]
+}

research/move-frame-phase-obstruction/TASK.json

@@ -0,0 +1,83 @@
+{
+  "schema_version": 1,
+  "task_id": "uniform-transfer-audit",
+  "priority_revision": 8,
+  "base_commit": "2485805a6d47f36ea83ddde6327d453ac82d44dc",
+  "original_card": {
+    "id": "uniform-transfer-audit",
+    "question": "Can one of the selected record's five inherited assumptions be proved at its actual caller?",
+    "starting_points": [
+      "docs/research/current-priorities.md",
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md"
+    ],
+    "methods": [
+      "Construct and independently check one source-bound instance of the stated first experiment.",
+      "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change."
+    ],
+    "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_selected_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.",
+      "scope": "Source-bound orientation only, not a supplier replay or theorem proof."
+    },
+    "first_experiment": "Choose one assumption ID (native_all_columns, owned_erasure, compiler, precision_tape, analytic_recovery), one quantified implication and exact dependency closure. Check current handoffs, including #5625 row reentry and #5707 root-prefix lowering, without treating their partial scope as the whole theorem. Prove or falsify that implication with a caller-bound argument; stop at the chosen obligation. Finite tests or root digits do not discharge an all-size statement.",
+    "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.",
+    "allowed_variations": [
+      "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes."
+    ],
+    "scope_change_triggers": [
+      "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.",
+      "Treating an archived proposal or local numerical pass as complete supplier admission."
+    ],
+    "overlap_terms": [
+      "native_all_columns",
+      "owned_erasure",
+      "compiler",
+      "precision_tape",
+      "analytic_recovery"
+    ],
+    "existing_checks": [
+      {
+        "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.",
+        "evidence": "research/unconditional-batched-crt/README.md",
+        "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.",
+        "status": "author-checked",
+        "source_commit": "337d04939571a637aeab54a0f58f54fde811663a",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.",
+        "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md",
+        "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.",
+        "status": "reviewed",
+        "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137",
+        "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+      }
+    ]
+  },
+  "scope_status": "refined",
+  "actual_scope": "Prove or refute scalar frame gauges that erase the fixed native MOVE phase tags on the selected PR6030 word, at every column multiplicity.",
+  "scope_change_reason": "Choose native_all_columns and allow a scalar chart phase per frame. The new result is a three-edge obstruction, not a repeat of the predecessor phase census or a discharge of the assumption.",
+  "bottleneck_link": "A frame gauge cannot remove the tensor-phase bookkeeping for all widths; a future native implementation must retain those factors or change its normal forms or compatibility contract.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after one exact cycle obstruction or a consistent frame potential; package the first verified result.",
+  "outcome": "partial",
+  "evidence": "PROOF.md and verify.py: cycle residue 1, ranks 1/2/3, exact -i I loop on 512 basis states, and the iff 4 divides f proof.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Can role-specific phase charts eliminate tags while preserving all actual scalar-gate and endpoint compatibility?",
+      "why_it_matters": "That changes the shared-frame premise of this obstruction and may simplify native phase handling.",
+      "first_step": "Add actual ADD/COPY phase equalities around the three witness occurrences and retain boundary normalizers.",
+      "blocked_by": "No complete role/history compatibility graph or physical scalar bill is supplied."
+    }
+  ]
+}

research/move-frame-phase-obstruction/VERIFY.json

@@ -0,0 +1,38 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/p104-helper470-twin-rung-removal/WORD.json.gz",
+    "research/p104-native-channel/vendor/clifford_exact.py",
+    "research/p104-native-channel/vendor/native_verify.py"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Authenticate sources; compile three edges; check every basis vector of both loops; finite gauge and fault controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Repeat all scientific acceptance and fault controls with Python assertions disabled."
+    }
+  ]
+}