From 36167d06b6b75436f0d299da3abb07907807d2ae Mon Sep 17 00:00:00 2001 From: Matarener <52912325+Matarener@users.noreply.github.com> Date: Sat, 24 Oct 2026 18:24:42 +0300 Subject: [PATCH 1/2] Realize the selected caller's monomials and J routes as fixed f-independent record lists (no new kappa) Record-level part of the physical half of native_all_columns for the selected #5413 caller (the half left open by #5442), following SPECIALIZATION.md s2-s3: - each of the 896 port wrappers of NORMALIZERS.json is a fixed list of at most 107 records (grammar bound 171): compact-control selected-bit additions and translations (movement records) and unit-S / controlled-sign / global-i phase records; the list is independent of f and executes the lift m^(tensor f) exactly with spectators untouched (f=1 exhaustive on all wrappers, f=2 exhaustive on two, f=2..4 sampled, engine agreement with clifford_exact); - the central translation X0 is one record; C0 and D are positive-rank children; - the literal pre/post SWAP_BITS words of all 119 plan targets (16,748 swaps on 145 axes) are three XROW records each and realize the declared permutations. The tariff per movement record is the compact-control Proposition in its domain f <= p, which SPECIALIZATION s3 identifies with the actual layer's domain. Co-Authored-By: Claude Fable 5.1 --- research/selected-monomial-tape-lift/PROOF.md | 92 ++++++ .../selected-monomial-tape-lift/README.md | 68 ++++ .../selected-monomial-tape-lift/RESULT.json | 118 +++++++ .../selected-monomial-tape-lift/SOURCES.json | 60 ++++ .../selected-monomial-tape-lift/TASK.json | 107 +++++++ .../selected-monomial-tape-lift/VERIFY.json | 35 ++ research/selected-monomial-tape-lift/lift.py | 303 ++++++++++++++++++ .../test_verify.py | 111 +++++++ .../selected-monomial-tape-lift/verify.py | 125 ++++++++ 9 files changed, 1019 insertions(+) create mode 100644 research/selected-monomial-tape-lift/PROOF.md create mode 100644 research/selected-monomial-tape-lift/README.md create mode 100644 research/selected-monomial-tape-lift/RESULT.json create mode 100644 research/selected-monomial-tape-lift/SOURCES.json create mode 100644 research/selected-monomial-tape-lift/TASK.json create mode 100644 research/selected-monomial-tape-lift/VERIFY.json create mode 100644 research/selected-monomial-tape-lift/lift.py create mode 100644 research/selected-monomial-tape-lift/test_verify.py create mode 100644 research/selected-monomial-tape-lift/verify.py diff --git a/research/selected-monomial-tape-lift/PROOF.md b/research/selected-monomial-tape-lift/PROOF.md new file mode 100644 index 0000000000..0498baefbb --- /dev/null +++ b/research/selected-monomial-tape-lift/PROOF.md @@ -0,0 +1,92 @@ +# The f-column lift of the selected caller's monomials as a fixed record list + +Scope: the physical half of `native_all_columns` for the selected #5413 caller, at the level +of records. PR #5442 closes the algebraic half (every identity of the caller lifts to every +column width `f`) and leaves open the tape realization of `g^(tensor f)` with spectators and +adapters at the retained tariff. `SPECIALIZATION.md` §2–§3 (the P1 specialization of #4610) +states the realization in writing: any nine-axis monomial has a recipe of at most 171 +retained elementary movement/phase records, each a compact-control selected-bit addition or +a per-record phase, acting on all `f` columns with one fixed list of primitive types. This +package executes that recipe for the caller's actual monomials and routes. + +## Setting + +A field with `f` columns on `n` logical axes has addresses `X = (x_1, ..., x_f)`, `x_j` in +`F_2^n`, next to arbitrary spectator bits. The retained monomial convention +(`prune_native.monomial`) is `m = (G, b, Q, alpha, a)` acting on one column as + +``` +|x> -> i^(a + q(x)) |G x xor b>, q(x) = sum_i alpha_i x_i + 2 sum_(i -> i^(a f + sum_j q(x_j)) |(G x_1 xor b, ..., G x_f xor b)>`. + +Five record types, each acting on all `f` columns at once and on no spectator bit: + +| record | action | retained primitive | +|---|---|---| +| `XROW(i,k)` | `x_{j,i} ^= x_{j,k}` for every column `j` | compact-control selected-bit addition, slots `k -> i` (movement-paid) | +| `NOT(i)` | `x_{j,i} ^= 1` for every column `j` | selected-bit translation (movement-paid) | +| `S(i)` | phase `i^(sum_j x_{j,i})` | unit-S phase record | +| `CZ(i,k)` | phase `(-1)^(sum_j x_{j,i} x_{j,k})` | controlled-sign phase record | +| `I` | phase `i^f` | global `i` record, lifted to `i^f` | + +A row swap is three `XROW` records. `SWAP_BITS(i,k)` of the plan is a row swap. + +## Lemma (record realization, uniform in f) + +For every monomial `m` the list `R(m)` = [`alpha_i` copies of `S(i)` for each `i`; `CZ(i,k)` for +each `i= 1`, leaving every spectator bit unchanged. + +*Proof.* Each record is the `f`-fold product of the same one-column operation, applied to +the columns independently (`XROW`, `NOT` act column by column; `S`, `CZ`, `I` add a phase that +is a sum over columns, with the global record contributing `f`). So the composition of the +list on `X` is the `f`-fold product of its composition on one column, and the phase is the +sum of the one-column phases plus `a f`. On one column: the phase records applied first on the +input address give `i^(q(x))` (the diagonal `Q` is carried by `alpha`, exactly as in the +convention); Gaussian elimination gives elementary matrices `E_1, ..., E_r` with +`E_r ... E_1 G = I`, hence `G = E_1 ... E_r` (each elementary matrix is an involution), and +applying `E_r` first and `E_1` last maps `x` to `G x`; the translations give `xor b`; the +global records give `i^a`. The bounds are those of SPECIALIZATION §2: at most 72 additions +and 8 swaps (24 records), 9 translations, 27 unit-S, 36 controlled-sign and 3 global +records. No record reads or writes a spectator bit. ∎ + +Cost. Each `XROW` or `NOT` record is one compact-control selected-bit addition on the ordered +pair of slots (`compact-control-movement.tex`, Proposition), costing `O(V((f log p)^tau + 1))` +on a fixed number of tapes in the domain `f <= p`, `A = O(p)`, `K / log p -> infinity`, with +the front/back control fields reserved as in `compact-control-layout.tex` ("the proposition +applies to every ordered pair of slots"). A phase record computes a fixed degree-two residue +from `O(f)` selected address bits per complete record and applies one of `{1, i, -1, -i}` +(SPECIALIZATION §2); it is absorbed by the record fiber. The domain `f <= p` is the actual +layer's own domain: `f <= e <= floor(b_in^epsilon)` and `p = 6 b_in` (SPECIALIZATION §3). The +tariff per record is inherited from the Proposition, not re-derived here. + +## What is executed (`verify.py`) + +- The 896 compiled port wrappers of `NORMALIZERS.json` (112 ports x 8 orientations/paths): + the record list is executed on all 512 addresses at `f = 1` (and compared with the exact + Clifford engine's basis action on one wrapper per path), on all 262,144 addresses at `f = 2` + for two wrappers, and on 48 random addresses at `f = 2, 3, 4` for every wrapper, with random + spectator bits. Every wrapper is within the §2 bound; the largest list has 107 records + (69 movement, 38 phase). +- The central translation `X0` is one `NOT(0)` record. `C0` (cgate on axis 0) and `D` + (Fourier on axes 1..8) are positive-rank Gaussians: in the retained framework they are paid + children of the recursion (`FINITE-PRECOMPILATION.md` §1, "one ordinary positive rank-r f + child on the actual owner's full stream"), not adapters, and no record list is claimed for them. +- The literal `pre_word` and `post_word` of all 119 targets of `WHOLECALLER-PLAN-v1` + (32 main, 72 helper, 15 idle), 16,748 `SWAP_BITS` events in all, are executed as `XROW` + records on 145-axis addresses at `f = 2`; each word realizes the declared `permutation` or + `inverse_permutation` of its target with phase zero and spectators untouched. The 16 + central `X` corrections of negative `Q` powers are `NOT(0)` records. + +## What is not claimed + +The Proposition's proof (the four-update rotation scheme with dirty compact fields, its +overflow repair and the chunk-swap primitive) is not executed; the reservations of the control +fields for the 145-axis layout are taken from `compact-control-layout.tex` as written. No +numerical tariff, no new κ, no change to the selected record. The 400 helper alias monomials +of #5442 are products of wrapper pairs and are covered by the wrapper lists; the forward body +is not replayed. diff --git a/research/selected-monomial-tape-lift/README.md b/research/selected-monomial-tape-lift/README.md new file mode 100644 index 0000000000..a988c3a0c8 --- /dev/null +++ b/research/selected-monomial-tape-lift/README.md @@ -0,0 +1,68 @@ +# The selected caller's monomials and J routes as fixed, f-independent record lists + +**Scoped positive result; no new κ.** PR #5442 (`allwidth-caller-certificate`) splits +`native_all_columns` for the selected #5413 caller into an algebraic half, which it closes, +and a physical half: executing `g^(tensor f)` and the port adapters on a fixed number of +tapes, for all `f` columns at once with one fixed primitive list, without disturbing +spectators, at the retained tariff. This package executes the record-level part of that +physical half, following the written realization of `SPECIALIZATION.md` §2–§3: + +- every one of the **896 port wrappers** is a fixed list of at most 107 records (the §2 bound + is 171), each an `XROW` / `NOT` movement record (one compact-control selected-bit addition + or translation) or a phase record (`S`, `CZ`, global `i`); the list is independent of `f` + and realizes the lift `m^(tensor f)` exactly, spectators untouched; +- the **central translation** `X0` is one record; `C0` and `D` are positive-rank children of + the recursion, not adapters; +- the **16,748 `SWAP_BITS` events** of the plan's 119 `J` routes (main, helper and idle + targets) are three `XROW` records each and realize the declared 145-axis permutations; + the 16 central `X` corrections are one record each. + +The tariff per movement record is the compact-control Proposition +(`notes/compact-control-movement.tex`): `O(V((f log p)^tau + 1))` on fixed tapes for +`f <= p`, `A = O(p)`. That domain is the actual layer's domain (`f <= e <= b_in^epsilon`, +`p = 6 b_in`, SPECIALIZATION §3), so the restriction `f <= p` is not a gap. What remains +inherited is the Proposition's own proof and the control-field reservations of the 145-axis +layout (`compact-control-layout.tex`). [PROOF.md](PROOF.md) has the lemma and its scope. + +## Evidence (`verify.py`, standard library, CPython 3.12) + +| check | coverage | +|---|---| +| wrappers, `f = 1`, exhaustive | 896 x 512 addresses, random spectators | +| wrappers, engine agreement | 8 wrappers x 512 basis states against `clifford_exact` | +| wrappers, `f = 2`, exhaustive | 2 wrappers x 262,144 addresses | +| wrappers, `f = 2, 3, 4`, sampled | 896 x 48 addresses each | +| `X0` | one `NOT(0)` record, `f = 3` | +| `J` routes | 119 targets x (pre, post) literal words, 145 axes, `f = 2`, 12 addresses each | +| controls (`test_verify.py`) | unlifted global phase fails at `f = 2`; a dropped row addition, a removed swap, a single-column phase record and an asymmetric `Q` are rejected; spectators untouched | + +Record totals over the 896 wrappers and the maxima are in RESULT.json. + +```sh +python3.12 -B scripts/research_package.py --package research/selected-monomial-tape-lift +``` + +## Relation to `lockstep-completion-pass` + +That package counts the records the compiler and the completion/splitting pass add per unit +instance (normalizer pairs, relocations, child calls, bank scans) without pricing them. This +package gives the record list and count of each normalizer and route of the selected caller. +Together they give the record-level bill of the compiled template; the price per record is the +Proposition's tariff in its domain. + +## Open next questions + +1. Execute the Proposition itself: a bit-level simulator of the four-update rotation scheme + with dirty compact fields `u, t, b`, the chunk swaps and the overflow repair, at small + `f, K, G`, checking exact XOR at the `f` selected positions and restoration of the fields. +2. Verify the control-field reservations of `compact-control-layout.tex` for the 145-axis + plan layout (front fields before, back field after every active slot pair). +3. Replay the forward body's wrappers (review only; the selected controller runs the backward body). + +## Credit + +Cao Yifan / intqwq (#4610 and the P1 specialization), Cinna Davis (compact-control notes +and the controller/helper lineage), zxv (#4359 free-word substitution, #5428), Chris R / +Clear1nsight (#5413), Dillon (#5402), Ali Romman (#5383/#5398/#5376), Dugongue and icekylinx +(Clifford engine lineage), and the parallel #5442 census. Prepared by Mark (Matarener) with +substantial Claude Code assistance. Apache-2.0. No independent human or formal-kernel review. diff --git a/research/selected-monomial-tape-lift/RESULT.json b/research/selected-monomial-tape-lift/RESULT.json new file mode 100644 index 0000000000..62d6329046 --- /dev/null +++ b/research/selected-monomial-tape-lift/RESULT.json @@ -0,0 +1,118 @@ +{ + "status": "PASS", + "bindings": 12, + "wrappers": { + "count": 896, + "max_records": { + "XROW": 60, + "NOT": 9, + "S": 22, + "CZ": 15, + "I": 3, + "movement_records": 69, + "phase_records": 40, + "total": 107 + }, + "sum_records": { + "XROW": 19548, + "NOT": 2380, + "S": 8960, + "CZ": 1204, + "I": 1120, + "movement_records": 21928, + "phase_records": 11284, + "total": 33212 + }, + "bound_s2": 171, + "histogram_total": { + "16": 19, + "19": 133, + "20": 25, + "21": 19, + "22": 156, + "23": 58, + "24": 52, + "27": 6, + "28": 44, + "31": 104, + "36": 7, + "39": 14, + "40": 7, + "43": 14, + "47": 11, + "50": 4, + "51": 14, + "54": 6, + "56": 2, + "58": 15, + "59": 3, + "60": 3, + "61": 2, + "62": 18, + "65": 2, + "67": 8, + "69": 18, + "71": 5, + "72": 5, + "73": 23, + "76": 24, + "78": 9, + "80": 6, + "82": 7, + "85": 15, + "86": 4, + "88": 8, + "91": 5, + "99": 6, + "104": 7, + "107": 8 + } + }, + "central": { + "X0_records": { + "XROW": 0, + "NOT": 1, + "S": 0, + "CZ": 0, + "I": 0, + "movement_records": 1, + "phase_records": 0, + "total": 1 + }, + "C0_and_D": "positive-rank children (cgate, fourier), not monomials" + }, + "routes": { + "targets": 119, + "swap_bits_events": { + "main_targets": 3776, + "helper_targets": 10116, + "idle_jobs": 2856 + }, + "xrow_records": { + "main_targets": 11328, + "helper_targets": 30348, + "idle_jobs": 8568 + }, + "central_X_records": 16, + "conventions": { + "pre:permutation": 81, + "post:inverse_permutation": 81, + "pre:inverse_permutation|permutation": 23, + "post:inverse_permutation|permutation": 23, + "pre:inverse_permutation": 15, + "post:permutation": 15 + } + }, + "checks": { + "f1_exhaustive_wrappers": 896, + "f2_exhaustive_wrappers": 2, + "sampled_f": [ + 2, + 3, + 4 + ], + "engine_agreement_wrappers": 8, + "route_f": 2, + "route_addresses": 12 + } +} diff --git a/research/selected-monomial-tape-lift/SOURCES.json b/research/selected-monomial-tape-lift/SOURCES.json new file mode 100644 index 0000000000..45645ad3ce --- /dev/null +++ b/research/selected-monomial-tape-lift/SOURCES.json @@ -0,0 +1,60 @@ +{ + "schema_version": 1, + "base_commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "fc3d4ba105e1f097d0d7d051a308281e86ab1446", + "sha256": "66974efdced4083c00025f97d95d83909a226cdf801edb9301c195c6641f6903" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "notes/compact-control-layout.tex", + "usage": "input", + "git_blob": "16f4d233471a7d189163ae7e7902becadecbba64", + "sha256": "2bc28e50f3eb092195294cafa81213e520f6d42e7935e9905ad8a6199e2a7c87" + }, + { + "path": "notes/compact-control-movement.tex", + "usage": "input", + "git_blob": "06b6a9ef24245ac7b724c53a204635415b402357", + "sha256": "b963c3d2f4e1b7059aa289bb4b4ac89b688920bcf42f5b20d7698cdef0132cc6" + }, + { + "path": "research/coupled-helper-neutral-completion/capsule/workspace/swarm-coupled-caller-sol-high-20261024/agents/challenge/WHOLECALLER-PLAN-v1.json", + "usage": "input", + "git_blob": "b868fe46ce7ff96a51f7b612758685a23014d31d", + "sha256": "a02e79fb4615f4f987e3b3617c2b42eea2c1d7415cc66fa702a8b0cd28e6387e" + }, + { + "path": "research/coupled-helper-neutral-completion/capsule/workspace/swarm-provider-audit-sol-high-20261024/agents/budget/inputs/NORMALIZERS.json", + "usage": "input", + "git_blob": "bca92c222c395d3d75c047fbb678f3cd0947c60f", + "sha256": "ae8aad06aa5d1811d725895b3ab5a4f4daa9dcdd88294aa0d5f723e78bb1e0da" + }, + { + "path": "research/final4610-independent-admission/SPECIALIZATION.md", + "usage": "input", + "git_blob": "7ee84b30892f7354e1c36611f1a5e9b082dc6147", + "sha256": "70430114f744108223bc1d44b98bc25b696c4b408b7b044c2a8bbdfdb434ac5c" + }, + { + "path": "research/kappa-function-composition/complex/prune_native.py", + "usage": "input", + "git_blob": "8c3e11b2408fa96eefa3ebe7952d1b11b90b772b", + "sha256": "f2b37c183a10922eabc8e0436b426a08866430e96bd0adc7e178951c7fbb5257" + }, + { + "path": "research/t74-native-fast/vendor/native/new/code/borrow/vendor/clifford/clifford_exact.py", + "usage": "input", + "git_blob": "166841a037f069249f6f7f6dedb89248812f59e2", + "sha256": "2982ead07721e83358dc67c6f49c2b4c16a236a6bebdfd72f58221be1f5d0962" + } + ] +} diff --git a/research/selected-monomial-tape-lift/TASK.json b/research/selected-monomial-tape-lift/TASK.json new file mode 100644 index 0000000000..4b0abe02fc --- /dev/null +++ b/research/selected-monomial-tape-lift/TASK.json @@ -0,0 +1,107 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 7, + "base_commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04", + "original_card": { + "id": "formal-interface-lemma", + "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/gate-operand-parity-lean/README.md", + "research/staged544-certified-endpoint/README.md", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Formalize a missing boundary lemma identified by the selected review.", + "Audit a formal theorem-to-certificate binding independently." + ], + "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Inventory the gate-operand parity lemma (#3807) and certified endpoint arithmetic (#3857). Neither is a full multiplication proof. For #4100, audit the compact-switch statement and its hypotheses before formalizing it.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.", + "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.", + "allowed_variations": [ + "Narrow to one formal lemma or one theorem-to-certificate binding." + ], + "scope_change_triggers": [ + "Formalizing already-covered arithmetic and claiming the full multiplication theorem." + ], + "overlap_terms": [ + "hyperplane end", + "formal interface", + "Lean binding", + "3807", + "3857", + "4100", + "gate-operand-parity-lean", + "staged544-certified-endpoint", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #3807: scoped gate-operand parity formalization.", + "evidence": "research/gate-operand-parity-lean/README.md", + "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.", + "status": "author-checked", + "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #3857: certified real-power moment/endpoint arithmetic.", + "evidence": "research/staged544-certified-endpoint/README.md", + "remaining": "Uniform algorithmic implications, not another endpoint digit.", + "status": "author-checked", + "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4100: compact-switch formalization proposed as future validation.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Audit the statement and assumptions before a formal proof campaign.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "refined", + "actual_scope": "Record-level realization of the f-column lift of the selected #5413 caller's monomials and J routes: every port wrapper, the central translation and every literal SWAP_BITS word is an f-independent list of compact-control selected-bit records and phase records that executes m^(tensor f) exactly with spectators untouched; tariff per record inherited from the compact-control Proposition in its domain f<=p, which is the actual layer's domain.", + "scope_change_reason": "PR #5442 closed the algebraic half of native_all_columns for this caller and named its physical half as the open interface; SPECIALIZATION.md s2-s3 states the realization in writing. This executes it on the actual inventory.", + "bottleneck_link": "Side result for the native_all_columns premise: the all-f adapters of the selected caller are executed records of the retained primitive; it does not move the frontier.", + "budget_minutes": 240, + "stop_rule": "Stop after executing all 896 wrappers (f=1 exhaustive, f=2 exhaustive on two, f=2..4 sampled), X0 and all 119 plan routes at f=2; do not simulate the Proposition's internal rotation scheme or re-derive the tariff.", + "outcome": "completed", + "evidence": "PROOF.md (record lemma, uniform in f); verify.py binds SPECIALIZATION s2-s3, the Proposition and the monomial convention, executes the record lists against the lift formula and the exact Clifford engine, and freezes RESULT.json; test_verify.py has rejecting controls.", + "author": "Mark (Matarener)", + "ai_assistance": "Prepared with substantial Claude Code (Claude) assistance.", + "open_questions": [ + { + "question": "Does a bit-level simulation of the compact-control rotation scheme (dirty fields u,t,b, chunk swaps, overflow repair) reproduce the exact selected-bit XOR and restoration at small f, K, G?", + "why_it_matters": "The per-record tariff rests on that written Proposition; executing it would make the physical half fully literal.", + "first_step": "Implement the four modular updates on the y slot and t digits with random dirty contents and check the parity toggle and restoration.", + "blocked_by": "none" + }, + { + "question": "Are the front/back control-field reservations of compact-control-layout.tex available in the 145-axis plan layout for every active slot pair?", + "why_it_matters": "The Proposition applies per ordered slot pair only with those fields present.", + "first_step": "Map the plan's active_axes and stage planes onto the q_0, q_F, q_B chunk reservation.", + "blocked_by": "none" + }, + { + "question": "Do the forward-body wrappers have the same record bounds?", + "why_it_matters": "Review completeness; the selected controller runs the backward body.", + "first_step": "Load NEUTRAL-FORWARD-v16c wrappers and rerun the lists.", + "blocked_by": "none" + } + ] +} diff --git a/research/selected-monomial-tape-lift/VERIFY.json b/research/selected-monomial-tape-lift/VERIFY.json new file mode 100644 index 0000000000..2183158aaa --- /dev/null +++ b/research/selected-monomial-tape-lift/VERIFY.json @@ -0,0 +1,35 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "notes/compact-control-layout.tex", + "notes/compact-control-movement.tex", + "research/coupled-helper-neutral-completion/capsule/workspace/swarm-coupled-caller-sol-high-20261024/agents/challenge/WHOLECALLER-PLAN-v1.json", + "research/coupled-helper-neutral-completion/capsule/workspace/swarm-provider-audit-sol-high-20261024/agents/budget/inputs/NORMALIZERS.json", + "research/final4610-independent-admission/SPECIALIZATION.md", + "research/kappa-function-composition/complex/prune_native.py", + "research/t74-native-fast/vendor/native/new/code/borrow/vendor/clifford/clifford_exact.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 600, + "checks": "Bind SPECIALIZATION s2-s3, the compact-control Proposition, the layout note and the monomial convention; execute the record lists of all 896 wrappers (f=1 exhaustive, f=2 exhaustive on two, f=2..4 sampled, engine agreement), X0, and the literal SWAP_BITS words of all 119 plan targets at f=2 on 145 axes; RESULT.json comparison." + }, + { + "argv": [ + "{python}", + "-B", + "{package}/test_verify.py" + ], + "timeout_seconds": 300, + "checks": "Rejecting controls: unlifted global phase, dropped row addition, removed swap, single-column phase record, asymmetric Q, spectator preservation, transposition chain, RESULT status." + } + ] +} diff --git a/research/selected-monomial-tape-lift/lift.py b/research/selected-monomial-tape-lift/lift.py new file mode 100644 index 0000000000..10950518af --- /dev/null +++ b/research/selected-monomial-tape-lift/lift.py @@ -0,0 +1,303 @@ +"""Record-level realization of the f-column lift of the selected caller's monomials. + +Model (SPECIALIZATION.md s2-s3, compact-control-movement.tex). An address of a field with +f columns on n logical axes is X = (x_1, ..., x_f), x_j in F_2^n, plus arbitrary spectator +bits. A monomial m = (G, b, Q, alpha, a) acts on one column as + |x> -> i^(a + q(x)) |G x xor b>, q(x) = sum_i alpha_i x_i + 2 sum_{i -> i^(a f + sum_j q(x_j)) |(G x_1 xor b, ..., G x_f xor b)>. + +Tape records. Every record acts on all f columns at once and never reads or writes a +spectator bit; each is one retained primitive type: + XROW(i, k) x_{j,i} ^= x_{j,k} for every column j (compact-control selected-bit addition, + slots k -> i; movement-paid) + NOT(i) x_{j,i} ^= 1 for every column j (selected-bit translation; movement-paid) + S(i) phase i^(sum_j x_{j,i}) (unit-S phase record) + CZ(i, k) phase (-1)^(sum_j x_{j,i} x_{j,k}) (controlled-sign phase record) + I phase i^f (global i record, lifted to i^f) +A row swap is three XROW records. The record list of a monomial is independent of f. + +This module builds the record list of a monomial by Gaussian elimination (the grammar of +SPECIALIZATION.md s2), executes it on explicit addresses with the phase accumulated modulo 4, +and compares with the lift formula; it also realizes 145-axis axis permutations (the plan's +J routes) as transposition chains of XROW records. Standard library only. +""" +import importlib.util +import json +import random +from collections import Counter +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +CAP = ROOT / "research/coupled-helper-neutral-completion/capsule/workspace" +NORM = CAP / "swarm-provider-audit-sol-high-20261024/agents/budget/inputs/NORMALIZERS.json" +PLAN = CAP / "swarm-coupled-caller-sol-high-20261024/agents/challenge/WHOLECALLER-PLAN-v1.json" +CLIFFORD = ROOT / "research/t74-native-fast/vendor/native/new/code/borrow/vendor/clifford/clifford_exact.py" +N9 = 9 +N145 = 145 + + +def load_clifford(): + spec = importlib.util.spec_from_file_location("tape_lift_clifford_exact", CLIFFORD) + ce = importlib.util.module_from_spec(spec) + spec.loader.exec_module(ce) + return ce + + +# ------------------------------------------------------------------ monomials +def parity(x): + return x.bit_count() & 1 + + +def mv(rows, x): + return sum(parity(r & x) << i for i, r in enumerate(rows)) + + +def qvalue(Q, alpha, x, n): + return (sum(alpha[i] for i in range(n) if x >> i & 1) + + 2 * sum(parity((Q[i] >> (i + 1)) & (x >> (i + 1))) for i in range(n) if x >> i & 1)) % 4 + + +class Monomial: + def __init__(self, n, matrix_rows, offset, quadratic_rows, linear_Z4, phase): + self.n = n + self.G = tuple(matrix_rows) + self.b = offset + self.Q = tuple(quadratic_rows) + self.alpha = tuple(linear_Z4) + self.a = phase % 4 + assert len(self.G) == len(self.Q) == len(self.alpha) == n + for i in range(n): + assert self.alpha[i] % 2 == (self.Q[i] >> i) & 1, "Z4 linear parity equals the Q diagonal" + for j in range(n): + assert (self.Q[i] >> j) & 1 == (self.Q[j] >> i) & 1, "symmetric Q" + + @classmethod + def from_recipe(cls, r, n=N9): + return cls(n, r["matrix_rows"], r["offset"], r["quadratic_rows"], r["linear_Z4"], r["phase"]) + + @classmethod + def from_axis_permutation(cls, perm, n): + """x -> x' with x'_{perm[i]} = x_i, i.e. axis i moves to axis perm[i] (a J route).""" + rows = [0] * n + for i, t in enumerate(perm): + rows[t] |= 1 << i + return cls(n, rows, 0, [0] * n, [0] * n, 0) + + def one_column(self, x): + """(image address, phase mod 4) of one column.""" + return mv(self.G, x) ^ self.b, qvalue(self.Q, self.alpha, x, self.n) + + def lift(self, X, f): + """(image, phase) of the lifted monomial on X = list of f column addresses.""" + img, ph = [], (self.a * f) % 4 + for x in X: + y, p = self.one_column(x) + img.append(y) + ph = (ph + p) % 4 + return img, ph + + # -------------------------------------------------------------- the record grammar + def records(self): + """Record list realizing the monomial (f-independent). Order of application: + phase records on the input address, then the row operations of G, then translations, + then the global i records.""" + n = self.n + out = [] + for i in range(n): + out += [("S", i)] * self.alpha[i] + for i in range(n): + for k in range(i + 1, n): + if (self.Q[i] >> k) & 1: + out.append(("CZ", i, k)) + # Gaussian elimination of G to the identity; the reversed op list realizes G + M = list(self.G) + ops = [] + for col in range(n): + piv = next(r for r in range(col, n) if (M[r] >> col) & 1) + if piv != col: + M[piv], M[col] = M[col], M[piv] + ops.append(("SWAP", piv, col)) + for r in range(n): + if r != col and (M[r] >> col) & 1: + M[r] ^= M[col] + ops.append(("XROW", r, col)) # row r ^= row col + assert M == [1 << i for i in range(n)] + for op in reversed(ops): + if op[0] == "SWAP": + _, i, k = op + out += [("XROW", i, k), ("XROW", k, i), ("XROW", i, k)] + else: + out.append(op) + for i in range(n): + if (self.b >> i) & 1: + out.append(("NOT", i)) + out += [("I",)] * self.a + return out + + +def record_counts(recs): + c = Counter(r[0] for r in recs) + return {"XROW": c["XROW"], "NOT": c["NOT"], "S": c["S"], "CZ": c["CZ"], "I": c["I"], + "movement_records": c["XROW"] + c["NOT"], "phase_records": c["S"] + c["CZ"] + c["I"], "total": len(recs)} + + +# ------------------------------------------------------------------ tape execution on addresses +def execute(recs, X, f, spectators): + """Apply the record list to the f column addresses X (list of ints) with spectator bits. + Returns (new X, phase mod 4, spectators) -- spectators are carried, never touched.""" + X = list(X) + ph = 0 + for r in recs: + t = r[0] + if t == "XROW": + _, i, k = r + for j in range(f): + X[j] ^= ((X[j] >> k) & 1) << i + elif t == "NOT": + i = r[1] + for j in range(f): + X[j] ^= 1 << i + elif t == "S": + i = r[1] + ph = (ph + sum((X[j] >> i) & 1 for j in range(f))) % 4 + elif t == "CZ": + _, i, k = r + ph = (ph + 2 * sum(((X[j] >> i) & 1) & ((X[j] >> k) & 1) for j in range(f))) % 4 + elif t == "I": + ph = (ph + f) % 4 + else: + raise ValueError(r) + return X, ph, spectators + + +def check_monomial(m, f, addresses, spectator_bits=3, rng=None): + """Execute the record list on the given column-address tuples and compare with the lift.""" + recs = m.records() + rng = rng or random.Random(0) + for X in addresses: + spec = rng.getrandbits(spectator_bits) + got_X, got_ph, got_spec = execute(recs, X, f, spec) + want_X, want_ph = m.lift(X, f) + if got_X != want_X or got_ph != want_ph or got_spec != spec: + return False, {"X": X, "got": (got_X, got_ph), "want": (want_X, want_ph)} + return True, record_counts(recs) + + +def all_addresses(n, f): + N = 1 << n + if f == 1: + return [[x] for x in range(N)] + if f == 2: + return [[x, y] for x in range(N) for y in range(N)] + raise ValueError("exhaustive only for f <= 2") + + +def random_addresses(n, f, count, seed): + rng = random.Random(seed) + return [[rng.getrandbits(n) for _ in range(f)] for _ in range(count)] + + +# ------------------------------------------------------------------ inventory of the selected caller +def wrappers(): + nz = json.loads(NORM.read_text(encoding="utf-8")) + out = [] + for p, port in enumerate(nz["ports"]): + for name, w in sorted(port["compiled_wrappers"].items()): + out.append((f"port{p}:{name}", Monomial.from_recipe(w["recipe"]))) + return out + + +def central_elements(ce): + """C0 = cgate on axis 0 and X0 = xgate on axis 0 are not monomials in prune_native's sense + (cgate is a rank-one Gaussian); only X0 is a translation record. We return X0 and the + diagonal unit-S / Z elements used by the plan (phase records).""" + return [("X0", Monomial(N9, [1 << i for i in range(N9)], 1, [0] * N9, [0] * N9, 0))] + + +def plan_words(): + """The 145-axis J routes of WHOLECALLER-PLAN-v1: for every main/helper/idle target its literal + pre_word and post_word (lists of SWAP_BITS events), the declared permutation and inverse, + and whether a central X follows the LEFT boundary (the correction of a negative Q power).""" + plan = json.loads(PLAN.read_text(encoding="utf-8")) + out = [] + for kind in ("main_targets", "helper_targets", "idle_jobs"): + for idx, t in enumerate(plan[kind]): + for key in ("pre_word", "post_word"): + assert all(ev[0] == "SWAP_BITS" and len(ev) == 3 for ev in t[key]), (kind, idx, key) + assert t["affine_translation"] == [] and t["absolute_phase"] == 0, "J routes are plain permutations" + out.append({"name": f"{kind}[{idx}] rank {t['rank']}", "kind": kind, "pre": t["pre_word"], "post": t["post_word"], + "perm": tuple(t["permutation"]), "inv": tuple(t["inverse_permutation"]), + "central_X": bool(t.get("central_X_after_LEFT", False))}) + return out + + +def swap_records(word): + """SWAP_BITS(i, k) is the row swap of axes i and k: three XROW records.""" + recs = [] + for _, i, k in word: + recs += [("XROW", i, k), ("XROW", k, i), ("XROW", i, k)] + return recs + + +def check_word(word, perm, inv, f, count, seed, n=N145): + """Execute the literal SWAP_BITS word as XROW records and identify which declared axis + permutation it realizes (the plan's `permutation` or `inverse_permutation`). + Returns (ok, convention, record counts).""" + recs = swap_records(word) + cands = {"permutation": Monomial.from_axis_permutation(perm, n), "inverse_permutation": Monomial.from_axis_permutation(inv, n)} + rng = random.Random(seed) + alive = set(cands) + for X in random_addresses(n, f, count, seed): + spec = rng.getrandbits(3) + got_X, got_ph, got_spec = execute(recs, X, f, spec) + if got_spec != spec or got_ph != 0: + return False, None, None + for c in list(alive): + if cands[c].lift(X, f) != (got_X, 0): + alive.discard(c) + if not alive: + return False, None, None + conv = sorted(alive) + return True, conv, record_counts(recs) + + +def transposition_chain(perm): + """Transpositions (i, k) whose product (applied left to right as axis swaps) is perm.""" + n = len(perm) + content = list(range(n)) # content[pos] = original axis whose bit now sits at pos + where = list(range(n)) # where[axis] = its current position + out = [] + for t in range(n): + s_axis = perm.index(t) # output position t must hold original axis s_axis + s = where[s_axis] + if s != t: + a, b = content[s], content[t] + content[s], content[t] = b, a + where[a], where[b] = t, s + out.append((s, t)) + assert all(where[i] == perm[i] for i in range(n)) + return out + + +def permutation_records(perm): + recs = [] + for i, k in transposition_chain(perm): + recs += [("XROW", i, k), ("XROW", k, i), ("XROW", i, k)] + return recs + + +def check_permutation(perm, f, count, seed): + n = len(perm) + m = Monomial.from_axis_permutation(perm, n) + recs = permutation_records(perm) + rng = random.Random(seed) + for X in random_addresses(n, f, count, seed): + spec = rng.getrandbits(3) + got_X, got_ph, got_spec = execute(recs, X, f, spec) + want_X, want_ph = m.lift(X, f) + if got_X != want_X or got_ph != want_ph or got_spec != spec: + return False, None + return True, record_counts(recs) diff --git a/research/selected-monomial-tape-lift/test_verify.py b/research/selected-monomial-tape-lift/test_verify.py new file mode 100644 index 0000000000..0d27029d55 --- /dev/null +++ b/research/selected-monomial-tape-lift/test_verify.py @@ -0,0 +1,111 @@ +#!/usr/bin/env python3 +"""Rejecting controls for the record grammar and its lift.""" +import json +import sys +import unittest +from pathlib import Path + +sys.path.insert(0, str(Path(__file__).resolve().parent)) + +import lift as L # noqa: E402 + + +def port0(): + return L.wrappers()[0][1] + + +class Controls(unittest.TestCase): + def test_grammar_realizes_every_wrapper_at_f1(self): + m = port0() + ok, info = L.check_monomial(m, 1, L.all_addresses(L.N9, 1)) + self.assertTrue(ok) + self.assertLessEqual(info["total"], 171) + + def test_unlifted_global_phase_fails_at_f2(self): + """SPECIALIZATION s3: keeping a single constant phase a instead of a*f violates the lift.""" + m = port0() + recs = m.records() + self.assertGreater(m.a, 0) + keep = [r for r in recs if r[0] != "I"] + [("I",)] * m.a + bad = [] + for X in L.random_addresses(L.N9, 2, 20, 3): + got_X, got_ph, _ = L.execute([r for r in keep if r[0] != "I"], X, 2, 0) + got_ph = (got_ph + m.a) % 4 # constant phase a, not a*f + want = m.lift(X, 2) + bad.append((got_X, got_ph) != want) + self.assertTrue(all(bad)) + + def test_dropped_row_addition_breaks_the_lift(self): + m = port0() + recs = m.records() + idx = next(i for i, r in enumerate(recs) if r[0] == "XROW") + mutated = recs[:idx] + recs[idx + 1:] + fails = 0 + for X in L.all_addresses(L.N9, 1): + got_X, got_ph, _ = L.execute(mutated, X, 1, 0) + fails += (got_X, got_ph) != m.lift(X, 1) + self.assertGreater(fails, 0) + + def test_single_column_cz_is_not_the_lift(self): + """A phase record that only reads column 0 fails at f=2 whenever a CZ or S is present.""" + m = port0() + recs = m.records() + self.assertTrue(any(r[0] in ("S", "CZ") for r in recs)) + + def execute_col0(recs, X, f): + X = list(X) + ph = 0 + for r in recs: + if r[0] == "XROW": + for j in range(f): + X[j] ^= ((X[j] >> r[2]) & 1) << r[1] + elif r[0] == "NOT": + for j in range(f): + X[j] ^= 1 << r[1] + elif r[0] == "S": + ph = (ph + ((X[0] >> r[1]) & 1)) % 4 + elif r[0] == "CZ": + ph = (ph + 2 * (((X[0] >> r[1]) & 1) & ((X[0] >> r[2]) & 1))) % 4 + else: + ph = (ph + f) % 4 + return X, ph + fails = sum(execute_col0(recs, X, 2) != tuple(m.lift(X, 2)) for X in L.random_addresses(L.N9, 2, 40, 9)) + self.assertGreater(fails, 0) + + def test_spectators_untouched(self): + m = port0() + recs = m.records() + for X in L.random_addresses(L.N9, 3, 10, 2): + _, _, spec = L.execute(recs, X, 3, 0b101) + self.assertEqual(spec, 0b101) + + def test_swap_word_with_one_swap_removed_is_rejected(self): + w = L.plan_words()[0] + ok, conv, _ = L.check_word(w["pre"], w["perm"], w["inv"], 2, 6, 1) + self.assertTrue(ok) + ok2, _, _ = L.check_word(w["pre"][1:], w["perm"], w["inv"], 2, 6, 1) + self.assertFalse(ok2) + + def test_transposition_chain_realizes_permutation(self): + import random + rng = random.Random(4) + perm = list(range(12)) + rng.shuffle(perm) + ok, info = L.check_permutation(tuple(perm), 2, 20, 3) + self.assertTrue(ok) + self.assertEqual(info["XROW"] % 3, 0) + + def test_asymmetric_Q_rejected(self): + with self.assertRaises(AssertionError): + L.Monomial(3, [1, 2, 4], 0, [2, 0, 0], [0, 0, 0], 0) + + def test_tampered_result_rejected(self): + here = Path(__file__).resolve().parent + res = json.loads((here / "RESULT.json").read_text(encoding="utf-8")) + self.assertEqual(res["status"], "PASS") + res["wrappers"]["count"] = 895 + self.assertNotEqual(res["wrappers"]["count"], 896) + + +if __name__ == "__main__": + unittest.main() diff --git a/research/selected-monomial-tape-lift/verify.py b/research/selected-monomial-tape-lift/verify.py new file mode 100644 index 0000000000..6a9fdaafa0 --- /dev/null +++ b/research/selected-monomial-tape-lift/verify.py @@ -0,0 +1,125 @@ +#!/usr/bin/env python3 +"""Record-level f-column lift of the selected caller's monomials and J routes. + +Standard library only. Exit status 0 means every check passed; a JSON summary is printed +and compared with RESULT.json (regenerate with --write-result). See README.md / PROOF.md. +""" +import json +import sys +import time +from collections import Counter +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +sys.path.insert(0, str(HERE)) + +import lift as L # noqa: E402 + +BINDINGS = { + "research/final4610-independent-admission/SPECIALIZATION.md": [ + "96+9+27+36+3 = 171", + "A row addition is precisely the selected compact-control addition with its full dirty-control restoration and repair.", + "The ideal algebraic lift holds for every positive f. Its physical tariff applies only in the selected source domain: f<=p, A=O(p), K/log p tending to infinity, and a superpolynomial record fiber. In the actual layer f<=e<=floor(b_in^epsilon) and p=6*b_in eventually.", + "It uses one fixed list of primitive **types/operations**, rather than f separately allocated tapes.", + ], + "notes/compact-control-movement.tex": [ + r"\begin{proposition}[Compact-control selected-bit addition]", + r" G=4\lceil\log_2 p\rceil+6,\quad f\le p,\quad A=O(p),", + r" O\bigl(V((f\log p)^\tau+1)\bigr)", + ], + "notes/compact-control-layout.tex": [ + "Both front fields precede all active", + "slots and the back field follows them, so the compact-control proposition", + "applies to every ordered pair of slots.", + ], + "research/kappa-function-composition/complex/prune_native.py": [ + "result = ce.diag(n, tuple(recipe['quadratic_rows']), tuple(recipe['linear_Z4']))", + "result = result.then(ce.perm(n, tuple(recipe['matrix_rows']))).then(ce.xgate(n, recipe['offset']))", + ], +} + + +def need(ok, msg): + if not ok: + raise SystemExit("FAIL: " + msg) + + +def engine_agreement(ce, m, name): + """The monomial's one-column action equals the exact Clifford engine on every basis state.""" + op = ce.diag(L.N9, m.Q, m.alpha).then(ce.perm(L.N9, m.G)).then(ce.xgate(L.N9, m.b)).then(ce.Op(L.N9, ce.identity(L.N9), [("phase", m.a)])) + for x in range(1 << L.N9): + vec, den = op.zero_state(x) + need(den == 0, f"{name}: monomial is dyadic-free") + y, ph = m.one_column(x) + want = [(1, 0), (0, 1), (-1, 0), (0, -1)][(ph + m.a) % 4] + need(vec[y] == want and all(v == (0, 0) for i, v in enumerate(vec) if i != y), f"{name}: engine agreement at x={x}") + + +def main(): + write = "--write-result" in sys.argv + t0 = time.time() + for path, needles in BINDINGS.items(): + text = (ROOT / path).read_text(encoding="utf-8") + for s in needles: + need(s in text, f"binding in {path}: {s!r}") + ce = L.load_clifford() + # 1. the 896 port wrappers of NORMALIZERS.json + W = L.wrappers() + need(len(W) == 896, "896 compiled wrappers (112 ports x 8)") + mx, tot = Counter(), Counter() + per_wrapper = {} + for i, (name, m) in enumerate(W): + if i % 112 == 0: + engine_agreement(ce, m, name) + ok, info = L.check_monomial(m, 1, L.all_addresses(L.N9, 1)) + need(ok, f"{name}: f=1 exhaustive, {info}") + need(info["total"] <= 171 and info["XROW"] <= 96, f"{name}: within the s2 grammar bound") + for f in (2, 3, 4): + ok, _ = L.check_monomial(m, f, L.random_addresses(L.N9, f, 48, 1000 * f + i)) + need(ok, f"{name}: f={f} sampled") + for k, v in info.items(): + mx[k] = max(mx[k], v) + tot[k] += v + per_wrapper[name] = info["total"] + for name, m in W[:2]: + ok, _ = L.check_monomial(m, 2, L.all_addresses(L.N9, 2)) + need(ok, f"{name}: f=2 exhaustive") + # 2. the central translation X0 (C0 and D are positive-rank children, not monomials) + (xname, x0), = L.central_elements(ce) + ok, xinfo = L.check_monomial(x0, 3, L.random_addresses(L.N9, 3, 200, 5)) + need(ok and xinfo["total"] == 1 and xinfo["NOT"] == 1, "X0 is one translation record") + # 3. the literal 145-axis J routes of the plan + words = L.plan_words() + need(len(words) == 32 + 72 + 15, "32 main, 72 helper, 15 idle targets") + route_counts, conventions, swaps = Counter(), Counter(), Counter() + central = 0 + for j, w in enumerate(words): + for key in ("pre", "post"): + ok, conv, info = L.check_word(w[key], w["perm"], w["inv"], 2, 12, 100 + j) + need(ok, f"{w['name']} {key}: literal SWAP_BITS word realizes a declared permutation") + conventions[(key, tuple(conv))] += 1 + route_counts[w["kind"]] += info["XROW"] + swaps[w["kind"]] += len(w[key]) + central += w["central_X"] + need(central == 16, "16 central X corrections (negative Q powers)") + out = {"status": "PASS", "bindings": sum(map(len, BINDINGS.values())), + "wrappers": {"count": len(W), "max_records": dict(mx), "sum_records": dict(tot), + "bound_s2": 171, "histogram_total": dict(sorted(Counter(per_wrapper.values()).items()))}, + "central": {"X0_records": xinfo, "C0_and_D": "positive-rank children (cgate, fourier), not monomials"}, + "routes": {"targets": len(words), "swap_bits_events": dict(swaps), "xrow_records": dict(route_counts), + "central_X_records": central, + "conventions": {f"{k[0]}:{'|'.join(k[1])}": v for k, v in conventions.items()}}, + "checks": {"f1_exhaustive_wrappers": 896, "f2_exhaustive_wrappers": 2, "sampled_f": [2, 3, 4], + "engine_agreement_wrappers": 8, "route_f": 2, "route_addresses": 12}} + path = HERE / "RESULT.json" + out = json.loads(json.dumps(out)) # JSON-normal form: tuples become lists, keys become strings + if write: + path.write_text(json.dumps(out, indent=1) + "\n", encoding="utf-8") + else: + need(json.loads(path.read_text(encoding="utf-8")) == out, "RESULT.json differs from the fresh computation") + print(json.dumps({**out, "seconds": round(time.time() - t0, 1)}, indent=1)) + + +if __name__ == "__main__": + main() From 377c2c7802b69e65db7a01afd5df3fb42ec3345e Mon Sep 17 00:00:00 2001 From: Matarener <52912325+Matarener@users.noreply.github.com> Date: Sat, 24 Oct 2026 21:11:30 +0300 Subject: [PATCH 2/2] Execute the body's own monomials and the provider mode words as record lists The package covered only the 896 port wrappers and the J routes and said the helper alias monomials were covered by the wrapper lists; none of the 1,072 body MONOMIAL words or the provider output_N words is a port wrapper. Each of the 283 distinct words is read off the exact engine as a monomial, certified as the same group element, and executed at f=1 (exhaustive) and f=2..4 (sampled); the largest list has 76 records. Pins the body and the provider; adds a read-off control. Co-Authored-By: Claude Opus 5.5 (1M context) --- research/selected-monomial-tape-lift/PROOF.md | 15 +++- .../selected-monomial-tape-lift/README.md | 5 ++ .../selected-monomial-tape-lift/RESULT.json | 31 ++++++++ .../selected-monomial-tape-lift/SOURCES.json | 12 +++ .../selected-monomial-tape-lift/TASK.json | 2 +- .../selected-monomial-tape-lift/VERIFY.json | 4 +- research/selected-monomial-tape-lift/lift.py | 74 +++++++++++++++++++ .../test_verify.py | 11 +++ .../selected-monomial-tape-lift/verify.py | 20 ++++- 9 files changed, 168 insertions(+), 6 deletions(-) diff --git a/research/selected-monomial-tape-lift/PROOF.md b/research/selected-monomial-tape-lift/PROOF.md index 0498baefbb..69e07e58c5 100644 --- a/research/selected-monomial-tape-lift/PROOF.md +++ b/research/selected-monomial-tape-lift/PROOF.md @@ -72,6 +72,14 @@ tariff per record is inherited from the Proposition, not re-derived here. for two wrappers, and on 48 random addresses at `f = 2, 3, 4` for every wrapper, with random spectator bits. Every wrapper is within the §2 bound; the largest list has 107 records (69 movement, 38 phase). +- The body's own monomials, which are not port wrappers: all 1,072 `MONOMIAL` operations of + `NEUTRAL-BACKWARD-v16c` (800 whole-job helper normalizers, 240 Z-map block maps, 16 paid C8 axis + routes and 16 mode aliases) and the 8 `output_N` words of the #5402 provider's mode boundaries, + which #5442's mode-output certificate binds (the 8 `input_K` words coincide with alias words). + These are 283 distinct words. Each is read off the exact engine as a monomial `(G, b, Q, alpha, a)` + on 46 basis states and certified to be the same group element (Pauli tableau and image of `|0>`); + its record list is then executed on all 512 addresses at `f = 1` and on 48 random addresses at + `f = 2, 3, 4`. The largest list has 76 records (60 movement), within the §2 bound. - The central translation `X0` is one `NOT(0)` record. `C0` (cgate on axis 0) and `D` (Fourier on axes 1..8) are positive-rank Gaussians: in the retained framework they are paid children of the recursion (`FINITE-PRECOMPILATION.md` §1, "one ordinary positive rank-r f @@ -87,6 +95,7 @@ tariff per record is inherited from the Proposition, not re-derived here. The Proposition's proof (the four-update rotation scheme with dirty compact fields, its overflow repair and the chunk-swap primitive) is not executed; the reservations of the control fields for the 145-axis layout are taken from `compact-control-layout.tex` as written. No -numerical tariff, no new κ, no change to the selected record. The 400 helper alias monomials -of #5442 are products of wrapper pairs and are covered by the wrapper lists; the forward body -is not replayed. +numerical tariff, no new κ, no change to the selected record. The body monomials, including the +400 helper alias pairs of #5442, are executed separately above (an earlier version said they +were covered by the port-wrapper lists; none of them is a port wrapper). The forward body is not +replayed. diff --git a/research/selected-monomial-tape-lift/README.md b/research/selected-monomial-tape-lift/README.md index a988c3a0c8..94e47cea44 100644 --- a/research/selected-monomial-tape-lift/README.md +++ b/research/selected-monomial-tape-lift/README.md @@ -11,6 +11,10 @@ physical half, following the written realization of `SPECIALIZATION.md` §2–§ is 171), each an `XROW` / `NOT` movement record (one compact-control selected-bit addition or translation) or a phase record (`S`, `CZ`, global `i`); the list is independent of `f` and realizes the lift `m^(tensor f)` exactly, spectators untouched; +- the body's **1,088 own monomial words** (283 distinct: 800 whole-job helper normalizers, 240 + Z-map block maps, 32 C8 routes and aliases, and the provider's 8 mode `output_N` words that + #5442's mode-output certificate binds) are fixed lists of at most 76 records each, read off + the exact engine as group elements; - the **central translation** `X0` is one record; `C0` and `D` are positive-rank children of the recursion, not adapters; - the **16,748 `SWAP_BITS` events** of the plan's 119 `J` routes (main, helper and idle @@ -32,6 +36,7 @@ layout (`compact-control-layout.tex`). [PROOF.md](PROOF.md) has the lemma and it | wrappers, engine agreement | 8 wrappers x 512 basis states against `clifford_exact` | | wrappers, `f = 2`, exhaustive | 2 wrappers x 262,144 addresses | | wrappers, `f = 2, 3, 4`, sampled | 896 x 48 addresses each | +| body and mode words | 283 distinct words (1,088 uses), engine read-off certified as group elements, `f = 1` exhaustive, `f = 2, 3, 4` sampled | | `X0` | one `NOT(0)` record, `f = 3` | | `J` routes | 119 targets x (pre, post) literal words, 145 axes, `f = 2`, 12 addresses each | | controls (`test_verify.py`) | unlifted global phase fails at `f = 2`; a dropped row addition, a removed swap, a single-column phase record and an asymmetric `Q` are rejected; spectators untouched | diff --git a/research/selected-monomial-tape-lift/RESULT.json b/research/selected-monomial-tape-lift/RESULT.json index 62d6329046..eac76e5afe 100644 --- a/research/selected-monomial-tape-lift/RESULT.json +++ b/research/selected-monomial-tape-lift/RESULT.json @@ -103,7 +103,38 @@ "post:permutation": 15 } }, + "body_words": { + "occurrences": 1088, + "distinct": 283, + "occurrences_by_first_kind": { + "block": 248, + "mode_output_N": 8, + "originalmodecanonicalC8inputalias": 32, + "whole_job": 800 + }, + "max_records": { + "XROW": 60, + "NOT": 6, + "S": 21, + "CZ": 19, + "I": 3, + "movement_records": 60, + "phase_records": 29, + "total": 76 + }, + "sum_records_over_occurrences": { + "XROW": 9575, + "NOT": 96, + "S": 16317, + "CZ": 536, + "I": 399, + "movement_records": 9671, + "phase_records": 17252, + "total": 26923 + } + }, "checks": { + "f1_exhaustive_body_words": 283, "f1_exhaustive_wrappers": 896, "f2_exhaustive_wrappers": 2, "sampled_f": [ diff --git a/research/selected-monomial-tape-lift/SOURCES.json b/research/selected-monomial-tape-lift/SOURCES.json index 45645ad3ce..fcd3bda2b3 100644 --- a/research/selected-monomial-tape-lift/SOURCES.json +++ b/research/selected-monomial-tape-lift/SOURCES.json @@ -26,6 +26,12 @@ "git_blob": "06b6a9ef24245ac7b724c53a204635415b402357", "sha256": "b963c3d2f4e1b7059aa289bb4b4ac89b688920bcf42f5b20d7698cdef0132cc6" }, + { + "path": "research/coupled-helper-neutral-completion/capsule/workspace/swarm-coupled-caller-sol-high-20261024/agents/caller/NEUTRAL-BACKWARD-v16c.json", + "usage": "input", + "git_blob": "04c6c7f36cb1b9fcf0b464bad3d3d83aaae7c864", + "sha256": "cc297ee54c2743615dfe857838d5f40424ccd33fdb08ecfafbc41b1710416d91" + }, { "path": "research/coupled-helper-neutral-completion/capsule/workspace/swarm-coupled-caller-sol-high-20261024/agents/challenge/WHOLECALLER-PLAN-v1.json", "usage": "input", @@ -38,6 +44,12 @@ "git_blob": "bca92c222c395d3d75c047fbb678f3cd0947c60f", "sha256": "ae8aad06aa5d1811d725895b3ab5a4f4daa9dcdd88294aa0d5f723e78bb1e0da" }, + { + "path": "research/coupled-helper-neutral-completion/capsule/workspace/swarm-provider-audit-sol-high-20261024/repository/research/native-rank8-helper-provider/PROVIDER.json", + "usage": "input", + "git_blob": "0afd30ed01202eb6ce62462dcf8bc9164f3b0455", + "sha256": "676de7551d3364598f4a7e29ae97cae0e4364348786bbe70435b84294ba7dd65" + }, { "path": "research/final4610-independent-admission/SPECIALIZATION.md", "usage": "input", diff --git a/research/selected-monomial-tape-lift/TASK.json b/research/selected-monomial-tape-lift/TASK.json index 4b0abe02fc..a257284c22 100644 --- a/research/selected-monomial-tape-lift/TASK.json +++ b/research/selected-monomial-tape-lift/TASK.json @@ -81,7 +81,7 @@ "budget_minutes": 240, "stop_rule": "Stop after executing all 896 wrappers (f=1 exhaustive, f=2 exhaustive on two, f=2..4 sampled), X0 and all 119 plan routes at f=2; do not simulate the Proposition's internal rotation scheme or re-derive the tariff.", "outcome": "completed", - "evidence": "PROOF.md (record lemma, uniform in f); verify.py binds SPECIALIZATION s2-s3, the Proposition and the monomial convention, executes the record lists against the lift formula and the exact Clifford engine, and freezes RESULT.json; test_verify.py has rejecting controls.", + "evidence": "PROOF.md (record lemma, uniform in f); verify.py binds SPECIALIZATION s2-s3, the Proposition and the monomial convention, executes the record lists of the 896 port wrappers, the 119 J routes and the 283 distinct body and mode words against the lift formula and the exact Clifford engine, and freezes RESULT.json; test_verify.py has rejecting controls.", "author": "Mark (Matarener)", "ai_assistance": "Prepared with substantial Claude Code (Claude) assistance.", "open_questions": [ diff --git a/research/selected-monomial-tape-lift/VERIFY.json b/research/selected-monomial-tape-lift/VERIFY.json index 2183158aaa..529b546c3e 100644 --- a/research/selected-monomial-tape-lift/VERIFY.json +++ b/research/selected-monomial-tape-lift/VERIFY.json @@ -6,8 +6,10 @@ "inputs": [ "notes/compact-control-layout.tex", "notes/compact-control-movement.tex", + "research/coupled-helper-neutral-completion/capsule/workspace/swarm-coupled-caller-sol-high-20261024/agents/caller/NEUTRAL-BACKWARD-v16c.json", "research/coupled-helper-neutral-completion/capsule/workspace/swarm-coupled-caller-sol-high-20261024/agents/challenge/WHOLECALLER-PLAN-v1.json", "research/coupled-helper-neutral-completion/capsule/workspace/swarm-provider-audit-sol-high-20261024/agents/budget/inputs/NORMALIZERS.json", + "research/coupled-helper-neutral-completion/capsule/workspace/swarm-provider-audit-sol-high-20261024/repository/research/native-rank8-helper-provider/PROVIDER.json", "research/final4610-independent-admission/SPECIALIZATION.md", "research/kappa-function-composition/complex/prune_native.py", "research/t74-native-fast/vendor/native/new/code/borrow/vendor/clifford/clifford_exact.py" @@ -20,7 +22,7 @@ "{package}/verify.py" ], "timeout_seconds": 600, - "checks": "Bind SPECIALIZATION s2-s3, the compact-control Proposition, the layout note and the monomial convention; execute the record lists of all 896 wrappers (f=1 exhaustive, f=2 exhaustive on two, f=2..4 sampled, engine agreement), X0, and the literal SWAP_BITS words of all 119 plan targets at f=2 on 145 axes; RESULT.json comparison." + "checks": "Bind SPECIALIZATION s2-s3, the compact-control Proposition, the layout note and the monomial convention; execute the record lists of all 896 wrappers (f=1 exhaustive, f=2 exhaustive on two, f=2..4 sampled, engine agreement), X0, the literal SWAP_BITS words of all 119 plan targets at f=2 on 145 axes, and the 1,088 body and mode words (283 distinct: whole-job helper normalizers, Z-map block maps, C8 routes and aliases, provider output_N) read off the engine as exact group elements and executed as record lists (f=1 exhaustive, f=2..4 sampled); RESULT.json comparison." }, { "argv": [ diff --git a/research/selected-monomial-tape-lift/lift.py b/research/selected-monomial-tape-lift/lift.py index 10950518af..167d085a91 100644 --- a/research/selected-monomial-tape-lift/lift.py +++ b/research/selected-monomial-tape-lift/lift.py @@ -35,6 +35,8 @@ NORM = CAP / "swarm-provider-audit-sol-high-20261024/agents/budget/inputs/NORMALIZERS.json" PLAN = CAP / "swarm-coupled-caller-sol-high-20261024/agents/challenge/WHOLECALLER-PLAN-v1.json" CLIFFORD = ROOT / "research/t74-native-fast/vendor/native/new/code/borrow/vendor/clifford/clifford_exact.py" +BODY = CAP / "swarm-coupled-caller-sol-high-20261024/agents/caller/NEUTRAL-BACKWARD-v16c.json" +PROVIDER = CAP / "swarm-provider-audit-sol-high-20261024/repository/research/native-rank8-helper-provider/PROVIDER.json" N9 = 9 N145 = 145 @@ -210,6 +212,78 @@ def wrappers(): return out +def literal_op(ce, word): + """Exact engine operator of a literal monomial word (primitives D, P, X, phase, applied in order).""" + op = ce.ident(N9) + for e in word: + if e[0] == "D": + op = op.then(ce.diag(N9, e[1], e[2])) + elif e[0] == "P": + op = op.then(ce.perm(N9, e[1])) + elif e[0] == "X": + op = op.then(ce.xgate(N9, e[1])) + elif e[0] == "phase": + op = op.then(ce.Op(N9, ce.identity(N9), [("phase", e[1])])) + else: + raise ValueError("unknown monomial primitive " + repr(e[0])) + return op + + +def from_engine(ce, op): + """The monomial (G, b, Q, alpha, a) of an exact engine operator, read off its action on the 46 basis states + 0, e_i, e_i + e_j, then certified as the same exact group element (Pauli tableau and image of |0>, which fixes + the absolute phase) as the engine operator of the read-off monomial. Raises if op is not that monomial.""" + units = {(1, 0): 0, (0, 1): 1, (-1, 0): 2, (0, -1): 3} + + def act(x): + vec, den = op.zero_state(x) + nz = [(y, v) for y, v in enumerate(vec) if v != (0, 0)] + if den != 0 or len(nz) != 1 or nz[0][1] not in units: + raise ValueError("not a dyadic-free monomial") + return nz[0][0], units[nz[0][1]] + b, a = act(0) + single = [act(1 << i) for i in range(N9)] + cols = [single[i][0] ^ b for i in range(N9)] + rows = [sum(((cols[i] >> r) & 1) << i for i in range(N9)) for r in range(N9)] + alpha = [(single[i][1] - a) % 4 for i in range(N9)] + Q = [0] * N9 + for i in range(N9): + Q[i] |= (alpha[i] & 1) << i + for j in range(i + 1, N9): + d = (act((1 << i) | (1 << j))[1] - single[i][1] - single[j][1] + a) % 4 + if d % 2: + raise ValueError("odd quadratic phase") + if d == 2: + Q[i] |= 1 << j + Q[j] |= 1 << i + m = Monomial(N9, rows, b, Q, alpha, a) + mine = ce.diag(N9, m.Q, m.alpha).then(ce.perm(N9, m.G)).then(ce.xgate(N9, m.b)).then(ce.Op(N9, ce.identity(N9), [("phase", m.a)])) + if mine.tab != op.tab or mine.zero_state() != op.zero_state(): + raise ValueError("read-off monomial is a different group element") + return m + + +def body_monomials(ce): + """Every literal monomial word the selected caller's body applies besides the port wrappers: the 1,072 + MONOMIAL operations of NEUTRAL-BACKWARD-v16c (800 whole-job helper normalizers, 240 Z-map block maps, + 16 paid C8 axis routes, 16 mode aliases) and the 16 mode words input_K / output_N of the #5402 provider, + which #5442's mode-output certificate binds. Returns (name, Monomial, occurrences) per distinct word.""" + body = json.loads(BODY.read_text(encoding="utf-8")) + prov = json.loads(PROVIDER.read_text(encoding="utf-8")) + words = {} + for i, o in enumerate(body["operations"]): + if o["op"] == "MONOMIAL": + kind = o.get("purpose") or ("whole_job" if "whole_job_boundary" in o else "block") + words.setdefault(json.dumps(o["word"]), [kind, 0])[1] += 1 + for m in prov["mode_boundaries"]: + for key in ("input_K", "output_N"): + words.setdefault(json.dumps(m[key]["literal_word"]), ["mode_" + key, 0])[1] += 1 + out = [] + for k, (kind, n) in words.items(): + out.append((kind, from_engine(ce, literal_op(ce, json.loads(k))), n)) + return out + + def central_elements(ce): """C0 = cgate on axis 0 and X0 = xgate on axis 0 are not monomials in prune_native's sense (cgate is a rank-one Gaussian); only X0 is a translation record. We return X0 and the diff --git a/research/selected-monomial-tape-lift/test_verify.py b/research/selected-monomial-tape-lift/test_verify.py index 0d27029d55..b50ab3ceb3 100644 --- a/research/selected-monomial-tape-lift/test_verify.py +++ b/research/selected-monomial-tape-lift/test_verify.py @@ -99,6 +99,17 @@ def test_asymmetric_Q_rejected(self): with self.assertRaises(AssertionError): L.Monomial(3, [1, 2, 4], 0, [2, 0, 0], [0, 0, 0], 0) + def test_body_word_read_off_rejects_wrong_words(self): + ce = L.load_clifford() + word = [["P", [2, 1, 4, 8, 16, 32, 64, 128, 256]], ["D", [0] * 9, [2, 0, 0, 0, 0, 0, 0, 0, 0]], ["X", 3], ["phase", 1]] + m = L.from_engine(ce, L.literal_op(ce, word)) + ok, _ = L.check_monomial(m, 2, L.random_addresses(L.N9, 2, 48, 3)) + self.assertTrue(ok) + with self.assertRaises(ValueError): # a Gaussian is not a monomial: no record list is claimed + L.from_engine(ce, ce.cgate(L.N9, 1, 1)) + with self.assertRaises(ValueError): # unknown primitive + L.literal_op(ce, [["H", 0]]) + def test_tampered_result_rejected(self): here = Path(__file__).resolve().parent res = json.loads((here / "RESULT.json").read_text(encoding="utf-8")) diff --git a/research/selected-monomial-tape-lift/verify.py b/research/selected-monomial-tape-lift/verify.py index 6a9fdaafa0..05a56bc24d 100644 --- a/research/selected-monomial-tape-lift/verify.py +++ b/research/selected-monomial-tape-lift/verify.py @@ -103,6 +103,22 @@ def main(): swaps[w["kind"]] += len(w[key]) central += w["central_X"] need(central == 16, "16 central X corrections (negative Q powers)") + # 4. the body's own monomials and the provider's mode words (not port wrappers; #5442's mode-output certificate + # binds output_N, and the body applies whole-job helper normalizers, Z-map block maps, C8 routes and aliases) + B = L.body_monomials(ce) + need(sum(n for _, _, n in B) == 1072 + 16 and len(B) == 283, "1,088 body and mode words, 283 distinct") + bmx, btot, bocc = Counter(), Counter(), Counter() + for i, (kind, m, n) in enumerate(B): + ok, info = L.check_monomial(m, 1, L.all_addresses(L.N9, 1)) + need(ok, f"body word {i} ({kind}): f=1 exhaustive, {info}") + need(info["total"] <= 171 and info["XROW"] <= 96, f"body word {i}: within the s2 grammar bound") + for f in (2, 3, 4): + ok, _ = L.check_monomial(m, f, L.random_addresses(L.N9, f, 48, 7000 + 1000 * f + i)) + need(ok, f"body word {i} ({kind}): f={f} sampled") + for k, v in info.items(): + bmx[k] = max(bmx[k], v) + btot[k] += v * n + bocc[kind] += n out = {"status": "PASS", "bindings": sum(map(len, BINDINGS.values())), "wrappers": {"count": len(W), "max_records": dict(mx), "sum_records": dict(tot), "bound_s2": 171, "histogram_total": dict(sorted(Counter(per_wrapper.values()).items()))}, @@ -110,7 +126,9 @@ def main(): "routes": {"targets": len(words), "swap_bits_events": dict(swaps), "xrow_records": dict(route_counts), "central_X_records": central, "conventions": {f"{k[0]}:{'|'.join(k[1])}": v for k, v in conventions.items()}}, - "checks": {"f1_exhaustive_wrappers": 896, "f2_exhaustive_wrappers": 2, "sampled_f": [2, 3, 4], + "body_words": {"occurrences": 1088, "distinct": len(B), "occurrences_by_first_kind": dict(sorted(bocc.items())), + "max_records": dict(bmx), "sum_records_over_occurrences": dict(btot)}, + "checks": {"f1_exhaustive_body_words": len(B), "f1_exhaustive_wrappers": 896, "f2_exhaustive_wrappers": 2, "sampled_f": [2, 3, 4], "engine_agreement_wrappers": 8, "route_f": 2, "route_addresses": 12}} path = HERE / "RESULT.json" out = json.loads(json.dumps(out)) # JSON-normal form: tuples become lists, keys become strings