From 121910f1890494d6134cd48c422facbe116db36d Mon Sep 17 00:00:00 2001 From: JoyboyBrian Date: Thu, 22 Oct 2026 13:02:11 -0700 Subject: [PATCH] Prove a resonant all-width partial target channel --- research/resonant-owner-extraction/README.md | 248 ++ .../resonant-owner-extraction/RESULT.json | 2471 +++++++++++++++++ .../resonant-owner-extraction/SOURCES.json | 30 + research/resonant-owner-extraction/TASK.json | 78 + .../resonant-owner-extraction/VERIFY.json | 32 + research/resonant-owner-extraction/verify.py | 276 ++ 6 files changed, 3135 insertions(+) create mode 100644 research/resonant-owner-extraction/README.md create mode 100644 research/resonant-owner-extraction/RESULT.json create mode 100644 research/resonant-owner-extraction/SOURCES.json create mode 100644 research/resonant-owner-extraction/TASK.json create mode 100644 research/resonant-owner-extraction/VERIFY.json create mode 100644 research/resonant-owner-extraction/verify.py diff --git a/research/resonant-owner-extraction/README.md b/research/resonant-owner-extraction/README.md new file mode 100644 index 0000000000..83d455ec60 --- /dev/null +++ b/research/resonant-owner-extraction/README.md @@ -0,0 +1,248 @@ +# A resonant original-owner partial target channel + +Changing the second paid pencil from `P+2Q` to `P+Q` in the staggered +five-call preparation produces an exact **pure partial `Kx` channel**. Its +coefficient is nonzero at every positive even tensor width and zero at every +odd width. At width two its rank is exactly one out of 64 coordinates. +All independent original inputs, including the unused fresh-owner complement, +are retained. This is a constructive partial identity, not a complete `Kx,Ky` +unit, a restoration algorithm, a paid saving, or a multiplication theorem. + +This changes the original-owner query excluded from the scope of +[PR #4751](https://github.com/CrocSwap/integer-mult-bounds/pull/4751). +That predecessor proves an obstruction with the original coefficient two, +even if the fresh-owner feed is changed arbitrarily. A resonant pencil alone +would not answer the continuation question: this package also supplies an +actual zero-`y` target identity and a nonvacuity proof for every even width. +The canonical claim is [Discussion #1166, comment 19131473](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19131473). + +## Conventions and paid preparation + +Base vectors are `e_j`, `j=j0+2j1+4j2`, with matrix words acting right to left. +Write `Xj,Zj` for the usual Pauli letters and + +``` +Cj = ((1+i) I + (1-i) Xj)/2 +S e_j = i^(j0+j1+j2) e_j +U = CNOT(0 -> 2), V = SWAP(0,1), T = SWAP(0,2), V21 = SWAP(1,2) +P = S U S, Q = S V S, Q2 = S V21 S +W = Z0 Z2, N = Z1 V, L = N T, J = N C2, K = C0 C1 C2. +``` + +For **each actual base word** `g`, put `g_f=g tensor ... tensor g`, with +`f >= 1`. A sum `sum_g q_g g_f` keeps its rational coefficients fixed across +widths; it is not the tensor power of the width-one sum. The central word +`c=iI` is retained: `c_f=i^f I`, and `(-I)_f=(-1)^f I`. + +Let `a=Y0 Z1`, `b=Y2`, with the Hermitian convention +`Pauli(x,z)=i^popcount(x&z) X^x Z^z`. Define the genuine free input projector + +``` +B_f = (I-a_f)(I-b_f)/4. +``` + +The two involutions commute, and `B_f` has rank `8^f/4` at every positive +width. Retain arbitrary original inputs `x,y` and their free copies. Execute + +``` +u = C0_f x +v = C0_f (P_f + Q_f) u +r = L_f^-1 J_f (W_f v + T_f B_f y) +t = C0_f (P_f + 2 Q_f) r +z = J_f (W_f t + Q2_f r + P_f v). +``` + +Every displayed line uses one paid `C` call. `J=N C2` applies one `C2` +call followed by the free monomial `N`; `L` is free. The changed second coefficient is one, +and the fourth coefficient remains two. This is the retained five-call +schedule of the predecessor, with that explicit change and the fresh feed. +The resonant pencil can be noninvertible. Its use here is a retained-register +linear calculation, with original `x` still present; no admission under an +invertible-pencil or full-rank prepared-unit contract is claimed. + +The output projector is the following finite free-word expression, in the +written multiplication order: + +``` +D_f = (I+c_f^2)(I+c_f X0_f)(I+Z0_f)(I+Z1_f)(I+Z2_f)/32. +``` + +The factor `I+c_f^2` makes it zero at odd widths. At even widths, the other +four Pauli constraints commute and are independent; `D_f` is a projector of +rank `8^f/16`. The checker also verifies `D^2=D` coefficientwise in the actual +word algebra. In particular this definition never silently identifies `-I` +with `I`. + +## A literal finite decoder + +The following deterministic elimination recipe, together with the explicit +monomial records in `RESULT.json`, specifies the decoder without a search or +numerical nullspace. `RESULT.json` lists its coefficients **before** the common +left factor `D`, as permutations and fourth-root phases. A matrix record acts +by `e_j -> i^phase_i[j] e_permutation[j]`; rational coefficients are literal. +Thus it is also a direct instruction list for free copies and register sums. + +Use formal rows with separate owners `x,y`. Let `H` be the group of +fourth-root monomial base matrices, and `p_h(w)` the coefficient of the +original `x` owner in the left coset `Hh`: a term `q g h x` contributes `q g`. +This notation is only used to derive the finite decoder; all its actual +monomials are independently certified to belong to the engine's free +alphabet below. + +Set `A0=L^-1 J W`, `R4=C0 P C0`, `R7=C0 Q A0 C0 P C0`. +The resonant pivot `p_R7(z)=g1+g2` has the following monomials: + +| | permutation on input columns 0,...,7 | phase exponents | +|---|---|---| +| g1 | 0 4 2 6 1 5 3 7 | 0 0 2 2 0 0 2 2 | +| g2 | 1 0 7 6 5 4 3 2 | 3 1 0 2 3 1 2 0 | + +With `R=g1^-1 g2`, the checker establishes exact order four. Consequently + +``` +E = (I-R+R^2-R^3) g1^-1 +E(g1+g2) = 0. +``` + +Start `e=E z`. For `(w,h)=(r,C2),(v,R4),(u,C0),(x,I)` in that order, the +pivot `p_h(w)` is a single nonzero term `q p`, with `p` free. Perform + +``` +e <- e - p_h(e) p^-1 w / q. +``` + +This gives fixed finite coefficients `d_w` such that `e=sum_w d_w w`. +The final output is + +``` +sum_w D_f (d_w)_f w = A_f K_f x, (1) +``` + +where `(d_w)_f` means the same wordwise evaluation, and `A` has 256 actual +free monomial terms. The coefficient of `y` is **exactly zero**. No term of +the `x` coefficient lies outside `HK`. All these statements are checked by +expanding the displayed preparation and decoder with exact Gaussian rational +base matrices, collecting equal actual words, and comparing coefficients. +The frozen receipt includes the target-coefficient SHA256, term counts and +its norm certificate; the verifier reconstructs all 256 terms. + +Why this proves (1) for every width: evaluation `[g] -> g_f` is an algebra +homomorphism, since `(gh)_f=g_f h_f`. The checker obtains zero separately for +every actual word in the `y` residual, and obtains the target coefficient +wordwise. Applying any positive-width evaluation preserves this identity. +No converse, matrix-family independence assumption, or inference from width +one or two is needed for this positive result. In particular the distinct +central words `g,-g,ig,-ig` remain distinct throughout. + +Every decoder, source-projector, output-projector and target-coefficient +monomial passes a stronger check than membership in `H`: its permutation is +`j -> Mj+s` with invertible binary `M`, and its phase has a mod-four Boolean +polynomial of degree at most two, whose quadratic coefficients are even. +These are actual free operations. Shifts and invertible XOR-linear address +maps supply the permutation; single-coordinate `S` gates supply the linear +phases. An even quadratic phase is generated by +`CZ_ij = S_i S_j S_(i xor j)^-1`, where a parity `S` is an address conjugate +of a coordinate `S`. Constant fourth-root phases and rational register sums +are also free. The receipt lists the affine columns and phase polynomial +for every emitted decoder term. This constructive claim does not rely on +allowing every fourth-root monomial for free. + +## Exact nonzero characterization + +Let `A=sum_g q_g [g]` be the target coefficient reconstructed above. Exact +Frobenius inner products give the all-width identity + +``` +||A_f||_HS^2 = sum_(g,h) q_g q_h (tr(g* h))^f + = 8^f + (-8)^f - 20 (2^f + (-2)^f) + 32 (1 + (-1)^f). +``` + +Here `g*` is conjugate transpose; every `q_g` is real rational. The checker +collects **all 256² ordered pairs** (65,536), computes their exact base traces and +verifies that the only nonzero trace powers have precisely these six +coefficients. Zero trace bases contribute zero because `f` is positive. +This is a finite certificate of a formula for every width, not a fit to +small-width values. + +For odd `f` the formula is zero, so `A_f=0`. For even `f`, it is +`2(8^f-20*2^f+32)`: at `f=2` it is 32; at every even `f>=4`, `4^f>20` +makes it strictly positive. Since `K_f` is unitary, `A_f K_f` has the same +rank and norm. Thus (1) is nonzero **exactly at positive even widths**. + +Separate exact matrix controls give ranks zero at width one and one at +width two. At width two the free coefficient has entry `(18,0)=-2`, with +zero-based indices. The general even-width rank is not determined here. +In particular, nonzero is not a full-target claim. + +## Information and cost ledger + +| Item | Established here | Still owed for a complete construction | +|---|---|---| +| Paid preparation | Exactly five displayed `C` calls | Physical preparation and recursive supplier realization | +| Independent owners | Original `x,y` remain available | Full target `Kx` and `Ky` extraction | +| Fresh-owner feed | `B y`, rank `8^f/4` | Work on the unused source sector | +| Whole complement | `(I-B)y` retained; `By+(I-B)y=y` | Charged handling/return of this complement in a full protocol | +| Retained intermediates | `u,v,r,t,z` and free decoder copies may all remain | Space, routing, terminal frame and cleanup accounting | +| Output | Pure partial `A_f K_f x`, zero `y` contamination | Missing target coordinates; exact rank for general even width | +| Budget | No additional paid call for the finite free decoder in this model | A complete per-call profile and family expansion decision | + +No dirty register is declared zero or discarded to establish (1). Keeping +`x,y` makes preservation of original information explicit; this does not +supply an in-place restoration schedule or price a physical encoding. No +recursive ceiling is evaluated because no complete supplier profile exists. +A later construction round must satisfy the family-level expansion gate. + +## Reproduction and limits + +``` +python3 scripts/research_package.py --package research/resonant-owner-extraction +``` + +The registered Python 3.12, standard-library-only commands run exact checks +normally and under `-O`. The arithmetic input is authenticated before load. +Six controls reject omitting either projector, restoring the coefficient-two +pencil with this decoder, dropping the input complement, identifying the +central minus identity with identity, and extrapolating a width-one zero. +The committed receipt is compared structurally; a direct `--write` option is +only for explicitly regenerating it after a justified implementation change. + +Local exact replay is not hosted CI or proof-kernel acceptance. No hook-rank +census, FFT replay, Lean, Docker, selected-frontier update, or full integer +multiplication theorem is claimed. + +## Provenance and overlap + +Canonical base is `624de9dc66858af0945e5f8a0942488d62280d43`, priority revision +7. `SOURCES.json` binds the task card, selected-record provenance, predecessor +proof and live arithmetic. The changed premise and stopped exploration are +recorded in `TASK.json`. + +Credit Yiyang (@Lyy-iiis) for the phase-aligned two-image repair, +[PR #4710](https://github.com/CrocSwap/integer-mult-bounds/pull/4710), exact +head `b0d5192390af493d626054b060921895df3c94d2`, and the staggered continuation; +lee-phys for the original two-image prefix, +[PR #4688](https://github.com/CrocSwap/integer-mult-bounds/pull/4688), exact +head `264c4b3cb13c82d171de352ecf60486dfb8d2bd4`; and Jacob Sussman for the +small-unit model and free alphabet in +[PR #4628](https://github.com/CrocSwap/integer-mult-bounds/pull/4628), exact +head `ee4fd87f064017c23e5a86fc1dcfe0a5237caed3`. The fixed-original-owner +obstruction and retained arithmetic in +[PR #4751](https://github.com/CrocSwap/integer-mult-bounds/pull/4751), exact +head `2b7b84971377e389bb60bc99973e023084225dc9`, remain unchanged. +Prepared by JoyboyBrian with substantial OpenAI Codex assistance. Apache-2.0. + +The initial fresh overlap checkpoint covered 299 open PRs, 3695 Discussion +records and 6319 local notes. Relevant predecessor heads were read live. +No matching resonant pure-target channel appeared; those checks are not a +novelty certificate. The predecessor's universal fresh-feed obstruction is +preserved because this construction changes its original-owner premise. + +## Open next questions + +1. Can a complete target and charged return use this channel? First write the + independent-target/complement ledger and price every additional call. + The remaining physical preparation, storage/routing, missing target, + restoration and supplier obligations prevent any saving claim now. +2. What is `rank(A_f)` for general even `f`? Seek an analytic factorization of + the frozen target coefficient. The exact nonzero norm alone cannot answer + rank or the complete construction budget. diff --git a/research/resonant-owner-extraction/RESULT.json b/research/resonant-owner-extraction/RESULT.json new file mode 100644 index 0000000000..6447797b3d --- /dev/null +++ b/research/resonant-owner-extraction/RESULT.json @@ -0,0 +1,2471 @@ +{ + "annihilator": [ + { + "affine_columns": [ + 4, + 2, + 1 + ], + "affine_shift": 0, + "coefficient": "1", + "permutation": [ + 0, + 4, + 2, + 6, + 1, + 5, + 3, + 7 + ], + "phase_i": [ + 0, + 0, + 2, + 2, + 0, + 0, + 2, + 2 + ], + "phase_polynomial_mod4": [ + 0, + 0, + 2, + 0, + 0, + 0, + 0, + 0 + ] + }, + { + "affine_columns": [ + 1, + 6, + 4 + ], + "affine_shift": 1, + "coefficient": "-1", + "permutation": [ + 1, + 0, + 7, + 6, + 5, + 4, + 3, + 2 + ], + "phase_i": [ + 3, + 1, + 0, + 2, + 3, + 1, + 2, + 0 + ], + "phase_polynomial_mod4": [ + 3, + 2, + 1, + 0, + 0, + 0, + 2, + 0 + ] + }, + { + "affine_columns": [ + 1, + 3, + 4 + ], + "affine_shift": 4, + "coefficient": "-1", + "permutation": [ + 4, + 5, + 7, + 6, + 0, + 1, + 3, + 2 + ], + "phase_i": [ + 3, + 3, + 0, + 2, + 1, + 1, + 2, + 0 + ], + "phase_polynomial_mod4": [ + 3, + 0, + 1, + 2, + 2, + 0, + 0, + 0 + ] + }, + { + "affine_columns": [ + 4, + 7, + 1 + ], + "affine_shift": 5, + "coefficient": "1", + "permutation": [ + 5, + 1, + 2, + 6, + 4, + 0, + 3, + 7 + ], + "phase_i": [ + 2, + 0, + 2, + 2, + 0, + 2, + 2, + 2 + ], + "phase_polynomial_mod4": [ + 2, + 2, + 0, + 2, + 2, + 0, + 2, + 0 + ] + } + ], + "decoder_before_output_projector": { + "r": [ + { + "affine_columns": [ + 1, + 4, + 2 + ], + "affine_shift": 0, + "coefficient": "-1", + "permutation": [ + 0, + 1, + 4, + 5, + 2, + 3, + 6, + 7 + ], + "phase_i": [ + 0, + 0, + 2, + 2, + 0, + 2, + 2, + 0 + ], + "phase_polynomial_mod4": [ + 0, + 0, + 2, + 0, + 0, + 2, + 0, + 0 + ] + }, + { + "affine_columns": [ + 6, + 1, + 2 + ], + "affine_shift": 0, + "coefficient": "-2", + "permutation": [ + 0, + 6, + 1, + 7, + 2, + 4, + 3, + 5 + ], + "phase_i": [ + 1, + 0, + 3, + 2, + 1, + 2, + 3, + 0 + ], + "phase_polynomial_mod4": [ + 1, + 3, + 2, + 0, + 0, + 2, + 0, + 0 + ] + }, + { + "affine_columns": [ + 4, + 1, + 6 + ], + "affine_shift": 1, + "coefficient": "1", + "permutation": [ + 1, + 5, + 0, + 4, + 7, + 3, + 6, + 2 + ], + "phase_i": [ + 3, + 3, + 3, + 3, + 2, + 2, + 2, + 2 + ], + "phase_polynomial_mod4": [ + 3, + 0, + 0, + 0, + 3, + 0, + 0, + 0 + ] + }, + { + "affine_columns": [ + 7, + 4, + 6 + ], + "affine_shift": 1, + "coefficient": "2", + "permutation": [ + 1, + 6, + 5, + 2, + 7, + 0, + 3, + 4 + ], + "phase_i": [ + 0, + 0, + 2, + 0, + 3, + 3, + 3, + 1 + ], + "phase_polynomial_mod4": [ + 0, + 0, + 2, + 2, + 3, + 0, + 2, + 0 + ] + }, + { + "affine_columns": [ + 4, + 1, + 3 + ], + "affine_shift": 4, + "coefficient": "1", + "permutation": [ + 4, + 0, + 5, + 1, + 7, + 3, + 6, + 2 + ], + "phase_i": [ + 3, + 1, + 1, + 3, + 2, + 2, + 2, + 2 + ], + "phase_polynomial_mod4": [ + 3, + 2, + 2, + 0, + 3, + 2, + 2, + 0 + ] + }, + { + "affine_columns": [ + 2, + 4, + 3 + ], + "affine_shift": 4, + "coefficient": "2", + "permutation": [ + 4, + 6, + 0, + 2, + 7, + 5, + 3, + 1 + ], + "phase_i": [ + 0, + 0, + 0, + 0, + 3, + 1, + 3, + 1 + ], + "phase_polynomial_mod4": [ + 0, + 0, + 0, + 0, + 3, + 2, + 0, + 0 + ] + }, + { + "affine_columns": [ + 1, + 4, + 7 + ], + "affine_shift": 5, + "coefficient": "-1", + "permutation": [ + 5, + 4, + 1, + 0, + 2, + 3, + 6, + 7 + ], + "phase_i": [ + 2, + 0, + 2, + 0, + 0, + 2, + 2, + 0 + ], + "phase_polynomial_mod4": [ + 2, + 2, + 0, + 0, + 2, + 0, + 2, + 0 + ] + }, + { + "affine_columns": [ + 3, + 1, + 7 + ], + "affine_shift": 5, + "coefficient": "-2", + "permutation": [ + 5, + 6, + 4, + 7, + 2, + 1, + 3, + 0 + ], + "phase_i": [ + 3, + 0, + 3, + 2, + 1, + 2, + 3, + 2 + ], + "phase_polynomial_mod4": [ + 3, + 1, + 0, + 2, + 2, + 0, + 2, + 0 + ] + } + ], + "t": [], + "u": [ + { + "affine_columns": [ + 1, + 4, + 2 + ], + "affine_shift": 2, + "coefficient": "-1", + "permutation": [ + 2, + 3, + 6, + 7, + 0, + 1, + 4, + 5 + ], + "phase_i": [ + 3, + 1, + 3, + 1, + 1, + 3, + 1, + 3 + ], + "phase_polynomial_mod4": [ + 3, + 2, + 0, + 0, + 2, + 0, + 0, + 0 + ] + }, + { + "affine_columns": [ + 1, + 4, + 7 + ], + "affine_shift": 2, + "coefficient": "-1", + "permutation": [ + 2, + 3, + 6, + 7, + 5, + 4, + 1, + 0 + ], + "phase_i": [ + 3, + 1, + 3, + 1, + 3, + 3, + 1, + 1 + ], + "phase_polynomial_mod4": [ + 3, + 2, + 0, + 0, + 0, + 2, + 2, + 0 + ] + }, + { + "affine_columns": [ + 4, + 3, + 2 + ], + "affine_shift": 2, + "coefficient": "-1", + "permutation": [ + 2, + 6, + 1, + 5, + 0, + 4, + 3, + 7 + ], + "phase_i": [ + 3, + 3, + 2, + 2, + 1, + 1, + 2, + 2 + ], + "phase_polynomial_mod4": [ + 3, + 0, + 3, + 0, + 2, + 0, + 2, + 0 + ] + }, + { + "affine_columns": [ + 4, + 6, + 7 + ], + "affine_shift": 2, + "coefficient": "-1", + "permutation": [ + 2, + 6, + 4, + 0, + 5, + 1, + 3, + 7 + ], + "phase_i": [ + 3, + 3, + 2, + 0, + 3, + 1, + 2, + 2 + ], + "phase_polynomial_mod4": [ + 3, + 0, + 3, + 2, + 0, + 2, + 0, + 0 + ] + }, + { + "affine_columns": [ + 4, + 1, + 6 + ], + "affine_shift": 7, + "coefficient": "1", + "permutation": [ + 7, + 3, + 6, + 2, + 1, + 5, + 0, + 4 + ], + "phase_i": [ + 1, + 1, + 3, + 3, + 0, + 2, + 2, + 0 + ], + "phase_polynomial_mod4": [ + 1, + 0, + 2, + 0, + 3, + 2, + 0, + 0 + ] + }, + { + "affine_columns": [ + 4, + 1, + 3 + ], + "affine_shift": 7, + "coefficient": "1", + "permutation": [ + 7, + 3, + 6, + 2, + 4, + 0, + 5, + 1 + ], + "phase_i": [ + 1, + 1, + 3, + 3, + 0, + 0, + 0, + 0 + ], + "phase_polynomial_mod4": [ + 1, + 0, + 2, + 0, + 3, + 0, + 2, + 0 + ] + }, + { + "affine_columns": [ + 1, + 7, + 3 + ], + "affine_shift": 7, + "coefficient": "1", + "permutation": [ + 7, + 6, + 0, + 1, + 4, + 5, + 3, + 2 + ], + "phase_i": [ + 1, + 3, + 3, + 3, + 0, + 0, + 2, + 0 + ], + "phase_polynomial_mod4": [ + 1, + 2, + 2, + 2, + 3, + 2, + 0, + 0 + ] + }, + { + "affine_columns": [ + 1, + 2, + 6 + ], + "affine_shift": 7, + "coefficient": "1", + "permutation": [ + 7, + 6, + 5, + 4, + 1, + 0, + 3, + 2 + ], + "phase_i": [ + 1, + 3, + 1, + 3, + 0, + 2, + 2, + 0 + ], + "phase_polynomial_mod4": [ + 1, + 2, + 0, + 0, + 3, + 0, + 2, + 0 + ] + } + ], + "v": [], + "x": [], + "y": [], + "z": [ + { + "affine_columns": [ + 4, + 2, + 1 + ], + "affine_shift": 0, + "coefficient": "1", + "permutation": [ + 0, + 4, + 2, + 6, + 1, + 5, + 3, + 7 + ], + "phase_i": [ + 0, + 0, + 2, + 2, + 0, + 0, + 2, + 2 + ], + "phase_polynomial_mod4": [ + 0, + 0, + 2, + 0, + 0, + 0, + 0, + 0 + ] + }, + { + "affine_columns": [ + 1, + 6, + 4 + ], + "affine_shift": 1, + "coefficient": "-1", + "permutation": [ + 1, + 0, + 7, + 6, + 5, + 4, + 3, + 2 + ], + "phase_i": [ + 3, + 1, + 0, + 2, + 3, + 1, + 2, + 0 + ], + "phase_polynomial_mod4": [ + 3, + 2, + 1, + 0, + 0, + 0, + 2, + 0 + ] + }, + { + "affine_columns": [ + 1, + 3, + 4 + ], + "affine_shift": 4, + "coefficient": "-1", + "permutation": [ + 4, + 5, + 7, + 6, + 0, + 1, + 3, + 2 + ], + "phase_i": [ + 3, + 3, + 0, + 2, + 1, + 1, + 2, + 0 + ], + "phase_polynomial_mod4": [ + 3, + 0, + 1, + 2, + 2, + 0, + 0, + 0 + ] + }, + { + "affine_columns": [ + 4, + 7, + 1 + ], + "affine_shift": 5, + "coefficient": "1", + "permutation": [ + 5, + 1, + 2, + 6, + 4, + 0, + 3, + 7 + ], + "phase_i": [ + 2, + 0, + 2, + 2, + 0, + 2, + 2, + 2 + ], + "phase_polynomial_mod4": [ + 2, + 2, + 0, + 2, + 2, + 0, + 2, + 0 + ] + } + ] + }, + "eliminations": [ + { + "register": "r", + "terms": 8 + }, + { + "register": "v", + "terms": 0 + }, + { + "register": "u", + "terms": 8 + }, + { + "register": "x", + "terms": 0 + } + ], + "final_decoder_term_counts": { + "r": 256, + "t": 0, + "u": 256, + "v": 0, + "x": 0, + "y": 0, + "z": 128 + }, + "formal_target_terms": 256, + "formal_y_terms": 0, + "hilbert_schmidt_trace_powers": [ + { + "base": [ + -8, + 0 + ], + "coefficient": "1" + }, + { + "base": [ + -2, + 0 + ], + "coefficient": "-20" + }, + { + "base": [ + -1, + 0 + ], + "coefficient": "32" + }, + { + "base": [ + 1, + 0 + ], + "coefficient": "32" + }, + { + "base": [ + 2, + 0 + ], + "coefficient": "-20" + }, + { + "base": [ + 8, + 0 + ], + "coefficient": "1" + } + ], + "negative_controls": [ + "omit_output_projector", + "restore_original_coefficient_two", + "omit_source_projector", + "discard_source_complement", + "identify_central_minus_I_with_I", + "infer_width_one_identity_at_width_two" + ], + "output_projector": [ + { + "affine_columns": [ + 1, + 2, + 4 + ], + "affine_shift": 0, + "coefficient": "1/32", + "permutation": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7 + ], + "phase_i": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "phase_polynomial_mod4": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ] + }, + { + "affine_columns": [ + 1, + 2, + 4 + ], + "affine_shift": 0, + "coefficient": "1/32", + "permutation": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7 + ], + "phase_i": [ + 0, + 0, + 0, + 0, + 2, + 2, + 2, + 2 + ], + "phase_polynomial_mod4": [ + 0, + 0, + 0, + 0, + 2, + 0, + 0, + 0 + ] + }, + { + "affine_columns": [ + 1, + 2, + 4 + ], + "affine_shift": 0, + "coefficient": "1/32", + "permutation": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7 + ], + "phase_i": [ + 0, + 0, + 2, + 2, + 0, + 0, + 2, + 2 + ], + "phase_polynomial_mod4": [ + 0, + 0, + 2, + 0, + 0, + 0, + 0, + 0 + ] + }, + { + "affine_columns": [ + 1, + 2, + 4 + ], + "affine_shift": 0, + "coefficient": "1/32", + "permutation": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7 + ], + "phase_i": [ + 0, + 0, + 2, + 2, + 2, + 2, + 0, + 0 + ], + "phase_polynomial_mod4": [ + 0, + 0, + 2, + 0, + 2, + 0, + 0, + 0 + ] + }, + { + "affine_columns": [ + 1, + 2, + 4 + ], + "affine_shift": 0, + "coefficient": "1/32", + "permutation": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7 + ], + "phase_i": [ + 0, + 2, + 0, + 2, + 0, + 2, + 0, + 2 + ], + "phase_polynomial_mod4": [ + 0, + 2, + 0, + 0, + 0, + 0, + 0, + 0 + ] + }, + { + "affine_columns": [ + 1, + 2, + 4 + ], + "affine_shift": 0, + "coefficient": "1/32", + "permutation": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7 + ], + "phase_i": [ + 0, + 2, + 0, + 2, + 2, + 0, + 2, + 0 + ], + "phase_polynomial_mod4": [ + 0, + 2, + 0, + 0, + 2, + 0, + 0, + 0 + ] + }, + { + "affine_columns": [ + 1, + 2, + 4 + ], + "affine_shift": 0, + "coefficient": "1/32", + "permutation": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7 + ], + "phase_i": [ + 0, + 2, + 2, + 0, + 0, + 2, + 2, + 0 + ], + "phase_polynomial_mod4": [ + 0, + 2, + 2, + 0, + 0, + 0, + 0, + 0 + ] + }, + { + "affine_columns": [ + 1, + 2, + 4 + ], + "affine_shift": 0, + "coefficient": "1/32", + "permutation": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7 + ], + "phase_i": [ + 0, + 2, + 2, + 0, + 2, + 0, + 0, + 2 + ], + "phase_polynomial_mod4": [ + 0, + 2, + 2, + 0, + 2, + 0, + 0, + 0 + ] + }, + { + "affine_columns": [ + 1, + 2, + 4 + ], + "affine_shift": 0, + "coefficient": "1/32", + "permutation": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7 + ], + "phase_i": [ + 2, + 0, + 0, + 2, + 0, + 2, + 2, + 0 + ], + "phase_polynomial_mod4": [ + 2, + 2, + 2, + 0, + 2, + 0, + 0, + 0 + ] + }, + { + "affine_columns": [ + 1, + 2, + 4 + ], + "affine_shift": 0, + "coefficient": "1/32", + "permutation": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7 + ], + "phase_i": [ + 2, + 0, + 0, + 2, + 2, + 0, + 0, + 2 + ], + "phase_polynomial_mod4": [ + 2, + 2, + 2, + 0, + 0, + 0, + 0, + 0 + ] + }, + { + "affine_columns": [ + 1, + 2, + 4 + ], + "affine_shift": 0, + "coefficient": "1/32", + "permutation": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7 + ], + "phase_i": [ + 2, + 0, + 2, + 0, + 0, + 2, + 0, + 2 + ], + "phase_polynomial_mod4": [ + 2, + 2, + 0, + 0, + 2, + 0, + 0, + 0 + ] + }, + { + "affine_columns": [ + 1, + 2, + 4 + ], + "affine_shift": 0, + "coefficient": "1/32", + "permutation": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7 + ], + "phase_i": [ + 2, + 0, + 2, + 0, + 2, + 0, + 2, + 0 + ], + "phase_polynomial_mod4": [ + 2, + 2, + 0, + 0, + 0, + 0, + 0, + 0 + ] + }, + { + "affine_columns": [ + 1, + 2, + 4 + ], + "affine_shift": 0, + "coefficient": "1/32", + "permutation": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7 + ], + "phase_i": [ + 2, + 2, + 0, + 0, + 0, + 0, + 2, + 2 + ], + "phase_polynomial_mod4": [ + 2, + 0, + 2, + 0, + 2, + 0, + 0, + 0 + ] + }, + { + "affine_columns": [ + 1, + 2, + 4 + ], + "affine_shift": 0, + "coefficient": "1/32", + "permutation": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7 + ], + "phase_i": [ + 2, + 2, + 0, + 0, + 2, + 2, + 0, + 0 + ], + "phase_polynomial_mod4": [ + 2, + 0, + 2, + 0, + 0, + 0, + 0, + 0 + ] + }, + { + "affine_columns": [ + 1, + 2, + 4 + ], + "affine_shift": 0, + "coefficient": "1/32", + "permutation": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7 + ], + "phase_i": [ + 2, + 2, + 2, + 2, + 0, + 0, + 0, + 0 + ], + "phase_polynomial_mod4": [ + 2, + 0, + 0, + 0, + 2, + 0, + 0, + 0 + ] + }, + { + "affine_columns": [ + 1, + 2, + 4 + ], + "affine_shift": 0, + "coefficient": "1/32", + "permutation": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7 + ], + "phase_i": [ + 2, + 2, + 2, + 2, + 2, + 2, + 2, + 2 + ], + "phase_polynomial_mod4": [ + 2, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ] + }, + { + "affine_columns": [ + 1, + 2, + 4 + ], + "affine_shift": 1, + "coefficient": "1/32", + "permutation": [ + 1, + 0, + 3, + 2, + 5, + 4, + 7, + 6 + ], + "phase_i": [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ], + "phase_polynomial_mod4": [ + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ] + }, + { + "affine_columns": [ + 1, + 2, + 4 + ], + "affine_shift": 1, + "coefficient": "1/32", + "permutation": [ + 1, + 0, + 3, + 2, + 5, + 4, + 7, + 6 + ], + "phase_i": [ + 1, + 1, + 1, + 1, + 3, + 3, + 3, + 3 + ], + "phase_polynomial_mod4": [ + 1, + 0, + 0, + 0, + 2, + 0, + 0, + 0 + ] + }, + { + "affine_columns": [ + 1, + 2, + 4 + ], + "affine_shift": 1, + "coefficient": "1/32", + "permutation": [ + 1, + 0, + 3, + 2, + 5, + 4, + 7, + 6 + ], + "phase_i": [ + 1, + 1, + 3, + 3, + 1, + 1, + 3, + 3 + ], + "phase_polynomial_mod4": [ + 1, + 0, + 2, + 0, + 0, + 0, + 0, + 0 + ] + }, + { + "affine_columns": [ + 1, + 2, + 4 + ], + "affine_shift": 1, + "coefficient": "1/32", + "permutation": [ + 1, + 0, + 3, + 2, + 5, + 4, + 7, + 6 + ], + "phase_i": [ + 1, + 1, + 3, + 3, + 3, + 3, + 1, + 1 + ], + "phase_polynomial_mod4": [ + 1, + 0, + 2, + 0, + 2, + 0, + 0, + 0 + ] + }, + { + "affine_columns": [ + 1, + 2, + 4 + ], + "affine_shift": 1, + "coefficient": "1/32", + "permutation": [ + 1, + 0, + 3, + 2, + 5, + 4, + 7, + 6 + ], + "phase_i": [ + 1, + 3, + 1, + 3, + 1, + 3, + 1, + 3 + ], + "phase_polynomial_mod4": [ + 1, + 2, + 0, + 0, + 0, + 0, + 0, + 0 + ] + }, + { + "affine_columns": [ + 1, + 2, + 4 + ], + "affine_shift": 1, + "coefficient": "1/32", + "permutation": [ + 1, + 0, + 3, + 2, + 5, + 4, + 7, + 6 + ], + "phase_i": [ + 1, + 3, + 1, + 3, + 3, + 1, + 3, + 1 + ], + "phase_polynomial_mod4": [ + 1, + 2, + 0, + 0, + 2, + 0, + 0, + 0 + ] + }, + { + "affine_columns": [ + 1, + 2, + 4 + ], + "affine_shift": 1, + "coefficient": "1/32", + "permutation": [ + 1, + 0, + 3, + 2, + 5, + 4, + 7, + 6 + ], + "phase_i": [ + 1, + 3, + 3, + 1, + 1, + 3, + 3, + 1 + ], + "phase_polynomial_mod4": [ + 1, + 2, + 2, + 0, + 0, + 0, + 0, + 0 + ] + }, + { + "affine_columns": [ + 1, + 2, + 4 + ], + "affine_shift": 1, + "coefficient": "1/32", + "permutation": [ + 1, + 0, + 3, + 2, + 5, + 4, + 7, + 6 + ], + "phase_i": [ + 1, + 3, + 3, + 1, + 3, + 1, + 1, + 3 + ], + "phase_polynomial_mod4": [ + 1, + 2, + 2, + 0, + 2, + 0, + 0, + 0 + ] + }, + { + "affine_columns": [ + 1, + 2, + 4 + ], + "affine_shift": 1, + "coefficient": "1/32", + "permutation": [ + 1, + 0, + 3, + 2, + 5, + 4, + 7, + 6 + ], + "phase_i": [ + 3, + 1, + 1, + 3, + 1, + 3, + 3, + 1 + ], + "phase_polynomial_mod4": [ + 3, + 2, + 2, + 0, + 2, + 0, + 0, + 0 + ] + }, + { + "affine_columns": [ + 1, + 2, + 4 + ], + "affine_shift": 1, + "coefficient": "1/32", + "permutation": [ + 1, + 0, + 3, + 2, + 5, + 4, + 7, + 6 + ], + "phase_i": [ + 3, + 1, + 1, + 3, + 3, + 1, + 1, + 3 + ], + "phase_polynomial_mod4": [ + 3, + 2, + 2, + 0, + 0, + 0, + 0, + 0 + ] + }, + { + "affine_columns": [ + 1, + 2, + 4 + ], + "affine_shift": 1, + "coefficient": "1/32", + "permutation": [ + 1, + 0, + 3, + 2, + 5, + 4, + 7, + 6 + ], + "phase_i": [ + 3, + 1, + 3, + 1, + 1, + 3, + 1, + 3 + ], + "phase_polynomial_mod4": [ + 3, + 2, + 0, + 0, + 2, + 0, + 0, + 0 + ] + }, + { + "affine_columns": [ + 1, + 2, + 4 + ], + "affine_shift": 1, + "coefficient": "1/32", + "permutation": [ + 1, + 0, + 3, + 2, + 5, + 4, + 7, + 6 + ], + "phase_i": [ + 3, + 1, + 3, + 1, + 3, + 1, + 3, + 1 + ], + "phase_polynomial_mod4": [ + 3, + 2, + 0, + 0, + 0, + 0, + 0, + 0 + ] + }, + { + "affine_columns": [ + 1, + 2, + 4 + ], + "affine_shift": 1, + "coefficient": "1/32", + "permutation": [ + 1, + 0, + 3, + 2, + 5, + 4, + 7, + 6 + ], + "phase_i": [ + 3, + 3, + 1, + 1, + 1, + 1, + 3, + 3 + ], + "phase_polynomial_mod4": [ + 3, + 0, + 2, + 0, + 2, + 0, + 0, + 0 + ] + }, + { + "affine_columns": [ + 1, + 2, + 4 + ], + "affine_shift": 1, + "coefficient": "1/32", + "permutation": [ + 1, + 0, + 3, + 2, + 5, + 4, + 7, + 6 + ], + "phase_i": [ + 3, + 3, + 1, + 1, + 3, + 3, + 1, + 1 + ], + "phase_polynomial_mod4": [ + 3, + 0, + 2, + 0, + 0, + 0, + 0, + 0 + ] + }, + { + "affine_columns": [ + 1, + 2, + 4 + ], + "affine_shift": 1, + "coefficient": "1/32", + "permutation": [ + 1, + 0, + 3, + 2, + 5, + 4, + 7, + 6 + ], + "phase_i": [ + 3, + 3, + 3, + 3, + 1, + 1, + 1, + 1 + ], + "phase_polynomial_mod4": [ + 3, + 0, + 0, + 0, + 2, + 0, + 0, + 0 + ] + }, + { + "affine_columns": [ + 1, + 2, + 4 + ], + "affine_shift": 1, + "coefficient": "1/32", + "permutation": [ + 1, + 0, + 3, + 2, + 5, + 4, + 7, + 6 + ], + "phase_i": [ + 3, + 3, + 3, + 3, + 3, + 3, + 3, + 3 + ], + "phase_polynomial_mod4": [ + 3, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ] + } + ], + "relative_order": 4, + "scope": "Exact all-positive-width pure partial Kx channel; nonzero at every even width, rank one at width two, and zero at odd widths. No full Kx, Ky, restoration budget, recursive saving or multiplication theorem.", + "source_arithmetic_sha256": "0d277854396e4ceda1e0f26916bd576b6decb474c0692b6671ebf2595283ddb9", + "source_projector": [ + { + "affine_columns": [ + 1, + 2, + 4 + ], + "affine_shift": 0, + "coefficient": "1/4", + "permutation": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7 + ], + "phase_i": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "phase_polynomial_mod4": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ] + }, + { + "affine_columns": [ + 1, + 2, + 4 + ], + "affine_shift": 1, + "coefficient": "-1/4", + "permutation": [ + 1, + 0, + 3, + 2, + 5, + 4, + 7, + 6 + ], + "phase_i": [ + 1, + 3, + 3, + 1, + 1, + 3, + 3, + 1 + ], + "phase_polynomial_mod4": [ + 1, + 2, + 2, + 0, + 0, + 0, + 0, + 0 + ] + }, + { + "affine_columns": [ + 1, + 2, + 4 + ], + "affine_shift": 4, + "coefficient": "-1/4", + "permutation": [ + 4, + 5, + 6, + 7, + 0, + 1, + 2, + 3 + ], + "phase_i": [ + 1, + 1, + 1, + 1, + 3, + 3, + 3, + 3 + ], + "phase_polynomial_mod4": [ + 1, + 0, + 0, + 0, + 2, + 0, + 0, + 0 + ] + }, + { + "affine_columns": [ + 1, + 2, + 4 + ], + "affine_shift": 5, + "coefficient": "1/4", + "permutation": [ + 5, + 4, + 7, + 6, + 1, + 0, + 3, + 2 + ], + "phase_i": [ + 2, + 0, + 0, + 2, + 0, + 2, + 2, + 0 + ], + "phase_polynomial_mod4": [ + 2, + 2, + 2, + 0, + 2, + 0, + 0, + 0 + ] + } + ], + "status": "PASS_RESONANT_OWNER_EXTRACTION", + "target_coefficient_sha256": "445b3e5f8edb6f345981c02c1feb91f2ce473763be74ca7d949421e1ca64d03d", + "width_checks": [ + { + "first_nonzero": null, + "nonzero_entries": 0, + "output_projector_rank": 0, + "source_projector_rank": 2, + "target_coefficient_rank": 0, + "width": 1 + }, + { + "first_nonzero": [ + 18, + 0, + [ + "-2", + "0" + ] + ], + "nonzero_entries": 8, + "output_projector_rank": 4, + "source_projector_rank": 16, + "target_coefficient_rank": 1, + "width": 2 + } + ] +} diff --git a/research/resonant-owner-extraction/SOURCES.json b/research/resonant-owner-extraction/SOURCES.json new file mode 100644 index 0000000000..2692ac0f72 --- /dev/null +++ b/research/resonant-owner-extraction/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/staggered-single-owner-obstruction/retained/arithmetic.py", + "usage": "input", + "git_blob": "9130ce2171e4af01338be27e7ffbf1feaf88da9e", + "sha256": "0d277854396e4ceda1e0f26916bd576b6decb474c0692b6671ebf2595283ddb9" + }, + { + "path": "research/staggered-single-owner-obstruction/README.md", + "usage": "provenance", + "git_blob": "42cf519d1737dbabc31d0c0f9c77dedda5f9e6f0", + "sha256": "ff1acb5907e2f5fb1ca41bacbe331384dd6e5b9cfec821cd4d7209b8dddb1030" + } + ] +} diff --git a/research/resonant-owner-extraction/TASK.json b/research/resonant-owner-extraction/TASK.json new file mode 100644 index 0000000000..7aedec6743 --- /dev/null +++ b/research/resonant-owner-extraction/TASK.json @@ -0,0 +1,78 @@ +{ + "schema_version": 1, + "task_id": "complex-rank-shape-decoder", + "priority_revision": 7, + "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "original_card": { + "id": "complex-rank-shape-decoder", + "question": "Can a decoder deliver the local paid mass in fewer, larger-rank children (block frame climbs instead of rank-1 to rank-3 steps)?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/complex-local-word-ceiling/README.md", + "research/complex-decoder-field-extension-seed44/README.md", + "research/complex-frame-pair-decoders/README.md", + "research/selected-k8-unrestricted-ends/README.md", + "research/eisenstein-reduction-copy-floor/README.md" + ], + "methods": [ + "Find one exact small decoding identity whose frame path climbs in blocks, and price its complete per-call profile.", + "Bound the best effective child rank achievable for one fixed support alphabet, including copies, frames and restoration." + ], + "acceptance_gate": "A per-call local profile, with all copied information, frames and restoration counted, whose ceiling exceeds the selected word's by at least 5%; masked or overcomplete supports must change an assumption of the eight-term all-pairs bound. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "research/complex-local-word-ceiling/verify.py" + ], + "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING", + "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.", + "scope": "Positive control and planning budget only; this is not a new construction or full cold replay." + }, + "first_experiment": "Before any synthesis, write the candidate per-call local profile (and centre charge / unpaid coordinates if changed) and screen it with ceiling.ceiling(); reject it if even the ideal ceiling does not beat the selected word's by your stated margin. Ideal budget: rank-16 delivery is 2.31x (levers.py).", + "bottleneck_link": "Rank-1 children are about half of recursive cost; the selected word's effective child rank is about 3.9. Larger-rank delivery lowers recursive cost per unit of paid mass.", + "allowed_variations": [ + "One masked, overcomplete or block decoder family with exact labels and supports.", + "A scoped lower bound on effective rank for one alphabet.", + "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope." + ], + "scope_change_triggers": [ + "Repacking idle remainders of an unchanged word (covered by the packing ceiling).", + "Repeating the eight-term all-pairs search inside its proved scope.", + "Only changing helper terminal subspaces and monotone frames within the fixed scalar word, entrances and cleanup contract already covered by #1995/#2013.", + "Searching below C=40 in the #2017 Eisenstein binary scalar-rectangle or fixed-support block-linear additive pairing model; specify a changed premise instead. This bound does not cover every complex decoder.", + "Continuing a partial cost improvement while leaving the same unpriced consumer, restoration or central-readout obligation unresolved; refresh the family expansion decision first. Local product-retiming evidence has a narrow scope and is not a ban on changed graphs or contracts." + ], + "overlap_terms": [ + "rank shape", + "block climb", + "masked decoder", + "overcomplete", + "effective rank" + ] + }, + "scope_status": "changed", + "actual_scope": "Construct and characterize one exact uniform pure partial Kx channel after changing the original-owner second-call pencil from P+2Q to P+Q, with an explicit fresh-owner sector and whole complement retained.", + "scope_change_reason": "PR4751 excludes all fresh-feed-only changes to the original coefficient-two scaffold. The canonical continuation handoff asks for a changed original-owner query. Resonance removes its unit pivot; this task requires an actual all-width channel rather than only a vanished pivot or a finite matrix kernel.", + "bottleneck_link": "A scoped algebraic side result identifies a nonzero target channel outside the fixed-original-owner obstruction. It does not provide a passing cost profile: full target recovery, physical preparation/routing, complement recovery and supplier bills are still open, so no packing-ceiling or saving claim is made.", + "budget_minutes": 60, + "stop_rule": "At 25 minutes stop exploration with an exact constructive partial channel or a useful general obstruction; use the remaining session for verification. Do not expand hook censuses or infer a completed unit from this partial channel.", + "outcome": "completed", + "evidence": "README.md gives the uniform group-word identity and all-width nonzero characterization. verify.py authenticates sources, derives the literal decoder, checks its actual free alphabet and complement, and certifies an exact trace-power norm formula plus six failure controls.", + "author": "JoyboyBrian", + "ai_assistance": "Substantial OpenAI Codex assistance for proof, exact implementation, source audit and independent agent review. No independent human or proof-kernel acceptance is claimed.", + "open_questions": [ + { + "question": "Can a changed paid chronology deliver a complete target with a charged return using this even-width partial channel?", + "why_it_matters": "The present channel has rank one at width two; no full Kx or Ky and no unit saving follows.", + "first_step": "Write a complete independent-target and complement ledger before extending the construction; price every additional call and physical preparation/return.", + "blocked_by": "Unpriced physical storage/routing, missing target complement, y target, restoration, recursive supplier and the family expansion gate." + }, + { + "question": "What is the exact rank of A_f for general even f?", + "why_it_matters": "The norm formula proves nonzero at every even width but does not determine delivered target dimension.", + "first_step": "Seek an analytic factorization of the frozen 256-word target coefficient, rather than a width-only census.", + "blocked_by": "Nonzero Hilbert-Schmidt norm is not an exact rank formula or a cost profile." + } + ] +} diff --git a/research/resonant-owner-extraction/VERIFY.json b/research/resonant-owner-extraction/VERIFY.json new file mode 100644 index 0000000000..a04d17f09d --- /dev/null +++ b/research/resonant-owner-extraction/VERIFY.json @@ -0,0 +1,32 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/staggered-single-owner-obstruction/retained/arithmetic.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Exact formal identity, actual free-alphabet decomposition, all-width norm polynomial, retained complement and six negative controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Same explicit validation with Python assertions disabled." + } + ] +} diff --git a/research/resonant-owner-extraction/verify.py b/research/resonant-owner-extraction/verify.py new file mode 100644 index 0000000000..03ac399707 --- /dev/null +++ b/research/resonant-owner-extraction/verify.py @@ -0,0 +1,276 @@ +#!/usr/bin/env python3 +"""Exact uniform group-word certificate for a resonant partial target channel.""" +import argparse +from fractions import Fraction as F +from functools import lru_cache +import hashlib +import json +from pathlib import Path +import types + +HERE = Path(__file__).resolve().parent +ARITHMETIC = 'research/staggered-single-owner-obstruction/retained/arithmetic.py' +ARITHMETIC_SHA = '0d277854396e4ceda1e0f26916bd576b6decb474c0692b6671ebf2595283ddb9' + + +def require(value, message): + if not value: + raise ValueError(message) + + +def verify(): + path = HERE.parent.parent / ARITHMETIC + data = path.read_bytes() + require(hashlib.sha256(data).hexdigest() == ARITHMETIC_SHA, 'arithmetic source hash') + v = types.ModuleType('arithmetic') + exec(compile(data, str(path), 'exec'), v.__dict__) + v.mm = lru_cache(maxsize=8192)(v.mm) + I = v.ident() + C = [v.c_letter(j) for j in range(3)] + S = v.s_letter(7) + U = v.monomial([0, 5, 2, 7, 4, 1, 6, 3]) + V = v.monomial([0, 2, 1, 3, 4, 6, 5, 7]) + T = v.monomial([0, 4, 2, 6, 1, 5, 3, 7]) + V21 = v.monomial([0, 1, 4, 5, 2, 3, 6, 7]) + P, Q, Q2 = v.word(S, U, S), v.word(S, V, S), v.word(S, V21, S) + W, N = v.pauli(0, 5), v.word(v.pauli(0, 2), V) + L, J, K = v.word(N, T), v.word(N, C[2]), v.word(*C) + a, b, central = v.pauli(1, 3), v.pauli(4, 4), v.scale(v.I, I) + + def plus(*rows): + out = {} + for row in rows: + for key, coefficient in row.items(): + out[key] = out.get(key, F(0)) + coefficient + return {key: value for key, value in out.items() if value} + + def scaled(row, coefficient): + return {key: value * coefficient for key, value in row.items() if value * coefficient} + + def product(left, right): + out = {} + for g, c in left.items(): + for h, d in right.items(): + word = v.mm(g, h) + out[word] = out.get(word, F(0)) + c * d + return {word: value for word, value in out.items() if value} + + def apply(operator, row): + out = {} + for g, c in operator.items(): + for (owner, h), d in row.items(): + key = owner, v.mm(g, h) + out[key] = out.get(key, F(0)) + c * d + return {key: value for key, value in out.items() if value} + + def left(g, row, c=1): + return apply({g: F(c)}, row) + + def monomial(matrix): + return (all(sum(c != v.ZERO for c in row) == 1 for row in matrix) + and all(sum(matrix[i][j] != v.ZERO for i in range(8)) == 1 for j in range(8)) + and all(c == v.ZERO or c in v.I_POWERS for row in matrix for c in row)) + + def describe(matrix): + require(monomial(matrix), 'fourth-root monomial') + places = [next(i for i in range(8) if matrix[i][j] != v.ZERO) for j in range(8)] + phases = [v.I_POWERS.index(matrix[places[j]][j]) for j in range(8)] + shift = places[0] + columns = [places[1 << j] ^ shift for j in range(3)] + for x in range(8): + image = shift + for j in range(3): + if x & (1 << j): + image ^= columns[j] + require(places[x] == image, 'actual free alphabet: affine permutation') + polynomial = phases[:] + for bit in range(3): + for mask in range(8): + if mask & (1 << bit): + polynomial[mask] = (polynomial[mask] - polynomial[mask ^ (1 << bit)]) % 4 + require(polynomial[7] == 0 and all(polynomial[m] % 2 == 0 for m in (3, 5, 6)), + 'actual free alphabet: linear plus even quadratic phase') + return {'permutation': places, 'phase_i': phases, + 'affine_shift': shift, 'affine_columns': columns, + 'phase_polynomial_mod4': polynomial} + + def serialize(operator): + records = [{'coefficient': str(c), **describe(g)} for g, c in operator.items()] + return sorted(records, key=lambda rec: (rec['permutation'], rec['phase_i'])) + + def project(row, representative): + out = {} + for (owner, word), c in row.items(): + quotient = v.mm(word, v.adjoint(representative)) + if owner == 0 and monomial(quotient): + out[quotient] = out.get(quotient, F(0)) + c + return {word: c for word, c in out.items() if c} + + def program(feed, coefficient=1): + x, y = {(0, I): F(1)}, {(1, I): F(1)} + u = left(C[0], x) + vv = left(C[0], plus(left(P, u), left(Q, u, coefficient))) + r = left(v.word(v.adjoint(L), J), plus(left(W, vv), left(T, feed))) + t = left(C[0], plus(left(P, r), left(Q, r, 2))) + z = left(J, plus(left(W, t), left(Q2, r), left(P, vv))) + return {'x': x, 'y': y, 'u': u, 'v': vv, 'r': r, 't': t, 'z': z} + + identity = {I: F(1)} + B = scaled(product(plus(identity, {a: F(-1)}), plus(identity, {b: F(-1)})), F(1, 4)) + complement = plus(identity, scaled(B, -1)) + require(v.mm(a, a) == I and v.mm(b, b) == I and v.mm(a, b) == v.mm(b, a), 'commuting involutions') + require(product(B, B) == B and plus(B, complement) == identity and product(B, complement) == {}, + 'source projector and whole complement') + output_projector = identity + for factor in (plus(identity, {v.mm(central, central): F(1)}), + plus(identity, {v.mm(central, v.pauli(1, 0)): F(1)}), + *[plus(identity, {v.pauli(0, 1 << j): F(1)}) for j in range(3)]): + output_projector = product(output_projector, factor) + output_projector = scaled(output_projector, F(1, 32)) + require(len(output_projector) == 32 and product(output_projector, output_projector) == output_projector, + 'uniform output projector') + rows = program(apply(B, {(1, I): F(1)})) + A0 = v.word(v.adjoint(L), J, W) + R4 = v.word(C[0], P, C[0]) + R7 = v.word(C[0], Q, A0, C[0], P, C[0]) + pivot = project(rows['z'], R7) + require(len(pivot) == 2 and list(pivot.values()) == [1, 1], 'resonant pencil') + g1, g2 = pivot + R = v.mm(v.adjoint(g1), g2) + powers = [I] + for _ in range(4): + powers.append(v.mm(powers[-1], R)) + require(powers[4] == I and len(set(powers[:4])) == 4, 'exact order four') + E = {v.mm(powers[j], v.adjoint(g1)): F((-1) ** j) for j in range(4)} + require(product(E, pivot) == {}, 'left annihilator in actual word algebra') + decoder = {name: {} for name in rows} + decoder['z'] = E + row = apply(E, rows['z']) + eliminations = [] + for name, representative in [('r', C[2]), ('v', R4), ('u', C[0]), ('x', I)]: + coefficient = project(row, representative) + old_pivot = project(rows[name], representative) + require(len(old_pivot) == 1, 'single free pivot') + pg, pc = next(iter(old_pivot.items())) + correction = {v.mm(g, v.adjoint(pg)): -c / pc for g, c in coefficient.items()} + decoder[name] = plus(decoder[name], correction) + row = plus(row, apply(correction, rows[name])) + require(project(row, representative) == {}, 'eliminated residual') + eliminations.append({'register': name, 'terms': len(correction)}) + require(row == plus(*(apply(decoder[name], rows[name]) for name in rows)), 'literal retained decoder') + final_decoder = {name: product(output_projector, op) for name, op in decoder.items()} + result = plus(*(apply(final_decoder[name], rows[name]) for name in rows)) + require(result == apply(output_projector, row), 'projected literal decoder') + require(result and all(owner == 0 for owner, _ in result), 'all-width y cancellation') + target = project(result, K) + require(len(target) == len(result), 'all x words in target coset') + require(result == apply(target, {(0, K): F(1)}), 'exact pure target identity') + # This also certifies that every actual monomial is in the engine free alphabet. + decoder_records = {name: serialize(op) for name, op in final_decoder.items()} + target_records = serialize(target) + source_records, output_records = serialize(B), serialize(output_projector) + + def tensor_monomial_sum(operator, width): + n = 8 ** width + out = [[v.ZERO for _ in range(n)] for _ in range(n)] + for g, coefficient in operator.items(): + d = describe(g) + for col in range(n): + rest, dest, phase, power = col, 0, 0, 1 + for _ in range(width): + digit, rest = rest % 8, rest // 8 + dest += power * d['permutation'][digit] + power *= 8 + phase += d['phase_i'][digit] + out[dest][col] = v.add(out[dest][col], v.mul(v.q(coefficient), v.I_POWERS[phase % 4])) + return out + + def gaussian_rank(matrix): + rows = [list(row) for row in matrix] + rank = 0 + def inverse(q): + norm = q[0] ** 2 + q[1] ** 2 + return (q[0] / norm, -q[1] / norm) + for col in range(len(rows[0])): + pivot = next((r for r in range(rank, len(rows)) if rows[r][col] != v.ZERO), None) + if pivot is None: + continue + rows[pivot], rows[rank] = rows[rank], rows[pivot] + inv = inverse(rows[rank][col]) + rows[rank] = [v.mul(inv, q) for q in rows[rank]] + for r in range(rank + 1, len(rows)): + scale = rows[r][col] + if scale != v.ZERO: + rows[r] = [v.add(x, v.mul((-scale[0], -scale[1]), y)) for x, y in zip(rows[r], rows[rank])] + rank += 1 + return rank + + widths = [] + for width in (1, 2): + concrete = tensor_monomial_sum(target, width) + nonzero = [(r, c, q) for r, values in enumerate(concrete) for c, q in enumerate(values) if q != v.ZERO] + rank = gaussian_rank(concrete) + expected_rank = 0 if width == 1 else 1 + require(rank == expected_rank, 'exact small-width channel rank: width=' + str(width) + ', actual=' + str(rank)) + widths.append({'width': width, 'target_coefficient_rank': rank, 'nonzero_entries': len(nonzero), + 'first_nonzero': [nonzero[0][0], nonzero[0][1], list(map(str, nonzero[0][2]))] if nonzero else None, + 'source_projector_rank': gaussian_rank(tensor_monomial_sum(B, width)), + 'output_projector_rank': gaussian_rank(tensor_monomial_sum(output_projector, width))}) + # Frobenius inner products tensorize word by word; collect exact trace powers. + norm_polynomial = {} + units = ((1, 0), (0, 1), (-1, 0), (0, -1)) + for first in target_records: + for second in target_records: + real = imag = 0 + for j in range(8): + if first['permutation'][j] == second['permutation'][j]: + unit = units[(second['phase_i'][j] - first['phase_i'][j]) % 4] + real += unit[0] + imag += unit[1] + key = real, imag + norm_polynomial[key] = norm_polynomial.get(key, F(0)) + F(first['coefficient']) * F(second['coefficient']) + norm_polynomial = {key: value for key, value in norm_polynomial.items() if value and key != (0, 0)} + require(norm_polynomial == {(8, 0): F(1), (-8, 0): F(1), (2, 0): F(-20), + (-2, 0): F(-20), (1, 0): F(32), (-1, 0): F(32)}, + 'all-width Hilbert-Schmidt norm polynomial') + controls = [] + def rejects(name, condition): + require(not condition, 'negative control incorrectly accepted: ' + name) + controls.append(name) + rejects('omit_output_projector', all(owner == 0 for owner, _ in row)) + wrong = program(apply(B, {(1, I): F(1)}), coefficient=2) + wrong_result = plus(*(apply(final_decoder[name], wrong[name]) for name in wrong)) + rejects('restore_original_coefficient_two', wrong_result == result) + unfed = program({(1, I): F(1)}) + unfed_result = plus(*(apply(final_decoder[name], unfed[name]) for name in unfed)) + rejects('omit_source_projector', all(owner == 0 for owner, _ in unfed_result)) + rejects('discard_source_complement', B == identity) + rejects('identify_central_minus_I_with_I', v.mm(central, central) == I) + rejects('infer_width_one_identity_at_width_two', widths[1]['target_coefficient_rank'] == widths[0]['target_coefficient_rank']) + return {'status': 'PASS_RESONANT_OWNER_EXTRACTION', 'source_arithmetic_sha256': ARITHMETIC_SHA, + 'source_projector': source_records, 'output_projector': output_records, + 'annihilator': serialize(E), 'relative_order': 4, 'eliminations': eliminations, + 'decoder_before_output_projector': {name: serialize(op) for name, op in decoder.items()}, + 'final_decoder_term_counts': {name: len(records) for name, records in decoder_records.items()}, + 'target_coefficient_sha256': hashlib.sha256(json.dumps(target_records, sort_keys=True).encode()).hexdigest(), + 'hilbert_schmidt_trace_powers': [{'base': list(key), 'coefficient': str(value)} for key, value in sorted(norm_polynomial.items())], + 'formal_target_terms': len(target), 'formal_y_terms': 0, 'width_checks': widths, + 'negative_controls': controls, + 'scope': 'Exact all-positive-width pure partial Kx channel; nonzero at every even width, rank one at width two, and zero at odd widths. No full Kx, Ky, restoration budget, recursive saving or multiplication theorem.'} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--write', action='store_true') + args = parser.parse_args() + result = verify() + target = HERE / 'RESULT.json' + if args.write: + target.write_text(json.dumps(result, indent=2, sort_keys=True) + '\n') + else: + require(json.loads(target.read_text()) == result, 'frozen receipt') + print(result['status']) + + +if __name__ == '__main__': + main()