Audit existing phase coverage for selected P104 MOVE maps

research/selected-move-phase-coverage/README.md

@@ -0,0 +1,81 @@
+# Selected MOVE phase coverage: a corrected handoff
+
+**Source-coverage finding with one independent finite operator check; no new κ.** The selected #5599 checker already compares both signed Pauli conjugations and the exact image of `|0>` for every distinct local MOVE pair. The latter fixes absolute phase. Its registered path covers all 3,447 MOVE occurrences (2,887 distinct ordered pairs, including 11 owned occurrences). These are inventory counts, not 3,447 newly replayed operators.
+
+The added value is a correction to the proposed next task in [#5837](https://github.com/CrocSwap/integer-mult-bounds/pull/5837), head `764e7bd6d615d92019445bec92e2a473af021878`. Its [README](https://github.com/unpaidmoon/integer-mult-bounds/blob/764e7bd6d615d92019445bec92e2a473af021878/research/native-scalar-chart-lift/README.md) says the selected native checker “only compares width-1 signed Pauli recipes” and proposes an absolute-phase group-identity census. The existing checker includes that phase comparison. A fresh census should be justified as independent verification of existing coverage, rather than a newly missing algebraic implication. The predecessor's scalar proposition is unaffected, and its physical tape limitation is valid.
+
+Scientific base: canonical main `de5ec2e7a6074068452f45b1a191b5c72832df4a`, priority revision 8. Selected source: #5599, `09dd0965711ca7eeb169057a420abab1c9052137`. Exact bytes are in [SOURCES.json](SOURCES.json). The four execution-chain files below are unchanged between those commits. [TASK.json](TASK.json) records the refined `uniform-transfer-audit` scope. The canonical public context is [the #5837 handoff](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19209962).
+
+## Existing coverage, traced to its entry point
+
+All source links below resolve in the pinned base tree; these are source-inspection findings, not a new execution of the full selected suite.
+
+| Source | What it already does |
+| --- | --- |
+| [VERIFY.json](../p104-helper-subspace-splits/VERIFY.json) | Registers normal and optimized `verify.py`, including native maps. |
+| [verify.py](../p104-helper-subspace-splits/verify.py), `run` and `main` | Authenticates inputs, reconstructs the split word, runs `L.replay(word)` and `L.native(word)`, then structurally compares both reconstructed WORD and RESULT to saved artifacts unless `--write` is explicit. |
+| [local.py](../p104-helper-subspace-splits/local.py), `replay` | Checks every MOVE's current source chart, ownership, nesting and paid rank. |
+| [local.py](../p104-helper-subspace-splits/local.py), `native` | Traverses every MOVE without a public/private exclusion; caches only repeated ordered frame pairs. Lowers `chart(a).adjoint().then(chart(b))`, checks the independent chart circuit and rank, and separately covers helper endpoints and main adapters. |
+| [native_verify.py](../p104-native-channel/vendor/native_verify.py), `equal` | Requires both `tableau(actual) == tableau(expected)` and `state(actual) == state(expected)`. `state` uses exact Gaussian integer pairs and a dyadic denominator, including global phase. |
+| `local.native`, wrong-phase control | Increments the first recipe's left phase modulo four and requires rejection. |
+
+The source circuit order means “execute the old chart's adjoint, then the new chart.” For column vectors the resulting matrix is `C_b C_a^{-1}`. This note does not invert that order.
+
+The [selected proof](../p104-helper-subspace-splits/PROOF.md) already invokes exact phases and all-width frame induction. The [maintainer review](../../docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md) explicitly records signed-Pauli and absolute-phase checks while retaining universal native implementation as an assumption. Its prior complete replay is inherited evidence; it was not rerun here.
+
+## Why this is exact matrix equality, and what lifts
+
+Let `U,V` be invertible operators on `n` binary axes with equal signed conjugations of every `X_j,Z_j`. Then `W = V^{-1}U` commutes with those generators. Commutation with all `Z_j` forces `W` to be diagonal in the computational basis, since different bit strings have different joint eigenvalues. Commutation with each `X_j` equates diagonal entries along every edge of the connected Boolean cube. Hence `W = cI`. Exact equality `U|0> = V|0>` forces `c=1`, because `V|0>` is nonzero. Thus `U=V`, including absolute phase.
+
+Consequently `U^(tensor f) = V^(tensor f)` for every integer `f>=1`. The mixed-product identity also gives `(AB)^(tensor f) = A^(tensor f) B^(tensor f)`, so products and inverses lift gatewise. This elementary implication is already part of [Matarener's #5442 argument](../allwidth-caller-certificate/PROOF.md); no new theorem priority is claimed and its converse/Burnside argument is not needed here.
+
+The premise is the declared width-`f` tensor semantics of the operators. Tensor power is not additive: a width-one linear relation among distinct operators need not lift with fixed external coefficients. Scalar ADD/SCALE coefficients remain outside tensor powers. A central phase that belongs to a native operator remains inside them. This distinction is why the phase check matters, but it does not supply a physical arbitrary-width executor.
+
+## New bounded evidence: the actual first MOVE
+
+Zero-based event 9589 is `["MOVE",224,3,0,false]`, from frame `[]` to `[11]`. Independently of the retained `state` and `tableau` equality routines, [verify.py](verify.py) compares all 512 basis columns of its lowered rank-one recipe with
+
+```text
+U = ((1+i) I + (1-i) X_11 Z_3)/2,
+X_11 |x> = |x xor 11>,   Z_3 |x> = (-1)^(x_0+x_1) |x>.
+```
+
+Bits are numbered from zero. The canonical basis completion has columns `(11,1,2,4,16,32,64,128,256)`. Its diagonal form is `q(x)=2*x_3*(x_0+x_1) mod 4`. With `K=D_q P_G`, the frame is `K C_1 K^{-1}`. Conjugating the nontrivial branch gives `P_G X_1 P_G^{-1}=X_11` and `q(x xor 11)-q(x)=2*(x_0+x_1) mod 4`, proving the displayed formula. Bits 0, 1 and 3 are active; all six untouched bits are included in the exhaustive columns.
+
+The independent recipe evaluator applies its two monomial records directly and adds the two Gaussian numerators over denominator two. The compiler supplies only the candidate recipe; neither its own state evaluator nor the retained interpreter decides the new equality verdict.
+
+All 512 columns match. Incrementing `left.phase` by one changes every column to exactly `iU`; toggling `left.offset` bit zero changes every column and is separately detected. Only after that independent verdict, the retained checker is called diagnostically: the original passes; the phase mutant has the same signed tableau and fails specifically with `phase-only control: exact global phase`. At the origin:
+
+| Address | Original numerator / 2 | Phase mutant numerator / 2 |
+| --- | --- | --- |
+| 0 | `1+i` | `-1+i` |
+| 11 | `1-i` | `1+i` |
+
+[RESULT.json](RESULT.json) is the generated exact receipt. All 3,447 occurrences are counted, but **only this one ordered pair is newly executed**. The general all-width consequence is the written argument, not a finite width sweep.
+
+## Reproduce
+
+CPython 3.12, standard library only, from the repository root:
+
+```sh
+python3 -I -W error -B research/selected-move-phase-coverage/verify.py
+python3 -I -O -W error -B research/selected-move-phase-coverage/verify.py
+python3 -B scripts/research_package.py --package research/selected-move-phase-coverage
+python3 -B scripts/check_research_commit.py --package research/selected-move-phase-coverage --check-source-history
+```
+
+The direct verifier is read-only and works in the official Git-free export. It authenticates every live source before import and isolates import bytecode caches. Expected status is `PASS_INDEPENDENT_FIRST_MOVE_CLOSED_FORM`; normal and optimized receipts agree. [VALIDATION.md](VALIDATION.md) records actual commands/results, internal review and unrun obligations. A source-integrity pass is not a mathematical proof.
+
+## Open next questions
+
+The remaining useful task is physical: bind this same rank-one recipe to an actual arbitrary-width owner/tape interface. Specify the complete input vector, spectators, entry/exit layout and head positions, both monomial normalizers, the rank-one child, owned/borrowed scratch and restoration. Prove that the literal address/phase operations realize its tensor power for every permitted `f`, and attach every preparation, movement, normalization and return charge to the actual caller tariff. Start with this event and its dynamically lowered recipe; stop at the first missing head map, primitive contract or cost inequality. Another width-one group census does not fill that gap.
+
+The current `native` function synthesizes recipes during verification and saves counts plus a recipe-payload hash; it does not emit an arbitrary-width tape program. The older [selected-monomial-tape-lift](../selected-monomial-tape-lift/README.md) and [selected-control-reservations](../selected-control-reservations/README.md) concern #5413's 145-axis caller and provide relevant record/address contracts, not automatic admission of #5599's changed caller. Exact source/layout compatibility must be proved before reuse. No implementation expansion is undertaken or reserved here.
+
+All five selected framework assumptions remain. No full native census, selected cold replay, complete body/controller proof, cost improvement, rounded multiplier, Lean check or physical implementation is claimed. The shared compiler supplies the tested recipe; the closed-form oracle is independent of both state engines but shares the documented monomial grammar. The general checker implementation is not formally verified.
+
+## Credit and review status
+
+Prepared for **DLamdata**, with substantial **OpenAI Codex assistance**, including two native agents for independent mathematical checking and skeptical source review. This is internal AI review, not independent human or proof-kernel review. Apache-2.0.
+
+Credit unpaidmoon for #5837 and the precise follow-up question; Ali Romman for #5599 and the source verification path; Pierre-Loic Doulcet / hexapode for #5565; Mark / Matarener for #5442 and the algebraic/physical distinction; Chris R / Clear1nsight for independent caller/native verification; and Dugongue, icekylinx, David Arias, Cinna Davis, Gareth Davidson, Cao Yifan, zxv, Jacob Alan Sussman and the retained Clifford/controller/compiler lineage. Frozen predecessor files and the selected frontier are unchanged.

research/selected-move-phase-coverage/RESULT.json

@@ -0,0 +1,71 @@
+{
+  "status": "PASS_INDEPENDENT_FIRST_MOVE_CLOSED_FORM",
+  "base": "de5ec2e7a6074068452f45b1a191b5c72832df4a",
+  "word_sha256": "bbb072bced5824a8d9094c49be2fc51fbfdd05fb2b7dab8106e1275053075099",
+  "producer_sha256": "2982ead07721e83358dc67c6f49c2b4c16a236a6bebdfd72f58221be1f5d0962",
+  "checker_sha256": "3049471905b47b385c88378a1a3be7a18b8858aadd035b8a6da2f4a03b470f38",
+  "event_index_zero_based": 9589,
+  "event": [
+    "MOVE",
+    224,
+    3,
+    0,
+    false
+  ],
+  "domain": "all 512 width-one basis columns of the first actual MOVE",
+  "closed_form": "((1+i)I + (1-i)X_11 Z_3)/2",
+  "columns_checked": 512,
+  "phase_fault_columns_detected": 512,
+  "address_fault_columns_detected": 512,
+  "move_occurrences_counted": 3447,
+  "distinct_move_pairs_counted": 2887,
+  "owned_move_occurrences_counted": 11,
+  "newly_replayed_move_pairs": 1,
+  "mutant_relation": "i times original operator",
+  "source_signed_tableau_unchanged": true,
+  "source_rejection": "phase-only control: exact global phase",
+  "origin_column_numerators_over_2": [
+    [
+      0,
+      [
+        1,
+        1
+      ]
+    ],
+    [
+      11,
+      [
+        1,
+        -1
+      ]
+    ]
+  ],
+  "mutant_origin_column_numerators_over_2": [
+    [
+      0,
+      [
+        -1,
+        1
+      ]
+    ],
+    [
+      11,
+      [
+        1,
+        1
+      ]
+    ]
+  ],
+  "new_checker_dependencies": "standard library; source compiler produces fixture; independent direct column formula decides equality before retained verifier diagnostic",
+  "authenticated_inputs": [
+    "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md",
+    "research/allwidth-caller-certificate/PROOF.md",
+    "research/p104-helper-subspace-splits/PROOF.md",
+    "research/p104-helper-subspace-splits/VERIFY.json",
+    "research/p104-helper-subspace-splits/WORD.json.gz",
+    "research/p104-helper-subspace-splits/local.py",
+    "research/p104-helper-subspace-splits/verify.py",
+    "research/p104-native-channel/vendor/clifford_exact.py",
+    "research/p104-native-channel/vendor/native_verify.py"
+  ]
+}

research/selected-move-phase-coverage/SOURCES.json

@@ -0,0 +1,84 @@
+{
+  "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": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md",
+      "usage": "input",
+      "git_blob": "8089de45c78fb229a70ee1587cc90aacaca01ebc",
+      "sha256": "7688e5d8bf40fcdfb5bea43ba47e1f8d60a77a91ede6c307bb8163a9a7e16b3f"
+    },
+    {
+      "path": "research/allwidth-caller-certificate/PROOF.md",
+      "usage": "input",
+      "git_blob": "d9ea1027c4ef5a732d8e3f429695fde5b1fdf738",
+      "sha256": "5f79f819bbafc020cfd5a0e37bed28a067fc16ed5c9f51dee148f4c5e30f7386"
+    },
+    {
+      "path": "research/p104-helper-subspace-splits/PROOF.md",
+      "usage": "input",
+      "git_blob": "ca979984444a431b02b62da7094a3b23d5341742",
+      "sha256": "f4c68acf9373e34d88e14e1a7791b4b739c8b5297a1ae4c0121f579a02fde04e"
+    },
+    {
+      "path": "research/p104-helper-subspace-splits/VERIFY.json",
+      "usage": "input",
+      "git_blob": "f02fe9b97043e626e9906346d230508247a5871d",
+      "sha256": "30499c00a5c6a9718561a152e8008ce1a765535647306dc4b2d2a7ce78b7b2ac"
+    },
+    {
+      "path": "research/p104-helper-subspace-splits/WORD.json.gz",
+      "usage": "input",
+      "git_blob": "e325091e3051afe37a2d9c82f85afe9028510edb",
+      "sha256": "bbb072bced5824a8d9094c49be2fc51fbfdd05fb2b7dab8106e1275053075099"
+    },
+    {
+      "path": "research/p104-helper-subspace-splits/local.py",
+      "usage": "input",
+      "git_blob": "e6e28bacdad7cb51400d827b9a6e02f2b605d357",
+      "sha256": "ef430511ce36fc658ab711bd84cd2d7b484b8af173238ff89cbfec6139fefbad"
+    },
+    {
+      "path": "research/p104-helper-subspace-splits/verify.py",
+      "usage": "input",
+      "git_blob": "547751915ad09b2229bacf29af02241b0ef29696",
+      "sha256": "f79c78d009d8a88bc5721644237074569fbb992fe7e49784f4b0c0a97523ea91"
+    },
+    {
+      "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"
+    },
+    {
+      "path": "research/selected-monomial-tape-lift/README.md",
+      "usage": "provenance",
+      "git_blob": "94e47cea4427ed0072f8283f431793b52601be9b",
+      "sha256": "f34e186a0576eea5b15b5d2368274cc77c96d2150e8a3d3fbd67275e020c8a3f"
+    },
+    {
+      "path": "research/selected-control-reservations/README.md",
+      "usage": "provenance",
+      "git_blob": "2ff556a541a32274ed88a85801d3f3b77138de43",
+      "sha256": "cccf5d032f5bdaa7e1f6d331e882d27108b473216a4cdd68e83647ef0312f259"
+    }
+  ]
+}