From 2b7b84971377e389bb60bc99973e023084225dc9 Mon Sep 17 00:00:00 2001 From: JoyboyBrian Date: Thu, 22 Oct 2026 12:02:55 -0700 Subject: [PATCH] Prove a single-owner obstruction to staggered fresh-feed repair --- .../README.md | 228 ++++++ .../RESULT.json | 652 ++++++++++++++++++ .../SOURCES.json | 18 + .../TASK.json | 72 ++ .../VERIFY.json | 30 + .../retained/LICENSE | 201 ++++++ .../retained/NOTICE.md | 10 + .../retained/arithmetic.py | 233 +++++++ .../verify.py | 198 ++++++ 9 files changed, 1642 insertions(+) create mode 100644 research/staggered-single-owner-obstruction/README.md create mode 100644 research/staggered-single-owner-obstruction/RESULT.json create mode 100644 research/staggered-single-owner-obstruction/SOURCES.json create mode 100644 research/staggered-single-owner-obstruction/TASK.json create mode 100644 research/staggered-single-owner-obstruction/VERIFY.json create mode 100644 research/staggered-single-owner-obstruction/retained/LICENSE create mode 100644 research/staggered-single-owner-obstruction/retained/NOTICE.md create mode 100644 research/staggered-single-owner-obstruction/retained/arithmetic.py create mode 100644 research/staggered-single-owner-obstruction/verify.py diff --git a/research/staggered-single-owner-obstruction/README.md b/research/staggered-single-owner-obstruction/README.md new file mode 100644 index 0000000000..42cf519d17 --- /dev/null +++ b/research/staggered-single-owner-obstruction/README.md @@ -0,0 +1,228 @@ +# A single-owner obstruction to fresh-feed repair of the staggered prefix + +**A uniform-word obstruction, not a general small-unit lower bound.** In the +five-call staggered preparation of Yiyang's +[continuation handoff](https://github.com/Lyy-iiis/integer-mult-bounds/tree/dcd20b2112327d903babbddc654a535dcfdb1b63/research/phase-prefix-continuations), +changing only the fresh-owner feed cannot create a nonzero pure-target channel. +This includes all fourteen `Π±,f=(I±X_a^⊗f)/2` feeds with nonzero three-bit `a`, +while retaining the independent complementary input. In fact, the result holds +for **every uniform free feed B**, without an invertibility assumption on B. + +The new certificate sees only the original `x` input. Six retained registers +have a triangular, invertible coefficient matrix on six low-order left cosets. +The old two-owner graph screen used a unit on the fresh `y` side; replacing that +unit by a projector could invalidate that particular screen. The new screen +remains unchanged because it ignores the `y` coefficients entirely. Thus this +proposed change does not exploit the missing kernel-bearing interface. + +This closes the claimed fresh-feed scaffold and advises changing the original +`x` chronology before further construction. It does not exclude different +five-call preparations, general five-in-fourteen or six-in-seventeen programs, +fixed-width identities, or width-dependent scalar decoders. No κ or selected +frontier changes. + +## Exact program and model + +Use the predecessor's eight-dimensional base matrices, with words acting +right to left. `C_j=((1+i)I+(1-i)X_j)/2`, `K=C_0 C_1 C_2`, and +`S e_x=i^popcount(x)e_x`. Let `U=CNOT(0→2)`, `V=SWAP01`, `T=SWAP02`, and + +``` +P = S U S Q = S V S +Q2 = S SWAP21 S W = Z0 Z2 +N = Z1 V J = N C2 L = N T. +``` + +For a base word `g`, write `g_f=g^⊗f`. Each base word is tensorized **before** +forming sums, whose scalar coefficients stay independent of positive width f. +For any free uniform operator `B_f`, retain `x,y` and execute + +``` +u = C0_f x +v = C0_f (P_f + 2 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). +``` + +Each displayed line costs one call. `J_f` is a free monomial followed by one +`C2_f` call. All free intermediates and arbitrary extra zero scratch are +allowed. Keeping all seven registers strengthens the decoder, even if a real +implementation would overwrite some. Free copies and mixtures of retained +registers are allowed without restriction in the enlarged free group below. +The theorem does not treat an unrelated transformed `y` supplied by an oracle +as a free input. + +### Uniform-word algebra is not a width-one matrix algebra + +Let H be **all** 8×8 monomial matrices with fourth-root entries, retaining +central phases, and A=ℂ[H]. H is finite and contains the actual free letters. +Let G be the group of actual base matrices generated by H and the paid letters. +G need not be finite. A uniform word is a finite element of ℂ[G], evaluated at +width f by sending each actual matrix g to `g^⊗f`. The feed B belongs to A. +A decoder may use any coefficients in A on all retained registers. This +enlarges the actual engine, so its obstruction also applies to the original +free alphabet. Scalar mixing may be complex, but is fixed across widths. + +**Separation lemma (retained from the predecessor).** Distinct actual matrices +`g_1,...,g_n` are linearly independent as the families `(g_i^⊗f)_(f≥1)`. +Choose a complex linear functional ℓ whose values on these matrices are +nonzero and pairwise distinct; the excluded choices are finitely many proper +hyperplanes. Applying `ℓ^⊗f` for f=1,...,n to a uniform relation gives an +invertible Vandermonde matrix (with an additional nonzero diagonal factor). +Every coefficient therefore vanishes. Distinct global phases are not +identified. Consequently a claimed identity at every positive width is an +identity in ℂ[G]; an identity at width one alone is insufficient. + +Partition G into left cosets Hh. Their spans are independent copies of the +left A-module A. Projection onto any collection of left cosets commutes with +arbitrary free left processing. Exact base-matrix tests `g h^-1∈H` establish +membership in these **defined groups**, rather than extrapolating a finite +numeric rank to a statement about all widths. + +## New triangular certificate + +Put `A0=L^-1 J W` and define the single-word representatives + +``` +R4 = C0 P C0 +R6 = C0 P A0 C0 Q C0 +R7 = C0 Q A0 C0 P C0. +``` + +`I,C0,R4,C2,R7,R6,K` belong to seven distinct left H-cosets. The exact checker +verifies all 21 separating pairs over Gaussian rationals. Project the **x +coefficient only** onto the ordered six cosets + +``` +HI, HC0, HR4, HC2, HR7, HR6. +``` + +Order the six registers as `x,u,v,r,z,t`. Their coefficient matrix is + +| Register | HI | HC0 | HR4 | HC2 | HR7 | HR6 | +|---|---:|---:|---:|---:|---:|---:| +| x | 1 | 0 | 0 | 0 | 0 | 0 | +| u | 0 | 1 | 0 | 0 | 0 | 0 | +| v | 0 | 0 | 1 | 0 | 0 | 0 | +| r | 0 | 0 | 0 | U0 | 0 | 0 | +| z | 0 | * | 0 | * | D | 0 | +| t | * | 0 | 0 | 0 | * | 2 | + +The starred coefficients are explicit finite elements of A, not assumed zero. +`U0` is a monomial unit. All coefficient words, including the starred cells, +are recorded in [RESULT.json](RESULT.json). Neither the table nor its proof +depends on B: every changed feed is supported only on y. + +The only nontrivial diagonal is `D=g1+2g2`, where the fourth-root monomials are +specified by output row and phase exponent for input columns 0,...,7: + +``` +g1 permutation: 0 4 2 6 1 5 3 7 phases: 0 0 2 2 0 0 2 2 +g2 permutation: 1 0 7 6 5 4 3 2 phases: 3 1 0 2 3 1 2 0. +``` + +For `R=g1^-1 g2`, exact multiplication gives order four. In A, + +``` +(I+2R)(I-2R+4R²-8R³) = -15 I, +D^-1 = -(I-2R+4R²-8R³)g1^-1/15. +``` + +This is checked coefficientwise in the group algebra, as well as on the base +matrices. The identity tensorizes term by term with the same scalar +coefficients at every width. Thus every diagonal of the triangular table is +a unit in A; no commutativity assumption on A is needed. + +### Decoder consequence + +Suppose an arbitrary free mixture of retained registers is a pure target +`a K x + b K y`, with a,b∈A. Its six projected x coefficients vanish because +HK is distinct from every chosen coset. In the table, the HR6 column first +forces the coefficient of t to vanish; HR7 then forces the coefficient of z +to vanish; HC2, HR4, HC0 and HI successively force those of r,v,u,x to vanish. +This is elimination over A using the explicit units, not a ban on free +mixtures. The only remaining retained input is a free multiple of y. Its +coefficient lies in H, whereas a pure target lies in HK. Coset independence +forces that remaining coefficient and a,b to vanish as well. + +Therefore the retained A-span intersects the pure two-target module only in +zero, for every B∈A. The two target directions have dimension `2 dim(A)`. +One further paid call creates at most one new A-generator, increasing the +span by at most `dim(A)`, regardless of free copies or mixing. **At least two +additional calls are necessary after this five-call preparation.** This +extends the predecessor's endpoint conclusion across the whole fresh-feed +class. It does not prevent other preparations from using six calls for two +arrays, and supplies no global small-unit lower bound. + +## Evidence, scope and decision + +The written argument supplies the quantifiers. The checker authenticates and +compiles the retained arithmetic bytes, expands the actual program as finite +sums of distinct actual base words, verifies the triangular table and every +coset separation, and checks the unit inverse in the group algebra. It also +checks all fourteen originally claimed projector feeds and exact recovery of +their complements. The receipt is deterministic and does not regenerate by +default. Five controls cover missing pivots, replacing a residual by a target, +the singular coefficient-one pencil, the failure of a width-one identity to +tensorize as a sum, and central-phase separation. + +The family decision is **stop fresh-feed-only repair**. The five paid calls, +free feed/decoder allowance and two further-call necessity are proved in the +uniform word model. Physical storage, routing, precision and full supplier +costs are unknown here; no consumer cost is priced as zero in a κ calculation. +This is a structural screen, not an implementation expansion. + +Reproduce from the repository root with standard-library Python 3.12: + +```sh +python3.12 -B scripts/research_package.py --package research/staggered-single-owner-obstruction +``` + +Or copy the package alone and run `python3 -I -B verify.py` and +`python3 -I -O -B verify.py`. Both print +`PASS_STAGGERED_SINGLE_OWNER_OBSTRUCTION`. No Git or network is needed by the +direct verifier. No width-five hook rank engine, Lean, Docker, broad historical +suite or selected-construction replay is needed or claimed. + +## Sources and attribution + +- Yiyang (@Lyy-iiis), `phase-prefix-continuations` at + `dcd20b2112327d903babbddc654a535dcfdb1b63`: the exact staggered program, + two-owner graph screen, uniform-word separation lemma and concrete handoff. + Its unchanged `arithmetic.py` is retained here with SHA256 + `0d277854396e4ceda1e0f26916bd576b6decb474c0692b6671ebf2595283ddb9` + (Git blob `9130ce2171e4af01338be27e7ffbf1feaf88da9e`). The new checker adapts + its literal row expansion; the source notice is retained alongside it. +- Yiyang's [PR #4710](https://github.com/CrocSwap/integer-mult-bounds/pull/4710), + head `b0d5192390af493d626054b060921895df3c94d2`, supplies the phase-aligned + prefix and exact residual identities. +- lee-phys's [PR #4688](https://github.com/CrocSwap/integer-mult-bounds/pull/4688), + head `264c4b3cb13c82d171de352ecf60486dfb8d2bd4`, supplies the two-image + construction and hook engine; that expensive engine is not rerun here. +- Jacob Sussman's [PR #4628](https://github.com/CrocSwap/integer-mult-bounds/pull/4628), + head `ee4fd87f064017c23e5a86fc1dcfe0a5237caed3`, supplies the small-unit + model and existing lower bounds, with eumemic/#288 and Swapnil Jain P1/P2 + as credited there. Those bounds are not rederived. + +The source URLs and exact retained bytes provide provenance; none of these +unmerged commit objects is required at replay. Canonical base is +`b58ad9ef4d4e861b0eaa5dba41742bdc072dca51`, priority revision 7, selecting the +conditional κ 0.00302015. Initial overlap covered 506 open PRs, 3650 Discussion +records and the complete local-note inventory; it does not cover every closed +PR or code diff. [Canonical claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19130780). + +New single-owner witness, proof and checks: JoyboyBrian with substantial +OpenAI Codex assistance; Apache-2.0. This is author-checked exact evidence, +not independent human review or a formal-kernel proof. + +## Open next questions + +1. Change the original x path so its low-order triangular module loses a unit + pivot while retaining information. Start with a changed second/fourth call + and recompute this six-coset table before expensive hook ranks. A zero pivot + only removes this obstruction; it does not construct a target channel. +2. For any resulting candidate, produce a literal uniform pure-target + combination and charge recovery of every independent complement. The + present theorem supplies no such candidate and does not justify another + search that changes only B or enlarges the projector list. diff --git a/research/staggered-single-owner-obstruction/RESULT.json b/research/staggered-single-owner-obstruction/RESULT.json new file mode 100644 index 0000000000..0485746a40 --- /dev/null +++ b/research/staggered-single-owner-obstruction/RESULT.json @@ -0,0 +1,652 @@ +{ + "coefficient_table": [ + [ + [ + { + "coefficient": "1", + "permutation": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7 + ], + "phase_i": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ] + } + ], + [], + [], + [], + [], + [] + ], + [ + [], + [ + { + "coefficient": "1", + "permutation": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7 + ], + "phase_i": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ] + } + ], + [], + [], + [], + [] + ], + [ + [], + [], + [ + { + "coefficient": "1", + "permutation": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7 + ], + "phase_i": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ] + } + ], + [], + [], + [] + ], + [ + [], + [], + [], + [ + { + "coefficient": "1", + "permutation": [ + 4, + 0, + 6, + 2, + 1, + 5, + 3, + 7 + ], + "phase_i": [ + 2, + 0, + 0, + 2, + 1, + 1, + 3, + 3 + ] + } + ], + [], + [] + ], + [ + [], + [ + { + "coefficient": "1", + "permutation": [ + 2, + 6, + 3, + 7, + 0, + 4, + 1, + 5 + ], + "phase_i": [ + 1, + 3, + 1, + 3, + 1, + 3, + 1, + 3 + ] + }, + { + "coefficient": "2", + "permutation": [ + 2, + 3, + 4, + 5, + 0, + 1, + 6, + 7 + ], + "phase_i": [ + 1, + 1, + 2, + 2, + 1, + 1, + 0, + 0 + ] + } + ], + [], + [ + { + "coefficient": "4", + "permutation": [ + 2, + 0, + 6, + 4, + 3, + 1, + 7, + 5 + ], + "phase_i": [ + 1, + 1, + 1, + 1, + 3, + 3, + 3, + 3 + ] + }, + { + "coefficient": "1", + "permutation": [ + 2, + 0, + 3, + 1, + 4, + 6, + 5, + 7 + ], + "phase_i": [ + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 1 + ] + } + ], + [ + { + "coefficient": "1", + "permutation": [ + 0, + 4, + 2, + 6, + 1, + 5, + 3, + 7 + ], + "phase_i": [ + 0, + 0, + 2, + 2, + 0, + 0, + 2, + 2 + ] + }, + { + "coefficient": "2", + "permutation": [ + 1, + 0, + 7, + 6, + 5, + 4, + 3, + 2 + ], + "phase_i": [ + 3, + 1, + 0, + 2, + 3, + 1, + 2, + 0 + ] + } + ], + [] + ], + [ + [ + { + "coefficient": "1", + "permutation": [ + 5, + 1, + 7, + 3, + 4, + 0, + 6, + 2 + ], + "phase_i": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ] + } + ], + [], + [], + [], + [ + { + "coefficient": "2", + "permutation": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7 + ], + "phase_i": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ] + }, + { + "coefficient": "4", + "permutation": [ + 4, + 0, + 7, + 3, + 5, + 1, + 6, + 2 + ], + "phase_i": [ + 3, + 1, + 2, + 0, + 3, + 1, + 0, + 2 + ] + } + ], + [ + { + "coefficient": "2", + "permutation": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7 + ], + "phase_i": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ] + } + ] + ] + ], + "columns": [ + "I", + "C0", + "R4", + "C2", + "R7", + "R6" + ], + "coset_representative_sha256": { + "C0": "47a3996d2d0e67befee756f9806bbed2e93344cc331c53c15749ab19f41a3e3c", + "C2": "e43b7c8d5388dd88f650c204c3649f11e705d18da8807a6f6d010b2dd771ceef", + "I": "9c79cea778dbc704ee88acd7d9915d188f4066f801bde5274788299c77053cb4", + "K": "6f76aeb345e38c2e71c110a3715fc47ebdeca06e6e2c84bdce0600340eb8afa7", + "R4": "82efa93afd3e51b10d4fc65991d84a434ac7bc7af9799a1a3cd99965a5b497ad", + "R6": "79ad6de5ee983bde45824ee27ca368ba788524534b815d79d7869de81d40160a", + "R7": "2fb503308836dc2be008b163478317912be267188c9d97c0fc192dc60b8c6a7f" + }, + "last_unit": { + "g1": { + "permutation": [ + 0, + 4, + 2, + 6, + 1, + 5, + 3, + 7 + ], + "phase_i": [ + 0, + 0, + 2, + 2, + 0, + 0, + 2, + 2 + ] + }, + "g2": { + "permutation": [ + 1, + 0, + 7, + 6, + 5, + 4, + 3, + 2 + ], + "phase_i": [ + 3, + 1, + 0, + 2, + 3, + 1, + 2, + 0 + ] + }, + "inverse_polynomial": [ + "-1/15", + "2/15", + "-4/15", + "8/15" + ], + "order": 4, + "relative": { + "permutation": [ + 4, + 0, + 7, + 3, + 5, + 1, + 6, + 2 + ], + "phase_i": [ + 3, + 1, + 2, + 0, + 3, + 1, + 0, + 2 + ] + } + }, + "negative_controls": [ + "missing_t_pivot", + "target_substituted_for_residual", + "coefficient_one_is_not_a_unit", + "width_one_free_span_does_not_tensorize", + "central_phase_not_quotiented" + ], + "rows": [ + "x", + "u", + "v", + "r", + "z", + "t" + ], + "scope": "Uniform finite words over complex scalars independent of tensor width; any fresh-owner-only feed preserving the original x chronology. No fixed-width or global small-unit impossibility.", + "sector_variants": [ + { + "same_x_certificate": true, + "shift": 1, + "sign": -1 + }, + { + "same_x_certificate": true, + "shift": 1, + "sign": 1 + }, + { + "same_x_certificate": true, + "shift": 2, + "sign": -1 + }, + { + "same_x_certificate": true, + "shift": 2, + "sign": 1 + }, + { + "same_x_certificate": true, + "shift": 3, + "sign": -1 + }, + { + "same_x_certificate": true, + "shift": 3, + "sign": 1 + }, + { + "same_x_certificate": true, + "shift": 4, + "sign": -1 + }, + { + "same_x_certificate": true, + "shift": 4, + "sign": 1 + }, + { + "same_x_certificate": true, + "shift": 5, + "sign": -1 + }, + { + "same_x_certificate": true, + "shift": 5, + "sign": 1 + }, + { + "same_x_certificate": true, + "shift": 6, + "sign": -1 + }, + { + "same_x_certificate": true, + "shift": 6, + "sign": 1 + }, + { + "same_x_certificate": true, + "shift": 7, + "sign": -1 + }, + { + "same_x_certificate": true, + "shift": 7, + "sign": 1 + } + ], + "separated_coset_pairs": [ + [ + "I", + "C0" + ], + [ + "I", + "R4" + ], + [ + "C0", + "R4" + ], + [ + "I", + "C2" + ], + [ + "C0", + "C2" + ], + [ + "R4", + "C2" + ], + [ + "I", + "R7" + ], + [ + "C0", + "R7" + ], + [ + "R4", + "R7" + ], + [ + "C2", + "R7" + ], + [ + "I", + "R6" + ], + [ + "C0", + "R6" + ], + [ + "R4", + "R6" + ], + [ + "C2", + "R6" + ], + [ + "R7", + "R6" + ], + [ + "I", + "K" + ], + [ + "C0", + "K" + ], + [ + "R4", + "K" + ], + [ + "C2", + "K" + ], + [ + "R7", + "K" + ], + [ + "R6", + "K" + ] + ], + "source_arithmetic_sha256": "0d277854396e4ceda1e0f26916bd576b6decb474c0692b6671ebf2595283ddb9", + "status": "PASS_STAGGERED_SINGLE_OWNER_OBSTRUCTION" +} diff --git a/research/staggered-single-owner-obstruction/SOURCES.json b/research/staggered-single-owner-obstruction/SOURCES.json new file mode 100644 index 0000000000..4916cee8e5 --- /dev/null +++ b/research/staggered-single-owner-obstruction/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "b58ad9ef4d4e861b0eaa5dba41742bdc072dca51", + "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" + } + ] +} diff --git a/research/staggered-single-owner-obstruction/TASK.json b/research/staggered-single-owner-obstruction/TASK.json new file mode 100644 index 0000000000..192a23f572 --- /dev/null +++ b/research/staggered-single-owner-obstruction/TASK.json @@ -0,0 +1,72 @@ +{ + "schema_version": 1, + "task_id": "complex-rank-shape-decoder", + "priority_revision": 7, + "base_commit": "b58ad9ef4d4e861b0eaa5dba41742bdc072dca51", + "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": "Prove that every uniform free fresh-owner feed in the retained staggered five-call preparation leaves the pure two-target module disjoint from the retained span, using a single-owner triangular left-coset certificate.", + "scope_change_reason": "The user requests challenging tasks. The concrete #4710 continuation handoff asks for kernel-bearing partial-owner coefficients; the claimed fourteen complementary-sector feeds share an unchanged x path. A new x-only unit-triangular witness extends the scoped obstruction to every free feed B without requiring B invertible.", + "bottleneck_link": "Decides whether changing the fresh-owner coefficient can produce the missing target channel. It cannot in this scaffold, so a useful next attempt must change original-owner chronology rather than expand sector counts.", + "budget_minutes": 60, + "stop_rule": "Stop after the exact all-width obstruction or a genuine pure-target channel; do not rerun expensive hook censuses or generalize to all small-unit programs.", + "outcome": "completed", + "evidence": "README.md proves uniform-word separation and decoder elimination; verify.py checks every base-word coset, all coefficients, group-algebra inverse, fourteen feed variants and five controls.", + "author": "JoyboyBrian", + "ai_assistance": "Substantial OpenAI Codex assistance for proof, exact implementation and source audit; no independent human or proof-kernel acceptance claimed.", + "open_questions": [ + { + "question": "Which changed original-owner query removes the triangular low-order obstruction while retaining information?", + "why_it_matters": "The entire fresh-feed-only class is excluded by the same certificate.", + "first_step": "Change the second or fourth x query and recompute the six-coset table before hook ranks.", + "blocked_by": "A changed unit pivot only removes this obstruction; an actual uniform target identity and complement recovery remain required." + } + ] +} diff --git a/research/staggered-single-owner-obstruction/VERIFY.json b/research/staggered-single-owner-obstruction/VERIFY.json new file mode 100644 index 0000000000..5753df77a0 --- /dev/null +++ b/research/staggered-single-owner-obstruction/VERIFY.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 30, + "checks": "Exact uniform-word coset certificate, geometric inverse, fourteen complementary feeds and five controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 30, + "checks": "Same explicit checks with Python assertions disabled." + } + ] +} diff --git a/research/staggered-single-owner-obstruction/retained/LICENSE b/research/staggered-single-owner-obstruction/retained/LICENSE new file mode 100644 index 0000000000..261eeb9e9f --- /dev/null +++ b/research/staggered-single-owner-obstruction/retained/LICENSE @@ -0,0 +1,201 @@ + Apache License + Version 2.0, January 2004 + http://www.apache.org/licenses/ + + TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION + + 1. Definitions. + + "License" shall mean the terms and conditions for use, reproduction, + and distribution as defined by Sections 1 through 9 of this document. + + "Licensor" shall mean the copyright owner or entity authorized by + the copyright owner that is granting the License. + + "Legal Entity" shall mean the union of the acting entity and all + other entities that control, are controlled by, or are under common + control with that entity. For the purposes of this definition, + "control" means (i) the power, direct or indirect, to cause the + direction or management of such entity, whether by contract or + otherwise, or (ii) ownership of fifty percent (50%) or more of the + outstanding shares, or (iii) beneficial ownership of such entity. + + "You" (or "Your") shall mean an individual or Legal Entity + exercising permissions granted by this License. + + "Source" form shall mean the preferred form for making modifications, + including but not limited to software source code, documentation + source, and configuration files. + + "Object" form shall mean any form resulting from mechanical + transformation or translation of a Source form, including but + not limited to compiled object code, generated documentation, + and conversions to other media types. + + "Work" shall mean the work of authorship, whether in Source or + Object form, made available under the License, as indicated by a + copyright notice that is included in or attached to the work + (an example is provided in the Appendix below). + + "Derivative Works" shall mean any work, whether in Source or Object + form, that is based on (or derived from) the Work and for which the + editorial revisions, annotations, elaborations, or other modifications + represent, as a whole, an original work of authorship. For the purposes + of this License, Derivative Works shall not include works that remain + separable from, or merely link (or bind by name) to the interfaces of, + the Work and Derivative Works thereof. + + "Contribution" shall mean any work of authorship, including + the original version of the Work and any modifications or additions + to that Work or Derivative Works thereof, that is intentionally + submitted to Licensor for inclusion in the Work by the copyright owner + or by an individual or Legal Entity authorized to submit on behalf of + the copyright owner. For the purposes of this definition, "submitted" + means any form of electronic, verbal, or written communication sent + to the Licensor or its representatives, including but not limited to + communication on electronic mailing lists, source code control systems, + and issue tracking systems that are managed by, or on behalf of, the + Licensor for the purpose of discussing and improving the Work, but + excluding communication that is conspicuously marked or otherwise + designated in writing by the copyright owner as "Not a Contribution." + + "Contributor" shall mean Licensor and any individual or Legal Entity + on behalf of whom a Contribution has been received by Licensor and + subsequently incorporated within the Work. + + 2. Grant of Copyright License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + copyright license to reproduce, prepare Derivative Works of, + publicly display, publicly perform, sublicense, and distribute the + Work and such Derivative Works in Source or Object form. + + 3. Grant of Patent License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + (except as stated in this section) patent license to make, have made, + use, offer to sell, sell, import, and otherwise transfer the Work, + where such license applies only to those patent claims licensable + by such Contributor that are necessarily infringed by their + Contribution(s) alone or by combination of their Contribution(s) + with the Work to which such Contribution(s) was submitted. If You + institute patent litigation against any entity (including a + cross-claim or counterclaim in a lawsuit) alleging that the Work + or a Contribution incorporated within the Work constitutes direct + or contributory patent infringement, then any patent licenses + granted to You under this License for that Work shall terminate + as of the date such litigation is filed. + + 4. Redistribution. You may reproduce and distribute copies of the + Work or Derivative Works thereof in any medium, with or without + modifications, and in Source or Object form, provided that You + meet the following conditions: + + (a) You must give any other recipients of the Work or + Derivative Works a copy of this License; and + + (b) You must cause any modified files to carry prominent notices + stating that You changed the files; and + + (c) You must retain, in the Source form of any Derivative Works + that You distribute, all copyright, patent, trademark, and + attribution notices from the Source form of the Work, + excluding those notices that do not pertain to any part of + the Derivative Works; and + + (d) If the Work includes a "NOTICE" text file as part of its + distribution, then any Derivative Works that You distribute must + include a readable copy of the attribution notices contained + within such NOTICE file, excluding those notices that do not + pertain to any part of the Derivative Works, in at least one + of the following places: within a NOTICE text file distributed + as part of the Derivative Works; within the Source form or + documentation, if provided along with the Derivative Works; or, + within a display generated by the Derivative Works, if and + wherever such third-party notices normally appear. The contents + of the NOTICE file are for informational purposes only and + do not modify the License. You may add Your own attribution + notices within Derivative Works that You distribute, alongside + or as an addendum to the NOTICE text from the Work, provided + that such additional attribution notices cannot be construed + as modifying the License. + + You may add Your own copyright statement to Your modifications and + may provide additional or different license terms and conditions + for use, reproduction, or distribution of Your modifications, or + for any such Derivative Works as a whole, provided Your use, + reproduction, and distribution of the Work otherwise complies with + the conditions stated in this License. + + 5. Submission of Contributions. Unless You explicitly state otherwise, + any Contribution intentionally submitted for inclusion in the Work + by You to the Licensor shall be under the terms and conditions of + this License, without any additional terms or conditions. + Notwithstanding the above, nothing herein shall supersede or modify + the terms of any separate license agreement you may have executed + with Licensor regarding such Contributions. + + 6. Trademarks. This License does not grant permission to use the trade + names, trademarks, service marks, or product names of the Licensor, + except as required for reasonable and customary use in describing the + origin of the Work and reproducing the content of the NOTICE file. + + 7. Disclaimer of Warranty. Unless required by applicable law or + agreed to in writing, Licensor provides the Work (and each + Contributor provides its Contributions) on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or + implied, including, without limitation, any warranties or conditions + of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A + PARTICULAR PURPOSE. You are solely responsible for determining the + appropriateness of using or redistributing the Work and assume any + risks associated with Your exercise of permissions under this License. + + 8. Limitation of Liability. In no event and under no legal theory, + whether in tort (including negligence), contract, or otherwise, + unless required by applicable law (such as deliberate and grossly + negligent acts) or agreed to in writing, shall any Contributor be + liable to You for damages, including any direct, indirect, special, + incidental, or consequential damages of any character arising as a + result of this License or out of the use or inability to use the + Work (including but not limited to damages for loss of goodwill, + work stoppage, computer failure or malfunction, or any and all + other commercial damages or losses), even if such Contributor + has been advised of the possibility of such damages. + + 9. Accepting Warranty or Additional Liability. While redistributing + the Work or Derivative Works thereof, You may choose to offer, + and charge a fee for, acceptance of support, warranty, indemnity, + or other liability obligations and/or rights consistent with this + License. However, in accepting such obligations, You may act only + on Your own behalf and on Your sole responsibility, not on behalf + of any other Contributor, and only if You agree to indemnify, + defend, and hold each Contributor harmless for any liability + incurred by, or claims asserted against, such Contributor by reason + of your accepting any such warranty or additional liability. + + END OF TERMS AND CONDITIONS + + APPENDIX: How to apply the Apache License to your work. + + To apply the Apache License to your work, attach the following + boilerplate notice, with the fields enclosed by brackets "[]" + replaced with your own identifying information. (Don't include + the brackets!) The text should be enclosed in the appropriate + comment syntax for the file format. We also recommend that a + file or class name and description of purpose be included on the + same "printed page" as the copyright notice for easier + identification within third-party archives. + + Copyright [yyyy] [name of copyright owner] + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. diff --git a/research/staggered-single-owner-obstruction/retained/NOTICE.md b/research/staggered-single-owner-obstruction/retained/NOTICE.md new file mode 100644 index 0000000000..f87e39f041 --- /dev/null +++ b/research/staggered-single-owner-obstruction/retained/NOTICE.md @@ -0,0 +1,10 @@ +# Attribution + +The original two-image block3 prefix, hook representation, eight-cut family and Gaussian rank engine are from CrocSwap/integer-mult-bounds PR4688, by lee-phys, exact head264c4b3cb13c82d171de352ecf60486dfb8d2bd4: +https://github.com/CrocSwap/integer-mult-bounds/pull/4688 + +The unchanged source files in vendor/pr4688 are authenticated by SHA256. The underlying small-m goal and hook framework are also discussed in PR4628 by jacobalansussman: +https://github.com/CrocSwap/integer-mult-bounds/pull/4628 + +The phase-aligned two-call repair and its exact residual identity are PR4710, scientific commit e7988a43f523690c279232845ab2bfeabb5df10b, current head b0d5192390af493d626054b060921895df3c94d2: +https://github.com/CrocSwap/integer-mult-bounds/pull/4710 The arithmetic.py file is an unchanged copy of that contribution's standalone Gaussian-rational residual verifier. This handoff uses those identities and contributes two concrete continuation preparations, exact replay, and scoped graph obstructions. It does not claim that the predecessor authors proposed these two preparations or made the disproved continuation claim. diff --git a/research/staggered-single-owner-obstruction/retained/arithmetic.py b/research/staggered-single-owner-obstruction/retained/arithmetic.py new file mode 100644 index 0000000000..9130ce2171 --- /dev/null +++ b/research/staggered-single-owner-obstruction/retained/arithmetic.py @@ -0,0 +1,233 @@ +#!/usr/bin/env python3 +"""Exact residual and projector transport for the repaired two-call prefix. + +This verifier uses only the Python standard library. Entries are pairs of +fractions representing Gaussian rationals; no floating point or source checker +is used. Matrix words act right-to-left on e_x, x=x0+2*x1+4*x2. + +Provenance: C, U=CNOT(0->2), V=SWAP(0,1), and the original two-image prefix +are from CrocSwap/integer-mult-bounds PR #4688, exact head +264c4b3cb13c82d171de352ecf60486dfb8d2bd4, package +research/complex-two-image-hook-prefix. The repair P=S_all U S_all, +Q=S_all V S_all, and the residual identity below are this contribution. + +For EACH base letter A let A_f=A tensor ... tensor A (f factors). Define +F_f=C0_f (P_f+2 Q_f) C0_f. In particular F_f is NOT F_1 tensor ... tensor F_1. +We verify the two distinct word equalities + J W C0 P C0 = M C2, J W C0 Q C0 = K a. +Tensor functoriality applies separately to these two products. Linearity then +gives, for every positive integer f, with the SAME coefficient 2, + J_f W_f F_f = M_f C2_f + 2 K_f a_f. +This is an exact target-plus-one-call residual identity, not a 5-in-14 program. + +All scalar phases are attached to base letters before tensorization. Thus +(-A)_f=(-1)^f A_f. The projector sign map below retains this parity explicitly. +""" + +from __future__ import annotations + +import argparse +from fractions import Fraction as F +import json +from pathlib import Path + + +def q(real=0, imag=0): + return (F(real), F(imag)) + + +ZERO, ONE, I = q(), q(1), q(0, 1) +I_POWERS = (ONE, I, q(-1), q(0, -1)) + + +def add(x, y): + return (x[0] + y[0], x[1] + y[1]) + + +def mul(x, y): + return (x[0] * y[0] - x[1] * y[1], x[0] * y[1] + x[1] * y[0]) + + +def scale(c, a): + return tuple(tuple(mul(c, v) for v in row) for row in a) + + +def plus(a, b): + return tuple(tuple(add(x, y) for x, y in zip(ar, br)) for ar, br in zip(a, b)) + + +def mm(a, b): + n = len(a) + out = [[ZERO for _ in range(n)] for _ in range(n)] + for r in range(n): + for k in range(n): + if a[r][k] == ZERO: + continue + for c in range(n): + if b[k][c] != ZERO: + out[r][c] = add(out[r][c], mul(a[r][k], b[k][c])) + return tuple(tuple(row) for row in out) + + +def word(*letters): + out = ident(len(letters[0])) + for letter in letters: + out = mm(out, letter) + return out + + +def ident(n=8): + return tuple(tuple(ONE if r == c else ZERO for c in range(n)) for r in range(n)) + + +def adjoint(a): + return tuple(tuple((a[c][r][0], -a[c][r][1]) for c in range(len(a))) for r in range(len(a))) + + +def monomial(permutation, phases=None): + if phases is None: + phases = [0] * len(permutation) + n = len(permutation) + require(sorted(permutation) == list(range(n)), "invalid monomial permutation") + return tuple(tuple(I_POWERS[phases[c] % 4] if r == permutation[c] else ZERO for c in range(n)) for r in range(n)) + + +def pauli(x, z): + """Hermitian convention i^popcount(x&z) X^x Z^z, not bare X^x Z^z.""" + return monomial([j ^ x for j in range(8)], [(x & z).bit_count() + 2 * (j & z).bit_count() for j in range(8)]) + + +def c_letter(bit): + return plus(scale(q(F(1, 2), F(1, 2)), ident()), scale(q(F(1, 2), F(-1, 2)), pauli(1 << bit, 0))) + + +def s_letter(mask): + """Product of S gates on the selected bits, with phase sum mod4.""" + return monomial(list(range(8)), [(j & mask).bit_count() for j in range(8)]) + + +def conj(a, b): + return word(a, b, adjoint(a)) + + +def describe_pauli(a): + hits = [] + for x in range(8): + for z in range(8): + for exponent in range(4): + if a == scale(I_POWERS[exponent], pauli(x, z)): + hits.append({"label_x_or_8z": x | (8 * z), "phase_i_exponent": exponent}) + require(len(hits) == 1, "ambiguous or missing Hermitian Pauli label: " + str(hits)) + return hits[0] + + +def require(condition, message): + if not condition: + raise AssertionError(message) + + +def verify(): + e = ident() + c0, c1, c2 = (c_letter(j) for j in range(3)) + sall = s_letter(7) + u = monomial([0, 5, 2, 7, 4, 1, 6, 3]) + v = monomial([0, 2, 1, 3, 4, 6, 5, 7]) + p, qword = word(sall, u, sall), word(sall, v, sall) + zall = pauli(0, 7) + require(qword == word(zall, v), "Q=Z_all V") + # Normalize each paid and free base letter independently. + for name, a in (("C0", c0), ("C1", c1), ("C2", c2), ("S_all", sall), ("U", u), ("V", v), ("P", p), ("Q", qword)): + require(word(a, adjoint(a)) == e, name + " unitarity") + for bit, c in enumerate((c0, c1, c2)): + require(word(c, c) == pauli(1 << bit, 0), "C_bit^2=X_bit") + + k = word(c0, c1, c2) + a, b = pauli(1, 3), pauli(4, 4) # a=Y0 Z1, b=Y2. + w = pauli(0, 5) # W=Z0 Z2. + jword = word(pauli(0, 2), v, c2) # J=Z1 V C2: exactly one paid call. + m_perm = [2, 0, 3, 1, 4, 6, 5, 7] + m_phases = [0, 0, 2, 2, 1, 3, 3, 1] + m = monomial(m_perm, m_phases) + u20 = monomial([0, 1, 2, 3, 5, 4, 7, 6]) + cz02 = monomial(list(range(8)), [2 * (x & 1) * ((x >> 2) & 1) for x in range(8)]) + s_parity02 = monomial(list(range(8)), [((x & 5).bit_count() % 2) for x in range(8)]) + require(cz02 == word(s_letter(1), s_letter(4), adjoint(s_parity02)), "CZ uses allowed S of parity") + require(m == word(pauli(2, 0), v, u20, pauli(0, 2), s_letter(4), cz02), "M free-letter factorization") + + branch_p, branch_q = word(c0, p, c0), word(c0, qword, c0) + require(word(jword, w, branch_p) == word(m, c2), "P branch target residual") + require(word(jword, w, branch_q) == word(k, a), "Q branch target term") + prefix = plus(branch_p, scale(q(2), branch_q)) + require(word(jword, w, prefix) == plus(word(m, c2), scale(q(2), word(k, a))), "combined identity") + + middle_a, middle_b = pauli(0, 3), pauli(4, 4) + r = word(adjoint(p), qword) + require(word(r, r, r, r) == e, "R has order dividing4") + require(word(r, r) != e, "R has exact order4") + require(word(r, middle_a) == word(middle_a, r), "R commutes A") + require(word(r, middle_b) == word(middle_b, r), "R commutes B") + require(conj(adjoint(c0), middle_a) == a, "input a label") + require(conj(adjoint(c0), middle_b) == b, "input b label") + out_a, out_b = conj(word(c0, p), middle_a), conj(word(c0, p), middle_b) + require(out_a == scale(q(-1), a) and out_b == scale(q(-1), b), "base output signs") + require(word(prefix, a) == word(out_a, prefix), "prefix a transport") + require(word(prefix, b) == word(out_b, prefix), "prefix b transport") + require(conj(jword, a) == conj(k, a) and conj(jword, b) == conj(k, b), "one-call projector bridge") + lword = word(adjoint(jword), k) + gword = word(w, branch_p) + require(lword == word(v, pauli(0, 2), c0, c1), "residual L factorization") + require(word(lword, lword) == scale(q(-1), a), "L^2=-a at base width") + require(word(gword, gword) == scale(q(-1), e), "G^2=-I at base width") + require(word(w, branch_q) == word(a, lword), "Q branch with W") + for generator in (a, b): + require(word(lword, generator) == word(generator, lword), "L centralizes input sectors") + require(word(w, prefix, generator) == word(generator, w, prefix), "WF centralizes input sectors") + projectors = [] + for alpha in (1, -1): + for beta in (1, -1): + ep = scale(q(F(1, 4)), word(plus(e, scale(q(alpha), a)), plus(e, scale(q(beta), b)))) + ep_out = scale(q(F(1, 4)), word(plus(e, scale(q(-alpha), a)), plus(e, scale(q(-beta), b)))) + require(word(ep, ep) == ep, "projector idempotence") + require(word(prefix, ep) == word(ep_out, prefix), "base sector sign flip") + projectors.append(ep) + require(plus(plus(projectors[0], projectors[1]), plus(projectors[2], projectors[3])) == e, "complete four-sector partition") + for i in range(4): + for j in range(i): + require(word(projectors[i], projectors[j]) == scale(ZERO, e), "orthogonal sectors") + + # Meaningful negative controls: one wrong free phase and one wrong mixer. + wrong_phases = m_phases.copy() + wrong_phases[0] = 1 + require(word(jword, w, branch_p) != word(monomial(m_perm, wrong_phases), c2), "wrong M phase rejected") + require(word(jword, w, prefix) != plus(word(m, c2), word(k, a)), "wrong mixing coefficient rejected") + return { + "status": "PASS", + "arithmetic": "exact Gaussian rationals; Python stdlib Fraction pairs", + "branch_identities": ["J W C0 P C0 = M C2", "J W C0 Q C0 = K a"], + "all_width_identity": "J_f W_f F_f = M_f C2_f + 2 K_f a_f", + "all_width_reason": "Tensorize each branch word separately, then add with coefficient2; never tensorize the sum F_1.", + "M_permutation": m_perm, + "M_phase_i_exponents": m_phases, + "M_free_factorization": "X1 SWAP01 CNOT(2->0) Z1 S2 CZ02", + "input_generators": [describe_pauli(a), describe_pauli(b)], + "output_generators_at_base_width": [describe_pauli(out_a), describe_pauli(out_b)], + "target_generators_at_base_width": [describe_pauli(conj(k, a)), describe_pauli(conj(k, b))], + "all_width_projectors": "e(alpha,beta)=(I+alpha*a_f)(I+beta*b_f)/4; F_f e(alpha,beta)=e(epsilon*alpha,epsilon*beta)F_f, epsilon=(-1)^f", + "negative_controls": ["wrong M phase rejected", "wrong coefficient2 rejected"], + "limitation": "Exact residual and sector transport only; no independent-array 5-in-14 continuation or improved kappa is claimed.", + } + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--out", type=Path, help="Optional JSON receipt path; otherwise print only") + args = parser.parse_args() + result = verify() + data = json.dumps(result, indent=2) + "\n" + if args.out: + args.out.write_text(data) + print(data, end="") + + +if __name__ == "__main__": + main() diff --git a/research/staggered-single-owner-obstruction/verify.py b/research/staggered-single-owner-obstruction/verify.py new file mode 100644 index 0000000000..9984cdd7ff --- /dev/null +++ b/research/staggered-single-owner-obstruction/verify.py @@ -0,0 +1,198 @@ +#!/usr/bin/env python3 +"""Exact base-word certificate for a uniform single-owner coset obstruction.""" +import argparse +from fractions import Fraction as F +import hashlib +import json +from pathlib import Path +import types + +HERE = Path(__file__).resolve().parent +ARITHMETIC_SHA = '0d277854396e4ceda1e0f26916bd576b6decb474c0692b6671ebf2595283ddb9' + + +def require(value, message): + if not value: + raise ValueError(message) + + +def load(): + path = HERE / 'retained' / 'arithmetic.py' + data = path.read_bytes() + require(hashlib.sha256(data).hexdigest() == ARITHMETIC_SHA, 'retained arithmetic hash') + module = types.ModuleType('retained_arithmetic') + exec(compile(data, str(path), 'exec'), module.__dict__) + return module + + +def verify(): + v = load() + 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 = v.pauli(0, 5) + N = v.word(v.pauli(0, 2), V) + L, J = v.word(N, T), v.word(N, C[2]) + K = v.word(*C) + A = v.word(v.adjoint(L), J, W) + R4 = v.word(C[0], P, C[0]) + R6 = v.word(C[0], P, A, C[0], Q, C[0]) + R7 = v.word(C[0], Q, A, C[0], P, C[0]) + refs = [('I', I), ('C0', C[0]), ('R4', R4), ('C2', C[2]), ('R7', R7), ('R6', R6)] + row_order = ['x', 'u', 'v', 'r', 'z', 't'] + + def plus(*rows): + result = {} + for row in rows: + for key, coefficient in row.items(): + result[key] = result.get(key, F(0)) + coefficient + return {key: value for key, value in result.items() if value} + + def left(matrix, row, coefficient=F(1)): + result = {} + for (owner, word), value in row.items(): + key = owner, v.mm(matrix, word) + result[key] = result.get(key, F(0)) + coefficient * value + return {key: value for key, value in result.items() if value} + + def program(feed): + x = {(0, I): F(1)} + y = {(1, I): F(1)} + u = left(C[0], x) + vv = left(C[0], plus(left(P, u), left(Q, u, 2))) + 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} + + 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)] + return {'permutation': places, 'phase_i': [v.I_POWERS.index(matrix[places[j]][j]) for j in range(8)]} + + def digest(matrix): + return hashlib.sha256(json.dumps([[str(x) for pair in row for x in pair] for row in matrix]).encode()).hexdigest() + + def project(row): + out = [[] for _ in refs] + for (owner, word), coefficient in row.items(): + if owner != 0: + continue + for index, (_, representative) in enumerate(refs): + quotient = v.word(word, v.adjoint(representative)) + if monomial(quotient): + out[index].append((coefficient, quotient)) + return out + + def certificate(rows): + table = [project(rows[name]) for name in row_order] + require(all(not table[i][j] for i in range(6) for j in range(i + 1, 6)), 'triangular support') + require([c for c, _ in table[0][0]] == [1], 'x pivot') + require([c for c, _ in table[1][1]] == [1], 'u pivot') + require([c for c, _ in table[2][2]] == [1], 'v pivot') + require([c for c, _ in table[3][3]] == [1], 'r pivot') + require([c for c, _ in table[4][4]] == [1, 2], 'z unit pencil') + require([c for c, _ in table[5][5]] == [2], 't pivot') + return table + + all_refs = refs + [('K', K)] + separated = [] + for i, (name, representative) in enumerate(all_refs): + require(v.word(representative, v.adjoint(representative)) == I, 'unitary base word') + for other, value in all_refs[:i]: + require(not monomial(v.word(representative, v.adjoint(value))), 'distinct left H cosets') + separated.append([other, name]) + rows = program({(1, I): F(1)}) + table = certificate(rows) + g1, g2 = [matrix for _, matrix in table[4][4]] + R = v.word(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, 'relative monomial has exact order four') + # Verify in the group algebra, not only its possibly nonfaithful 8x8 representation. + polynomial = {powers[k]: F((-2) ** k) for k in range(4)} + multiplied = plus({(0, key): value for key, value in polynomial.items()}, + left(R, {(0, key): value for key, value in polynomial.items()}, 2)) + require(multiplied == {(0, I): F(-15)}, 'group-algebra geometric inverse') + inverse = v.scale(v.q(F(-1, 15)), v.plus(v.plus(I, v.scale(v.q(-2), powers[1])), + v.plus(v.scale(v.q(4), powers[2]), v.scale(v.q(-8), powers[3])))) + D = v.plus(g1, v.scale(v.q(2), g2)) + require(v.word(D, inverse, v.adjoint(g1)) == I, 'right concrete inverse') + require(v.word(inverse, v.adjoint(g1), D) == I, 'left concrete inverse') + + sectors = [] + y = {(1, I): F(1)} + for shift in range(1, 8): + X = v.pauli(shift, 0) + require(v.word(X, X) == I and X != I, 'nontrivial sector involution') + for sign in (-1, 1): + feed = plus(left(I, y, F(1, 2)), left(X, y, F(sign, 2))) + complement = plus(left(I, y, F(1, 2)), left(X, y, F(-sign, 2))) + require(plus(feed, complement) == y, 'fresh-owner complement retained') + changed = program(feed) + require(certificate(changed) == table, 'x certificate independent of sector feed') + sectors.append({'shift': shift, 'sign': sign, 'same_x_certificate': True}) + + controls = [] + def rejects(name, action): + try: + action() + except ValueError: + controls.append(name) + else: + raise ValueError('control accepted: ' + name) + + broken = dict(rows); broken['t'] = {} + rejects('missing_t_pivot', lambda: certificate(broken)) + broken2 = dict(rows); broken2['r'] = {(0, K): F(1)} + rejects('target_substituted_for_residual', lambda: certificate(broken2)) + bad_d = v.plus(g1, g2) + alternating = v.plus(v.plus(I, v.scale(v.q(-1), powers[1])), v.plus(powers[2], v.scale(v.q(-1), powers[3]))) + require(alternating != v.scale(v.ZERO, I) and v.word(bad_d, alternating) == v.scale(v.ZERO, I), 'coefficient-one singular control') + controls.append('coefficient_one_is_not_a_unit') + alpha, beta = v.q(F(1, 2), F(1, 2)), v.q(F(1, 2), F(-1, 2)) + require(C[0] == v.plus(v.scale(alpha, I), v.scale(beta, v.pauli(1, 0))), 'width-one free span calibration') + # At width two the (00,01) entry is alpha*beta=1/2, whereas a*I+b*(X tensor X) gives zero. + require(v.mul(alpha, beta) == v.q(F(1, 2)), 'width-one identity does not tensorize as a sum') + controls.append('width_one_free_span_does_not_tensorize') + require(v.scale(v.q(-1), I) != I and v.word(v.scale(v.q(-1), I), v.scale(v.q(-1), I)) == I, 'central phases remain distinct base words') + controls.append('central_phase_not_quotiented') + + return {'status': 'PASS_STAGGERED_SINGLE_OWNER_OBSTRUCTION', + 'source_arithmetic_sha256': ARITHMETIC_SHA, + 'rows': row_order, 'columns': [name for name, _ in refs], + 'coset_representative_sha256': {name: digest(matrix) for name, matrix in all_refs}, + 'separated_coset_pairs': separated, + 'coefficient_table': [[ [{'coefficient': str(c), **describe(g)} for c, g in cell] for cell in row] for row in table], + 'last_unit': {'g1': describe(g1), 'g2': describe(g2), 'relative': describe(R), 'order': 4, + 'inverse_polynomial': ['-1/15', '2/15', '-4/15', '8/15']}, + 'sector_variants': sectors, 'negative_controls': controls, + 'scope': 'Uniform finite words over complex scalars independent of tensor width; any fresh-owner-only feed preserving the original x chronology. No fixed-width or global small-unit impossibility.'} + + +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()