diff --git a/research/negative-e-decoder-gram-bound/INPUTS.json b/research/negative-e-decoder-gram-bound/INPUTS.json new file mode 100644 index 0000000000..a473f9160a --- /dev/null +++ b/research/negative-e-decoder-gram-bound/INPUTS.json @@ -0,0 +1,26 @@ +[ + { + "path": "source/decoder-proof.md", + "repository": "JoyboyBrian/integer-mult-bounds", + "commit": "7e6824d560337e2b2e49da8b98727183491f6ecf", + "source_path": "research/odd-e8-negative-exit-algebra/PROOF.md", + "git_blob": "bc945b4901cc1c20da7d904ad238224aada71634", + "sha256": "6109fd631868ca7cf55c1d9178ff0a2ac030afe4353bc701e715757e4a754b06" + }, + { + "path": "source/decoder-result.json", + "repository": "JoyboyBrian/integer-mult-bounds", + "commit": "7e6824d560337e2b2e49da8b98727183491f6ecf", + "source_path": "research/odd-e8-negative-exit-algebra/RESULT.json", + "git_blob": "0813bbb062c5ab28247d24fadac94d3cd67db137", + "sha256": "df10c3db7f0513e4cd43311bb22c9db15af8422c272339fffa933081c01768c7" + }, + { + "path": "source/clifford-proof.md", + "repository": "aliromman/integer-mult-bounds", + "commit": "32e014bec9206f3987857e6153ec0fd8058f04e3", + "source_path": "research/clifford-pointwise-faithfulness/PROOF.md", + "git_blob": "465009d9d1b6947e80e6f1e868022f47ddab1f3c", + "sha256": "45483e4b5f604a5e70602c5caaa4394d4a0d0d1a6d0b6e8a93b836d50b23f764" + } +] diff --git a/research/negative-e-decoder-gram-bound/README.md b/research/negative-e-decoder-gram-bound/README.md new file mode 100644 index 0000000000..f386834bb5 --- /dev/null +++ b/research/negative-e-decoder-gram-bound/README.md @@ -0,0 +1,204 @@ +# A width-296 exclusion and error floor for the actual negative E decoder + +This source-bound application lowers the ordinary-decoder exclusion threshold +in JoyboyBrian's [PR #5508](https://github.com/CrocSwap/integer-mult-bounds/pull/5508) +from width 4198 to 296. It also gives a nonzero approximation-error floor. +It uses the pointwise Clifford Gram theorem in +[PR #5526](https://github.com/CrocSwap/integer-mult-bounds/pull/5526). +The complete kappa calculation and selected frontier are unchanged. + +## Exact scope and conclusion + +Use the fixed source endpoint chart and negative-bank observation contract of +PR #5508. There are 73 binary address axes. At width f the required postdecoder is + +```text +J_f = Q_f^-1 E_(1,f)^-1 E_(2,f) E_(3,f)^-1 Q_f. +``` + +The only available dependent input is the emitted negative bank. Other owned +or dirty inputs are independent. Ordinary address operations are tensor lifts +of one-column monomial Cliffords. Arbitrary scalar owner mixing, instruction +count, independent workspace and f-dependent coefficients are permitted. + +For every integer f>=296, no such ordinary program implements J_f. More +strongly, for every such ordinary endpoint O_f, in the fixed source chart, + +```text +||J_f-O_f||_op >= 1541/1255956. +``` + +This is a worst-case unit-input error floor, not an error on every input. It +also applies to any larger endpoint required to contain the specified decoder +block, by restriction to its original input and projection onto its output. +It is not invariant under arbitrary nonunitary rescaling of that chart. + +No minimum width is asserted. At smaller widths the new argument gives no +decision. Paid calls, correlated original-input histories, operations mixing +tensor columns, nonlinear rounding and changed target contracts remain outside +scope. This is not a paid-child lower bound or a physical completion invoice. + +## Pinned premises and their roles + +The package keeps byte-exact copies of three public files. INPUTS.json records +their repositories, commits, Git objects and SHA256 values. The verifier checks +those bytes before using the consumed data. Frozen predecessor files are not +edited and no predecessor executable is imported. + +1. [PR #5508 proof](https://github.com/JoyboyBrian/integer-mult-bounds/blob/7e6824d560337e2b2e49da8b98727183491f6ecf/research/odd-e8-negative-exit-algebra/PROOF.md): + the actual owner code, negative endpoint, ordered fresh-stage path uniqueness + and unique nonzero path class are cited premises. +2. Its [exact result](https://github.com/JoyboyBrian/integer-mult-bounds/blob/7e6824d560337e2b2e49da8b98727183491f6ecf/research/odd-e8-negative-exit-algebra/RESULT.json): + the selected owner endpoints, signed 25-axis map, source coefficient and + sparse conjugated column are checked independently below. +3. [PR #5526 proof](https://github.com/aliromman/integer-mult-bounds/blob/32e014bec9206f3987857e6153ec0fd8058f04e3/research/clifford-pointwise-faithfulness/PROOF.md): + projective Clifford tensor independence and its dimension-uniform Gram + bounds are cited premises. The consumed rational row bounds are recomputed. + +These pending written proofs are not declared independently accepted by this +application. Source authentication and the checks below do not replace their +full mathematical review or the source producer's physical admission. + +## Verify the full alphabet premise + +Each stage source factor is a scalar owner matrix conjugated by block-diagonal +signed linear address permutations L_i. Expanding the fixed owner block gives + +```text +(J_f)_(i,j) = sum_path c_path (Q^-1 M_path Q)^(tensor f), +``` + +where M_path is a product of signed linear binary permutations. The scalar +owner coefficients c_path are applied once; they are not raised to f. +A binary invertible linear permutation is a CNOT Clifford, and a linear sign +is a Pauli Z product. Thus every M_path is unitary Clifford. The source Q is +the one-central-axis square root of X, + +```text +Q = ((1+i)/2) I + ((1-i)/2) X. +``` + +It is unitary, Q squared is X, and it conjugates Paulis to Paulis. Hence every +conjugated path is a 73-axis unitary Clifford with Gaussian-dyadic entries. +This checks the actual expanded alphabet; the sum J itself need not be a +Clifford. The distinction is required for applying PR #5526. + +The source's ordered path separation says that distinct paths between the +fixed owner endpoints have distinct linear maps. Therefore they are not +projectively equal, before or after conjugation by Q. At each width, folding a +representative phase changes a path coefficient only by a unit phase. It does +not cancel the chosen coefficient with another path. + +For each original-input/output block, any ordinary program in the stated +alphabet lies in the scalar span of lifted monomial Cliffords. Composition, +addition, scalar multiplication, COPY and CLEAR preserve this property, for +any number of independent workspace fields. This also holds for each specified +f when the word and its scalars depend on f. + +## The actual path is outside the ordinary alphabet + +The retained endpoints are j=(0,0,0) and i=(1,0,0). The source root rows have +squared norm four and mutual dot product two. The inverse-stage cross entry +is therefore 1/4, while the diagonal inverse entry is one. The middle-stage +entry is + +```text +39*98/(2744*97) + 1078/(2744*1079) = 1541/104663. +``` + +The selected path coefficient is + +```text +c_star = (1/4)*(1541/104663)*1 = 1541/418652. +``` + +These rational identities are recomputed from the consumed source data. +The complete path map reduces to the signed 25-axis map supplied in the +source result, extended by identity on the other 48 axes. Its first binary +column is 657934, so it moves the central direction e0. + +If a signed monomial M has linear map G with Ge0 different from e0, expansion +of Q^-1 M Q gives four distinct output addresses on every basis input x: +Gx, Gx+e0, Gx+Ge0 and Gx+e0+Ge0. Their coefficient magnitudes are 1/2. +The four destinations are distinct because G is invertible and Ge0 is neither +zero nor e0. Thus the chosen Clifford class is nonmonomial, even after a global +phase. At input zero the exact consumed column is + +```text +0 : 1/2 +1 : i/2 +657934 : i/2 +657935 : -1/2. +``` + +The independent sparse interpreter reconstructs this column and 146 further +basis columns, checks invertibility of the binary map, and checks Q inverse +and square identities. The all-input conclusion follows from the four distinct +addresses, not extrapolation from the finite sample. + +## Apply the pointwise Gram theorem + +Put D=2^73. For distinct projective unitary Clifford classes, PR #5526 gives, +at every f>=4*73+4=296, + +```text +D^(-f) ||sum_g b_g U_g^(tensor f)||_HS^2 >= (1/9) sum_g |b_g|^2. +``` + +Subtract any ordinary block O from the selected decoder block. Its monomial +classes cannot change the chosen nonmonomial coefficient. After all projective +classes are combined, that coefficient still has magnitude c_star. Therefore + +```text +D^(-f) ||(J_f)_(i,j)-O||_HS^2 >= c_star^2/9 + = 2374681/1577425473936. +``` + +Since the normalized Hilbert-Schmidt norm is at most the operator norm, this +proves the error floor and exact nonmembership. Restricting the complete +endpoint to this input block and projecting onto this output block cannot +increase operator norm, which gives the stated complete-endpoint consequence. + +The later source bound also gives normalized squared error at least +(125/126)*c_star squared for every f>=308. It is a stronger sufficient constant, +not a claim of optimal distance. The source's old support argument first +passes at f=4198 because 2f-216 must exceed 8178. Its ADD-count lower bound and +broader cross-column exclusions retain their original scopes. + +## Verification and limitations + +```sh +python3.12 -B scripts/research_package.py --package research/negative-e-decoder-gram-bound +``` + +Use Python 3.12 and the standard library. Registered warning-strict normal and +optimized runs print `PASS_NEGATIVE_E_DECODER_GRAM_BOUND` and the launcher prints +`PASS_REGISTERED_RESEARCH_PACKAGE`. Each run authenticates three immutable +inputs and checks 147 sparse columns, 36 finite rational Gram row bounds, +complete dimension-uniform geometric tails and nine rejecting or semantic +controls. It checks changed coefficients, source axes, owner endpoints, signs, +unproved width, projective phase cancellation and external-scalar placement. + +The complete source owner-path family and general Clifford counting theorem +are credited written premises. Their full scientific suites, independent human +review, proof-kernel verification, selected cold replay, physical emission, +precision application and complete paid invoice were not run here. No native +supplier, new kappa or change to the five selected framework assumptions follows. + +## Open next questions + +Bind a changed paid decoder or a correlated-history interface to the complete +caller and its remaining invoice. That change can evade the present observation +contract. State the new original-input identity first, then check every paid +call, helper lifetime and precision budget. The present floor must not be +subtracted as a paid-call count. + +## Credit + +JoyboyBrian supplies PR #5508, its actual E-code/path binding, signed normalizer +and support consequence, with the source producer and helper lineage retained +in the copied proof. Ali Romman (@aliromman) supplies PR #5526 and the earlier +fresh-stage separation lineage. The retained sources credit their native, +Clifford, stabilizer and compiler predecessors. The new contribution is this +source-bound width and error application. Proof and checks by Ali Romman with +substantial OpenAI Codex assistance; Apache-2.0. No global novelty claim is made. diff --git a/research/negative-e-decoder-gram-bound/SOURCES.json b/research/negative-e-decoder-gram-bound/SOURCES.json new file mode 100644 index 0000000000..2a2c456287 --- /dev/null +++ b/research/negative-e-decoder-gram-bound/SOURCES.json @@ -0,0 +1,44 @@ +{ + "schema_version": 1, + "base_commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "fc3d4ba105e1f097d0d7d051a308281e86ab1446", + "sha256": "66974efdced4083c00025f97d95d83909a226cdf801edb9301c195c6641f6903" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + } + ], + "external_provenance": [ + { + "path": "source/decoder-proof.md", + "repository": "JoyboyBrian/integer-mult-bounds", + "commit": "7e6824d560337e2b2e49da8b98727183491f6ecf", + "source_path": "research/odd-e8-negative-exit-algebra/PROOF.md", + "git_blob": "bc945b4901cc1c20da7d904ad238224aada71634", + "sha256": "6109fd631868ca7cf55c1d9178ff0a2ac030afe4353bc701e715757e4a754b06" + }, + { + "path": "source/decoder-result.json", + "repository": "JoyboyBrian/integer-mult-bounds", + "commit": "7e6824d560337e2b2e49da8b98727183491f6ecf", + "source_path": "research/odd-e8-negative-exit-algebra/RESULT.json", + "git_blob": "0813bbb062c5ab28247d24fadac94d3cd67db137", + "sha256": "df10c3db7f0513e4cd43311bb22c9db15af8422c272339fffa933081c01768c7" + }, + { + "path": "source/clifford-proof.md", + "repository": "aliromman/integer-mult-bounds", + "commit": "32e014bec9206f3987857e6153ec0fd8058f04e3", + "source_path": "research/clifford-pointwise-faithfulness/PROOF.md", + "git_blob": "465009d9d1b6947e80e6f1e868022f47ddab1f3c", + "sha256": "45483e4b5f604a5e70602c5caaa4394d4a0d0d1a6d0b6e8a93b836d50b23f764" + } + ] +} diff --git a/research/negative-e-decoder-gram-bound/TASK.json b/research/negative-e-decoder-gram-bound/TASK.json new file mode 100644 index 0000000000..78ffd2a951 --- /dev/null +++ b/research/negative-e-decoder-gram-bound/TASK.json @@ -0,0 +1,74 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 7, + "base_commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Does one quantified step of the proposed #4100 all-size construction hold at its actual caller?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Prove one missing implication with explicit quantified hypotheses.", + "Find an exact counterexample at the claimed interface boundary." + ], + "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read PROOF.md and AUDIT.md in #4100. Select one distinct obligation: CRT total repair, native/free-algebra lifting, precision/conditioning, or complete fixed-tape cost. This is an author-submitted proof, not an accepted unconditional theorem.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Check live handoffs; name one proposition, its caller, quantified domain and dependency closure. Independently prove the implication or exhibit a precise gap/counterexample. Prioritize CRT.md total repair or COMPLEX.md free-algebra lift only if unclaimed. Stop at the chosen obligation; do not substitute finite samples or root arithmetic for an all-size proof, or launch the complete package by default.", + "bottleneck_link": "Finite supplier improvements are useful only under the retained transfer obligations.", + "allowed_variations": [ + "One CRT repair, native lift, precision/conditioning or tape-cost proposition, with its exact caller." + ], + "scope_change_triggers": [ + "Replacing a quantified obligation with another finite smoke test.", + "Treating archive intake, an author PASS receipt or a finite composed fixture as discharge of the universal hypotheses." + ], + "overlap_terms": [ + "uniform transfer", + "all-size", + "precision", + "4100", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Bind the pointwise Clifford Gram theorem to the actual 73-axis negative E postdecoder.", + "scope_change_reason": "Take the released PR5508 decoder boundary and the unreserved actual-caller application in PR5526.", + "bottleneck_link": "Lower the width of the actual ordinary-decoder obstruction and quantify its worst-case approximation error.", + "budget_minutes": 60, + "stop_rule": "Check the consumed alphabet, coefficient and sparse native map; do not claim paid-child pricing or correlated-history coverage.", + "outcome": "completed", + "evidence": "Pinned source proofs, independently checked source coefficient and sparse columns, exact Gram row bounds.", + "author": "Ali Romman", + "ai_assistance": "Substantial OpenAI Codex assistance.", + "open_questions": [ + { + "question": "Can a paid decoder or changed correlated-history contract complete the actual caller within its full budget?", + "why_it_matters": "Those interfaces can evade the negative-bank-only ordinary span.", + "first_step": "State the complete original-input identity and added-paid/lost-target ledger.", + "blocked_by": "No physical completion, retained-history ownership or complete precision and cost bill is supplied." + } + ] +} diff --git a/research/negative-e-decoder-gram-bound/VERIFY.json b/research/negative-e-decoder-gram-bound/VERIFY.json new file mode 100644 index 0000000000..f7a5a9250a --- /dev/null +++ b/research/negative-e-decoder-gram-bound/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 source proofs and data; check exact path, sparse native map, rational Gram bounds and controls." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "-O", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Authenticate source proofs and data; check exact path, sparse native map, rational Gram bounds and controls." + } + ] +} diff --git a/research/negative-e-decoder-gram-bound/source/clifford-proof.md b/research/negative-e-decoder-gram-bound/source/clifford-proof.md new file mode 100644 index 0000000000..465009d9d1 --- /dev/null +++ b/research/negative-e-decoder-gram-bound/source/clifford-proof.md @@ -0,0 +1,305 @@ +# Pointwise tensor faithfulness for Clifford and stabilizer maps + +Ali Romman, with substantial OpenAI Codex assistance. Apache-2.0. + +This is an algebraic result. It supplies no physical implementation or new +kappa. The classical ingredients are stabilizer normal forms, symplectic +residual forms, character orthogonality and the Gram row bound. The new +contribution in this repository is their quantitative pointwise consequence. + +## 1. Statements + +Let C_n be the unitary n-qubit Clifford matrices with entries in Z[i,1/2]. +Its scalar subgroup is {I,iI,-I,-iI}. Choose one representative U_g for +each projective class. Indeed a unit Gaussian-dyadic scalar satisfies +a^2+b^2=4^k with integers a,b. Repeated parity reduction leaves only a +Gaussian unit. Set D=2^n. For n>=1 and every integer f>=4n+4, + + (1/9) sum_g |b_g|^2 + <= D^(-f) ||sum_g b_g U_g^(tensor f)||_HS^2 + <= (17/9) sum_g |b_g|^2. (1) + +The coefficients are arbitrary complex numbers at this one width. Thus all +the projective tensor operators are linearly independent at every such f. +Any subset has the same bounds. The choice of representative phase does not +change the bounds. The proof also applies to the usual Clifford group with +arbitrary unit scalar phases, after projective classes are combined. + +For a fixed residual in the exact dyadic group algebra, the following are +equivalent: + +1. Every exact-operator coefficient is zero. +2. The residual vanishes at every positive width. +3. It vanishes at the four widths 4n+4,...,4n+7. + +If M is the squared coefficient norm after equal exact operators are +combined, at least one of these four normalized squared norms is >= M/9. +Four tests are necessary for this exact group with arbitrary complex scalar +coefficients. This is a sufficient width bound, not a sharp width threshold. +For n=0 the group is the four scalar phases; widths 1,2,3,4 suffice. + +There is a broader result. A nonzero stabilizer map from a binary input +space to a binary output space is a matrix whose vectorization, up to a +nonzero scalar, is a pure stabilizer state. Let N be the total number of +input and output axes. Normalize these vectors to unit length and choose +one per projective class. At every f>=2N+6 their tensor Gram matrix has + + (2/5) I <= Gram_f <= (8/5) I. (2) + +This includes rectangular maps and Pauli projections. For arbitrary +unnormalized representatives A_g, (2) means + + ||sum_g b_g A_g^(tensor f)||_HS^2 + >= (2/5) sum_g |b_g|^2 ||A_g||_HS^(2f). (3) + +The statements at a single width allow different finite words, different +scalar coefficients and different subsets at each width. They do not infer +all-width equality of a changing family from four tests. Products must +still have the stated columnwise Clifford or stabilizer-map form. + +There is a robust consequence. If a unitary Clifford target T is absent +from a set of projective classes S, then for f>=4n+4, + + D^(-f) ||T^(tensor f)-sum_(g in S) b_g U_g^(tensor f)||_HS^2 + >= (1/9)(1+sum_g |b_g|^2) >= 1/9. (4) + +Its operator norm error is therefore at least 1/3. This is a worst-case +unit-input error bound, not a guarantee about the error on each input. +Later widths use the stronger constants in Section 4. In particular the +lower bound on normalized squared error tends to one as f increases. + +## 2. Count the stabilizer overlaps + +A projective N-qubit stabilizer state has a computational-basis support +which is an affine binary subspace. In coordinates t on its k-dimensional +support, its amplitudes have the form + + 2^(-k/2) i^(a.t + 2 sum_(j. A state has a nonzero overlap of modulus 2^(-k/2) +with it exactly when its support is a k-subspace containing zero. Normalize +its amplitude at zero to be positive. The remaining phase polynomial is +unique. There are + + A_(N,k) = [N choose k]_2 2^(k(k+3)/2) (5) + +such states, including A_(N,0)=1. Here + + [N choose k]_2 = product_(j=0..k-1) + (2^(N-j)-1)/(2^(k-j)-1). + +There are k coefficients with four choices and k(k-1)/2 coefficients with +two choices. This proves the exponent in (5). The other states have zero +overlap. Clifford conjugation is transitive on pure stabilizer states, so +the same distribution holds about every projective stabilizer state. + +Transitivity can also be seen directly: a basis change puts the support +on coordinate axes, a translation removes its offset, diagonal Clifford +phases remove its phase polynomial, and Hadamards send its uniform support +to zero. This argument does not use a counting formula for the Clifford +group. + +It follows that the absolute off-diagonal row sum of the f-fold tensor +Gram matrix of all these states is exactly + + S_(N,f) = sum_(k=1..N) A_(N,k) 2^(-kf/2). (6) + +An arbitrary subset has no larger row sum. This count concerns projective +states. Repeating scalar-phase copies would make a pointwise Gram singular. + +## 3. The Clifford first-overlap improvement + +Vectorize U/sqrt(D) to obtain its unit Choi state on 2n qubits. It is a +stabilizer state: the Bell state is a stabilizer state and Clifford action +on one half preserves that property. Projectively different matrices give +different projective Choi states. Formula (5), with N=2n, therefore bounds +their overlap counts. + +For k=1 the Clifford count is exactly + + B_(n,1) = 2(2^(2n)-1) = A_(2n,1)/2. (7) + +Here is a separate proof which retains the signs. Let S be the symplectic +Pauli action of U, and L=ker(S-I). In the Hermitian Pauli basis, conjugation +has trace |tr U|^2. Its contribution at a fixed label v is its sign epsilon(v). +On L these signs form a character: conjugation cancels the same Pauli +multiplication phase on both sides. Thus |tr U|^2 is either zero or +2^dim(L). + +For a fixed S, its projective Clifford lifts differ by the 2^(2n) Paulis. +They multiply the sign on L by every character of L, each with multiplicity +2^(2n-dim(L)). Therefore exactly 2^k lifts have nonzero trace when +rank(S-I)=k. Their normalized trace modulus is 2^(-k/2). + +A rank-one symplectic displacement is a transvection. Indeed, write +(S-I)x=ell(x)a for nonzero a. Symplecticity gives +ell(x) omega(a,y)+ell(y) omega(x,a)=0. Nondegeneracy then forces +ell(x)=omega(x,a) over F_2. Every nonzero a gives one such map. There are +2^(2n)-1 choices, and each has two nonzero-trace lifts. This proves (7). + +For clarity, a second count gives the same general upper bound without +Choi states. Put W=im(S-I), dim W=k. Then ker(S-I)=W-perp. The residual +form B((S-I)x,w)=omega(x,w) is well-defined, nonsingular and satisfies +B(u,v)+B(v,u)=omega(u,v). For fixed W there are at most +2^(k(k+1)/2) bilinear forms with this fixed symmetrization. Each nonsingular +one determines S uniquely: solve B((S-I)x,w)=omega(x,w) for every w in W. +There are [2n choose k]_2 possible W and 2^k nonzero-trace Pauli lifts. +Their product is exactly A_(2n,k). No equality is asserted for k>=2. + +The Choi and residual-form arguments are different derivations of the same +upper bound. The checks enumerate signed Pauli actions and literal Choi +vectors separately. + +## 4. Uniform rational row bounds + +Set d_k=product_(j=1..k)(2^j-1). The subspace count satisfies + + [N choose k]_2 <= 2^(k(N-k)) / + product_(j=1..k)(1-2^(-j)). + +At f=2N+4, its term in (6) is at most 1/d_k. The Clifford first term is +at most 1/2 by (7). Its whole off-diagonal row sum is consequently at most + + 1/2 + 1/3 + 1/21 + 1/315 + + (1/9765)/(1-1/63) < 8/9. (8) + +The tail starts at k=5. Each subsequent term has ratio at most 1/63. +The bound is independent of n. Terms with k>2n were added only to bound +the finite sum from above. At all larger widths the row sum can only fall. + +For all stabilizer states use f=2N+6. Each term is at most 2^(-k)/d_k, +so the full row sum is at most + + 1/2 + 1/12 + 1/168 + 1/5040 + + (1/312480)/(1-1/126) < 3/5. (9) + +Again this is a rational bound on the complete infinite tail. The executable +also provides the sharper finite sums for any specified axis count and any +even width. For an odd width it uses the preceding even width. A failed +sufficient bound is no decision, not evidence of linear dependence. + +If a Hermitian matrix has diagonal one and absolute off-diagonal row sums +at most s, then its eigenvalues lie in [1-s,1+s]. One direct proof bounds +each pair by 2|b_i b_j| <= |b_i|^2+|b_j|^2 in its quadratic form. +Apply this to the Gram matrices and (8)-(9). This proves (1)-(3). +Apply (1) to the residual with target coefficient one to obtain (4). +The inequality ||R||_HS <= sqrt(D^f)||R||_op gives its operator norm claim. + +There are useful stronger bounds at a slightly later width. At +f=4n+4+2s the Clifford row bound is at most + + 2^(-s-1) + sum_(k>=2) 2^(-sk)/d_k. (10) + +For s=2 this is <3/20. For s=6 it is <1/126. +Thus four consecutive widths starting at 4n+8 have a 17/20 lower bound; +four starting at 4n+16 have a 125/126 lower bound. The same geometric-tail +argument proves these constants. These are sufficient constants, not +optimal spectral values. + +## 5. Exact phases and the four-width theorem + +For the Gaussian-dyadic group write every exact matrix uniquely as i^j U_g, +where g is its projective class and j=0,1,2,3. For a fixed residual define + + beta_(g,r) = sum_(j=0..3) c_(g,j) i^(jr). + +At any f>=4n+4 with f=r modulo four, (1) says that the residual is zero +exactly when all beta_(g,r) vanish. This is the exact pointwise kernel: +only the unavoidable scalar-phase relations remain. Four consecutive +widths supply all four residues. Fourier inversion then makes every +c_(g,j) zero. + +Parseval gives (1/4) sum_(g,r)|beta_(g,r)|^2=M. Averaging (1) over the +four tested widths proves the M/9 claim. Formula (10) gives the two stronger +four-width constants stated above. Apply the argument to each entry of a +complete input-to-output register matrix; every dirty role must be retained. + +For each r the residual sum_(j=0..3) i^(-rj)[i^j I] vanishes at every width +outside r modulo four and is 4I in that residue. Thus three widths cannot +be a universal fixed-residual test. The same argument gives eight necessary +residues if a chosen finite normalized Clifford lift includes eighth-root +scalar phases. The four-test conclusion is for the repository's exact +Gaussian-dyadic group, not that larger central extension. + +## 6. Quantifiers, applications and exclusions + +At a single specified f>=4n+4, the coefficient vector may be chosen after +f. Its entries may be arbitrary complex numbers. Its finite support and +the finite word that produces it may also depend on f. There is no term +count in the theorem. Thus an equality at that width can be read as an +identity in the projective phase quotient of the group algebra. A scalar +phase is evaluated as its f-th power, not discarded. + +This gives an explicit threshold for future applications of the retained +finite-alphabet tensor-separation arguments. It replaces an unspecified +large width or a projective-group-size bound when the entire operator +alphabet in the argument is contained in this fixed n-axis Clifford group. +For n=9 the pointwise threshold is 40 and the four test widths are 40..43. +For n=17 they are 72 and 72..75. At n=64 they are 260 and 260..263. +The prior full-Clifford fixed-residual tests are 69..76, 133..140 and +509..516 respectively. These comparisons are theorem bounds, not measured +execution speedups. + +The [retained passive application](APPLICATION.md) meets the full alphabet +premise. It gives a uniform width-72 obstruction and an operator error bound +of 1/3 under that exact passive contract. Its sources and both mandatory +clarifications are retained as byte-pinned inputs. + +For stabilizer maps, terms which differ by any nonzero scalar must first be +combined with that scalar raised to f. Their coefficients may then depend +on f. Formula (3) does not identify scaled copies at all widths, and it does +not give four tests for arbitrary nonunitary scalings. + +This does not by itself strengthen an additional-call bound at a caller +cut with already paid observations. That needs its correct initial module, +source versions, ownership and cost ledger. Nor does it show that any +particular paid-history theorem's whole alphabet consists of Clifford +maps. A nominal matrix or a sum of Cliffords is not automatically a +Clifford or a stabilizer map. Each application must check that premise. + +Arbitrary non-Clifford matrices, nonlinear/rounded operations, operators +which act across tensor columns, unpriced physical routing, and omitted +dirty returns remain outside the result. No all-size multiplication +assumption is declared discharged by this algebraic theorem alone. + +## 7. Verification and attribution + +The registered verifier checks the finite counting identities by separate +state and signed-Pauli enumerations, the rational tail bounds, literal Gram +matrices, complete native register examples and deliberate invalid inputs. +The written proof supplies the all-dimension and all-width quantifiers. +Finite computation is corroboration; it is not a formal-kernel proof or +independent human acceptance. + +The retained tensor-Gram package supplies the exact native grammar, compact +quadratic sums and complete register frontend. Its original trace filter, +code invariant, one-axis sharpness and provider results remain its work. +The monomial tensor-cutoff package remains a stronger cutoff for its smaller +class. Chris R and the retained paid-history authors supply the earlier +finite-alphabet applications. Krzysztof Wojt and Nick Petalas supply the +repository's related residual-form and partial-Pauli statements. + +Classical stabilizer descriptions follow Dehaene and De Moor, +[*Clifford group, stabilizer states, and linear and quadratic operations +over GF(2)*](https://arxiv.org/abs/quant-ph/0304125). The finite symplectic residual-form +method is classical Wall-form theory. No general counting, Gram, Fourier, +stabilizer-simulation or literature-priority claim is made. Exact repository +pins and the role of each source are in SOURCES.json and README.md. + +## Open next questions + +Find the least pointwise threshold and best spectral constant for this +group, with the phase residue kept explicit. Test one actual complete +caller against the new pointwise kernel, retaining its available history +and complete bill. Extend the exact native frontend to a source-bound +nonunitary stabilizer caller only when its projections and scalar factors +are supplied. None of these follow-ups is claimed complete here. diff --git a/research/negative-e-decoder-gram-bound/source/decoder-proof.md b/research/negative-e-decoder-gram-bound/source/decoder-proof.md new file mode 100644 index 0000000000..bc945b4901 --- /dev/null +++ b/research/negative-e-decoder-gram-bound/source/decoder-proof.md @@ -0,0 +1,51 @@ +# The actual odd-E8 negative terminal has no constant-size ordinary decoder + +This is an application of the attributed fresh-stage path-separation and coordinate-contraction proof retained in `source/separation-proof.md` (Ali Romman, PR4933/5065 lineage), with a new nonzero-path certificate for the actual nonfitting E code of PR5464. The old A polynomial and proper-K terminal support cap are not premises. No new general separation theorem is claimed. + +## Exact target and source + +At immutable56ba6d7d609124d71c067d6a380caed573963f8f, the source has v=112^3 owners and three24-private-axis stages sharing one central binary axis. Let Q=C0, D123 the three fresh positive Gaussian products, and B=E3 E2^-1 E1. The emitted negative endpoint is Q^-1 B D123. Its specified target is Q^-1 D123 on the same original independent inputs. Since both maps are invertible, the unique postdecoder is J=Q^-1 B^-1 Q=Q^-1 E1^-1 E2 E3^-1 Q. This statement observes only the emitted negative bank plus independent workspace; no correlated original-input histories or other unpaid observations are granted. Independent extra inputs cannot change the required restriction to this bank. + +Each stage E is physically L^-1 A L with owner-block diagonal signed monomials L_i and scalar A=K(I-C)^-1. Only the address monomials tensor-power with field width f; scalar owner coefficients are applied once. The source has C spectrum0,98,-1078, KC=-C, and K^2=I. Therefore E^-1 in normalized owner coordinates is K+C. This uses the actual20480-mode nonfitting E construction, not the earlier proper-K code. + +## Actual nonzero path + +Put j=(0,0,0), i=(1,0,0). Source root rows are M0=(1,1,1,1,0,0,0,0), M1=(1,1,0,0,1,1,0,0). Their supports belong to different cubes and their dot product is2. Let P=MM^T/4, so P00=P11=1 and P10=1/2. The scalar source code is C=(P1P2+P1P3+P2P3-P1P2P3)/2. For i,j above its entry is P10/2=1/4. The block-diagonal K has zero entry between these different cubes, hence (E^-1)_ij=1/4. Every diagonal entry of K is0, so (E^-1)_jj=C_jj=1. + +The projector onto the8-dimensional active base space is MM^T/56; every diagonal entry equals1/14. For the three selector axes, the diagonal mass on exactly-two-active sectors is39/2744, and on the all-active sector1/2744. Since E=K-C(I-C)^-1 and K_jj=0, + E_jj=39*98/(2744*97)+1078/(2744*1079)=1541/104663. +Thus the path j→j→j→i in E1^-1 E2 E3^-1 has coefficient1541/418652, nonzero. All matrices and coefficients here are exact rational source data. There is no inference from the source's smaller lambda98 toy caller to this112^3-owner claim. + +## Path separation and nonmonomial support + +Let V_s be the24 private binary coordinates of stage s and E the common binary line. The linear normalizer G_s,i acts only on E+V_s and sends e0 to the distinct actual product label q_i. All product labels are distinct: concatenation of the three distinct112-label coordinates is injective, and conversion through the source orthonormal basis of U25 is injective. The source rule constructs G for every norm-one noncharacteristic q; signed phases do not identify different binary maps. + +Ordered products of one local map per distinct stage factor uniquely. Moving the last factors to one side puts their quotient both in GL(E+V_last) and in the subgroup supported on E plus earlier private spaces. Their intersection is GL(E,F2), which is trivial. Peel stages successively. With fixed endpoint owners, equal complete maps therefore imply equal intermediate owners, since G_i e0=q_i distinguishes owners. This is the existing separation lemma with24 private coordinates, not a census of owner paths. + +Consequently the selected nonzero path cannot cancel with another path, including after absolute phases. Its complete map reduces to L_i^-1 L_j in stage1, because the other two local factors are identity. Its binary map moves e0 since q_i differs from q_j. For M|x>=s(x)|Gx>, s(x)=+/-1, direct expansion of Q^-1 M Q has four distinct destinations Gx,Gx+Ge0,Gx+e0,Gx+Ge0+e0, each coefficient of magnitude1/2. Its inverse also moves e0, giving four entries in each row. The verifier checks the actual25-axis signed normalizers and exact sparse phase columns without constructing a2^25 dense matrix. + +## Quantified ordinary-cost consequence + +Use the existing private-basis contraction proof with m=72 private directions in the73-axis address space. For each private basis vector x_l set y_l=G_* x_l and ell_l(N)=(Q N Q^-1)[y_l,x_l]. Orthogonality means agreement on these72 columns forces agreement on the remaining central column. By path separation the markers isolate the selected path. For f>=72, contracting the first72 tensor factors leaves a nonzero scalar times N_*^(tensor(f-72)). Each resulting row has4^(f-72) nonzero entries. + +Each marker uses at most two original output rows and two input entries. If original maximum row support is S, the contracted row support is at most2^72 S. Therefore S>=2^(2f-216). A monomial address operation, SCALE, COPY or CLEAR does not increase maximum row support; a binary ADD increases it by at most two. Any exact linear ordinary program with g ADDs therefore satisfies + g>=max(0,2f-216). +This allows arbitrary owner mixing, arbitrary independent owned/dirty workspace and f-dependent scalar coefficients or monomial permutations. It rules out a fixed finite number of ordinary field ADDs uniformly in width. It does not rule out f-dependent scalar programs, paid Gaussian calls, correlated histories, repeated stages, changed target inventories or joint whole-caller decoders. The two-common-axis and repeated-stage controls explicitly exhibit failure of the separation premises outside scope. + +## Stronger eventual nonmembership for the columnwise native alphabet + +For this additional claim restrict each ordinary address operation to a tensor lift gamma^(tensor f) of a single73-bit-column monomial Clifford, as in the actual native P/D/X/phase alphabet. Owner mixing and scalar coefficients may depend on f, and there is no bound on instruction count. Products of such lifted monomials remain lifted monomials in the same finite group Gamma; sums, COPY, CLEAR and arbitrarily many independent workspace rows leave each original-input/output block in their scalar linear span. + +A monomial Clifford on n bits is a binary affine permutation (at most2^(n^2+n) choices) times a diagonal phase i^(c+sum a_j x_j+2sum b_jk x_j x_k), with c,a_j in Z4 and b_jk in F2. Arbitrary scalar global phases may be absorbed into the owner coefficients, so no continuous scalar phase group is counted. For the native Z4 representatives, |Gamma|<=2^(n^2+3n+n(n-1)/2+2). At n=73 the exponent is8178. Every lifted monomial has only one nonzero entry in each row, so every block in this span has row support at most2^8178. The selected owner block of J_f has support at least2^(2f-216); the contraction argument already fixes both owner endpoints. Hence J_f lies outside the entire ordinary columnwise Clifford algebra for every f>=4198. This excludes arbitrary-length f-dependent words in that alphabet, not only a constant instruction count. Multiplication by fixed ordinary invertible owner/monomial boundaries cannot change membership. + +If a broader alphabet permits arbitrary one-column permutations or arbitrary phases, but still repeats the same one-column permutation across all f columns, a weaker support-only bound remains: for d=2^73 possible one-column addresses, at most d! repeated permutations give different support maps. Phases cannot enlarge those supports. Since d!<=d^d, eventual nonmembership follows whenever2f-216>73*2^73. This broader bound does not need a finite phase set. Neither argument applies to arbitrary permutations mixing tensor columns; those retain only the ADD-count lower bound above. This distinction is essential to the claimed ordinary-algebra decision. + +## Complete invoice decision and remaining costs + +The unchanged three-call producer pays3v each of H8,H9,H15,H16 plus61440 H25. The positive half is already decoded. Granting a second autonomous H73 half leaves the source's conditional margin about.0438207413 per port per LOCAL at selected saving. Our result rejects treating the missing specified postdecoder as a fixed-size ordinary recoding. It additionally proves eventual nonmembership in the full columnwise native algebra, but supplies no paid-child lower bound and must not be subtracted as one from that margin. + +A scalar decoder growing with f must charge every ADD, route, coefficient-generation division, owned lifetime, precision guard and visited-cell cost against the complete caller. A paid decoder must retain all original-input targets and pay its children before claiming that conditional margin. No such completion is constructed here. The producer's20480 modes, source-contact histories, scalar rational denominators and field-l2/coordinatewise precision gap remain inherited open costs. No selected-frontier change or kappa claim follows. + +## Open next questions + +Can an already-paid IDLE or a charged f-dependent ordinary program implement J within the complete remaining budget? Can a genuinely different target or correlated-history contract remove the required conjugated inverse? First write the complete source/caller identity and invoice; do not repeat the failed naive B^-1 postdecoder or apply the proper-K support cap to E. diff --git a/research/negative-e-decoder-gram-bound/source/decoder-result.json b/research/negative-e-decoder-gram-bound/source/decoder-result.json new file mode 100644 index 0000000000..0813bbb062 --- /dev/null +++ b/research/negative-e-decoder-gram-bound/source/decoder-result.json @@ -0,0 +1,97 @@ +{ + "columnwise_group_log2_upper": 8178, + "columnwise_nonmembership_from_f": 4198, + "owner_input": [ + 0, + 0, + 0 + ], + "owner_output": [ + 1, + 0, + 0 + ], + "middle_owners": [ + [ + 0, + 0, + 0 + ], + [ + 0, + 0, + 0 + ] + ], + "E_inverse_cross_entry": "1/4", + "E_diagonal": "1541/104663", + "E_inverse_diagonal": "1", + "surviving_coefficient": "1541/418652", + "product_labels": [ + 657939, + 657931 + ], + "selected_permutation_columns": [ + 657934, + 657933, + 657931, + 16, + 657927, + 32, + 64, + 128, + 256, + 657423, + 1024, + 655887, + 4096, + 8192, + 16384, + 32768, + 65536, + 526863, + 262144, + 133647, + 1048576, + 2097152, + 4194304, + 8388608, + 16777216 + ], + "selected_sign": 657943, + "conjugated_zero_column": [ + [ + 0, + [ + "1/2", + "0" + ] + ], + [ + 1, + [ + "0", + "1/2" + ] + ], + [ + 657934, + [ + "0", + "1/2" + ] + ], + [ + 657935, + [ + "-1/2", + "0" + ] + ] + ], + "ambient_axes": 73, + "private_markers": 72, + "ADD_lower_bound": "max(0,2*f-216)", + "target": "Q^-1 D123 on original independent negative-bank inputs", + "scope": "postdecoder from emitted bank and independent workspace; no correlated retained histories" +} diff --git a/research/negative-e-decoder-gram-bound/verify.py b/research/negative-e-decoder-gram-bound/verify.py new file mode 100644 index 0000000000..a5bee07779 --- /dev/null +++ b/research/negative-e-decoder-gram-bound/verify.py @@ -0,0 +1,188 @@ +#!/usr/bin/env python3 +"""Check the source-bound negative E decoder application. + +Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. +""" +from fractions import Fraction as F +from pathlib import Path +import hashlib +import json + +ROOT = Path(__file__).resolve().parent +ZERO = (F(0), F(0)) +ONE = (F(1), F(0)) +A, B = (F(1, 2), F(1, 2)), (F(1, 2), F(-1, 2)) + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def plus(a, b): + return a[0] + b[0], a[1] + b[1] + + +def times(a, b): + return a[0] * b[0] - a[1] * b[1], a[0] * b[1] + a[1] * b[0] + + +def norm2(a): + return a[0] ** 2 + a[1] ** 2 + + +def q_apply(state, inverse=False): + a, b = (B, A) if inverse else (A, B) + out = {} + for x, value in state.items(): + for y, factor in ((x, a), (x ^ 1, b)): + out[y] = plus(out.get(y, ZERO), times(value, factor)) + return {x: value for x, value in out.items() if value != ZERO} + + +def binary_rank(vectors): + pivots = {} + for x in vectors: + while x: + bit = x.bit_length() - 1 + if bit in pivots: + x ^= pivots[bit] + else: + pivots[bit] = x + break + return len(pivots) + + +def native_apply(state, columns, sign): + out = {} + for x, value in state.items(): + y = x & ~((1 << len(columns)) - 1) + for j, column in enumerate(columns): + if x >> j & 1: + y ^= column + factor = -1 if (x & sign).bit_count() % 2 else 1 + out[y] = (value[0] * factor, value[1] * factor) + return out + + +def read_inputs(): + for entry in json.loads(ROOT.joinpath('INPUTS.json').read_text()): + data = ROOT.joinpath(entry['path']).read_bytes() + require(hashlib.sha256(data).hexdigest() == entry['sha256'], 'source SHA256') + blob = hashlib.sha1(b'blob ' + str(len(data)).encode() + b'\0' + data).hexdigest() + require(blob == entry['git_blob'], 'source Git object') + return json.loads(ROOT.joinpath('source/decoder-result.json').read_text()) + + +def validate_data(data): + require(type(data['ambient_axes']) is int and data['ambient_axes'] == 73, 'ambient axes') + require(data['owner_input'] == [0, 0, 0] and data['owner_output'] == [1, 0, 0], 'owner endpoints') + r0, r1 = (1, 1, 1, 1, 0, 0, 0, 0), (1, 1, 0, 0, 1, 1, 0, 0) + cross = F(sum(x * y for x, y in zip(r0, r1)), 8) + active = F(8, 112) + middle = 3 * active ** 2 * (1 - active) * F(98, 97) + active ** 3 * F(1078, 1079) + coefficient = cross * middle + require(cross == F(data['E_inverse_cross_entry']) == F(1, 4), 'actual cross coefficient') + require(middle == F(data['E_diagonal']) == F(1541, 104663), 'actual middle coefficient') + require(F(data['E_inverse_diagonal']) == 1, 'actual diagonal inverse') + require(coefficient == F(data['surviving_coefficient']) == F(1541, 418652), 'path coefficient') + columns = data['selected_permutation_columns'] + require(len(columns) == 25 and binary_rank(columns) == 25, 'invertible local map') + require(all(type(x) is int and 0 < x < 1 << 25 for x in columns), 'local columns') + require(columns[0] != 1, 'central axis must move') + sign = data['selected_sign'] + require(type(sign) is int and 0 <= sign < 1 << 25, 'native sign') + got = q_apply(native_apply(q_apply({0: ONE}), columns, sign), True) + expected = {x: tuple(F(v) for v in value) for x, value in data['conjugated_zero_column']} + require(got == expected and len(got) == 4 and all(norm2(z) == F(1, 4) for z in got.values()), 'actual sparse column') + return coefficient, columns, sign + + +def row_bound(n, width): + require(n >= 1 and width >= 4 * n + 4, 'unproved width') + width -= width % 2 + N, gaussian, total = 2 * n, 1, F(0) + for k in range(1, N + 1): + numerator = gaussian * ((1 << (N - k + 1)) - 1) + denominator = (1 << k) - 1 + require(numerator % denominator == 0, 'Gaussian binomial integrality') + gaussian = numerator // denominator + count = 2 * ((1 << N) - 1) if k == 1 else gaussian * (1 << (k * (k + 3) // 2)) + total += F(count, 1 << (k * width // 2)) + return total + + +def infinite_bound(shift): + d, total = 1, F(1, 1 << (shift + 1)) + for k in range(1, 6): + d *= (1 << k) - 1 + if 2 <= k <= 4: + total += F(1, (1 << (shift * k)) * d) + total += F(1, (1 << (5 * shift)) * d) / (1 - F(1, 63 * (1 << shift))) + return total + + +def controls(data): + rejected = 0 + mutations = [('ambient_axes', True), ('surviving_coefficient', '1/4'), ('E_diagonal', '98'), + ('selected_sign', data['selected_sign'] ^ 1), ('owner_output', [0, 0, 0])] + for key, value in mutations: + altered = {**data, key: value} + try: + validate_data(altered) + except ValueError: + rejected += 1 + else: + raise ValueError('changed source field accepted') + try: + row_bound(73, 295) + except ValueError: + rejected += 1 + else: + raise ValueError('unproved width accepted') + require(F(data['surviving_coefficient']) ** 2 != F(data['surviving_coefficient']), 'external scalar is not tensorized') + rejected += 1 + # Two phase copies can cancel. The source uniqueness premise excludes this case. + require(1 + (-1) ** 1 == 0 and 1 + (-1) ** 2 == 2, 'projective phase merging') + rejected += 1 + raw = ROOT.joinpath('source/decoder-result.json').read_bytes() + require(hashlib.sha256(raw + b' ').hexdigest() != hashlib.sha256(raw).hexdigest(), 'source corruption control') + return rejected + 1 + + +def main(): + data = read_inputs() + coefficient, columns, sign = validate_data(data) + for x in (0, 1): + before = q_apply({x: ONE}, True) + shifted = {y ^ 1: z for y, z in before.items()} + signed = {y: ((-1) ** (y & 1) * z[0], (-1) ** (y & 1) * z[1]) for y, z in before.items()} + require(q_apply(shifted) == {x ^ 1: ONE}, 'Q X Q inverse') + require(q_apply(signed) == {x ^ 1: (F(0), F(-1 if x == 0 else 1))}, 'Q Z Q inverse') + addresses = [0] + [1 << j for j in range(73)] + [(1 << j) | (1 << ((j + 7) % 73)) for j in range(73)] + for x in addresses: + require(q_apply(q_apply({x: ONE}), True) == {x: ONE}, 'unitary Q inverse') + require(q_apply(q_apply({x: ONE})) == {x ^ 1: ONE}, 'Q squared is X') + result = q_apply(native_apply(q_apply({x: ONE}), columns, sign), True) + require(len(result) == 4 and sum(norm2(z) for z in result.values()) == 1, 'nonmonomial unit column') + bounds = 0 + for n in (1, 2, 3, 9, 17, 73): + for shift, cap in ((0, F(8, 9)), (2, F(3, 20)), (6, F(1, 126))): + uniform = infinite_bound(shift) + require(uniform < cap, 'complete infinite tail') + for parity in (0, 1): + actual = row_bound(n, 4 * n + 4 + 2 * shift + parity) + require(actual <= uniform, 'finite count versus dimension-uniform row bound') + bounds += 1 + require(4 * 73 + 4 == 296 and coefficient / 3 == F(1541, 1255956), 'application threshold and norm floor') + require(2 * 4198 - 216 > 8178 and 2 * 4197 - 216 == 8178, 'credited old support threshold') + print('PASS_NEGATIVE_E_DECODER_GRAM_BOUND ' + json.dumps(dict(source_files=3, + sparse_columns=len(addresses),clifford_generator_checks=4,finite_gram_bounds=bounds,controls=controls(data), + axes=73,old_support_threshold=4198,new_threshold=296, + path_coefficient=str(coefficient),operator_error_floor=str(coefficient / 3), + normalized_squared_error_floor=str(coefficient ** 2 / 9), + stronger_squared_floor_from_308=str(F(125, 126) * coefficient ** 2)), sort_keys=True)) + + +if __name__ == '__main__': + main()