diff --git a/research/two-sided-ten-term-floor/LICENSE b/research/two-sided-ten-term-floor/LICENSE new file mode 100644 index 0000000000..261eeb9e9f --- /dev/null +++ b/research/two-sided-ten-term-floor/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/two-sided-ten-term-floor/MANIFEST.sha256 b/research/two-sided-ten-term-floor/MANIFEST.sha256 new file mode 100644 index 0000000000..4baa2f9309 --- /dev/null +++ b/research/two-sided-ten-term-floor/MANIFEST.sha256 @@ -0,0 +1,23 @@ +c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4 LICENSE +7eddad15c98ae79954d47967ed201e21cac9ff642ddd6e4e3062142b91797040 NOTICE.md +b7df6853204e67a8b445237be3e7c02b439de0c9e8591308942e480a0b767e60 README.md +d80ab20ed11b4a60ddd782cafa5edc67ad1fc77c3534bae29daeb211e98d5456 checks/caseb4.py +bdf45de589166710fd17f37183e72361f24c8be0ce28b97818f4b1a160f0313e checks/check_logs.py +13944fe88af139ff303af29a54f82ebb861b57f0d0010860e378efad1d7b3b31 checks/clique.py +1423c813da4df655bd34b089dafe20d54c39fb670ac6ddedf8b1a7a3a2686f32 checks/clique2.py +63e584cba74716389cc7e849296ff0b8dbbf8c6c8ec3571e31e2c939a54625f5 checks/d4A.py +bc01efbc204b3ff2827fe2a914c35548466b2106c7f1b55661df495278b5610a checks/d4A2.py +79a81624cc2c11ad45b5f514acf6ac877f86a7d154f19d2ce822fd935aada8c5 checks/d4A3.py +9b5208b4b76d672bb17e5794b20dd48b27f5193b468eb565cd575ddbeb05e68b checks/diag9.py +c8eb877799c141679bb375c5c97e78833a09480a6af495e5ab7836977b2c193b checks/enum9.py +196c7feae38df821209482bc40bc703605866e30fa812504aa522c5ed64f5e98 checks/lib.py +bcf486c760ad5f73299847962518637fcc3ef375eeb1d8bb90c2b45efa6c3a97 checks/lib2.py +012739ff3dc3421c187ca089b361c0b1d49f808908a5a7efdb0603c20f08ca71 checks/manifest_check.py +f16b2f67eed9427e77995556547d7ab2966cf6a9a8e71176245287e995d959c7 checks/stab.py +208d0cfb1ba44f470de575cf2793daf482af2c8100885d5b5c5debedf826d763 checks/swapfam.py +2e5a965cb469cca07474810c210c7dfd6cbe66428918a3f7a19bbfe2a29b0bc7 checks/sym.py +feefcf624e37ba22fe9a29ee289a181358a0ccac27a35fd5f84700a8980cf0e9 checks/verify_cl.py +0544fd29ddddb241cfa17d3809a26485123e29f184f4da799976e5aa34e80743 checks/witness16.py +8e4b2a306dfe3499b9d2104753a4cb203e14fbfa94fda03f6a415da956ba642b data/data.json +a27e2ffabcff8bf39160f211358ec022c176993bef64fa0ecc8d5ea196b708bd requirements.txt +7b64aee8eb79b8671d4c5222bfd997fa35bbf1611fdffb4b994be2ed377bbf7f verify.sh diff --git a/research/two-sided-ten-term-floor/NOTICE.md b/research/two-sided-ten-term-floor/NOTICE.md new file mode 100644 index 0000000000..496f71838b --- /dev/null +++ b/research/two-sided-ten-term-floor/NOTICE.md @@ -0,0 +1,9 @@ +# Notice + +Prepared by DreamingOfClouds with Claude Opus 5.5 (Anthropic), via Claude Code; Apache-2.0 (`LICENSE`, copied from the repository root). + +## Credits + +- Imported: #2832 (Lemma 2.3, Lemmas 3.7–3.9, Theorem 3.5, Corollary 3.6, §3.6), #2816 (Lemma 3.1, cover facts, g(5) = 12, direction-list completeness), #2338 (Lemma D). Not used: #1212, #2724, #2826. +- Tools: Python, numpy, sympy, networkx. No SAT solver. +- No file is copied from another contributor. `checks/manifest_check.py` comes from the author's #2816 and #2832 packages; all other scripts are the author's, with absolute paths removed (`clique.py` additionally recomputes the form Ω and the frame classes instead of loading them; `caseb4.py` is chunked). diff --git a/research/two-sided-ten-term-floor/README.md b/research/two-sided-ten-term-floor/README.md new file mode 100644 index 0000000000..b719710b0a --- /dev/null +++ b/research/two-sided-ten-term-floor/README.md @@ -0,0 +1,182 @@ +# Decoder floors: the smallest two-sided case (m = 10, one outside direction per side) costs ≥ 64 on P112 — conjecture K3 of #2832 (no κ claim) + +**Status: research note. No κ claim, no supplier word, no new floor beyond the single class below.** Every claim is a written proof in this file plus exact finite computations that `verify.sh` re-runs +(about 12 minutes wall unloaded (696 s measured; about 22 minutes under heavy load), at most 4 parallel processes (`JOBS=2` runs two at a time), each under `timeout 1200`, no SAT solver). Only `research/two-sided-ten-term-floor/` is added; nothing existing is changed. + +Labels: **PROVEN** (written proof here; finite inputs listed), **CHECKED** (exact script in `checks/`, re-run by `verify.sh`, asserted in `checks/check_logs.py`), +**FROM #n** (a statement of another PR, cited, not re-derived), **CONDITIONAL on #n** (depends on a PR that is not merged), **RECORDED** (not re-run). + +## 0. Result + +**Theorem K3.** Let `(P, Q)` be a decoder of `N₀ = G/2` on P112 (dense h = 9 table) with `m = 10` terms, two-sided with `(s, t) = (1, 1)` (§1), and *normalised*: every `p_k, q_k ≠ 0` and no two `p`'s and no two `q`'s are proportional (Lemma D of #2338). +Then `cost(P, Q) ≥ 64`. No assumption on `J_P ∩ J_Q` (disjoint or not) is made. + +**Dependencies.** CONDITIONAL on the open PR **#2816** only, entering through #2832: Lemma 3.1 of #2816, the cover facts (C1), (C3) and `g(5) = 12` of #2816 and the completeness of its 1200-direction list (these underlie #2832 Lemmas 3.8–3.9, Theorem 3.5, Corollary 3.6 and the twelve-overlap check of §3.6). +**Not used:** #1212, #2724 (so none of #2832 Corollary 3.4), #2826, any disjointness hypothesis, and the disjoint closure #2832 Theorem 3.13 (it is covered again here; it may be cited as an independent proof of that sub-case). +**Tight:** two exact cost-64 decoders in the class, one with `J_P ∩ J_Q = ∅` and one with `|J_P ∩ J_Q| = 2` (§7). + +**Consequence for the map of #2832 (§5 there).** K3 is now a theorem (conditional as stated). With #2832, the P112 master `C(P112) ≥ 64` reduces to **K1** (every two-sided decoder of `N₀(P112)`, general `m, s, t`) and **K2** (excess pays for corrections, one-sided) only. Nothing is claimed about K1, K2 or P120. + +## 1. Setting, imports, notation + +**Setting (#2832 §1–§2).** Lines `t ∈ L` (112 lines of P112); `C ∈ ℚ^{L×8}` with `N₀ = CCᵀ`, row `t` of `C` equal to `c_t/2`, where `c_t ∈ {0, ±1}⁸` has four non-zero entries (frame coordinates of the root, supports are the 14 blocks of the Steiner system S(3,4,8), CHECKED `caseb4.py`) and `⟨c_t, c_s⟩ = 2⟨r_t, r_s⟩ ∈ {0, ±2, ±4}`; `Off(y) = supp(Cy)`. +Labels `u_t ∈ F₂⁹` with the nondegenerate symmetric form `Ω`, `Bd[t,s] = Ω(u_t, u_s)`, `Bd[t,s] = 1` iff `t = s` or `t ⊥ s`. The eight frame roots `f_1..f_8` (the lines of E8 outside P112) have labels `z_i`; since `Bd` is the table of all of E8, **`Ω(z_i, z_j) = 1` for all `i, j`** and `Ω(z_i, u_t) = 1` iff `t ⊥ f_i` iff `c_t[i] = 0`. Put `W_i := z_i^⊥` (a hyperplane), so `z_j ∉ W_i` for all `i, j`, and labels of distinct E8 lines are distinct. +For a set `S` of lines: `U_S = span u(S)`, `w(S) = dim U_S`, `Z_S = U_S^⊥`; `O_z := {t : Ω(u_t, z) = 1}`; `g(w)` = largest number of lines whose labels lie in a `w`-flat. +`ρ(R, A) := rank_{F₂} Bd[R, A] = w(R) − dim(U_R ∩ Z_A) = w(A) − dim(U_A ∩ Z_R)` (symmetric, `Bd` is symmetric). + +**Decoders (#2832 §2.2).** `p_k = C x_k + x2_k E`, `q_k = C y_k + y2_k F` (`k = 1..10`; `E, F ∉ col C`), with `X̂Ŷᵀ = diag(I₈, 0)`, i.e. +`Σ_k x_k y_kᵀ = I₈`, `Σ_k y2_k x_k = 0`, `Σ_k x2_k y_k = 0`, `Σ_k x2_k y2_k = 0`. `J_P = {k : x2_k ≠ 0}`, `J_Q = {k : y2_k ≠ 0}`. `R_k = supp p_k`, `A_k = supp q_k`, `cost_k = ρ(R_k, A_k)`. A term outside `J_P` has *inside row*, outside `J_Q` *inside column*. +The transpose `(Q, P)` is again a normalised (1,1), `m = 10` decoder of the symmetric `N₀`; every statement about columns below holds for rows, and conversely ("by transposition"). + +**Imports (all FROM #2832, which cites #2816 and #2338; statements only).** +* **(F1)** (#2816 Lemma 3.1) For `y ∈ ℚ⁸∖0`, `U_{Off(y)} = F₂⁹` unless `y ∝ e_i`, and then `U_{Off(y)} = W_i`. So an inside row/column has weight 9, or weight 8 with `U = W_i`. +* **(F2)** (#2832 Lemma 2.3) In a normalised decoder `|J_P|, |J_Q| ≥ 3`. (Each row restriction `p(t)|_{J_Q}` lies in the kernel of `Y₂[:,J_Q]`; if `|J_Q| ≤ 2`, all `p_k`, `k ∈ J_Q`, are proportional.) +* **(F3)** (#2832 Theorem 3.5 and the twelve-overlap check of §3.6, `d4.py`) *Catalogue.* Let `λ` be an outside vector of the coset with `w(supp λ) ≤ 5` (so `|supp λ| ≤ g(5) = 12`), and `p_k = x2_k(λ + Cη_k)` another outside row, `η_k ≠ 0`. If `w(R_k) = 8`, i.e. `p_k` vanishes on `O_z` for a class `z` with `U_{R_k} = z^⊥`, then `|Off(η_k) ∩ O_z| ≤ |supp λ ∩ O_z| ≤ 12`, and: either **frame type** (`η_k ∝ e_i`, `z = z_i`) or **root swap** (`η_k ∝ c_v`, `z = u_v`, `v ∈ supp λ`, `supp λ ∩ O_{u_v} = {v}`). The twelve-overlap sets have label span of dimension 7 and do not fit in `supp λ`. +* **(F3′)** (#2832 Corollary 3.6, stated there from F1 alone, without the weight hypothesis of F3) For outside columns (rows, by transposition) of the coset with distinct `η`, a non-frame class `z` lies in `Z_{A_k}` for at most one `k`. +* **(F4)** (#2832 Lemmas 3.7–3.9) Among outside columns there is at most one of weight ≤ 6, and then no other column of weight ≤ 7; otherwise at most two columns have weight ≤ 7 and both have weight 7. + +Fact used with its proof in §3 (Lemma S): a root swap row is `p_k = x2_k(λ + α C c_v)`, where `(C c_v)(t) = G_{tv} = ⟨r_t, r_v⟩` is non-zero exactly at `v` (value 2) and at the lines non-orthogonal to `v`; it vanishes on `O_{u_v} = {v} ∪ v^⊥` iff `α = −λ(v)/2` and `supp λ ∩ O_{u_v} = {v}`. + +## 2. Normal form (PROVEN) + +**Lemma N.** Let `a ∈ J_Q`, `a′ ∈ J_P`, `a ≠ a′` (possible by F2). After rescaling terms (`(p_k, q_k) ↦ (c p_k, c⁻¹ q_k)`) and moving the outside directions, `y2_a = x2_{a′} = 1` and +`p_k = C x_k + x2_k λ`, `q_k = C y_k + y2_k μ` for all `k`, with `λ := p_{a′}`, `μ := q_a` (outside vectors), `x_{a′} = 0`, `y_a = 0`. The eight **dual terms** `l ∉ {a, a′}` satisfy `⟨x_l, y_{l′}⟩ = δ_{ll′}` (`(x_l)` a basis of ℚ⁸, `(y_l)` its dual basis), and +`x_a = −Σ_l y2_l x_l`, `y_{a′} = −Σ_l x2_l y_l`, hence `⟨x_a, y_l⟩ = −y2_l`, `⟨x_l, y_{a′}⟩ = −x2_l`. +*Proof.* Put `Ŷ′ = SŶ`, `S = [[I₈, −y_a/y2_a],[0, 1]]`, and `F′ = F + C y_a/y2_a = q_a/y2_a`. Then `X̂ Ŷ′ᵀ = diag(I₈,0)·Sᵀ = diag(I₈,0)` and `[C F′]Ŷ′ = [C F]Ŷ` (since `[C F′]S = [C F]`): the same matrix `Q`, written with `y_a = 0` and outside direction `μ := F′`. Likewise on the `P` side with `x_{a′}` and `λ`. Terms `a, a′` then contribute `0` to `Σ x_k y_kᵀ = I₈`, so the other eight form a dual-basis pair; the circuits `Σ y2_k x_k = 0`, `Σ x2_k y_k = 0` give the formulas for `x_a`, `y_{a′}` (`x_{a′} = 0 = y_a`). All `p_k, q_k` are non-zero: `C x_l ≠ 0`, `λ ∉ col C`, and `x_a ≠ 0` because some dual `l ∈ J_Q∖{a′}` exists (`|J_Q| ≥ 3`), so `x_a = −Σ y2_l x_l ≠ 0` (the `x_l` are independent). ∎ +Consequence: `y2_l ≠ 0` for a dual column that is outside, and outside rows/columns lie in the cosets `λ + 𝒞`, `μ + 𝒞` (`𝒞 = col C`) with `η_k = x_k/x2_k`, `η_k = y_k/y2_k`; normalised ⇒ the `η` of different outside rows (columns) are distinct. + +## 3. Accounting (PROVEN) + +**Savings.** `d^R_k := 9 − w(R_k)`, `d^A_k := 9 − w(A_k)`, `c_k := dim(U_{R_k} ∩ Z_{A_k}) ≤ d^A_k`, `c′_k := dim(U_{A_k} ∩ Z_{R_k}) ≤ d^R_k`, `s_k := 9 − cost_k = d^R_k + c_k = d^A_k + c′_k ≤ d^R_k + d^A_k`. +`cost = 90 − Σ_k s_k`, so **cost ≤ 63 ⇔ Σ s_k ≥ 27** (E1). + +**Row profiles and D̂ (L1).** By F1 inside rows have `d^R ≤ 1`. Call an outside row *low* if its weight is ≤ 7. By F4 (rows, by transposition) exactly one of four profiles occurs: +| profile of low rows | `D̂_P` | `Σ_k d^R_k` | +|---|---|---| +| one low row of weight `9 − D ≤ 6` (`D ≥ 3`), no other low | `D` | `D + (9 − ζ_P)` | +| two low rows, both weight 7 | 3 | `2 + 2 + (8 − ζ_P)` | +| one low row, weight 7 | 2 | `2 + (9 − ζ_P)` | +| no low row | 1 | `10 − ζ_P` | + +where `ζ_P` = number of non-low terms with `d^R = 0` (non-low terms have `d^R ≤ 1`). So `Σ d^R = D̂_P + 9 − ζ_P` in every profile; `D̂ = D` for `D ≥ 3`, `D̂ ∈ {2,3}` for `D = 2`, `D̂ = 1` for `D ≤ 1`. Same for columns (`D̂_Q`, `ζ_Q`). With `Λ := Σ_k (d^A_k − c_k) ≥ 0`: +**cost = 72 − D̂_P − D̂_Q + ζ_P + ζ_Q + Λ** (E2), so with `σ := D̂_P + D̂_Q − 9`: +**cost ≤ 63 ⇒ σ ≥ 0 and ζ_P + ζ_Q + Λ ≤ σ** (E3). In particular **(L1) cost ≤ 63 needs D̂_P + D̂_Q ≥ 9**; (4,4) and everything smaller is closed here. + +**Lemma S (swap slots).** Let `λ` be the low outside row vector with `w_P := w(supp λ) ≤ 5`. Root-swap rows (type of F3) of different terms have pairwise distinct lines, pairwise non-orthogonal, and their labels are `Ω`-orthonormal in `U_{supp λ}`; hence at most `w_P` terms have a root-swap row (the term carrying `λ` itself does not count). Same for columns with `μ`, `w_Q`. +*Proof.* Two swap rows at the same line `v` both lie in `span(λ, Cc_v)` and vanish at `v`, so they are proportional (excluded). Every swap line `v` has `supp λ ∩ O_{u_v} = {v}` (F3), so for swap lines `v ≠ v′` we get `v′ ∈ supp λ∖{v}`, hence `Bd[v, v′] = 0`: `Ω(u_v, u_{v′}) = 0`, `Ω(u_v, u_v) = 1`. An orthonormal family is independent, and lies in `U_{supp λ}`. ∎ + +**Lemma F (frame/frame).** If a term has `d^R = d^A = 1` and both its row and column are of frame type (`U_R = W_i`, `Z_A = ⟨z_{i′}⟩`) then `s = 1`, because `z_{i′} ∉ W_i`. Hence, when F3 applies on both sides, **`s_k = 2` forces a root swap on at least one side of term `k`**. + +## 4. Cells with a low side, `min D̂ ≤ 3` (PROVEN; finite part CHECKED) + +**Theorem LOWD.** A normalised (1,1), `m = 10` decoder in which some side has `D̂ ≤ 3` (a unique low of weight 6, one or two lows of weight 7, or no low) costs ≥ 64, for every `K = J_P ∩ J_Q`. + +*Proof.* Suppose cost ≤ 63. By (L1) the other side has `D̂ ≥ 6`; by transposition it is `P`: a unique low row `a′` with `D_P ≥ 6`, `w_P = 9 − D_P ≤ 3`; and `D̂_Q ≤ 3`. Then `σ = D_P + D̂_Q − 9 ≥ 0` and `w_P + σ = D̂_Q`. +Fix `a ∈ J_Q∖{a′}` and the normal form of Lemma N at `(a, a′)`; `λ = p_{a′}`. + +*Step 1 (dual rows).* A dual row has `d^R ∈ {0, 1}`; if `d^R = 1`, by F1 (inside) or F3 (outside) it is a **frame row** (`x_l ∝ e_i`; normalise `x_l = e_{i_l}`) or a **root swap**. Let `F` be the set of dual terms with frame rows; the `i_l` are distinct (the `x_l` are independent); `I := {i_l}`, `I^c := [8]∖I`. Then `|I^c|` = #(swap rows) + #(rows with `d^R = 0`) ≤ `w_P` + ζ_P (Lemma S). +Call `l ∈ F` **lossless** if `d^A_l ≥ 1` and `c_l = d^A_l` (i.e. `Z_{A_l} ⊆ U_{R_l} = W_{i_l}`; here `U_{R_l} = W_{i_l}` by F1, or by F3 for an outside frame-type row). A term of `F` that is not lossless contributes ≥ 1 to `ζ_Q + Λ` (either `d^A_l = 0`, a non-low column, or `d^A_l − c_l ≥ 1`); terms of `F` have `d^R = 1`, so they are not counted in `ζ_P`. By (E3), +(#rows with `d^R = 0`) + (|F| − #lossless) ≤ ζ_P + ζ_Q + Λ ≤ σ, whence +**#lossless ≥ 8 − w_P − σ = 8 − D̂_Q ≥ 5** and **|I^c| ≤ w_P + σ = D̂_Q ≤ 3**. + +*Step 2 (a lossless column is outside, in a non-frame class).* Let `l` be lossless, so `Z_{A_l} ≠ 0` and `Z_{A_l} ⊆ W_{i_l}`. If the column were inside, F1 gives `y_l ∝ e_{i′}`, `⟨x_l, y_l⟩ ≠ 0` forces `i′ = i_l` and `Z_{A_l} = ⟨z_{i_l}⟩ ⊄ W_{i_l}`: contradiction. So `y2_l ≠ 0`, `q_l = y2_l(μ + Cη_l)`. Pick `z_l ∈ Z_{A_l}∖0`; `z_l ∈ W_{i_l}`, so it is **not a frame class**, and `q_l` vanishes on `O_{z_l}`. For `l ≠ l′` lossless, `z_l ≠ z_{l′}` (F3′; `η_l ≠ η_{l′}` since `y_l, y_{l′}` are independent). + +*Step 3 (linear constraints).* Duality `⟨e_{i_{l′}}, y_l⟩ = δ_{ll′}` for `l′ ∈ F` gives **`η_l ∈ span(e_{i_l}, e_{I^c})` and `η_l[i_l] ≠ 0`**. For `l ≠ l′` lossless both columns vanish on `Θ := O_{z_l} ∩ O_{z_{l′}}`, so `μ = −Cη_l = −Cη_{l′}` there: +**`⟨c_t, η_l − η_{l′}⟩ = 0` for `t ∈ Θ`**, with `η_l − η_{l′} ∈ span(e_{i_l}, e_{i_{l′}}, e_{I^c})` having non-zero `i_l` and `i_{l′}` coordinates. + +*Step 4 (finite test, CHECKED).* For `I^c` with `|I^c| ≤ 3` let `V = {(i, z) : i ∈ I, z ∈ W_i∖0}` (255 classes per `i`; no frame class lies in `W_i`), with an edge `(i,z) ~ (i′,z′)` iff `i ≠ i′`, `z ≠ z′` and some `h ∈ span(e_i, e_{i′}, e_{I^c})` has `⟨c_t, h⟩ = 0` on `O_z ∩ O_{z′}` and `h_i ≠ 0 ≠ h_{i′}`. Step 3 turns the lossless terms into a clique with distinct `i`, which also passes the **joint test** (one exact solution of all pair systems with every `η_l[i_l] ≠ 0`; solvable iff every coordinate functional is non-zero on the kernel, exact rational arithmetic). Steps 1–3 give such a clique of size ≥ 5. +`clique2.py 5` (exact, sympy): on **every** `I^c` with `|I^c| ≤ 3` (1 + 8 + 28 + 56 = 93 sets; no symmetry used) there is **no 5-clique passing the joint test**. The independent re-implementation `verify_cl.py` (compatibility from exact `Bd`-ranks, edges by the row-space criterion, networkx maximal cliques) agrees on the four orbit representatives: + +| `I^c` | vertices | edges | largest clique | +|---|---|---|---| +| `∅` | 2040 | 3584 | 2 | +| `{0}` | 1785 | 2856 | 2 | +| `{0,1}` | 1530 | 9648 | 2 | +| `{0,1,2}` | 1275 | 16496 | 4 (7936 maximal 4-cliques) | + +(`stab.py`, `sym.py`: the frame stabiliser acts on the 8 coordinates as AGL(3,2), order 1344, 3-transitive, one orbit per size ≤ 3, and preserves the family `{O_z}` and the compatible classes; this only explains why the four representatives are typical, the 93 direct runs do not use it.) +A clique of size ≥ 5 does not exist: contradiction. ∎ +The margin is structural: the largest clique is 4 < 5. + +## 5. Cells with both sides high, `min D̂ ≥ 4` (PROVEN) + +Here both sides have a unique low of weight ≤ 5: `a′` the low row (`D_P ≥ 4`, `λ = p_{a′}`, `w_P = 9 − D_P ≤ 5`), `a` the low column (`D_Q ≥ 4`, `μ = q_a`). F3 applies on both sides, so Lemmas S and F hold. Every other term has non-low row and column, `d^R, d^A ≤ 1`, `s ≤ 2`. + +**Theorem H.** (ii) If `a ≠ a′`: `Σ s ≤ 26`, so `cost ≥ 64`. (i) If `a = a′ =: b` and `D_P + D_Q ≥ 9` (the cell `(4,4)` is closed by (L1)): `Σ s ≤ 36 − cost_b − (D_P + D_Q)`; so `cost ≥ 64` unless `cost_b = 0` and `D_P + D_Q = 9`, i.e. `(D_P, D_Q) ∈ {(4,5), (5,4)}`, which Proposition B closes. + +### 5.1 `a ≠ a′` (Theorem H(ii)) +Take the normal form at `(a, a′)`. `Σ s = s_a + s_{a′} + Σ_{dual} s_l`. By F1/F3 a term has `d^R = 1` only with a frame or root-swap row (same for columns); `s_a = D_Q + c_a`, `c_a := dim(U_{A_a} ∩ Z_{R_a}) ≤ d^R_a ≤ 1`; `s_{a′} = D_P + c_{a′}`, `c_{a′} := dim(U_{R_{a′}} ∩ Z_{A_{a′}}) ≤ 1`. A dual term has `s ≤ 2`, and `s = 2` needs a swap on one side (Lemma F). Let `N₂` be the number of dual terms with `s = 2`: `Σ s ≤ D_Q + c_a + D_P + c_{a′} + 8 + N₂`, and `N₂ ≤ (#dual row swaps) + (#dual column swaps) ≤ w_P + w_Q` (Lemma S), `D_P + w_P = D_Q + w_Q = 9`. **It remains to pay for `c_a` and `c_{a′}`:** `N₂ ≤ w_P + w_Q − c_a − c_{a′}`. +* `c_a = 1`, row of `a` of frame type `x_a ∝ e_j` (`Z_{R_a} = ⟨z_j⟩ ⊆ U_μ`). For a dual column swap `l` (`y_l ∝ c_v`, `v ∈ supp μ`, `y2_l ≠ 0`): `0 ≠ −y2_l = ⟨x_a, y_l⟩` gives `c_v[j] ≠ 0`, i.e. `u_v ∈ W_j`. Since `Ω(z_j, z_j) = 1`, `z_j ∈ U_μ∖W_j`, so `dim(U_μ ∩ W_j) = w_Q − 1` and **dual column swaps ≤ w_Q − 1** (α). +* `c_a = 1`, row of `a` a root swap at `v₀`: it occupies one of the `w_P` row slots: **dual row swaps ≤ w_P − 1** (β). +* `c_{a′} = 1` is symmetric: column of `a′` of frame type `f_i` (`z_i ∈ U_λ`): dual row swaps lie in `W_i ∩ U_λ`, **≤ w_P − 1** (α′); or a column swap: **dual column swaps ≤ w_Q − 1** (β′). +* If both are 1 and the losses fall on different sides, `N₂ ≤ w_P + w_Q − 2`. They fall on the same side in the pairs (α, β′) and (β, α′). In (α, β′): the dual column swaps and `u_{v₀}` (`a′`'s own swap line) are `Ω`-orthonormal in `U_μ`; if there were `w_Q − 1` dual swaps, together with `u_{v₀}` they would be an orthonormal basis of `U_μ`, the dual ones lie in `W_j`, so `z_j ∈ U_μ` would equal `Ω(z_j, u_{v₀}) u_{v₀} = u_{v₀}`: a frame label equal to a line label, impossible. So dual column swaps ≤ `w_Q − 2`. (β, α′) is the transpose. +Hence `Σ s ≤ D_P + D_Q + w_P + w_Q + 8 = 26`. ∎ + +### 5.2 `a = a′ = b` (Theorem H(i)), `D_P + D_Q ≥ 9` +`Σ s = s_b + Σ_{9 others} s_k ≤ (9 − cost_b) + 9 + N₂`, where `N₂` (# others with `s = 2`, each with a swap, Lemma F) `≤ w_P + w_Q = 18 − D_P − D_Q`. This gives the bound of H(i): `≤ 26 − cost_b` if `D_P + D_Q ≥ 10`, and `≤ 27 − cost_b` if `D_P + D_Q = 9`. So `Σ s ≥ 27` forces `D_P + D_Q = 9` (with both `≥ 4`: `(4,5)` or `(5,4)`), `cost_b = 0`, `N₂ = 9`. ∎ + +### 5.3 Proposition B: `a = a′ = b`, `cost_b = 0`, `D_P + D_Q = 9` is impossible (PROVEN; CHECKED corroboration) +**Setup.** Shear both sides at `b` (it lies in `J_P ∩ J_Q`; Lemma N's shear on each side): `x_b = y_b = 0`, `p_b = λ`, `q_b = μ`, and the nine other terms satisfy `Σ_{k≠b} x_k y_kᵀ = I₈`. `cost_b = ρ(supp λ, supp μ) = 0` means `Bd[supp λ, supp μ] = 0`: every line of `supp λ` is non-orthogonal to every line of `supp μ`, hence `⟨c_u, c_v⟩ = ±2 ≠ 0` for such pairs, and `U_λ ⊥ U_μ`. Here `(w_P, w_Q) ∈ {(5,4), (4,5)}`. +By the equality case of Theorem H(i): all nine other terms have `s = 2`, each has a swap, and `#row-swap terms + #column-swap terms ≤ w_P + w_Q = 9` (Lemma S) with at least one swap per term forces: **no term has two swaps, exactly `r := w_P` terms are *R-terms* (root-swap row) and `c := w_Q` are *C-terms* (root-swap column)**, `r + c = 9`. A term with `d^A = 1` that is not a swap has a frame column (pure outside is proportional to `q_b`, excluded): +* R-term `k`: `x_k = a_k c_{u_k}`, `y_k = e_{j_k}`, `u_k ∈ supp λ`, `a_k ≠ 0` (swap line, F3). +* C-term `l`: `x_l = e_{i_l}`, `y_l = b_l c_{v_l}`, `v_l ∈ supp μ`, `b_l ≠ 0`. +Identity (★): **`I₈ = A + B`**, `A := Σ_R a_k c_{u_k} e_{j_k}ᵀ`, `B := Σ_C b_l e_{i_l} c_{v_l}ᵀ`. Let `J = {j_k}`, `I = {i_l}` (as sets; indices may repeat). + +**Case 1: some index repeats** (`|J| < r` or `|I| < c`). `A` has non-zero columns only in `J`, `B` non-zero rows only in `I`, so `8 = rank(A + B) ≤ rank A + rank B ≤ |J| + |I| ≤ 8`. Hence equality throughout: exactly one index repeats, exactly twice, and `rank A + rank B = 8`. +*Then `A, B` are complementary idempotents:* `ℚ⁸ = im A + im B` (as `v = Av + Bv`) and the dimensions add up, so the sum is direct. For `y ∈ im A`: `By = y − Ay ∈ im A ∩ im B = 0`. Thus `BA = 0` (and `A² = A`). +Say the repeated index is a `j` (R side; the C side is symmetric). Then `|J| = r − 1 ≥ 3` and `|I| = c`, so there is a column index `j ∈ J` hit by a single R-term `k` and a row index `i` hit by a single C-term `l`. The `(i, j)` entry of `BA = Σ_{l,k} a_k b_l ⟨c_{v_l}, c_{u_k}⟩ e_{i_l} e_{j_k}ᵀ` is the single product `a_k b_l ⟨c_{v_l}, c_{u_k}⟩ ≠ 0`: contradiction with `BA = 0`. + +**Case 2: no index repeats** (`|J| = r`, `|I| = c`). By transposing `(★)` (roles `R, J, r ↔ C, I, c`) we may assume `r = 5`, `c = 4`. +* A column `h ∉ J` has `A e_h = 0`, so `e_h = B e_h ∈ span(e_i : i ∈ I)`: `J^c ⊆ I`. As `|J^c| = 3` and `|I| = 4`: `I = J^c ∪ {m}` with a unique `m ∈ J`. +* A row `ρ ∉ I`, i.e. `ρ ∈ J∖{m}`, has `e_ρᵀ = e_ρᵀ A`: for the R-term `k` with `j_k = j`, `a_k c_{u_k}[ρ] = δ_{jρ}`. So `c_{u_k}[ρ] = 0` for `ρ ∈ J∖{m, j_k}`, and `c_{u_k}[j_k] ≠ 0` when `j_k ≠ m`. +* The R-term with `j_k = m` has `supp c_{u_k} ⊆ J^c ∪ {m} =: B₀` (4 points), so `supp c_{u_k} = B₀` is a block. Any other R-term `k` has `supp c_{u_k}` a 4-subset of the 5-set `B₀ ∪ {j_k}` containing `j_k ∉ B₀`, hence containing at least 3 points of `B₀`; three points lie in a unique block (S(3,4,8)), so `supp c_{u_k} = B₀ ∋ j_k`: contradiction. +So Proposition B holds. ∎ +**CHECKED corroboration.** `diag9.py`: for each of the 280 pairs `(J, m)` (`|J| = 5`, `m ∈ J`) some column `j ∈ J` has no root with `supp ⊆ J^c ∪ {m, j}` (the finite content of Case 2, 0 candidates for all 280). `caseb4.py` (chunked, 22,020,096 linear-core solutions): the case `r = 5` with one repeated column and `c = 4` distinct rows (singles with `supp ⊆ I ∪ {j}`) has **no** configuration with `s = 2` at both repeated terms (`lin_s2 = 0`) and none with pairwise non-orthogonal lines (`full = 0`); it enumerates one orientation of Case 1, and is not used in the proof. + +### 5.4 A second proof for `(4, ≥5)` with distinct lows (Case A; PROVEN, CHECKED `d4A*.py`) +Not needed (Theorem H(ii) already covers it) and kept because its finite check ships. Let `D_Q = 4`, `D_P ≥ 5`, `a ≠ a′`, `σ = D_P − 5`. Run Steps 1–3 of §4 with the roles of `D̂_Q` as 4: `#lossless ≥ 4`, `|I^c| ≤ 4`. The column catalogue (F3 transposed, `μ` with `w = 5`) says a lossless column (non-frame class) is a **column root swap**, `η_l ∝ c_{w_l}`, `w_l ∈ supp μ`; with `η_l ∈ span(e_{i_l}, e_{I^c})` and `η_l[i_l] ≠ 0`, `supp c_{w_l} = {i_l} ∪ T_l`, `T_l` a 3-subset of `I^c`. By S(3,4,8): `|I^c| = 3` gives one block, so `i_l` are equal: ≤ 1 lossless; `|I^c| = 4` a block gives 0; so `I^c` is a **non-block 4-set**, the four 3-subsets give four blocks, `#lossless = |I^c| = 4`, all slack is used (`ζ_P = σ`, no other loss). Then `d^R_a = 1`, and `a`'s row cannot be a swap (`w_P` slots are taken), so `x_a = γ e_m` is a frame vector. +`x_a = −Σ_l y2_l x_l = −Σ_{lossless} y2_l e_{i_l} − w`, `w ∈ W^⊥ := span` of the four non-frame dual rows `= (span c_{w_l})^⊥` (duality, `y_l ∝ c_{w_l}`), and `W^⊥ ∩ span(e_I) = 0` (the `x_l` are a basis); all `y2_l ≠ 0`. +(a) `m ∈ I`: `w ∈ span(e_I) ∩ W^⊥ = 0` so `x_a = −Σ y2_l e_{i_l}` has four non-zero entries: not a frame vector. +(b) `m ∈ I^c`: `γ e_m + Σ y2_l e_{i_l} ∈ W^⊥` is orthogonal to every `c_{w_l}`: `γ c_{w_l}[m] + y2_l c_{w_l}[i_l] = 0`, so `m ∈ supp c_{w_l}` for all four `l`, i.e. `m ∈ ∩ T_l`, but the four 3-subsets of a 4-set have empty intersection. +**CHECKED:** `clique2.py 4` on the non-block set `I^c = {0,1,2,4}` finds 16128 joint-feasible 4-cliques; `d4A.py`: 128 are column-swap configurations passing the non-orthogonality and joint `β` system; `d4A2.py`: `{0,1,2,3}` is a block (so `{0,1,2,4}` is the non-block orbit; `stab.py`: two orbits of 4-sets); `d4A3.py`: **0 of the 128** admit a frame row for term `a`. ∎ + +## 6. Coverage: every cell of `(D̂_P, D̂_Q)` has a proof + +`D̂` as in §3 (`D̂ = D` for `D ≥ 3`; `D̂ ∈ {2, 3}` for `D = 2`: one weight-7 low gives 2, two weight-7 lows give 3; `D̂ = 1` for `D ≤ 1`). By transposition only unordered cells matter. +| cell | proof | +|---|---| +| `D̂_P + D̂_Q ≤ 8` (includes `(4,4)`) | (L1), §3: `cost ≥ 72 − D̂_P − D̂_Q` | +| `min D̂ ≤ 3`, sum ≥ 9 (so `max D̂ ≥ 6`): `(1..3, 6..8)` | Theorem LOWD, §4 (any `K`, `a = a′` or not) | +| both `≥ 4`, lows in different terms (`a ≠ a′`) | Theorem H(ii), §5.1 (for `(4, ≥5)` also §5.4) | +| both `≥ 4`, one term is the low of both sides, `D_P + D_Q ≥ 10`, or `cost_b > 0` | Theorem H(i), §5.2 | +| both `≥ 4`, `a = a′`, `cost_b = 0`, `D_P + D_Q = 9`: `(4,5)`, `(5,4)` | Proposition B, §5.3 | +A cell with `min D̂ ≥ 4` has unique lows (F4) of weight ≤ 5, which is what §5 uses; `D = 3` (a weight-6 low, `|supp| ≤ 20`, F3 not available) is a `D̂ = 3` cell and is covered by §4. The disjoint sub-case also has the independent proof #2832 Theorem 3.13. + +## 7. Tightness (CHECKED `witness16.py`) + +Starting from the two-sided root-swap family (one row swap and one column swap, each with its own outside direction, cost 64; #2832 §3.7), frame terms are inflated with outside components that cancel at the swap line, and the `δ`-term's inside part is re-solved. Both decoders have `P Qᵀ = N₀` on **all** `112²` entries, `m = 10`, no proportional `p`'s or `q`'s, and cost exactly 64: +* **disjoint:** `|J_P| = |J_Q| = 3`, `J_P ∩ J_Q = ∅`, cost 64, `Σ(s − 1) = 16`. +* **shared:** `|J_P| = 4`, `|J_Q| = 3`, `|J_P ∩ J_Q| = 2`, cost 64. +Both have `Σ s = 26`, equal to the bound of Theorem H(ii) (`c_a = c_{a′} = 0`, `N₂ = w_P + w_Q = 2` with `D_P = D_Q = 8`): the bound 64 is attained inside the class, and the proof is exact there. + +## 8. What is and is not claimed +* **Claimed:** Theorem K3 (§0), CONDITIONAL on #2816 as listed; the coverage of §6; tightness at 64. +* **Not claimed:** anything for `m ≥ 11`, `(s, t) ≠ (1, 1)` (K1), the one-sided excess statement (K2), P120, or any κ. +* The proofs of §5 use the catalogue only through F3 on both sides; §4 uses it on one side and F1 on the other. No SAT solver and no random search enters any claim. + +## 9. Reproduce + +`bash verify.sh [/fresh/output/dir]` (Python ≥ 3.10 with numpy, sympy, networkx: `requirements.txt`; `PYTHON=` to choose; `timeout`/`gtimeout` if present). Phases, each stream a serial list under `timeout 1200` and `nice -n 10`, at most 4 processes: 0 manifest; 1 (`clique.py` → `null.pkl` | three `caseb4.py` chunks, plus the small scripts); 2 (four `clique2.py 5` chunks over the 93 sets `I^c`); 3 (`clique2.py 4`, `d4A.py`, `d4A2.py`, `d4A3.py` | `verify_cl.py` on four representatives, two streams | `sym.py`, `stab.py`); 4 `check_logs.py` asserts every number quoted above as PASS/FAIL. + +| Claim | Script | +|---|---| +| compatible classes (255 per `i`), 35400 pairs with deficient `Θ`-rank | `clique.py` | +| no 5-clique on any of the 93 `I^c` (|I^c| ≤ 3) | `clique2.py 5` | +| independent clique table (2, 2, 2, 4) | `verify_cl.py` | +| AGL(3,2) of order 1344 preserves `{O_z}`, compat | `stab.py`, `sym.py` | +| S(3,4,8) supports; `diag9`: 280 pairs, 0 candidates | `caseb4.py`, `diag9.py` (`enum9.py`, `lib2.py`) | +| single repeated column, `r = 5`: 22,020,096 solutions, 0 valid | `caseb4.py` (3 chunks) | +| §5.4 chain: 16128 → 128 → 0 | `clique2.py 4`, `d4A.py`, `d4A2.py`, `d4A3.py` | +| exact cost-64 witnesses | `witness16.py` (`swapfam.py`, `lib.py`) | + +Data: `data/data.json` (labels, frame coordinates, E8 roots of P112), identical to the file of #2832. diff --git a/research/two-sided-ten-term-floor/checks/caseb4.py b/research/two-sided-ten-term-floor/checks/caseb4.py new file mode 100644 index 0000000000..213a879e0b --- /dev/null +++ b/research/two-sided-ten-term-floor/checks/caseb4.py @@ -0,0 +1,50 @@ +import sys, itertools, os +sys.dont_write_bytecode=True +from enum9 import FCl, nonorth, v +import numpy as np +F=np.array(FCl,dtype=float) +sup=[frozenset(np.nonzero(F[t])[0]) for t in range(v)] +blocks=set(sup); print('#blocks',len(blocks),'S(3,4,8):',all(sum(1 for b in blocks if set(T)<=b)==1 for T in itertools.combinations(range(8),3)),flush=True) +root={tuple(F[t].astype(int)):t for t in range(v)}; root.update({tuple((-F[t]).astype(int)):t for t in range(v)}) +pairs=list(itertools.combinations(range(v),2)) +P1=np.array([F[a] for a,b in pairs]); P2=np.array([F[b] for a,b in pairs]) +G11=(P1*P1).sum(1);G12=(P1*P2).sum(1);G22=(P2*P2).sum(1);DET=G11*G22-G12*G12 +CACHE={} +def decomp(w): + kk=tuple(w) + if kk in CACHE: return CACHE[kk] + r1=P1@w; r2=P2@w; ok=np.abs(DET)>1e-9; d=np.where(ok,DET,1) + x1=(G22*r1-G12*r2)/d; x2=(G11*r2-G12*r1)/d + res=np.abs(x1[:,None]*P1+x2[:,None]*P2-w).max(1) + idx=np.nonzero(ok&(np.abs(x1)>1e-9)&(np.abs(x2)>1e-9)&(res<1e-9))[0] + CACHE[kk]=[pairs[k] for k in idx]; return CACHE[kk] +st=dict(rows_ok=0,lin=0,lin_s2=0,full=0,full_s2=0) +CH=int(sys.argv[1]) if len(sys.argv)>1 else 0; NCH=int(sys.argv[2]) if len(sys.argv)>2 else 1 # chunk CH of NCH over the 70 column sets J +for ji,J in enumerate(itertools.combinations(range(8),4)): + if ji%NCH!=CH: continue + I=[c for c in range(8) if c not in J] + for js in J: + singles=[j for j in J if j!=js] + cand=[[t for t in range(v) if F[t][j]!=0 and sup[t]<=set(I)|{j}] for j in singles] + if any(not c for c in cand): continue + for prod in itertools.product(*cand): + A=np.zeros((8,8)) + for j,t in zip(singles,prod): A[:,j]+=F[t]/F[t][j] + for wI in itertools.product((0,1,-1),repeat=4): + vs=[] + for i,wi in zip(I,wI): + row=np.eye(8)[i]-A[i]; row[js]-=wi + t=root.get(tuple(np.rint(row).astype(int))) if np.allclose(row,np.rint(row)) else None + if t is None: break + vs.append(t) + else: + st['rows_ok']+=1 + w=np.zeros(8); w[js]=1 + for i,wi in zip(I,wI): w[i]=wi + for (t1,t2) in decomp(w): + us=list(prod)+[t1,t2]; s2=F[t1][js]!=0 and F[t2][js]!=0 + st['lin']+=1; st['lin_s2']+=s2 + if len(set(us))==5 and len(set(vs))==4 and all(nonorth(a,b) for a,b in itertools.combinations(us,2)) and all(nonorth(a,b) for a,b in itertools.combinations(vs,2)): + st['full']+=1; st['full_s2']+=s2 +st={k:int(v) for k,v in st.items()} +print('chunk',CH,'of',NCH,st,flush=True) diff --git a/research/two-sided-ten-term-floor/checks/check_logs.py b/research/two-sided-ten-term-floor/checks/check_logs.py new file mode 100644 index 0000000000..c12bafb706 --- /dev/null +++ b/research/two-sided-ten-term-floor/checks/check_logs.py @@ -0,0 +1,65 @@ +# Step 3 of verify.sh: every number the README quotes from a script, as PASS/FAIL lines. usage: python check_logs.py LOGDIR +import os, sys, re, itertools, ast +D = sys.argv[1]; ok = True +def log(n): + p = os.path.join(D, n + '.log'); return open(p).read() if os.path.exists(p) else '' +def chk(name, cond): + global ok + print(('PASS ' if cond else 'FAIL ') + name); ok = ok and cond +# clique.py +t = log('clique') +chk('clique.py: 255 compatible non-frame classes for each i', 'compatible nonframe classes per i: [255, 255, 255, 255, 255, 255, 255, 255]' in t) +chk('clique.py: 35400 class pairs with deficient Theta-rank', 'pairs with nontrivial Theta-perp: 35400' in t) +# clique2.py 5 on all 93 sets +pat = re.compile(r'Ic \(([0-9, ]*)\) vertices (\d+) edges (\d+) max clique\(distinct i\) \d+ cliques>=5 passing joint (\d+)') +rows = [] +for k in range(4): rows += pat.findall(log('c2_%d' % k)) +sets = {tuple(int(x) for x in r[0].replace(' ', '').split(',') if x) for r in rows} +want = {c for k in range(4) for c in itertools.combinations(range(8), k)} +chk('clique2.py 5: all 93 sets I^c (|I^c| <= 3) were run (%d lines, %d distinct)' % (len(rows), len(sets)), len(rows) == 93 and sets == want) +chk('clique2.py 5: no 5-clique passes the joint test on any of the 93 sets', len(rows) == 93 and all(r[3] == '0' for r in rows)) +VE = {0: (2040, 3584), 1: (1785, 2856), 2: (1530, 9648), 3: (1275, 16496)} +chk('clique2.py 5: vertex/edge counts 2040/3584, 1785/2856, 1530/9648, 1275/16496 by |I^c|', + all((int(r[1]), int(r[2])) == VE[len([x for x in r[0].replace(' ', '').split(',') if x])] for r in rows)) +# verify_cl.py +cl = {} +for n in ['vcl_none', 'vcl_0', 'vcl_0_1', 'vcl_0_1_2']: + m = re.search(r'VERIFY Ic \(([0-9, ]*)\) vertices (\d+) edges (\d+) maximal clique sizes (\[.*\])', log(n)) + if m: cl[n] = (int(m.group(2)), int(m.group(3)), ast.literal_eval(m.group(4))) +for n, k, mx in [('vcl_none', 0, 2), ('vcl_0', 1, 2), ('vcl_0_1', 2, 2), ('vcl_0_1_2', 3, 4)]: + chk('verify_cl.py |I^c| = %d: vertices/edges %s, largest clique %d' % (k, VE[k], mx), n in cl and (cl[n][0], cl[n][1]) == VE[k] and max(s for s, _ in cl[n][2]) == mx) +chk('verify_cl.py {0,1,2}: 7936 maximal 4-cliques', 'vcl_0_1_2' in cl and (4, 7936) in cl['vcl_0_1_2'][2]) +# sym.py / stab.py +t = log('sym') +chk('sym.py: stabiliser of order 1344 preserves {O_z} and compat (0 failures), one orbit on 3-sets', 'group order 1344' in t and 'elements failing O-family/compat invariance: 0' in t and 'orbits on 3-sets: {(0, 1, 2)}' in t) +t = log('stab') +chk('stab.py: permutation part of order 1344; one orbit on 3-sets, two on 4-sets', 'perm group order 1344' in t and '3 orbits [(0, 1, 2)]' in t and '4 orbits [(0, 1, 2, 3), (0, 1, 2, 4)]' in t) +# witnesses +t = log('w16') +chk('witness16.py disjoint: P Q^T = N0 on all entries, m 10, cost 64, |J_P| = |J_Q| = 3, K empty, no proportional terms', + bool(re.search(r"disjoint .* m 10 PQ\^T=N0 mismatches 0 cost 64 \|J_P\| 3 \|J_Q\| 3 K \[\] proportional pairs \[\]", t))) +chk('witness16.py shared: exact, m 10, cost 64, |J_P| 4, |J_Q| 3, |K| = 2, no proportional terms', + bool(re.search(r"shared .* m 10 PQ\^T=N0 mismatches 0 cost 64 \|J_P\| 4 \|J_Q\| 3 K \[3, 4\] proportional pairs \[\]", t))) +# Case B +t = log('d9') +chk('diag9.py: 280 pairs (J, m), none has candidates for all five columns', "{'us': 0, 'nonorth': 0, 'sol': 0, 'vl': 0} {'nocand': 280}" in t) +tot = {'rows_ok': 0, 'lin': 0, 'lin_s2': 0, 'full': 0, 'full_s2': 0}; good = True +for k in range(3): + t = log('cb4_%d' % k) + m = re.search(r'chunk %d of 3 (\{.*\})' % k, t) + good = good and ('#blocks 14 S(3,4,8): True' in t) and bool(m) + if m: + for a, b in ast.literal_eval(m.group(1)).items(): tot[a] += b +chk('caseb4.py: 14 blocks form S(3,4,8) (each chunk)', good) +chk('caseb4.py: 917504 row patterns, 22020096 linear-core solutions, none with s = 2 at both repeated terms, none valid (lin_s2 = full = full_s2 = 0)', + tot == {'rows_ok': 917504, 'lin': 22020096, 'lin_s2': 0, 'full': 0, 'full_s2': 0}) +# Case A chain +t = log('c24') +chk('clique2.py 4 on I^c = {0,1,2,4}: 1020 vertices, 15936 edges, 16128 joint-feasible 4-cliques', 'Ic (0, 1, 2, 4) vertices 1020 edges 15936 max clique(distinct i) 4 cliques>=4 passing joint 16128' in t) +t = log('d4A') +chk('d4A.py: 16128 cliques, 128 column-swap configurations, 128 survive non-orthogonality + joint beta system', 'cliques 16128 all-line-class 5248 column-swap-compatible 128' in t and 'survive (non-orth swap lines + joint beta system): 128' in t) +t = log('d4A2') +chk('d4A2.py: {0,1,2,3} is a block; every configuration has 10 roots orthogonal to the four swap roots', '(0,1,2,3) is a block: True' in t and '[((10, 4), 128)]' in t) +t = log('d4A3') +chk('d4A3.py: 0 of 128 configurations admit a frame row for term a', 'configs 128 with an admissible frame row for term a: 0' in t) +print('ALL PASS' if ok else 'SOME FAIL'); sys.exit(0 if ok else 1) diff --git a/research/two-sided-ten-term-floor/checks/clique.py b/research/two-sided-ten-term-floor/checks/clique.py new file mode 100644 index 0000000000..f7517803d3 --- /dev/null +++ b/research/two-sided-ten-term-floor/checks/clique.py @@ -0,0 +1,75 @@ +# LOWD residual test: lossless frame-row dual terms j (x_j = e_i, i in I = [8]\Ic) with outside columns of compatible non-frame class z_j, +# eta_j in span(e_i, e_Ic), eta_j[i] != 0, pairwise eta_j - eta_j' ⟂ c_t for t in O_zj ∩ O_zj'. Find all sets of >= KMIN such terms. +import sys, json, itertools, pickle, numpy as np +from fractions import Fraction as Fr +import sympy as sp +D=json.load(open('data.json')); LAB=D['LAB']; FC=np.array(D['FC'],dtype=np.int64); v=112 +Lf=np.array(D['L']); F0=np.array(D['F0']) +# Omega: Bd[t][s] = LAB[t]^T G LAB[s] over F2 (Bd = 1 iff t = s or t orthogonal to s); solve the 81 unknowns of G exactly +def _solve_G(): + rows=[] + for t in range(v): + for s_ in range(v): + b=1 if (t==s_ or abs(Lf[t]@Lf[s_])<1e-9) else 0 + eq=0 + for a in range(9): + for c in range(9): + if (LAB[t]>>a)&1 and (LAB[s_]>>c)&1: eq|=1<<(9*a+c) + rows.append(eq|(b<<81)) + piv={} + for r in rows: + for p,pr in piv.items(): + if (r>>p)&1: r^=pr + low=[i for i in range(81) if (r>>i)&1] + if not low: + assert not (r>>81)&1, 'inconsistent'; continue + p=low[0] + for q in list(piv): + if (piv[q]>>p)&1: piv[q]^=r + piv[p]=r + assert len(piv)==81, 'G not determined' + G=np.zeros((9,9),dtype=np.int64) + for p,pr in piv.items(): G[p//9,p%9]=(pr>>81)&1 + return G +G=_solve_G() +par=lambda x: bin(x).count('1')&1 +O={z:[t for t in range(v) if par(z&LAB[t])] for z in range(1,512)} +framez=set() # classes of the 8 frame roots: O_z = lines orthogonal to f_i +for f in F0: + S_=set(t for t in range(v) if abs(Lf[t]@f)<1e-9) + framez|={z for z in range(1,512) if set(O[z])==S_} +assert len(framez)==8 +def rk2(rows): + B=[] + for r in rows: + for b in B: r=min(r,r^b) + if r: B.append(r) + return len(B) +def bits(vec): return sum(int(b)<>i)&1 for i in range(9)]); z=bits(G@xv%2); Ginv[z]=x +assert len(Ginv)==512 +off=[[t for t in range(v) if FC[t][i]!=0] for i in range(8)] +compat={i:[z for z in range(1,512) if z not in framez and rk2([LAB[t] for t in off[i]]+[Ginv[z]])==8] for i in range(8)} +print('compatible nonframe classes per i:',[len(compat[i]) for i in range(8)],flush=True) +# sanity: compat <=> rank Bd[Off f_i, L\O_z] == 7 +Bd=lambda t,s: par(bits(G@np.array([(LAB[s]>>k)&1 for k in range(9)])%2)&LAB[t]) +# nullspace of FC[Theta] for every pair z per Ic (|Ic|<=3): max clique size, # cliques >= KMIN passing the joint test +import sys, json, itertools, pickle, numpy as np +import sympy as sp +D=json.load(open('data.json')); LAB=D['LAB']; FC=np.array(D['FC'],dtype=np.int64); v=112 +par=lambda x: bin(x).count('1')&1 +O={z:set(t for t in range(v) if par(z&LAB[t])) for z in range(1,512)} +compat,null=pickle.load(open('null.pkl','rb')) +KMIN=int(sys.argv[1]); ICS=sys.argv[2] if len(sys.argv)>2 else 'all' +def theta(z,z2): return sorted(O[z]&O[z2]) +def rank(M): return np.linalg.matrix_rank(np.array(M,dtype=float)) if len(M) else 0 +def edge(i,z,i2,z2,S): + key=(min(z,z2),max(z,z2)) + if key not in null: return False + N=null[key] + if N=='ALL': return True + # subspace of span(N) supported in S + Nm=np.array(N).T # 8 x d + out=[c for c in range(8) if c not in S] + A=sp.Matrix(Nm[out,:].tolist()) if out else sp.zeros(0,Nm.shape[1]) + ker=A.nullspace() if out else [sp.eye(Nm.shape[1])[:,k] for k in range(Nm.shape[1])] + if not ker: return False + H=[sp.Matrix(Nm.tolist())*k for k in ker] + return any(h[i]!=0 for h in H) and any(h[i2]!=0 for h in H) +def joint(cl,Ic): + # unknowns: for each (i,z) in cl, eta on coords [i]+Ic + coords=[[i]+list(Ic) for i,z in cl]; off=[0] + for c in coords: off.append(off[-1]+len(c)) + rows=[] + for a in range(len(cl)): + for b in range(a+1,len(cl)): + for t in theta(cl[a][1],cl[b][1]): + r=[0]*off[-1] + for k,c in enumerate(coords[a]): r[off[a]+k]+=int(FC[t][c]) + for k,c in enumerate(coords[b]): r[off[b]+k]-=int(FC[t][c]) + rows.append(r) + M=sp.Matrix(rows) if rows else sp.zeros(1,off[-1]) + ker=M.nullspace() + if not ker: return False + return all(any(k[off[a]]!=0 for k in ker) for a in range(len(cl))) +Ics=[c for r in range(4) for c in itertools.combinations(range(8),r)] +if ICS!='all': Ics=[tuple(map(int,x.split(','))) if x else () for x in ICS.split(';')] +for Ic in Ics: + I=[i for i in range(8) if i not in Ic] + V=[(i,z) for i in I for z in compat[i]] + adj={x:set() for x in V} + for a in range(len(V)): + i,z=V[a] + for b in range(a+1,len(V)): + i2,z2=V[b] + if i2==i or z2==z: continue + if edge(i,z,i2,z2,set([i,i2])|set(Ic)): adj[V[a]].add(V[b]); adj[V[b]].add(V[a]) + ne=sum(len(s) for s in adj.values())//2 + # cliques with distinct i: DFS over vertices sorted by i + best=[0]; found=[] + def dfs(cl,cands): + if len(cl)>best[0]: best[0]=len(cl) + if len(cl)>=KMIN: + if joint(cl,Ic): found.append(list(cl)) + for x in sorted(cands): + nc={y for y in cands&adj[x] if y[0]>x[0]} + # bound: distinct i remaining + if len(cl)+1+len({y[0] for y in nc})=%d passing joint'%KMIN,len(found),flush=True) + if found: pickle.dump(found,open('found_%s.pkl'%('_'.join(map(str,Ic)) or 'none'),'wb')) diff --git a/research/two-sided-ten-term-floor/checks/d4A.py b/research/two-sided-ten-term-floor/checks/d4A.py new file mode 100644 index 0000000000..ff7b3f040c --- /dev/null +++ b/research/two-sided-ten-term-floor/checks/d4A.py @@ -0,0 +1,40 @@ +# D=4 case A filter: in KMIN=4 cliques, all classes must be line classes u_w with eta_j ∝ c_w, supp c_w ⊆ {i_j} ∪ Ic +import sys, pickle, json, itertools, numpy as np +from lib import Bd, LAB, C, n +par=lambda x: bin(x).count('1')&1 +lineclass={} +for w in range(n): + S=set(t for t in range(n) if Bd[t][w]==1) + zs=[z for z in range(1,512) if set(t for t in range(n) if par(z&LAB[t]))==S] + assert len(zs)==1; lineclass[zs[0]]=w +for f in sys.argv[1:]: + Ic=tuple(int(x) for x in f[6:-4].split('_')) if f!='found_none.pkl' else () + cl=pickle.load(open(f,'rb')) + good=[] + for c in cl: + if all(z in lineclass for i,z in c): + ws=[lineclass[z] for i,z in c] + if all(set(np.nonzero(C[w])[0])<=set([i])|set(Ic) and C[w][i]!=0 for (i,z),w in zip(c,ws)): good.append((c,ws)) + print(f,'cliques',len(cl),'all-line-class',sum(all(z in lineclass for i,z in c) for c in cl),'column-swap-compatible',len(good)) + for g in good[:5]: print(' ',g) +# filters on column-swap-compatible cliques: (1) swap lines pairwise non-orthogonal (Bd=0), (2) joint pair system with eta_j = beta_j c_wj +import sympy as sp +O={z:set(t for t in range(n) if par(z&LAB[t])) for z in range(1,512)} +for f in sys.argv[1:]: + Ic=tuple(int(x) for x in f[6:-4].split('_')) + cl=pickle.load(open(f,'rb')); surv=[] + for c in cl: + if not all(z in lineclass for i,z in c): continue + ws=[lineclass[z] for i,z in c] + if not all(set(np.nonzero(C[w])[0])<=set([i])|set(Ic) and C[w][i]!=0 for (i,z),w in zip(c,ws)): continue + f1=all(Bd[w][w2]==0 for w,w2 in itertools.combinations(ws,2)) + rows=[] + for a,b in itertools.combinations(range(4),2): + for t in sorted(O[c[a][1]]&O[c[b][1]]): + r=[0]*4; r[a]=sum(C[t][k]*C[ws[a]][k] for k in range(8)); r[b]=-sum(C[t][k]*C[ws[b]][k] for k in range(8)); rows.append(r) + ker=sp.Matrix(rows).nullspace() if rows else [sp.eye(4)[:,k] for k in range(4)] + f2=bool(ker) and all(any(k[j]!=0 for k in ker) for j in range(4)) + if f1 and f2: surv.append((c,ws)) + print(f,'survive (non-orth swap lines + joint beta system):',len(surv)) + pickle.dump(surv,open('d4A_surv.pkl','wb')) + for s in surv[:4]: print(' ',s) diff --git a/research/two-sided-ten-term-floor/checks/d4A2.py b/research/two-sided-ten-term-floor/checks/d4A2.py new file mode 100644 index 0000000000..a74d74b466 --- /dev/null +++ b/research/two-sided-ten-term-floor/checks/d4A2.py @@ -0,0 +1,15 @@ +import sys, pickle, itertools, numpy as np +from lib import Bd, C, n +from collections import Counter +surv=pickle.load(open('d4A_surv.pkl','rb')) +print('(0,1,2,3) is a block:', any(set(np.nonzero(C[t])[0])=={0,1,2,3} for t in range(n))) +h=Counter() +for c,ws in surv: + roots=[t for t in range(n) if all(sum(C[t][k]*C[w][k] for k in range(8))==0 for w in ws)] + # max pairwise non-orthogonal (Bd=0) subset + best=0 + for r in range(1,len(roots)+1): + if any(all(Bd[a][b]==0 for a,b in itertools.combinations(S,2)) for S in itertools.combinations(roots,r)): best=r + else: break + h[(len(roots),best)]+=1 +print('(#roots ⟂ all four c_w, max pairwise non-orth set):',sorted(h.items())) diff --git a/research/two-sided-ten-term-floor/checks/d4A3.py b/research/two-sided-ten-term-floor/checks/d4A3.py new file mode 100644 index 0000000000..166f4572da --- /dev/null +++ b/research/two-sided-ten-term-floor/checks/d4A3.py @@ -0,0 +1,13 @@ +# Case A kill check: a's row must be frame x_a ∝ e_m; m in I impossible (x_a = -Σ y2_j e_ij - w, w in W⊥, W⊥∩span e_I = 0, all y2_j≠0); +# m in I^c needs u = e_m + Σ β_j e_ij ⟂ all c_wj with β_j ≠ 0, i.e. m ∈ supp c_wj for all four j. Check over the 128 survivors. +import sys, pickle, numpy as np +from lib import C +surv=pickle.load(open('d4A_surv.pkl','rb')); Ic=(0,1,2,4); bad=0 +for c,ws in surv: + I=[i for i,z in c] + # exact: does W⊥ contain a vector e_m + Σ β_j e_ij (all β_j≠0)? solve per m + for m in Ic: + if all(C[w][m]!=0 for w in ws): bad+=1 + # and W⊥ ∩ span(e_I) = 0 (4 roots with distinct private coords i_j restricted to I: matrix [c_wj[i]] diagonal-nonzero) + M=np.array([[C[w][i] for i in I] for w in ws]); assert round(abs(np.linalg.det(M)))!=0 +print('configs',len(surv),'with an admissible frame row for term a:',bad) diff --git a/research/two-sided-ten-term-floor/checks/diag9.py b/research/two-sided-ten-term-floor/checks/diag9.py new file mode 100644 index 0000000000..941c8c3c70 --- /dev/null +++ b/research/two-sided-ten-term-floor/checks/diag9.py @@ -0,0 +1,35 @@ +from enum9 import * +import itertools +AMS=sorted({Fr(p,q) for p in range(-8,9) for q in range(1,9) if p!=0}) +cnt=dict(us=0,nonorth=0,sol=0,vl=0) +fail_i={} +for J in itertools.combinations(range(8),5): + Jc=[c for c in range(8) if c not in J] + for m in J: + cand={} + for j in J: + allowed=set(Jc)|{m,j} + cand[j]=[t for t in range(v) if FCl[t][j]!=0 and all(FCl[t][c]==0 for c in range(8) if c not in allowed)] + if any(len(cand[j])==0 for j in J): + fail_i['nocand']=fail_i.get('nocand',0)+1; continue + for prod in itertools.product(*[cand[j] for j in J]): + cnt['us']+=1 + if len(set(prod))<5 or not all(nonorth(a_,b_) for a_,b_ in itertools.combinations(prod,2)): continue + cnt['nonorth']+=1 + us=dict(zip(J,prod)) + a={c:Fr(1,FCl[us[c]][c]) for c in J if c!=m} + I=Jc+[m] + for am in AMS: + a2=dict(a);a2[m]=am + A=[[Fr(0)]*8 for _ in range(8)] + for c in J: + for i in range(8): A[i][c]=a2[c]*FCl[us[c]][i] + if any(A[r][c]!=Fr(int(r==c)) for r in range(8) if r not in I for c in range(8)): + fail_i['Irows']=fail_i.get('Irows',0)+1; break + ok=0 + for i in I: + w=[Fr(int(i==c))-A[i][c] for c in range(8)] + k=key(w) + if k is not None and k in RK: ok+=1 + fail_i[ok]=fail_i.get(ok,0)+1 +print(cnt,fail_i) diff --git a/research/two-sided-ten-term-floor/checks/enum9.py b/research/two-sided-ten-term-floor/checks/enum9.py new file mode 100644 index 0000000000..66054989f0 --- /dev/null +++ b/research/two-sided-ten-term-floor/checks/enum9.py @@ -0,0 +1,100 @@ +import sys, itertools, random, time, pickle +sys.argv=[sys.argv[0]]+sys.argv[1:] +from lib2 import * +FC=np.array(D['FC'],dtype=np.int64) +FCl=[tuple(int(a) for a in FC[t]) for t in range(v)] +def key(w): + j=next((i for i in range(8) if w[i]!=0),None) + if j is None: return None + c=w[j]; return tuple(Fr(a)/c for a in w) +RK={} +for t in range(v): + RK[key(FCl[t])]=t +def nonorth(a,b): return a!=b and Gm[a][b]!=0 +def solve_config(J,m,us,kR=5): + """J: list of 5 column idx; m in J; us: dict j->root line t for R-terms. returns terms or None""" + Jc=[c for c in range(8) if c not in J]; I=Jc+[m] + # a_c for c in J\m + a={} + for c in J: + if c==m: continue + val=FCl[us[c]][c] + if val==0: return None + a[c]=Fr(1,val) + # a_m free: try values later; first determine v_i for i in Jc using a (they involve only c in J incl m!) + # A[i,c]=a_c*c_{u_c}[i], includes c=m with a_m unknown. Solve for a_m by requiring roots. + outs=[] + for am in [Fr(x,y) for x in (1,-1,2,-2,3,-3,1,1) for y in (1,2,3,4)]: + a2=dict(a); a2[m]=am + A=[[Fr(0)]*8 for _ in range(8)] + for c in J: + for i in range(8): A[i][c]=a2[c]*FCl[us[c]][i] + vs={} + ok=True + for i in I: + w=[Fr(int(i==c))-A[i][c] for c in range(8)] + k=key(w) + if k is None or k not in RK: ok=False;break + vs[i]=(w,RK[k]) + if not ok: continue + # rows not in I must match identity: A row r = e_r + if any(A[r][c]!=Fr(int(r==c)) for r in range(8) if r not in I for c in range(8)): continue + outs.append((a2,vs)) + return outs +def terms_from(J,us,a2,vs): + X=[];Y=[];types=[] + for c in J: + x=[a2[c]*FCl[us[c]][i] for i in range(8)]; y=[Fr(int(i==c)) for i in range(8)] + X.append(x);Y.append(y);types.append(('R',us[c],c)) + for i,(w,t) in vs.items(): + x=[Fr(int(r==i)) for r in range(8)]; X.append(x);Y.append(list(w));types.append(('C',t,i)) + return X,Y,types +def kernel(M,ncols): + # M list of rows (len ncols) Fractions -> basis of right nullspace + A=[r[:] for r in M]; piv=[];r=0 + for c in range(ncols): + p=next((i for i in range(r,len(A)) if A[i][c]!=0),None) + if p is None: continue + A[r],A[p]=A[p],A[r]; pv=A[r][c]; A[r]=[x/pv for x in A[r]] + for i in range(len(A)): + if i!=r and A[i][c]!=0: + f=A[i][c]; A[i]=[x-f*y for x,y in zip(A[i],A[r])] + piv.append(c); r+=1 + free=[c for c in range(ncols) if c not in piv] + out=[] + for f in free: + v_=[Fr(0)]*ncols; v_[f]=Fr(1) + for i,c in enumerate(piv): v_[c]=-A[i][f] + out.append(v_) + return out +if __name__=='__main__': + chunk=int(sys.argv[1]); nch=int(sys.argv[2]); TL=float(sys.argv[3]) + t0=time.time(); stats={}; nconf=0; best=999 + Js=list(itertools.combinations(range(8),5)) + for ji,J in enumerate(Js): + if ji%nch!=chunk: continue + Jc=[c for c in range(8) if c not in J] + for m in J: + cand={} + for j in J: + allowed=set(Jc)|{m,j} + cand[j]=[t for t in range(v) if FCl[t][j]!=0 and all(FCl[t][c]==0 for c in range(8) if c not in allowed)] + # m: support subset of Jc+m + for prod in itertools.product(*[cand[j] for j in J]): + us=dict(zip(J,prod)) + if len(set(prod))<5: continue + if not all(nonorth(a_,b_) for a_,b_ in itertools.combinations(prod,2)): continue + res=solve_config(J,m,us) + if not res: continue + for a2,vs in res: + vl=[t for (_,t) in vs.values()] + if len(set(vl))<4 or not all(nonorth(a_,b_) for a_,b_ in itertools.combinations(vl,2)): continue + X,Y,types=terms_from(J,us,a2,vs) + # check sum x y^T = I + S=[[sum(X[k][i]*Y[k][j] for k in range(9)) for j in range(8)] for i in range(8)] + assert all(S[i][j]==int(i==j) for i in range(8) for j in range(8)) + nconf+=1 + stats.setdefault('conf',[]).append((J,m,prod,tuple(vl))) + if time.time()-t0>TL: break + print('chunk',chunk,'configs',nconf,flush=True) + pickle.dump(stats,open(f'conf9_{chunk}.pkl','wb')) diff --git a/research/two-sided-ten-term-floor/checks/lib.py b/research/two-sided-ten-term-floor/checks/lib.py new file mode 100644 index 0000000000..b2674a2af3 --- /dev/null +++ b/research/two-sided-ten-term-floor/checks/lib.py @@ -0,0 +1,64 @@ +# TWINSWAP common: P112 data, exact decoder builder/checker. python = W/venv/bin/python +import json, os +from fractions import Fraction as Fr +_D=json.load(open(os.path.join(os.path.dirname(os.path.abspath(__file__)),'data.json'))) +Lr=[[int(round(x*1)) if abs(x-round(x))<1e-9 else x for x in r] for r in _D['L']] +n=len(Lr) +C=[[int(x) for x in row] for row in _D['FC']] # F0 coords c_t (entries 0,±1, four nonzero) +def dotL(a,b): return sum(x*y for x,y in zip(a,b)) +G=[[dotL(Lr[t],Lr[s]) for s in range(n)] for t in range(n)] +Bd=[[1 if (t==s or abs(G[t][s])<1e-9) else 0 for s in range(n)] for t in range(n)] +LAB=_D['LAB']; ZF=_D['Z'] +assert all(sum(C[t][i]*C[s][i] for i in range(8))==2*G[t][s] for t in range(n) for s in range(n)) +# N0 = G/2 = C' C'^T with C' = C/2 +def N0(t,s): return Fr(G[t][s])/2 if True else None +def f2rank(vs): + basis=[] + for v in vs: + for b in basis: v=min(v,v^b) + if v: basis.append(v) + return len(basis) +def bdrank(R,A): + # rank over F2 of Bd[R,A] + rows=[] + for t in R: + x=0 + for j,s in enumerate(A): + if Bd[t][s]: x|=1<0] + out=set() + def dfs(cur,cands): + if len(cur)==8: out.add(tuple(cur)); return + for k,j in enumerate(cands): + dfs(cur+[j],[c for c in cands[k+1:] if G0[j,c]==0]) + dfs([],rep) + return [list(f) for f in out] diff --git a/research/two-sided-ten-term-floor/checks/manifest_check.py b/research/two-sided-ten-term-floor/checks/manifest_check.py new file mode 100644 index 0000000000..0c39981713 --- /dev/null +++ b/research/two-sided-ten-term-floor/checks/manifest_check.py @@ -0,0 +1,12 @@ +# Step 0 of verify.sh: every line of MANIFEST.sha256 (" ") must match the file; the manifest must list every file of the package except itself. +import hashlib, os, sys +root = os.path.dirname(os.path.dirname(os.path.abspath(__file__))) +listed = {} +for l in open(os.path.join(root, 'MANIFEST.sha256')): + h, p = l.rstrip('\n').split(' ', 1); listed[p] = h +bad = [p for p, h in listed.items() if not os.path.isfile(os.path.join(root, p)) or hashlib.sha256(open(os.path.join(root, p), 'rb').read()).hexdigest() != h] +allf = {os.path.relpath(os.path.join(d, f), root) for d, _, fs in os.walk(root) for f in fs if '__pycache__' not in d and f != 'MANIFEST.sha256' and not f.endswith('.pyc')} +extra = sorted(allf - set(listed)) +print(('FAIL' if bad else 'PASS') + ' manifest: %d files hash-checked, %d mismatching %s' % (len(listed), len(bad), bad[:3])) +print(('FAIL' if extra else 'PASS') + ' manifest lists every package file (%d unlisted %s)' % (len(extra), extra[:3])) +sys.exit(1 if bad or extra else 0) diff --git a/research/two-sided-ten-term-floor/checks/stab.py b/research/two-sided-ten-term-floor/checks/stab.py new file mode 100644 index 0000000000..a857df5206 --- /dev/null +++ b/research/two-sided-ten-term-floor/checks/stab.py @@ -0,0 +1,30 @@ +# permutation part of the frame stabiliser: perms pi of 8 coords s.t. {supp c_t} blocks map to blocks (sign patterns handled by sign flips) +import json, itertools, numpy as np +D=json.load(open('data.json')); FC=np.array(D['FC'],dtype=int); v=112 +lines=set() +for t in range(v): + r=tuple(FC[t]); r2=tuple(-x for x in r); lines.add(max(r,r2)) +blocks=set(frozenset(np.nonzero(FC[t])[0]) for t in range(v)); print('blocks',len(blocks)) +G=[] +for p in itertools.permutations(range(8)): + if all(frozenset(p[i] for i in b) in blocks for b in blocks): + # need sign vector s with signed perm preserving lines + ok=False + for s in itertools.product([1,-1],repeat=8): + good=True + for r in lines: + w=[0]*8 + for i in range(8): w[p[i]]=s[i]*r[i] + w=tuple(w); w2=tuple(-x for x in w) + if max(w,w2) not in lines: good=False;break + if good: ok=True;break + if ok: G.append(p) +print('perm group order',len(G)) +for k in range(5): + orb=set() + reps=[] + for c in itertools.combinations(range(8),k): + if frozenset(c) in orb: continue + reps.append(c) + for p in G: orb.add(frozenset(p[i] for i in c)) + print(k,'orbits',reps) diff --git a/research/two-sided-ten-term-floor/checks/swapfam.py b/research/two-sided-ten-term-floor/checks/swapfam.py new file mode 100644 index 0000000000..4445f6c543 --- /dev/null +++ b/research/two-sided-ten-term-floor/checks/swapfam.py @@ -0,0 +1,98 @@ +# Two-sided root-swap family: row swaps (j_a, r_a) and column swaps (j_b, r_b) + frame terms. +# Inside rank-one terms form a dual basis pair: row swap (x=c_ra, y=e_ja), col swap (x=e_jb, y=c_rb), frame terms x=e_i or y=e_i. +# Search min #bad (frame slots with neither side frame) over all choices; then build exactly, verify P Q^T = N0, cost. +import itertools, sys +from lib import * +import sympy as sp +roots_by=[ [t for t in range(n) if C[t][j]] for j in range(8)] +def feasible_search(kr,kc,want_all=False): + best=(99,None) + for Jr in itertools.combinations(range(8),kr): + rest=[i for i in range(8) if i not in Jr] + for Jc in itertools.combinations(rest,kc): + if kr and Jr[0]!=0 and kc==0: continue # symmetry trim (one-sided) + J=set(Jr)|set(Jc); I=[i for i in range(8) if i not in J] + rc=[[t for t in roots_by[j] if supp8(t)&set(Jr)=={j}] for j in Jr] + cc=[[t for t in roots_by[j] if supp8(t)&set(Jc)=={j}] for j in Jc] + # backtrack rows then cols with orthogonality row/col; minimise bad + def rec_rows(a,chosen,U): + nonlocal best + if a==kr: return rec_cols(0,chosen,[],U,set()) + seen=set() + for t in rc[a]: + key=(frozenset(supp8(t)),) + if t in chosen: continue + rec_rows(a+1,chosen+[t],U|supp8(t)) + if best[0]==0: return + def rec_cols(b,rows,cols,U,V): + nonlocal best + bad=len([i for i in I if i in U and i in V]) + if bad>=best[0]: return + if b==kc: + best=(bad,(Jr,Jc,rows,cols)); return + for t in cc[b]: + if t in cols: continue + if any(sum(C[t][i]*C[r][i] for i in range(8))!=0 for r in rows): continue + rec_cols(b+1,rows,cols+[t],U,V|supp8(t)) + if best[0]==0: return + rec_rows(0,[],set()) + if best[0]==0: return best + return best +def build_family(Jr,Jc,rows,cols,verbose=True): + kr,kc=len(Jr),len(Jc) + J=set(Jr)|set(Jc); I=[i for i in range(8) if i not in J] + U=set().union(*[supp8(t) for t in rows]) if rows else set() + V=set().union(*[supp8(t) for t in cols]) if cols else set() + terms=[] # (xpres or None, ypres or None, kind) + for j,t in zip(Jr,rows): terms.append((croot(t),e(j),('row',j,t))) + for j,t in zip(Jc,cols): terms.append((e(j),croot(t),('col',j,t))) + for i in I: + if i not in V: terms.append((e(i),None,('fx',i))) + elif i not in U: terms.append((None,e(i),('fy',i))) + else: terms.append((None,None,('bad',i))) + for k,tm in enumerate(terms): + if tm[0] is not None and tm[1] is not None: + ip=sum(a*b for a,b in zip(tm[0],tm[1])); assert ip!=0 + terms[k]=(tm[0],[v/ip for v in tm[1]],tm[2]) + PY=[k for k,tm in enumerate(terms) if tm[1] is not None] + X=[None]*8 + for k,tm in enumerate(terms): + if tm[0] is not None: X[k]=tm[0] + # unknown x_l: =delta_lk for k in PY; pick particular solution, generic in free part (deterministic) + for l,tm in enumerate(terms): + if X[l] is not None: continue + xs=sp.symbols('x0:8'); eqs=[sum(xs[i]*terms[k][1][i] for i in range(8))-(1 if k==l else 0) for k in PY] + sol=sp.solve(eqs,xs,dict=True)[0] + free=[s for s in xs if s not in sol] + vals={s:(l+2*idx+1) for idx,s in enumerate(free)} + X[l]=[Fr(str(sp.sympify(sol.get(s,s)).subs(vals))) for s in xs] + Xm=sp.Matrix([[sp.Rational(str(v)) for v in r] for r in X]); Ym=(Xm.inv()).T + Y=[[Fr(str(Ym[k,i])) for i in range(8)] for k in range(8)] + for k in PY: assert Y[k]==terms[k][1], ('dual mismatch',k) + E=[delta(t) for t in rows]; F=[delta(t) for t in cols] + Xh=[];Yh=[];names=[] + for k,tm in enumerate(terms): + kind=tm[2] + if kind[0]=='row': + a=Jr.index(kind[1]); t=kind[2]; z2=[Fr(0)]*kr; z2b=[Fr(0)]*kr; z2[a]=Fr(-2); z2b[a]=Fr(2) + Xh+= [(X[k],z2),([Fr(0)]*8,z2b)]; Yh+=[(Y[k],[Fr(0)]*kc)]*2; names+=['row-swap p\'','row-swap delta'] + elif kind[0]=='col': + b=Jc.index(kind[1]); t=kind[2]; z2=[Fr(0)]*kc; z2b=[Fr(0)]*kc; val=sum(Fr(C[t][i],2)*Y[k][i] for i in range(8)); z2[b]=-val; z2b[b]=val + Yh+= [(Y[k],z2),([Fr(0)]*8,z2b)]; Xh+=[(X[k],[Fr(0)]*kr)]*2; names+=['col-swap q\'','col-swap delta'] + else: + Xh.append((X[k],[Fr(0)]*kr)); Yh.append((Y[k],[Fr(0)]*kc)); names.append('frame '+kind[0]) + if not verbose: return Xh,Yh,E,F,names + P,Q=build(Xh,Yh,E,F) + bad=check(P,Q,masked=False); cs=costs(P,Q) + if verbose: + print(f' kr={kr} kc={kc} Jr={Jr} Jc={Jc} rows={rows} cols={cols} m={len(P)} exact PQ^T=N0 mismatches={bad} cost={sum(cs)}') + print(' ',list(zip(names,cs))) + return bad,sum(cs) +if __name__=='__main__': + for kr in range(0,5): + for kc in range(kr,9-kr): + if kr+kc==0 or kr+kc>8: continue + b,ex=feasible_search(kr,kc) + print(f'(k_r,k_c)=({kr},{kc}): min #both-nonframe frame slots = {b}' + ('' if ex else ' (no admissible config)')) + if ex: build_family(*ex) + sys.stdout.flush() diff --git a/research/two-sided-ten-term-floor/checks/sym.py b/research/two-sided-ten-term-floor/checks/sym.py new file mode 100644 index 0000000000..a93d0b635b --- /dev/null +++ b/research/two-sided-ten-term-floor/checks/sym.py @@ -0,0 +1,42 @@ +# Audit: verify that the signed-permutation frame stabiliser preserves the full L3 structure (O_z family, compat, frame classes), +# so the AGL(3,2) orbit reduction of I^c is legitimate. Run from cards/LOWD. +import json, itertools, pickle, numpy as np +D=json.load(open('data.json')); FC=[tuple(int(x) for x in r) for r in D['FC']]; LAB=D['LAB']; v=112 +par=lambda x: bin(x).count('1')&1 +O={z:frozenset(t for t in range(v) if par(z&LAB[t])) for z in range(1,512)} +Oinv={} +for z,s in O.items(): Oinv.setdefault(s,[]).append(z) +assert all(len(l)==1 for l in Oinv.values()), 'O_z not injective' +compat,null=pickle.load(open('null.pkl','rb')) +lineidx={} +for t,r in enumerate(FC): lineidx[r]=t; lineidx[tuple(-x for x in r)]=t +blocks=set(frozenset(i for i in range(8) if FC[t][i]) for t in range(v)) +G=[] +for p in itertools.permutations(range(8)): + if not all(frozenset(p[i] for i in b) in blocks for b in blocks): continue + for s in itertools.product([1,-1],repeat=8): + pi=[] + for r in FC: + w=[0]*8 + for i in range(8): w[p[i]]=s[i]*r[i] + w=tuple(w) + if w not in lineidx: break + pi.append(lineidx[w]) + else: + G.append((p,pi)); break +print('group order',len(G)) +bad=0 +for p,pi in G: + zmap={} + for z in range(1,512): + img=frozenset(pi[t] for t in O[z]) + if img not in Oinv: bad+=1; break + zmap[z]=Oinv[img][0] + else: + for i in range(8): + if set(zmap[z] for z in compat[i])!=set(compat[p[i]]): bad+=1; break +print('elements failing O-family/compat invariance:',bad) +reps=set() +for c in itertools.combinations(range(8),3): + reps.add(min(tuple(sorted(p[i] for i in c)) for p,_ in G)) +print('orbits on 3-sets:',reps) diff --git a/research/two-sided-ten-term-floor/checks/verify_cl.py b/research/two-sided-ten-term-floor/checks/verify_cl.py new file mode 100644 index 0000000000..83d9b6ebf2 --- /dev/null +++ b/research/two-sided-ten-term-floor/checks/verify_cl.py @@ -0,0 +1,26 @@ +# Independent re-implementation of the L3 clique test (no null.pkl/compat from clique.py): +# compat via exact Bd-rank (TWINSWAP lib), edge via row-space criterion: e_i, e_i2 not in rowspace(FC[Theta][:,S]). +import sys, itertools, numpy as np, networkx as nx +from lib import bdrank, LAB, C, n +from collections import Counter +FC=np.array(C,dtype=float); par=lambda x: bin(x).count('1')&1 +O={z:frozenset(t for t in range(n) if par(z&LAB[t])) for z in range(1,512)} +offs=[[t for t in range(n) if C[t][i]!=0] for i in range(8)] +compat={i:[z for z in range(1,512) if bdrank(offs[i],[t for t in range(n) if t not in O[z]])==7] for i in range(8)} +rk=np.linalg.matrix_rank +Ic=tuple(map(int,sys.argv[1].split(','))) if len(sys.argv)>1 and sys.argv[1] else () +I=[i for i in range(8) if i not in Ic] +V=[(i,z) for i in I for z in compat[i]] +Gr=nx.Graph(); Gr.add_nodes_from(V) +for a in range(len(V)): + i,z=V[a] + for b in range(a+1,len(V)): + i2,z2=V[b] + if i2==i or z2==z: continue + Th=sorted(O[z]&O[z2]); S=sorted(set([i,i2])|set(Ic)) + if not Th: Gr.add_edge(V[a],V[b]); continue + B=FC[Th][:,S]; r=rk(B) + ei=np.zeros(len(S)); ei[S.index(i)]=1; ej=np.zeros(len(S)); ej[S.index(i2)]=1 + if rk(np.vstack([B,ei]))>r and rk(np.vstack([B,ej]))>r: Gr.add_edge(V[a],V[b]) +cs=Counter(len(c) for c in nx.find_cliques(Gr)) +print('VERIFY Ic',Ic,'vertices',len(V),'edges',Gr.number_of_edges(),'maximal clique sizes',sorted(cs.items()),flush=True) diff --git a/research/two-sided-ten-term-floor/checks/witness16.py b/research/two-sided-ten-term-floor/checks/witness16.py new file mode 100644 index 0000000000..7bbe5852ba --- /dev/null +++ b/research/two-sided-ten-term-floor/checks/witness16.py @@ -0,0 +1,48 @@ +# Exact tightness witnesses in WALL's OPEN class: (1,1), m=10, Lemma-D normalised, |J_P|,|J_Q| >= 3, cost 64 (E_Q+E_P = 16). +# Start: two-sided swap member (k_r,k_c)=(1,1) (|J_P|=|J_Q|=2), inflate frame terms with outside components cancelling at the swap line. +from swapfam import feasible_search, build_family +from lib import * +b,ex=feasible_search(1,1); Jr,Jc,rows,cols=ex; r,rp=rows[0],cols[0] +def inflate(mode): + Xh,Yh,E,F,names=build_family(*ex,verbose=False) + Xh=[(list(x),list(x2)) for x,x2 in Xh]; Yh=[(list(y),list(y2)) for y,y2 in Yh] + iR=names.index('row-swap delta'); iC=names.index('col-swap delta') + fx=[k for k,nm in enumerate(names) if nm=='frame fx']; fy=[k for k,nm in enumerate(names) if nm=='frame fy'] + def xfr(k): return [i for i in range(8) if Xh[k][0][i]!=0] + def yfr(k): return [i for i in range(8) if Yh[k][0][i]!=0] + # column side: y-frame term k with r' in Off(f_i): add y2_k = -(C'y_k)(r'), fix x of col-delta term + def col_inflate(k): + val=sum(Fr(C[rp][i],2)*Yh[k][0][i] for i in range(8)); assert val!=0 + Yh[k][1][0]=-val + vC=Yh[iC][1][0] + Xh[iC]=([a - (-val/vC)*b for a,b in zip(Xh[iC][0],Xh[k][0])],Xh[iC][1]) + def row_inflate(k): + val=sum(Fr(C[r][i],2)*Xh[k][0][i] for i in range(8)); assert val!=0 + Xh[k][1][0]=-val + vR=Xh[iR][1][0] + Yh[iR]=([a - (-val/vR)*b for a,b in zip(Yh[iR][0],Yh[k][0])],Yh[iR][1]) + candC=[k for k in fy if Yh[k][0] and sum(Fr(C[rp][i],2)*Yh[k][0][i] for i in range(8))!=0 and len(yfr(k))==1] + candR=[k for k in fx if sum(Fr(C[r][i],2)*Xh[k][0][i] for i in range(8))!=0 and len(xfr(k))==1] + if mode=='disjoint': + col_inflate(candC[0]); row_inflate(candR[0]); tag=('Q+',names[candC[0]],'P+',names[candR[0]]) + else: + # same frame term on both sides: a y-frame term k with r' in its column Off and r in Off(x_k) + both=[k for k in fy+fx if sum(Fr(C[rp][i],2)*Yh[k][0][i] for i in range(8))!=0 and sum(Fr(C[r][i],2)*Xh[k][0][i] for i in range(8))!=0] + k=both[0]; col_inflate(k); row_inflate(k) + # restore x2.y2 = 0 by giving the col-delta term an x2 part (its y-inside is 0, so the J_P circuit is untouched) + s=Xh[k][1][0]*Yh[k][1][0] + Xh[iC]=(Xh[iC][0],[-s/Yh[iC][1][0]]) + tag=('K-term',names[k]) + P,Q=build(Xh,Yh,E,F) + bad=check(P,Q,masked=False); cs=costs(P,Q) + JP=[k for k in range(len(Xh)) if any(Xh[k][1])]; JQ=[k for k in range(len(Yh)) if any(Yh[k][1])] + # Lemma D: no two proportional p's or q's + def prop(u,v): + nz=[t for t in range(n) if u[t]!=0 or v[t]!=0] + if any((u[t]==0)!=(v[t]==0) for t in nz): return False + c=v[nz[0]]/u[nz[0]]; return all(v[t]==c*u[t] for t in nz) + pp=[(i,j) for i in range(len(P)) for j in range(i+1,len(P)) if prop(P[i],P[j]) or prop(Q[i],Q[j])] + s=[9-c for c in cs] + print(mode,tag,'m',len(P),'PQ^T=N0 mismatches',bad,'cost',sum(cs),'|J_P|',len(JP),'|J_Q|',len(JQ),'K',sorted(set(JP)&set(JQ)),'proportional pairs',pp) + print(' per-term (name,cost):',list(zip(names,cs)),' sum(s-1)=',sum(x-1 for x in s)) +inflate('disjoint'); inflate('shared') diff --git a/research/two-sided-ten-term-floor/data/data.json b/research/two-sided-ten-term-floor/data/data.json new file mode 100644 index 0000000000..2b799f9238 --- /dev/null +++ b/research/two-sided-ten-term-floor/data/data.json @@ -0,0 +1 @@ +{"LAB": [457, 211, 3, 281, 349, 71, 379, 97, 195, 473, 373, 111, 403, 137, 89, 323, 263, 29, 289, 59, 153, 387, 303, 53, 399, 149, 425, 179, 17, 267, 423, 189, 69, 351, 99, 377, 475, 193, 109, 375, 133, 415, 307, 41, 163, 441, 277, 15, 257, 429, 21, 419, 51, 389, 61, 145, 365, 219, 355, 463, 325, 489, 81, 487, 167, 273, 169, 5, 143, 35, 411, 45, 465, 381, 197, 371, 227, 341, 237, 65, 47, 409, 33, 141, 7, 171, 275, 165, 345, 501, 77, 507, 107, 477, 101, 201, 147, 63, 391, 49, 417, 23, 431, 259, 255, 329, 241, 93, 215, 123, 451, 117], "Z": [321, 209, 317, 173, 91, 459, 39, 439], "FC": [[1, 1, 0, 0, 1, 1, 0, 0], [1, -1, 0, 0, 1, -1, 0, 0], [1, 1, 0, 0, 1, -1, 0, 0], [1, -1, 0, 0, 1, 1, 0, 0], [1, 0, 1, 0, 1, 0, 1, 0], [1, 0, -1, 0, 1, 0, -1, 0], [1, 0, 1, 0, 1, 0, -1, 0], [1, 0, -1, 0, 1, 0, 1, 0], [1, 0, 0, 1, 1, 0, 0, 1], [1, 0, 0, -1, 1, 0, 0, -1], [1, 0, 0, 1, 1, 0, 0, -1], [1, 0, 0, -1, 1, 0, 0, 1], [1, 1, 0, 0, -1, 1, 0, 0], [1, -1, 0, 0, -1, -1, 0, 0], [1, 1, 0, 0, -1, -1, 0, 0], [1, -1, 0, 0, -1, 1, 0, 0], [1, 0, 1, 0, -1, 0, 1, 0], [1, 0, -1, 0, -1, 0, -1, 0], [1, 0, 1, 0, -1, 0, -1, 0], [1, 0, -1, 0, -1, 0, 1, 0], [1, 0, 0, 1, -1, 0, 0, 1], [1, 0, 0, -1, -1, 0, 0, -1], [1, 0, 0, 1, -1, 0, 0, -1], [1, 0, 0, -1, -1, 0, 0, 1], [0, 1, 1, 0, 0, 1, 1, 0], [0, 1, -1, 0, 0, 1, -1, 0], [0, 1, 1, 0, 0, 1, -1, 0], [0, 1, -1, 0, 0, 1, 1, 0], [0, 1, 0, 1, 0, 1, 0, 1], [0, 1, 0, -1, 0, 1, 0, -1], [0, 1, 0, 1, 0, 1, 0, -1], [0, 1, 0, -1, 0, 1, 0, 1], [0, 1, 1, 0, 0, -1, 1, 0], [0, 1, -1, 0, 0, -1, -1, 0], [0, 1, 1, 0, 0, -1, -1, 0], [0, 1, -1, 0, 0, -1, 1, 0], [0, 1, 0, 1, 0, -1, 0, 1], [0, 1, 0, -1, 0, -1, 0, -1], [0, 1, 0, 1, 0, -1, 0, -1], [0, 1, 0, -1, 0, -1, 0, 1], [0, 0, 1, 1, 0, 0, 1, 1], [0, 0, 1, -1, 0, 0, 1, -1], [0, 0, 1, 1, 0, 0, 1, -1], [0, 0, 1, -1, 0, 0, 1, 1], [0, 0, 1, 1, 0, 0, -1, 1], [0, 0, 1, -1, 0, 0, -1, -1], [0, 0, 1, 1, 0, 0, -1, -1], [0, 0, 1, -1, 0, 0, -1, 1], [1, 1, 1, 1, 0, 0, 0, 0], [1, 1, 1, -1, 0, 0, 0, 0], [1, 1, 0, 0, 0, 0, 1, 1], [1, 1, 0, 0, 0, 0, 1, -1], [1, 1, 0, 0, 0, 0, -1, 1], [1, 1, 0, 0, 0, 0, -1, -1], [1, 1, -1, 1, 0, 0, 0, 0], [1, 1, -1, -1, 0, 0, 0, 0], [1, 0, 1, 0, 0, 1, 0, 1], [1, 0, 1, 0, 0, 1, 0, -1], [1, 0, 0, 1, 0, 1, 1, 0], [1, 0, 0, -1, 0, 1, 1, 0], [1, 0, 0, 1, 0, 1, -1, 0], [1, 0, 0, -1, 0, 1, -1, 0], [1, 0, -1, 0, 0, 1, 0, 1], [1, 0, -1, 0, 0, 1, 0, -1], [1, 0, 1, 0, 0, -1, 0, 1], [1, 0, 1, 0, 0, -1, 0, -1], [1, 0, 0, 1, 0, -1, 1, 0], [1, 0, 0, -1, 0, -1, 1, 0], [1, 0, 0, 1, 0, -1, -1, 0], [1, 0, 0, -1, 0, -1, -1, 0], [1, 0, -1, 0, 0, -1, 0, 1], [1, 0, -1, 0, 0, -1, 0, -1], [1, -1, 1, 1, 0, 0, 0, 0], [1, -1, 1, -1, 0, 0, 0, 0], [1, -1, 0, 0, 0, 0, 1, 1], [1, -1, 0, 0, 0, 0, 1, -1], [1, -1, 0, 0, 0, 0, -1, 1], [1, -1, 0, 0, 0, 0, -1, -1], [1, -1, -1, 1, 0, 0, 0, 0], [1, -1, -1, -1, 0, 0, 0, 0], [0, 1, 1, 0, 1, 0, 0, 1], [0, 1, 1, 0, 1, 0, 0, -1], [0, 1, 0, 1, 1, 0, 1, 0], [0, 1, 0, -1, 1, 0, 1, 0], [0, 1, 0, 1, 1, 0, -1, 0], [0, 1, 0, -1, 1, 0, -1, 0], [0, 1, -1, 0, 1, 0, 0, 1], [0, 1, -1, 0, 1, 0, 0, -1], [0, 0, 1, 1, 1, 1, 0, 0], [0, 0, 1, -1, 1, 1, 0, 0], [0, 0, 0, 0, 1, 1, 1, 1], [0, 0, 0, 0, 1, 1, 1, -1], [0, 0, 0, 0, 1, 1, -1, 1], [0, 0, 0, 0, 1, 1, -1, -1], [0, 0, -1, 1, 1, 1, 0, 0], [0, 0, -1, -1, 1, 1, 0, 0], [0, 0, 1, 1, 1, -1, 0, 0], [0, 0, 1, -1, 1, -1, 0, 0], [0, 0, 0, 0, 1, -1, 1, 1], [0, 0, 0, 0, 1, -1, 1, -1], [0, 0, 0, 0, 1, -1, -1, 1], [0, 0, 0, 0, 1, -1, -1, -1], [0, 0, -1, 1, 1, -1, 0, 0], [0, 0, -1, -1, 1, -1, 0, 0], [0, -1, 1, 0, 1, 0, 0, 1], [0, -1, 1, 0, 1, 0, 0, -1], [0, -1, 0, 1, 1, 0, 1, 0], [0, -1, 0, -1, 1, 0, 1, 0], [0, -1, 0, 1, 1, 0, -1, 0], [0, -1, 0, -1, 1, 0, -1, 0], [0, -1, -1, 0, 1, 0, 0, 1], [0, -1, -1, 0, 1, 0, 0, -1]], "L": [[1.0, 0.0, 1.0, 0.0, 0.0, 0.0, 0.0, 0.0], [1.0, 0.0, -1.0, 0.0, 0.0, 0.0, 0.0, 0.0], [1.0, 0.0, 0.0, 1.0, 0.0, 0.0, 0.0, 0.0], [1.0, 0.0, 0.0, -1.0, 0.0, 0.0, 0.0, 0.0], [1.0, 0.0, 0.0, 0.0, 1.0, 0.0, 0.0, 0.0], [1.0, 0.0, 0.0, 0.0, -1.0, 0.0, 0.0, 0.0], [1.0, 0.0, 0.0, 0.0, 0.0, 1.0, 0.0, 0.0], [1.0, 0.0, 0.0, 0.0, 0.0, -1.0, 0.0, 0.0], [1.0, 0.0, 0.0, 0.0, 0.0, 0.0, 1.0, 0.0], [1.0, 0.0, 0.0, 0.0, 0.0, 0.0, -1.0, 0.0], [1.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 1.0], [1.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, -1.0], [0.0, 1.0, 1.0, 0.0, 0.0, 0.0, 0.0, 0.0], [0.0, 1.0, -1.0, 0.0, 0.0, 0.0, 0.0, 0.0], [0.0, 1.0, 0.0, 1.0, 0.0, 0.0, 0.0, 0.0], [0.0, 1.0, 0.0, -1.0, 0.0, 0.0, 0.0, 0.0], [0.0, 1.0, 0.0, 0.0, 1.0, 0.0, 0.0, 0.0], [0.0, 1.0, 0.0, 0.0, -1.0, 0.0, 0.0, 0.0], [0.0, 1.0, 0.0, 0.0, 0.0, 1.0, 0.0, 0.0], [0.0, 1.0, 0.0, 0.0, 0.0, -1.0, 0.0, 0.0], [0.0, 1.0, 0.0, 0.0, 0.0, 0.0, 1.0, 0.0], [0.0, 1.0, 0.0, 0.0, 0.0, 0.0, -1.0, 0.0], [0.0, 1.0, 0.0, 0.0, 0.0, 0.0, 0.0, 1.0], [0.0, 1.0, 0.0, 0.0, 0.0, 0.0, 0.0, -1.0], [0.0, 0.0, 1.0, 0.0, 1.0, 0.0, 0.0, 0.0], [0.0, 0.0, 1.0, 0.0, -1.0, 0.0, 0.0, 0.0], [0.0, 0.0, 1.0, 0.0, 0.0, 1.0, 0.0, 0.0], [0.0, 0.0, 1.0, 0.0, 0.0, -1.0, 0.0, 0.0], [0.0, 0.0, 1.0, 0.0, 0.0, 0.0, 1.0, 0.0], [0.0, 0.0, 1.0, 0.0, 0.0, 0.0, -1.0, 0.0], [0.0, 0.0, 1.0, 0.0, 0.0, 0.0, 0.0, 1.0], [0.0, 0.0, 1.0, 0.0, 0.0, 0.0, 0.0, -1.0], [0.0, 0.0, 0.0, 1.0, 1.0, 0.0, 0.0, 0.0], [0.0, 0.0, 0.0, 1.0, -1.0, 0.0, 0.0, 0.0], [0.0, 0.0, 0.0, 1.0, 0.0, 1.0, 0.0, 0.0], [0.0, 0.0, 0.0, 1.0, 0.0, -1.0, 0.0, 0.0], [0.0, 0.0, 0.0, 1.0, 0.0, 0.0, 1.0, 0.0], [0.0, 0.0, 0.0, 1.0, 0.0, 0.0, -1.0, 0.0], [0.0, 0.0, 0.0, 1.0, 0.0, 0.0, 0.0, 1.0], [0.0, 0.0, 0.0, 1.0, 0.0, 0.0, 0.0, -1.0], [0.0, 0.0, 0.0, 0.0, 1.0, 0.0, 1.0, 0.0], [0.0, 0.0, 0.0, 0.0, 1.0, 0.0, -1.0, 0.0], [0.0, 0.0, 0.0, 0.0, 1.0, 0.0, 0.0, 1.0], [0.0, 0.0, 0.0, 0.0, 1.0, 0.0, 0.0, -1.0], [0.0, 0.0, 0.0, 0.0, 0.0, 1.0, 1.0, 0.0], [0.0, 0.0, 0.0, 0.0, 0.0, 1.0, -1.0, 0.0], [0.0, 0.0, 0.0, 0.0, 0.0, 1.0, 0.0, 1.0], [0.0, 0.0, 0.0, 0.0, 0.0, 1.0, 0.0, -1.0], [0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5], [0.5, 0.5, 0.5, 0.5, 0.5, 0.5, -0.5, -0.5], [0.5, 0.5, 0.5, 0.5, 0.5, -0.5, 0.5, -0.5], [0.5, 0.5, 0.5, 0.5, 0.5, -0.5, -0.5, 0.5], [0.5, 0.5, 0.5, 0.5, -0.5, 0.5, 0.5, -0.5], [0.5, 0.5, 0.5, 0.5, -0.5, 0.5, -0.5, 0.5], [0.5, 0.5, 0.5, 0.5, -0.5, -0.5, 0.5, 0.5], [0.5, 0.5, 0.5, 0.5, -0.5, -0.5, -0.5, -0.5], [0.5, 0.5, 0.5, -0.5, 0.5, 0.5, 0.5, -0.5], [0.5, 0.5, 0.5, -0.5, 0.5, 0.5, -0.5, 0.5], [0.5, 0.5, 0.5, -0.5, 0.5, -0.5, 0.5, 0.5], [0.5, 0.5, 0.5, -0.5, 0.5, -0.5, -0.5, -0.5], [0.5, 0.5, 0.5, -0.5, -0.5, 0.5, 0.5, 0.5], [0.5, 0.5, 0.5, -0.5, -0.5, 0.5, -0.5, -0.5], [0.5, 0.5, 0.5, -0.5, -0.5, -0.5, 0.5, -0.5], [0.5, 0.5, 0.5, -0.5, -0.5, -0.5, -0.5, 0.5], [0.5, 0.5, -0.5, 0.5, 0.5, 0.5, 0.5, -0.5], [0.5, 0.5, -0.5, 0.5, 0.5, 0.5, -0.5, 0.5], [0.5, 0.5, -0.5, 0.5, 0.5, -0.5, 0.5, 0.5], [0.5, 0.5, -0.5, 0.5, 0.5, -0.5, -0.5, -0.5], [0.5, 0.5, -0.5, 0.5, -0.5, 0.5, 0.5, 0.5], [0.5, 0.5, -0.5, 0.5, -0.5, 0.5, -0.5, -0.5], [0.5, 0.5, -0.5, 0.5, -0.5, -0.5, 0.5, -0.5], [0.5, 0.5, -0.5, 0.5, -0.5, -0.5, -0.5, 0.5], [0.5, 0.5, -0.5, -0.5, 0.5, 0.5, 0.5, 0.5], [0.5, 0.5, -0.5, -0.5, 0.5, 0.5, -0.5, -0.5], [0.5, 0.5, -0.5, -0.5, 0.5, -0.5, 0.5, -0.5], [0.5, 0.5, -0.5, -0.5, 0.5, -0.5, -0.5, 0.5], [0.5, 0.5, -0.5, -0.5, -0.5, 0.5, 0.5, -0.5], [0.5, 0.5, -0.5, -0.5, -0.5, 0.5, -0.5, 0.5], [0.5, 0.5, -0.5, -0.5, -0.5, -0.5, 0.5, 0.5], [0.5, 0.5, -0.5, -0.5, -0.5, -0.5, -0.5, -0.5], [0.5, -0.5, 0.5, 0.5, 0.5, 0.5, 0.5, -0.5], [0.5, -0.5, 0.5, 0.5, 0.5, 0.5, -0.5, 0.5], [0.5, -0.5, 0.5, 0.5, 0.5, -0.5, 0.5, 0.5], [0.5, -0.5, 0.5, 0.5, 0.5, -0.5, -0.5, -0.5], [0.5, -0.5, 0.5, 0.5, -0.5, 0.5, 0.5, 0.5], [0.5, -0.5, 0.5, 0.5, -0.5, 0.5, -0.5, -0.5], [0.5, -0.5, 0.5, 0.5, -0.5, -0.5, 0.5, -0.5], [0.5, -0.5, 0.5, 0.5, -0.5, -0.5, -0.5, 0.5], [0.5, -0.5, 0.5, -0.5, 0.5, 0.5, 0.5, 0.5], [0.5, -0.5, 0.5, -0.5, 0.5, 0.5, -0.5, -0.5], [0.5, -0.5, 0.5, -0.5, 0.5, -0.5, 0.5, -0.5], [0.5, -0.5, 0.5, -0.5, 0.5, -0.5, -0.5, 0.5], [0.5, -0.5, 0.5, -0.5, -0.5, 0.5, 0.5, -0.5], [0.5, -0.5, 0.5, -0.5, -0.5, 0.5, -0.5, 0.5], [0.5, -0.5, 0.5, -0.5, -0.5, -0.5, 0.5, 0.5], [0.5, -0.5, 0.5, -0.5, -0.5, -0.5, -0.5, -0.5], [0.5, -0.5, -0.5, 0.5, 0.5, 0.5, 0.5, 0.5], [0.5, -0.5, -0.5, 0.5, 0.5, 0.5, -0.5, -0.5], [0.5, -0.5, -0.5, 0.5, 0.5, -0.5, 0.5, -0.5], [0.5, -0.5, -0.5, 0.5, 0.5, -0.5, -0.5, 0.5], [0.5, -0.5, -0.5, 0.5, -0.5, 0.5, 0.5, -0.5], [0.5, -0.5, -0.5, 0.5, -0.5, 0.5, -0.5, 0.5], [0.5, -0.5, -0.5, 0.5, -0.5, -0.5, 0.5, 0.5], [0.5, -0.5, -0.5, 0.5, -0.5, -0.5, -0.5, -0.5], [0.5, -0.5, -0.5, -0.5, 0.5, 0.5, 0.5, -0.5], [0.5, -0.5, -0.5, -0.5, 0.5, 0.5, -0.5, 0.5], [0.5, -0.5, -0.5, -0.5, 0.5, -0.5, 0.5, 0.5], [0.5, -0.5, -0.5, -0.5, 0.5, -0.5, -0.5, -0.5], [0.5, -0.5, -0.5, -0.5, -0.5, 0.5, 0.5, 0.5], [0.5, -0.5, -0.5, -0.5, -0.5, 0.5, -0.5, -0.5], [0.5, -0.5, -0.5, -0.5, -0.5, -0.5, 0.5, -0.5], [0.5, -0.5, -0.5, -0.5, -0.5, -0.5, -0.5, 0.5]], "F0": [[1.0, 1.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0], [0.0, 0.0, 1.0, 1.0, 0.0, 0.0, 0.0, 0.0], [0.0, 0.0, 0.0, 0.0, 1.0, 1.0, 0.0, 0.0], [0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 1.0, 1.0], [1.0, -1.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0], [0.0, 0.0, 1.0, -1.0, 0.0, 0.0, 0.0, 0.0], [0.0, 0.0, 0.0, 0.0, 1.0, -1.0, 0.0, 0.0], [0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 1.0, -1.0]], "E8": [[1.0, 1.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0], [1.0, -1.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0], [1.0, 0.0, 1.0, 0.0, 0.0, 0.0, 0.0, 0.0], [1.0, 0.0, -1.0, 0.0, 0.0, 0.0, 0.0, 0.0], [1.0, 0.0, 0.0, 1.0, 0.0, 0.0, 0.0, 0.0], [1.0, 0.0, 0.0, -1.0, 0.0, 0.0, 0.0, 0.0], [1.0, 0.0, 0.0, 0.0, 1.0, 0.0, 0.0, 0.0], [1.0, 0.0, 0.0, 0.0, -1.0, 0.0, 0.0, 0.0], [1.0, 0.0, 0.0, 0.0, 0.0, 1.0, 0.0, 0.0], [1.0, 0.0, 0.0, 0.0, 0.0, -1.0, 0.0, 0.0], [1.0, 0.0, 0.0, 0.0, 0.0, 0.0, 1.0, 0.0], [1.0, 0.0, 0.0, 0.0, 0.0, 0.0, -1.0, 0.0], [1.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 1.0], [1.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, -1.0], [0.0, 1.0, 1.0, 0.0, 0.0, 0.0, 0.0, 0.0], [0.0, 1.0, -1.0, 0.0, 0.0, 0.0, 0.0, 0.0], [0.0, 1.0, 0.0, 1.0, 0.0, 0.0, 0.0, 0.0], [0.0, 1.0, 0.0, -1.0, 0.0, 0.0, 0.0, 0.0], [0.0, 1.0, 0.0, 0.0, 1.0, 0.0, 0.0, 0.0], [0.0, 1.0, 0.0, 0.0, -1.0, 0.0, 0.0, 0.0], [0.0, 1.0, 0.0, 0.0, 0.0, 1.0, 0.0, 0.0], [0.0, 1.0, 0.0, 0.0, 0.0, -1.0, 0.0, 0.0], [0.0, 1.0, 0.0, 0.0, 0.0, 0.0, 1.0, 0.0], [0.0, 1.0, 0.0, 0.0, 0.0, 0.0, -1.0, 0.0], [0.0, 1.0, 0.0, 0.0, 0.0, 0.0, 0.0, 1.0], [0.0, 1.0, 0.0, 0.0, 0.0, 0.0, 0.0, -1.0], [0.0, 0.0, 1.0, 1.0, 0.0, 0.0, 0.0, 0.0], [0.0, 0.0, 1.0, -1.0, 0.0, 0.0, 0.0, 0.0], [0.0, 0.0, 1.0, 0.0, 1.0, 0.0, 0.0, 0.0], [0.0, 0.0, 1.0, 0.0, -1.0, 0.0, 0.0, 0.0], [0.0, 0.0, 1.0, 0.0, 0.0, 1.0, 0.0, 0.0], [0.0, 0.0, 1.0, 0.0, 0.0, -1.0, 0.0, 0.0], [0.0, 0.0, 1.0, 0.0, 0.0, 0.0, 1.0, 0.0], [0.0, 0.0, 1.0, 0.0, 0.0, 0.0, -1.0, 0.0], [0.0, 0.0, 1.0, 0.0, 0.0, 0.0, 0.0, 1.0], [0.0, 0.0, 1.0, 0.0, 0.0, 0.0, 0.0, -1.0], [0.0, 0.0, 0.0, 1.0, 1.0, 0.0, 0.0, 0.0], [0.0, 0.0, 0.0, 1.0, -1.0, 0.0, 0.0, 0.0], [0.0, 0.0, 0.0, 1.0, 0.0, 1.0, 0.0, 0.0], [0.0, 0.0, 0.0, 1.0, 0.0, -1.0, 0.0, 0.0], [0.0, 0.0, 0.0, 1.0, 0.0, 0.0, 1.0, 0.0], [0.0, 0.0, 0.0, 1.0, 0.0, 0.0, -1.0, 0.0], [0.0, 0.0, 0.0, 1.0, 0.0, 0.0, 0.0, 1.0], [0.0, 0.0, 0.0, 1.0, 0.0, 0.0, 0.0, -1.0], [0.0, 0.0, 0.0, 0.0, 1.0, 1.0, 0.0, 0.0], [0.0, 0.0, 0.0, 0.0, 1.0, -1.0, 0.0, 0.0], [0.0, 0.0, 0.0, 0.0, 1.0, 0.0, 1.0, 0.0], [0.0, 0.0, 0.0, 0.0, 1.0, 0.0, -1.0, 0.0], [0.0, 0.0, 0.0, 0.0, 1.0, 0.0, 0.0, 1.0], [0.0, 0.0, 0.0, 0.0, 1.0, 0.0, 0.0, -1.0], [0.0, 0.0, 0.0, 0.0, 0.0, 1.0, 1.0, 0.0], [0.0, 0.0, 0.0, 0.0, 0.0, 1.0, -1.0, 0.0], [0.0, 0.0, 0.0, 0.0, 0.0, 1.0, 0.0, 1.0], [0.0, 0.0, 0.0, 0.0, 0.0, 1.0, 0.0, -1.0], [0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 1.0, 1.0], [0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 1.0, -1.0], [0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5, 0.5], [0.5, 0.5, 0.5, 0.5, 0.5, 0.5, -0.5, -0.5], [0.5, 0.5, 0.5, 0.5, 0.5, -0.5, 0.5, -0.5], [0.5, 0.5, 0.5, 0.5, 0.5, -0.5, -0.5, 0.5], [0.5, 0.5, 0.5, 0.5, -0.5, 0.5, 0.5, -0.5], [0.5, 0.5, 0.5, 0.5, -0.5, 0.5, -0.5, 0.5], [0.5, 0.5, 0.5, 0.5, -0.5, -0.5, 0.5, 0.5], [0.5, 0.5, 0.5, 0.5, -0.5, -0.5, -0.5, -0.5], [0.5, 0.5, 0.5, -0.5, 0.5, 0.5, 0.5, -0.5], [0.5, 0.5, 0.5, -0.5, 0.5, 0.5, -0.5, 0.5], [0.5, 0.5, 0.5, -0.5, 0.5, -0.5, 0.5, 0.5], [0.5, 0.5, 0.5, -0.5, 0.5, -0.5, -0.5, -0.5], [0.5, 0.5, 0.5, -0.5, -0.5, 0.5, 0.5, 0.5], [0.5, 0.5, 0.5, -0.5, -0.5, 0.5, -0.5, -0.5], [0.5, 0.5, 0.5, -0.5, -0.5, -0.5, 0.5, -0.5], [0.5, 0.5, 0.5, -0.5, -0.5, -0.5, -0.5, 0.5], [0.5, 0.5, -0.5, 0.5, 0.5, 0.5, 0.5, -0.5], [0.5, 0.5, -0.5, 0.5, 0.5, 0.5, -0.5, 0.5], [0.5, 0.5, -0.5, 0.5, 0.5, -0.5, 0.5, 0.5], [0.5, 0.5, -0.5, 0.5, 0.5, -0.5, -0.5, -0.5], [0.5, 0.5, -0.5, 0.5, -0.5, 0.5, 0.5, 0.5], [0.5, 0.5, -0.5, 0.5, -0.5, 0.5, -0.5, -0.5], [0.5, 0.5, -0.5, 0.5, -0.5, -0.5, 0.5, -0.5], [0.5, 0.5, -0.5, 0.5, -0.5, -0.5, -0.5, 0.5], [0.5, 0.5, -0.5, -0.5, 0.5, 0.5, 0.5, 0.5], [0.5, 0.5, -0.5, -0.5, 0.5, 0.5, -0.5, -0.5], [0.5, 0.5, -0.5, -0.5, 0.5, -0.5, 0.5, -0.5], [0.5, 0.5, -0.5, -0.5, 0.5, -0.5, -0.5, 0.5], [0.5, 0.5, -0.5, -0.5, -0.5, 0.5, 0.5, -0.5], [0.5, 0.5, -0.5, -0.5, -0.5, 0.5, -0.5, 0.5], [0.5, 0.5, -0.5, -0.5, -0.5, -0.5, 0.5, 0.5], [0.5, 0.5, -0.5, -0.5, -0.5, -0.5, -0.5, -0.5], [0.5, -0.5, 0.5, 0.5, 0.5, 0.5, 0.5, -0.5], [0.5, -0.5, 0.5, 0.5, 0.5, 0.5, -0.5, 0.5], [0.5, -0.5, 0.5, 0.5, 0.5, -0.5, 0.5, 0.5], [0.5, -0.5, 0.5, 0.5, 0.5, -0.5, -0.5, -0.5], [0.5, -0.5, 0.5, 0.5, -0.5, 0.5, 0.5, 0.5], [0.5, -0.5, 0.5, 0.5, -0.5, 0.5, -0.5, -0.5], [0.5, -0.5, 0.5, 0.5, -0.5, -0.5, 0.5, -0.5], [0.5, -0.5, 0.5, 0.5, -0.5, -0.5, -0.5, 0.5], [0.5, -0.5, 0.5, -0.5, 0.5, 0.5, 0.5, 0.5], [0.5, -0.5, 0.5, -0.5, 0.5, 0.5, -0.5, -0.5], [0.5, -0.5, 0.5, -0.5, 0.5, -0.5, 0.5, -0.5], [0.5, -0.5, 0.5, -0.5, 0.5, -0.5, -0.5, 0.5], [0.5, -0.5, 0.5, -0.5, -0.5, 0.5, 0.5, -0.5], [0.5, -0.5, 0.5, -0.5, -0.5, 0.5, -0.5, 0.5], [0.5, -0.5, 0.5, -0.5, -0.5, -0.5, 0.5, 0.5], [0.5, -0.5, 0.5, -0.5, -0.5, -0.5, -0.5, -0.5], [0.5, -0.5, -0.5, 0.5, 0.5, 0.5, 0.5, 0.5], [0.5, -0.5, -0.5, 0.5, 0.5, 0.5, -0.5, -0.5], [0.5, -0.5, -0.5, 0.5, 0.5, -0.5, 0.5, -0.5], [0.5, -0.5, -0.5, 0.5, 0.5, -0.5, -0.5, 0.5], [0.5, -0.5, -0.5, 0.5, -0.5, 0.5, 0.5, -0.5], [0.5, -0.5, -0.5, 0.5, -0.5, 0.5, -0.5, 0.5], [0.5, -0.5, -0.5, 0.5, -0.5, -0.5, 0.5, 0.5], [0.5, -0.5, -0.5, 0.5, -0.5, -0.5, -0.5, -0.5], [0.5, -0.5, -0.5, -0.5, 0.5, 0.5, 0.5, -0.5], [0.5, -0.5, -0.5, -0.5, 0.5, 0.5, -0.5, 0.5], [0.5, -0.5, -0.5, -0.5, 0.5, -0.5, 0.5, 0.5], [0.5, -0.5, -0.5, -0.5, 0.5, -0.5, -0.5, -0.5], [0.5, -0.5, -0.5, -0.5, -0.5, 0.5, 0.5, 0.5], [0.5, -0.5, -0.5, -0.5, -0.5, 0.5, -0.5, -0.5], [0.5, -0.5, -0.5, -0.5, -0.5, -0.5, 0.5, -0.5], [0.5, -0.5, -0.5, -0.5, -0.5, -0.5, -0.5, 0.5]]} \ No newline at end of file diff --git a/research/two-sided-ten-term-floor/requirements.txt b/research/two-sided-ten-term-floor/requirements.txt new file mode 100644 index 0000000000..157e508b6b --- /dev/null +++ b/research/two-sided-ten-term-floor/requirements.txt @@ -0,0 +1,3 @@ +numpy +sympy +networkx diff --git a/research/two-sided-ten-term-floor/verify.sh b/research/two-sided-ten-term-floor/verify.sh new file mode 100644 index 0000000000..6cf3001804 --- /dev/null +++ b/research/two-sided-ten-term-floor/verify.sh @@ -0,0 +1,58 @@ +#!/usr/bin/env bash +# Verification of research/two-sided-ten-term-floor (no kappa claim). usage: bash verify.sh [/fresh/output/dir] +# Needs Python >= 3.10 with numpy, sympy, networkx (PYTHON=/path/to/python to choose). No SAT solver. About 18 minutes wall, at most 4 processes, each command under timeout 1200, niced. +# 0 MANIFEST.sha256 +# 1 four streams: clique.py (+ witness16, diag9) | caseb4.py chunks 0, 1, 2 of 3 +# 2 four streams: clique2.py 5 on the 93 sets I^c (|I^c| <= 3), four chunks +# 3 four streams: clique2.py 4 + d4A + d4A2 + d4A3 | verify_cl (2 representatives) x2 | sym + stab +# 4 check_logs.py: every number of the README as a PASS/FAIL line +set -uo pipefail +JOBS=${JOBS:-4} +HERE=$(cd "$(dirname "$0")" && pwd) +OUT=${1:-$(mktemp -d "${TMPDIR:-/tmp}/two-sided-floor.XXXXXX")} +mkdir -p "$OUT"; OUT=$(cd "$OUT" && pwd) +case "$OUT/" in "$HERE"/*) echo "output dir must be outside the package"; exit 2;; esac +PY="${PYTHON:-python3}"; export PYTHONDONTWRITEBYTECODE=1 OMP_NUM_THREADS=1 VECLIB_MAXIMUM_THREADS=1 OPENBLAS_NUM_THREADS=1 +TMO=""; command -v timeout >/dev/null 2>&1 && TMO="timeout 1200"; command -v gtimeout >/dev/null 2>&1 && TMO="gtimeout 1200" +W="$OUT/work"; LOG="$OUT/logs"; mkdir -p "$W" "$LOG"; : > "$OUT/all.out"; : > "$OUT/times.out"; T0=$SECONDS +echo "== 0. manifest" +"$PY" -B "$HERE/checks/manifest_check.py" | tee -a "$OUT/all.out" | sed 's/^/ /'; grep -q '^FAIL' "$OUT/all.out" && { echo "step 0 FAILED"; exit 1; } +cp "$HERE"/checks/*.py "$HERE"/data/data.json "$W"/ +cd "$W" +run() { local n=$1; shift; local s=$SECONDS; $TMO nice -n 10 "$@" > "$LOG/$n.log" 2>&1; local rc=$?; echo "ran $n rc=$rc in $((SECONDS - s))s" >> "$OUT/times.out"; return 0; } +# the 93 sets I^c with |I^c| <= 3, as "a,b,c;..." strings, dealt into four chunks +"$PY" -B - <<'PYE' +import itertools +sets = [c for k in range(4) for c in itertools.combinations(range(8), k)] +for j in range(4): + open('ics_%d.txt' % j, 'w').write(';'.join(','.join(map(str, c)) for i, c in enumerate(sets) if i % 4 == j)) +PYE +echo "== 1. computations, phase 1 (four streams)" +( run clique "$PY" -B clique.py; run w16 "$PY" -B witness16.py; run d9 "$PY" -B diag9.py ) & P1=$! +( run cb4_0 "$PY" -B caseb4.py 0 3 ) & P2=$! +[ "$JOBS" -le 2 ] && { wait $P1; wait $P2; } +( run cb4_1 "$PY" -B caseb4.py 1 3 ) & P3=$! +( run cb4_2 "$PY" -B caseb4.py 2 3 ) & P4=$! +wait $P1; wait $P2; wait $P3; wait $P4 +echo "== 1. computations, phase 2 (four streams)" +( run c2_0 "$PY" -B clique2.py 5 "$(cat ics_0.txt)" ) & P1=$! +( run c2_1 "$PY" -B clique2.py 5 "$(cat ics_1.txt)" ) & P2=$! +[ "$JOBS" -le 2 ] && { wait $P1; wait $P2; } +( run c2_2 "$PY" -B clique2.py 5 "$(cat ics_2.txt)" ) & P3=$! +( run c2_3 "$PY" -B clique2.py 5 "$(cat ics_3.txt)" ) & P4=$! +wait $P1; wait $P2; wait $P3; wait $P4 +echo "== 1. computations, phase 3 (four streams)" +( run c24 "$PY" -B clique2.py 4 "0,1,2,4"; run d4A "$PY" -B d4A.py found_0_1_2_4.pkl; run d4A2 "$PY" -B d4A2.py; run d4A3 "$PY" -B d4A3.py ) & P1=$! +( run vcl_none "$PY" -B verify_cl.py ""; run vcl_0_1_2 "$PY" -B verify_cl.py "0,1,2" ) & P2=$! +[ "$JOBS" -le 2 ] && { wait $P1; wait $P2; } +( run vcl_0 "$PY" -B verify_cl.py "0"; run vcl_0_1 "$PY" -B verify_cl.py "0,1" ) & P3=$! +( run sym "$PY" -B sym.py; run stab "$PY" -B stab.py ) & P4=$! +wait $P1; wait $P2; wait $P3; wait $P4 +sed 's/^/ /' "$OUT/times.out" +grep -v 'rc=0 ' "$OUT/times.out" | sed 's/^/FAIL nonzero exit: /' | tee -a "$OUT/all.out" +echo "== 4. assertions (check_logs.py)" +"$PY" -B "$HERE/checks/check_logs.py" "$LOG" | tee -a "$OUT/all.out" | sed 's/^/ /' +npass=$(grep -c '^PASS' "$OUT/all.out"); nfail=$(grep -c '^FAIL' "$OUT/all.out") +echo "== done in $((SECONDS - T0))s: $npass PASS, $nfail FAIL; logs in $OUT" +[ "$nfail" = 0 ] && { echo "PASS: all assertions hold"; exit 0; } +echo "FAIL"; exit 1