From fcede4106b9f175d2060f41a4feb4eca2b1acbad Mon Sep 17 00:00:00 2001 From: ToikY <27568617+ToikY@users.noreply.github.com> Date: Fri, 6 Nov 2026 16:53:05 -0800 Subject: [PATCH] research: tighten Clifford conditioning with an order-three trace --- research/clifford-order3-conditioning/LICENSE | 201 + research/clifford-order3-conditioning/NOTICE | 20 + .../clifford-order3-conditioning/PROOF.md | 403 ++ .../clifford-order3-conditioning/README.md | 127 + .../clifford-order3-conditioning/RESULT.json | 2524 +++++++++ .../SOURCE-PINS.json | 60 + .../clifford-order3-conditioning/SOURCES.json | 24 + .../clifford-order3-conditioning/TASK.json | 127 + .../clifford-order3-conditioning/VERIFY.json | 28 + .../predecessor/PR6714-PROOF.md | 430 ++ .../predecessor/PR6794-PROOF.md | 178 + .../source/EXTERNAL.json | 31 + .../source/table.json | 4649 +++++++++++++++++ .../source/width-nine-input.json | 494 ++ .../clifford-order3-conditioning/verify.py | 542 ++ 15 files changed, 9838 insertions(+) create mode 100644 research/clifford-order3-conditioning/LICENSE create mode 100644 research/clifford-order3-conditioning/NOTICE create mode 100644 research/clifford-order3-conditioning/PROOF.md create mode 100644 research/clifford-order3-conditioning/README.md create mode 100644 research/clifford-order3-conditioning/RESULT.json create mode 100644 research/clifford-order3-conditioning/SOURCE-PINS.json create mode 100644 research/clifford-order3-conditioning/SOURCES.json create mode 100644 research/clifford-order3-conditioning/TASK.json create mode 100644 research/clifford-order3-conditioning/VERIFY.json create mode 100644 research/clifford-order3-conditioning/predecessor/PR6714-PROOF.md create mode 100644 research/clifford-order3-conditioning/predecessor/PR6794-PROOF.md create mode 100644 research/clifford-order3-conditioning/source/EXTERNAL.json create mode 100644 research/clifford-order3-conditioning/source/table.json create mode 100644 research/clifford-order3-conditioning/source/width-nine-input.json create mode 100644 research/clifford-order3-conditioning/verify.py diff --git a/research/clifford-order3-conditioning/LICENSE b/research/clifford-order3-conditioning/LICENSE new file mode 100644 index 0000000000..261eeb9e9f --- /dev/null +++ b/research/clifford-order3-conditioning/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/clifford-order3-conditioning/NOTICE b/research/clifford-order3-conditioning/NOTICE new file mode 100644 index 0000000000..9b9a065332 --- /dev/null +++ b/research/clifford-order3-conditioning/NOTICE @@ -0,0 +1,20 @@ +Prepared for ToikY with substantial source-aware OpenAI Codex assistance. +New proof/certificate code and text: Apache-2.0, repository LICENSE included. + +Retained exact predecessor proof prose: Nick Petalas, PR6794, +clifford-transvection-conditioning, headc6252da020819a08ef2b2ff14280146c43ad374c; +alephnan, PR6714, clifford-three-qubit-threshold, +headf7f32a18dde54e67624a9ed9cc7e1b266d9585c0. Original notices in those files +are retained verbatim. Source inputs/assumptions and excluded prior results +are described in README.md/PROOF.md and SOURCE-PINS.json. + +Retained numerical mathematical table and multiplicity facts are credited to +the predecessor packages and to Chin-Yen Lee, Wei-Hsuan Yu, Yung-Ning Peng +and Ching-Jui Lai, On character table of Clifford groups, arXiv2309.14850v2, +https://arxiv.org/html/2309.14850v2 . The article's own CC BY-NC-ND4.0 license +is linked on that page; article prose and figures are not redistributed here. +The published group/table identification remains a cited mathematical input. + +Retain Ali Romman/MatShep and all authors/notices cited by the predecessor +sources. Own earlier PR6718 review is excluded from the new contribution. +Classical representation/quadratic-form/convexity methods are credited in PROOF. diff --git a/research/clifford-order3-conditioning/PROOF.md b/research/clifford-order3-conditioning/PROOF.md new file mode 100644 index 0000000000..e7985044d5 --- /dev/null +++ b/research/clifford-order3-conditioning/PROOF.md @@ -0,0 +1,403 @@ +# An order-three constraint for three-qubit Clifford conditioning + +## 1. Claim, premises, and attribution + +This note adds an order-three character constraint to the transvection +relaxation of [PR6794](https://github.com/CrocSwap/integer-mult-bounds/pull/6794). +Together with the retained exact thirty-row certificate it proves, for the +source's normalized character-power Gram matrices and every $f\geq10$, +\[ + \frac{405}{16384}I\preceq H_f + \preceq\frac{1334151}{131072}I,\qquad + \operatorname{cond}(H_f)\leq\frac{16471}{40}=411.775<807. +\] +This is a sufficient bound, improving the credited 807 certificate. It is +not the actual Gram spectrum or exact condition number. The width threshold +remains ten, and no multiplication-frontier change is asserted. + +Use the finite Gaussian-dyadic Clifford group and notation of +[PR6714, proof at its pinned head](https://github.com/alephnan/integer-mult-bounds/blob/f7f32a18dde54e67624a9ed9cc7e1b266d9585c0/research/clifford-three-qubit-threshold/PROOF.md): + +* $V=\mathbb C^8$ is the natural representation, $z=iI_8$, and + $P\triangleleft G$ is the three-qubit Pauli group. +* $G/P=S=\operatorname{Sp}(6,2)$, while the projective alphabet has size + $M=|G/\langle z\rangle|=92897280$. +* Every relevant irreducible $\mu$ with $\mu(z)=-I$ restricts to one + quadratic-form orbit of $P$, of size $N=36$ or $28$, each character + occurring with the same multiplicity $a\geq1$. Thus $d_\mu=Na$. + The orbit sizes correspond respectively to Arf invariant zero and one. +* The odd-central-sector irreducibles are the honest representations + $V\otimes\sigma$, for the thirty irreducibles $\sigma$ of $S$. + Write $d_\sigma=\dim\sigma$, and let $m_\sigma$ be their multiplicities + in $V^{\otimes9}$. For nonnegative integers $n_\sigma$, + \[ + \overline V\otimes\mu + =\bigoplus_\sigma n_\sigma(V\otimes\sigma),\qquad + d_\mu=\sum_\sigma n_\sigma d_\sigma,\qquad + m_{\mu,10}=\sum_\sigma n_\sigma m_\sigma. \tag{1} + \] +* For a transvection $t\in S$, with $t_\sigma=\chi_\sigma(t)$, the + inherited bound from PR6794 is + \[ + \left|\sum_\sigma n_\sigma t_\sigma\right|\leq16a. \tag{2} + \] + +These representation and width-nine multiplicity statements, the published +table identification, and the later-width Gram propagation are inherited +premises. They are not re-established by reading their retained numerical +data. The source byte pins identify the exact versions used. + +Credit for the three-qubit threshold, quadratic-form description, and +width-nine decomposition belongs to alephnan's PR6714, using the published +Clifford character table of Chin-Yen Lee, Wei-Hsuan Yu, Yung-Ning Peng, and +Ching-Jui Lai. Credit for the transvection relaxation and its certified +807 bound belongs to Nick Petalas's PR6794 at head +`c6252da020819a08ef2b2ff14280146c43ad374c`. Classical finite-group character +theory supplies the reciprocity and trace principles used below. Our earlier +PR6718 reviewed parts of PR6714's argument; it is not a fresh table +identification or multiplicity computation. + +The new written lemma is that for the order-three quotient element $s$ +specified below, and $c_\sigma=\chi_\sigma(s)$, +\[ + \frac{\operatorname{Re}\sum_\sigma n_\sigma c_\sigma}{d_\mu} + \in + \begin{cases} + [-3/36,\;6/36],&N=36,\\ + [-5/28,\;10/28],&N=28. + \end{cases} \tag{3} +\] +The selected quotient column is real, so the real-part notation can be +omitted after that inherited table binding has been made. We do not assume +that each individual fixed multiplicity-space trace is real. + +## 2. A lift with exact phase + +On one qubit set +\[ + h=\frac{1+i}{2}\begin{pmatrix}1&1\\1&-1\end{pmatrix}, + \qquad S_0=\begin{pmatrix}1&0\\0&i\end{pmatrix}, + \qquad A=hS_0, + \qquad g=A\otimes I_4. \tag{4} +\] +The entries lie in $\mathbb Z[i,1/2]$. Since +$\left|(1+i)/2\right|^2=1/2$, the two real Hadamard rows have squared +norm two, and $S_0$ is unitary, both $A$ and $g$ are unitary. + +Put $b=(1+i)/2$. Then +\[ + A=b\begin{pmatrix}1&i\\1&-i\end{pmatrix},\qquad + \operatorname{tr}A=b(1-i)=1,\qquad + \det A=b^2(-2i)=1. +\] +Its characteristic equation gives +\[ + A^2-A+I_2=0,\qquad A^3=-I_2. +\] +Consequently +\[ + \operatorname{tr}_V g=4,\qquad g^3=-I_8=z^2. \tag{5} +\] +This is an equality of actual Gaussian-dyadic operators; no projective phase +has been discarded. + +For the usual Hermitian Pauli matrices $X,Y,Z$, direct conjugation gives +\[ + AXA^*=-Y,\qquad AYA^*=-Z,\qquad AZA^*=X. \tag{6} +\] +For example $S_0XS_0^*=Y$, $hYh^*=-Y$, and the other two identities +follow in the same way. Thus $g$ normalizes the Pauli group and belongs to +the source group $G$. On Pauli labels in its first symplectic plane its +quotient action is +\[ + (x_1,y_1)\longmapsto(x_1+y_1,x_1), \tag{7} +\] +and it is the identity on the other four label coordinates. This quotient +element $s\in S$ has order exactly three: it cycles the three nonzero +vectors of that plane. Its fixed space has dimension four. + +As a hand check of the class size, there are +$63\cdot32/6=336$ nondegenerate symplectic two-planes in a six-dimensional +space over $\mathbb F_2$. Indeed, choose a nonzero first basis vector in +63 ways and its symplectic partner in 32 ways, and divide by the six ordered +symplectic bases of a two-plane. On each such plane there are two order-three +elements, acting as the identity on its orthogonal complement. They are +conjugate under the symplectic group, including interchange of the two +orientations inside the plane. The plane is recovered as +$\operatorname{im}(s-I)$, so there is no overcount. The class size is +therefore $336\cdot2=672$. + +To associate this class with an actual character column, use PR6714's +inherited *complete* thirty-class quotient catalogue and its published-table +identification. Its retained thirty-entry quotient-class-size list contains +**672 exactly once**, at quotient fibre **5**. Since the hand calculation +above proves that our $s$ has class size 672, completeness and uniqueness in +that catalogue identify its class with fibre 5. This is an inference from +both the computed class size and the inherited complete catalogue; class +size alone, without that uniqueness premise, would not suffice. Fibre 5 +comprises published projective classes **9 and 10**, and its retained fixed +dimension **4** also agrees with (7). Both projective classes give the same +inflated quotient-character column. Use that column for every $c_\sigma$ +below. The completeness, size list, source-class association, and thirty-row +ordering remain cited source data rather than a rebuilt character table. + +## 3. Exactly six or ten fixed Pauli characters + +For $\mu(z)=-I$, one has $\mu(-I)=\mu(z^2)=I$. The restriction to $P$ +therefore factors through its abelianization. In the source convention its +one-dimensional characters are indexed by quadratic forms +\[ + Q_{\alpha,\beta}(x,y)=x\cdot y+\alpha\cdot x+\beta\cdot y, + \qquad \alpha,\beta\in\mathbb F_2^3, \tag{8} +\] +with Arf invariant $\alpha\cdot\beta$. For the Hermitian Pauli representative +$W_{x,y}=i^{x\cdot y}X^xZ^y$, the character is +$\lambda_Q(W_{x,y})=(-1)^{Q(x,y)}$. Its value on the central generator +is separately fixed as $\lambda_Q(z)=-1$. + +Conjugation by $g$ sends each $W_v$ to $\pm W_{sv}$. The sign is +invisible to these characters because their value on $-I$ is one. Thus +the action on $Q$ is ordinary quadratic pullback. Whether one writes the +pullback by $s$ or by $s^{-1}$ does not change its fixed forms. + +Apply (7) to the first summand of (8). Its transformed expression is +\[ + x_1y_1+(1+\alpha_1+\beta_1)x_1+\alpha_1y_1. +\] +Equality with +$x_1y_1+\alpha_1x_1+\beta_1y_1$ for every $x_1,y_1$ is equivalent to +\[ + \alpha_1=\beta_1=1. \tag{9} +\] +The other four parameters are free. The total Arf invariant is now +\[ + 1+\alpha_2\beta_2+\alpha_3\beta_3. +\] +Among pairs $(\alpha',\beta')\in\mathbb F_2^2\times\mathbb F_2^2$, +ten have dot product zero and six have dot product one: if $\alpha'=0$ +there are four zero-dot-product choices; for each of the other three +$\alpha'$, exactly two of the four $\beta'$ have each dot product. +Therefore the fixed-form counts in the two source orbits are +\[ + f_{36}=6,\qquad f_{28}=10. \tag{10} +\] +This calculation uses all sixteen fixed forms, with the source's actual +Arf-orbit convention; it does not replace either orbit by its size alone. + +## 4. An order-three trace bound on each fixed space + +By the inherited restriction statement, +\[ + V_\mu=\bigoplus_{Q\in\mathcal O_N} E_Q, + \qquad \dim E_Q=a. +\] +The operator $\mu(g)$ permutes these summands. A nonfixed summand contributes +zero to the trace, because its diagonal block in this decomposition is zero. +If $Q$ is fixed, $\mu(g)|_{E_Q}$ has cube $I$, by (5) and +$\mu(-I)=I$. A finite-group representation can be unitarized, or simply +one can use that $X^3-1$ has distinct roots over $\mathbb C$. Its +eigenvalues belong to $\{1,\omega,\omega^2\}$, where +$\omega=e^{2\pi i/3}$. Each eigenvalue has real part either one or +minus one half. Hence +\[ + -\frac a2\leq + \operatorname{Re}\operatorname{tr}(\mu(g)|_{E_Q}) + \leq a. +\] +Summing the fixed summands proves +\[ + -\frac{f_Na}{2}\leq + \operatorname{Re}\chi_\mu(g)\leq f_Na. \tag{11} +\] +There is no assertion that the extreme multiplicity-space eigenvalue +patterns occur in actual irreducibles. Equation (11) is a necessary bound, +not an actual-spectrum endpoint statement. + +## 5. Exact cancellation in the character identity + +Evaluate (1) at the actual lift $g$. The left side is +$\overline{\operatorname{tr}_V g}\,\chi_\mu(g)$. On the right, every +inflated $\sigma$ has character $\chi_\sigma(s)$, so +\[ + \overline{\operatorname{tr}_V g}\,\chi_\mu(g) + =\operatorname{tr}_V g + \sum_\sigma n_\sigma\chi_\sigma(s). +\] +By (5), both natural-character factors are the same real nonzero number +four. Thus the cancellation has phase exactly one: +\[ + T_3:=\sum_\sigma n_\sigma c_\sigma + =\chi_\mu(g). \tag{12} +\] +In particular, no unit-modulus phase needs to be bounded or chosen. Combining +(10)--(12) and dividing by $d_\mu=Na$ proves (3). The retained quotient +column consists of real integers, so $T_3$ is real in this application. + +## 6. The two-trace relaxation and exact certificate + +For an actual $\mu$ define +\[ + x_\sigma=\frac{n_\sigma d_\sigma}{d_\mu},\quad + r_\sigma=\frac{m_\sigma}{d_\sigma},\quad + u_\sigma=\frac{t_\sigma}{d_\sigma},\quad + v_\sigma=\frac{c_\sigma}{d_\sigma}. +\] +Then $x_\sigma\geq0$, $\sum x_\sigma=1$, and (1) gives +\[ + \frac{m_{\mu,10}}{d_\mu}=\sum_\sigma x_\sigma r_\sigma. +\] +For each $N\in\{28,36\}$, actual irreducibles therefore give feasible +points of the rational polytope +\[ + \begin{split} + x_\sigma&\geq0,\qquad\sum x_\sigma=1,\\ + -16/N&\leq\sum x_\sigma u_\sigma\leq16/N,\\ + -f_N/(2N)&\leq\sum x_\sigma v_\sigma\leq f_N/N. + \end{split} \tag{13} +\] +This remains a relaxation: integrality of the $n_\sigma$, actual branching +rules, and all other irreducible character constraints have been discarded. +The bounds need not be attained by actual $\mu$. + +A checked rowwise affine bound +\[ + m_\sigma\geq A d_\sigma+B t_\sigma+C c_\sigma + \quad\hbox{for every one of the thirty rows} +\] +gives +$m_{\mu,10}/d_\mu\geq A+B\tau+C\gamma$, where +$\tau=\sum x_\sigma u_\sigma$ and +$\gamma=\sum x_\sigma v_\sigma$. Minimizing this affine expression over +the rectangle in (13) is an exact rational lower certificate. Reversing the +rowwise inequality and maximizing gives an upper certificate. Feasible +mixtures with matching objectives additionally certify sharpness of the +*relaxation*. Those are sufficient certificate obligations; numerical +optimization output without the row and feasibility checks is insufficient. + +The retained exact certificate checks nonnegative residuals on all thirty +source rows for each of these three integer inequalities: +\[ + \begin{split} + 21m_\sigma-16d_\sigma+28c_\sigma&\geq0,\\ + 5m_\sigma-19d_\sigma+84c_\sigma&\geq0,\\ + 1007d_\sigma+7063c_\sigma-30m_\sigma&\geq0. + \end{split} \tag{14} +\] +The verifier stores all thirty exact rational residuals for each displayed +supporting plane; multiplication by its positive denominator yields the +corresponding integer inequality above. These are finite checks of the +inherited character/multiplicity input, not a new reconstruction of it. + +For $N=28$, the first inequality gives +\[ + \frac{m_{\mu,10}}{d_\mu} + \geq\frac{16}{21}-\frac43\gamma + \geq\frac{16}{21}-\frac43\frac5{14}=\frac27. +\] +For $N=36$, the second gives +\[ + \frac{m_{\mu,10}}{d_\mu} + \geq\frac{19}{5}-\frac{84}{5}\gamma + \geq\frac{19}{5}-\frac{84}{5}\frac16=1. +\] +The third supplies the upper bound +$1007/30+(7063/30)\gamma$. Its coefficient of $\gamma$ is positive, +so the upper endpoint of the order-three slab applies. The resulting +per-orbit intervals are +\[ + \frac{m_{\mu,10}}{d_\mu}\in + \begin{cases} + [\,2/7,\;2353/20\,],&N=28,\\ + [\,1,\;2621/36\,],&N=36. + \end{cases} \tag{15} +\] +Both lower supporting planes have negative $\gamma$ coefficient and +likewise use that same upper slab endpoint. All four displayed dual +certificates have transvection coefficient zero. + +Here are feasible matching primal mixtures from the retained packet. +Row numbers refer to the **published table's original row indices**, as +in the source's thirty-row list, not a newly numbered list. Weights are +the normalized simplex variables $x_\sigma$, not the integers +$n_\sigma$ of an asserted actual irreducible. + +| $N$ | Extremum | Nonzero row weights | $\tau$ | $\gamma$ | Objective | +| --- | --- | --- | --- | --- | --- | +| 28 | Minimum | row 2: $3/7$; row 9: $4/7$ | $-27/49$ | $5/14$ | $2/7$ | +| 28 | Maximum | row 1: $2/5$; row 13: $3/5$ | $3/7$ | $5/14$ | $2353/20$ | +| 36 | Minimum | row 9: $8/9$; row 12: $1/9$ | $-25/63$ | $1/6$ | $1$ | +| 36 | Maximum | row 1: $2/9$; row 13: $7/9$ | $7/27$ | $1/6$ | $2621/36$ | + +Each mixture has nonnegative weights summing to one, satisfies both +moment slabs, and meets its supporting plane with equality. In +particular, its transvection moment is strictly inside the transvection +slab. The bounds are therefore exact optima of (13). In fact the +order-three *upper* trace constraint, together with the simplex and source +row data, already yields these same extrema: the duals need no +transvection term and the matching primals remain feasible. This does not +make them actual irreducible or spectral endpoints. + +For completeness, the generic finite vertex check covers support sizes +one, two, and three. A vertex with $s$ positive weights needs $s-1$ +independent active moment equations after normalization; only two moment +coordinates are available, so $s\leq3$. Support-two vertices are obtained +by intersecting pairs with each slab boundary. Support-three vertices +require one boundary from each coordinate and a nonsingular three-column +system; degenerate supports reduce to smaller ones. All candidates are +then checked against both slabs and positivity. The retained run records +84 distinct vertices for $N=28$ (28 single-support and 56 two-support), +and 168 for $N=36$ (24 single-support and 144 two-support), with no +positive three-support vertices. These are finite fixed-input outputs, +not a claim about all possible character polytopes. The rowwise duals +and matching primals above independently suffice to certify (15). + +Taking the union of the two possible orbit types gives +\[ + \frac27\leq \frac{m_{\mu,10}}{d_\mu}\leq\frac{2353}{20}. +\] +The inherited Gram-eigenvalue scale is +$M/8^{10}=2835/32768$. Hence +\[ + \frac{405}{16384}I\preceq H_{10} + \preceq\frac{1334151}{131072}I. \tag{16} +\] +The inherited Schur-product relation +$H_{j+1}=H_j\circ H_1$, with $H_1\succeq0$ and diagonal one, +preserves (16) for every $j\geq10$: multiply each PSD difference +entrywise by $H_1$, and use $I\circ H_1=I$. Finally, the ratio of the +upper and lower bounds is +\[ + \frac{2353/20}{\,2/7\,} + =\frac{16471}{40}=411.775<807. \tag{17} +\] +This improves a sufficient uniform conditioning bound. It does not +assert equality for the condition number, change the already proved +width threshold, or remove any inherited representation or Gram premise. + +## 7. Evidence and limits + +The derivation above is written, source-aware mathematics. The proposed lift +and target bounds were supplied in the coordinator's preclaim recipe, and +the author had prior exposure to PR6714, PR6794, and PR6718. It is not a blind +derivation, a human review, or a formal-kernel certificate. No original +source checker, tensor constructor, table reconstruction, numerical LP, +matrix experiment, or spectral computation was executed by this proof role. +Any separately reported program evidence must retain its own exact scope. + +The numerical completion of section 6 was made only after the coordinator +preserved and ran the sealed new verifier once in its explicit generation +mode, and retained its complete successful packet. This proof role read +that existing packet without rerunning any engine. The packet's source +authentication, actual Gaussian lift/Pauli/form calculations, rational +primal/dual residuals, and six discriminating controls are finite evidence +with their own receipts. Normal/optimized replays, export/cold checks, +public CI, and independent human or formal acceptance require their own +evidence and are not inferred from that first run. + +The source finite group, its published-table association, the width-nine +multiplicities, tensor reciprocity premises, and Gram interpretation remain +explicit dependencies. The hand lift, fixed-form count, fixed-space trace +inequality, and exact phase cancellation are the new proof obligations +resolved here. No physical native implementation, all-input caller, +precision/overflow envelope, supplier, asymptotic multiplication exponent, +or selected-frontier change follows from this conditioning lemma. diff --git a/research/clifford-order3-conditioning/README.md b/research/clifford-order3-conditioning/README.md new file mode 100644 index 0000000000..cdb7af4420 --- /dev/null +++ b/research/clifford-order3-conditioning/README.md @@ -0,0 +1,127 @@ +# A second trace constraint for three-qubit Clifford conditioning + +Prepared for ToikY with substantial source-aware OpenAI Codex assistance. +New work Apache-2.0; [LICENSE](LICENSE) and [NOTICE](NOTICE) retain the repository +license and source attribution. Retained source notices and numerical facts +keep their provenance. This is a written native-algebra side result, separate from +physical implementation, selected admission and human/proof-kernel acceptance. + +This takes [Nick Petalas PR6794](https://github.com/CrocSwap/integer-mult-bounds/pull/6794)'s +second-class trace handoff, using [alephnan PR6714](https://github.com/CrocSwap/integer-mult-bounds/pull/6714)'s +exact alphabet, width-nine multiplicities, tensor reciprocity, Pauli-character +orbits, Gram normalization, Schur propagation and published-table identification +as inherited mathematical inputs. The one-transvection relaxation and bound807 +are predecessor work, not a new computation or theorem here. Own excluded6718 +reviewed the earlier even-sector argument and is not counted again. + +The actual new lift is g=(hS) tensor I4, with +h=(1+i)/2 [[1,1],[1,-1]] and S=diag(1,i). It is Gaussian-dyadic, has trace4 +and cube -I. Its symplectic quotient acts with order three on one hyperbolic +plane and fixes the complementary four dimensions. The associated source +quotient fibre5 has size672 and fixed dimension4, corresponding to published +columns9/10, distinct from the transvection's quotient index14/columns31..33. +The lift-to-class argument is in PROOF.md; the old table identification remains +a cited premise, not reconstructed from group multiplication. + +For an even-sector irreducible mu with central iI acting by -I, write +conjugate(V) tensor mu = sum n_sigma (V tensor sigma), d_mu=N*a, N in{28,36}. +Exactly6 forms in the36-form even-Arf orbit and10 forms in the28-form odd-Arf +orbit are fixed by this quotient. On a fixed multiplicity space, g has cube I +in mu, so the real part of its trace lies between -a/2 and a. Individual traces +need not be real. The exact natural trace4 cancels in the character identity; +the retained real quotient column then gives the new constraint on +T3=sum n_sigma chi_sigma(gbar): + +``` +N=36: -3/N <= T3/d_mu <= 6/N +N=28: -5/N <= T3/d_mu <= 10/N. +``` + +Combine this with the credited transvection constraint |Tt/d_mu|<=16/N. +The checked orbit-specific multiplicity-ratio intervals are [2/7,2353/20] +for N=28 and [1,2621/36] for N=36. They give, for every integer f>=10, + +``` +(405/16384) I <= H_f <= (1334151/131072) I, +condition(H_f) <= 16471/40 = 411.775 < 807. +``` + +Three rowwise affine inequalities, checked for every one of the thirty cited +types, and feasible primal mixtures certify the relaxation extrema. All four +displayed dual certificates have zero transvection coefficient: the new +order-three constraint alone supplies the numerical bounds, while all +attaining mixtures also satisfy the retained transvection slab. These convex +extremizers need not be actual irreducible decompositions or actual Gram +eigenvalues. No threshold change is proposed. The all-width consequence uses +the written proof and inherited Schur propagation, separately from execution. + +## Evidence and reproduction + +The new standard-library verifier authenticates five retained inert source +files and their exact manifest before calculating. The first run passed in +0.702 seconds with24.3125MiB maximum RSS. It checks one actual8x8 Gaussian lift, +64 signed Pauli images, all64 quadratic forms over4,096 distinct form/vector +cases, and252 distinct feasible vertices:84 for N28 and168 for N36. The generic +support-three branch finds no positive three-row vertex in this fixed dataset; +it is not an enumeration of the full group or all representations. Four +30-row dual certificates and six witnessed controls pass. Controls distinguish +phase, Pauli membership, Arf classification, omitted/new bound information and +column selection; two display lost-constraint primal admission, rather than +rejection of an otherwise valid representation. It imports +or runs no predecessor scientific program, group census, numerical decomposition +or full even-sector table. No new dependencies are required. + +``` +python3.12 -B scripts/research_package.py --package research/clifford-order3-conditioning +python3.12 -B scripts/check_research_commit.py --package research/clifford-order3-conditioning --check-source-history +``` + +Generic SOURCES binds only canonical-main selection/catalogue provenance. +Actual foreign mathematical sources are byte-identical package-local copies, +bound by SOURCE-PINS with exact head/path/blob/mode/size/hash and checked at +acquisition against the source trees. That foreign association is distinct +from generic canonical ancestry; cached refs are not publication history. +Direct replay needs only these local files and no Git or network. VERIFY has +no external live runtime input. Default normal/optimized commands compare the +entire typed retained RESULT. Final normal/optimized packets are identical: +13,000bytes, SHA25638380ddd9be74d0bf0beb6bd2c21a4dddbc7e78e94ffc3607c08bf421118771a. +After the first PASS, one receipt key was renamed from form_vector_evaluations +to distinct_form_vector_pairs:4,096 denotes distinct grid cases, not the two +function evaluations per case. The entire typed first packet is otherwise +identical; original bytes/code and both pre-correction replays are retained +in the session receipts. No mathematical arithmetic/source/control changed. +No package self-hash is included in its own scientific packet. + +## Open next questions + +Determine whether the relaxed extrema are realized by actual even-sector +irreducibles. The smallest useful next step is one actual quadratic-form +stabilizer representation/decomposition bound to this central sector, not an +unlabelled convex mixture. That information is absent here; no full table or +follow-on search is reserved. + +For physical use, name an exact caller and its alphabet/coefficients, then price +preparation, coefficient recovery, precision, routing, movement, ownership, +restoration, stock and the complete recursive supplier invoice. These remain +unknown. All five selected assumptions and the frontier are unchanged. +The formal-interface-lemma card is explicitly changed/partial: no Lean +proposition or original selected-interface acceptance gate is closed. + +## Credit and exposure + +Credit Petalas6794 for its exact one-transvection807 certificate and explicit +second-class request; alephnan6714 for the three-qubit theorem, decomposition, +normalization, reciprocity and Pauli-orbit reduction; Lee, Yu, Peng and Lai for +[the published table](https://arxiv.org/html/2309.14850v2#S6.SS3); Ali Romman and +MatShep for the general Clifford and sharp small-qubit lineage; and all retained +authors/notices. Quadratic-form classification, character trace bounds, +centralizers, tensor reciprocity, convex duality and Schur positivity are +classical. No new character table or separate review of those inherited +identifications is claimed. + +The root proposed paired-transvection count guesses and the hS lift/phase +recipe during preclaim orientation; these were unaccepted then and no new +scientific execution had occurred. Related source-aware proof, implementation, +overlap/metadata and challenge roles see those sources and proposal. This is +not blind independence, human acceptance or proof-kernel verification. Exact +claim, source pins, stop rule and preserved exposure are linked from TASK.json. diff --git a/research/clifford-order3-conditioning/RESULT.json b/research/clifford-order3-conditioning/RESULT.json new file mode 100644 index 0000000000..afd16aacc3 --- /dev/null +++ b/research/clifford-order3-conditioning/RESULT.json @@ -0,0 +1,2524 @@ +{ + "Gram_interval": [ + [ + 405, + 16384 + ], + [ + 1334151, + 131072 + ] + ], + "Gram_scale": [ + 2835, + 32768 + ], + "LP": [ + { + "distinct_vertices": 84, + "maximum": { + "affine_coefficients": [ + [ + 1007, + 30 + ], + [ + 0, + 1 + ], + [ + 7063, + 30 + ] + ], + "objective": [ + 2353, + 20 + ], + "primal": { + "objective": [ + 2353, + 20 + ], + "order3": [ + 5, + 14 + ], + "transvection": [ + 3, + 7 + ], + "weights": [ + [ + 1, + [ + 2, + 5 + ] + ], + [ + 13, + [ + 3, + 5 + ] + ] + ] + }, + "scaled_residuals": [ + [ + 1, + [ + 0, + 1 + ] + ], + [ + 2, + [ + 11767, + 10 + ] + ], + [ + 3, + [ + 837, + 2 + ] + ], + [ + 4, + [ + 4165, + 2 + ] + ], + [ + 5, + [ + 2555, + 2 + ] + ], + [ + 6, + [ + 5676, + 5 + ] + ], + [ + 7, + [ + 377, + 1 + ] + ], + [ + 8, + [ + 2177, + 1 + ] + ], + [ + 9, + [ + 8883, + 2 + ] + ], + [ + 12, + [ + 1645, + 2 + ] + ], + [ + 13, + [ + 0, + 1 + ] + ], + [ + 14, + [ + 6846, + 1 + ] + ], + [ + 15, + [ + 1799, + 2 + ] + ], + [ + 16, + [ + 3899, + 2 + ] + ], + [ + 17, + [ + 7319, + 2 + ] + ], + [ + 18, + [ + 13209, + 5 + ] + ], + [ + 19, + [ + 7518, + 1 + ] + ], + [ + 20, + [ + 7896, + 1 + ] + ], + [ + 21, + [ + 5628, + 1 + ] + ], + [ + 22, + [ + 10661, + 2 + ] + ], + [ + 23, + [ + 1785, + 2 + ] + ], + [ + 24, + [ + 6807, + 2 + ] + ], + [ + 25, + [ + 5243, + 2 + ] + ], + [ + 26, + [ + 10353, + 1 + ] + ], + [ + 29, + [ + 17997, + 2 + ] + ], + [ + 32, + [ + 9751, + 1 + ] + ], + [ + 33, + [ + 77343, + 10 + ] + ], + [ + 36, + [ + 15039, + 2 + ] + ], + [ + 37, + [ + 8848, + 1 + ] + ], + [ + 38, + [ + 39896, + 5 + ] + ] + ], + "signed_active_bounds": [ + null, + [ + 5, + 14 + ] + ] + }, + "minimum": { + "affine_coefficients": [ + [ + 16, + 21 + ], + [ + 0, + 1 + ], + [ + -4, + 3 + ] + ], + "objective": [ + 2, + 7 + ], + "primal": { + "objective": [ + 2, + 7 + ], + "order3": [ + 5, + 14 + ], + "transvection": [ + -27, + 49 + ], + "weights": [ + [ + 2, + [ + 3, + 7 + ] + ], + [ + 9, + [ + 4, + 7 + ] + ] + ] + }, + "scaled_residuals": [ + [ + 1, + [ + 1887, + 7 + ] + ], + [ + 2, + [ + 0, + 1 + ] + ], + [ + 3, + [ + 515, + 7 + ] + ], + [ + 4, + [ + 27, + 1 + ] + ], + [ + 5, + [ + 832, + 1 + ] + ], + [ + 6, + [ + 13170, + 7 + ] + ], + [ + 7, + [ + 1955, + 1 + ] + ], + [ + 8, + [ + 155, + 1 + ] + ], + [ + 9, + [ + 0, + 1 + ] + ], + [ + 12, + [ + 290, + 1 + ] + ], + [ + 13, + [ + 1335, + 1 + ] + ], + [ + 14, + [ + 150, + 1 + ] + ], + [ + 15, + [ + 2545, + 1 + ] + ], + [ + 16, + [ + 1495, + 1 + ] + ], + [ + 17, + [ + 26800, + 7 + ] + ], + [ + 18, + [ + 4290, + 1 + ] + ], + [ + 19, + [ + 813, + 1 + ] + ], + [ + 20, + [ + 435, + 1 + ] + ], + [ + 21, + [ + 2703, + 1 + ] + ], + [ + 22, + [ + 5110, + 1 + ] + ], + [ + 23, + [ + 2445, + 1 + ] + ], + [ + 24, + [ + 10860, + 7 + ] + ], + [ + 25, + [ + 5380, + 1 + ] + ], + [ + 26, + [ + 1200, + 1 + ] + ], + [ + 29, + [ + 1335, + 1 + ] + ], + [ + 32, + [ + 2692, + 1 + ] + ], + [ + 33, + [ + 2535, + 1 + ] + ], + [ + 36, + [ + 40365, + 7 + ] + ], + [ + 37, + [ + 4930, + 1 + ] + ], + [ + 38, + [ + 35200, + 7 + ] + ] + ], + "signed_active_bounds": [ + null, + [ + 5, + 14 + ] + ] + }, + "orbit_size": 28, + "slabs": [ + [ + -4, + 7 + ], + [ + 4, + 7 + ], + [ + -5, + 28 + ], + [ + 5, + 14 + ] + ], + "support_histogram": { + "1": 28, + "2": 56 + }, + "vertex_digest": "2a477f74ca9fc0ed3a6cc9d6135df992da498cd564ad5997ff3a2358724e9cd1" + }, + { + "distinct_vertices": 168, + "maximum": { + "affine_coefficients": [ + [ + 1007, + 30 + ], + [ + 0, + 1 + ], + [ + 7063, + 30 + ] + ], + "objective": [ + 2621, + 36 + ], + "primal": { + "objective": [ + 2621, + 36 + ], + "order3": [ + 1, + 6 + ], + "transvection": [ + 7, + 27 + ], + "weights": [ + [ + 1, + [ + 2, + 9 + ] + ], + [ + 13, + [ + 7, + 9 + ] + ] + ] + }, + "scaled_residuals": [ + [ + 1, + [ + 0, + 1 + ] + ], + [ + 2, + [ + 11767, + 10 + ] + ], + [ + 3, + [ + 837, + 2 + ] + ], + [ + 4, + [ + 4165, + 2 + ] + ], + [ + 5, + [ + 2555, + 2 + ] + ], + [ + 6, + [ + 5676, + 5 + ] + ], + [ + 7, + [ + 377, + 1 + ] + ], + [ + 8, + [ + 2177, + 1 + ] + ], + [ + 9, + [ + 8883, + 2 + ] + ], + [ + 12, + [ + 1645, + 2 + ] + ], + [ + 13, + [ + 0, + 1 + ] + ], + [ + 14, + [ + 6846, + 1 + ] + ], + [ + 15, + [ + 1799, + 2 + ] + ], + [ + 16, + [ + 3899, + 2 + ] + ], + [ + 17, + [ + 7319, + 2 + ] + ], + [ + 18, + [ + 13209, + 5 + ] + ], + [ + 19, + [ + 7518, + 1 + ] + ], + [ + 20, + [ + 7896, + 1 + ] + ], + [ + 21, + [ + 5628, + 1 + ] + ], + [ + 22, + [ + 10661, + 2 + ] + ], + [ + 23, + [ + 1785, + 2 + ] + ], + [ + 24, + [ + 6807, + 2 + ] + ], + [ + 25, + [ + 5243, + 2 + ] + ], + [ + 26, + [ + 10353, + 1 + ] + ], + [ + 29, + [ + 17997, + 2 + ] + ], + [ + 32, + [ + 9751, + 1 + ] + ], + [ + 33, + [ + 77343, + 10 + ] + ], + [ + 36, + [ + 15039, + 2 + ] + ], + [ + 37, + [ + 8848, + 1 + ] + ], + [ + 38, + [ + 39896, + 5 + ] + ] + ], + "signed_active_bounds": [ + null, + [ + 1, + 6 + ] + ] + }, + "minimum": { + "affine_coefficients": [ + [ + 19, + 5 + ], + [ + 0, + 1 + ], + [ + -84, + 5 + ] + ], + "objective": [ + 1, + 1 + ], + "primal": { + "objective": [ + 1, + 1 + ], + "order3": [ + 1, + 6 + ], + "transvection": [ + -25, + 63 + ], + "weights": [ + [ + 9, + [ + 8, + 9 + ] + ], + [ + 12, + [ + 1, + 9 + ] + ] + ] + }, + "scaled_residuals": [ + [ + 1, + [ + 282, + 1 + ] + ], + [ + 2, + [ + 203, + 5 + ] + ], + [ + 3, + [ + 28, + 1 + ] + ], + [ + 4, + [ + 56, + 1 + ] + ], + [ + 5, + [ + 861, + 1 + ] + ], + [ + 6, + [ + 9693, + 5 + ] + ], + [ + 7, + [ + 1926, + 1 + ] + ], + [ + 8, + [ + 126, + 1 + ] + ], + [ + 9, + [ + 0, + 1 + ] + ], + [ + 12, + [ + 0, + 1 + ] + ], + [ + 13, + [ + 987, + 1 + ] + ], + [ + 14, + [ + 63, + 1 + ] + ], + [ + 15, + [ + 2226, + 1 + ] + ], + [ + 16, + [ + 1176, + 1 + ] + ], + [ + 17, + [ + 3696, + 1 + ] + ], + [ + 18, + [ + 19362, + 5 + ] + ], + [ + 19, + [ + 378, + 1 + ] + ], + [ + 20, + [ + 0, + 1 + ] + ], + [ + 21, + [ + 2268, + 1 + ] + ], + [ + 22, + [ + 4704, + 1 + ] + ], + [ + 23, + [ + 1575, + 1 + ] + ], + [ + 24, + [ + 756, + 1 + ] + ], + [ + 25, + [ + 4452, + 1 + ] + ], + [ + 26, + [ + 504, + 1 + ] + ], + [ + 29, + [ + 378, + 1 + ] + ], + [ + 32, + [ + 1764, + 1 + ] + ], + [ + 33, + [ + 6237, + 5 + ] + ], + [ + 36, + [ + 4536, + 1 + ] + ], + [ + 37, + [ + 3654, + 1 + ] + ], + [ + 38, + [ + 16128, + 5 + ] + ] + ], + "signed_active_bounds": [ + null, + [ + 1, + 6 + ] + ] + }, + "orbit_size": 36, + "slabs": [ + [ + -4, + 9 + ], + [ + 4, + 9 + ], + [ + -1, + 12 + ], + [ + 1, + 6 + ] + ], + "support_histogram": { + "1": 24, + "2": 144 + }, + "vertex_digest": "5f371f4451b6a727cdf8da4a36da0aa17a27635303f89bfd59055fb27d3e26db" + } + ], + "Pauli_action": [ + { + "label": 0, + "sign": 1, + "target": 0 + }, + { + "label": 1, + "sign": -1, + "target": 9 + }, + { + "label": 2, + "sign": 1, + "target": 2 + }, + { + "label": 3, + "sign": -1, + "target": 11 + }, + { + "label": 4, + "sign": 1, + "target": 4 + }, + { + "label": 5, + "sign": -1, + "target": 13 + }, + { + "label": 6, + "sign": 1, + "target": 6 + }, + { + "label": 7, + "sign": -1, + "target": 15 + }, + { + "label": 8, + "sign": 1, + "target": 1 + }, + { + "label": 9, + "sign": -1, + "target": 8 + }, + { + "label": 10, + "sign": 1, + "target": 3 + }, + { + "label": 11, + "sign": -1, + "target": 10 + }, + { + "label": 12, + "sign": 1, + "target": 5 + }, + { + "label": 13, + "sign": -1, + "target": 12 + }, + { + "label": 14, + "sign": 1, + "target": 7 + }, + { + "label": 15, + "sign": -1, + "target": 14 + }, + { + "label": 16, + "sign": 1, + "target": 16 + }, + { + "label": 17, + "sign": -1, + "target": 25 + }, + { + "label": 18, + "sign": 1, + "target": 18 + }, + { + "label": 19, + "sign": -1, + "target": 27 + }, + { + "label": 20, + "sign": 1, + "target": 20 + }, + { + "label": 21, + "sign": -1, + "target": 29 + }, + { + "label": 22, + "sign": 1, + "target": 22 + }, + { + "label": 23, + "sign": -1, + "target": 31 + }, + { + "label": 24, + "sign": 1, + "target": 17 + }, + { + "label": 25, + "sign": -1, + "target": 24 + }, + { + "label": 26, + "sign": 1, + "target": 19 + }, + { + "label": 27, + "sign": -1, + "target": 26 + }, + { + "label": 28, + "sign": 1, + "target": 21 + }, + { + "label": 29, + "sign": -1, + "target": 28 + }, + { + "label": 30, + "sign": 1, + "target": 23 + }, + { + "label": 31, + "sign": -1, + "target": 30 + }, + { + "label": 32, + "sign": 1, + "target": 32 + }, + { + "label": 33, + "sign": -1, + "target": 41 + }, + { + "label": 34, + "sign": 1, + "target": 34 + }, + { + "label": 35, + "sign": -1, + "target": 43 + }, + { + "label": 36, + "sign": 1, + "target": 36 + }, + { + "label": 37, + "sign": -1, + "target": 45 + }, + { + "label": 38, + "sign": 1, + "target": 38 + }, + { + "label": 39, + "sign": -1, + "target": 47 + }, + { + "label": 40, + "sign": 1, + "target": 33 + }, + { + "label": 41, + "sign": -1, + "target": 40 + }, + { + "label": 42, + "sign": 1, + "target": 35 + }, + { + "label": 43, + "sign": -1, + "target": 42 + }, + { + "label": 44, + "sign": 1, + "target": 37 + }, + { + "label": 45, + "sign": -1, + "target": 44 + }, + { + "label": 46, + "sign": 1, + "target": 39 + }, + { + "label": 47, + "sign": -1, + "target": 46 + }, + { + "label": 48, + "sign": 1, + "target": 48 + }, + { + "label": 49, + "sign": -1, + "target": 57 + }, + { + "label": 50, + "sign": 1, + "target": 50 + }, + { + "label": 51, + "sign": -1, + "target": 59 + }, + { + "label": 52, + "sign": 1, + "target": 52 + }, + { + "label": 53, + "sign": -1, + "target": 61 + }, + { + "label": 54, + "sign": 1, + "target": 54 + }, + { + "label": 55, + "sign": -1, + "target": 63 + }, + { + "label": 56, + "sign": 1, + "target": 49 + }, + { + "label": 57, + "sign": -1, + "target": 56 + }, + { + "label": 58, + "sign": 1, + "target": 51 + }, + { + "label": 59, + "sign": -1, + "target": 58 + }, + { + "label": 60, + "sign": 1, + "target": 53 + }, + { + "label": 61, + "sign": -1, + "target": 60 + }, + { + "label": 62, + "sign": 1, + "target": 55 + }, + { + "label": 63, + "sign": -1, + "target": 62 + } + ], + "control_count": 6, + "controls": [ + { + "name": "wrong_global_phase_i_g", + "outcome": "REJECTED_FOR_INTENDED_REASON", + "reason": "lift cube is not minus identity", + "witness": { + "character_witnesses": { + "exterior_square_trace": [ + -10, + 1, + 0, + 1 + ], + "natural_trace": [ + 0, + 1, + 4, + 1 + ], + "scope": "Actual natural symmetric/exterior-square characters; no irreducibility assertion.", + "symmetric_square_trace": [ + -6, + 1, + 0, + 1 + ], + "trace_of_square": [ + 4, + 1, + 0, + 1 + ] + }, + "cube_phase": [ + 0, + 1, + 1, + 1 + ], + "same_signed_Pauli_action": true, + "trace": [ + 0, + 1, + 4, + 1 + ] + } + }, + { + "name": "non_Pauli_Toffoli_permutation", + "outcome": "DETECTED_NON_PAULI_IMAGE", + "witness": { + "image": [ + [ + 0, + 4, + [ + 1, + 1, + 0, + 1 + ] + ], + [ + 1, + 5, + [ + 1, + 1, + 0, + 1 + ] + ], + [ + 2, + 7, + [ + 1, + 1, + 0, + 1 + ] + ], + [ + 3, + 6, + [ + 1, + 1, + 0, + 1 + ] + ], + [ + 4, + 0, + [ + 1, + 1, + 0, + 1 + ] + ], + [ + 5, + 1, + [ + 1, + 1, + 0, + 1 + ] + ], + [ + 6, + 3, + [ + 1, + 1, + 0, + 1 + ] + ], + [ + 7, + 2, + [ + 1, + 1, + 0, + 1 + ] + ] + ], + "input_label": 1 + } + }, + { + "name": "omit_first_pair_from_Arf", + "outcome": "REJECTED_FOR_INTENDED_REASON", + "reason": "quadratic orbit sizes", + "witness": { + "actual_fixed": [ + 6, + 10 + ], + "actual_form9": { + "arf": 1, + "fixed": true, + "form": 9, + "pullback": 9 + }, + "actual_orbits": [ + 36, + 28 + ], + "mutated_fixed": [ + 10, + 6 + ], + "mutated_form9": { + "arf": 0, + "fixed": true, + "form": 9, + "pullback": 9 + }, + "mutated_orbits": [ + 40, + 24 + ] + } + }, + { + "name": "omit_order3_constraint", + "outcome": "OLD_PRIMAL_ADMITTED_ONLY_AFTER_OMISSION", + "rejected_by": "order3 trace slab", + "witness": { + "objective": [ + 807, + 4 + ], + "order3": [ + 25, + 28 + ], + "transvection": [ + 4, + 7 + ], + "weights": [ + [ + 1, + [ + 3, + 4 + ] + ], + [ + 2, + [ + 1, + 4 + ] + ] + ] + } + }, + { + "correct_bounds": [ + [ + -5, + 28 + ], + [ + 5, + 14 + ] + ], + "name": "reuse_transvection_fixed16_for_order3", + "outcome": "LOOSE_BOUND_ADMITS_FORBIDDEN_PRIMAL", + "rejected_by": "order3 trace slab", + "witness": { + "objective": [ + 1, + 4 + ], + "order3": [ + 43, + 112 + ], + "transvection": [ + -4, + 7 + ], + "weights": [ + [ + 2, + [ + 1, + 2 + ] + ], + [ + 9, + [ + 1, + 2 + ] + ] + ] + }, + "wrong_bounds": [ + [ + -2, + 7 + ], + [ + 4, + 7 + ] + ] + }, + { + "name": "transvection_column_used_as_order3", + "outcome": "REJECTED_FOR_INTENDED_REASON", + "reason": "selected column anchors", + "witness": { + "actual_wrong_T3": -5, + "expected_T3": 4, + "source_row": 2 + } + } + ], + "credited_one_trace_bound": 807, + "improves_credited_bound": true, + "inherited_premises": [ + "published quotient-character identification", + "width-nine multiplicities", + "even-sector decomposition/reciprocity", + "transvection bound16/N", + "order3 class5 identification", + "Pauli orbit/central phase rules", + "Schur propagation" + ], + "multiplicity_ratio_interval": [ + [ + 2, + 7 + ], + [ + 2353, + 20 + ] + ], + "quadratic_forms": { + "distinct_form_vector_pairs": 4096, + "fixed_by_arf": [ + 6, + 10 + ], + "orbit_sizes": [ + 36, + 28 + ], + "records": [ + { + "arf": 0, + "fixed": false, + "form": 0, + "pullback": 1 + }, + { + "arf": 0, + "fixed": false, + "form": 1, + "pullback": 8 + }, + { + "arf": 0, + "fixed": false, + "form": 2, + "pullback": 3 + }, + { + "arf": 0, + "fixed": false, + "form": 3, + "pullback": 10 + }, + { + "arf": 0, + "fixed": false, + "form": 4, + "pullback": 5 + }, + { + "arf": 0, + "fixed": false, + "form": 5, + "pullback": 12 + }, + { + "arf": 0, + "fixed": false, + "form": 6, + "pullback": 7 + }, + { + "arf": 0, + "fixed": false, + "form": 7, + "pullback": 14 + }, + { + "arf": 0, + "fixed": false, + "form": 8, + "pullback": 0 + }, + { + "arf": 1, + "fixed": true, + "form": 9, + "pullback": 9 + }, + { + "arf": 0, + "fixed": false, + "form": 10, + "pullback": 2 + }, + { + "arf": 1, + "fixed": true, + "form": 11, + "pullback": 11 + }, + { + "arf": 0, + "fixed": false, + "form": 12, + "pullback": 4 + }, + { + "arf": 1, + "fixed": true, + "form": 13, + "pullback": 13 + }, + { + "arf": 0, + "fixed": false, + "form": 14, + "pullback": 6 + }, + { + "arf": 1, + "fixed": true, + "form": 15, + "pullback": 15 + }, + { + "arf": 0, + "fixed": false, + "form": 16, + "pullback": 17 + }, + { + "arf": 0, + "fixed": false, + "form": 17, + "pullback": 24 + }, + { + "arf": 1, + "fixed": false, + "form": 18, + "pullback": 19 + }, + { + "arf": 1, + "fixed": false, + "form": 19, + "pullback": 26 + }, + { + "arf": 0, + "fixed": false, + "form": 20, + "pullback": 21 + }, + { + "arf": 0, + "fixed": false, + "form": 21, + "pullback": 28 + }, + { + "arf": 1, + "fixed": false, + "form": 22, + "pullback": 23 + }, + { + "arf": 1, + "fixed": false, + "form": 23, + "pullback": 30 + }, + { + "arf": 0, + "fixed": false, + "form": 24, + "pullback": 16 + }, + { + "arf": 1, + "fixed": true, + "form": 25, + "pullback": 25 + }, + { + "arf": 1, + "fixed": false, + "form": 26, + "pullback": 18 + }, + { + "arf": 0, + "fixed": true, + "form": 27, + "pullback": 27 + }, + { + "arf": 0, + "fixed": false, + "form": 28, + "pullback": 20 + }, + { + "arf": 1, + "fixed": true, + "form": 29, + "pullback": 29 + }, + { + "arf": 1, + "fixed": false, + "form": 30, + "pullback": 22 + }, + { + "arf": 0, + "fixed": true, + "form": 31, + "pullback": 31 + }, + { + "arf": 0, + "fixed": false, + "form": 32, + "pullback": 33 + }, + { + "arf": 0, + "fixed": false, + "form": 33, + "pullback": 40 + }, + { + "arf": 0, + "fixed": false, + "form": 34, + "pullback": 35 + }, + { + "arf": 0, + "fixed": false, + "form": 35, + "pullback": 42 + }, + { + "arf": 1, + "fixed": false, + "form": 36, + "pullback": 37 + }, + { + "arf": 1, + "fixed": false, + "form": 37, + "pullback": 44 + }, + { + "arf": 1, + "fixed": false, + "form": 38, + "pullback": 39 + }, + { + "arf": 1, + "fixed": false, + "form": 39, + "pullback": 46 + }, + { + "arf": 0, + "fixed": false, + "form": 40, + "pullback": 32 + }, + { + "arf": 1, + "fixed": true, + "form": 41, + "pullback": 41 + }, + { + "arf": 0, + "fixed": false, + "form": 42, + "pullback": 34 + }, + { + "arf": 1, + "fixed": true, + "form": 43, + "pullback": 43 + }, + { + "arf": 1, + "fixed": false, + "form": 44, + "pullback": 36 + }, + { + "arf": 0, + "fixed": true, + "form": 45, + "pullback": 45 + }, + { + "arf": 1, + "fixed": false, + "form": 46, + "pullback": 38 + }, + { + "arf": 0, + "fixed": true, + "form": 47, + "pullback": 47 + }, + { + "arf": 0, + "fixed": false, + "form": 48, + "pullback": 49 + }, + { + "arf": 0, + "fixed": false, + "form": 49, + "pullback": 56 + }, + { + "arf": 1, + "fixed": false, + "form": 50, + "pullback": 51 + }, + { + "arf": 1, + "fixed": false, + "form": 51, + "pullback": 58 + }, + { + "arf": 1, + "fixed": false, + "form": 52, + "pullback": 53 + }, + { + "arf": 1, + "fixed": false, + "form": 53, + "pullback": 60 + }, + { + "arf": 0, + "fixed": false, + "form": 54, + "pullback": 55 + }, + { + "arf": 0, + "fixed": false, + "form": 55, + "pullback": 62 + }, + { + "arf": 0, + "fixed": false, + "form": 56, + "pullback": 48 + }, + { + "arf": 1, + "fixed": true, + "form": 57, + "pullback": 57 + }, + { + "arf": 1, + "fixed": false, + "form": 58, + "pullback": 50 + }, + { + "arf": 0, + "fixed": true, + "form": 59, + "pullback": 59 + }, + { + "arf": 1, + "fixed": false, + "form": 60, + "pullback": 52 + }, + { + "arf": 0, + "fixed": true, + "form": 61, + "pullback": 61 + }, + { + "arf": 0, + "fixed": false, + "form": 62, + "pullback": 54 + }, + { + "arf": 1, + "fixed": true, + "form": 63, + "pullback": 63 + } + ] + }, + "schema_version": 1, + "scope": "Two-trace30-point relaxation; primal optima are not asserted actual irreducibles or spectrum.", + "selected_lift": { + "character_witnesses": { + "exterior_square_trace": [ + 10, + 1, + 0, + 1 + ], + "natural_trace": [ + 4, + 1, + 0, + 1 + ], + "scope": "Actual natural symmetric/exterior-square characters; no irreducibility assertion.", + "symmetric_square_trace": [ + 6, + 1, + 0, + 1 + ], + "trace_of_square": [ + -4, + 1, + 0, + 1 + ] + }, + "cube_phase": [ + -1, + 1, + 0, + 1 + ], + "fixed_quotient_vectors": 16, + "g2": [ + [ + 0, + 0, + [ + 1, + 2, + 1, + 2 + ] + ], + [ + 0, + 1, + [ + -1, + 2, + 1, + 2 + ] + ], + [ + 1, + 0, + [ + 1, + 2, + 1, + 2 + ] + ], + [ + 1, + 1, + [ + 1, + 2, + -1, + 2 + ] + ] + ], + "quotient_matrix": [ + [ + 1, + 0, + 0, + 1, + 0, + 0 + ], + [ + 0, + 1, + 0, + 0, + 0, + 0 + ], + [ + 0, + 0, + 1, + 0, + 0, + 0 + ], + [ + 1, + 0, + 0, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + 0, + 1, + 0 + ], + [ + 0, + 0, + 0, + 0, + 0, + 1 + ] + ], + "trace": [ + 4, + 1, + 0, + 1 + ], + "unitary": true + }, + "source_points": [ + { + "d": 1, + "m": 269, + "row": 1, + "t": 1, + "z": 1 + }, + { + "d": 7, + "m": 0, + "row": 2, + "t": -5, + "z": 4 + }, + { + "d": 15, + "m": 85, + "row": 3, + "t": -5, + "z": 0 + }, + { + "d": 21, + "m": 35, + "row": 4, + "t": -11, + "z": 6 + }, + { + "d": 21, + "m": 840, + "row": 5, + "t": 9, + "z": 6 + }, + { + "d": 27, + "m": 1890, + "row": 6, + "t": 15, + "z": 9 + }, + { + "d": 35, + "m": 1975, + "row": 7, + "t": 15, + "z": 5 + }, + { + "d": 35, + "m": 175, + "row": 8, + "t": -5, + "z": 5 + }, + { + "d": 56, + "m": 28, + "row": 9, + "t": -24, + "z": 11 + }, + { + "d": 70, + "m": 350, + "row": 12, + "t": -10, + "z": -5 + }, + { + "d": 84, + "m": 1407, + "row": 13, + "t": 4, + "z": -6 + }, + { + "d": 105, + "m": 210, + "row": 14, + "t": -35, + "z": 15 + }, + { + "d": 105, + "m": 2625, + "row": 15, + "t": 25, + "z": 0 + }, + { + "d": 105, + "m": 1575, + "row": 16, + "t": 5, + "z": 0 + }, + { + "d": 120, + "m": 3900, + "row": 17, + "t": 40, + "z": 15 + }, + { + "d": 168, + "m": 4410, + "row": 18, + "t": 40, + "z": 6 + }, + { + "d": 189, + "m": 945, + "row": 19, + "t": -39, + "z": 9 + }, + { + "d": 189, + "m": 567, + "row": 20, + "t": -51, + "z": 9 + }, + { + "d": 189, + "m": 2835, + "row": 21, + "t": 21, + "z": 9 + }, + { + "d": 210, + "m": 5250, + "row": 22, + "t": 50, + "z": 15 + }, + { + "d": 210, + "m": 2625, + "row": 23, + "t": 10, + "z": -15 + }, + { + "d": 216, + "m": 1728, + "row": 24, + "t": -24, + "z": -9 + }, + { + "d": 280, + "m": 5600, + "row": 25, + "t": 40, + "z": -5 + }, + { + "d": 280, + "m": 1400, + "row": 26, + "t": -40, + "z": 10 + }, + { + "d": 315, + "m": 1575, + "row": 29, + "t": -45, + "z": 0 + }, + { + "d": 336, + "m": 2940, + "row": 32, + "t": -16, + "z": 6 + }, + { + "d": 378, + "m": 2835, + "row": 33, + "t": -30, + "z": -9 + }, + { + "d": 405, + "m": 6075, + "row": 36, + "t": 45, + "z": 0 + }, + { + "d": 420, + "m": 5250, + "row": 37, + "t": 20, + "z": 0 + }, + { + "d": 512, + "m": 5440, + "row": 38, + "t": 0, + "z": -16 + } + ], + "source_programs_executed": false, + "source_sha256": { + "predecessor/PR6714-PROOF.md": "d29091eb12b4ccd3f5acb389634a858af3beb0dc78865613bb7bd68c9440c6d0", + "predecessor/PR6794-PROOF.md": "cff2a5c894f20f368ecb88410dbd29c8380144c46cfa7dac4428296725e50ef3", + "source/EXTERNAL.json": "eb64deffd68787fe12df7b745d98f3139f77c5ab7ecd41a86bd832db0c7ebe0a", + "source/table.json": "388d617a76e345774a8768f32a6a9bc6e94b87f9c8a5cf6712a95a5a3a945fcd", + "source/width-nine-input.json": "308b8dee094eb5481565ea89698ed5df69edeeecd4b63b4d78cb9cecdbe71c27" + }, + "status": "PASS_CLIFFORD_ORDER3_CONDITIONING", + "sufficient_condition_bound": [ + 16471, + 40 + ] +} diff --git a/research/clifford-order3-conditioning/SOURCE-PINS.json b/research/clifford-order3-conditioning/SOURCE-PINS.json new file mode 100644 index 0000000000..8c10930096 --- /dev/null +++ b/research/clifford-order3-conditioning/SOURCE-PINS.json @@ -0,0 +1,60 @@ +{ + "schema_version": 1, + "files": [ + { + "local_path": "predecessor/PR6794-PROOF.md", + "source_repository": "petalas/integer-mult-bounds", + "source_commit": "c6252da020819a08ef2b2ff14280146c43ad374c", + "source_path": "research/clifford-transvection-conditioning/PROOF.md", + "git_blob": "60a16b0578affc88657e8e79bb503ec9d2fa00a6", + "sha256": "cff2a5c894f20f368ecb88410dbd29c8380144c46cfa7dac4428296725e50ef3", + "bytes": 7156, + "mode": "100644", + "usage": "Inert mathematical provenance or retained source data; not executed or independently accepted." + }, + { + "local_path": "source/table.json", + "source_repository": "petalas/integer-mult-bounds", + "source_commit": "c6252da020819a08ef2b2ff14280146c43ad374c", + "source_path": "research/clifford-transvection-conditioning/source/pr6714-table.json", + "git_blob": "01f56d329aec686e49dc18f83adfea47b7fa423e", + "sha256": "388d617a76e345774a8768f32a6a9bc6e94b87f9c8a5cf6712a95a5a3a945fcd", + "bytes": 44024, + "mode": "100644", + "usage": "Inert mathematical provenance or retained source data; not executed or independently accepted." + }, + { + "local_path": "source/width-nine-input.json", + "source_repository": "petalas/integer-mult-bounds", + "source_commit": "c6252da020819a08ef2b2ff14280146c43ad374c", + "source_path": "research/clifford-transvection-conditioning/source/pr6714-result.json", + "git_blob": "77a5c8b23b91ed215b41cd2181a245d3f7d2374e", + "sha256": "308b8dee094eb5481565ea89698ed5df69edeeecd4b63b4d78cb9cecdbe71c27", + "bytes": 5463, + "mode": "100644", + "usage": "Inert mathematical provenance or retained source data; not executed or independently accepted." + }, + { + "local_path": "predecessor/PR6714-PROOF.md", + "source_repository": "alephnan/integer-mult-bounds", + "source_commit": "f7f32a18dde54e67624a9ed9cc7e1b266d9585c0", + "source_path": "research/clifford-three-qubit-threshold/PROOF.md", + "git_blob": "9f89ee36a0a1a0bdda09582d88477e15674fda5e", + "sha256": "d29091eb12b4ccd3f5acb389634a858af3beb0dc78865613bb7bd68c9440c6d0", + "bytes": 17137, + "mode": "100644", + "usage": "Inert mathematical provenance or retained source data; not executed or independently accepted." + }, + { + "local_path": "source/EXTERNAL.json", + "source_repository": "alephnan/integer-mult-bounds", + "source_commit": "f7f32a18dde54e67624a9ed9cc7e1b266d9585c0", + "source_path": "research/clifford-three-qubit-threshold/EXTERNAL.json", + "git_blob": "3fe07503d342e91a1cc0b35061b0ac84de31eb0e", + "sha256": "eb64deffd68787fe12df7b745d98f3139f77c5ab7ecd41a86bd832db0c7ebe0a", + "bytes": 1995, + "mode": "100644", + "usage": "Inert mathematical provenance or retained source data; not executed or independently accepted." + } + ] +} diff --git a/research/clifford-order3-conditioning/SOURCES.json b/research/clifford-order3-conditioning/SOURCES.json new file mode 100644 index 0000000000..c64cc0b47d --- /dev/null +++ b/research/clifford-order3-conditioning/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "files": [ + { + "path": "docs/research/agent-task-catalog.json", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81", + "usage": "provenance" + }, + { + "path": "certificates/selected-result.json", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa", + "usage": "provenance" + }, + { + "path": "LICENSE", + "usage": "provenance", + "git_blob": "261eeb9e9f8b2b4b0d119366dda99c6fd7d35c64", + "sha256": "c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4" + } + ], + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a" +} diff --git a/research/clifford-order3-conditioning/TASK.json b/research/clifford-order3-conditioning/TASK.json new file mode 100644 index 0000000000..7713c3dc56 --- /dev/null +++ b/research/clifford-order3-conditioning/TASK.json @@ -0,0 +1,127 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "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_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.", + "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse." + }, + "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": "Phase-correct order-three Clifford trace constraint and sufficient tensor-Gram condition bound16471/40=411.775 for every integer widthf>=10, under inherited representation/table premises; exact declared trace-relaxation extrema, not actual spectral endpoints.", + "scope_change_reason": "Take explicit PR6794 second-class handoff. Written native-algebra side result; no Lean proposition, actual caller or selected assumption discharge.", + "bottleneck_link": "Conditioning constrains coefficient recovery in the declared finite native alphabet. Physical implementation, complete signed invoice and selected admission remain separate.", + "budget_minutes": 120, + "stop_rule": "Stop after one actual order-three class/lift and its two-trace rational consequence. No full even-sector table, other classes, group enumeration or physical construction. At least30actualminutes after science freeze for verification/handoff.", + "outcome": "partial", + "evidence": "Written actual-lift/fixed-form/phase lemma and exact all-f>=10 sufficient condition16471/40. FirstnewrunPASS0.702s/24.3125MiB,64Pauliimages/64forms/4096distinctform-vectorcases/252vertices/four30rowdualcertificates/6controls. Final normal/O complete13000-byte packets agree SHA38380ddd9be74d0bf0beb6bd2c21a4dddbc7e78e94ffc3607c08bf421118771a. Three supporting row inequalities and matching primal mixtures certify relaxation extrema; actual spectrum unclaimed.", + "author": "ToikY with substantial OpenAI Codex assistance", + "ai_assistance": "Source-aware root proposal, proof/implementation, overlap/metadata and related-role challenge. Preclaim recipe exposed; no blind independent/human/proof-kernel acceptance.", + "selection": { + "kind": "explicit_handoff", + "source_pr": 6794, + "source_head": "c6252da020819a08ef2b2ff14280146c43ad374c", + "upstream_pr": 6714, + "upstream_head": "f7f32a18dde54e67624a9ed9cc7e1b266d9585c0", + "claim": "https://github.com/CrocSwap/integer-mult-bounds/pull/6794#issuecomment-6699582538", + "picker_draw": null + }, + "exposure": { + "preclaim_orientation": "Root provisionally considered paired transvections, guessed6/10 for the order-three candidate and8/8 for unselected commuting pair, and proposed actualhS lift/phase/one-sided trace recipe while reading sources before claim. Unaccepted then, no scientific execution; related AI roles see it.", + "excluded_prior_work": [ + "PR6714 width-nine decomposition/threshold/oldconstants", + "PR6794 one-transvection807 relaxation", + "own6718 even-sector review" + ], + "source_scientific_programs_executed": false, + "source_data_consumed": "Inert cited mathematical table/multiplicities/prose only; published group/table identification remains inherited.", + "post_first_receipt_schema_fix": "One key renamed form_vector_evaluations -> distinct_form_vector_pairs (4096), distinguishing grid cases from8192 healthyfunctioncalls. Complete typed packets otherwise identical; no arithmetic/source/LP/control change. First code/packet and pre-correction replays retained." + }, + "physical_obligations": { + "actual_caller": null, + "preparation_restoration_price": null, + "native_rank_and_recursive_child_conversion": null, + "complete_supplier_invoice": null + }, + "open_questions": [ + { + "question": "Do additional stabilizer multiplicity constraints determine the actual width-ten endpoints?", + "why_it_matters": "Convex trace-relaxation extrema need not be actual even-sector irreducibles.", + "first_step": "Bind one actual quadratic-form stabilizer representation/decomposition to the declared central sector before deriving actual endpoints.", + "blocked_by": "Full even-sector realization is not supplied or searched here." + }, + { + "question": "Can the improved formal conditioning interval be consumed by one actual source-bound caller?", + "why_it_matters": "An abstract tensor-Gram bound does not price preparation, recovery or restoration.", + "first_step": "Name the exact caller/alphabet/coefficients and supply its complete precision/movement/stock/ownership and recursive invoice.", + "blocked_by": "No actual physical caller is instantiated here." + } + ] +} diff --git a/research/clifford-order3-conditioning/VERIFY.json b/research/clifford-order3-conditioning/VERIFY.json new file mode 100644 index 0000000000..e8a555796d --- /dev/null +++ b/research/clifford-order3-conditioning/VERIFY.json @@ -0,0 +1,28 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "New exact one-lift/phase/64-quadratic-form and two-trace rational certificate corroboration; no predecessor program." + }, + { + "argv": [ + "{python}", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Same complete typed scientific packet with explicit optimized-mode guards." + } + ] +} diff --git a/research/clifford-order3-conditioning/predecessor/PR6714-PROOF.md b/research/clifford-order3-conditioning/predecessor/PR6714-PROOF.md new file mode 100644 index 0000000000..9f89ee36a0 --- /dev/null +++ b/research/clifford-order3-conditioning/predecessor/PR6714-PROOF.md @@ -0,0 +1,430 @@ +# The three-qubit Clifford tensor threshold is ten + +This is a scoped algebraic theorem about the complete Gaussian-dyadic +three-qubit Clifford alphabet. It gives no new multiplication exponent, +physical supplier, or implementation of the five assumptions retained by +the selected construction. Classical finite-group representation theory +and the cited character table are premises; the proof is not a proof-assistant +formalization or independent human review. + +## 1. Statement and conventions + +Let `D = Z[i,1/2]`, and let `G` be the group of all unitary three-qubit +Clifford matrices with entries in `D`. Its natural representation `V` has +dimension eight. Let `z=iI`. The scalar subgroup is + + Z = = {I,iI,-I,-iI}. + +Let `P` be the Pauli subgroup generated by `z` and the three pairs `X_j,Z_j`. +Then `|P|=256`, `G/P = Sp(6,2) = S`, and + + |S| = 1,451,520, + |G/Z| = 64 |S| = 92,897,280, + |G| = 4 |G/Z| = 371,589,120. + +The usual Pauli and symplectic conventions are those of the retained +pointwise-faithfulness and two-qubit-centre packages. The Gaussian-dyadic +group has scalar kernel `mu_4`, not `mu_8`. Indeed, if `(a+bi)/2^k` has +modulus one, successive parity division in `a^2+b^2=2^(2k)` reduces it to +one of the four Gaussian units. The Gaussian-dyadic gates `S`, +`((1+i)I+(1-i)X)/2`, and CNOT realize the standard symplectic generators; +thus the quotient is the full `Sp(6,2)`. The Pauli action determines a +Clifford up to scalar. + +Choose one unitary representative `U_a` for each `a in G/Z`, with `U_1=I`. +Define + + H_f(a,b) = (tr(U_a^* U_b)/8)^f, f = 1,2,... . + +This is the Gram matrix of `U_a^(tensor f)/8^(f/2)` in Hilbert-Schmidt +space. Changing the representatives conjugates `H_f` by a diagonal +unitary matrix and does not change its rank or spectrum. + +**Theorem.** The least width at which this projective alphabet is linearly +independent is exactly **ten**. Equivalently, its least eventual pointwise +threshold is + + T(3) = 10. + +At width nine the nullity is exactly `56^2 = 3,136`, so + + rank H_9 = 92,894,144. + +For every integer `f >= 10`, the following additional, nonoptimal bounds hold: + + (945/262144) I <= H_f <= (762615/32768) I. (1) + +The resulting Gram condition-number bound is 6,456. We do not claim sharp +spectral constants. In particular, the threshold is not the extrapolated +value `4n+1=13` suggested by the one- and two-qubit cases. + +## 2. Why tensor independence is an irreducible-support question + +For each `r mod 4`, let `A_r` be the central-character ideal of `C[G]` on +which `z` acts as `i^r`. Its dimension is `|G/Z|`, and one representative +per projective class gives a basis after projection to this ideal. +The representation `V^(tensor f)` annihilates the other three ideals. + +By semisimplicity, + + A_r = direct_sum_{rho : rho(z)=i^r I} End(rho). + +The representation of `A_r` is injective exactly when every irreducible +in this sector occurs. A missing irreducible of dimension `d` removes +an entire matrix block of dimension `d^2`. Thus + + rank H_f = sum_{rho occurring in V^(tensor f)} (dim rho)^2. (2) + +If `m_rho(f)` is its multiplicity, the normalized Gram eigenvalue on its +regular matrix block is + + lambda_rho(f) = |G/Z| m_rho(f) / (8^f dim rho). (3) + +One way to check the normalization is to use central convolution on all +of `G`, whose eigenvalue is `|G| m_rho(f)/dim rho`. Combining the four +scalar lifts multiplies the projective Gram by `4*8^f`; dividing gives +(3). The regular multiplicity is `(dim rho)^2`, not four times that value. + +## 3. The odd central sector and a smaller character calculation + +The Pauli group has a unique irreducible with `z` acting by `i`, namely +the eight-dimensional restriction of `V`. This follows directly from +the usual irreducible representation of the three Pauli pairs; its +matrix algebra has dimension 64. Consequently every irreducible of `G` +in central sector `i` has the unique form + + V tensor sigma, sigma in Irr(S). (4) + +For completeness, for such a representation `R`, the multiplicity space +`Hom_P(V,R)` carries the honest quotient action + + g . phi = R(g) phi V(g)^(-1). + +Pauli elements act trivially on this space. Evaluation identifies +`R` with `V tensor Hom_P(V,R)`, and irreducibility on one side is equivalent +to irreducibility of the multiplicity space. No splitting of `G` over `P` +is being assumed. The actual natural representation supplies the extension +needed in (4). + +Let `s in S`, and put `d(s)=dim_F2 ker(s-I)`. Among the 64 projective +Pauli lifts of `s`, exactly `2^(6-d(s))` have nonzero trace; on each such +lift `g`, + + |tr V(g)|^2 = 2^d(s). (5) + +To recall the argument, conjugation on the Hermitian Pauli basis is a +signed permutation. Its trace is `|tr V(g)|^2`. The signs on the fixed +label space form a binary character, so their sum is zero or `2^d`. +Multiplication by Paulis runs through all its characters equally often. +In particular there is always a nonzero-trace lift. + +For a Gaussian-dyadic number of squared modulus `2^d`, its fourth power is + + (tr V(g))^4 = (-1)^d 2^(2d). (6) + +This includes the phase: writing the number as `(a+bi)/2^k`, the equation +`a^2+b^2=2^(d+2k)` implies that, after removing common powers of two, +either one coordinate is zero or the coordinates have equal absolute +value. The two cases give the sign in (6). + +For `f=4t+1`, write + + V^(tensor f) = V tensor W_f. + +The quotient representation `W_f` is honest, and the character product +on a nonzero-trace lift gives + + chi_W_f(s) = (-1)^(dt) 2^(2dt). (7) + +In particular, + + chi_W_9(s) = 2^(4d(s)). (8) + +This is also the permutation character of `S` acting on ordered +four-tuples of vectors in `F_2^6`. Thus the width-nine input to the proof +is an ordinary 30-character calculation for `Sp(6,2)`, rather than a +92,897,280-by-92,897,280 Gram calculation. + +## 4. Exact width-nine decomposition + +We use the published character table of Chin-Yen Lee, Wei-Hsuan Yu, +Yung-Ning Peng and Ching-Jui Lai, [arXiv:2309.14850v2](https://arxiv.org/html/2309.14850v2#S6.SS3), Section 6.3, +and its Section 5.2 identification of the adjoint character as +`1 + chi_10`. The package retains the exact transcribed table and the +class-fibre extraction. Inflated characters are those trivial on the +64-element projective Pauli subgroup. The executable checks character +orthogonality, class and degree sums, the quotient extraction, fixed-space +trace data, and every integer inner product below. Those checks validate +the transcription and calculation; they do not independently reconstruct +the published character table from group multiplication. + +More explicitly, the nonidentity projective Paulis constitute one +63-element conjugacy class. A character is trivial on this subgroup +exactly when its value on that class equals its degree: equality in the +unitary trace bound forces the matrix to be the identity. These are +precisely the inflated quotient irreducibles. Two source classes have the +same quotient class exactly when all these characters agree, since +irreducible characters separate conjugacy classes. Each quotient class +size is the sum of its source class sizes divided by 64. Finally, the +maximum of the adjoint value `1+chi_10` over a quotient fibre is `2^d` +by (5). This identifies the fixed-space data used in (8), including the +63-element transvection class, without inferring `d` from class order alone. + +Taking inner products of (8) with the quotient characters gives the +following complete list. Repeated degrees denote distinct irreducibles, +in their retained source order. + +| Degree | Multiplicity in `W_9` | +|---:|---:| +| 1 | 269 | +| 7 | 0 | +| 15 | 85 | +| 21 | 35 | +| 21 | 840 | +| 27 | 1890 | +| 35 | 1975 | +| 35 | 175 | +| 56 | 28 | +| 70 | 350 | +| 84 | 1407 | +| 105 | 210 | +| 105 | 2625 | +| 105 | 1575 | +| 120 | 3900 | +| 168 | 4410 | +| 189 | 945 | +| 189 | 567 | +| 189 | 2835 | +| 210 | 5250 | +| 210 | 2625 | +| 216 | 1728 | +| 280 | 5600 | +| 280 | 1400 | +| 315 | 1575 | +| 336 | 2940 | +| 378 | 2835 | +| 405 | 6075 | +| 420 | 5250 | +| 512 | 5440 | + +The multiplicity-weighted dimensions sum to `8^8=16,777,216`. Let `sigma_0` denote the sole +missing character, of degree seven. On a symplectic transvection `tau`, + + chi_sigma_0(tau) = -5. (9) + +This is the class of size 63 with fixed-space dimension five. The +nonzero multiplicities in the table also satisfy + + (1/2) dim sigma <= m_sigma(9) <= 269 dim sigma. (10) + +The only missing irreducible in `V^(tensor 9)` is therefore +`rho_0=V tensor sigma_0`, of dimension 56. Equation (2) proves the +claimed nullity and rank. + +There is an explicit null witness. For a projective representative `U_a`, +let `s_a` be its symplectic image and define + + b_a = chi_rho_0(U_a^(-1)) + = conjugate(tr V(U_a) * chi_sigma_0(s_a)). + +Then + + sum_a b_a U_a^(tensor 9) = 0. (11) + +Indeed, the central primitive idempotent + + (56/|G|) sum_{g in G} chi_rho_0(g^(-1)) [g] + +acts as zero in `V^(tensor 9)`. Grouping its four scalar lifts gives +(11), since their factors `i^(-j)` and `i^(9j)` cancel. This is a +nonzero coefficient vector: its coefficient at the identity is 56. +It is a width-nine relation, not an all-width identity. + +## 5. The even sector is controlled by quadratic forms + +Consider any irreducible `mu` of `G` with `mu(z)=-I`, the sector of +`V^(tensor 10)`. Its restriction to `P` is a sum of one-dimensional +characters because `[P,P]=<-I>` and `mu(-I)=I`. + +Write a binary label as `v=(a,b)` and use the Hermitian Pauli convention + + W_v = i^(a.b) X^a Z^b. + +The one-dimensional characters with `z` acting by `-1` are indexed by +the 64 quadratic forms with polar form the standard symplectic form: + + Q_(alpha,beta)(a,b) = a.b + alpha.a + beta.b, + lambda_Q(W_v) = (-1)^Q(v). + +In a Clifford conjugation `W_v -> +/- W_(s v)`, the sign has no effect +on `lambda_Q`, since it sends `-I` to one. The quotient therefore acts +on these characters by its ordinary action on quadratic forms. + +There are exactly two orbits, distinguished by Arf invariant, + + Arf Q_(alpha,beta) = alpha.beta. + +Their sizes are 36 and 28. This is the standard symplectic classification +of nondegenerate binary quadratic forms: choosing successive hyperbolic +pairs gives one normal form for each Arf value. The counts also follow +directly by summing over `alpha,beta`. + +Since `mu` is irreducible, its Pauli character spaces form one transitive +orbit and have a common dimension `a>=1`. Hence for one `N in {28,36}`, + + mu restricted to P = a sum_{Q in orbit} lambda_Q, + dim mu = N a. (12) + +For a nonzero vector `v`, the symplectic transvection is + + tau_v(x) = x + omega(x,v) v. + +The quadratic identity gives + + Q(tau_v x) = Q(x) + omega(x,v)(Q(v)+1). + +Thus a form is fixed exactly when `Q(v)=1`. Each Arf orbit has exactly +16 such forms. For example, use symplectic coordinates with `v=e_1`. +Then `alpha_1=1`; the four coordinates +`alpha_2,alpha_3,beta_2,beta_3` are arbitrary, and `beta_1` is uniquely +fixed by the prescribed Arf invariant. + +Any Clifford lift `g` of this transvection permutes the Pauli character +spaces. Only the sixteen fixed spaces contribute to its trace. Since +the representation can be made unitary, each contributes absolute trace +at most `a`. Consequently + + |chi_mu(g)| <= 16 a. (13) + +This bound uses neither the character table of the even central sector +nor extensions of its stabilizer representations. + +## 6. Every irreducible occurs at width ten + +Suppose, for contradiction, that `mu` is missing from `V^(tensor 10)`. +Tensor reciprocity gives + + = . + +The representation on the right has central character `i`. The sole +irreducible absent from `V^(tensor 9)` is `rho_0`. All multiplicities are +nonnegative integers, so absence forces + + conjugate(V) tensor mu = m rho_0, m >= 1. + +Dimensions give `7m=Na`. Take `g=S` on the first qubit and the identity +on the other two. Its symplectic image is a transvection and +`tr V(g)=4(1+i)` is nonzero. The character identity and (9) imply + + |chi_mu(g)| = 5m = (5N/7)a. + +For `N=28` this is `20a`; for `N=36` it is `180a/7`. Both exceed `16a`, +contradicting (13). Therefore no even-sector irreducible is missing. +By Section 2, `H_10` is positive definite. + +This argument is also a useful check against a phase error: conjugate `V`, +not `V`, is used in reciprocity, and the relevant Pauli character orbit is +the quadratic-form orbit for central character `-1`. + +## 7. Quantitative bounds and every larger width + +The same reasoning gives (1) without computing the full even-sector +spectrum. Decompose + + conjugate(V) tensor mu = sum_sigma n_sigma (V tensor sigma), + d_mu := dim mu = sum_sigma n_sigma dim sigma. + +Let `n_0` be the coefficient of the missing degree-seven character and +put `R=d_mu-7n_0`. At the transvection lift used above, the character +identity and the elementary bound +`|chi_sigma(tau)|<=dim sigma` give + + 12n_0-d_mu + = 5n_0-R + <= |sum_sigma n_sigma chi_sigma(tau)| + = |chi_mu(g)| + <= 16a. + +The first inequality is valid even when its left side is negative. +Using `d_mu=Na` and `N in {28,36}` yields + + R >= a(5N-112)/12 >= d_mu/12. + +Reciprocity and (10) now show + + d_mu/24 <= m_mu(10) <= 269 d_mu. + +Substituting into (3) gives precisely (1) at width ten. The lower bound +also proves positivity directly. + +Finally, + + H_(f+1) = H_f Hadamard H_1. + +The Schur product theorem and the unit diagonal of `H_1` imply + + alpha I <= H_f <= beta I + => alpha I <= H_(f+1) <= beta I. + +This proves (1), hence independence, at every `f>=10`. If any smaller +positive width were independent, the same Schur step would make width +nine independent, contrary to Section 4. The threshold is therefore +exactly ten, not just an upper bound. + +## 8. Four fixed-residual tests with exact phases + +Let a fixed residual in `C[G]` have coefficients `c_(a,j)` on the exact +operators `i^j U_a`, after equal operators are combined. For `r mod 4`, set + + beta_(a,r) = sum_{j=0}^3 c_(a,j) i^(jr). + +At width `f`, its operator evaluation is + + sum_a beta_(a,f mod 4) U_a^(tensor f). + +Pointwise independence at the four widths `10,11,12,13` makes these +evaluations zero exactly when all four sets of `beta` coefficients are +zero. Fourier inversion then gives `c_(a,j)=0` for every exact operator. +Consequently the following are equivalent for a fixed residual: + +1. Every exact-operator coefficient vanishes. +2. Its evaluation vanishes at every positive tensor width. +3. Its evaluations vanish at widths 10, 11, 12 and 13. + +If `M=sum_(a,j)|c_(a,j)|^2`, Parseval and (1) imply that at least one of +those four evaluations has normalized squared Hilbert-Schmidt norm at +least `(945/262144) M`. Coefficients must be fixed for this four-test +statement; pointwise independence itself allows coefficients to depend +on the chosen width. + +Four residue classes remain necessary for unrestricted fixed residuals: +`sum_j i^(-rj)[i^j I]` vanishes outside residue `r` and is nonzero in that +residue. The four-test count and the scalar Fourier argument are retained +predecessor principles; this theorem supplies the earlier sufficient window. + +## 9. Scope and attribution + +The alphabet is the full projective three-qubit Clifford group, with arbitrary +complex coefficients at a fixed width. The theorem is not a statement about +arbitrary sums of Cliffords as individual alphabet elements, operators coupling +tensor columns, nonlinear rounded gates, or nonunitary stabilizer maps. +It supplies no paid-call bound without a separate source-bound caller argument. +The selected conditional multiplication result and its five assumptions are +unchanged. + +Ali Romman's pointwise-faithfulness package supplies the general Clifford +framework, trace distribution, phase-residue interpretation, and open sharp +threshold question. MatShep's one- and two-qubit packages supply the earlier +sharp cases and the Schur-propagation method. The linear-lower-bound package +records the unresolved three-qubit case. The authors of arXiv:2309.14850 +supply the published character table and adjoint identification; their table +is a cited mathematical input, not newly constructed here. Pauli representation +theory, tensor reciprocity, character orthogonality, binary quadratic-form +classification, central idempotents and the Schur product theorem are classical. + +The new contribution is the exact width-nine decomposition and its missing +block, the even-sector transvection argument proving full support at ten, +and their quantitative and fixed-residual consequences. Prepared with +substantial OpenAI Codex assistance and separate agent proof/checking work. +No independent human acceptance or proof-kernel certification is claimed. +New material is Apache-2.0; retained sources keep their attribution and license. diff --git a/research/clifford-order3-conditioning/predecessor/PR6794-PROOF.md b/research/clifford-order3-conditioning/predecessor/PR6794-PROOF.md new file mode 100644 index 0000000000..60a16b0578 --- /dev/null +++ b/research/clifford-order3-conditioning/predecessor/PR6794-PROOF.md @@ -0,0 +1,178 @@ +# A transvection certificate for three-qubit conditioning + +## Statement and inherited mathematical inputs + +Use the full Gaussian-dyadic three-qubit Clifford alphabet and conventions of +[alephnan's PR6714](https://github.com/CrocSwap/integer-mult-bounds/pull/6714), +at head `f7f32a18dde54e67624a9ed9cc7e1b266d9585c0`. For representatives +`U_a` of its 92,897,280 projective classes, put + +\[ + H_f(a,b)=\left(\operatorname{tr}(U_a^*U_b)/8\right)^f. +\] + +For every integer `f >= 10`, this package proves the sufficient bounds + +\[ + \boxed{\frac{2835}{131072}I\preceq H_f + \preceq\frac{2287845}{131072}I.} \tag{1} +\] + +Consequently the spectral condition number is at most **807**. +The predecessor's sufficient bounds were `945/262144` and `762615/32768`, +with ratio 6,456. The lower bound in (1) is six times larger and the upper +bound is three quarters as large. No optimality for the actual spectrum is claimed. + +The following are cited predecessor results, rather than claims reproved here. +They are in its [PROOF.md, Sections 2 through 7](https://github.com/CrocSwap/integer-mult-bounds/blob/f7f32a18dde54e67624a9ed9cc7e1b266d9585c0/research/clifford-three-qubit-threshold/PROOF.md). + +1. Let `V` be the natural eight-dimensional representation, and `sigma` run + over the thirty irreducible characters of `Sp(6,2)`. The odd central-sector + irreducibles are `V tensor sigma`. Their multiplicities in `V^(tensor 9)` + are the nonnegative integers `m_sigma` retained in the source result. +2. If `mu` is an even-sector irreducible relevant at width ten, then + + \[ + \overline V\otimes\mu + =\bigoplus_\sigma n_\sigma(V\otimes\sigma),\qquad n_\sigma\ge0. + \] + + Write `d_sigma = dim sigma` and `d = dim mu`. Dimensions and reciprocity give + + \[ + d=\sum_\sigma n_\sigma d_\sigma,\qquad + m_\mu(10)=\sum_\sigma n_\sigma m_\sigma. \tag{2} + \] + +3. There is `N` equal to 28 or 36 and an integer `a >= 1` with `d=Na`. + For a transvection `tau` of `Sp(6,2)`, set + + \[ + T=\sum_\sigma n_\sigma\chi_\sigma(\tau). + \] + + Then `|T| <= 16a = 16d/N`. This follows because exactly sixteen quadratic + forms in either Pauli-character orbit are fixed by a transvection. + In the source's phase convention, the quotient-character sum differs from + the character of `mu` at its Clifford lift by a scalar of absolute value one. +4. The eigenvalue on the regular matrix block of `mu` is + + \[ + \lambda_\mu(10)=\frac{92897280}{8^{10}} + \frac{m_\mu(10)}{d}. \tag{3} + \] + + Also `H_(f+1) = H_f circ H_1`, where `circ` is the Schur product, + `H_1` is positive semidefinite, and its diagonal is one. + +The exact source numerical files are retained unchanged. Their origin and hashes +are in [ORIGIN.json](ORIGIN.json). The published character table is due to +Chin-Yen Lee, Wei-Hsuan Yu, Yung-Ning Peng and Ching-Jui Lai. This proof uses +the predecessor's identification and multiplicities as inputs. It does not +reconstruct the table, audit that identification, or rerun its decomposition. + +## The new finite certificate + +For every one of the thirty types, write `t_sigma = chi_sigma(tau)`. The +retained data satisfy the two integer inequalities + +\[ + 4m_\sigma-5d_\sigma-7t_\sigma\ge0,\qquad + 1345d_\sigma+1883t_\sigma-12m_\sigma\ge0. \tag{4} +\] + +These are the new supporting lines. The verifier reads the cited width-nine +multiplicities and the transvection column, evaluates every residual in (4) +exactly, and prints all thirty pairs. This is a finite arithmetic certificate +for new inequalities in the predecessor data, rather than another verification +of its threshold or multiplicity calculation. + +The source row numbers and the three tight data points explain the constants: + +| source row | `d_sigma` | `t_sigma` | `m_sigma` | +| --- | ---: | ---: | ---: | +| 1 | 1 | 1 | 269 | +| 2 | 7 | -5 | 0 | +| 9 | 56 | -24 | 28 | + +The lower supporting line passes through normalized rows 2 and 9. The upper +supporting line passes through normalized rows 1 and 2. Checking only these +three points would be insufficient; (4) is checked for **every** type. + +Multiply (4) by the nonnegative integers `n_sigma` and sum. By (2), + +\[ + \frac54d+\frac74T\le m_\mu(10) + \le\frac{1345}{12}d+\frac{1883}{12}T. \tag{5} +\] + +Both slopes are positive. Applying `-16d/N <= T <= 16d/N` gives + +\[ + \left(\frac54-\frac{28}{N}\right)d + \le m_\mu(10) + \le\left(\frac{1345}{12}+\frac{7532}{3N}\right)d. \tag{6} +\] + +Thus the two orbit-specific intervals for `m_mu(10)/d` are + +| `N` | lower bound | upper bound | +| --- | ---: | ---: | +| 28 | 1/4 | 807/4 | +| 36 | 17/36 | 19637/108 | + +The first interval contains the second. Since +`92897280/8^10 = 2835/32768`, (3) proves (1) at width ten. + +For propagation, if `alpha I <= H_f <= beta I`, Schur positivity gives + +\[ + (H_f-\alpha I)\circ H_1\succeq0,\qquad + (\beta I-H_f)\circ H_1\succeq0. +\] + +The unit diagonal means `I circ H_1=I`. Therefore the same interval holds at +`f+1`, proving (1) for every `f >= 10`. This is a written universal implication +from the stated representation-theoretic inputs, not a finite-width extrapolation. + +## What is sharp, and what is still open + +The two bounds in (6) are sharp for the following **relaxation only**. Assign +arbitrary nonnegative weights `x_sigma` summing to one, retain the thirty points + +\[ + (r_\sigma,c_\sigma)=(t_\sigma/d_\sigma,m_\sigma/d_\sigma), + \qquad \left|\sum_\sigma x_\sigma r_\sigma\right|\le16/N, +\] + +and minimize or maximize `sum x_sigma c_sigma`. The following explicit mixtures +attain all four bounds; weights refer to the indicated source rows. + +| `N` | extremum | nonzero weights | +| --- | --- | --- | +| 28 | minimum | row 2: 1/2; row 9: 1/2 | +| 28 | maximum | row 1: 3/4; row 2: 1/4 | +| 36 | minimum | row 2: 1/18; row 9: 17/18 | +| 36 | maximum | row 1: 73/108; row 2: 35/108 | + +Together with (4), these mixtures prove the relaxed optimum, including its +orientation at the two ends of the trace interval. The independent primal route +in the verifier lists every simplex vertex in the trace slab and every intersection +of a simplex edge with its two bounding hyperplanes. These cover the vertices: +at a vertex, at most two weights can be positive since there is the sum constraint +and at most one active trace constraint. If two trace coordinates coincide, a +nontrivial edge interior is not a vertex. All arithmetic is rational. + +The relaxation discards additional representation and multiplicity constraints. +Its attaining mixtures are not claimed to come from any actual irreducible `mu`. +In particular **807 is a sufficient uniform bound, not the exact condition +number**, and neither endpoint is claimed to be an actual eigenvalue. + +## Scope + +This is a scoped native-algebra conditioning theorem with exact finite +corroboration. It does not improve the already proved threshold ten. It supplies +no new paid-call construction, recursive invoice, physical implementation, +selected supplier admission or multiplication exponent. All five selected +framework assumptions retain their status. Independent human and formal +proof-kernel review are unclaimed. diff --git a/research/clifford-order3-conditioning/source/EXTERNAL.json b/research/clifford-order3-conditioning/source/EXTERNAL.json new file mode 100644 index 0000000000..3fe07503d3 --- /dev/null +++ b/research/clifford-order3-conditioning/source/EXTERNAL.json @@ -0,0 +1,31 @@ +{ + "schema": "external-mathematical-data/v1", + "source": { + "title": "On character table of Clifford groups", + "authors": [ + "Chin-Yen Lee", + "Wei-Hsuan Yu", + "Yung-Ning Peng", + "Ching-Jui Lai" + ], + "arxiv": "2309.14850v2", + "url": "https://arxiv.org/html/2309.14850v2", + "section": "6.3", + "retrieved_utc": "2026-11-04", + "html_sha256": "02e0adebe50fcb4ff3cb1112600094d77c9457c45707df041486cbb4491c2a2e", + "description": "Numerical mathematical table entries extracted from six HTML panels, in published character and conjugacy-class order. No article prose is redistributed.", + "tex_source_url": "https://arxiv.org/src/2309.14850v2", + "tex_sha256": "caa1e0449ef7575fc4c516238e939effb309038c45ae6f3d41f64206b9619de3", + "source_gzip_sha256": "c0b319313270000da28a9dd5c8358144dd613285ad7d6cdfabb1c9e409ab84f7", + "cross_check": "All 4489 numerical entries independently extracted from original TeX agree with the HTML transcription." + }, + "table_sha256": "388d617a76e345774a8768f32a6a9bc6e94b87f9c8a5cf6712a95a5a3a945fcd", + "identifications": { + "projective_group": "C_3 in the paper; quotient of the finite Gaussian-dyadic Clifford group by scalar fourth roots", + "adjoint": "Section 5.2: conjugation representation M_8 has character chi_1 + chi_10", + "normal_Pauli_subgroup": "Section 5.2 and Theorem 5.5: unique proper nontrivial normal subgroup has order64; the identity and class2 of size63", + "character_table": "Section6.3, characters1..67 and classes1..67 in published order" + }, + "reproduce_extraction": "python -B research/clifford-three-qubit-threshold/extract_table.py /path/to/2309.14850v2.html", + "scope": "The published character-table identification is cited, not independently reconstructed. Orthogonality and integrality checks detect corruption but do not establish that an abstract array is the character table of a named group. Only numerical mathematical facts are included, not article text." +} diff --git a/research/clifford-order3-conditioning/source/table.json b/research/clifford-order3-conditioning/source/table.json new file mode 100644 index 0000000000..01f56d329a --- /dev/null +++ b/research/clifford-order3-conditioning/source/table.json @@ -0,0 +1,4649 @@ +{ + "schema": "published-character-table/v1", + "source": { + "title": "On character table of Clifford groups", + "authors": [ + "Chin-Yen Lee", + "Wei-Hsuan Yu", + "Yung-Ning Peng", + "Ching-Jui Lai" + ], + "arxiv": "2309.14850v2", + "url": "https://arxiv.org/html/2309.14850v2", + "section": "6.3", + "retrieved_utc": "2026-11-04", + "html_sha256": "02e0adebe50fcb4ff3cb1112600094d77c9457c45707df041486cbb4491c2a2e", + "description": "Numerical mathematical table entries extracted from six HTML panels, in published character and conjugacy-class order. No article prose is redistributed." + }, + "order": 92897280, + "adjoint_character_rows": [ + 1, + 10 + ], + "pauli_nonidentity_class": 2, + "characters": [ + [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ], + [ + 7, + 7, + -2, + 1, + 3, + 3, + 3, + 3, + 4, + 4, + -3, + -3, + -3, + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 1, + -1, + -1, + -1, + 2, + 2, + 1, + 1, + -1, + -1, + -5, + -5, + -5, + 1, + 1, + -1, + -1, + -1, + -1, + -1, + -1, + 3, + 3, + 2, + 0, + 2, + 2, + 0, + 0, + -1, + -1, + -1, + -1, + -1, + 1, + 1, + 1, + 1, + 1, + 1, + -1, + -2, + -2, + -2, + -2, + -2, + 0 + ], + [ + 15, + 15, + -3, + 0, + 3, + 3, + 3, + 3, + 0, + 0, + 1, + 1, + 1, + 0, + 0, + 0, + -2, + -2, + -3, + -3, + -3, + 7, + 7, + 7, + -2, + -2, + 3, + 3, + 1, + 1, + -5, + -5, + -5, + 1, + 1, + -1, + -1, + -1, + -1, + -1, + -1, + -1, + -1, + 1, + -1, + 0, + 0, + 0, + 0, + 1, + 1, + 3, + 3, + 3, + -1, + -1, + 1, + 1, + 1, + 1, + 0, + -2, + -2, + -2, + 0, + 0, + 1 + ], + [ + 21, + 21, + 3, + 0, + 5, + 5, + 5, + 5, + 6, + 6, + -3, + -3, + -3, + 2, + 2, + 2, + 0, + 0, + -3, + -3, + -3, + 5, + 5, + 5, + 2, + 2, + 0, + 0, + 2, + 2, + -11, + -11, + -11, + -2, + -2, + -3, + -3, + -3, + -3, + 0, + 0, + 1, + 1, + -1, + 1, + 1, + 1, + -1, + -1, + -1, + -1, + 1, + 1, + 1, + -1, + -1, + 1, + 1, + 1, + 1, + 1, + -2, + -2, + -2, + 0, + 0, + 0 + ], + [ + 21, + 21, + 3, + 0, + 1, + 1, + 1, + 1, + 6, + 6, + 3, + 3, + 3, + -2, + -2, + -2, + 0, + 0, + -1, + -1, + -1, + -3, + -3, + -3, + 0, + 0, + 0, + 0, + 0, + 0, + 9, + 9, + 9, + 0, + 0, + -3, + -3, + -3, + -3, + 0, + 0, + 5, + 5, + 3, + -1, + 1, + 1, + -1, + -1, + -1, + -1, + 1, + 1, + 1, + 1, + 1, + -1, + -1, + -1, + -1, + 1, + 0, + 0, + 0, + 2, + 2, + 0 + ], + [ + 27, + 27, + 0, + 0, + 7, + 7, + 7, + 7, + 9, + 9, + 5, + 5, + 5, + 1, + 1, + 1, + -1, + -1, + 1, + 1, + 1, + 3, + 3, + 3, + 3, + 3, + 0, + 0, + 0, + 0, + 15, + 15, + 15, + 0, + 0, + 3, + 3, + 3, + 3, + 0, + 0, + 3, + 3, + 0, + 0, + 2, + 2, + 0, + 0, + 1, + 1, + -1, + -1, + -1, + -1, + -1, + 1, + 1, + 1, + 1, + -1, + 3, + 3, + 3, + 1, + 1, + -1 + ], + [ + 35, + 35, + -1, + -1, + 7, + 7, + 7, + 7, + 5, + 5, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 5, + 5, + 5, + 11, + 11, + 11, + -1, + -1, + 2, + 2, + 2, + 2, + 15, + 15, + 15, + 0, + 0, + 3, + 3, + 3, + 3, + 0, + 0, + -1, + -1, + -1, + -1, + 0, + 0, + 0, + 0, + -1, + -1, + 3, + 3, + 3, + 1, + 1, + 1, + 1, + 1, + 1, + 0, + 3, + 3, + 3, + -1, + -1, + 0 + ], + [ + 35, + 35, + -1, + -1, + -5, + -5, + -5, + -5, + 5, + 5, + -1, + -1, + -1, + 1, + 1, + 1, + -1, + -1, + -1, + -1, + -1, + 3, + 3, + 3, + -3, + -3, + 2, + 2, + 0, + 0, + -5, + -5, + -5, + -2, + -2, + 3, + 3, + 3, + 3, + 0, + 0, + 7, + 7, + 3, + 1, + 0, + 0, + 0, + 0, + 1, + 1, + -1, + -1, + -1, + 1, + 1, + -1, + -1, + -1, + -1, + 0, + 1, + 1, + 1, + -1, + -1, + 0 + ], + [ + 56, + 56, + 2, + -1, + 8, + 8, + 8, + 8, + 11, + 11, + -4, + -4, + -4, + -1, + -1, + -1, + -1, + -1, + 4, + 4, + 4, + -8, + -8, + -8, + 1, + 1, + 2, + 2, + -2, + -2, + -24, + -24, + -24, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + -2, + 0, + 1, + 1, + 1, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + -3, + -3, + -3, + 1, + 1, + 0 + ], + [ + 63, + -1, + 0, + 0, + -1, + -1, + -1, + 15, + -1, + 15, + -1, + -1, + 7, + 3, + -1, + -1, + -1, + 1, + -1, + -1, + 7, + -1, + 15, + -1, + -1, + 3, + 3, + -1, + -1, + 3, + -1, + 31, + -1, + -1, + 1, + -1, + 7, + -1, + -1, + -1, + 1, + 3, + -1, + 0, + 0, + -1, + 3, + 1, + -1, + 1, + -1, + 3, + -1, + -1, + -1, + 1, + -1, + 3, + -1, + -1, + 0, + -1, + -1, + 7, + 1, + -1, + 0 + ], + [ + 63, + -1, + 0, + 0, + -1, + -5, + 3, + 11, + -1, + 15, + 1, + 1, + -7, + -1, + -1, + 3, + 1, + -1, + 1, + -3, + 5, + -1, + -9, + 7, + -1, + 3, + 3, + -1, + 1, + -3, + -1, + -29, + 3, + -1, + 1, + -1, + -1, + 3, + -5, + 1, + -1, + 3, + -1, + 0, + 0, + -1, + 3, + 1, + -1, + -1, + 1, + -1, + -1, + 3, + -1, + 1, + 1, + 1, + 1, + -3, + 0, + -1, + 3, + -5, + -1, + 1, + 0 + ], + [ + 70, + 70, + 7, + 1, + 6, + 6, + 6, + 6, + -5, + -5, + 2, + 2, + 2, + 3, + 3, + 3, + -1, + -1, + 2, + 2, + 2, + -10, + -10, + -10, + -1, + -1, + 1, + 1, + -1, + -1, + -10, + -10, + -10, + -1, + -1, + -2, + -2, + -2, + -2, + 1, + 1, + 2, + 2, + -1, + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 2, + 2, + 2, + 0, + 0, + -2, + -2, + -2, + -2, + 0, + -1, + -1, + -1, + -1, + -1, + 0 + ], + [ + 84, + 84, + 3, + 0, + 4, + 4, + 4, + 4, + -6, + -6, + 0, + 0, + 0, + -2, + -2, + -2, + 0, + 0, + 0, + 0, + 0, + 20, + 20, + 20, + 2, + 2, + 3, + 3, + -1, + -1, + 4, + 4, + 4, + 1, + 1, + 4, + 4, + 4, + 4, + 1, + 1, + 4, + 4, + -1, + 1, + -1, + -1, + -1, + -1, + 0, + 0, + 4, + 4, + 4, + 0, + 0, + 0, + 0, + 0, + 0, + -1, + -2, + -2, + -2, + 0, + 0, + 0 + ], + [ + 105, + 105, + -3, + 0, + 5, + 5, + 5, + 5, + 15, + 15, + -5, + -5, + -5, + -1, + -1, + -1, + 1, + 1, + -1, + -1, + -1, + 1, + 1, + 1, + 1, + 1, + -3, + -3, + 1, + 1, + -35, + -35, + -35, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 5, + 5, + 1, + -1, + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 1, + 1, + -1, + -1, + -1, + -1, + -1, + -1, + 0, + 1, + 1, + 1, + -1, + -1, + 0 + ], + [ + 105, + 105, + 6, + 0, + 9, + 9, + 9, + 9, + 0, + 0, + -3, + -3, + -3, + 0, + 0, + 0, + 0, + 0, + -3, + -3, + -3, + -7, + -7, + -7, + -4, + -4, + 3, + 3, + -1, + -1, + 25, + 25, + 25, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + -3, + -3, + 2, + 0, + 0, + 0, + 0, + 0, + -1, + -1, + -3, + -3, + -3, + -1, + -1, + 1, + 1, + 1, + 1, + 0, + 4, + 4, + 4, + 0, + 0, + 0 + ], + [ + 105, + 105, + 6, + 0, + -3, + -3, + -3, + -3, + 0, + 0, + -1, + -1, + -1, + 0, + 0, + 0, + 2, + 2, + 3, + 3, + 3, + 17, + 17, + 17, + 2, + 2, + 3, + 3, + -1, + -1, + 5, + 5, + 5, + -1, + -1, + -7, + -7, + -7, + -7, + -1, + -1, + -3, + -3, + 2, + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 1, + 1, + -1, + -1, + -1, + -1, + -1, + -1, + 0, + 2, + 2, + 2, + 0, + 0, + 0 + ], + [ + 120, + 120, + -6, + 0, + 8, + 8, + 8, + 8, + 15, + 15, + 4, + 4, + 4, + -1, + -1, + -1, + 1, + 1, + -4, + -4, + -4, + -8, + -8, + -8, + 1, + 1, + 0, + 0, + -2, + -2, + 40, + 40, + 40, + -2, + -2, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + -2, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 1, + -1, + -1, + 1 + ], + [ + 168, + 168, + 6, + 0, + 8, + 8, + 8, + 8, + 6, + 6, + 0, + 0, + 0, + 2, + 2, + 2, + 0, + 0, + 0, + 0, + 0, + 8, + 8, + 8, + 2, + 2, + -3, + -3, + -1, + -1, + 40, + 40, + 40, + 1, + 1, + 8, + 8, + 8, + 8, + -1, + -1, + 0, + 0, + 2, + 0, + -2, + -2, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + -2, + -2, + -2, + 0, + 0, + 0 + ], + [ + 189, + 189, + 0, + 0, + 1, + 1, + 1, + 1, + 9, + 9, + -1, + -1, + -1, + 1, + 1, + 1, + -1, + -1, + -5, + -5, + -5, + 21, + 21, + 21, + 3, + 3, + 0, + 0, + 0, + 0, + -39, + -39, + -39, + 0, + 0, + -3, + -3, + -3, + -3, + 0, + 0, + -3, + -3, + 0, + 0, + -1, + -1, + 1, + 1, + -1, + -1, + 1, + 1, + 1, + 1, + 1, + -1, + -1, + -1, + -1, + -1, + 3, + 3, + 3, + 1, + 1, + 0 + ], + [ + 189, + 189, + 0, + 0, + 13, + 13, + 13, + 13, + 9, + 9, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + -3, + -3, + -3, + -3, + -3, + 0, + 0, + 0, + 0, + -51, + -51, + -51, + 0, + 0, + -3, + -3, + -3, + -3, + 0, + 0, + -3, + -3, + 0, + 0, + -1, + -1, + -1, + -1, + 1, + 1, + -3, + -3, + -3, + 1, + 1, + 1, + 1, + 1, + 1, + -1, + -3, + -3, + -3, + 1, + 1, + 0 + ], + [ + 189, + 189, + 0, + 0, + -11, + -11, + -11, + -11, + 9, + 9, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + -3, + -3, + -3, + -3, + -3, + 0, + 0, + 0, + 0, + 21, + 21, + 21, + 0, + 0, + -3, + -3, + -3, + -3, + 0, + 0, + 9, + 9, + 0, + 0, + -1, + -1, + 1, + 1, + -1, + -1, + 1, + 1, + 1, + -1, + -1, + 1, + 1, + 1, + 1, + -1, + -3, + -3, + -3, + 1, + 1, + 0 + ], + [ + 210, + 210, + 3, + 0, + 2, + 2, + 2, + 2, + 15, + 15, + 2, + 2, + 2, + -1, + -1, + -1, + -1, + -1, + 2, + 2, + 2, + 2, + 2, + 2, + -1, + -1, + 0, + 0, + 2, + 2, + 50, + 50, + 50, + 2, + 2, + -6, + -6, + -6, + -6, + 0, + 0, + -2, + -2, + -1, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + -2, + -2, + -2, + 0, + 0, + -2, + -2, + -2, + -2, + 0, + -1, + -1, + -1, + -1, + -1, + 0 + ], + [ + 210, + 210, + -6, + 0, + 10, + 10, + 10, + 10, + -15, + -15, + -2, + -2, + -2, + 1, + 1, + 1, + 1, + 1, + -2, + -2, + -2, + -14, + -14, + -14, + 1, + 1, + 3, + 3, + 1, + 1, + 10, + 10, + 10, + 1, + 1, + 2, + 2, + 2, + 2, + -1, + -1, + 6, + 6, + -2, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + -2, + -2, + -2, + 0, + 0, + -2, + -2, + -2, + -2, + 0, + 1, + 1, + 1, + 1, + 1, + 0 + ], + [ + 216, + 216, + 0, + 0, + 8, + 8, + 8, + 8, + -9, + -9, + 4, + 4, + 4, + -1, + -1, + -1, + 1, + 1, + -4, + -4, + -4, + 24, + 24, + 24, + -3, + -3, + 0, + 0, + 0, + 0, + -24, + -24, + -24, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + -3, + -3, + -3, + -1, + -1, + -1 + ], + [ + 280, + 280, + -8, + 1, + 8, + 8, + 8, + 8, + -5, + -5, + -4, + -4, + -4, + -1, + -1, + -1, + -1, + -1, + 4, + 4, + 4, + 24, + 24, + 24, + -3, + -3, + -2, + -2, + 0, + 0, + 40, + 40, + 40, + -2, + -2, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 1, + 1, + 0 + ], + [ + 280, + 280, + 10, + 1, + -8, + -8, + -8, + -8, + 10, + 10, + 0, + 0, + 0, + -2, + -2, + -2, + 0, + 0, + 0, + 0, + 0, + -8, + -8, + -8, + -2, + -2, + 1, + 1, + 1, + 1, + -40, + -40, + -40, + -1, + -1, + 8, + 8, + 8, + 8, + -1, + -1, + 0, + 0, + -2, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 2, + 2, + 2, + 0, + 0, + 0 + ], + [ + 315, + -5, + 0, + 0, + -5, + -5, + 11, + 11, + -2, + 30, + 3, + -1, + -9, + 2, + -2, + 2, + 0, + 0, + 3, + -1, + -9, + -5, + 27, + 11, + -2, + 6, + -3, + 1, + -1, + 3, + -5, + -85, + 11, + 1, + -1, + 3, + -5, + 3, + -13, + -1, + 1, + 3, + -1, + 0, + 0, + 0, + 0, + 0, + 0, + -1, + 1, + 3, + -1, + -1, + 1, + -1, + 3, + -1, + -1, + -1, + 0, + -2, + 2, + 2, + 0, + 0, + 0 + ], + [ + 315, + -5, + 0, + 0, + -5, + 7, + -1, + 23, + -2, + 30, + -3, + 1, + 9, + 2, + -2, + 2, + 0, + 0, + -3, + 5, + -3, + -5, + 3, + 19, + -2, + 6, + -3, + 1, + 1, + -3, + -5, + 95, + -1, + 1, + -1, + -5, + 11, + -1, + 7, + 1, + -1, + 3, + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + -1, + -1, + -1, + 3, + 1, + -1, + 1, + 1, + -3, + 1, + 0, + -2, + 2, + 2, + 0, + 0, + 0 + ], + [ + 315, + 315, + -9, + 0, + 3, + 3, + 3, + 3, + 0, + 0, + 3, + 3, + 3, + 0, + 0, + 0, + 0, + 0, + 3, + 3, + 3, + -21, + -21, + -21, + 0, + 0, + 0, + 0, + 0, + 0, + -45, + -45, + -45, + 0, + 0, + 3, + 3, + 3, + 3, + 0, + 0, + -5, + -5, + 3, + 1, + 0, + 0, + 0, + 0, + -1, + -1, + 3, + 3, + 3, + -1, + -1, + -1, + -1, + -1, + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 315, + -5, + 0, + 0, + -5, + -1, + 7, + 15, + 1, + -15, + 1, + -3, + 5, + -3, + 1, + 1, + 1, + -1, + 1, + 1, + -7, + -5, + 51, + 3, + 1, + -3, + 6, + -2, + 0, + 0, + -5, + -25, + 7, + -2, + 2, + 3, + 3, + -1, + -9, + 0, + 0, + 3, + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + -1, + 7, + -1, + -5, + 1, + -1, + 1, + 1, + -3, + 1, + 0, + 1, + 1, + -7, + -1, + 1, + 0 + ], + [ + 315, + -5, + 0, + 0, + -5, + 3, + 3, + 19, + 1, + -15, + -1, + 3, + -5, + 1, + 1, + -3, + -1, + 1, + -1, + 3, + -5, + -5, + -21, + 27, + 1, + -3, + 6, + -2, + 0, + 0, + -5, + 35, + 3, + -2, + 2, + -5, + 3, + 3, + 3, + 0, + 0, + 3, + -1, + 0, + 0, + 0, + 0, + 0, + 0, + -1, + 1, + -5, + -1, + 7, + 1, + -1, + 3, + -1, + -1, + -1, + 0, + 1, + -3, + 5, + 1, + -1, + 0 + ], + [ + 336, + 336, + -6, + 0, + -16, + -16, + -16, + -16, + 6, + 6, + 0, + 0, + 0, + 2, + 2, + 2, + 0, + 0, + 0, + 0, + 0, + 16, + 16, + 16, + -2, + -2, + 0, + 0, + -2, + -2, + -16, + -16, + -16, + 2, + 2, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + -2, + 0, + 1, + 1, + -1, + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 2, + 2, + 2, + 0, + 0, + 0 + ], + [ + 378, + 378, + 0, + 0, + 2, + 2, + 2, + 2, + -9, + -9, + 2, + 2, + 2, + -1, + -1, + -1, + -1, + -1, + 2, + 2, + 2, + -6, + -6, + -6, + 3, + 3, + 0, + 0, + 0, + 0, + -30, + -30, + -30, + 0, + 0, + -6, + -6, + -6, + -6, + 0, + 0, + 6, + 6, + 0, + 0, + -2, + -2, + 0, + 0, + 0, + 0, + -2, + -2, + -2, + 0, + 0, + 2, + 2, + 2, + 2, + 1, + 3, + 3, + 3, + -1, + -1, + 0 + ], + [ + 378, + -6, + 0, + 0, + -2, + 2, + -6, + 34, + -3, + 45, + 2, + 2, + -14, + 1, + 1, + -3, + -1, + 1, + -2, + 2, + 2, + 2, + -6, + -6, + -1, + 3, + 0, + 0, + 0, + 0, + 6, + -126, + 2, + 0, + 0, + 2, + -6, + -2, + 6, + 0, + 0, + 6, + -2, + 0, + 0, + -1, + 3, + -1, + 1, + 0, + 0, + -2, + 2, + -2, + 0, + 0, + -2, + 2, + -2, + 2, + 0, + 3, + -1, + -9, + -1, + 1, + 0 + ], + [ + 378, + -6, + 0, + 0, + -2, + -14, + 10, + 18, + -3, + 45, + -2, + -2, + 14, + -3, + 1, + 1, + 1, + -1, + 2, + -2, + -2, + 2, + -6, + -6, + -1, + 3, + 0, + 0, + 0, + 0, + 6, + 114, + -14, + 0, + 0, + 2, + -6, + -2, + 6, + 0, + 0, + 6, + -2, + 0, + 0, + -1, + 3, + -1, + 1, + 0, + 0, + -2, + 2, + -2, + 0, + 0, + 2, + -2, + 2, + -2, + 0, + 3, + -5, + 3, + 1, + -1, + 0 + ], + [ + 405, + 405, + 0, + 0, + -3, + -3, + -3, + -3, + 0, + 0, + -3, + -3, + -3, + 0, + 0, + 0, + 0, + 0, + -3, + -3, + -3, + -27, + -27, + -27, + 0, + 0, + 0, + 0, + 0, + 0, + 45, + 45, + 45, + 0, + 0, + -3, + -3, + -3, + -3, + 0, + 0, + -3, + -3, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 5, + 5, + 5, + 1, + 1, + 1, + 1, + 1, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + -1 + ], + [ + 420, + 420, + -3, + 0, + -12, + -12, + -12, + -12, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 4, + 4, + 4, + 4, + 4, + 3, + 3, + 1, + 1, + 20, + 20, + 20, + -1, + -1, + 4, + 4, + 4, + 4, + 1, + 1, + -4, + -4, + 1, + -1, + 0, + 0, + 0, + 0, + 0, + 0, + -4, + -4, + -4, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + -4, + -4, + -4, + 0, + 0, + 0 + ], + [ + 512, + 512, + 8, + -1, + 0, + 0, + 0, + 0, + -16, + -16, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + -4, + -4, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 2, + 2, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + -1, + 0, + 0, + 0, + 0, + 0, + 1 + ], + [ + 567, + -9, + 0, + 0, + -9, + -1, + 15, + 15, + 0, + 0, + 3, + -5, + 3, + 0, + 0, + 0, + 0, + 0, + 3, + -5, + 3, + -9, + -9, + 39, + 0, + 0, + 0, + 0, + 0, + 0, + -9, + -81, + 15, + 0, + 0, + -1, + -9, + 7, + -9, + 0, + 0, + 3, + -1, + 0, + 0, + 1, + -3, + -1, + 1, + 1, + -1, + -5, + -1, + 7, + -1, + 1, + -1, + 3, + -1, + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 567, + -9, + 0, + 0, + -9, + 11, + 3, + 27, + 0, + 0, + -3, + 5, + -3, + 0, + 0, + 0, + 0, + 0, + -3, + 1, + 9, + -9, + 63, + 15, + 0, + 0, + 0, + 0, + 0, + 0, + -9, + 99, + 3, + 0, + 0, + -1, + 15, + -5, + 3, + 0, + 0, + 3, + -1, + 0, + 0, + 1, + -3, + -1, + 1, + -1, + 1, + 7, + -1, + -5, + -1, + 1, + 1, + 1, + 1, + -3, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 630, + -10, + 0, + 0, + 2, + -2, + -10, + 30, + -1, + 15, + -2, + 2, + 2, + 3, + -1, + -1, + 1, + -1, + 2, + 2, + -14, + -2, + 54, + -10, + 1, + -3, + 3, + -1, + -1, + 3, + 10, + -130, + -2, + 1, + -1, + -2, + -10, + 2, + 10, + 1, + -1, + -6, + 2, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 2, + -2, + 2, + 0, + 0, + -2, + 2, + 2, + -2, + 0, + 1, + 1, + -7, + 1, + -1, + 0 + ], + [ + 630, + -10, + 0, + 0, + 2, + -2, + -10, + 30, + -1, + 15, + -2, + 2, + 2, + 3, + -1, + -1, + 1, + -1, + 2, + -6, + 10, + -2, + -42, + 22, + 1, + -3, + 3, + -1, + 1, + -3, + 10, + -130, + -2, + 1, + -1, + 6, + -2, + -6, + 2, + -1, + 1, + -6, + 2, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 2, + -2, + 2, + 0, + 0, + 2, + -2, + -2, + 2, + 0, + 1, + 1, + -7, + 1, + -1, + 0 + ], + [ + 630, + -10, + 0, + 0, + -10, + 14, + 14, + -18, + -1, + 15, + 2, + -2, + -2, + 3, + -1, + -1, + -1, + 1, + 2, + -2, + -2, + -10, + 54, + 22, + -1, + 3, + 3, + -1, + 1, + -3, + -10, + -50, + 14, + -1, + 1, + 6, + -10, + -2, + -2, + 1, + -1, + -6, + 2, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 2, + 2, + -6, + 0, + 0, + -2, + -2, + 2, + 2, + 0, + -1, + -1, + 7, + 1, + -1, + 0 + ], + [ + 630, + -10, + 0, + 0, + 2, + -18, + 6, + 14, + -1, + 15, + 2, + -2, + -2, + -1, + -1, + 3, + -1, + 1, + -2, + -2, + 14, + -2, + 54, + -10, + 1, + -3, + 3, + -1, + -1, + 3, + 10, + 110, + -18, + 1, + -1, + -2, + -10, + 2, + 10, + 1, + -1, + -6, + 2, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 2, + -2, + 2, + 0, + 0, + 2, + -2, + -2, + 2, + 0, + 1, + -3, + 5, + -1, + 1, + 0 + ], + [ + 630, + -10, + 0, + 0, + 2, + -18, + 6, + 14, + -1, + 15, + 2, + -2, + -2, + -1, + -1, + 3, + -1, + 1, + -2, + 6, + -10, + -2, + -42, + 22, + 1, + -3, + 3, + -1, + 1, + -3, + 10, + 110, + -18, + 1, + -1, + 6, + -2, + -6, + 2, + -1, + 1, + -6, + 2, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 2, + -2, + 2, + 0, + 0, + -2, + 2, + 2, + -2, + 0, + 1, + -3, + 5, + -1, + 1, + 0 + ], + [ + 630, + -10, + 0, + 0, + -10, + 22, + 6, + -10, + -1, + 15, + -2, + 2, + 2, + -1, + -1, + 3, + 1, + -1, + -2, + 2, + 2, + -10, + 6, + 38, + -1, + 3, + 3, + -1, + -1, + 3, + -10, + 70, + 6, + -1, + 1, + -2, + -2, + -2, + 14, + -1, + 1, + -6, + 2, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + -6, + 2, + 2, + 0, + 0, + -2, + -2, + 2, + 2, + 0, + -1, + 3, + -5, + -1, + 1, + 0 + ], + [ + 945, + -15, + 0, + 0, + 1, + 1, + -15, + 49, + -3, + 45, + 1, + -3, + 5, + 1, + 1, + -3, + 1, + -1, + 1, + -3, + 5, + 1, + 33, + -15, + 1, + -3, + 0, + 0, + 0, + 0, + -15, + 225, + 1, + 0, + 0, + 1, + 9, + 1, + -15, + 0, + 0, + -3, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + -1, + 1, + -3, + 1, + 1, + 1, + -1, + -3, + 1, + 1, + 1, + 0, + -3, + 1, + 9, + -1, + 1, + 0 + ], + [ + 945, + -15, + 0, + 0, + 1, + -7, + 9, + -23, + -3, + 45, + 1, + 1, + -7, + 1, + 1, + -3, + 1, + -1, + 1, + 1, + -7, + 1, + 33, + -15, + 1, + -3, + 0, + 0, + 0, + 0, + -15, + -135, + 25, + 0, + 0, + 1, + 9, + -7, + 9, + 0, + 0, + 9, + -3, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + -1, + 1, + -3, + 5, + -1, + 1, + 1, + -3, + 1, + 1, + 0, + -3, + 1, + 9, + -1, + 1, + 0 + ], + [ + 945, + -15, + 0, + 0, + 1, + -27, + 13, + 21, + -3, + 45, + -1, + 3, + -5, + -3, + 1, + 1, + -1, + 1, + -1, + -1, + 7, + 1, + -39, + 9, + 1, + -3, + 0, + 0, + 0, + 0, + -15, + -195, + 29, + 0, + 0, + -7, + 9, + 5, + -3, + 0, + 0, + -3, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + -1, + 1, + 1, + -3, + 1, + -1, + -1, + -1, + 3, + -1, + 0, + -3, + 5, + -3, + 1, + -1, + 0 + ], + [ + 945, + -15, + 0, + 0, + 1, + 13, + -11, + -3, + -3, + 45, + -1, + -1, + 7, + -3, + 1, + 1, + -1, + 1, + -1, + 3, + -5, + 1, + -39, + 9, + 1, + -3, + 0, + 0, + 0, + 0, + -15, + 165, + 5, + 0, + 0, + 1, + -15, + 5, + -3, + 0, + 0, + 9, + -3, + 0, + 0, + 0, + 0, + 0, + 0, + -1, + 1, + 5, + -3, + 1, + -1, + 1, + -1, + -1, + -1, + 3, + 0, + -3, + 5, + -3, + 1, + -1, + 0 + ], + [ + 1008, + -16, + 0, + 0, + -16, + 16, + 16, + 16, + 2, + -30, + 0, + 0, + 0, + -2, + 2, + -2, + 0, + 0, + 0, + 0, + 0, + -16, + 48, + 48, + 2, + -6, + -6, + 2, + 0, + 0, + -16, + 16, + 16, + 2, + -2, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + -1, + 3, + 1, + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 2, + -2, + -2, + 0, + 0, + 0 + ], + [ + 1260, + -20, + 0, + 0, + 4, + 12, + -4, + -52, + -2, + 30, + 0, + 0, + 0, + 2, + -2, + 2, + 0, + 0, + 0, + 0, + 0, + -4, + 12, + 12, + 2, + -6, + 6, + -2, + 0, + 0, + 20, + -20, + -20, + 2, + -2, + -4, + 12, + 4, + -12, + 0, + 0, + 12, + -4, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + -4, + 4, + -4, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 2, + -2, + -2, + 0, + 0, + 0 + ], + [ + 1512, + -24, + 0, + 0, + -8, + -8, + 24, + -8, + -3, + 45, + -4, + 4, + 4, + 1, + 1, + -3, + -1, + 1, + 4, + -4, + -4, + 8, + -24, + -24, + -1, + 3, + 0, + 0, + 0, + 0, + 24, + 216, + -40, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + -3, + 1, + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 3, + -1, + -9, + -1, + 1, + 0 + ], + [ + 1512, + -24, + 0, + 0, + -8, + 24, + -8, + 24, + -3, + 45, + 4, + -4, + -4, + -3, + 1, + 1, + 1, + -1, + -4, + 4, + 4, + 8, + -24, + -24, + -1, + 3, + 0, + 0, + 0, + 0, + 24, + -264, + -8, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + -3, + 1, + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 3, + -5, + 3, + 1, + -1, + 0 + ], + [ + 1890, + -30, + 0, + 0, + -10, + 10, + 2, + 42, + 3, + -45, + 2, + -6, + 10, + 3, + -1, + -1, + -1, + 1, + -2, + 2, + 2, + 10, + -30, + -30, + 1, + -3, + 0, + 0, + 0, + 0, + 30, + -150, + -22, + 0, + 0, + 2, + -6, + -2, + 6, + 0, + 0, + 6, + -2, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + -2, + 2, + -2, + 0, + 0, + 2, + -2, + 2, + -2, + 0, + -3, + 5, + -3, + -1, + 1, + 0 + ], + [ + 1890, + -30, + 0, + 0, + 2, + -14, + 2, + 18, + 3, + -45, + -2, + 2, + 2, + 3, + -1, + -1, + 1, + -1, + -2, + 2, + 2, + 2, + -78, + 18, + -1, + 3, + 0, + 0, + 0, + 0, + -30, + -30, + 34, + 0, + 0, + -6, + -6, + 10, + -6, + 0, + 0, + 6, + -2, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 6, + -2, + -2, + 0, + 0, + -2, + -2, + 2, + 2, + 0, + 3, + -5, + 3, + -1, + 1, + 0 + ], + [ + 1890, + -30, + 0, + 0, + -10, + -6, + 18, + 26, + 3, + -45, + -2, + 6, + -10, + -1, + -1, + 3, + 1, + -1, + 2, + -2, + -2, + 10, + -30, + -30, + 1, + -3, + 0, + 0, + 0, + 0, + 30, + 90, + -38, + 0, + 0, + 2, + -6, + -2, + 6, + 0, + 0, + 6, + -2, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + -2, + 2, + -2, + 0, + 0, + -2, + 2, + -2, + 2, + 0, + -3, + 1, + 9, + 1, + -1, + 0 + ], + [ + 1890, + -30, + 0, + 0, + 2, + -6, + -6, + 26, + 3, + -45, + 2, + -2, + -2, + -1, + -1, + 3, + -1, + 1, + 2, + -2, + -2, + 2, + 66, + -30, + -1, + 3, + 0, + 0, + 0, + 0, + -30, + 90, + 26, + 0, + 0, + 2, + 18, + -6, + -6, + 0, + 0, + 6, + -2, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + -2, + -2, + 6, + 0, + 0, + -2, + -2, + 2, + 2, + 0, + 3, + -1, + -9, + 1, + -1, + 0 + ], + [ + 2268, + -36, + 0, + 0, + -12, + 28, + 12, + -36, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 12, + -36, + -36, + 0, + 0, + 0, + 0, + 0, + 0, + 36, + -36, + -36, + 0, + 0, + -4, + 12, + 4, + -12, + 0, + 0, + -12, + 4, + 0, + 0, + -1, + 3, + -1, + 1, + 0, + 0, + 4, + -4, + 4, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 2520, + -40, + 0, + 0, + 8, + -24, + 8, + -24, + -1, + 15, + 4, + -4, + -4, + 3, + -1, + -1, + 1, + -1, + -4, + 4, + 4, + -8, + 24, + 24, + 1, + -3, + -6, + 2, + 0, + 0, + 40, + 200, + -56, + -2, + 2, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 1, + -7, + 1, + -1, + 0 + ], + [ + 2520, + -40, + 0, + 0, + 8, + 8, + -24, + 8, + -1, + 15, + -4, + 4, + 4, + -1, + -1, + 3, + -1, + 1, + 4, + -4, + -4, + -8, + 24, + 24, + 1, + -3, + -6, + 2, + 0, + 0, + 40, + -280, + -24, + -2, + 2, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + -3, + 5, + -1, + 1, + 0 + ], + [ + 2520, + -40, + 0, + 0, + 8, + -8, + -8, + -8, + 2, + -30, + 0, + 0, + 0, + -2, + 2, + -2, + 0, + 0, + 0, + 0, + 0, + -8, + -72, + 56, + -2, + 6, + 3, + -1, + -1, + 3, + 40, + -40, + -40, + 1, + -1, + 8, + 8, + -8, + -8, + 1, + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + -2, + 2, + 2, + 0, + 0, + 0 + ], + [ + 2520, + -40, + 0, + 0, + 8, + -8, + -8, + -8, + 2, + -30, + 0, + 0, + 0, + -2, + 2, + -2, + 0, + 0, + 0, + 0, + 0, + -8, + 120, + -8, + -2, + 6, + 3, + -1, + 1, + -3, + 40, + -40, + -40, + 1, + -1, + -8, + -8, + 8, + 8, + -1, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + -2, + 2, + 2, + 0, + 0, + 0 + ], + [ + 2835, + -45, + 0, + 0, + 3, + -25, + 15, + -9, + 0, + 0, + -3, + 1, + 9, + 0, + 0, + 0, + 0, + 0, + -3, + 5, + -3, + 3, + 27, + -21, + 0, + 0, + 0, + 0, + 0, + 0, + -45, + -225, + 63, + 0, + 0, + 3, + 3, + -1, + -9, + 0, + 0, + -9, + 3, + 0, + 0, + 0, + 0, + 0, + 0, + -1, + 1, + -5, + 3, + -1, + -1, + 1, + 1, + 1, + -3, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 2835, + -45, + 0, + 0, + 3, + 11, + -21, + 27, + 0, + 0, + 3, + -1, + -9, + 0, + 0, + 0, + 0, + 0, + 3, + -1, + -9, + 3, + -45, + 3, + 0, + 0, + 0, + 0, + 0, + 0, + -45, + 315, + 27, + 0, + 0, + -5, + 3, + 3, + 3, + 0, + 0, + -9, + 3, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + -1, + -1, + 3, + -5, + -1, + 1, + 3, + -1, + -1, + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 2835, + -45, + 0, + 0, + 3, + 15, + -9, + -33, + 0, + 0, + -3, + 5, + -3, + 0, + 0, + 0, + 0, + 0, + -3, + 1, + 9, + 3, + 27, + -21, + 0, + 0, + 0, + 0, + 0, + 0, + -45, + 135, + 39, + 0, + 0, + 11, + -21, + -1, + -9, + 0, + 0, + 3, + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + -1, + -1, + -1, + 3, + 1, + -1, + 1, + 1, + 1, + -3, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 2835, + -45, + 0, + 0, + 3, + 3, + 3, + -45, + 0, + 0, + 3, + -5, + 3, + 0, + 0, + 0, + 0, + 0, + 3, + -5, + 3, + 3, + -45, + 3, + 0, + 0, + 0, + 0, + 0, + 0, + -45, + -45, + 51, + 0, + 0, + -5, + 3, + -5, + 27, + 0, + 0, + 3, + -1, + 0, + 0, + 0, + 0, + 0, + 0, + -1, + 1, + 3, + -1, + -1, + 1, + -1, + -1, + 3, + -1, + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ] + ] +} diff --git a/research/clifford-order3-conditioning/source/width-nine-input.json b/research/clifford-order3-conditioning/source/width-nine-input.json new file mode 100644 index 0000000000..77a5c8b23b --- /dev/null +++ b/research/clifford-order3-conditioning/source/width-nine-input.json @@ -0,0 +1,494 @@ +{ + "status": "PASS_THREE_QUBIT_CLIFFORD_THRESHOLD_TEN", + "source_pins": 4, + "projective_order": 92897280, + "symplectic_order": 1451520, + "quotient_source_rows": [ + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 9, + 12, + 13, + 14, + 15, + 16, + 17, + 18, + 19, + 20, + 21, + 22, + 23, + 24, + 25, + 26, + 29, + 32, + 33, + 36, + 37, + 38 + ], + "quotient_source_classes": [ + [ + 1, + 2 + ], + [ + 3 + ], + [ + 4 + ], + [ + 5, + 6, + 7, + 8 + ], + [ + 9, + 10 + ], + [ + 11, + 12, + 13 + ], + [ + 14, + 15, + 16 + ], + [ + 17, + 18 + ], + [ + 19, + 20, + 21 + ], + [ + 22, + 23, + 24 + ], + [ + 25, + 26 + ], + [ + 27, + 28 + ], + [ + 29, + 30 + ], + [ + 31, + 32, + 33 + ], + [ + 34, + 35 + ], + [ + 36, + 37, + 38, + 39 + ], + [ + 40, + 41 + ], + [ + 42, + 43 + ], + [ + 44 + ], + [ + 45 + ], + [ + 46, + 47 + ], + [ + 48, + 49 + ], + [ + 50, + 51 + ], + [ + 52, + 53, + 54 + ], + [ + 55, + 56 + ], + [ + 57, + 58, + 59, + 60 + ], + [ + 61 + ], + [ + 62, + 63, + 64 + ], + [ + 65, + 66 + ], + [ + 67 + ] + ], + "quotient_class_sizes": [ + 1, + 2240, + 161280, + 945, + 672, + 7560, + 30240, + 60480, + 7560, + 315, + 10080, + 13440, + 40320, + 63, + 40320, + 3780, + 120960, + 3780, + 20160, + 120960, + 48384, + 145152, + 90720, + 11340, + 90720, + 45360, + 96768, + 10080, + 60480, + 207360 + ], + "fixed_dimensions": [ + 6, + 0, + 0, + 4, + 4, + 3, + 2, + 1, + 3, + 4, + 2, + 2, + 2, + 5, + 1, + 3, + 1, + 2, + 0, + 0, + 2, + 1, + 1, + 2, + 1, + 2, + 0, + 3, + 1, + 0 + ], + "transvection_column_one_based": 14, + "odd_tensor_multiplicities": { + "1": [ + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "3": [ + 0, + 1, + 1, + 2, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "5": [ + 0, + 5, + 5, + 10, + 0, + 0, + 0, + 0, + 4, + 0, + 1, + 5, + 0, + 0, + 0, + 0, + 5, + 6, + 0, + 0, + 0, + 4, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "7": [ + 30, + 0, + 1, + 0, + 28, + 104, + 105, + 0, + 0, + 0, + 35, + 0, + 70, + 35, + 120, + 126, + 7, + 0, + 42, + 140, + 35, + 20, + 140, + 0, + 0, + 28, + 21, + 90, + 70, + 64 + ], + "9": [ + 269, + 0, + 85, + 35, + 840, + 1890, + 1975, + 175, + 28, + 350, + 1407, + 210, + 2625, + 1575, + 3900, + 4410, + 945, + 567, + 2835, + 5250, + 2625, + 1728, + 5600, + 1400, + 1575, + 2940, + 2835, + 6075, + 5250, + 5440 + ], + "11": [ + 155, + 17204, + 23001, + 40953, + 5236, + 6138, + 11935, + 32725, + 86020, + 65450, + 60775, + 140250, + 45815, + 71995, + 41140, + 75922, + 207009, + 227205, + 106029, + 91630, + 137445, + 201960, + 157080, + 261800, + 294525, + 267036, + 318087, + 227205, + 274890, + 371008 + ], + "13": [ + 18383, + 632060, + 1008865, + 1640925, + 620620, + 721370, + 1098175, + 1884025, + 3918772, + 3768050, + 3861143, + 6782490, + 3878875, + 4765475, + 3989700, + 6250530, + 10927345, + 11530233, + 7912905, + 7757750, + 9420125, + 11454872, + 11525800, + 15072200, + 16956225, + 16579420, + 19217055, + 16956225, + 18840250, + 24115520 + ] + }, + "odd_tensor_ranks": { + "1": 64, + "3": 45760, + "5": 8961920, + "7": 77913472, + "9": 92894144, + "11": 92897280, + "13": 92897280 + }, + "width_nine_nullity": 3136, + "sharp_threshold": 10, + "quadratic_orbit_sizes": [ + 36, + 28 + ], + "transvection_fixtures": 63, + "remaining_degree_fractions": [ + "17/108", + "1/12" + ], + "uniform_spectral_bounds_from_ten": [ + "945/262144", + "762615/32768" + ], + "uniform_condition_upper_bound": 6456, + "negative_controls": [ + "changed table cell", + "wrong adjoint identification", + "discarded native fourth-power sign", + "omitted Pauli average", + "false width-nine independence", + "overfunded transvection trace", + "omitted odd-Arf orbit", + "even width through odd-sector formula" + ], + "scope": "Exact arithmetic supporting PROOF.md; the published character identification is a cited input, not reconstructed." +} diff --git a/research/clifford-order3-conditioning/verify.py b/research/clifford-order3-conditioning/verify.py new file mode 100644 index 0000000000..bf9d6070b5 --- /dev/null +++ b/research/clifford-order3-conditioning/verify.py @@ -0,0 +1,542 @@ +"""New order-three lift, quadratic-form and two-trace LP certificate. + +The character table, width-nine multiplicities and even-sector representation +identifications are inherited, authenticated mathematical inputs. No predecessor +executable or decomposition engine is imported or run. All arithmetic is exact. +""" +from fractions import Fraction as F +from itertools import combinations, product +import hashlib +import json +from pathlib import Path +import sys + +PACKAGE = Path(__file__).resolve().parent +MANIFEST_SHA = '51d69b9daeefb8ac8b9c530605e17dad60e35e426d31652928b1dff29582fd81' +PATHS = {'source/table.json', 'source/width-nine-input.json', 'source/EXTERNAL.json', + 'predecessor/PR6794-PROOF.md', 'predecessor/PR6714-PROOF.md'} +ZERO, ONE, IMAG = (F(0), F(0)), (F(1), F(0)), (F(0), F(1)) + + +def require(ok, message): + if not ok: + raise ValueError(message) + + +def unique(pairs): + result = {} + for key, value in pairs: + require(key not in result, 'duplicate JSON key') + result[key] = value + return result + + +def no_number(text): + raise ValueError('noninteger JSON number') + + +def load(raw): + return json.loads(raw, object_pairs_hook=unique, parse_float=no_number, parse_constant=no_number) + + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(',', ':'), ensure_ascii=True, allow_nan=False).encode() + + +def rational(value): + value = F(value) + return [value.numerator, value.denominator] + + +def gaussian(value): + return [*rational(value[0]), *rational(value[1])] + + +def authenticate(): + raw = (PACKAGE / 'SOURCE-PINS.json').read_bytes() + require(hashlib.sha256(raw).hexdigest() == MANIFEST_SHA, 'source manifest bytes') + pins = load(raw) + require(type(pins['schema_version']) is int and pins['schema_version'] == 1, 'source schema') + require(len(pins['files']) == 5 and {x['local_path'] for x in pins['files']} == PATHS, 'source inventory') + bodies, hashes = {}, {} + for row in pins['files']: + path = PACKAGE / row['local_path'] + require(path.is_file() and not path.is_symlink(), 'source regular file') + data = path.read_bytes() + blob = hashlib.sha1(b'blob ' + str(len(data)).encode() + b'\0' + data).hexdigest() + require((len(data), hashlib.sha256(data).hexdigest(), blob) == + (row['bytes'], row['sha256'], row['git_blob']) and row['mode'] == '100644', 'source bytes') + bodies[row['local_path']], hashes[row['local_path']] = data, row['sha256'] + return {name: load(bodies[name]) for name in PATHS if name.endswith('.json')}, hashes + + +def add(a, b): + return a[0] + b[0], a[1] + b[1] + + +def multiply(a, b): + return a[0]*b[0] - a[1]*b[1], a[0]*b[1] + a[1]*b[0] + + +def conjugate(a): + return a[0], -a[1] + + +def matrix_zero(n): + return [[ZERO for _ in range(n)] for _ in range(n)] + + +def matrix_identity(n): + result = matrix_zero(n) + for i in range(n): + result[i][i] = ONE + return result + + +def matrix_scale(matrix, scalar): + return [[multiply(scalar, value) for value in row] for row in matrix] + + +def matrix_adjoint(matrix): + return [[conjugate(matrix[j][i]) for j in range(len(matrix))] for i in range(len(matrix))] + + +def matrix_product(left, right): + n, result = len(left), matrix_zero(len(left)) + for i in range(n): + for k in range(n): + if left[i][k] == ZERO: + continue + for j in range(n): + if right[k][j] != ZERO: + result[i][j] = add(result[i][j], multiply(left[i][k], right[k][j])) + return result + + +def tensor(left, right): + return [[multiply(a, b) for a in ar for b in br] for ar in left for br in right] + + +def matrix_trace(matrix): + total = ZERO + for i in range(len(matrix)): + total = add(total, matrix[i][i]) + return total + + +def matrix_key(matrix): + return tuple(value for row in matrix for value in row) + + +def sparse_matrix(matrix): + return [[i, j, gaussian(value)] for i, row in enumerate(matrix) + for j, value in enumerate(row) if value != ZERO] + + +def selected_lift(): + c = F(1, 2), F(1, 2) + h = matrix_scale([[ONE, ONE], [ONE, (F(-1), F(0))]], c) + phase = [[ONE, ZERO], [ZERO, IMAG]] + small = matrix_product(h, phase) + return small, tensor(small, matrix_identity(4)) + + +def square_characters(g): + trace = matrix_trace(g) + second = matrix_trace(matrix_product(g, g)) + squared = multiply(trace, trace) + symmetric = multiply((F(1, 2), F(0)), add(squared, second)) + exterior = multiply((F(1, 2), F(0)), add(squared, (-second[0], -second[1]))) + return dict(natural_trace=gaussian(trace), trace_of_square=gaussian(second), + symmetric_square_trace=gaussian(symmetric), exterior_square_trace=gaussian(exterior), + scope='Actual natural symmetric/exterior-square characters; no irreducibility assertion.') + + +def lift_checks(g): + identity = matrix_identity(8) + require(matrix_product(g, matrix_adjoint(g)) == identity, 'lift is not unitary') + cube = matrix_product(matrix_product(g, g), g) + require(cube == matrix_scale(identity, (F(-1), F(0))), 'lift cube is not minus identity') + require(matrix_trace(g) == (F(4), F(0)), 'lift trace is not four') + characters = square_characters(g) + require(characters['symmetric_square_trace'] == gaussian((F(6), F(0))) + and characters['exterior_square_trace'] == gaussian((F(10), F(0))), 'square-character witnesses') + return dict(unitary=True, trace=gaussian(matrix_trace(g)), cube_phase=gaussian(cube[0][0]), + character_witnesses=characters) + + +def pauli(label): + a, b = label & 7, label >> 3 + basic = {(0, 0): matrix_identity(2), + (1, 0): [[ZERO, ONE], [ONE, ZERO]], + (0, 1): [[ONE, ZERO], [ZERO, (F(-1), F(0))]], + (1, 1): [[ZERO, (F(0), F(-1))], [IMAG, ZERO]]} + result = [[ONE]] + for bit in range(3): + result = tensor(result, basic[((a >> bit) & 1, (b >> bit) & 1)]) + return result + + +class NonPauli(ValueError): + def __init__(self, label, image): + super().__init__('conjugated image is not a signed Pauli') + self.label, self.image = label, image + + +def pauli_action(g): + originals = [pauli(label) for label in range(64)] + lookup = {} + for label, matrix in enumerate(originals): + for sign in (1, -1): + key = matrix_key(matrix_scale(matrix, (F(sign), F(0)))) + require(key not in lookup, 'signed Pauli collision') + lookup[key] = (label, sign) + action, adjoint = [], matrix_adjoint(g) + for label, matrix in enumerate(originals): + image = matrix_product(matrix_product(g, matrix), adjoint) + if matrix_key(image) not in lookup: + raise NonPauli(label, image) + target, sign = lookup[matrix_key(image)] + action.append(dict(label=label, target=target, sign=sign)) + require(len({row['target'] for row in action}) == 64, 'Pauli label permutation') + return action + + +def expected_label(label): + a, b = label & 7, label >> 3 + first_a, first_b = a & 1, b & 1 + return ((a & 6) | (first_a ^ first_b)) + 8 * ((b & 6) | first_a) + + +def quadratic(form, label): + alpha, beta, a, b = form & 7, form >> 3, label & 7, label >> 3 + return ((a & b).bit_count() + (alpha & a).bit_count() + (beta & b).bit_count()) & 1 + + +def arf(form): + return ((form & 7) & (form >> 3)).bit_count() & 1 + + +def form_data(action, classifier=arf): + tables = [tuple(quadratic(form, label) for label in range(64)) for form in range(64)] + lookup = {values: form for form, values in enumerate(tables)} + require(len(lookup) == 64, 'distinct quadratic forms') + sizes, fixed, records = [0, 0], [0, 0], [] + for form in range(64): + pullback = tuple(quadratic(form, row['target']) for row in action) + require(pullback in lookup, 'quadratic pullback') + target, orbit = lookup[pullback], classifier(form) + require(classifier(target) == orbit, 'Arf preservation') + sizes[orbit] += 1 + fixed[orbit] += int(target == form) + records.append(dict(form=form, pullback=target, arf=orbit, fixed=target == form)) + return dict(orbit_sizes=sizes, fixed_by_arf=fixed, records=records, + distinct_form_vector_pairs=64*64) + + +def check_forms(data): + require(data['orbit_sizes'] == [36, 28], 'quadratic orbit sizes') + require(data['fixed_by_arf'] == [6, 10], 'order3 fixed-form counts') + for row in data['records']: + expected = bool((row['form'] & 1) and ((row['form'] >> 3) & 1)) + require(row['fixed'] == expected, 'fixed-form coordinate condition') + + +def extract_points(table, width, tcols=(31, 32, 33), zcols=(9, 10)): + chars = table['characters'] + require(len(chars) == 67 and all(len(row) == 67 for row in chars), '67 by 67 table') + require(all(type(x) is int for row in chars for x in row), 'integer table') + rows, multiplicities = width['quotient_source_rows'], width['odd_tensor_multiplicities']['9'] + require(len(rows) == len(multiplicities) == 30 and rows == sorted(set(rows)), 'thirty quotient rows') + result = [] + for source_row, multiplicity in zip(rows, multiplicities): + require(type(source_row) is int and 1 <= source_row <= 67, 'source row index') + require(type(multiplicity) is int and multiplicity >= 0, 'width-nine multiplicity') + source = chars[source_row-1] + require(source[0] > 0, 'positive degree') + require(len({source[j-1] for j in tcols}) == len({source[j-1] for j in zcols}) == 1, + 'selected published columns agree') + result.append(dict(row=source_row, d=source[0], t=source[tcols[0]-1], + z=source[zcols[0]-1], m=multiplicity)) + return result + + +def bind_classes(points, width): + require(width['quotient_source_classes'][13] == [31, 32, 33], 'transvection columns') + require(width['quotient_source_classes'][4] == [9, 10], 'order3 columns') + require(width['quotient_class_sizes'][4] == 672 and width['fixed_dimensions'][4] == 4, + 'cited order3 class identification') + check_column_anchors(points) + + +def check_column_anchors(points): + expected = {1: (1, 1, 1, 269), 2: (7, -5, 4, 0), 9: (56, -24, 11, 28)} + actual = {row['row']: (row['d'], row['t'], row['z'], row['m']) for row in points if row['row'] in expected} + require(actual == expected, 'selected column anchors') + + +def bounds_for(orbit_size, forms): + index = forms['orbit_sizes'].index(orbit_size) + fixed = forms['fixed_by_arf'][index] + return (F(-16, orbit_size), F(16, orbit_size), + F(-fixed, 2*orbit_size), F(fixed, orbit_size)) + + +def determinant(rows): + a, b, c = rows + return (a[0]*(b[1]*c[2]-b[2]*c[1]) - a[1]*(b[0]*c[2]-b[2]*c[0]) + + a[2]*(b[0]*c[1]-b[1]*c[0])) + + +def solve3(rows, rhs): + det = determinant(rows) + if not det: + return None + result = [] + for column in range(3): + altered = [list(row) for row in rows] + for i in range(3): + altered[i][column] = rhs[i] + result.append(F(determinant(altered), det)) + return result + + +def metrics(points, weights): + total, t, z, objective = F(0), F(0), F(0), F(0) + for index, weight in weights: + row = points[index] + total += weight + t += weight * F(row['t'], row['d']) + z += weight * F(row['z'], row['d']) + objective += weight * F(row['m'], row['d']) + return total, t, z, objective + + +def feasibility(points, weights, bounds): + if not weights or any(weight <= 0 for _, weight in weights): + return 'positive support weights', None + total, t, z, objective = metrics(points, weights) + if total != 1: + return 'simplex normalization', None + if not bounds[0] <= t <= bounds[1]: + return 'transvection trace slab', None + if not bounds[2] <= z <= bounds[3]: + return 'order3 trace slab', None + return None, (t, z, objective) + + +def primal_record(points, weights, values): + return dict(weights=[[points[i]['row'], rational(w)] for i, w in weights], + transvection=rational(values[0]), order3=rational(values[1]), objective=rational(values[2])) + + +def record_vertex(state, points, weights, bounds): + reason, values = feasibility(points, weights, bounds) + if reason: + return + key = tuple((i, w.numerator, w.denominator) for i, w in weights) + if key in state['seen']: + return + state['seen'].add(key) + size = len(weights) + state['counts'][size] = state['counts'].get(size, 0) + 1 + state['digest'].update(canonical(primal_record(points, weights, values))) + for kind in ('minimum', 'maximum'): + old = state[kind] + if old is None or (values[2] < old[0] if kind == 'minimum' else values[2] > old[0]): + state[kind] = (values[2], tuple(weights), values) + + +def vertices(points, bounds): + state = dict(seen=set(), counts={}, digest=hashlib.sha256(), minimum=None, maximum=None) + for i in range(30): + record_vertex(state, points, [(i, F(1))], bounds) + for i, j in combinations(range(30), 2): + for coordinate, bound in ((0, bounds[0]), (0, bounds[1]), (1, bounds[2]), (1, bounds[3])): + key = 't' if coordinate == 0 else 'z' + left, right = F(points[i][key], points[i]['d']), F(points[j][key], points[j]['d']) + if left != right: + weight = (bound-right)/(left-right) + record_vertex(state, points, [(i, weight), (j, 1-weight)], bounds) + for indices in combinations(range(30), 3): + rows = [[points[i][key] for i in indices] for key in ('d', 't', 'z')] + for t, z in product(bounds[:2], bounds[2:]): + raw = solve3(rows, (F(1), t, z)) + if raw is not None: + weights = [(i, raw[j]*points[i]['d']) for j, i in enumerate(indices)] + record_vertex(state, points, weights, bounds) + require(state['seen'], 'empty two-trace feasible polytope') + return state + + +def dual_value(coefficients, bounds, kind): + constant, t, z = coefficients + chosen = [] + for coefficient, low, high in ((t, bounds[0], bounds[1]), (z, bounds[2], bounds[3])): + if coefficient == 0: + chosen.append(None) + elif kind == 'minimum': + chosen.append(low if coefficient > 0 else high) + else: + chosen.append(high if coefficient > 0 else low) + value = constant + sum((c*b for c, b in zip((t, z), chosen) if b is not None), F(0)) + return value, chosen + + +def dual_certificate(points, bounds, kind, primal): + objective, support, values = primal + required = [((points[i]['d'], points[i]['t'], points[i]['z']), F(points[i]['m'])) for i, _ in support] + extras = [((row['d'], row['t'], row['z']), F(row['m'])) for row in points] + extras += [((0, 1, 0), F(0)), ((0, 0, 1), F(0))] + for completion in combinations(extras, 3-len(required)): + equations = required + list(completion) + coefficients = solve3([row for row, _ in equations], [rhs for _, rhs in equations]) + if coefficients is None: + continue + residuals = [] + for row in points: + plane = sum((a*row[k] for a, k in zip(coefficients, ('d', 't', 'z'))), F(0)) + residuals.append(F(row['m'])-plane if kind == 'minimum' else plane-F(row['m'])) + value, chosen = dual_value(coefficients, bounds, kind) + if min(residuals) < 0 or value != objective: + continue + for coordinate, bound in zip(values[:2], chosen): + require(bound is None or coordinate == bound, 'primal/dual active-bound mismatch') + return dict(affine_coefficients=[rational(x) for x in coefficients], + signed_active_bounds=[rational(x) if x is not None else None for x in chosen], + scaled_residuals=[[row['row'], rational(x)] for row, x in zip(points, residuals)], + objective=rational(value), primal=primal_record(points, support, values)) + raise ValueError('no exact supporting-plane dual for primal optimum') + + +def lp_certificate(points, bounds, orbit_size): + state = vertices(points, bounds) + extrema = {kind: dual_certificate(points, bounds, kind, state[kind]) for kind in ('minimum', 'maximum')} + return dict(orbit_size=orbit_size, slabs=[rational(x) for x in bounds], + distinct_vertices=len(state['seen']), support_histogram=state['counts'], + vertex_digest=state['digest'].hexdigest(), **extrema) + + +def rejected(name, callback, reason, witness): + try: + callback() + except ValueError as error: + require(str(error) == reason, 'wrong control rejection: '+name) + return dict(name=name, outcome='REJECTED_FOR_INTENDED_REASON', reason=reason, witness=witness) + raise ValueError('control accepted: '+name) + + +def lifted_controls(g, action, forms): + shifted = matrix_scale(g, IMAG) + cube = matrix_product(matrix_product(shifted, shifted), shifted) + require(cube == matrix_scale(matrix_identity(8), IMAG), 'wrong-phase actual cube') + require(pauli_action(shifted) == action, 'global-phase control changed Pauli action') + characters = square_characters(shifted) + require(characters['symmetric_square_trace'] == gaussian((F(-6), F(0))) + and characters['exterior_square_trace'] == gaussian((F(-10), F(0))), 'wrong-phase actual characters') + first = rejected('wrong_global_phase_i_g', lambda: lift_checks(shifted), 'lift cube is not minus identity', + dict(trace=gaussian(matrix_trace(shifted)), cube_phase=gaussian(cube[0][0]), + same_signed_Pauli_action=True, character_witnesses=characters)) + permutation = matrix_identity(8) + permutation[6], permutation[7] = permutation[7], permutation[6] + try: + pauli_action(permutation) + except NonPauli as error: + second = dict(name='non_Pauli_Toffoli_permutation', outcome='DETECTED_NON_PAULI_IMAGE', + witness=dict(input_label=error.label, image=sparse_matrix(error.image))) + else: + raise ValueError('non-Pauli control was accepted') + bad_counts = form_data(action, classifier=lambda f: (((f & 7) & (f >> 3)) & 6).bit_count() & 1) + require(forms['records'][9]['fixed'] and forms['records'][9]['arf'] != bad_counts['records'][9]['arf'], + 'wrong-Arf actual fixed-form witness') + third = rejected('omit_first_pair_from_Arf', lambda: check_forms(bad_counts), 'quadratic orbit sizes', + dict(actual_orbits=forms['orbit_sizes'], mutated_orbits=bad_counts['orbit_sizes'], + actual_fixed=forms['fixed_by_arf'], mutated_fixed=bad_counts['fixed_by_arf'], + actual_form9=forms['records'][9], mutated_form9=bad_counts['records'][9])) + return [first, second, third] + + +def slab_controls(points, bounds): + by_row = {row['row']: i for i, row in enumerate(points)} + # Credited PR6794's fixed upper primal mixture; not its optimizer or verifier. + weights = [(by_row[1], F(3, 4)), (by_row[2], F(1, 4))] + reason, values = feasibility(points, weights, bounds) + require(reason == 'order3 trace slab', 'credited old mixture must fail new slab') + old_only = (bounds[0], bounds[1], F(-1), F(1)) + old_reason, old_values = feasibility(points, weights, old_only) + require(old_reason is None, 'old one-trace mixture witness') + other = [(by_row[2], F(1, 2)), (by_row[9], F(1, 2))] + correct_reason, _ = feasibility(points, other, bounds) + wrong_bounds = (bounds[0], bounds[1], F(-8, 28), F(16, 28)) + wrong_reason, wrong_values = feasibility(points, other, wrong_bounds) + require(correct_reason == 'order3 trace slab' and wrong_reason is None, 'wrong16-fixed orbit-bound witness') + return [dict(name='omit_order3_constraint', outcome='OLD_PRIMAL_ADMITTED_ONLY_AFTER_OMISSION', + witness=primal_record(points, weights, old_values), rejected_by=reason), + dict(name='reuse_transvection_fixed16_for_order3', outcome='LOOSE_BOUND_ADMITS_FORBIDDEN_PRIMAL', + witness=primal_record(points, other, wrong_values), rejected_by=correct_reason, + correct_bounds=[rational(x) for x in bounds[2:]], + wrong_bounds=[rational(x) for x in wrong_bounds[2:]])] + + +def column_controls(table, width): + wrong = extract_points(table, width, zcols=(31, 32)) + row = next(x for x in wrong if x['row'] == 2) + return [rejected('transvection_column_used_as_order3', lambda: check_column_anchors(wrong), + 'selected column anchors', dict(source_row=2, actual_wrong_T3=row['z'], expected_T3=4))] + + +def calculate(): + sources, identities = authenticate() + small, g = selected_lift() + lift = lift_checks(g) + action = pauli_action(g) + require(all(row['target'] == expected_label(row['label']) for row in action), 'selected symplectic action') + fixed_vectors = sum(row['target'] == row['label'] for row in action) + require(fixed_vectors == 16, 'six-bit fixed-space count') + require(all(action[action[action[i]['target']]['target']]['target'] == i for i in range(64)), + 'order-three quotient action') + forms = form_data(action) + check_forms(forms) + table, width = sources['source/table.json'], sources['source/width-nine-input.json'] + require(sources['source/EXTERNAL.json']['table_sha256'] == identities['source/table.json'], 'external table pin') + points = extract_points(table, width) + bind_classes(points, width) + certificates = [lp_certificate(points, bounds_for(size, forms), size) for size in (28, 36)] + lower = min(F(*cert['minimum']['objective']) for cert in certificates) + upper = max(F(*cert['maximum']['objective']) for cert in certificates) + require(lower > 0 and upper >= lower, 'positive spectral interval') + scale = F(92897280, 8**10) + condition = upper/lower + faults = lifted_controls(g, action, forms) + slab_controls(points, bounds_for(28, forms)) + faults += column_controls(table, width) + symplectic = [[(action[1 << j]['target'] >> i) & 1 for j in range(6)] for i in range(6)] + return dict(status='PASS_CLIFFORD_ORDER3_CONDITIONING', schema_version=1, source_sha256=identities, + source_programs_executed=False, selected_lift=dict(lift, g2=sparse_matrix(small), + quotient_matrix=symplectic, fixed_quotient_vectors=fixed_vectors), + Pauli_action=action, quadratic_forms=forms, + source_points=points, LP=certificates, + multiplicity_ratio_interval=[rational(lower), rational(upper)], + Gram_scale=rational(scale), Gram_interval=[rational(scale*lower), rational(scale*upper)], + sufficient_condition_bound=rational(condition), credited_one_trace_bound=807, + improves_credited_bound=condition < 807, controls=faults, control_count=len(faults), + inherited_premises=['published quotient-character identification', 'width-nine multiplicities', + 'even-sector decomposition/reciprocity', 'transvection bound16/N', + 'order3 class5 identification', 'Pauli orbit/central phase rules', 'Schur propagation'], + scope='Two-trace30-point relaxation; primal optima are not asserted actual irreducibles or spectrum.') + + +def main(): + require(sys.argv[1:] in ([], ['--emit']), 'only optional --emit is supported') + packet = calculate() + if not sys.argv[1:]: + require(canonical(load((PACKAGE / 'RESULT.json').read_bytes())) == canonical(packet), + 'retained complete result mismatch') + print(canonical(packet).decode()) + + +if __name__ == '__main__': + try: + main() + except (ValueError, KeyError, TypeError, OSError, json.JSONDecodeError) as error: + print('FAIL_CLIFFORD_ORDER3_CONDITIONING: '+str(error), file=sys.stderr) + raise SystemExit(1)