From 97db3fb45cd93a350e300781d75440d14e6a1f73 Mon Sep 17 00:00:00 2001 From: Ali Romman <226877337+aliromman@users.noreply.github.com> Date: Sun, 25 Oct 2026 15:56:16 -0500 Subject: [PATCH] Prove native equality-cut tariffs for active linear words --- research/native-equality-cut/OVERLAP.json | 28 ++ research/native-equality-cut/PROOF.md | 257 ++++++++++++++ research/native-equality-cut/README.md | 152 +++++++++ research/native-equality-cut/RESULT.json | 119 +++++++ research/native-equality-cut/SOURCES.json | 89 +++++ research/native-equality-cut/TASK.json | 107 ++++++ research/native-equality-cut/VERIFY.json | 34 ++ research/native-equality-cut/cuts.py | 91 +++++ .../evidence/p104-result.json | 315 ++++++++++++++++++ research/native-equality-cut/exact.py | 191 +++++++++++ .../examples/delayed-failure.json | 4 + .../examples/equal-mass-trade.json | 4 + .../examples/profitable-delayed-failure.json | 4 + research/native-equality-cut/vendor/LICENSE | 201 +++++++++++ research/native-equality-cut/vendor/NOTICE.md | 8 + research/native-equality-cut/vendor/fields.py | 140 ++++++++ research/native-equality-cut/verify.py | 235 +++++++++++++ 17 files changed, 1979 insertions(+) create mode 100644 research/native-equality-cut/OVERLAP.json create mode 100644 research/native-equality-cut/PROOF.md create mode 100644 research/native-equality-cut/README.md create mode 100644 research/native-equality-cut/RESULT.json create mode 100644 research/native-equality-cut/SOURCES.json create mode 100644 research/native-equality-cut/TASK.json create mode 100644 research/native-equality-cut/VERIFY.json create mode 100644 research/native-equality-cut/cuts.py create mode 100644 research/native-equality-cut/evidence/p104-result.json create mode 100644 research/native-equality-cut/exact.py create mode 100644 research/native-equality-cut/examples/delayed-failure.json create mode 100644 research/native-equality-cut/examples/equal-mass-trade.json create mode 100644 research/native-equality-cut/examples/profitable-delayed-failure.json create mode 100644 research/native-equality-cut/vendor/LICENSE create mode 100644 research/native-equality-cut/vendor/NOTICE.md create mode 100644 research/native-equality-cut/vendor/fields.py create mode 100644 research/native-equality-cut/verify.py diff --git a/research/native-equality-cut/OVERLAP.json b/research/native-equality-cut/OVERLAP.json new file mode 100644 index 0000000000..f4cd166f72 --- /dev/null +++ b/research/native-equality-cut/OVERLAP.json @@ -0,0 +1,28 @@ +{ + "canonical_main": "5e0052ca0aa3036a3afa8b0438927377c8d97d53", + "priority_revision": 7, + "remote_coverage": { + "open_prs": { + "fetched_at": "2026-10-25T20:50:20.277548+00:00", + "complete_pagination": true, + "records": 328 + }, + "discussions": { + "fetched_at": "2026-10-25T20:51:23.233881+00:00", + "complete_pagination": true, + "records": 4851 + } + }, + "terms": [ + "equality cut", + "native tariff", + "semisimple" + ], + "main_search": "Git grep on canonical-main research README/PROOF and docs/research Markdown for semisimple, matrix-unit, cut-rank and equality/collision terms. Relevant predecessors are identified in README.md.", + "limits": "No code-diff or exhaustive closed-PR review. Sparse local overlap helper omitted most notes; the separate committed-note search covered its declared patterns. No novelty guarantee or scientific acceptance follows.", + "canonical_discussion": "https://github.com/CrocSwap/integer-mult-bounds/discussions/5582", + "excluded_active_scopes": [ + "P104 endpoint retiming and helper706 handoff", + "P104 joint input/output basis changes and private-copy resynthesis" + ] +} diff --git a/research/native-equality-cut/PROOF.md b/research/native-equality-cut/PROOF.md new file mode 100644 index 0000000000..bd4964f178 --- /dev/null +++ b/research/native-equality-cut/PROOF.md @@ -0,0 +1,257 @@ +# A native tariff obstruction that permits changed paid inputs + +Ali Romman, with substantial OpenAI Codex assistance. Apache-2.0. + +This is a necessary condition for a declared class of complete linear native +programs. It is not a lower bound on integer multiplication. The general +off-diagonal rank inequality is classical and already used in the repository. +The contribution here is an invariant cut for the full columnwise monomial +alphabet, its exact Clifford price, and the resulting all-width tariff test. + +## 1. Contract and result + +Fix n>=1 and f>=1. A field has space V=(C^(2^n))^(tensor f). All fields have +this capacity. Independent original inputs, dirty helper inputs and owned +scratch fields are separate registers. A finite linear word may use: + +- Scalar linear combinations of fields, COPY, CLEAR and field permutations. +- Any linear combination of maps M^(tensor f), where M is a one-column + monomial matrix. In particular this includes every monomial Clifford map, + affine address change and quadratic diagonal phase on the n axes. +- A paid application of U^(tensor f) to one field, or a paid update + y <- y + c U^(tensor f) x. Here U is a unitary Clifford matrix and c is + a scalar. Count each field output of a multi-output primitive separately. + +The Fourier rank r(U) is n minus the dimension of the intersection of the +diagonal Pauli space Z with U Z U^*. Equivalently, it is the binary rank of +the X part of the images of the n diagonal Pauli generators. A native +rank-r Gaussian, with monomial changes of frame, has Fourier rank r. + +Require independent final jobs T_j^(tensor f), each on its own original +field. Monomial changes of frame and permutations are allowed. The initial +state contains original fields and zero or independent dirty scratch. Every +nonordinary initial observation must instead be accounted for in section 5. +No larger-field packing or operation between different tensor columns is +granted. More generally, a proposed free map is allowed for a cut exactly +when it preserves that cut and its complement. + +Let P_r and T_r count paid calls and required jobs of Fourier rank r. Then +for every integer k with 1<=2k<=f, + + sum_r P_r (1-2^(-kr)) >= sum_r T_r (1-2^(-kr)). (1) + +If the profiles are fixed and the word works at arbitrarily large widths, +(1) holds for every positive integer k. The word, order, paid inputs, +coefficients, feedback and number of ordinary steps may change with f. +No paid input is frozen. A proof of (1) therefore rejects every word with +the declared profiles and alphabet, including active feedback into paid gates. + +For example, one rank-one and one rank-three call cannot supply two +independent rank-two jobs. Their counts and rank masses agree, but at k=1 +the paid side is 11/8 and the target side is 3/2. This is an obstruction to +the complete native word, not a comparison of quoted upper cost estimates. + +## 2. The equality cut + +Put D=2^n. In each field, let E_k project onto basis strings for which +columns 1 and 2 are equal, columns 3 and 4 are equal, and so on through +columns 2k-1 and 2k. The other columns are unrestricted. Then + + a_k = rank(E_k) = D^(f-k). + +A one-column monomial matrix applies the same bijection to both members +of each pair. It preserves equality and inequality. Its phases are diagonal +and do not change support. Thus M^(tensor f) commutes with E_k. Every +allowed ordinary field operation also commutes with the direct sum of E_k +over the registers. This includes arbitrary ordinary codes across registers. + +For a map A between register banks, define + + rho_k(A) = rank((I-E_out) A E_in). + +The projectors are the direct sums for the relevant input and output banks. +For composable, possibly rectangular maps, + + (AB)_-+ = A_-- B_-+ + A_-+ B_++, + rho_k(AB) <= rho_k(A) + rho_k(B). (2) + +This uses only rank subadditivity and rank(AB)<=rank(B). Invertibility, +unitarity and a tree topology are not required. COPY, CLEAR, arbitrary +feedback and overwrites therefore do not invalidate (2). + +## 3. The exact native price + +For one pair of columns write E=E_1. Its range is spanned by |x,x> and +is the common +1 eigenspace of the n commuting Pauli operators + + Z_j tensor Z_j. + +Its conjugate F=(U tensor U) E (U tensor U)^* is the common +1 eigenspace +of (U Z_j U^*) tensor (U Z_j U^*). Every generator of E commutes with every +generator of F: the two Pauli commutation signs cancel. Thus E and F commute. + +The two stabilizer groups each have n independent generators. Their common +subgroup has dimension n-r(U). There is no sign conflict on this subgroup. +If U Z^v U^*=+/- Z^w, its tensor square is Z^w tensor Z^w. Hence their joint +group has n+r(U) independent generators and contains no negative identity. +It follows that + + rank(E F) = 2^(2n-(n+r(U))) = D 2^(-r(U)). (3) + +For clarity, the stabilizer dimension formula follows by expanding the +projector as the average of its commuting group. Only identity has nonzero +trace. A group with s independent signed Pauli generators and no negative +identity therefore has projector rank 2^(2n-s). + +Since E and F are commuting projections, (I-E)(U tensor U)E has only zero +and unit singular values. Its rank is rank(F)-rank(E F). For k disjoint +pairs, the projections and intersections tensor together. The remaining +columns contribute an identity factor. Consequently + + rho_k(U^(tensor f)) = a_k (1-2^(-k r(U))). (4) + +The nonzero singular values of this cut block are all one. Global phases +of U do not change (3) or (4). Inverse calls have the same rank. + +## 4. Complete words and approximation + +A paid call on one field has cut rank (4). A nonzero scalar query update +has the same cut rank; a zero update has rank zero and may be overcharged. +All ordinary steps have cut rank zero. Apply (2) along the actual word. +This gives the paid side of (1), multiplied by a_k, as an upper bound. + +The independent target jobs occupy disjoint input and output blocks. Their +cut ranks add and give the target side of (1), multiplied by a_k. This +proves (1). Zero scratch insertion and required output selection commute +with the cut. They cannot increase its rank. Arbitrary extra storage does +not invalidate the bound. Invertible ordinary input/output codes also +preserve the cut rank, so the exact obstruction permits those codes. + +There is an approximation consequence for the original independent target +maps and unitary monomial endpoint frames. Let + + delta_k = sum_r (T_r-P_r)(1-2^(-kr)) > 0. + +The target cut block has a_k sum_r T_r(1-2^(-kr)) unit singular values. +The program's cut block has rank at most a_k sum_r P_r(1-2^(-kr)). A rank +deficit leaves a unit vector in the target's initial singular subspace that +the program cut block kills. Thus + + ||program-target||_op >= 1, + ||program-target||_HS^2 >= a_k delta_k. (5) + +Projection onto a cut is a contraction, so the complete endpoint has at +least this error. General invertible ordinary endpoint codes retain the +exact rank obstruction, but can rescale singular values; the constant one +in (5) is not asserted after arbitrary ill-conditioned codes. The paid +maps in this argument are the exact ideal maps. Numerical error inside a +query is not a new free operation in this model. + +## 5. Prior observations and changes of model + +At a caller boundary, let J map the independent original inputs to all +initially available rows, including the actual versions of cached rows. +Use the same input cut and the direct sum cut on the available fields. +The necessary condition becomes + + rho_k(target) <= rho_k(J) + sum_calls rho_k(call). (6) + +This follows from (2) and does not charge a cached response twice. Compute +rho_k(J) on its complete matrix. Do not replace it by nominal row counts: +duplicates and dependent observations can have smaller joint rank. The +identity rows contribute zero. The CLI checks the zero-initial-cross-rank +case (1); it does not claim to extract J from an arbitrary caller. + +The theorem still applies when a later paid input changes, provided the +new word meets this contract. An extra free map that crosses the cut must +be charged by its actual cut rank. Inter-column permutations or payload +maps need not preserve E_k. Different field capacities require typed cuts +and their separate rank factors; canceling a common a_k is then invalid. +Nonlinear or data-dependent operations are outside this linear theorem. + +## 6. A finite exact test for the infinite tariff family + +For fixed finite profiles define the integer polynomial + + C(x) = sum_r (P_r-T_r)(1-x^r). + +The required signs are C(2^(-k))>=0 for k=1,2,... . Rank-zero jobs make +no contribution. If C=0 the test is complete. Otherwise write + + C(x) = x^j (a + sum_(r>j) c_r x^(r-j)), + L = sum_(r>j) |c_r|, a!=0. + +Choose K>=1 with |a| 2^K > L. For k>=K, the absolute remainder in +parentheses is at most L 2^(-k)<|a|. Thus the sign is the sign of a. +Check the finitely many k=1,...,K exactly. A negative leading coefficient +has a failure by K; a positive one certifies the entire remaining tail. +For a fixed width check only k<=floor(f/2). No floating-point roots or +sampled extrapolation is used. Passing this test proves only necessary +inequalities, not a circuit, recursion, compiler result or kappa saving. + +No fixed finite prefix of the hierarchy is sufficient for all profiles. +For any K>=1, put m=2^(K+1), P_1=3, P_3=m and T_2=m+3. Then + + C(x) = x (m x-3) (1-x). + +This is positive at x=2^(-k) for k sum_r P_r r^(1-c). (8) + +Indeed, all target ranks are at most four, so the left side is at least +(22m+42) 4^(-c). The right side is at most 21m+45. For m>=4, + + (21m+45)/(22m+42) <= 129/130 < 2^(-1/128). + +The last strict inequality is equivalent to the integer comparison +130^128 > 2*129^128. Since 4^(-c)>=2^(-1/128), (8) follows. Thus even a +favorable raw saving of 1/256 and any fixed number of these native cut +tests can miss an impossible word. This is not a kappa construction: +the cut proves that no word in the stated model realizes these profiles. +No outer or compiler claim is inferred from the favorable raw moment. + +## 7. Relation to the initial module question + +This investigation began with the semisimple question left by PR5449. +For A=direct_sum_s M_(d_s)(K), let the target module modulo retained history +have simple multiplicities m_s. The exact number of arbitrary linear row +returns in the enlarged multi-input oracle model is + + max_s ceil(m_s/d_s). + +One return is cyclic and contributes at most d_s copies of simple s. +Conversely, matrix units pack up to d_s copies from each simple into one +row, at the same time. This is a direct use of classical semisimple module +theory, not a new theorem in that subject. + +That upper construction need not be one physical single-input query. For +example let A be all diagonal maps on K^3. Start with independent fields +x and y. Require rows e_1 x_3 and e_2 y_3. The output-module formula gives +one arbitrary row return, which can pack the two answers. But one physical +query on one field cannot obtain both independent source values. Before +the query its third coordinate is one scalar combination of x_3 and y_3. +The cut from coordinate 3 to coordinates 1 and 2 has target rank two and +one-call rank at most one. Two calls suffice and are necessary. + +This input bottleneck led to (2). The equality cut makes that principle +work with the full columnwise monomial alphabet, where a coordinate cut +does not. The package therefore develops the native cut obstruction. It +does not publish the unrestricted row-packing formula as a physical +query compiler. The earlier frozen 104-return result remains unchanged. diff --git a/research/native-equality-cut/README.md b/research/native-equality-cut/README.md new file mode 100644 index 0000000000..83fcc474f5 --- /dev/null +++ b/research/native-equality-cut/README.md @@ -0,0 +1,152 @@ +# Native tariff constraints that permit active feedback + +This package proves a necessary cost constraint for complete linear native +words. It permits changed paid inputs, feedback, arbitrary scalar mixing, +COPY, CLEAR and the full columnwise monomial alphabet. It does not keep +the old caller frozen. + +For paid and target Fourier-rank profiles P and T, every such word at +width f must satisfy + +```text +sum_r P_r (1-2^(-k*r)) >= sum_r T_r (1-2^(-k*r)) +for every integer k with 1 <= 2*k <= f. +``` + +Fixed profiles that work at arbitrarily large widths must pass every k. +[cuts.py](cuts.py) decides this infinite family with a finite exact +polynomial test. It gives a failing cut when one exists. The proof uses +equality of pairs of tensor columns. Every columnwise monomial map +preserves this cut. A rank-r Clifford query has exactly the displayed +normalized cut rank. + +This can reject a proposed supplier invoice before native synthesis. One +rank-one plus one rank-three call cannot supply two independent rank-two +jobs, although both the call count and rank mass agree. More strongly, +for every K there is a profile that passes all earlier cuts and first +fails at K. No fixed prefix of checks is complete. A failing cut also +forces operator norm error at least one for the ideal native word and +the stated unitary target frames. + +The delayed failures include profiles with a strictly favorable raw +power moment for every saving from zero through **1/256**. Thus a large +raw saving and any fixed prefix of native cuts can both be false signals. +The adaptive exact test detects these profiles without a word search. +This is an impossibility result for those invoices, not a new kappa. + +**No kappa improvement or native admission is claimed.** The pinned P104 +complete profile, with 69,930 paid calls and 12,814 target jobs, passes +all these necessary constraints. The test does not reject that route. +This is a new obstruction and search filter for changed caller designs. + +## Exact scope + +Read [PROOF.md](PROOF.md) for the theorem and all hypotheses. Every field +has the same whole-field capacity. Paid calls are single-field Clifford +tensor maps or scalar query updates. The final credit is for independent +native target jobs. Ordinary maps must preserve the chosen cuts. The +full columnwise monomial group does; general inter-column routing does +not. Larger-field packing and different capacities need separate factors. + +The exact rank obstruction also permits invertible ordinary input/output +codes. The unit error constant needs the stated unitary endpoint frames. +For a boundary with nonordinary cached observations, the joint cut rank +of the complete initial availability matrix belongs on the paid side. +Section 5 gives this relative form; the CLI does not extract that matrix. +Duplicate rows do not earn duplicate initial rank. + +The original semisimple-module question led to a useful distinction: +an optimal set of arbitrary linear output rows need not fit through the +inputs of physical single-field queries. Section 7 gives the exact +three-coordinate counterexample and records that part of the research. + +## Reproduce and use in a search + +Python 3.12 and its standard library suffice. No native build, external +package, solver or network access is needed. + +```sh +python3 -B scripts/research_package.py --package research/native-equality-cut +python3 -I -B research/native-equality-cut/cuts.py research/native-equality-cut/examples/equal-mass-trade.json +``` + +The second command returns exit code 1 and an exact failing witness. For +another candidate, supply JSON objects `paid` and `targets`, with decimal +rank strings and nonnegative integer counts. An optional positive `width` +restricts the check to that width. Without it the CLI checks all positive +k. Exit code 0 means only that these necessary conditions pass. + +For a profile search, first include every paid call and every required +target once. Run the CLI on each proposed invoice. A witness k gives the +linear constraint displayed above for the next optimization round. Use +exact rational coefficients when certifying that constraint. A passing +profile still needs a word, physical input/output bindings and the full +compiler, precision, storage, routing and outer bill. + +## Evidence + +The registered normal and optimized checks use literal Gaussian-rational +matrices. They check all 24 projective one-axis Clifford classes and +constructed two-/three-axis words, including non-diagonal frames. There +are 172 literal cross-block rank checks and 172 exact partial-isometry +checks. A separate support count checks the binary Pauli Fourier rank. +The explicit rank-three obstruction supplies an additional native case. + +The full input/output matrices of 48 chronological words cover 480 +prefixes with feedback, overwrite, COPY, CLEAR and arbitrary dirty +directions. Controls check duplicate initial responses, the physical +input bottleneck and a noncolumnwise map that crosses the cut. The tariff +tests include 192 profile pairs, all 625 differences with four ranks and +coefficients from -2 through 2, two families with first failures at cuts +1 through 12, width boundaries and invalid inputs. The favorable raw +moment uses an exact integer-power comparison. See [RESULT.json](RESULT.json). + +The P104 application authenticates a byte-exact copy of its source result +and checks its complete profiles. It does not rerun the P104 native word, +its compiler or the selected cold replay. Finite checks support the +written proof; they are not proof-kernel acceptance or independent human +review. The baseline binding helper stopped on omitted sparse source +files during orientation. No selected-baseline pass is claimed. + +## Open next questions + +1. Apply these linear constraints in a supplier search that changes the + word. Start with the complete proposed paid/target profiles. A physical + caller and its ordinary-operation contract remain necessary. +2. Find stronger invariant cuts for operations that mix tensor columns. + First state the permitted maps and check which projectors they preserve. + The present cuts do not charge those maps for free. +3. At an actual retained-observation boundary, extract the complete + availability matrix J and use its joint cut rank. The missing source + versions and physical availability ledger remain the blocker. + +## Sources, overlap and credit + +Base: canonical main `5e0052ca0aa3036a3afa8b0438927377c8d97d53`, priority +revision 7. [Discussion #5582](https://github.com/CrocSwap/integer-mult-bounds/discussions/5582) +is the canonical investigation. The initial claim took the open semisimple +question in [PR #5449](https://github.com/CrocSwap/integer-mult-bounds/pull/5449). +The changed scope and its input bottleneck are recorded there and in TASK. +Active P104 endpoint-retiming and joint-basis claims were excluded. + +The repository already uses the classical off-diagonal rank inequality in +[the fused-block audit](../../docs/research/fused-block-audit.md), the +dirty-host cut-rank work of an664 and its reviewers, and the later tariff +work of Adam Gall and Ross Richardson. Those arguments retain their credit. +The full monomial-invariant equality cut and exact Clifford tariff are +the contribution here. General cut-rank, stabilizer and semisimple-module +theory are not claimed as new. + +Chris R / Clear1nsight supplies the retained-history context in PR5425/5446. +The source-specific frozen repair is PR5526. Discussion5300/PR5310 uses +related module theory for a different finite-ring source-insertion contract. +P104 retains Gareth Davidson's PR2305, David Arias's PR2152, Cinna's PR2219, +the productive-helper, native, compiler and outer predecessors, and Ali +Romman's PR5544 integration. Its profile is evidence for the arithmetic +screen here, not a new verification of that full construction. + +The exact scalar layer is unchanged from zxv's +`research/universal-dirty-certificates/fields.py`; its notice is retained. +[SOURCES.json](SOURCES.json) pins the source files and unchanged local +copies. New proof, code and prose: Ali Romman, with substantial OpenAI Codex +assistance. No subagents. Apache-2.0. No selected-frontier change. diff --git a/research/native-equality-cut/RESULT.json b/research/native-equality-cut/RESULT.json new file mode 100644 index 0000000000..94e98e601f --- /dev/null +++ b/research/native-equality-cut/RESULT.json @@ -0,0 +1,119 @@ +{ + "authenticated_sources": 3, + "chronological": { + "complete_dirty_prefixes": 480, + "words": 48 + }, + "native": { + "fourier_ranks": { + "0": 54, + "1": 106, + "2": 12 + }, + "literal_cross_blocks": 172, + "one_axis_projective_classes": 24, + "partial_isometry_checks": 172 + }, + "no_new_kappa": true, + "obstructions": { + "duplicate_cache_joint_rank": 1, + "literal_small_native_ranks": [ + 4, + 6, + 7 + ], + "noncolumnwise_cut_rank": 2, + "single_input_bottleneck": 2 + }, + "polynomials": { + "delayed_first_failures": [ + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 9, + 10, + 11, + 12 + ], + "exhaustive_rank_four_differences": 625, + "invalid_input_controls": 4, + "profitable_first_failures": [ + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 9, + 10, + 11, + 12 + ], + "profitable_raw_saving": "1/256", + "random_profile_pairs": 192 + }, + "source_screen": { + "cut_test": { + "checks": [ + { + "k": 1, + "paid": "12902133998418396879119859/295147905179352825856", + "paid_minus_targets": "86415520319733806820061916777035493241977307149/2787593149816327892691964784081045188247552", + "targets": "35441689983514108204574126187216441278927470579/2787593149816327892691964784081045188247552" + } + ], + "polynomial": { + "0": 57116, + "1": -45282, + "145": 208, + "16": -416, + "17": 416, + "2": -10026, + "24": -416, + "25": 416, + "3": -7002, + "32": -416, + "33": 416, + "4": -1098, + "40": -416, + "41": 416, + "48": -416, + "49": 416, + "5": -1296, + "56": -416, + "57": 416, + "6": -288, + "64": -416, + "65": 416, + "7": 198, + "72": -208, + "73": 208, + "8": 2196, + "9": 5274 + }, + "schema": "native-equality-cut/v1", + "scope": "necessary conditions; no native admission or kappa claim", + "status": "PASS_NECESSARY_EQUALITY_CUTS", + "tail": { + "certified_from_k": 1, + "first_degree": 0, + "leading_coefficient": 57116, + "remaining_absolute_sum": 79108, + "strict_sign": 1 + }, + "width": null + }, + "paid_calls": 69930, + "source_native_word_replayed": false, + "status": "PASS_SOURCE_PROFILE_SCREEN_ONLY", + "target_jobs": 12814 + }, + "status": "PASS_NATIVE_EQUALITY_CUT" +} diff --git a/research/native-equality-cut/SOURCES.json b/research/native-equality-cut/SOURCES.json new file mode 100644 index 0000000000..f3670030de --- /dev/null +++ b/research/native-equality-cut/SOURCES.json @@ -0,0 +1,89 @@ +{ + "schema_version": 1, + "base_commit": "5e0052ca0aa3036a3afa8b0438927377c8d97d53", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "fc3d4ba105e1f097d0d7d051a308281e86ab1446", + "sha256": "66974efdced4083c00025f97d95d83909a226cdf801edb9301c195c6641f6903" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/paid-history-quotient/README.md", + "usage": "provenance", + "git_blob": "f1c72c7c8e291f04272d645fea3e78f5f7ecb80a", + "sha256": "c219f4d143be68639c676a5ff6e3ff84651b484be6a95f1a3d538c71182fd78f" + }, + { + "path": "research/clifford-pointwise-faithfulness/REPAIR.md", + "usage": "provenance", + "git_blob": "417748bf8620ef23330dfd30d823b4e89370d263", + "sha256": "4b1ec6a8c41dd8e5d49f33c926738b18a41b7cf28d8e81b68faa2ddc59fa3e23" + }, + { + "path": "docs/research/fused-block-audit.md", + "usage": "provenance", + "git_blob": "a6020c272835a00d441aa711b2dc566402deaab0", + "sha256": "b304d2dc368443f67e6817dcad9d1a277f85ed6b8b7ae529763a53bc05020e79" + }, + { + "path": "research/dirty-host-cutrank-audit/PROOF.md", + "usage": "provenance", + "git_blob": "042fc663f14f0aff985984f201a1cdf89997d594", + "sha256": "2921c2c741ab5086a87c53340f18180ecc55675ca7dadc49579da32aba71d2f5" + }, + { + "path": "research/universal-dirty-certificates/fields.py", + "usage": "provenance", + "git_blob": "f1b6dc83e26bd9fd9ec67ded3fedb330ef89598d", + "sha256": "0829ad6ed3775ba6e3d11cf04cfb3513ac763549b730aaed74958b1238e660d7" + }, + { + "path": "research/p104-productive-controller/RESULT.json", + "usage": "provenance", + "git_blob": "5637130d4a3884948eda39c185e3b6e8f4b4717b", + "sha256": "03e9f8424b9166899d3ae3b188d9defb851162a3183ecab237fb783d78216782" + }, + { + "path": "research/p104-productive-controller/PROOF.md", + "usage": "provenance", + "git_blob": "e0bb34fbef6b412b572818d669150b54a13ea30d", + "sha256": "f4c4e400092954562252df6c4dd157a9b4c1642252168ce72738cdbecfc5ad41" + }, + { + "path": "LICENSE", + "usage": "provenance", + "git_blob": "261eeb9e9f8b2b4b0d119366dda99c6fd7d35c64", + "sha256": "c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4" + } + ], + "retained_files": [ + { + "local_path": "vendor/fields.py", + "source_path": "research/universal-dirty-certificates/fields.py", + "source_commit": "5e0052ca0aa3036a3afa8b0438927377c8d97d53", + "git_blob": "f1b6dc83e26bd9fd9ec67ded3fedb330ef89598d", + "sha256": "0829ad6ed3775ba6e3d11cf04cfb3513ac763549b730aaed74958b1238e660d7" + }, + { + "local_path": "vendor/LICENSE", + "source_path": "LICENSE", + "source_commit": "5e0052ca0aa3036a3afa8b0438927377c8d97d53", + "git_blob": "261eeb9e9f8b2b4b0d119366dda99c6fd7d35c64", + "sha256": "c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4" + }, + { + "local_path": "evidence/p104-result.json", + "source_path": "research/p104-productive-controller/RESULT.json", + "source_commit": "5e0052ca0aa3036a3afa8b0438927377c8d97d53", + "git_blob": "5637130d4a3884948eda39c185e3b6e8f4b4717b", + "sha256": "03e9f8424b9166899d3ae3b188d9defb851162a3183ecab237fb783d78216782" + } + ] +} diff --git a/research/native-equality-cut/TASK.json b/research/native-equality-cut/TASK.json new file mode 100644 index 0000000000..3d93601952 --- /dev/null +++ b/research/native-equality-cut/TASK.json @@ -0,0 +1,107 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 7, + "base_commit": "5e0052ca0aa3036a3afa8b0438927377c8d97d53", + "original_card": { + "id": "formal-interface-lemma", + "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/gate-operand-parity-lean/README.md", + "research/staged544-certified-endpoint/README.md", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Formalize a missing boundary lemma identified by the selected review.", + "Audit a formal theorem-to-certificate binding independently." + ], + "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Inventory the gate-operand parity lemma (#3807) and certified endpoint arithmetic (#3857). Neither is a full multiplication proof. For #4100, audit the compact-switch statement and its hypotheses before formalizing it.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.", + "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.", + "allowed_variations": [ + "Narrow to one formal lemma or one theorem-to-certificate binding." + ], + "scope_change_triggers": [ + "Formalizing already-covered arithmetic and claiming the full multiplication theorem." + ], + "overlap_terms": [ + "hyperplane end", + "formal interface", + "Lean binding", + "3807", + "3857", + "4100", + "gate-operand-parity-lean", + "staged544-certified-endpoint", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #3807: scoped gate-operand parity formalization.", + "evidence": "research/gate-operand-parity-lean/README.md", + "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.", + "status": "author-checked", + "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #3857: certified real-power moment/endpoint arithmetic.", + "evidence": "research/staged544-certified-endpoint/README.md", + "remaining": "Uniform algorithmic implications, not another endpoint digit.", + "status": "author-checked", + "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4100: compact-switch formalization proposed as future validation.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Audit the statement and assumptions before a formal proof campaign.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "A complete-word native tariff obstruction from equal-column cuts, with active feedback and changed paid inputs allowed.", + "scope_change_reason": "The PR5449 semisimple handoff gives an output-module count but not a single-field input construction. A physical input-cut counterexample led to a monomial-invariant native cut and its exact Clifford tariff. This is a written interface theorem, not a Lean proof.", + "bottleneck_link": "Reject impossible proposed paid/target profiles before native synthesis, while permitting changes to the paid word and its inputs.", + "budget_minutes": 180, + "stop_rule": "Prove the cut tariff and complete-word inequality, test literal native matrices and chronological words, decide all dyadic cuts exactly, bind a current source profile, then publish the scoped result.", + "outcome": "completed", + "evidence": "PROOF.md, including an arbitrarily delayed impossible profile with favorable raw saving 1/256; exact.py and verify.py; RESULT.json; source-authenticated P104 profile screen.", + "author": "Ali Romman", + "ai_assistance": "Substantial OpenAI Codex assistance. No subagents.", + "open_questions": [ + { + "question": "Can a changed-word supplier search use the cut inequalities to discard impossible candidate invoices?", + "why_it_matters": "The filter can avoid native synthesis of a profile that no word in the declared alphabet can attain.", + "first_step": "Apply cuts.py to complete candidate profiles and add each failing cut as an exact linear constraint.", + "blocked_by": "A passing profile still needs a physical word and complete native/compiler/outer pricing." + }, + { + "question": "Which cuts survive an explicitly larger inter-column ordinary alphabet?", + "why_it_matters": "Such an alphabet can escape this obstruction and may permit a new supplier.", + "first_step": "State the new ordinary generators and compute their invariant projections.", + "blocked_by": "No larger-alphabet physical contract is supplied." + }, + { + "question": "What is the joint initial cut rank at one actual boundary with retained observations?", + "why_it_matters": "The relative inequality prevents a duplicate charge and preserves active feedback.", + "first_step": "Extract the full versioned availability map J, including original independent inputs.", + "blocked_by": "The current package does not supply the boundary availability and ownership ledger." + } + ] +} diff --git a/research/native-equality-cut/VERIFY.json b/research/native-equality-cut/VERIFY.json new file mode 100644 index 0000000000..cc7d4e7386 --- /dev/null +++ b/research/native-equality-cut/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Authenticate retained sources; exact native cut ranks and singular values; full chronological dirty prefixes; delayed tariff failures and source profile screen." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "-O", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Authenticate retained sources; exact native cut ranks and singular values; full chronological dirty prefixes; delayed tariff failures and source profile screen." + } + ] +} diff --git a/research/native-equality-cut/cuts.py b/research/native-equality-cut/cuts.py new file mode 100644 index 0000000000..516e2b641e --- /dev/null +++ b/research/native-equality-cut/cuts.py @@ -0,0 +1,91 @@ +#!/usr/bin/env python3 +"""Check necessary native tariffs from equal-column cuts. + +Ali Romman, with substantial OpenAI Codex assistance. Apache-2.0. +""" +import argparse +from fractions import Fraction +import json +from pathlib import Path + + +def profile(value): + if type(value) is not dict: + raise ValueError("a profile must be an object") + result = {} + for key, count in value.items(): + if type(key) is not str or not key.isdecimal() or str(int(key)) != key: + raise ValueError("ranks must be canonical nonnegative integer strings") + if type(count) is not int or count < 0: + raise ValueError("counts must be nonnegative integers") + if int(key) and count: + result[int(key)] = count + return result + + +def tariff(counts, k): + return sum((count * (1 - Fraction(1, 1 << (k * rank))) + for rank, count in counts.items()), Fraction(0)) + + +def audit(data): + paid, targets = profile(data['paid']), profile(data['targets']) + width = data.get('width') + if width is not None and (type(width) is not int or width < 1): + raise ValueError("width must be a positive integer") + coefficients = {0: sum(paid.values()) - sum(targets.values())} + for rank in paid.keys() | targets.keys(): + coefficients[rank] = targets.get(rank, 0) - paid.get(rank, 0) + coefficients = {r: a for r, a in sorted(coefficients.items()) if a} + result = { + 'schema': 'native-equality-cut/v1', + 'scope': 'necessary conditions; no native admission or kappa claim', + 'width': width, + 'polynomial': {str(r): a for r, a in coefficients.items()}, + 'checks': [], + } + if not coefficients: + result.update(status='PASS_NECESSARY_EQUALITY_CUTS', tail='identically zero') + return result + first = next(iter(coefficients)) + lead = coefficients[first] + remainder = sum(abs(a) for r, a in coefficients.items() if r > first) + cutoff = 1 + while abs(lead) * (1 << cutoff) <= remainder: + cutoff += 1 + result['tail'] = { + 'first_degree': first, 'leading_coefficient': lead, + 'remaining_absolute_sum': remainder, 'certified_from_k': cutoff, + 'strict_sign': 1 if lead > 0 else -1, + } + limit = cutoff if width is None else min(cutoff, width // 2) + for k in range(1, limit + 1): + p, t = tariff(paid, k), tariff(targets, k) + result['checks'].append({'k': k, 'paid': str(p), 'targets': str(t), + 'paid_minus_targets': str(p - t)}) + if p < t: + result.update(status='FAIL_NECESSARY_EQUALITY_CUTS', witness={ + 'k': k, 'minimum_width': 2 * k, + 'normalized_rank_deficit': str(t - p), + 'ideal_endpoint_operator_error_lower_bound': 1, + }) + return result + result['status'] = ('PASS_NECESSARY_EQUALITY_CUTS' if limit + else 'NO_EQUALITY_CUT_AT_THIS_WIDTH') + return result + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('invoice', type=Path) + args = parser.parse_args() + try: + result = audit(json.loads(args.invoice.read_text(encoding='utf-8'))) + except (KeyError, TypeError, ValueError) as error: + parser.error(str(error)) + print(json.dumps(result, indent=2, sort_keys=True)) + return 1 if result['status'] == 'FAIL_NECESSARY_EQUALITY_CUTS' else 0 + + +if __name__ == '__main__': + raise SystemExit(main()) diff --git a/research/native-equality-cut/evidence/p104-result.json b/research/native-equality-cut/evidence/p104-result.json new file mode 100644 index 0000000000..5637130d4a --- /dev/null +++ b/research/native-equality-cut/evidence/p104-result.json @@ -0,0 +1,315 @@ +{ + "complete_cost": { + "compiler": { + "H": 64215200000000, + "N": "2^64215200000000", + "eta": { + "lower": "0.000000185845792706621973271570", + "upper": "0.000000185845792706621973271571" + }, + "gap": "1/1400000000", + "integer_test_exponent": 45868, + "logarithm_power": 1000, + "theta": "63/64", + "uniform_saving": "1064201/350000000", + "word_materialized": false + }, + "full_forward_calls": 18, + "gain": "2656353/200000000000", + "kappa": "304057/100000000", + "kappa_decimal": ".00304057", + "margin_at_previous": { + "lower": "3.300756773058285958096643251393", + "upper": "3.300756773058285958096643251394" + }, + "negative_controls": { + "old_BIT": "Rejected by outer inequalities", + "old_cutoff": "Rejected by completion-tail ratio greater than one" + }, + "nonrecursive": { + "fixed_scalar_growth_bound": "At most 2^(16*26000) before native factors; a declared constant, not an attained norm.", + "local_routes": 5335000, + "local_scalar": 217428, + "peak_owned_fields": 1, + "raw_budget": 1000000000, + "raw_scalar_upper": 184647552, + "tensor_native_growth_bound": "Each rank-r Gaussian has row l1 norm at most 2^(rf); sum of local ranks is 5894." + }, + "ordinary_BIT": { + "admitted": "17/5000", + "after_cover": "69/20000", + "atom": "1/250", + "before_cover": "3459/1000000", + "ordinary_saving": "8590884599/2500000000000", + "prime_rule": "odd q > 2^26*N^5 avoiding all fixed denominators and rank witnesses" + }, + "outer": { + "functional_checks": { + "actual_new_BIT_stock_sublinear": "348599999253/350000000000", + "fixed_halo_explicit_metadata_branch": "26950000001/350000000", + "new_BIT_row_stock_sublinear_in_active_group": "1395799997009/1400000000000", + "new_semantic_group_guard": "3/1400000000" + }, + "margins": { + "boundary_algebraic_matrix": "5959522795743199/1960000000000000000", + "fused_gaussian": "5959522787229597/1960000000000000000", + "global_coordinate_router": "2128401/700000000", + "group_bit_router": "2979762093614797/980000000000000000", + "group_scans": "699999999/700000000", + "main_transform": "5959521395743199/1960000000000000000", + "microbox_face_corrections": "26950000001/350000000", + "polynomial_products": "1399999999/1400000000", + "sparse_union_movement": "802209522795743199/1960000000000000000" + }, + "parameters": { + "a": "2128401/700000000", + "b": "4256803/1400000000", + "beta": "1399999997/1400000000", + "bit_saving": "17/5000", + "cap_xi": "1782209521395743199/1960000000000000000", + "complex_uniform_saving": "1064201/350000000", + "d": "1/1400000000", + "epsilon": "1399999999/1400000000", + "kappa": "304057/100000000", + "lambda_": "398783771/400000000", + "lambda_prime": "1395743199/1400000000", + "layout": "1/1400000000", + "q": "4256801/1400000000", + "r0": "1/14000000000", + "stop": "1/1400000000", + "tested_saving": "121623/40000000" + }, + "strict_checks": { + "actual_bit_above_effective": "251599/700000000", + "actual_logarithmic_gamma_guard": "1/1400000000", + "actual_logarithmic_group_guard": "177790480704256801/980000000000000000", + "alpha_logarithm_absorption": "1/14000000000", + "boundary_algebraic_matrix_above_kappa": "5595743199/1960000000000000000", + "cap_above_band": "802209521395743199/1960000000000000000", + "cap_below_cell": "177790477204256801/1960000000000000000", + "cap_below_phase_cell_power": "2137790478604256801/1960000000000000000", + "complex_above_effective": "1/1400000000", + "complex_below_one_over_32": "39493197/1400000000", + "complex_endpoint": "1/700000000", + "epsilon_below_one": "1/1400000000", + "epsilon_positive": "1399999999/1400000000", + "fine_prime_halo_umbrella": "7/2", + "fused_gaussian_above_kappa": "5587229597/1960000000000000000", + "gaussian_above_main": "695743199/980000000000000000", + "global_coordinate_router_above_kappa": "1/350000000", + "global_gamma_power_slack": "9/14000000000", + "group_below_dimension": "1/700000000", + "group_bit_router_above_kappa": "3493614797/980000000000000000", + "group_gauge_power_slack": "177790480634256801/980000000000000000", + "group_key_fits_record": "1/700000000", + "group_positive": "1399999997/1400000000", + "group_scans_above_kappa": "1744679/1750000", + "halo_covers_generic_inverse_radius": "5", + "improvement_over_user_baseline": "654799790400418148631/500000000000000000000000", + "lambda_above_internal": "1/2800000000", + "lambda_above_sigma": "3/2800000000", + "lambda_above_tau": "1/2800000000", + "lambda_prime_above_lambda": "1/2800000000", + "lambda_prime_above_leaf": "2795743197/1960000000000000000", + "leaf_saving_above_effective": "1395743197/1960000000000000000", + "main_transform_above_kappa": "4195743199/1960000000000000000", + "membership_arithmetic_fits_record": "1/1400000000", + "microbox_face_corrections_above_kappa": "53897871603/700000000", + "microbox_halo_volume": "110600000003/1400000000", + "new_complex_uniform_saving_above_b": "1/1400000000", + "new_semantic_guard_with_C1_one": "1/1400000000", + "polynomial_products_above_kappa": "1395743201/1400000000", + "positive_layout_slack": "1/1400000000", + "q_below_effective": "1/1400000000", + "q_below_internal": "1/1400000000", + "q_below_leaf": "2795743197/1960000000000000000", + "q_positive": "4256801/1400000000", + "short_record_fallback": "1395743197/1400000000", + "source_axis_superpolynomial": "1/1400000000", + "sparse_union_movement_above_kappa": "796250005595743199/1960000000000000000", + "stop_below_one": "1399999999/1400000000", + "stop_positive": "1/1400000000", + "strassen_integer_power_gap": "1951441519231", + "support_router_span": "3/1400000000", + "theta_positive_polynomial_power": "2", + "union_header_fits_record": "3/1400000000", + "union_tag_work_per_visit_fits_record": "3/1400000000" + } + }, + "paid": { + "1": 45282, + "16": 416, + "2": 10026, + "24": 416, + "3": 7002, + "32": 416, + "4": 2016, + "40": 416, + "48": 416, + "5": 1944, + "56": 416, + "6": 288, + "64": 416, + "7": 234, + "72": 208, + "9": 18 + }, + "paid_calls": 69930, + "previous_selected": "605457647/200000000000", + "productive_fields": 12814, + "query_shears": 15, + "rank_mass_surplus": 760, + "raw_headroom": [ + "80763/10000000000000", + "807631/100000000000000" + ], + "raw_root_interval": [ + "30405780763/10000000000000", + "304057807631/100000000000000" + ], + "relative_gain_percent": "265635300/605457647", + "strictification": { + "alpha": { + "lower": "0.999999996781290806577194629544", + "upper": "0.999999996781290806577194629545" + }, + "cutoff": 17, + "delta": { + "lower": "0.963354732998265185478252854607", + "upper": "0.963354732998265185478252854608" + }, + "floor": 18, + "gamma": { + "lower": "0.965182172149361102612340648898", + "upper": "0.965182172149361102612340648899" + }, + "normalized_paid_upper": "5242880004882813/5242880536870912", + "power": 1024, + "reserve": "1/10000000000", + "tail_offset": "1/5", + "tested": "121623/40000000" + }, + "targets": { + "145": 208, + "17": 416, + "25": 416, + "33": 416, + "4": 918, + "41": 416, + "49": 416, + "5": 648, + "57": 416, + "65": 416, + "7": 432, + "73": 208, + "8": 2196, + "9": 5292 + }, + "whole_idle_jobs": 3120 + }, + "limits": [ + "Conditional on the retained native all-column, owned-erasure, compiler, precision/tape and analytic-recovery framework.", + "The winning uniform compiler word and complete integer multiplier are not materialized.", + "No proof-kernel check or independent human review is claimed." + ], + "local": { + "endpoint_coefficients": 552049, + "helpers": { + "4": 51, + "5": 36, + "7": 24, + "8": 122, + "9": 294 + }, + "owned_lifetimes": 8, + "paid": { + "1": 2429, + "2": 557, + "3": 389, + "4": 112, + "5": 108, + "6": 16, + "7": 13, + "9": 1 + }, + "peak_owned_fields": 1, + "public_inputs": 735, + "real_scalar_allowance": 217428 + }, + "native": { + "distinct_maps": 2981, + "helper_normalizers": 1054, + "helpers": { + "4": 51, + "5": 36, + "7": 24, + "8": 122, + "9": 294 + }, + "main_adapters": 208, + "proof": "Every signed Pauli image and exact global phase; frame induction at every positive tensor width", + "recipe_payload_sha256": "0a12b2a43238496b226b47dd0e790882d03d1b1b66107308ab37dd6ce21a0481", + "wrong_phase_rejected": true + }, + "negative_controls": { + "missing_central_translation": "Rejected by the complete Laurent endpoint", + "omitted_copy": "Rejected by full arbitrary-input endpoint", + "unearned_helper": "Rejected by native helper census", + "wrong_frame": "Rejected by literal source-frame check" + }, + "physical_caller": { + "central_square_columns": 53248, + "full_calls": 18, + "main_targets": { + "145": 208, + "17": 416, + "25": 416, + "33": 416, + "41": 416, + "49": 416, + "57": 416, + "65": 416, + "73": 208 + }, + "new_paid_jobs": 0, + "physical_contacts": 7488, + "ports": 104, + "route_payload_sha256": "7f4f0ca768ffbc4f93dcff575592c4c67411f46b4289e45b73f715a2ad47b142", + "tensor_rule": "Factorwise native maps; scalar signs stay outside the tensor power.", + "whole_idle_jobs": { + "16": 416, + "24": 416, + "32": 416, + "40": 416, + "48": 416, + "56": 416, + "64": 416, + "72": 208 + }, + "wrapper_sites": [ + 1, + 3, + 5, + 7, + 9, + 11, + 13, + 15, + 17, + 19, + 21, + 23, + 25, + 27, + 29, + 31 + ] + }, + "separate_columns": { + "arithmetic": "Dense integer rows with binary denominators; reverse chronology", + "coefficients": 552049, + "columns": 743 + }, + "source_inputs_authenticated": 16, + "status": "PASS_P104_PRODUCTIVE_COMPLETE_KAPPA_00304057" +} diff --git a/research/native-equality-cut/exact.py b/research/native-equality-cut/exact.py new file mode 100644 index 0000000000..b90d096146 --- /dev/null +++ b/research/native-equality-cut/exact.py @@ -0,0 +1,191 @@ +"""Small exact matrices for independent native-cut checks. + +The scalar implementation is the unchanged, attributed predecessor file. +Ali Romman, with substantial OpenAI Codex assistance. Apache-2.0. +""" +from itertools import product +from pathlib import Path +import sys + +sys.path.insert(0, str(Path(__file__).resolve().parent / 'vendor')) +from fields import Gaussian as G + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def eye(d): + return tuple(tuple(G(int(i == j)) for j in range(d)) for i in range(d)) + + +def zero(rows, columns): + return [[G(0) for _ in range(columns)] for _ in range(rows)] + + +def mul(a, b): + out = zero(len(a), len(b[0])) + sparse = [[(j, v) for j, v in enumerate(row) if v] for row in b] + for i, row in enumerate(a): + for k, x in enumerate(row): + if x: + for j, y in sparse[k]: + out[i][j] = out[i][j] + x * y + return tuple(map(tuple, out)) + + +def adjoint(a): + return tuple(tuple(G.pair(x.real, -x.imag) for x in col) for col in zip(*a)) + + +def rank(a): + basis = {} + for vector in a: + row = list(vector) + for p, old in sorted(basis.items()): + if row[p]: + c = row[p] + row = [x - c * y for x, y in zip(row, old)] + p = next((j for j, x in enumerate(row) if x), None) + if p is not None: + c = row[p] + basis[p] = tuple(x / c for x in row) + return len(basis) + + +def tensor(a, b): + return tuple(tuple(x * y for x in ar for y in br) for ar in a for br in b) + + +def power_tensor(a, f): + out = ((G(1),),) + for _ in range(f): + out = tensor(out, a) + return out + + +def matrix_key(a): + return tuple((z.real, z.imag) for row in a for z in row) + + +def canonical(a): + choices = [tuple(tuple(c * x for x in row) for row in a) + for c in (G(1), G('i'), G(-1), G('-i'))] + return min(choices, key=matrix_key) + + +def gate(n, kind, i=0, j=1): + d = 1 << n + if kind in ('S', 'X', 'CX', 'CZ'): + a = zero(d, d) + for x in range(d): + y, phase = x, G(1) + if kind == 'S' and (x >> i) & 1: + phase = G('i') + elif kind == 'X': + y ^= 1 << i + elif kind == 'CX' and (x >> i) & 1: + y ^= 1 << j + elif kind == 'CZ' and (x >> i) & (x >> j) & 1: + phase = G(-1) + a[y][x] = phase + return tuple(map(tuple, a)) + need(kind == 'Q', 'gate kind') + a = zero(d, d) + for x in range(d): + a[x][x] = G('1/2+1/2i') + a[x ^ (1 << i)][x] = G('1/2-1/2i') + return tuple(map(tuple, a)) + + +def one_axis_cliffords(): + first = canonical(eye(2)) + found = {matrix_key(first): first} + queue = [first] + for a in queue: + for g in (gate(1, 'S'), gate(1, 'Q')): + b = canonical(mul(g, a)) + key = matrix_key(b) + if key not in found: + found[key] = b + queue.append(b) + need(len(queue) == 24, 'complete one-axis projective orbit') + return queue + + +def fourier_rank(a): + """Use conjugated diagonal Paulis, not the target tariff.""" + d = len(a) + n = d.bit_length() - 1 + need(d == 1 << n and mul(adjoint(a), a) == eye(d), 'unitary power-of-two map') + labels = [] + for j in range(n): + z = tuple(tuple(G((-1 if (x >> j) & 1 else 1) if x == y else 0) + for y in range(d)) for x in range(d)) + b = mul(mul(a, z), adjoint(a)) + xs = [] + for col in range(d): + rows = [row for row in range(d) if b[row][col]] + need(len(rows) == 1, 'conjugated Pauli support') + xs.append(rows[0] ^ col) + need(len(set(xs)) == 1, 'Pauli translation') + labels.append(xs[0]) + pivots = {} + for x in labels: + while x: + p = x.bit_length() - 1 + if p not in pivots: + pivots[p] = x + break + x ^= pivots[p] + r = len(pivots) + need(all(sum(bool(row[j]) for row in a) == 1 << r for j in range(d)), + 'independent support-rank check') + return r + + +def equality_indices(d, f, k): + return [j for j, word in enumerate(product(range(d), repeat=f)) + if all(word[2*t] == word[2*t+1] for t in range(k))] + + +def literal_cross(a, f, k): + """Build only the literal cross block; use no stabilizer formula.""" + d = len(a) + words = list(product(range(d), repeat=f)) + inside = [w for w in words if all(w[2*t] == w[2*t+1] for t in range(k))] + outside = [w for w in words if any(w[2*t] != w[2*t+1] for t in range(k))] + out = [] + for y in outside: + row = [] + for x in inside: + value = G(1) + for u, v in zip(y, x): + value = value * a[u][v] + row.append(value) + out.append(tuple(row)) + return tuple(out) + + +def bank_gate(registers, payload, kind, dst, src=None, coefficient=1): + """Build a literal complete bank operation, including dirty directions.""" + v = len(payload) + result = [list(row) for row in eye(registers * v)] + if kind in ('apply', 'clear', 'copy'): + for i in range(v): + result[dst*v+i] = [G(0) for _ in range(registers * v)] + if kind in ('apply', 'add', 'copy'): + source = dst if kind == 'apply' else src + for i in range(v): + for j in range(v): + result[dst*v+i][source*v+j] += coefficient * payload[i][j] + else: + need(kind == 'clear', 'bank operation kind') + return tuple(map(tuple, result)) + + +def cross_rank(a, inside, output_inside=None): + selected = set(inside if output_inside is None else output_inside) + return rank(tuple(tuple(row[j] for j in inside) + for i, row in enumerate(a) if i not in selected)) diff --git a/research/native-equality-cut/examples/delayed-failure.json b/research/native-equality-cut/examples/delayed-failure.json new file mode 100644 index 0000000000..c784d4f25f --- /dev/null +++ b/research/native-equality-cut/examples/delayed-failure.json @@ -0,0 +1,4 @@ +{ + "paid": {"1": 3, "3": 8}, + "targets": {"2": 11} +} diff --git a/research/native-equality-cut/examples/equal-mass-trade.json b/research/native-equality-cut/examples/equal-mass-trade.json new file mode 100644 index 0000000000..257c21f217 --- /dev/null +++ b/research/native-equality-cut/examples/equal-mass-trade.json @@ -0,0 +1,4 @@ +{ + "paid": {"1": 1, "3": 1}, + "targets": {"2": 2} +} diff --git a/research/native-equality-cut/examples/profitable-delayed-failure.json b/research/native-equality-cut/examples/profitable-delayed-failure.json new file mode 100644 index 0000000000..dd74de784a --- /dev/null +++ b/research/native-equality-cut/examples/profitable-delayed-failure.json @@ -0,0 +1,4 @@ +{ + "paid": {"1": 9, "3": 68}, + "targets": {"2": 45, "4": 32} +} diff --git a/research/native-equality-cut/vendor/LICENSE b/research/native-equality-cut/vendor/LICENSE new file mode 100644 index 0000000000..261eeb9e9f --- /dev/null +++ b/research/native-equality-cut/vendor/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/native-equality-cut/vendor/NOTICE.md b/research/native-equality-cut/vendor/NOTICE.md new file mode 100644 index 0000000000..121af323bb --- /dev/null +++ b/research/native-equality-cut/vendor/NOTICE.md @@ -0,0 +1,8 @@ +# Retained scalar implementation + +`fields.py` is byte-identical to +`research/universal-dirty-certificates/fields.py` at canonical main +`5e0052ca0aa3036a3afa8b0438927377c8d97d53`. It was prepared for zxv with +substantial OpenAI Codex assistance under Apache-2.0. Its original notice +is unchanged. `LICENSE` is the repository's Apache-2.0 license at that +same commit. The exact source and copy hashes are in `../SOURCES.json`. diff --git a/research/native-equality-cut/vendor/fields.py b/research/native-equality-cut/vendor/fields.py new file mode 100644 index 0000000000..f1b6dc83e2 --- /dev/null +++ b/research/native-equality-cut/vendor/fields.py @@ -0,0 +1,140 @@ +"""Small exact scalar layer shared by producer and checker (part of their trust base). + +Prepared for zxv with substantial OpenAI Codex assistance. Apache-2.0. +""" +from fractions import Fraction +from math import isqrt +from functools import lru_cache +import re + + +class Gaussian: + """Q(i); input strings use a+bi with rational a,b, or just i/-i.""" + def __init__(self, value=0): + if isinstance(value, Gaussian): + self.real, self.imag = value.real, value.imag + elif type(value) is str and value.endswith("i"): + body = value[:-1] + rational = r"\d+(?:/\d+)?" + match = re.fullmatch(r"([+-]?"+rational+r")([+-](?:"+rational+r")?)", body) + if match: + self.real = Fraction(match[1]) + self.imag = Fraction(match[2]+"1" if match[2] in ("+", "-") else match[2]) + else: + if body in ("", "+", "-"): + body += "1" + self.real, self.imag = Fraction(0), Fraction(body) + else: + self.real, self.imag = Fraction(value), Fraction(0) + + @classmethod + def pair(cls, real, imag): + out = cls() + out.real, out.imag = real, imag + return out + + def __add__(self, other): + z = Gaussian(other) + return self.pair(self.real+z.real, self.imag+z.imag) + + __radd__ = __add__ + + def __mul__(self, other): + z = Gaussian(other) + return self.pair(self.real*z.real-self.imag*z.imag, self.real*z.imag+self.imag*z.real) + + __rmul__ = __mul__ + + def __neg__(self): + return self.pair(-self.real, -self.imag) + + def __sub__(self, other): + return self+-Gaussian(other) + + def __rsub__(self, other): + return Gaussian(other)+-self + + def __truediv__(self, other): + z = Gaussian(other) + norm = z.real*z.real+z.imag*z.imag + return self*self.pair(z.real/norm, -z.imag/norm) + + def __rtruediv__(self, other): + return Gaussian(other)/self + + def __eq__(self, other): + z = Gaussian(other) + return self.real == z.real and self.imag == z.imag + + def __bool__(self): + return bool(self.real or self.imag) + + def __str__(self): + if not self.imag: + return str(self.real) + return str(self.real)+("+" if self.imag >= 0 else "")+str(self.imag)+"i" + + __repr__ = __str__ + + +def scalars(problem): + p = problem.get("field", "Q") + if p == "Q": + return Fraction + if p == "Qi": + return Gaussian + if type(p) is not int: + raise ValueError("field must be Q, Qi or a prime at most 2^31-1") + return prime_scalars(p) + + +@lru_cache(maxsize=32) +def prime_scalars(p): + if not 2 <= p <= 2**31-1 or any(p % d == 0 for d in range(2, isqrt(p)+1)): + raise ValueError("field must be Q, Qi or a prime at most 2^31-1") + + class Prime: + def __init__(self, x=0): + if isinstance(x, Prime): + self.value = x.value + else: + q = Fraction(x) + self.value = q.numerator*pow(q.denominator, -1, p) % p + + def __add__(self, other): + return Prime(self.value+Prime(other).value) + + __radd__ = __add__ + + def __mul__(self, other): + return Prime(self.value*Prime(other).value) + + __rmul__ = __mul__ + + def __neg__(self): + return Prime(-self.value) + + def __sub__(self, other): + return self+-Prime(other) + + def __rsub__(self, other): + return Prime(other)+-self + + def __truediv__(self, other): + return Prime(self.value*pow(Prime(other).value, -1, p)) + + def __rtruediv__(self, other): + return Prime(other)/self + + def __eq__(self, other): + return self.value == Prime(other).value + + def __bool__(self): + return bool(self.value) + + def __str__(self): + return str(self.value) + + __repr__ = __str__ + + return Prime diff --git a/research/native-equality-cut/verify.py b/research/native-equality-cut/verify.py new file mode 100644 index 0000000000..f52c9c8bb8 --- /dev/null +++ b/research/native-equality-cut/verify.py @@ -0,0 +1,235 @@ +#!/usr/bin/env python3 +"""Check native equality cuts with exact independent matrix calculations. + +Ali Romman, with substantial OpenAI Codex assistance. Apache-2.0. +""" +import argparse +from fractions import Fraction as Q +import hashlib +from itertools import product +import json +from pathlib import Path +import random +import sys + +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE)) +from cuts import audit +from exact import (G, adjoint, bank_gate, cross_rank, equality_indices, eye, + fourier_rank, gate, literal_cross, mul, need, + one_axis_cliffords, power_tensor, rank, tensor) + + +def authenticated_sources(): + manifest = json.loads((HERE / 'SOURCES.json').read_text()) + for item in manifest.get('retained_files', []): + payload = (HERE / item['local_path']).read_bytes() + need(hashlib.sha256(payload).hexdigest() == item['sha256'], + 'retained source hash: ' + item['local_path']) + return len(manifest.get('retained_files', [])) + + +def native_checks(): + maps = [(u, f, k) for u in one_axis_cliffords() + for f, k in ((2, 1), (3, 1), (4, 1), (4, 2), (6, 3))] + rng = random.Random(5582) + for n, samples in ((2, 32), (3, 16)): + for sample in range(samples): + u = eye(1 << n) + for _ in range(9): + kind = rng.choice(('Q', 'S', 'X', 'CX', 'CZ')) + i, j = rng.sample(range(n), 2) + u = mul(gate(n, kind, i, j), u) + maps.append((u, 2, 1)) + if n == 2 and sample < 4: + maps.append((u, 4, 2)) + counts = {} + partial_isometries = 0 + for u, f, k in maps: + d, r = len(u), fourier_rank(u) + b = literal_cross(u, f, k) + expected = d**(f-k) * (1 - Q(1, 1 << (k*r))) + need(rank(b) == expected, 'literal native cut tariff') + counts[str(r)] = counts.get(str(r), 0) + 1 + gram = mul(adjoint(b), b) + need(mul(gram, gram) == gram, 'unit nonzero cut singular values') + partial_isometries += 1 + return {'literal_cross_blocks': len(maps), 'fourier_ranks': counts, + 'partial_isometry_checks': partial_isometries, + 'one_axis_projective_classes': 24} + + +def chronological_checks(): + rng = random.Random(16582) + registers, v = 3, 4 + inside = [r*v+i for r in range(registers) for i in equality_indices(2, 2, 1)] + orbit = one_axis_cliffords() + prefixes = 0 + for _ in range(48): + word, budget = eye(registers*v), 0 + for step in range(10): + dst, src = rng.sample(range(registers), 2) + coefficient = rng.choice((1, -1, G('i'), Q(1, 2))) + if step in (2, 6): + u = rng.choice(orbit) + payload = power_tensor(u, 2) + kind = rng.choice(('add', 'apply')) + budget += cross_rank(payload, equality_indices(2, 2, 1)) + else: + u = gate(1, rng.choice(('S', 'X'))) + payload = power_tensor(u, 2) + kind = rng.choice(('add', 'apply', 'copy', 'clear')) + need(cross_rank(payload, equality_indices(2, 2, 1)) == 0, + 'ordinary map must preserve the cut') + event = bank_gate(registers, payload, kind, dst, src, coefficient) + word = mul(event, word) + need(cross_rank(word, inside) <= budget, 'chronological rank budget') + prefixes += 1 + return {'words': 48, 'complete_dirty_prefixes': prefixes} + + +def obstruction_checks(): + native = [] + for r in (1, 2, 3): + u = eye(8) + for j in range(r): + u = mul(gate(3, 'Q', j), u) + native.append(rank(literal_cross(u, 2, 1))) + need(native == [4, 6, 7], 'literal rank-one/two/three prices') + need(native[0]+native[2] < 2*native[1], 'equal-mass fusion fails') + + q = power_tensor(gate(1, 'Q'), 2) + initial = tuple(eye(4)) + tuple(q) + tuple(q) + source_inside = equality_indices(2, 2, 1) + available_inside = [r*4+i for r in range(3) for i in source_inside] + need(cross_rank(initial, source_inside, available_inside) == 1, + 'duplicate observations have one joint cut rank') + + # One field query cannot move two independent coordinate-three inputs. + target = [[G(0) for _ in range(6)] for _ in range(6)] + target[0][2] = G(1) + target[4][5] = G(1) + need(cross_rank(target, [2, 5]) == 2, 'input bottleneck has rank two') + two_calls = eye(12) + for source, output_coordinate in ((0, 0), (1, 1)): + two_calls = mul(bank_gate(4, eye(3), 'copy', source+2, source), two_calls) + paid = [[G(0) for _ in range(3)] for _ in range(3)] + paid[output_coordinate][2] = G(1) + two_calls = mul(bank_gate(4, paid, 'apply', source+2), two_calls) + expected = [list(row) for row in eye(12)[:6]] + expected += [[G(0) for _ in range(12)] for _ in range(6)] + expected[6][2] = G(1) + expected[10][5] = G(1) + need(two_calls == tuple(map(tuple, expected)), 'complete two-call packing endpoint') + + # A map on only one tensor column is not an ordinary columnwise lift. + bad_free = tensor(gate(1, 'X'), eye(2)) + need(cross_rank(bad_free, source_inside) == 2, 'noncolumnwise escape control') + return {'literal_small_native_ranks': native, 'duplicate_cache_joint_rank': 1, + 'single_input_bottleneck': 2, 'noncolumnwise_cut_rank': 2} + + +def polynomial_checks(): + delayed = [] + profitable = [] + need(130**128 > 2*129**128, 'exact raw-saving comparison at 1/256') + for k in range(1, 13): + m = 1 << (k+1) + data = {'paid': {'1': 3, '3': m}, 'targets': {'2': m+3}} + result = audit(data) + need(result['status'] == 'FAIL_NECESSARY_EQUALITY_CUTS' and + result['witness']['k'] == k, 'first failure at a prescribed cut') + if k > 1: + need(audit(dict(data, width=2*k-1))['status'] == + 'PASS_NECESSARY_EQUALITY_CUTS', 'width cutoff must apply') + need(audit(dict(data, width=2*k))['status'] == + 'FAIL_NECESSARY_EQUALITY_CUTS', 'failure at the first valid width') + delayed.append(k) + phantom = {'paid': {'1': 9, '3': 7*m+12}, + 'targets': {'2': 3*m+21, '4': 4*m}} + result = audit(phantom) + need(result['status'] == 'FAIL_NECESSARY_EQUALITY_CUTS' and + result['witness']['k'] == k, 'profitable profile first failing cut') + need(130*(21*m+45) <= 129*(22*m+42), 'raw moment ratio bound') + # Check the factored polynomial by a separate exact evaluation. + for j in range(1, k+2): + x = Q(1, 1 << j) + literal = 9*(1-x)+(7*m+12)*(1-x**3)-(3*m+21)*(1-x**2)-4*m*(1-x**4) + need(literal == x*(m*x-3)*(3-4*x)*(1-x), 'profitable polynomial identity') + profitable.append(k) + rng = random.Random(5922) + cases = [{side: {str(r): rng.randrange(8) for r in range(1, 8)} + for side in ('paid', 'targets')} for _ in range(192)] + for delta in product(range(-2, 3), repeat=4): + cases.append({'paid': {str(r): max(c, 0) for r, c in enumerate(delta, 1)}, + 'targets': {str(r): max(-c, 0) for r, c in enumerate(delta, 1)}}) + for data in cases: + result = audit(data) + p = {int(r): c for r, c in data['paid'].items()} + t = {int(r): c for r, c in data['targets'].items()} + limit = (result['tail']['certified_from_k'] + 24 + if type(result['tail']) is dict else 24) + highest = max(p.keys() | t.keys()) + values = [Q(sum((p[r]-t[r])*((1 << (k*highest)) - (1 << (k*(highest-r)))) + for r in p), 1 << (k*highest)) for k in range(1, limit+1)] + failed = result['status'] == 'FAIL_NECESSARY_EQUALITY_CUTS' + need(failed == any(x < 0 for x in values), 'direct independent tariff evaluation') + if failed: + need(result['witness']['k'] == next(k for k, x in enumerate(values, 1) if x < 0), + 'first failure witness') + need(audit({'paid': {'0': 17, '1': 2}, 'targets': {'1': 2}})['tail'] == + 'identically zero', 'rank-zero jobs are ordinary') + need(audit({'paid': {'1': 1}, 'targets': {'1': 2}, 'width': 1})['status'] == + 'NO_EQUALITY_CUT_AT_THIS_WIDTH', 'no invented width-one cut') + invalid = [({'paid': {'01': 1}, 'targets': {}}, 'rank encoding'), + ({'paid': {'1': True}, 'targets': {}}, 'boolean count'), + ({'paid': {'1': -1}, 'targets': {}}, 'negative count'), + ({'paid': {}, 'targets': {}, 'width': 0}, 'zero width')] + for data, label in invalid: + try: + audit(data) + except ValueError: + pass + else: + raise ValueError('accepted invalid input: '+label) + return {'delayed_first_failures': delayed, 'random_profile_pairs': 192, + 'exhaustive_rank_four_differences': 625, + 'profitable_first_failures': profitable, + 'profitable_raw_saving': '1/256', + 'invalid_input_controls': len(invalid)} + + +def source_screens(): + path = HERE / 'evidence' / 'p104-result.json' + source = json.loads(path.read_text()) + invoice = {side: source['complete_cost'][side] for side in ('paid', 'targets')} + result = audit(invoice) + need(result['status'] == 'PASS_NECESSARY_EQUALITY_CUTS', 'P104 source tariff screen') + need(source['complete_cost']['paid_calls'] == sum(invoice['paid'].values()) == 69930, + 'P104 paid census') + need(source['complete_cost']['productive_fields'] == sum(invoice['targets'].values()) == 12814, + 'P104 target census') + return {'status': 'PASS_SOURCE_PROFILE_SCREEN_ONLY', + 'paid_calls': 69930, 'target_jobs': 12814, + 'cut_test': result, 'source_native_word_replayed': False} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--write', action='store_true') + args = parser.parse_args() + result = {'status': 'PASS_NATIVE_EQUALITY_CUT', + 'authenticated_sources': authenticated_sources(), + 'native': native_checks(), 'chronological': chronological_checks(), + 'obstructions': obstruction_checks(), 'polynomials': polynomial_checks(), + 'source_screen': source_screens(), 'no_new_kappa': True} + text = json.dumps(result, indent=2, sort_keys=True) + '\n' + if args.write: + (HERE / 'RESULT.json').write_text(text) + else: + need(text == (HERE / 'RESULT.json').read_text(), 'retained result comparison') + print(text) + + +if __name__ == '__main__': + main()