diff --git a/research/phase-aligned-two-call-prefix/NOTICE.md b/research/phase-aligned-two-call-prefix/NOTICE.md new file mode 100644 index 0000000000..91b45680f7 --- /dev/null +++ b/research/phase-aligned-two-call-prefix/NOTICE.md @@ -0,0 +1,7 @@ +# Attribution and provenance + +The unchanged files `vendor/pr4688/verify.py` and `vendor/pr4688/README.md` come from `research/complex-two-image-hook-prefix/` in lee-phys's CrocSwap/integer-mult-bounds PR #4688, commit `264c4b3cb13c82d171de352ecf60486dfb8d2bd4`. Their mathematical construction, model, rank engine, calibrations and seven controls are credited to that work. This package's main checker reuses the engine's sparse Gaussian arithmetic and exterior-power routines. + +Jacob Sussman's PR #4628, commit `ee4fd87f064017c23e5a86fc1dcfe0a5237caed3`, and its source repository jacobalansussman/wht-power-saving-lean, commit `86e575e28ed94890872dcff1bb2621d7ff559cbd`, are the sources of the block-3 engine model, the 14W/5 hook bound, the single-image obstruction and the singular-frame subgame motivating the phase repair. The present obstruction uses an explicit joint-target rank and does not depend on an unimplemented singular-frame theorem. + +New work in this package: the fresh-input target-deficit obstruction; the explicit S U S / S V S phase repair; the exact joint-rank and four-point-pencil calculations; the higher-width lifted-hook argument; and the independently checked residual interface when included. This work was produced by OpenAI Codex agents acting for Lyy-iiis. No contribution by the predecessors is claimed as new, and no Lean or human verification is claimed. diff --git a/research/phase-aligned-two-call-prefix/OVERLAP.json b/research/phase-aligned-two-call-prefix/OVERLAP.json new file mode 100644 index 0000000000..dfed15e160 --- /dev/null +++ b/research/phase-aligned-two-call-prefix/OVERLAP.json @@ -0,0 +1,46 @@ +{ + "checked_at_utc": "2026-10-22T17:15:40.151026+00:00", + "canonical_main": "b58ad9ef4d4e861b0eaa5dba41742bdc072dca51", + "open_prs": { + "count": 473, + "complete_pagination": true, + "fetched_at": "2026-10-22T16:59:54.607649+00:00" + }, + "discussions": { + "1166": { + "top_level_comments": 100, + "records_with_recent_replies": 101, + "coverage": "last100 top-level comments, at most last20 replies each; not complete history" + }, + "1167": { + "top_level_comments": 100, + "records_with_recent_replies": 109, + "coverage": "last100 top-level comments, at most last20 replies each; not complete history" + } + }, + "related_discussion_hits": [ + { + "url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19126887", + "author": "lee-phys", + "node_id": "DC_kwDOU-508s4BI9pn" + } + ], + "nearest_prs": [ + 4688, + 4628 + ], + "limitations": [ + "Full Discussions refresh was blocked by automatic approval review because the default authenticated CLI request unexpectedly targeted cafe.github.com. It was not retried.", + "Bounded Discussion reads instead used explicit official github.com host arguments; no complete historical coverage is claimed.", + "Sparse local notes were not a complete main-branch research inventory.", + "No matching follow-up in this bounded search is not a novelty certificate." + ], + "final_updated_pr_window": { + "checked_at_utc": "2026-10-22T17:17:34.430814+00:00", + "records": 100, + "order": "updated descending", + "matching_small_unit_followup": "Only credited predecessor #4688 found; its head remained264c4b3cb13c82d171de352ecf60486dfb8d2bd4", + "complete_open_queue_refresh": false + }, + "canonical_investigation": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19128894" +} diff --git a/research/phase-aligned-two-call-prefix/PINNED-SOURCES.json b/research/phase-aligned-two-call-prefix/PINNED-SOURCES.json new file mode 100644 index 0000000000..a26f0e5643 --- /dev/null +++ b/research/phase-aligned-two-call-prefix/PINNED-SOURCES.json @@ -0,0 +1,20 @@ +{ + "base_commit": "b58ad9ef4d4e861b0eaa5dba41742bdc072dca51", + "predecessor": { + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/4688", + "author": "lee-phys", + "head": "264c4b3cb13c82d171de352ecf60486dfb8d2bd4", + "path": "research/complex-two-image-hook-prefix", + "unchanged_files": { + "vendor/pr4688/verify.py": "99ff0beccd9a4e94cc607e02114d62b8ce0ea57ee00748b07ce0a0af91aec85e", + "vendor/pr4688/README.md": "91d45b5af6063e30c6860a4cb46cfc44960ecd67f37c3bce9675924e30b89b4e" + } + }, + "model_and_bound": { + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/4628", + "author": "jacobalansussman", + "head": "ee4fd87f064017c23e5a86fc1dcfe0a5237caed3", + "upstream_repository": "https://github.com/jacobalansussman/wht-power-saving-lean", + "upstream_commit": "86e575e28ed94890872dcff1bb2621d7ff559cbd" + } +} diff --git a/research/phase-aligned-two-call-prefix/README.md b/research/phase-aligned-two-call-prefix/README.md new file mode 100644 index 0000000000..ef39626e0b --- /dev/null +++ b/research/phase-aligned-two-call-prefix/README.md @@ -0,0 +1,152 @@ +# A target-compatible phase repair of the two-image block-3 prefix + +This package gives a necessary-condition obstruction for one proposed beginning of a five-array, fourteen-call unit, and an explicit phase repair that removes that obstruction. It does **not** give a completed unit or a new multiplication exponent. + +The starting construction is [lee-phys's PR #4688](https://github.com/CrocSwap/integer-mult-bounds/pull/4688), frozen at `264c4b3cb13c82d171de352ecf60486dfb8d2bd4`. That work proves that its two-call prefix is invertible at every digit width and gains the full 80 per call in eight block-3 hook cuts. We retain its exact rank engine unchanged, with its complete calibration and controls. Jacob Sussman's [PR #4628](https://github.com/CrocSwap/integer-mult-bounds/pull/4628), head `ee4fd87f064017c23e5a86fc1dcfe0a5237caed3`, supplies the engine model and hook lower bound. Neither predecessor claimed that hook equality itself guaranteed a completion. + +## The missing target-alignment condition + +Let `𝓥=C^8`, with addresses `x=x0+2*x1+4*x2`. Write + +- `C_j = ((1+i)/2) I + ((1-i)/2) X_j`, where `X_j` flips bit `j`; +- `C=C_0` and `K=C_2 C_1 C_0`; +- `U`: CNOT from bit 0 to bit 2; +- `V`: swap bits 0 and 1. + +Every letter acts by its tensor power at digit width `f`; a sum is implemented by mixing registers **after** the individual tensor powers. + +At width five, use `H=𝓥 tensor exterior^4(𝓥)`, of dimension 560, and the eight coordinate subspaces `N_b` of #4688. If `q_b:H->H/N_b`, the target has rank 224 and any one paid rank-one call adds at most 80 quotient rows. The two prefixes are + +``` +F_old,f = C_f (U_f + 2 V_f) C_f, +F_new,f = C_f (P_f + 2 Q_f) C_f, +S e_x = i^popcount(x) e_x, +P = S U S, +Q = S V S. +``` + +All factors in `P,Q` are admitted free letters. `S` is the product of the three one-coordinate S phases. Both prefixes use exactly two paid rank-one calls and one zero scratch register, with the same copy/mix/erase schedule as #4688 (replace its `U,V` branches by `P,Q`, and restore the retained first output using `Q^{-1}`). The second prefix contains genuine phase letters, not just Pauli signs. + +The exact ranks are: + +| Cuts `b` | `rank(q F_old)` | `rank([q K; q F_old])` | `rank(q F_new)` | `rank([q K; q F_new])` | +|---|---:|---:|---:|---:| +| 3, 6, 7 | 160 | **280** | 160 | **224** | +| 2, 8, 9, 12, 13 | 160 | 224 | 160 | 224 | + +All restrictions have domain `N_b`. These are ranks over `Q(i)`, calculated by exact Gaussian integer elimination. As in the predecessor, the implementation replaces each `C` by `I-iX` to remove a nonzero scalar. The two branches have equal paid-word length, so their common scalar cancels consistently in every pencil; independent nonzero scaling of target rows also preserves every joint rank. The second column of joint ranks is the extra test; measuring only the rank of the prefix does not detect the first prefix's misalignment. + +### Why the original literal beginning needs at least fifteen calls + +Fix the target rowspace `T` on all five independent inputs, and let `E` be the rowspace of the current stacked quotient observations. Define the remaining target deficit + +``` +d_T(E) = dim(T+E) - dim(E). +``` + +A free operation sends `E` into a subspace of itself, so it cannot decrease this deficit. For a paid call, retain the previous quotient rows conceptually: modulo those rows, at most `rank(q C|N)=80` new independent rows can appear. Consequently a paid call decreases `d_T` by at most 80. This argument permits arbitrary scratch, singular mixing and erasure. + +Suppose the **first two paid calls** are exactly the original #4688 prefix on one fresh independent input, and the other four inputs have not received paid work. For cut 3, the current rowspace has rank 160 and its union with the five target rowspaces has rank `280+4*224=1176`. Thus the deficit is **1016**, exceeding the capacity `12*80=960` of the twelve remaining calls. At least thirteen further calls are needed, for at least fifteen total. Keeping the first output `C_f y` does not help: #4688 already certifies `rank([q C; q F_old])=rank(q F_old)=160`. + +The same calculation for `W` fresh inputs gives the total lower bound `ceil((224*W+56)/80)` for this literal beginning. For example, six inputs would need at least eighteen calls, so it cannot begin a six-in-seventeen unit either. + +This is not an obstruction to an arbitrarily pre-encoded or later occurrence of the same word, nor a lower bound excluding five in fourteen generally. It is a statement about this literal two-call beginning on one fresh input. The original prefix's invertibility and full local gains remain valid. + +For the repaired prefix, the corresponding deficit is `64+4*224=960`. It passes this necessary test exactly. This equality does not supply a continuation. + +## An exact all-width inverse + +Both `U,V` are involutions. The relative monomial is + +``` +R=P^{-1}Q = S^{-1} U^{-1} V S, +R^4=I, +(I+2R)(I-2R+4R^2-8R^3)=-15I. +``` + +The same identity holds for `R_f=R^{tensor f}` at every positive `f`. Since `P_f+2Q_f=P_f(I+2R_f)`, the free middle operator is invertible with a fixed rational inverse. The two outside calls are invertible too. Thus clearing the retained first output loses no input information. No inverse has to be executed by the forward prefix. + +There is also no width-dependent conditioning loss: all outside factors are unitary and the eigenvalues of `R_f` are fourth roots of unity. The singular values of the prefix therefore belong to `{1,sqrt(5),3}`, with both extremes present for every positive width. Its Euclidean condition number is exactly 3. The original prefix has this same property; it is not a unique benefit of the repair and is not a full outer precision theorem. + +## The natural higher-width hook tests also pass + +The result is stronger than a width-five numerical coincidence. Put + +``` +A=C P C, B=C Q C, +A5=rho(A), B5=rho(B), K5=rho(K), +rho(g)=g tensor exterior^4(g). +``` + +The checker proves, separately for each of the eight cuts: + +1. `rank([q K5; q A5])=rank([q K5; q B5])=224`. Equivalently, each branch separately annihilates `ker(q K5)` after applying `q`. +2. All four pencil matrices `q(A5+2 lambda B5)|N`, for `lambda=1,-1,i,-i`, have rank **160**. + +For `r` additional digit columns, use the invariant space `H tensor 𝓥^{tensor r}` and the kept subspace `N_b tensor 𝓥^{tensor r}`. The relative single-column matrix `A^{-1}B=C^{-1}RC` has fourth power one and eigenvalue multiplicities `4,2,1,1`. Multiplying by an invertible matrix in the additional columns reduces the quotient prefix to the direct sum of the four pencil evaluations, with the multiplicities of `(A^{-1}B)^{tensor r}`. Its rank is therefore exactly + +``` +160 * 8^r. +``` + +The branchwise kernel inclusions tensor with the additional columns, so the joint target-prefix rank is exactly `224*8^r`. This proves zero alignment defect and two maximal call gains for **all these lifted cuts**, at every `r>=0`. In particular the width-six ranks are 1280 for the prefix and 1792 for the target and joint state. + +This does not claim that every possible higher-width certificate passes, that all output end conditions hold, or that a multi-input completion exists. + +## A concrete residual interface for further work + +The repaired prefix also has an explicit all-width relation to the target. With Hermitian Paulis `Y_j=i X_j Z_j`, put + +``` +a=Y0 Z1, W=Z0 Z2, J=Z1 V C2, +M=X1 V CNOT(2->0) Z1 S2 CZ02. +``` + +`J` uses one paid call and `M` is entirely free. The independent standard-library checker `verify_residual.py` multiplies actual 8-by-8 matrices over Gaussian rationals and verifies the two **word** identities + +``` +J W C0 P C0 = M C2, +J W C0 Q C0 = K a. +``` + +Tensorize these identities separately and then add the second with coefficient 2. For every positive digit width, + +``` +J_f W_f F_new,f = M_f C2_f + 2 K_f a_f. +``` + +Thus the remaining contamination is exactly a free image of one paid call, rather than an unspecified operator. This gives a precise cross-input cancellation problem. The formula itself is not a saving: directly computing both terms is insufficient to deliver five independent targets in fourteen calls. + +The same checker verifies four actual free projector sectors, generated on input by the commuting Hermitian Paulis `a=Y0 Z1` and `b=Y2`. At width `f`, set `e(alpha,beta)=(I+alpha*a_f)(I+beta*b_f)/4`. The prefix transports this projector to `e(epsilon*alpha,epsilon*beta)`, where `epsilon=(-1)^f`. These projectors can pack pieces of distinct independent inputs and separate them after the two-call prefix, but the other pieces must also be preserved and eventually processed. This is a feasible interface, not a complete unit. + +## Reproduction + +Only the Python standard library is required. No network, solver, floating point rank, or source checkout is used. + +```sh +python3 -B verify.py --check RESULT.json +python3 -O -B verify.py --check RESULT.json +``` + +The checker authenticates the unchanged #4688 engine and README, runs that predecessor's complete calibration and seven controls, computes the new Gaussian ranks, verifies the four-point pencils and the actual monomial inverse, and checks the exact deficit arithmetic. It also invokes the independent Gaussian-rational residual checker, including its wrong-phase and wrong-coefficient controls. Regenerate the deterministic report with `python3 -B verify.py --out RESULT.json`. + +The frozen predecessor engine is retained under `vendor/pr4688`; its provenance and hashes are in `PINNED-SOURCES.json` and `NOTICE.md`. No Lean proof or human review is claimed. + +The registered repository replay is: + +```sh +python3 scripts/research_package.py --package research/phase-aligned-two-call-prefix +``` + +## Open next questions + +1. Complete the repaired prefix to five independent transforms in fourteen calls. Start with the explicit residual identity and the four Pauli sectors, preserving every complementary input piece and restored scratch. A literal all-width continuation and its complete paid bill remain missing. +2. Test other width-six invariant subspaces and output end conditions. The proof above covers every natural `H tensor V^r` hook lift; it does not cover every invariant of the engine game. + +The structured questions, scope change and current-priority provenance are recorded in `TASK.json`. The selected frontier is unchanged. + +## Attribution and review scope + +Prepared by Yiyang (@Lyy-iiis), with substantial OpenAI Codex assistance in parallel research, implementation and independent agent review. New work is Apache-2.0. Credit lee-phys's #4688 for the original two-image construction, rank engine and controls; Jacob Sussman's #4628 and its retained sources for the model and lower bound; and the predecessors credited in the unchanged source README. The new result is the target-deficit analysis, explicit phase repair, lifted-hook proof and residual interface. No independent human review or full multiplication-theorem verification is claimed. + +`SOURCES.json` authenticates the vendored files through their first preservation commit on this branch; their Git blob IDs are also checked equal to the files at the original #4688 head. The original commit, paths and SHA256 hashes are recorded separately in `PINNED-SOURCES.json`. No predecessor branch is merged or modified. diff --git a/research/phase-aligned-two-call-prefix/RESULT.json b/research/phase-aligned-two-call-prefix/RESULT.json new file mode 100644 index 0000000000..5973ffc647 --- /dev/null +++ b/research/phase-aligned-two-call-prefix/RESULT.json @@ -0,0 +1,374 @@ +{ + "all_extra_widths": { + "extra_width_variable": "r >= 0", + "prefix_rank_each_lifted_cut": "160*8^r", + "proof": "four eigenvalues of relative branch matrix; four-point pencil ranks and termwise kernel inclusion", + "target_and_joint_rank_each_lifted_cut": "224*8^r" + }, + "arithmetic": "Gaussian integer elimination over Q(i), no numerical rank tolerance", + "cuts": [ + { + "N_dimension": 224, + "mask": 2, + "new_missing_target_dimensions": 64, + "new_pencil_ranks_coefficients_2_minus2_2i_minus2i": [ + 160, + 160, + 160, + 160 + ], + "new_prefix_rank": 160, + "new_single_branch_target_joint_ranks": [ + 224, + 224 + ], + "new_target_joint_rank": 224, + "old_missing_target_dimensions": 64, + "old_prefix_rank": 160, + "old_target_joint_rank": 224, + "target_rank": 224, + "width6_lifted_prefix_rank": 1280, + "width6_lifted_target_and_joint_rank": 1792 + }, + { + "N_dimension": 280, + "mask": 3, + "new_missing_target_dimensions": 64, + "new_pencil_ranks_coefficients_2_minus2_2i_minus2i": [ + 160, + 160, + 160, + 160 + ], + "new_prefix_rank": 160, + "new_single_branch_target_joint_ranks": [ + 224, + 224 + ], + "new_target_joint_rank": 224, + "old_missing_target_dimensions": 120, + "old_prefix_rank": 160, + "old_target_joint_rank": 280, + "target_rank": 224, + "width6_lifted_prefix_rank": 1280, + "width6_lifted_target_and_joint_rank": 1792 + }, + { + "N_dimension": 280, + "mask": 6, + "new_missing_target_dimensions": 64, + "new_pencil_ranks_coefficients_2_minus2_2i_minus2i": [ + 160, + 160, + 160, + 160 + ], + "new_prefix_rank": 160, + "new_single_branch_target_joint_ranks": [ + 224, + 224 + ], + "new_target_joint_rank": 224, + "old_missing_target_dimensions": 120, + "old_prefix_rank": 160, + "old_target_joint_rank": 280, + "target_rank": 224, + "width6_lifted_prefix_rank": 1280, + "width6_lifted_target_and_joint_rank": 1792 + }, + { + "N_dimension": 336, + "mask": 7, + "new_missing_target_dimensions": 64, + "new_pencil_ranks_coefficients_2_minus2_2i_minus2i": [ + 160, + 160, + 160, + 160 + ], + "new_prefix_rank": 160, + "new_single_branch_target_joint_ranks": [ + 224, + 224 + ], + "new_target_joint_rank": 224, + "old_missing_target_dimensions": 120, + "old_prefix_rank": 160, + "old_target_joint_rank": 280, + "target_rank": 224, + "width6_lifted_prefix_rank": 1280, + "width6_lifted_target_and_joint_rank": 1792 + }, + { + "N_dimension": 224, + "mask": 8, + "new_missing_target_dimensions": 64, + "new_pencil_ranks_coefficients_2_minus2_2i_minus2i": [ + 160, + 160, + 160, + 160 + ], + "new_prefix_rank": 160, + "new_single_branch_target_joint_ranks": [ + 224, + 224 + ], + "new_target_joint_rank": 224, + "old_missing_target_dimensions": 64, + "old_prefix_rank": 160, + "old_target_joint_rank": 224, + "target_rank": 224, + "width6_lifted_prefix_rank": 1280, + "width6_lifted_target_and_joint_rank": 1792 + }, + { + "N_dimension": 280, + "mask": 9, + "new_missing_target_dimensions": 64, + "new_pencil_ranks_coefficients_2_minus2_2i_minus2i": [ + 160, + 160, + 160, + 160 + ], + "new_prefix_rank": 160, + "new_single_branch_target_joint_ranks": [ + 224, + 224 + ], + "new_target_joint_rank": 224, + "old_missing_target_dimensions": 64, + "old_prefix_rank": 160, + "old_target_joint_rank": 224, + "target_rank": 224, + "width6_lifted_prefix_rank": 1280, + "width6_lifted_target_and_joint_rank": 1792 + }, + { + "N_dimension": 280, + "mask": 12, + "new_missing_target_dimensions": 64, + "new_pencil_ranks_coefficients_2_minus2_2i_minus2i": [ + 160, + 160, + 160, + 160 + ], + "new_prefix_rank": 160, + "new_single_branch_target_joint_ranks": [ + 224, + 224 + ], + "new_target_joint_rank": 224, + "old_missing_target_dimensions": 64, + "old_prefix_rank": 160, + "old_target_joint_rank": 224, + "target_rank": 224, + "width6_lifted_prefix_rank": 1280, + "width6_lifted_target_and_joint_rank": 1792 + }, + { + "N_dimension": 336, + "mask": 13, + "new_missing_target_dimensions": 64, + "new_pencil_ranks_coefficients_2_minus2_2i_minus2i": [ + 160, + 160, + 160, + 160 + ], + "new_prefix_rank": 160, + "new_single_branch_target_joint_ranks": [ + 224, + 224 + ], + "new_target_joint_rank": 224, + "old_missing_target_dimensions": 64, + "old_prefix_rank": 160, + "old_target_joint_rank": 224, + "target_rank": 224, + "width6_lifted_prefix_rank": 1280, + "width6_lifted_target_and_joint_rank": 1792 + } + ], + "exact_residual_interface": { + "M_free_factorization": "X1 SWAP01 CNOT(2->0) Z1 S2 CZ02", + "M_permutation": [ + 2, + 0, + 3, + 1, + 4, + 6, + 5, + 7 + ], + "M_phase_i_exponents": [ + 0, + 0, + 2, + 2, + 1, + 3, + 3, + 1 + ], + "all_width_identity": "J_f W_f F_f = M_f C2_f + 2 K_f a_f", + "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", + "all_width_reason": "Tensorize each branch word separately, then add with coefficient2; never tensorize the sum F_1.", + "arithmetic": "exact Gaussian rationals; Python stdlib Fraction pairs", + "branch_identities": [ + "J W C0 P C0 = M C2", + "J W C0 Q C0 = K a" + ], + "input_generators": [ + { + "label_x_or_8z": 25, + "phase_i_exponent": 0 + }, + { + "label_x_or_8z": 36, + "phase_i_exponent": 0 + } + ], + "limitation": "Exact residual and sector transport only; no independent-array 5-in-14 continuation or improved kappa is claimed.", + "negative_controls": [ + "wrong M phase rejected", + "wrong coefficient2 rejected" + ], + "output_generators_at_base_width": [ + { + "label_x_or_8z": 25, + "phase_i_exponent": 2 + }, + { + "label_x_or_8z": 36, + "phase_i_exponent": 2 + } + ], + "status": "PASS", + "target_generators_at_base_width": [ + { + "label_x_or_8z": 26, + "phase_i_exponent": 2 + }, + { + "label_x_or_8z": 32, + "phase_i_exponent": 0 + } + ] + }, + "monomial_inverse": { + "P": { + "permutation": [ + 0, + 5, + 2, + 7, + 4, + 1, + 6, + 3 + ], + "phase_exponents_mod4": [ + 0, + 3, + 2, + 1, + 2, + 3, + 0, + 1 + ] + }, + "Q": { + "permutation": [ + 0, + 2, + 1, + 3, + 4, + 6, + 5, + 7 + ], + "phase_exponents_mod4": [ + 0, + 2, + 2, + 0, + 2, + 0, + 0, + 2 + ] + }, + "R": { + "permutation": [ + 0, + 2, + 5, + 7, + 4, + 6, + 1, + 3 + ], + "phase_exponents_mod4": [ + 0, + 0, + 3, + 3, + 0, + 0, + 1, + 1 + ] + }, + "R_order": 4, + "eigenvalue_multiplicities_1_minus1_i_minusi": [ + 4, + 2, + 1, + 1 + ], + "inverse_polynomial_product": [ + -15, + 0, + 0, + 0 + ], + "negative_control": "one changed R phase fails R^4=I", + "traces_R_powers": [ + [ + 8, + 0 + ], + [ + 2, + 0 + ], + [ + 4, + 0 + ], + [ + 2, + 0 + ] + ] + }, + "original_five_array_remaining_deficit": 1016, + "remaining_twelve_call_capacity": 960, + "repaired_five_array_remaining_deficit": 960, + "result": "PASS", + "schema_version": 1, + "scope": "two-call prefix and necessary continuation conditions; no completed unit or new exponent", + "source_head": "264c4b3cb13c82d171de352ecf60486dfb8d2bd4", + "source_pr": 4688, + "source_sha256": { + "vendor/pr4688/README.md": "91d45b5af6063e30c6860a4cb46cfc44960ecd67f37c3bce9675924e30b89b4e", + "vendor/pr4688/verify.py": "99ff0beccd9a4e94cc607e02114d62b8ce0ea57ee00748b07ce0a0af91aec85e" + } +} diff --git a/research/phase-aligned-two-call-prefix/REVIEW.md b/research/phase-aligned-two-call-prefix/REVIEW.md new file mode 100644 index 0000000000..a0786a397a --- /dev/null +++ b/research/phase-aligned-two-call-prefix/REVIEW.md @@ -0,0 +1,84 @@ +# Independent subagent review of the phase-aligned prefix + +Reviewed on 22 October 2026 by the `refit_candidate` OpenAI Codex agent for +Yiyang. This is a second computational/mathematical review in the same agent +team, not independent human review. No candidate files were modified. + +Verdict: the stated local construction, fixed-target continuation obstruction, +and all-extra-width hook-rank argument are sound within the explicit scope. +No completed five-in-fourteen unit or improved multiplication bound follows. + +## Fixed-target missing dimensions + +Let E be the span of all current quotient rows on the original input domain, +and fix the required target rowspace T. Then + +`d_T(E)=dim(T)-dim(T intersection E)`. + +A free letter preserving N induces a map on H/N. Its new rows are combinations +of the old quotient rows. Copies, arbitrary scalar register mixing and erasure +therefore give E_new contained in E and cannot decrease d_T. + +For one paid operation C on one current register A, choose any linear +projection p onto N. The new quotient map is + +`q C A = q C p A + q C (I-p) A`. + +The second summand factors through qA, whose rows were already in E. The first +has rank at most rank(qC restricted to N)=80. Thus E_new is contained in E+W +for some W of dimension at most80, even if old rows are erased. Hence +`d_T(E_new) >= d_T(E)-80`. No injectivity assumption on the state or the free +mixing is needed. + +For the literal two-call beginning on one fresh input, the bad cut has +dim(E)=160 and dim(T+E)=280+4*224=1176. Its remaining deficit1016 requires +at least13 more calls. A retained copy of the first paid output adds no +quotient rows because its stacked rank with F_old is already160. This proves +fifteen total for that beginning only. It does not rule out arbitrary +pre-encoding, later reuse of the word, or a general five-in-fourteen circuit. + +The repair changes the joint rank to224, so the remaining deficit is exactly +64+4*224=960. Matching the twelve-call capacity is a necessary condition, +not a continuation algorithm. + +## All-extra-width argument + +The new family is a sum of two individually tensorized branches. It is never +the tensor power of the two-branch sum. On H tensor V^r it has the form + +`A5 tensor A^tensor r + 2 B5 tensor B^tensor r`. + +Left multiplication by the invertible extra-column operator +`(A^tensor r)^-1` reduces this to +`A5 tensor I + 2 B5 tensor (A^-1 B)^tensor r`. +The relative operator is similar to R=P^-1Q, with R^4=I. Over characteristic +zero it is diagonalizable and all eigenvalues lie in {1,-1,i,-i}. The four +checked pencil ranks are all160, so every spectral summand has that rank; +summing their multiplicities gives160*8^r. Exact branchwise containment in +the target rowspace tensors with the additional columns, giving joint rank +224*8^r. This proves the advertised family of lifted cuts for f=5+r, r>=0. +It does not assert every possible certificate at every width passes. + +The invertibility proof is separate and applies to every positive digit +width: R_f^4=I and +`(I+2R_f)(I-2R_f+4R_f^2-8R_f^3)=-15I`. +No inverse needs to be executed by the forward two-call prefix. The schedule +must restore its retained first output using Q^-1, not Q; the README says so. + +## Residual and sector phases + +The two exact branch-word identities are sufficient to tensorize the residual +identity without tensorizing a sum. The coefficient2 remains2 at every width. +The explicit free factorization of M uses only Pauli, address permutation and +S/parity phase letters; J has exactly one paid C2 call. + +For the sector transport, R commutes with both middle generators. Together +with the checked input and output conjugations this gives the intertwining +identity separately for both branches, not merely for their width-one sum. +Consequently the tensor sign is epsilon=(-1)^f, exactly as stated. The four +sector projections preserve the omitted pieces as an outstanding obligation; +they do not create independent-array target credit automatically. + +## Verification scope + +This note records an independent agent review in the same research team. The exact package replay is the reproducible numerical evidence; this review is not independent human or formal-kernel acceptance. The phase alphabet and fresh-input beginning are explicit premises. diff --git a/research/phase-aligned-two-call-prefix/SOURCES.json b/research/phase-aligned-two-call-prefix/SOURCES.json new file mode 100644 index 0000000000..0dacb1a92f --- /dev/null +++ b/research/phase-aligned-two-call-prefix/SOURCES.json @@ -0,0 +1,42 @@ +{ + "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" + }, + { + "path": "research/phase-aligned-two-call-prefix/vendor/pr4688/verify.py", + "usage": "input", + "git_blob": "8d2815a2806894bcc50fb34e854f4ef7632ea588", + "sha256": "99ff0beccd9a4e94cc607e02114d62b8ce0ea57ee00748b07ce0a0af91aec85e", + "pin": "head:03e78a0a562f5099d0fffdfc4d6768875052bd52:research/phase-aligned-two-call-prefix/vendor/pr4688/verify.py", + "original_source": { + "commit": "264c4b3cb13c82d171de352ecf60486dfb8d2bd4", + "path": "research/complex-two-image-hook-prefix/verify.py", + "git_blob": "8d2815a2806894bcc50fb34e854f4ef7632ea588" + } + }, + { + "path": "research/phase-aligned-two-call-prefix/vendor/pr4688/README.md", + "usage": "input", + "git_blob": "ac33ab36287fe1f1d9ba51b5360f44536c2ff3fc", + "sha256": "91d45b5af6063e30c6860a4cb46cfc44960ecd67f37c3bce9675924e30b89b4e", + "pin": "head:03e78a0a562f5099d0fffdfc4d6768875052bd52:research/phase-aligned-two-call-prefix/vendor/pr4688/README.md", + "original_source": { + "commit": "264c4b3cb13c82d171de352ecf60486dfb8d2bd4", + "path": "research/complex-two-image-hook-prefix/README.md", + "git_blob": "ac33ab36287fe1f1d9ba51b5360f44536c2ff3fc" + } + } + ] +} diff --git a/research/phase-aligned-two-call-prefix/TASK.json b/research/phase-aligned-two-call-prefix/TASK.json new file mode 100644 index 0000000000..3ff6c6e6ce --- /dev/null +++ b/research/phase-aligned-two-call-prefix/TASK.json @@ -0,0 +1,99 @@ +{ + "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": "Construct a phase-repaired two-call block-3 prefix with exact target alignment on eight hook cuts and every natural higher-width lift; prove the fresh-input obstruction for the predecessor prefix.", + "scope_change_reason": "The donor requested sustained mechanism exploration for a materially larger bound. We follow the current open small-unit attainment question in PR4688/PR4628, changing phase letters and checking a missing target-alignment condition rather than repricing the selected fixed word.", + "bottleneck_link": "A completed five-array fourteen-call block-3 unit would change the complex supplier mechanism substantially. This contribution supplies an exact necessary-condition repair and residual interface, but does not complete that unit or price a new outer exponent.", + "budget_minutes": 180, + "stop_rule": "Package one exact independently reviewable prefix result after target-deficit proof review, all-width analysis and bounded exact replay; leave multi-input completion explicitly open.", + "outcome": "completed", + "evidence": "Exact Gaussian-integer rank elimination, four-point pencil checks, an analytic all-width inverse and lifted-hook proof, and independent Gaussian-rational residual identities. No new kappa.", + "author": "Yiyang (@Lyy-iiis)", + "ai_assistance": "Substantial OpenAI Codex assistance, including parallel research and independent agent review. No independent human or Lean review.", + "open_questions": [ + { + "question": "Can the repaired prefix be completed to five independent block-3 transforms in fourteen calls?", + "why_it_matters": "That would provide a substantially different complex supplier, whereas a saturated prefix alone gives no saving.", + "first_step": "Use the verified residual identity and the four free Pauli sectors to cancel contamination across independent inputs, checking a literal all-width program.", + "blocked_by": "No complete multi-input continuation, restored scratch contract or positive complete invoice has been constructed." + }, + { + "question": "Does another higher-width invariant obstruct this repaired prefix?", + "why_it_matters": "Passing the eight natural lifted hooks is a necessary condition, not all output or representation constraints.", + "first_step": "Test the independent width-six symmetric-sector end conditions on the two phase-repaired branches.", + "blocked_by": "The present all-width proof covers H tensor V^r lifted hooks, not every invariant subspace." + } + ], + "predecessors": [ + { + "pr": 4688, + "head": "264c4b3cb13c82d171de352ecf60486dfb8d2bd4", + "credit": "lee-phys: two-image prefix, all-width inverse method, unchanged exact rank engine and controls." + }, + { + "pr": 4628, + "head": "ee4fd87f064017c23e5a86fc1dcfe0a5237caed3", + "credit": "Jacob Sussman: small-unit model, hook lower bound and attainment question." + } + ], + "overlap": { + "report": "OVERLAP.json", + "open_pr_records": 473, + "complete_open_pr_pagination": true, + "complete_discussion_history": false, + "discussion_records_checked": 210, + "local_note_coverage": "sparse; not a novelty certificate" + }, + "coordination_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19128894" +} diff --git a/research/phase-aligned-two-call-prefix/VALIDATION.json b/research/phase-aligned-two-call-prefix/VALIDATION.json new file mode 100644 index 0000000000..5fa6a49f5d --- /dev/null +++ b/research/phase-aligned-two-call-prefix/VALIDATION.json @@ -0,0 +1,45 @@ +{ + "scoped_result": "Phase-repaired prefix and necessary continuation condition; no new exponent", + "checks": [ + { + "command": "python3 scripts/research_package.py --package research/phase-aligned-two-call-prefix --check-only", + "result": "PASS_PACKAGE_METADATA_AND_PINS" + }, + { + "command": "python3.14 -I -B research/phase-aligned-two-call-prefix/verify.py --check research/phase-aligned-two-call-prefix/RESULT.json", + "result": "PASS_PHASE_PREFIX_TARGET_ALIGNMENT" + }, + { + "command": "python3.14 -O -B verify.py --check RESULT.json", + "result": "PASS_PHASE_PREFIX_TARGET_ALIGNMENT (independent construction directory)" + }, + { + "command": "python3.12 scripts/research_package.py --package research/phase-aligned-two-call-prefix", + "result": "PASS_REGISTERED_RESEARCH_PACKAGE" + }, + { + "command": "python3 scripts/check_research_commit.py --package research/phase-aligned-two-call-prefix", + "result": "PASS_RESEARCH_COMMIT_BYTES, all14 files at scientific commit" + }, + { + "command": "python3 scripts/export_research_package.py export ...; check ...", + "result": "PASS_RESEARCH_EXPORT, all14 files at scientific commit", + "archive_sha256": "373797e88ffc3d67e3d516175b78a07306d9419e89b23e1db1f46879391204ec" + } + ], + "python312": "CPython 3.12.15, aarch64-apple-darwin; authenticated official python-build-standalone release 20261021", + "python312_archive_sha256": "a18cc33862b53bd54a148c710def5375c1b47470cccedf817a19c2d211764584", + "independent_agent_mathematical_review": "REVIEW.md", + "unrun": [ + "No selected cold replay (selected construction unchanged).", + "No Lean or full compiler/outer theorem audit.", + "No independent human verification.", + "Optional --check-source-history preflight requires a full Git history and declined this shallow checkout. Original predecessor blob equality and all committed package bytes were checked separately." + ], + "scientific_commit": "e7988a43f523690c279232845ab2bfeabb5df10b", + "hosted_ci": { + "initial_head": "66dee75557a6685f550476eb413d59d23a39d1f2", + "run": "https://github.com/CrocSwap/integer-mult-bounds/actions/runs/39822323568", + "result": "Initial Ubuntu replay hit the 240-second manifest timeout after predecessor controls and six of eight new cuts passed. No mathematical assertion failed. Timeout raised to the repository maximum 600 seconds for the same unchanged exact verification; rerun pending." + } +} diff --git a/research/phase-aligned-two-call-prefix/VERIFY.json b/research/phase-aligned-two-call-prefix/VERIFY.json new file mode 100644 index 0000000000..6bea8154d0 --- /dev/null +++ b/research/phase-aligned-two-call-prefix/VERIFY.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/phase-aligned-two-call-prefix/vendor/pr4688/README.md", + "research/phase-aligned-two-call-prefix/vendor/pr4688/verify.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py", + "--check", + "{package}/RESULT.json" + ], + "timeout_seconds": 600, + "checks": "Exact target-alignment ranks, predecessor calibrations, all-width inverse, four-point pencils, residual/projector identities and failure controls." + } + ] +} diff --git a/research/phase-aligned-two-call-prefix/vendor/pr4688/README.md b/research/phase-aligned-two-call-prefix/vendor/pr4688/README.md new file mode 100644 index 0000000000..ac33ab3628 --- /dev/null +++ b/research/phase-aligned-two-call-prefix/vendor/pr4688/README.md @@ -0,0 +1,257 @@ +# An invertible two-call prefix attaining eight block-3 hook bounds + +**Result.** Two calls on one input can each gain the full 80 in eight +width-five coordinate certificates, using one zero scratch register and a +sum of two free address permutations between the calls. The scratch can be +cleared, and the resulting operator is invertible at **every** positive digit +width. Each of the two summands used alone gives a second gain of only 72. + +This is a scoped mathematical construction and an exact computational proof +of its ranks. It makes the single-free-image obstruction in Jacob Sussman's +[#4628](https://github.com/CrocSwap/integer-mult-bounds/pull/4628) sharp with +respect to allowing two images, in this explicit example. It does **not** +construct five transforms in fourteen calls, improve the call lower bound, +or supply a new multiplication exponent. No Lean or human review is claimed. + +## 1. Was the proposed small-unit problem already solved? + +At the research checkpoint of 22 October 2026, canonical main was +`b58ad9ef4d4e861b0eaa5dba41742bdc072dca51`. PR #4628 remained open at +`ee4fd87f064017c23e5a86fc1dcfe0a5237caed3`; its source repository still had +head `86e575e28ed94890872dcff1bb2621d7ff559cbd`. Both list block 3, +five arrays in fourteen calls, as open in the engine game. The subsequent +[#4643](https://github.com/CrocSwap/integer-mult-bounds/pull/4643) audits the +projection bound at blocks at least 4; it does not settle this case. + +The overlap helper refreshed all pages of 445 open PR bodies and 3,589 +discussion records (snapshot times 15:29 and 15:31 UTC). Targeted PR search +also included closed results. No resolution or competing claim for this +prefix question was found. The sparse checkout searched only 36 of 5,860 +tracked package-note paths; neither this search nor the predecessor's open +label proves global novelty. Exact source links are in section 6. + +## 2. Model and explicit program + +Addresses are triples $x=(x_0,x_1,x_2)\in\mathbb F_2^3$, encoded as +$x_0+2x_1+4x_2$. Let $\mathcal V=\mathbb C^8$. A paid call is + +$$ +C=C_{e_0}=aI+bX_{e_0},\qquad +a=(1+i)/2,\quad b=(1-i)/2, +$$ + +where $X_v e_x=e_{x+v}$. At digit width $f$, write +$C_f=C^{\otimes f}$. The engine permits free invertible binary address +maps on an array, applied identically in each column, and rational linear +mixing of registers, including copies and erasures. + +Use just these two address permutations: + +$$ +Ue_{(x_0,x_1,x_2)}=e_{(x_0,x_1,x_2+x_0)},\qquad +Ve_{(x_0,x_1,x_2)}=e_{(x_1,x_0,x_2)}. +$$ + +In address order $0,\ldots,7$, their images are respectively +`[0,5,2,7,4,1,6,3]` and `[0,2,1,3,4,6,5,7]`. +Write $U_f=U^{\otimes f}$, $V_f=V^{\otimes f}$. +The prefix returns + +$$ +F_{2,f}y=C_f(U_f+2V_f)C_fy. \tag{1} +$$ + +An actual two-register implementation, starting from $(r_0,r_1)=(y,0)$, is: + +1. $r_0\leftarrow C_f r_0$. **One paid call.** +2. $r_1\leftarrow r_0$; $r_1\leftarrow U_f r_1$. +3. $r_0\leftarrow V_f r_0$; $r_1\leftarrow r_1+2r_0$. +4. $r_0\leftarrow V_f r_0$, restoring $u=C_fy$, since $V^2=I$. +5. $r_1\leftarrow C_f r_1$. **One paid call.** The state is $(u,F_{2,f}y)$. +6. Apply the free mixing matrix $\left(\begin{smallmatrix}0&1\\0&0\end{smallmatrix}\right)$, + returning $(F_{2,f}y,0)$. + +This uses two rank-one calls, one initially zero scratch register, integer +mixing coefficients, and no phase letters. No input copy outside these two +registers is assumed. In particular, the sum in (1) is implemented by mixing; +it is **not** $(U+2V)^{\otimes f}$. + +## 3. Invertibility at every width + +Both $U$ and $V$ are involutions. Put $R=U^{-1}V=UV$. +As an address permutation, + +$$ +R=(0)(4)(1\ 2\ 5\ 6)(3\ 7),\qquad R^4=I. +$$ + +Consequently $R_f=R^{\otimes f}$ also satisfies $R_f^4=I$, and + +$$ +(I+2R_f)(I-2R_f+4R_f^2-8R_f^3)=-15I. +$$ + +Since $U_f+2V_f=U_f(I+2R_f)$, this supplies an explicit inverse using +fixed rational coefficients, for every $f$. The two factors $C_f$ are +invertible as well. Thus (1) is invertible at every width, and clearing +$u$ in step 6 loses no input information. This is an analytic all-width +proof; it does not infer uniform correctness from the width-five experiment. + +## 4. Exact simultaneous equality in eight cuts + +At width five restrict to the invariant subspace +$H=\mathcal V\otimes\Lambda^4\mathcal V$, of dimension $8\binom84=560$. +For a single-column matrix $g$, its action is +$\rho(g)=g\otimes\Lambda^4g$, with entries + +$$ +\rho(g)_{(y,S),(x,T)}=g_{yx}\det(g_{S,T}). \tag{2} +$$ + +Split the coordinate basis $e_x\otimes e_T$ into four classes: + +| Class | Condition | Size | +|---|---|---:| +| $O_0$ | $x\in T$, $\bigoplus_{t\in T}t=0$ | 56 | +| $O_1$ | $x\in T$, $\bigoplus_{t\in T}t\ne0$ | 224 | +| $O_2$ | $x\notin T$, $\bigoplus_{t\in T}t=0$ | 56 | +| $O_3$ | $x\notin T$, $\bigoplus_{t\in T}t\ne0$ | 224 | + +The zero-XOR four-subsets are affine planes. For a mask $b$, let $N_b$ +span the classes selected by its four binary digits. Every affine address +map preserves membership and zero XOR (four copies of a translation cancel). +Every diagonal phase preserves each coordinate line. Hence every $N_b$ +below is kept by the engine's free letters. In particular $N_3$ is the +usual hook, and $N_8$ is the published single-term certificate $O_c$. + +Let $q_b:H\to H/N_b$. For a state with one input and output maps +$A_1,\ldots,A_r$, its potential is + +$$ +\Phi_b(A_1,\ldots,A_r) +=\operatorname{rank}\begin{bmatrix} +q_bA_1|_{N_b}\\ \vdots\\ q_bA_r|_{N_b} +\end{bmatrix}. +$$ + +Put $D=\rho(C)$, $A=D\rho(U)D$, $B=D\rho(V)D$, and +$K=\rho(C_{e_2}C_{e_1}C_{e_0})$. Here $A+2B$ is the restriction +of the actual output family (1) to $H$; no tensor lift of a sum is taken. +The complete exact calculation is: + +| Mask $b$ | $\dim N_b$ | $\Phi_b(D)$ | $\Phi_b(D,A)$ | $\Phi_b(D,B)$ | $\Phi_b(D,A+2B)$ | $\Phi_b(A+2B)$ | $\Phi_b(K)$ | +|---:|---:|---:|---:|---:|---:|---:|---:| +| 2 | 224 | 80 | 152 | 152 | 160 | 160 | 224 | +| 3 | 280 | 80 | 152 | 152 | 160 | 160 | 224 | +| 6 | 280 | 80 | 152 | 152 | 160 | 160 | 224 | +| 7 | 336 | 80 | 152 | 152 | 160 | 160 | 224 | +| 8 | 224 | 80 | 152 | 152 | 160 | 160 | 224 | +| 9 | 280 | 80 | 152 | 152 | 160 | 160 | 224 | +| 12 | 280 | 80 | 152 | 152 | 160 | 160 | 224 | +| 13 | 336 | 80 | 152 | 152 | 160 | 160 | 224 | + +The rank 80 is the cap for **every** direction: a binary invertible address +map sends $e_0$ to any nonzero direction and preserves $N_b$. +The kept-subspace argument of #4628 therefore bounds the increase from one +call by 80, even with scratch and singular mixing. These caps and demands +reproduce the known bound $80s\ge224W$, or $s\ge14W/5$. +They are calibration results, not new lower bounds. + +For our prefix the first increase is 80 and the second is +$160-80=80$, simultaneously for every listed cut. The free steps in +between retain $u$ up to an invertible free image and hence preserve its +potential. The joint-state and final-state columns show that the erasure also +preserves all eight potentials. With either branch alone the second +increase is only $152-80=72$. + +**What is new.** A second call can be fully productive on all these cuts +without receiving a fresh independent input: two free images of the same +earlier output suffice, and the combined map can remain uniformly invertible. +Thus the published obstruction for a *single* free image cannot be used as +a pruning rule for arbitrary free linear combinations of that output. +This does not dispute the predecessor's deliberately narrower statement. + +## 5. A singular control that the eight cuts do not distinguish + +Replacing coefficient 2 by 1 gives $F_{1,f}=C_f(U_f+V_f)C_f$. +The checker also obtains $\Phi_b(F_{1,5}|_H)=160$ for every listed cut. +Nevertheless this family is singular. Indeed its nullity is the multiplicity +of eigenvalue $-1$ in $R_f$. The projection onto that eigenspace is +$(I-R_f+R_f^2-R_f^3)/4$. Since the numbers of fixed addresses of +$R^0,R^1,R^2,R^3$ are $8,2,4,2$, tensor traces give exactly + +$$ +\dim\ker F_{1,f}=\frac{8^f+4^f-2\cdot2^f}{4}>0\quad(f\ge1). +$$ + +It is 2 at width one and 8,432 at width five. Erasing the retained first +output in this variant therefore destroys information while preserving all +eight potentials. This is a concrete check that equality in these +certificates does not itself certify injectivity or completion. Coefficient +2 avoids this defect by the explicit inverse in section 3. + +## 6. Reproduction, status, and credit + +```sh +python3.12 -B research/complex-two-image-hook-prefix/verify.py +python3.12 -O -B research/complex-two-image-hook-prefix/verify.py +python3.12 -B scripts/research_package.py --package research/complex-two-image-hook-prefix +``` + +The verifier uses the standard library and computes ranks exactly over +$\mathbb Q(i)$, with Gaussian-integer elimination and exact common-divisor +removal. The ranks over $\mathbb C$ are the same. It replaces $C$ by +$I-iX_{e_0}$, removing a nonzero scalar: each affected block of a rank +matrix is rescaled uniformly, so no rank changes. It expands exterior +products directly, checks all 313,600 entries of the first call against the +independent minor formula (2), and checks its square against +$\rho(I-iX)^2=-32i\rho(X)$. + +Seven controls cover deletion of either summand, duplication of a summand, +replacement of the second permutation by the identity, an incorrect cap of +79, the wrong tensor lift of a sum, and the singular coefficient-1 variant. +Independent cycle enumeration at widths 1, 2, 3 checks the nullity formula. +Exploration used NumPy/modular ranks; **none of those exploratory calculations +or external libraries is an input to the registered proof computation**. +No Lean build, all-history replay, or full integer-multiplication verification +is claimed or needed for this scope. + +`SOURCES.json` pins the originating catalogue and selected record in this +branch's base history. The pending predecessor's exact URLs and document +hashes are bibliographic references in this note and `TASK.json`; replay +does not require fetching an unrelated PR's Git objects. + +Predecessor credit: + +- Jacob Sussman, [#4628 README](https://github.com/jacobalansussman/integer-mult-bounds/blob/ee4fd87f064017c23e5a86fc1dcfe0a5237caed3/research/complex-small-m-lower-bounds/README.md) + and [PROOF.md](https://github.com/jacobalansussman/integer-mult-bounds/blob/ee4fd87f064017c23e5a86fc1dcfe0a5237caed3/research/complex-small-m-lower-bounds/PROOF.md): + model, kept-subspace argument, 14/5 bound, and open shapes. +- Sussman's [single-term gain package](https://github.com/jacobalansussman/wht-power-saving-lean/tree/86e575e28ed94890872dcff1bb2621d7ff559cbd/research/block-bounds-and-new-rules/programs/five-in-fourteen-block3) + and [block-bounds README, section 3.5](https://github.com/jacobalansussman/wht-power-saving-lean/blob/86e575e28ed94890872dcff1bb2621d7ff559cbd/research/block-bounds-and-new-rules/README.md): + the single-image cap 72, eight tight-certificate context, and the warning + that a width-five candidate can fail at width six. This package independently + derives and checks its explicit example; it does not import those programs + or recheck the predecessor's classification of every single-image class. +- eumemic's [#288](https://github.com/CrocSwap/integer-mult-bounds/pull/288) + for the underlying certificate method; Swapnil Jain's P1/P2 as credited by + #4628; OpenAI for the engine's call and free-operation model. + +Prepared for lee-phys with substantial OpenAI Codex assistance in the +derivation, search, code, and writing. No independent human review. +Apache-2.0. No predecessor package or selected-result record is modified. + +## Open next questions + +1. **Can a full 5-in-14 program use this prefix?** It may start with two + saturated calls on one input, but the remaining schedule must deliver all + five independent targets at every width. First test the prefix's allowed + continuations against the per-array end conditions at width six; do not + accept a candidate from this rank table alone. No continuation is supplied. +2. **Which additional invariant distinguishes the singular and invertible + variants while retaining useful call bounds?** Their eight potentials + agree despite different kernels. Start from the explicit order-four + eigenspace in section 5 and track where that information resides under + shared-register mixing. A global lower bound requires a new argument. + +The structured questions and the explicit change from the task card's +selected-supplier scope are recorded in `TASK.json`. diff --git a/research/phase-aligned-two-call-prefix/vendor/pr4688/verify.py b/research/phase-aligned-two-call-prefix/vendor/pr4688/verify.py new file mode 100644 index 0000000000..8d2815a280 --- /dev/null +++ b/research/phase-aligned-two-call-prefix/vendor/pr4688/verify.py @@ -0,0 +1,313 @@ +#!/usr/bin/env python3 +"""Exact Gaussian-integer ranks for a two-image block-3 prefix. + +Standard library only; no input files, floating point, assertions, or outputs +other than the report. See README.md for the mathematical scope. +""" + +from itertools import combinations, permutations, product + + +ZERO, ONE, MINUS_I = (0, 0), (1, 0), (0, -1) +I_POWERS = (ONE, (0, 1), (-1, 0), MINUS_I) +SUBSETS = tuple(combinations(range(8), 4)) +BASIS = tuple((x, subset) for x in range(8) for subset in SUBSETS) +INDEX = {label: index for index, label in enumerate(BASIS)} +CUTS = (2, 3, 6, 7, 8, 9, 12, 13) +U_PERM = tuple(x ^ ((x & 1) << 2) for x in range(8)) +V_PERM = tuple(x ^ (((x ^ (x >> 1)) & 1) * 3) for x in range(8)) + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def add(a, b): + return a[0] + b[0], a[1] + b[1] + + +def sub(a, b): + return a[0] - b[0], a[1] - b[1] + + +def mul(a, b): + return a[0] * b[0] - a[1] * b[1], a[0] * b[1] + a[1] * b[0] + + +def gaussian_divide(a, b): + denominator = b[0] ** 2 + b[1] ** 2 + require(denominator != 0, "division by zero") + real = a[0] * b[0] + a[1] * b[1] + imag = a[1] * b[0] - a[0] * b[1] + require(real % denominator == imag % denominator == 0, + "Gaussian division is not exact") + return real // denominator, imag // denominator + + +def gaussian_gcd(a, b): + """Euclidean gcd, up to a unit, using nearest integer quotients.""" + while b != ZERO: + denominator = b[0] ** 2 + b[1] ** 2 + quotient = ( + (a[0] * b[0] + a[1] * b[1] + denominator // 2) // denominator, + (a[1] * b[0] - a[0] * b[1] + denominator // 2) // denominator, + ) + a, b = b, sub(a, mul(quotient, b)) + return a + + +def accumulate(vector, index, coefficient): + value = add(vector.get(index, ZERO), coefficient) + if value == ZERO: + vector.pop(index, None) + else: + vector[index] = value + + +def wedge_sign(addresses): + if len(set(addresses)) != len(addresses): + return 0 + inversions = sum(addresses[i] > addresses[j] + for i in range(len(addresses)) + for j in range(i + 1, len(addresses))) + return -1 if inversions % 2 else 1 + + +def lift_direction(direction): + """Columns of rho(I - i X_direction) on V tensor exterior^4 V.""" + require(1 <= direction < 8, "direction must be nonzero") + columns = [] + for x, subset in BASIS: + column = {} + for choices in product((0, 1), repeat=5): + images = tuple(t ^ (direction if choice else 0) + for t, choice in zip(subset, choices[1:])) + sign = wedge_sign(images) + if not sign: + continue + phase = I_POWERS[-sum(choices) % 4] + row = INDEX[x ^ (direction if choices[0] else 0), tuple(sorted(images))] + accumulate(column, row, (sign * phase[0], sign * phase[1])) + columns.append(column) + return columns + + +def apply_permutation(permutation, columns): + """Apply rho(P), retaining the sign from sorting each exterior basis.""" + require(sorted(permutation) == list(range(8)), "not a permutation") + action = [] + for x, subset in BASIS: + images = tuple(permutation[t] for t in subset) + action.append((INDEX[permutation[x], tuple(sorted(images))], wedge_sign(images))) + return [{action[j][0]: (action[j][1] * value[0], action[j][1] * value[1]) + for j, value in column.items()} for column in columns] + + +def compose(left, right): + columns = [] + for column in right: + result = {} + for j, coefficient in column.items(): + for i, value in left[j].items(): + accumulate(result, i, mul(value, coefficient)) + columns.append(result) + return columns + + +def add_columns(left, right): + columns = [] + for a, b in zip(left, right): + result = a.copy() + for i, value in b.items(): + accumulate(result, i, value) + columns.append(result) + return columns + + +def scale_columns(columns, scalar): + return [{j: mul((scalar, 0), value) for j, value in column.items()} + for column in columns] + + +def orbit_number(x, subset): + nonplane = int(bool(subset[0] ^ subset[1] ^ subset[2] ^ subset[3])) + return 2 * int(x not in subset) + nonplane + + +def cut_indices(mask): + return tuple(i for i, label in enumerate(BASIS) + if mask & (1 << orbit_number(*label))) + + +def project(columns, indices): + """Rows of the map N -> H/N, in coordinate bases.""" + inside = set(indices) + rows = {i: {} for i in range(len(BASIS)) if i not in inside} + for column_index, j in enumerate(indices): + for i, value in columns[j].items(): + if i in rows: + rows[i][column_index] = value + return list(rows.values()) + + +def rank_exact(rows): + """Rank over Q(i), using span-preserving operations in Z[i]. + + Multiply a row by a nonzero pivot, subtract a pivot-row multiple, and + divide by a nonzero common Gaussian divisor. Content removal keeps the + coefficients small. This computes exact rank, not a modular lower bound. + """ + pivots = {} + for source in rows: + row = source.copy() + while row: + column = min(row) + if column not in pivots: + pivots[column] = row + break + pivot = pivots[column] + a, b = row[column], pivot[column] + row = {j: mul(b, value) for j, value in row.items()} + for j, value in pivot.items(): + coefficient = mul(a, value) + accumulate(row, j, (-coefficient[0], -coefficient[1])) + if row: + common = ZERO + for value in row.values(): + common = gaussian_gcd(common, value) + if common[0] ** 2 + common[1] ** 2 == 1: + break + if common[0] ** 2 + common[1] ** 2 > 1: + row = {j: gaussian_divide(value, common) for j, value in row.items()} + return len(pivots) + + +def check_lift(direction): + """Check every entry against a separate determinant definition.""" + matrix = [[ZERO for _ in range(8)] for _ in range(8)] + for x in range(8): + matrix[x][x] = ONE + matrix[x ^ 1][x] = MINUS_I + orders = tuple((order, wedge_sign(order)) for order in permutations(range(4))) + minors = {} + for rows in SUBSETS: + for cols in SUBSETS: + total = ZERO + for order, sign in orders: + term = (sign, 0) + for i in range(4): + term = mul(term, matrix[rows[i]][cols[order[i]]]) + total = add(total, term) + minors[rows, cols] = total + for j, (x, cols) in enumerate(BASIS): + for i, (y, rows) in enumerate(BASIS): + expected = mul(matrix[y][x], minors[rows, cols]) + require(direction[j].get(i, ZERO) == expected, "exterior lift disagrees with minor") + + +def reject_rank(rows, incorrect, label): + observed = rank_exact(rows) + require(observed != incorrect, "negative control was accepted: " + label) + + +def main(): + require(tuple(sum(orbit_number(*label) == j for label in BASIS) for j in range(4)) + == (56, 224, 56, 224), "coordinate class sizes changed") + direction = lift_direction(1) + check_lift(direction) + identity = [{j: ONE} for j in range(len(BASIS))] + shift = apply_permutation(tuple(x ^ 1 for x in range(8)), identity) + expected_square = [{i: mul((0, -32), value) for i, value in column.items()} + for column in shift] + require(compose(direction, direction) == expected_square, + "rho(I-iX)^2 must equal -32i rho(X)") + first_branch = compose(direction, apply_permutation(U_PERM, direction)) + second_branch = compose(direction, apply_permutation(V_PERM, direction)) + combined = add_columns(first_branch, scale_columns(second_branch, 2)) + singular_variant = add_columns(first_branch, second_branch) + target = compose(lift_direction(4), compose(lift_direction(2), direction)) + + print("mask dim first U-only V-only joint final lambda=1-final target", flush=True) + for mask in CUTS: + indices = cut_indices(mask) + first = project(direction, indices) + values = (rank_exact(first), + rank_exact(first + project(first_branch, indices)), + rank_exact(first + project(second_branch, indices)), + rank_exact(first + project(combined, indices)), + rank_exact(project(combined, indices)), + rank_exact(project(singular_variant, indices)), + rank_exact(project(target, indices))) + require(values == (80, 152, 152, 160, 160, 160, 224), + "rank profile failed for cut " + str(mask)) + print(mask, len(indices), *values, flush=True) + + indices = cut_indices(2) + first = project(direction, indices) + reject_rank(first + project(first_branch, indices), 160, "delete V branch") + reject_rank(first + project(second_branch, indices), 160, "delete U branch") + reject_rank(first + project(add_columns(first_branch, first_branch), indices), + 160, "duplicate U branch") + square = compose(direction, direction) + reject_rank(first + project(add_columns(first_branch, square), indices), + 160, "replace V by identity") + reject_rank(first, 79, "undercount first call") + + # R = U^{-1} V has cycles of lengths 1, 1, 2, 4. Its fourth power is I. + require(all(U_PERM[U_PERM[x]] == V_PERM[V_PERM[x]] == x for x in range(8)), + "U and V must be involutions") + ratio = tuple(U_PERM[V_PERM[x]] for x in range(8)) + remaining, lengths = set(range(8)), [] + while remaining: + start = min(remaining) + cycle, x = [], start + while x not in cycle: + cycle.append(x) + remaining.remove(x) + x = ratio[x] + require(x == start, "invalid permutation cycle") + lengths.append(len(cycle)) + require(sorted(lengths) == [1, 1, 2, 4], "ratio cycle type changed") + + # Polynomial identity (I+2R)(I-2R+4R^2-8R^3) = -15I for R^4=I. + polynomial = [0] * 4 + for i, a in enumerate((1, 2)): + for j, b in enumerate((1, -2, 4, -8)): + polynomial[(i + j) % 4] += a * b + require(polynomial == [-15, 0, 0, 0], "uniform inverse identity failed") + + # Independent cycle enumeration at widths 1, 2, 3 checks the all-width + # nullity formula of the lambda=1 negative control. + for width in (1, 2, 3): + remaining = set(product(range(8), repeat=width)) + even_cycles = 0 + while remaining: + start = min(remaining) + x, length = start, 0 + while True: + remaining.remove(x) + length += 1 + x = tuple(ratio[t] for t in x) + if x == start: + break + even_cycles += int(length % 2 == 0) + require(even_cycles == (8 ** width + 4 ** width - 2 * 2 ** width) // 4, + "singular-variant nullity formula failed") + require(even_cycles > 0, "lambda=1 incorrectly accepted as invertible") + + # Mixing acts outside the tensor lift: on e_1 tensor e_1, the incorrect + # (U+V) tensor (U+V) has the cross term e_5 tensor e_2; the true sum does not. + tensor_sum, sum_tensor = {}, {} + for permutation in (U_PERM, V_PERM): + accumulate(tensor_sum, (permutation[1], permutation[1]), ONE) + for p, q in product((U_PERM, V_PERM), repeat=2): + accumulate(sum_tensor, (p[1], q[1]), ONE) + require(tensor_sum.get((5, 2), ZERO) == ZERO + and sum_tensor[(5, 2)] == ONE, "width-two lift control failed") + print("PASS_CONTROLS 7", flush=True) + print("PASS_COMPLEX_TWO_IMAGE_HOOK_PREFIX", flush=True) + + +if __name__ == "__main__": + main() diff --git a/research/phase-aligned-two-call-prefix/verify.py b/research/phase-aligned-two-call-prefix/verify.py new file mode 100644 index 0000000000..1d81448d5f --- /dev/null +++ b/research/phase-aligned-two-call-prefix/verify.py @@ -0,0 +1,178 @@ +#!/usr/bin/env python3 +"""Exact target alignment and a phase-corrected two-call prefix. Standard library only.""" +from __future__ import annotations +import argparse +import hashlib +import types +import json +from pathlib import Path +import sys +sys.dont_write_bytecode = True +ROOT = Path(__file__).resolve().parent +PINS = { + 'vendor/pr4688/verify.py': '99ff0beccd9a4e94cc607e02114d62b8ce0ea57ee00748b07ce0a0af91aec85e', + 'vendor/pr4688/README.md': '91d45b5af6063e30c6860a4cb46cfc44960ecd67f37c3bce9675924e30b89b4e', +} + +def require(ok, message): + if not ok: + raise ValueError(message) + +def load_engine(): + authenticated = {} + for path, digest in PINS.items(): + payload = (ROOT / path).read_bytes() + require(hashlib.sha256(payload).hexdigest() == digest, + 'changed immutable predecessor: ' + path) + authenticated[path] = payload + path = ROOT / 'vendor/pr4688/verify.py' + module = types.ModuleType('pinned_pr4688') + module.__file__ = str(path) + # Compile the exact authenticated bytes; never consult an existing .pyc. + exec(compile(authenticated['vendor/pr4688/verify.py'], str(path), 'exec'), module.__dict__) + return module + +def monomial_compose(a, b): + return (tuple(a[0][b[0][x]] for x in range(8)), + tuple((b[1][x] + a[1][b[0][x]]) % 4 for x in range(8))) + +def monomial_inverse(a): + p = tuple(a[0].index(x) for x in range(8)) + return p, tuple(-a[1][p[x]] % 4 for x in range(8)) + +def monomial_checks(m): + identity = (tuple(range(8)), (0,) * 8) + phase = (identity[0], tuple(x.bit_count() % 4 for x in range(8))) + u, v = (tuple(m.U_PERM), identity[1]), (tuple(m.V_PERM), identity[1]) + P = monomial_compose(phase, monomial_compose(u, phase)) + Q = monomial_compose(phase, monomial_compose(v, phase)) + ratio = monomial_compose(monomial_inverse(P), Q) + power = identity + powers = [] + for k in range(4): + powers.append(power) + power = monomial_compose(ratio, power) + require(power == identity and all(x != identity for x in powers[1:]), 'ratio order is not four') + # The ratio equals S^{-1} U^{-1} V S as an actual monomial, not merely projectively. + conjugate = monomial_compose(monomial_inverse(phase), + monomial_compose(monomial_inverse(u), monomial_compose(v, phase))) + require(ratio == conjugate, 'ratio conjugacy') + traces = [] + for p, e in powers: + trace = (0, 0) + for x in range(8): + if p[x] == x: + trace = m.add(trace, m.I_POWERS[e[x]]) + traces.append(trace) + require(traces == [(8, 0), (2, 0), (4, 0), (2, 0)], 'ratio traces') + # Exact polynomial multiplication, reduced using R^4 = I. + product = [0] * 4 + for degree, coefficient in enumerate((1, -2, 4, -8)): + product[degree] += coefficient + product[(degree + 1) % 4] += 2 * coefficient + require(product == [-15, 0, 0, 0], 'all-width inverse polynomial') + bad_phases = list(ratio[1]) + bad_phases[1] = (bad_phases[1] + 1) % 4 + bad_ratio = (ratio[0], tuple(bad_phases)) + bad_power = identity + for _ in range(4): + bad_power = monomial_compose(bad_ratio, bad_power) + require(bad_power != identity, 'wrong monomial phase must fail fourth-power check') + return {'P': {'permutation': P[0], 'phase_exponents_mod4': P[1]}, + 'Q': {'permutation': Q[0], 'phase_exponents_mod4': Q[1]}, + 'R': {'permutation': ratio[0], 'phase_exponents_mod4': ratio[1]}, + 'R_order': 4, 'traces_R_powers': traces, + 'eigenvalue_multiplicities_1_minus1_i_minusi': [4, 2, 1, 1], + 'inverse_polynomial_product': product, + 'negative_control': 'one changed R phase fails R^4=I'} + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--out', type=Path, help='write the deterministic exact report') + parser.add_argument('--check', type=Path, help='require exact equality with a stored JSON report') + args = parser.parse_args() + m = load_engine() + # Unchanged predecessor replay includes independent exterior-minor calibration, + # the paid-call cap and target ranks, and its seven negative controls. + m.main() + D = m.lift_direction(1) + K = m.compose(m.lift_direction(4), m.compose(m.lift_direction(2), D)) + phases = [m.I_POWERS[(x.bit_count() + sum(t.bit_count() for t in subset)) % 4] + for x, subset in m.BASIS] + def phase_columns(columns): + return [{i: m.mul(phases[i], value) for i, value in column.items()} for column in columns] + def repaired_branch(permutation): + return m.compose(D, phase_columns(m.apply_permutation(permutation, phase_columns(D)))) + def complex_scale(columns, coefficient): + return [{i: m.mul(coefficient, value) for i, value in column.items()} for column in columns] + old_A = m.compose(D, m.apply_permutation(m.U_PERM, D)) + old_B = m.compose(D, m.apply_permutation(m.V_PERM, D)) + old = m.add_columns(old_A, m.scale_columns(old_B, 2)) + A, B = repaired_branch(m.U_PERM), repaired_branch(m.V_PERM) + new = m.add_columns(A, m.scale_columns(B, 2)) + pencil = [m.add_columns(A, complex_scale(B, coefficient)) + for coefficient in ((2, 0), (-2, 0), (0, 2), (0, -2))] + records = [] + print('mask oldPhi oldJoint newPhi newJoint branchJoints pencilRanks', flush=True) + for mask in m.CUTS: + inside = m.cut_indices(mask) + target = m.project(K, inside) + old_rows, new_rows = m.project(old, inside), m.project(new, inside) + old_phi, new_phi = m.rank_exact(old_rows), m.rank_exact(new_rows) + # Put the structured target rows first to keep Gaussian intermediates small. + old_joint = m.rank_exact(target + old_rows) + new_joint = m.rank_exact(target + new_rows) + branch_joints = [m.rank_exact(target + m.project(branch, inside)) for branch in (A, B)] + pencil_ranks = [m.rank_exact(m.project(value, inside)) for value in pencil] + expected_old_joint = 280 if mask in (3, 6, 7) else 224 + require((old_phi, old_joint, new_phi, new_joint) == (160, expected_old_joint, 160, 224), + 'prefix/target alignment at mask ' + str(mask)) + require(branch_joints == [224, 224], 'termwise all-width alignment at mask ' + str(mask)) + require(pencil_ranks == [160] * 4, 'four-point pencil at mask ' + str(mask)) + record = {'mask': mask, 'N_dimension': len(inside), 'target_rank': 224, + 'old_prefix_rank': old_phi, 'old_target_joint_rank': old_joint, + 'old_missing_target_dimensions': old_joint - old_phi, + 'new_prefix_rank': new_phi, 'new_target_joint_rank': new_joint, + 'new_missing_target_dimensions': new_joint - new_phi, + 'new_single_branch_target_joint_ranks': branch_joints, + 'new_pencil_ranks_coefficients_2_minus2_2i_minus2i': pencil_ranks, + 'width6_lifted_prefix_rank': sum(w*r for w,r in zip((4,2,1,1), pencil_ranks)), + 'width6_lifted_target_and_joint_rank': 8 * 224} + records.append(record) + print(mask, old_phi, old_joint, new_phi, new_joint, branch_joints, pencil_ranks, flush=True) + require(records[1]['old_missing_target_dimensions'] + 4 * 224 == 1016, + 'five-array remaining deficit') + require(1016 > 12 * 80, 'original prefix obstruction') + require(records[1]['new_missing_target_dimensions'] + 4 * 224 == 12 * 80, + 'repaired remaining deficit') + monomials = monomial_checks(m) + residual_path = ROOT / 'verify_residual.py' + residual = types.ModuleType('independent_residual') + residual.__file__ = str(residual_path) + exec(compile(residual_path.read_bytes(), str(residual_path), 'exec'), residual.__dict__) + residual_report = residual.verify() + report = {'schema_version': 1, + 'source_pr': 4688, 'source_head': '264c4b3cb13c82d171de352ecf60486dfb8d2bd4', + 'source_sha256': PINS, + 'scope': 'two-call prefix and necessary continuation conditions; no completed unit or new exponent', + 'arithmetic': 'Gaussian integer elimination over Q(i), no numerical rank tolerance', + 'cuts': records, 'monomial_inverse': monomials, + 'exact_residual_interface': residual_report, + 'all_extra_widths': {'extra_width_variable': 'r >= 0', + 'prefix_rank_each_lifted_cut': '160*8^r', + 'target_and_joint_rank_each_lifted_cut': '224*8^r', + 'proof': 'four eigenvalues of relative branch matrix; four-point pencil ranks and termwise kernel inclusion'}, + 'original_five_array_remaining_deficit': 1016, + 'remaining_twelve_call_capacity': 960, + 'repaired_five_array_remaining_deficit': 960, + 'result': 'PASS'} + # Normalize tuples before comparing the JSON encoding. + report = json.loads(json.dumps(report)) + if args.check: + require(json.loads(args.check.read_text()) == report, 'stored report mismatch') + if args.out: + args.out.write_text(json.dumps(report, indent=2, sort_keys=True) + '\n') + print('PASS_PHASE_PREFIX_TARGET_ALIGNMENT', flush=True) + +if __name__ == '__main__': + main() diff --git a/research/phase-aligned-two-call-prefix/verify_residual.py b/research/phase-aligned-two-call-prefix/verify_residual.py new file mode 100644 index 0000000000..9130ce2171 --- /dev/null +++ b/research/phase-aligned-two-call-prefix/verify_residual.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()