diff --git a/research/p104-port-window-nine/LICENSE b/research/p104-port-window-nine/LICENSE new file mode 100644 index 0000000000..261eeb9e9f --- /dev/null +++ b/research/p104-port-window-nine/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/p104-port-window-nine/NOTICE b/research/p104-port-window-nine/NOTICE new file mode 100644 index 0000000000..0ade81c2a7 --- /dev/null +++ b/research/p104-port-window-nine/NOTICE @@ -0,0 +1,4 @@ +The port window of P104 is 9 in characteristic 2: statements, proofs and checks (no new kappa). +Prepared by DreamingOfClouds with Claude Opus 5.5 (Anthropic), via Claude Code. Apache-2.0. + +check.py reads only files inside this package (data/). Standard library only. data/ports_p104.json and data/witness14.json are vendored byte for byte from research/p104-port-window-haemers. The solver results in data/sat_rows.json come from kissat 4.0.4 runs that the checks do not repeat; no DRAT proofs were produced for them. diff --git a/research/p104-port-window-nine/README.md b/research/p104-port-window-nine/README.md new file mode 100644 index 0000000000..fe8a34ce38 --- /dev/null +++ b/research/p104-port-window-nine/README.md @@ -0,0 +1,37 @@ +# The port window of P104 is 9 in characteristic 2 (no kappa) + +**No new kappa.** No word is built and nothing is priced. This package proves that every block-mask pattern on the ports of P104 has rank at least 9k over every field, so the window w(P104;F) is at least 9 for every field and exactly 9 in characteristic 2. Statements and proofs are in `THEOREM.md`. + +Tags (as in `THEOREM.md`): **[C]** exact computation reproduced by `check.py` (one PASS line per claim); **[P]** hand proof; **[P+C]** a proof whose inequalities `check.py` also evaluates on explicit representations; **[R]** a solver run recorded in `data/sat_rows.json`, not repeated by the checks; **[Q]** quoted from another source. + +## Setting + +Ports, odd graph, k-block patterns and the window w = inf_k rank/k are those of `research/p104-port-window-haemers` (#6933): ports are vectors of F_2^9, orthogonal pairs get zero k x k blocks, diagonal blocks are invertible. P104 is the port set in `data/ports_p104.json`; P120 is the 120 vectors of weight 3 mod 4; P112 is P104 plus one of the two odd 8-cliques that P120 deletes. + +## Results + +1. **Edge inequality (E') [P+C].** The proof of #6933 Theorem 3 has a double count: the part of the block X_TT that is not new already lies inside the column space of gamma_T(c) (its Step 2 containment). Using the containment itself gives k <= g_T(c) + g_T(d) + min(Y_c, Y_d) for every edge port. +2. **Theorem 3' [P+C].** If the edge ports of an orthogonal 8-set can be charged so that every non-isolated vertex gets charge at least 2 (for instance minimum degree at least 4 with weights 1/2), every k-block pattern of rank 8k + j has j >= k, over every field. +3. **Values [P+C].** Every orthogonal 8-set of P104 has minimum degree 5 (P112: 6, P120: 7), so rank >= 9k for every k and every field. **w(P104;F) >= 9 for every field; w = 9 in characteristic 2** (Gram matrix). P112 and P120 are recovered without weights. With #7014 (13 disjoint 8-cliques, rank 13 over every field) and #6933 Theorem 4: **w(P104) is 9 in characteristic 2 and 13 otherwise** (P112: 9 and 14; P120: 9 and 15) [Q]. +4. **Second proof [P+C].** A star inequality (LR) proves j >= k for minimum degree at least 4 by a radical dimension count. +5. **Corollaries [P+C].** H_f(G_{K_n}) = n+1 for n >= 5 over every field; H_f(Petersen;F) >= 9/2 over every field (**not checked against the literature**). +6. **Field-only dependence [P+C].** w(V;F) depends only on the characteristic of F. +7. **Solver rows [R].** F_2 instances inside P104 (Petersen k = 2 and 4; G_{K_5} k = 3) agree with the theorem, with same-size controls; no DRAT proofs. A k = 6 rank-53 run on 30 ports was undecided at 20 minutes and is not used. + +## Scope and what is not claimed + +No bound on kappa and no word. The window is defined by the uniform whole-block mask; sub-block masks, port-dependent block sizes and nonlinear labels are different models and are not covered. Whether a physical construction realises a k-block window with exactly this mask for k > 1 is not derived. No human has reviewed the proofs: two model sessions proved the result by different routes and a third read the first proof line by line (`THEOREM.md`, section 12). + +## Exact checks + +`python3.12 -I -B research/p104-port-window-nine/check.py` (about 6 s); it prints one PASS line per claim and ends with `PASS_P104_PORT_WINDOW_NINE`. Standard library only. The checks include planted violations that must be flagged. The solver rows are recorded, not repeated. + +## Open next questions + +1. Is there a pattern on P104 below ratio 9 in a model other than the uniform whole-block mask (port-dependent block sizes, sub-block masks)? +2. What is H_f(Petersen;F) between 9/2 and 5, and is 9/2 known or refuted in the literature? +3. Can the recorded UNSAT rows be certified with DRAT proofs, and can the k = 6 rank-53 run on 30 ports be decided? + +The structured form with first steps and blockers is in `TASK.json`. + +Prepared by DreamingOfClouds with Claude Opus 5.5 (Anthropic), via Claude Code. diff --git a/research/p104-port-window-nine/SOURCES.json b/research/p104-port-window-nine/SOURCES.json new file mode 100644 index 0000000000..92230e318c --- /dev/null +++ b/research/p104-port-window-nine/SOURCES.json @@ -0,0 +1,12 @@ +{ + "schema_version": 1, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "files": [ + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + } + ] +} \ No newline at end of file diff --git a/research/p104-port-window-nine/TASK.json b/research/p104-port-window-nine/TASK.json new file mode 100644 index 0000000000..af3a41fef1 --- /dev/null +++ b/research/p104-port-window-nine/TASK.json @@ -0,0 +1,138 @@ +{ + "schema_version": 1, + "task_id": "p104-side-correction", + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "original_card": { + "id": "p104-side-correction", + "question": "Can joint helper bases and a legal causal split improve the complete P104 productive/paid invoice?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "research/p104-helper-subspace-splits/README.md", + "research/dyadic-helper-channel-capacity/README.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "An exact arbitrary-input identity, source/target frame availability and restoration at the chosen cut, plus the complete channel+correction+idle/hosting bill or an explicit favorable bound. The native channel alone is not a supplier. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Start with the selected #5599 emitted word and review pending #5718 distinct input/output bases plus #5717/#5719 coverage before claiming work. Pick one uncovered source word, helper group and cut region. Prove the arbitrary-input relation and legal entry/exit corrections, then compare full target and paid profiles. Reject if completion, owned lifetimes or consumer costs repay the gain. A static pairing rank alone is not a physical split.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "P104", + "helper basis", + "helper split", + "5718", + "dyadic capacity" + ], + "existing_checks": [ + { + "scope": "PR #4133: literal-slot defect", + "evidence": "research/p104-literal-slot-defect/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "88666f1dee93fbd85b31fd5d6f91a219e111b5f4", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4136: uniform commutation gap", + "evidence": "research/p104-uniform-commutation-gap/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "281ce601a8be9db470de630759179c23e1dfaa88", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4140: uniform encoding gap", + "evidence": "research/p104-uniform-encoding-gap/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "de25c6525aa866962309df5d107b32d55e6e5628", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4153: source-chart shortcut exhausts its optimistic allowance", + "evidence": "research/p104-source-chart-shortcut/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "9123241fea53df77e51ffe30d9aca1625d4bf3a8", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4154: fiber-tag seam mismatch", + "evidence": "research/p104-fiber-tag-seam/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "4ffcdaee5d6255a9cea1fe53a5424435068089d0", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Proof note on the block-mask window of the P104 port set: the edge inequality (E') (the containment inside the proof of #6933 Theorem 3 used without the double count) gives Theorem 3': every k-block pattern on P104 over any field has rank >= 9k, so w(P104;F) >= 9 for every field and w = 9 exactly in characteristic 2 (P112 and P120 recovered without weights); a second proof by a star inequality; H_f(G_{K_n}) = n+1 for n >= 5 and H_f(Petersen) >= 9/2 over every field (not compared with the literature); w depends only on the characteristic; recorded F_2 solver rows (no DRAT) agree with the theorem.", + "scope_change_reason": "The card asks for a joint helper basis and a legal causal split on the complete invoice. This package builds no word and prices no supplier. It closes the interval [53/6, 9] left open by the earlier port-window note: no block-mask window below 9 exists on P104, so no fractional-window saving is available there, and it states what a window construction on P104 must respect.", + "bottleneck_link": "docs/research/research-family-status.md; the statements bound the window of the port set from below (and equal the tensor-lift value 9 in characteristic 2). They say nothing about the denominator or about kappa.", + "stop_rule": "No kappa claim and no new word. Open and stated: windows in models other than the uniform whole-block mask (sub-block masks, port-dependent block sizes, nonlinear labels); the value of H_f(Petersen) in [9/2, 5] and its literature status; DRAT-checked solver rows.", + "evidence": "README.md and THEOREM.md (statements, proofs, hypothesis ledger), check.py (exact integer and finite-field computations, standard library only) and data/ (port list, 14-port representation, recorded solver rows).", + "author": "DreamingOfClouds", + "ai_assistance": "Prepared by DreamingOfClouds with Claude Opus 5.5 (Anthropic), via Claude Code.", + "outcome": "completed", + "open_questions": [ + { + "question": "Is there a pattern on P104 below ratio 9 in a model other than the uniform whole-block mask: port-dependent block sizes k_T, or masks on sub-blocks?", + "why_it_matters": "The block-mask window is now exactly 9 in characteristic 2, so any saving from a fractional window needs a different model; the arithmetic left by (E') and (Star) is sum k_T <= sum k_c + (E - n') j for the star configuration, which only a window that prices edge ports below points could use.", + "first_step": "State a cost model that charges edge ports less than points (and derive it from the compiler), then test the star inequality with unequal block sizes on one 8-set.", + "blocked_by": "No such window is defined; the mask of the compiler on sub-blocks is not derived." + }, + { + "question": "What is H_f(Petersen; F) between 9/2 and 5, and is the lower bound 9/2 known or refuted in the literature?", + "why_it_matters": "Theorem 3' gives 9/2 over every field, above the Shannon capacity 4; a known representation of ratio below 9/2 would refute the theorem, and the exact value would show how sharp the star argument is.", + "first_step": "Search Bukh-Cox, Blasiak's thesis and index-coding papers for the fractional Haemers or broadcast rate of the Petersen graph; then decide k = 2 rank 9 over F_3 and k = 4 rank 18 over F_2 (rank 9 at k = 2 over F_2 is recorded UNSAT).", + "blocked_by": "The literature was not searched here; no DRAT-checked rows exist for the Petersen instance." + }, + { + "question": "Can the recorded UNSAT rows be certified (DRAT) and the k = 6 rank-53 run on 30 ports be decided?", + "why_it_matters": "The theorem is a proof, so the rows are only a cross-check of the encoding; certified rows would let a reader trust the encoding independently of the proof.", + "first_step": "Regenerate the Petersen k = 4 rank 17 and 5-point k = 3 rank 17 instances, solve with proof output and check the proofs.", + "blocked_by": "The k = 6 instances (about 180,000 variables) were undecided at 20 minutes, with the same-size feasible control also undecided; the encoder is not part of this package." + } + ], + "research_context": { + "sources": [ + "research/p104-port-window-haemers: setting, Theorem 1 (window = fractional Haemers bound), Theorem 3, Theorem 4, the 14-port pattern (DreamingOfClouds)", + "Pull request #7014 (unpaidmoon): partition of the odd graph on the 104 ports into 13 cliques of size 8", + "Bukh and Cox, On a fractional version of Haemers' bound (arXiv:1802.00476; IEEE Trans. Inform. Theory 65(6), 2019)", + "Haemers, On some problems of Lovasz concerning the Shannon capacity of a graph (IEEE Trans. Inform. Theory 25(2), 1979)", + "Blasiak, A graph-theoretic approach to network coding (Cornell PhD thesis, 2013), as cited by Bukh and Cox" + ], + "credit": "DreamingOfClouds; unpaidmoon for the odd-characteristic upper bound 13." + }, + "selected_frontier_changed": false +} diff --git a/research/p104-port-window-nine/THEOREM.md b/research/p104-port-window-nine/THEOREM.md new file mode 100644 index 0000000000..c4bce0fbd7 --- /dev/null +++ b/research/p104-port-window-nine/THEOREM.md @@ -0,0 +1,249 @@ +# The port window of P104 is 9 in characteristic 2 (no kappa) + +Tags: **[P]** hand proof, written out below; **[C]** exact computation reproduced by `check.py` (one PASS line per claim); **[P+C]** a proof whose inequalities `check.py` also evaluates on explicit representations; **[R]** a solver run recorded in `data/sat_rows.json`, not repeated by the checks; **[Q]** quoted from another source and not re-proved here. No kappa claim and no word are made. No human has reviewed the proofs; their status is in section 12. + +## 0. Results + +Setting, notation and the first results on the port window are those of #6933 (research/p104-port-window-haemers). Section 1 restates what is used. A *k-block pattern* on a port set V is a matrix with k x k blocks, invertible diagonal blocks and zero blocks on orthogonal pairs; the window w(V;F) is the infimum over k of rank/k. + +1. **Edge inequality (E') [P+C].** In the proof of #6933 Theorem 3 (Step 2) the part of the block X_TT that is not new already lies inside the column space of gamma_T(c). Using that containment itself, and not only its dimension, removes the term s_T from the edge inequality and gives, for every edge port T = cd, + + **(E') k <= g_T(c) + g_T(d) + min(Y_c, Y_d).** + +2. **Theorem 3' [P+C].** If weights lambda_T in [0,1] on the edge ports give every non-isolated vertex a charge Lambda_c >= 2, every k-block pattern of rank 8k + j (more generally mk + j) has **j >= k**. This needs no field property and no weights to tune: it holds whenever every non-isolated vertex of Gamma(K) has degree at least 4. +3. **P104, P112, P120 [P+C].** Every orthogonal 8-set of P104 has n' = 8 and minimum degree 5 (the three K-types are recomputed); P112 and P120 have minimum degree 6 and 7. So **rank >= 9k for every k and every field on all three systems.** Hence **w(P104;F) >= 9 for every field, and w(P104;F) = 9 exactly in characteristic 2** (the Gram matrix has rank 9). #6933 had 53/6 on P104 and 9 on P112 and P120 with weights; the weights are no longer needed. +4. **A second proof [P+C].** A star inequality (LR) found independently proves j >= k when the minimum degree is at least 4, by a radical dimension count in place of (E'). Either proof alone gives the theorem. +5. **Corollaries [P+C].** H_f(G_{K_n}) = n+1 for n >= 5 over every field, and H_f(Petersen;F) >= 9/2 over every field. The Petersen statement was **not checked against the literature**. +6. **Field-only dependence [P+C].** w(V;F) depends only on the characteristic of F. +7. **Combined values [P, Q].** With #7014 (an explicit 13-clique cover of the odd graph of P104, rank 13 over every field) and #6933 Theorem 4 (w >= 13 outside characteristic 2): **w(P104) = 9 in characteristic 2 and 13 otherwise; P112 is 9 and 14; P120 is 9 and 15.** +8. **Solver rows [R].** kissat answers on F_2 instances inside P104, recorded with same-size controls; they agree with the theorem. A k = 6, rank 53 run on 30 ports was undecided at 20 minutes and is not used. + +What this closes: the interval [53/6, 9] of #6933 for w(P104;F_2) and the question whether Theorem 3 extends to the floor 9. **No window below 9 exists in the block-mask model, so a fractional window saves nothing on P104.** What it does not close is in section 11. + +## 1. Setting + +**Ports.** P120 is the set of the 120 vectors of F_2^9 of weight 3 mod 4. P104 is the 104-port set of `data/ports_p104.json` (vendored byte for byte from #6933), a subset of P120. The 16 vectors of P120 outside P104 form two odd 8-cliques; P112 is P104 plus one of them [C]. dot(a,b) is the F_2 dot product; every port has dot(a,a) = 1 because its weight is odd. Distinct ports are **orthogonal** if dot = 0 and **adjacent** if dot = 1. G(V) is the graph on V with the adjacent pairs as edges. + +**Block patterns.** For a field F and k >= 1, a *k-block pattern* on V is a matrix B over F, rows and columns indexed by V x [k], whose k x k blocks satisfy: B_TT is invertible for every T, and B_ST = B_TS = 0 for every orthogonal pair S != T. B need not be symmetric. w_k(V;F) = min rank(B)/k and **w(V;F) = inf_k w_k(V;F)**. For any graph G the same definition (zero blocks on non-adjacent pairs) gives w(G;F). #6933 Theorem 1: w(G(V);F) is the fractional Haemers bound H_f(G(V);F) of Bukh and Cox (the block pattern with identity diagonal blocks is word for word their d-representation), and at k = 1 it is Haemers' bound H(G;F). Nothing below needs that identification except in the statements about H_f in section 8. + +**Normalisation.** Replacing each block row T of B by B_TT^{-1} times itself keeps the rank and all zero blocks. So in every proof below B_TT = I_k for all T. + +**Configurations.** Let G be a graph and F a field. A **star configuration** (K, Gamma, (T_e)) in G consists of + +- an independent set K of G of size m (for ports: m pairwise orthogonal ports), +- a simple graph Gamma on K, with E edges, degrees d_c, and n' non-isolated vertices, +- for each edge e = cd of Gamma a vertex T_e of G outside K, all distinct, such that **(C1)** T_e is adjacent to c and d and to no other vertex of K, and **(C2)** T_e and T_f are non-adjacent whenever e != f share an end. + +The T_e are called edge ports. Adjacency between edge ports with disjoint pairs is left free and never used. + +## 2. Gauge, stars, the rank lemma + +Fix a configuration, a field F and a k-block pattern B on G with B_TT = I for all T. Write rank B = mk + j. + +**Lemma 1 (gauge) [P].** j >= 0, and B = W U^T with W, U having r = mk + j columns and k rows per vertex of G (write W_T, U_T for the k x r row blocks, so B_TS = W_T U_S^T), such that, with the first mk coordinates grouped in m blocks of k (one per c in K) and the last j coordinates called x: +(a) W_c = U_c = [e-block of c, 0], i.e. the k x r matrix with I_k in block c and zeros elsewhere, for every c in K; +(b) for an edge port T = cd, W_T and U_T vanish outside the blocks c, d and x. + +*Proof.* K is independent, so the blocks B_cc' are 0 for c != c' and I_k for c = c': W_K U_K^T = I_{mk}, where W_K, U_K stack the labels of K. Hence W_K and U_K have rank mk and r = mk + j with j >= 0. (This is the first step of the proof of #6933 Theorem 3.) Take a full-rank factorisation B = W U^T with r = rank B. Choose g in GL_r with W_K g = [I_{mk} 0]; then U_K g^{-T} = [I Z] for some Z, because (W_K g)(U_K g^{-T})^T = I_{mk}. Let h = [[I,0],[Z^T,I]]; then [I 0] h = [I 0] and [I Z] h^{-T} = [I 0]. Replacing W, U by W g h and U g^{-T} h^{-T} changes neither B nor the factorisation property and gives W_K = U_K = [I_{mk} 0], which is (a). For (b): if c' in K is not an end of T, then T and c' are non-adjacent by (C1), so the mask gives 0 = B_{c'T} = W_{c'} U_T^T = U_T[c']^T (block c' of U_T) and 0 = B_{Tc'} = W_T U_{c'}^T = W_T[c'] (block c' of W_T, because U_{c'} is the identity on block c'). ∎ + +**Notation.** For an edge port T with ends c, d and S, T edge ports: alpha_T(c) = W_T[c] U_T[c]^T, X_ST = W_S[x] U_T[x]^T (k x k each), gamma_T(c) = alpha_T(c) + X_TT, g_T(c) = rank gamma_T(c). By Lemma 1(b), B_TT = alpha_T(c) + alpha_T(d) + X_TT, and B_TT = I, so + + **(1) I_k = gamma_T(c) + gamma_T(d) - X_TT.** + +**The star at c.** Let T_1, ..., T_q (q = d_c) be the edge ports at c. Put M_c = (W_S[c] U_T[c]^T) (S, T in the star), X_c = (X_ST), D_c = M_c + X_c, all qk x qk. For S != T in the star the supports of W_S and U_T meet only in block c and in x (the other ends differ because Gamma is simple), so B_ST = W_S[c]U_T[c]^T + X_ST, and this is 0 by (C2) and the mask. Hence **D_c is block diagonal** with diagonal blocks gamma_T(c), and rank D_c = sum over T at c of g_T(c) =: G_c. Moreover M_c = (stack of the W_S[c]) (stack of the U_T[c])^T factors through k dimensions, so **rank M_c <= k**, and X_c factors through the j coordinates x, so x_c := rank X_c <= j. Define + + y_c = x_c - dim(col D_c ∩ col X_c), y'_c = x_c - dim(row D_c ∩ row X_c), Y_c = (y_c + y'_c)/2. + +Then 0 <= y_c, y'_c <= x_c <= j, so 0 <= Y_c <= j. + +**Lemma 2 (rank lemma) [P].** For matrices A, B of the same shape, rank(A+B) >= rank A + rank B - dim(col A ∩ col B) - dim(row A ∩ row B). + +*Proof.* Write A = P Q, B = R S with P, R of full column rank a = rank A, b = rank B and Q, S of full row rank. Then A + B = [P R][Q; S]. The left factor has rank a + b - dim(col A ∩ col B), the right factor a + b - dim(row A ∩ row B), and Sylvester's inequality for a product through dimension a + b gives rank(A+B) >= (a+b-dc) + (a+b-dr) - (a+b). ∎ + +**Lemma 3 (Star) [P+C].** G_c <= k + x_c - y_c - y'_c <= k + j - 2 Y_c. + +*Proof.* M_c = D_c + (-X_c). Lemma 2 with A = D_c, B = -X_c: k >= rank M_c >= G_c + x_c - (x_c - y_c) - (x_c - y'_c) = G_c - x_c + y_c + y'_c. ∎ + +## 3. Containment and the edge inequality (E') + +**Lemma 4 (containment) [P+C].** Let T be an edge port with end c. There are subspaces R, R' of F^k with dim R <= y_c, dim R' <= y'_c, col X_TT ⊆ col gamma_T(c) + R and row X_TT ⊆ row gamma_T(c) + R'. + +*Proof.* Let pi_T be the projection of F^{qk} onto the T-th block of k coordinates. Write col X_c = V0 ⊕ C with V0 = col D_c ∩ col X_c; then dim C = x_c - dim V0 = y_c. The columns of X_TT are the pi_T-images of the columns of the T-th block column of X_c, so col X_TT ⊆ pi_T(col X_c) = pi_T(V0) + pi_T(C). Since D_c is block diagonal, col D_c is the direct sum of the col gamma_S(c), so pi_T(col D_c) = col gamma_T(c) and pi_T(V0) ⊆ col gamma_T(c). Put R = pi_T(C), of dimension at most y_c. The row statement is the same argument for the transposed matrices (D_c^T is block diagonal with blocks gamma^T). ∎ + +**Proposition 5 (E') [P+C].** For every edge port T = cd: + + k <= g_T(c) + g_T(d) + min(y_c, y'_c, y_d, y'_d), hence **k <= g_T(c) + g_T(d) + min(Y_c, Y_d)**. + +*Proof.* By (1), every column of I_k is a sum of columns of gamma_T(c), of gamma_T(d) and of X_TT. So F^k = col I_k ⊆ col gamma_T(c) + col gamma_T(d) + col X_TT ⊆ col gamma_T(c) + col gamma_T(d) + R by Lemma 4 (the part of col X_TT in col gamma_T(c) is absorbed). Counting dimensions, k <= g_T(c) + g_T(d) + y_c. The row version gives y'_c; the same argument with the roles of c and d exchanged gives y_d and y'_d. Finally min(y,y') <= (y+y')/2. ∎ + +The proof of #6933 Theorem 3 used only dim(col X_TT) <= g_T(c) + y_c (its (Block)) and then added the rank s_T of X_TT to g_T(c) + g_T(d) in (Edge). That counts g_T(c) twice, because the part of col X_TT that is not new is already inside col gamma_T(c). The containment lemma removes the double count. + +## 4. Theorem 3' + +**Theorem 6 (Theorem 3') [P+C].** Let (K, Gamma, (T_e)) be a star configuration in a graph G, F any field, B a k-block pattern on G of rank mk + j. Suppose lambda_T in [0,1] are given for the edge ports, and put, for each vertex c of K, Lambda_c = sum over the edge ports T at c of (lambda_T if c is the first end of T, else 1 - lambda_T), with a fixed orientation of each edge. Then + + **(a)** j / k >= (E - n') / ( n' + sum over c of (Lambda_c - 2)^+ ), and + **(b)** if Lambda_c >= 2 for every non-isolated c, then **j >= k**. In particular j >= k if every non-isolated vertex of Gamma has degree >= 4 (take lambda_T = 1/2, so Lambda_c = d_c/2 >= 2). + +*Proof.* Take min(Y_c, Y_d) <= lambda_T Y_c + (1 - lambda_T) Y_d in (E'), and sum over the E edge ports T = cd (c the first end): + + E k <= sum_c [ sum over T at c of g_T(c) + Lambda_c Y_c ]. + +Apply Lemma 3 at each of the n' vertices of positive degree (sum over T at c of g_T(c) = G_c <= k + j - 2 Y_c): + + E k <= sum_c [ k + j + (Lambda_c - 2) Y_c ] = n'(k + j) + sum_c (Lambda_c - 2) Y_c. + +Since 0 <= Y_c <= j, (Lambda_c - 2) Y_c <= (Lambda_c - 2)^+ j, which gives (a). Under the hypothesis of (b), Lambda_c - 2 >= 0 and sum_c (Lambda_c - 2) = E - 2n' (the charges add to E), so E k <= n'(k + j) + (E - 2n') j = n' k + (E - n') j, that is (E - n')(k - j) <= 0. As E > n' (the charges add to E and each is at least 2, so E >= 2n' > n'), j >= k. ∎ + +No field property, symmetry, or k = 1 argument is used. The case of (a) with Lambda_c < 2 everywhere (for example Gamma = K_4) gives j/k >= (E - n')/n'. + +## 5. Application to the port systems + +**Lemma 7 (ports relative to an orthogonal 8-set) [P+C].** Let V be any set of odd-weight vectors of F_2^9 containing an orthogonal 8-set K (pairwise dot 0). Put v = all-ones + sum of K. Then K and v form an orthonormal basis of F_2^9 (dot(v,c) = 0, dot(v,v) = 1), so every port t is the sum of the c in A(t) = {c in K : dot(t,c) = 1} plus eps v, with eps = dot(t,v), and 1 = dot(t,t) = |A(t)| + eps. Call t outside K an *edge port* if |A(t)| = 2; then eps = 1. Let Gamma(K) have a vertex for each c in K and one edge cd for each edge port with A = {c,d}. +- **(H1)** distinct edge ports have distinct pairs, because t is determined by (A, eps); so Gamma(K) is simple. +- **(H2)** two edge ports t = c + d + v and t' = c + e + v (d != e) sharing exactly one vertex are orthogonal: dot(t,t') = dot(c,c) + dot(v,v) = 1 + 1 = 0. +- An edge port is adjacent to its two K-neighbours and orthogonal to the other six points of K. + +So (K, Gamma(K), edge ports) is a star configuration in G(V): (C1) is the definition, (C2) is (H2), and K is independent in G(V). `check.py` recomputes (H1), (H2) on every orthogonal 8-set of every system as well [C]. + +**Counts [C].** The orthogonal 8-sets (there is no orthogonal 9-set): P104 1728, P112 4032 (either clique), P120 8640. K-types (E; sorted degrees): + +| system | type | number of 8-sets | minimum degree | +|---|---|---|---| +| P104 | (22; 5,5,5,5,6,6,6,6) | 960 | 5 | +| P104 | (22; 5,5,5,5,5,6,6,7) | 384 | 5 | +| P104 | (21; 5,5,5,5,5,5,6,6) | 384 | 5 | +| P112 | (25; 6,6,6,6,6,6,7,7) | 3584 | 6 | +| P112 | (24; 6^8) | 448 | 6 | +| P120 | (28; 7^8) | 8640 | 7 | + +In every case n' = 8, so lambda_T = 1/2 gives Lambda_c = d_c/2 >= 5/2 >= 2. + +**Theorem 8 [P+C].** For P104, P112 and P120, every field F and every k, every k-block pattern has rank >= 9k. *Proof.* Theorem 6(b) on any one orthogonal 8-set: rank = 8k + j >= 9k. ∎ + +## 6. The window values + +**Corollary 9 [P+C].** (i) w(P104;F) >= 9 for every field F, and w(P112;F), w(P120;F) >= 9. (ii) If char F = 2, the Gram matrix (dot(S,T)) has unit diagonal, zeros on orthogonal pairs, and rank <= 9 (a Gram matrix of vectors in a 9-dimensional space); it is a 1-block pattern on P120, hence by restriction on P112 and P104. So **w(P104;F) = w(P112;F) = w(P120;F) = 9 when char F = 2**, attained at k = 1. (iii) In particular no k-block pattern on P104 over any field has rank below 9k, for any k. The first case that #6933 left undecided, k = 6 with rank 53 < 54, is excluded. + +**Combined values [Q].** #7014 (unpaidmoon) partitions the odd graph on the 104 ports into 13 pairwise disjoint cliques of size 8; the 104 x 13 indicator matrix W has W W^T with unit diagonal and zeros on orthogonal pairs, and rank 13 over every field, so w(P104;F) <= 13 for every F; adjoining one or both of the omitted 8-cliques gives 14 and 15 for P112 and P120. #6933 Theorem 4 gives w >= 13, 14, 15 when char F != 2. Together with Corollary 9: + +| system | char F = 2 | char F != 2 | +|---|---|---| +| P104 | 9 | 13 | +| P112 | 9 | 14 | +| P120 | 9 | 15 | + +The odd-characteristic values are the lower bounds of #6933 Theorem 4 and the upper bounds of #7014, both quoted; they are not re-derived here. + +## 7. A second, independent proof: the star inequality (LR) + +This proof uses the same gauge (Lemma 1) and the same stars, but not Lemma 2, not the containment lemma and not (E'). + +**Notation.** Fix an edge port T = cd and let T_1, ..., T_q be the edge ports at c. Let L_S be W_S restricted to the coordinates x and the block c (a k x (j+k) matrix) and R_S the same for U_S; lambda_S = rank L_S, rho_S = rank R_S; L and R are the stacks (qk x (j+k)); ell = rank L, rho = rank R. + +**Proposition 10 (LR) [P+C].** For every edge port T = cd: + + **G_c + k <= j + 2 (g_T(c) + g_T(d)).** + +*Proof.* +1. For S != T in the star, L_S R_T^T = B_ST = 0 (the supports of W_S, U_T meet in block c and x only), and L_T R_T^T = gamma_T(c). So L R^T = D_c is block diagonal and rank(L R^T) = G_c. +2. Let Z = rowsp L ∩ (rowsp R)^perp, the vectors of the row space of L that are orthogonal (standard bilinear form) to every row of R. The map v -> v R^T on rowsp L has kernel Z and image of dimension rank(L R^T) = G_c, so dim Z = ell - G_c. Z lies in (rowsp R)^perp, of dimension j + k - rho. So **ell - G_c <= j + k - rho.** +3. Z_S = rowsp L_S ∩ (rowsp R_S)^perp has dimension lambda_S - g_S(c) (same argument for one block). It lies in Z, because rowsp L_S is orthogonal to every R_{S'} with S' != S (step 1). So **lambda_S - g_S(c) <= ell - G_c**, and symmetrically **rho_S - g_S(c) <= rho - G_c.** +4. Adding the two inequalities of step 3 for S = T and using step 2: lambda_T + rho_T - 2 g_T(c) <= ell + rho - 2 G_c <= k + j - G_c. +5. By (1), alpha_T(c) = I - gamma_T(d), so rank alpha_T(c) >= k - g_T(d). Also lambda_T >= rank W_T[c] >= rank alpha_T(c), and the same for rho_T. So lambda_T + rho_T >= 2k - 2 g_T(d). +6. Combining 4 and 5: 2k - 2 g_T(d) - 2 g_T(c) <= k + j - G_c. ∎ + +**Theorem 11 [P+C].** If every non-isolated vertex of Gamma has degree >= 4, then j >= k. + +*Proof.* Fix c of degree d_c and sum Proposition 10 over the d_c edge ports T at c: d_c (G_c + k) <= d_c j + 2 sum over T at c of e_T, with e_T = g_T(c) + g_T(d). Sum over c. Each e_T occurs at both its ends, and sum over T of e_T = sum over c of G_c. So + + sum_c d_c G_c + 2E k <= 2E j + 4 sum_c G_c, i.e. 2E (k - j) <= sum_c (4 - d_c) G_c <= 0 + +(isolated vertices have G_c = 0; the others have d_c >= 4). As E > 0, j >= k. ∎ + +(E') is an inequality per edge and carries the charges of Theorem 6(a); (LR) is an inequality per edge and star, summed with degree weights. Either gives Theorem 8. + +## 8. Corollaries on the graphs G_Gamma + +For a simple graph Gamma on n vertices let **G_Gamma** be the graph with vertex set V(Gamma) together with the edges of Gamma ("pairs"); a point is adjacent to the pairs containing it, two pairs are adjacent iff disjoint, and two points are never adjacent. (K = the points and T_e = the pairs form a star configuration: (C1) and (C2) are the definition.) + +**Corollary 12 [P+C].** If Gamma has minimum degree >= 4, then **H_f(G_Gamma;F) = n+1 for every field F**; in particular H_f(G_{K_m};F) = m+1 for m >= 5. + +*Proof.* Lower bound: Theorem 6(b) with n' = n and mk + j >= (n+1)k. Upper bound: in F^{n+1} with the bilinear form diag(1, ..., 1, -1) put x_c = e_c and x_T = e_c + e_d + e_v for T = cd. Then = 1 for all points and pairs (1 + 1 - 1 for a pair); two points are orthogonal; a point and a pair not containing it are orthogonal; two pairs sharing a vertex give 1 - 1 = 0. Their Gram matrix has unit diagonal, zeros on non-adjacent pairs and rank <= n+1, so H(G_Gamma;F) <= n+1 and H_f <= H. ∎ + +`check.py` verifies this representation over F_2, F_3, F_5 for m = 5, 6, 7 [C]. #6933's weights gave only 16/3 for G_{K_5} and 20/3 for G_{K_6}. + +**Corollary 13 (Petersen) [P+C].** G_{K_4} is the Petersen graph [C]: the map point a -> {a,5}, pair {b,c} -> {1,2,3,4} minus {b,c} is an isomorphism onto the Kneser graph K(5,2). Here Lambda_c = 3/2 < 2 at every vertex, n' = 4, E = 6, so Theorem 6(a) gives j/k >= 2/4 and **H_f(Petersen;F) >= 9/2 for every field F.** Since the Gram representation above gives H <= 5 (the F_2 rank of I + A is 5 [C]), the value is in [9/2, 5]. Over F_2 with k = 2 the rank-9 row (ratio 9/2) is recorded UNSAT [R] (section 10), so 9/2 is not attained at k = 2 over F_2. + +**This corollary was not checked against the literature.** The Shannon capacity of the Petersen graph is 4 (alpha = 4 and the Lovasz number is 4; stated from memory, not rechecked), so the claim is above that capacity. If a representation of the Petersen graph of ratio below 9/2 is known, Theorem 6 is wrong, and that would be the quickest refutation. Bukh and Cox and Blasiak's thesis were not searched for a Petersen value. + +## 9. Field-only dependence [P+C] + +**Remark 14.** For every field E, w(V;E) = w(V;F_0), with F_0 the prime field of E; the same holds for w(G;E) for every graph G. + +*Proof.* (a) *Subfields.* A k-block pattern over F_0 is one over E, so w(V;E) <= w(V;F_0). +(b) *Finite extensions.* Let L/F be an extension of degree s, and fix an F-basis of L. Replace each entry a of a k-block pattern B over L by the s x s matrix rho(a) of multiplication by a. rho is an injective ring homomorphism M_t(L) -> M_{st}(F), so it maps invertible blocks to invertible blocks and zero blocks to zero blocks, and rank_F rho(M) = s rank_L(M) (rho(M) is M as an F-linear map). So rho(B) is an sk-block pattern over F of ratio rank_L(B)/k: w(V;F) <= w(V;L). With (a), w(V;L) = w(V;F). (`check.py` verifies the homomorphism and the rank identity for F_4 over F_2 on 60 random matrices [C].) +(c) *Arbitrary fields.* Let B be a k-block pattern over E. Let A be the subring of E generated by F_0 and the entries of B and the inverses of the determinants of the diagonal blocks; A is a finitely generated F_0-algebra and a domain. Choose a maximal ideal m of A. By the Nullstellensatz (Zariski's lemma) A/m is a finite extension of F_0 (a finite field if char E > 0, a number field if char E = 0). Reduction modulo m keeps the diagonal blocks invertible (their determinants are units in A) and the zero blocks zero, and cannot raise the rank (minors that vanish keep vanishing). So there is a pattern over A/m of the same k and rank at most rank B; by (b) w(V;F_0) = w(V;A/m) <= rank B / k. Hence w(V;F_0) <= w(V;E). ∎ + +So "try F_4 or F_8" is not a new search space: w depends only on the characteristic. Theorem 6 does not need this; it holds for every field directly. + +## 10. Solver cross-checks [R] + +Rows of `data/sat_rows.json`: F_2 block patterns in the gauge of Lemma 1 (K on blocks; each edge port supported on the blocks of its odd K-neighbours and on j extra coordinates), unit diagonal blocks, zero blocks on all orthogonal pairs among the instance ports; rank = |K| k + j; solver kissat 4.0.4, 20-minute cap. **No DRAT proofs were produced for these rows**: each UNSAT is the solver's answer only. `check.py` recomputes each instance from `data/ports_p104.json`, applies Theorem 6 to it and compares with the recorded row; it does not run a solver, and the CNF files are not shipped. "SB" means each W_T is put in reduced row echelon form, which is a symmetry of the problem ((W_T, U_T) -> (g W_T, g^{-T} U_T), g in GL_k(F_2), keeps B_TT = I and all zero blocks) [P]. + +| instance | k | rank | result (time) | Theorem 6 says | +|---|---|---|---|---| +| Petersen: 4 points + 6 pair ports (10 ports; cubic, girth 5) | 4 | 17 (j=1) | UNSAT (SB, 8.5 s); undecided at 20 min without SB | infeasible (j >= 2) | +| same | 4 | 20 (j=4), control | SAT (0.0 s), decoded and re-checked | allowed | +| same | 2 | 9 (j=1) | UNSAT (SB 0.0 s; no SB 0.5 s) | allowed (j/k = 1/2 equals the threshold) | +| same | 2 | 10 (j=2), control | SAT (0.0 s), decoded and re-checked | allowed | +| G_{K_5}: 5 points + 10 pair ports (15 ports) | 3 | 16 (j=1) | UNSAT (SB, 0.6 s) | infeasible (j >= 3) | +| same | 3 | 17 (j=2) | UNSAT (SB, 57.2 s) | infeasible | +| same | 3 | 18 (j=3), control | SAT (SB, 689.7 s), decoded and re-checked | allowed (threshold attained) | +| 14-port subset of #6933 (K0 + 6 edge ports) | 2 | 17 (j=1), control | SAT, decoded and re-checked; the recorded witness itself, planted as unit clauses, is SAT; a mutant is rejected | allowed (minimum degree 1) | +| 30 ports (K of type (22; 5,5,5,5,6,6,6,6) + 22 edge ports) | 6 | 53 (j=5) | **undecided at 20 min** (SB; and without SB) | infeasible, not tested | +| same | 6 | 54 (j=6), control | undecided at 20 min (SB; and without SB) | allowed | + +Every row that Theorem 6 predicts infeasible and that was decided came back UNSAT, and no decided row contradicts the theorem. The k = 6 rank 53 run on 30 ports was undecided at 20 minutes, and so was its same-size feasible control; **neither is used**, and nothing in this note depends on any row: Theorem 6 is a proof, the rows are a cross-check of it and of the encoding. The two 5-point rows use a different orthogonal 8-set from the 30-port row; only the sub-structure (5 points and all 10 pair ports) matters. The k = 2, rank 9 Petersen row sits at the threshold of Theorem 6(a) and says that no 2-block pattern of ratio 9/2 exists over F_2 for this instance. + +## 11. Relation to #6933, and what is not closed + +**Why Theorem 3 stopped at 53/6.** (E') replaces the pair (Block), (Edge) of #6933 by one inequality without the term s_T. A floating-point linear program over the old inequality system (per-edge, per-end weights; (Edge), (Block) with a family-wise Y, (Star), s <= j) on one K of type (22; 5,5,5,5,6,6,6,6) returned 5/6 as the optimum, including after adding every single-block family containing the pair port and the diagonal; this is recorded only, nothing here depends on it, and the data are not shipped. With the old system the value 53/6 could not be beaten by changing weights. + +**Closed.** Open questions 1 and 2 of #6933: w(P104;F_2) = 9, and Theorem 3 extends to the floor 9 (Theorem 3', which uses only K and its edge ports). Every k-block pattern on P104 has rank >= 9k, so a tensor lift (ratio exactly 9, #6933 Theorem 5) is optimal in the block-mask model and **no fractional-window saving exists**. In odd characteristic the window is 13 by #7014 and #6933. + +**Not closed, not claimed.** +- The window is defined by the block mask on whole k x k blocks with one block size k for all ports. A mask on sub-blocks, or port-dependent block sizes k_T, are different models. From (E') and (Star) one gets sum over T of k_T <= sum over c of k_c + (E - n') j for the star configuration, which leaves arithmetic room only for a window that prices edge ports below points; no such window is defined here, and nothing here says one helps. +- Nonlinear labels are not covered (the patterns are linear algebra over a field). +- That a physical construction realises a k-block window with exactly this mask for k > 1 was not derived in #6933 and is not derived here. +- The Petersen and G_{K_m} statements are not compared with the literature (section 8). +- The value of H_f(Petersen;F) between 9/2 and 5 is open. + +## 12. Status, hypotheses, scope + +| item | statement | label | +|---|---|---| +| gauge, stars, Lemmas 1 to 3 | steps 0 and 1 of #6933 Theorem 3, restated | [P+C] | +| containment, (E') | Lemma 4, Proposition 5 | [P+C]: proof above; inequalities evaluated on explicit representations, tight on the Gram representations and the 14-port witness | +| Theorem 3' | Theorem 6 | [P+C] | +| port facts | H1, H2, K-types, minimum degree | [P] and [C] on every orthogonal 8-set of P104, P112, P120 | +| second proof | Proposition 10, Theorem 11 | [P+C] | +| G_Gamma, Petersen | Corollaries 12, 13 | [P+C]; not compared with the literature | +| field-only dependence | Remark 14 | [P+C] (F_4 over F_2 checked); the Nullstellensatz is quoted | +| odd characteristic values | 13, 14, 15 | [Q] #7014 and #6933 Theorem 4 | +| solver rows | section 10 | [R], no DRAT | + +**Review.** No human has reviewed any proof in this note. Two model sessions proved the result independently, by (E') and by (LR); a third model session read the proof of (E') line by line, found no broken step, and ran its own representation tests (106 valid representations of seven small graphs over F_2 and F_3 plus the port-system and witness cases, with planted violations that were caught). `check.py` repeats such tests with its own code written from the definitions. Representations in the checks seldom stress (E') with g > 0 and Y > 0 on the same edge in a P104-sized example; the small-graph representations do (check.py counts 1990 such edge ends), and the proof is what carries the general statement. + +**Hypotheses used.** B_TT invertible for every port; zero blocks on all orthogonal pairs among K and the edge ports (the other ports of the system are not used); K independent; edge ports have distinct pairs and edge ports at one vertex are non-adjacent. No field property, no symmetry of B, and no k = 1 assumption. + +**Not claimed.** No bound on kappa and no word; any window below 9 in a model other than the block mask; the literature status of the Petersen value; DRAT-checked solver rows. + +## References + +- [6933] research/p104-port-window-haemers (this repository, DreamingOfClouds): setting, Theorem 1 (window = fractional Haemers bound), Theorem 3 (weighted star bound), Theorem 4 (odd characteristic), Theorem 5, the 14-port pattern. +- [7014] unpaidmoon, pull request #7014 of this repository: partition of the odd graph on the 104 ports into 13 cliques of size 8. +- [BC] B. Bukh, C. Cox, *On a fractional version of Haemers' bound*, IEEE Transactions on Information Theory 65(6), 3340-3348 (2019); arXiv:1802.00476. +- [Bl] A. Blasiak, *A graph-theoretic approach to network coding*, PhD thesis, Cornell University, 2013 (as cited in [BC]). +- [H79] W. H. Haemers, *On some problems of Lovasz concerning the Shannon capacity of a graph*, IEEE Transactions on Information Theory 25(2), 231-232 (1979). +- kissat 4.0.4 (A. Biere et al.), used as an external program for section 10. diff --git a/research/p104-port-window-nine/VERIFY.json b/research/p104-port-window-nine/VERIFY.json new file mode 100644 index 0000000000..ccf9376608 --- /dev/null +++ b/research/p104-port-window-nine/VERIFY.json @@ -0,0 +1,19 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/check.py" + ], + "timeout_seconds": 300, + "checks": "Port systems P104, P112, P120 (orthogonal 8-sets 1728, 4032, 8640 and no orthogonal 9-set; structure of ports relative to every orthogonal 8-set: distinct pairs and orthogonality of edge ports at one vertex; the K-types with E and degree sequences; minimum degree 5, 6, 7 so every charge is at least 2 with weights 1/2); every inequality of the proofs (gauge and support premises, star, containment, edge inequality (E'), star inequality (LR) and its sub-lemmas, Theorem 3' conclusion j >= k) on explicit representations: Gram of P104 and P120 at k = 1 and tensor I_3 with random port scalings, the 14-port k = 2 witness over F_2 and F_3, and 800 small-graph representations over F_2 and F_3 (0/1 covers, Gram, direct sums, random solved, scalings) with g > 0 and Y > 0 on many edge ends; two planted violations that must be flagged and a valid control; H_f(G_{K_n}) = n+1 for n = 5, 6, 7 by explicit Gram representations; G_{K4} is the Petersen graph (cubic, girth 5, explicit isomorphism with Kneser K(5,2)); F_2 rank 5 of I + A(Petersen); the Petersen threshold 9/2; restriction of scalars F_4 to F_2; the recorded solver rows (instances recomputed from the port list, compared with the threshold of Theorem 3', undecided runs flagged unused)." + } + ] +} diff --git a/research/p104-port-window-nine/check.py b/research/p104-port-window-nine/check.py new file mode 100644 index 0000000000..2207819531 --- /dev/null +++ b/research/p104-port-window-nine/check.py @@ -0,0 +1,958 @@ +#!/usr/bin/env python3 +"""Exact checks for THEOREM.md. Standard library only, writes nothing, reads only data/ in this package. +Run from anywhere: python3.12 -I -B research/p104-port-window-nine/check.py +One 'PASS [tag] claim' line per claim; any failed claim prints FAIL and the exit status is 1. +The final marker is PASS_P104_PORT_WINDOW_NINE. Tags: [C] exact computation, [P+C] a proof in THEOREM.md +evaluated on explicit objects, [R] recorded solver rows (read from data/sat_rows.json, not repeated here).""" +import os, sys, json, random, itertools, collections, time +from fractions import Fraction as Fr + +HERE = os.path.dirname(os.path.abspath(__file__)) +DATA = os.path.join(HERE, 'data') +T0 = time.time() +FAILS = [] + + +def load(name): + with open(os.path.join(DATA, name), encoding='utf-8') as f: + return json.load(f) + + +def PASS(tag, msg): + print('PASS [%s] %s' % (tag, msg), flush=True) + + +def FAIL(tag, msg): + FAILS.append(msg) + print('FAIL [%s] %s' % (tag, msg), flush=True) + + +def claim(cond, tag, msg): + (PASS if cond else FAIL)(tag, msg) + return cond + + +# ---------------------------------------------------------------------------------------------------------- +# F_p linear algebra (matrices are lists of rows of ints) +# ---------------------------------------------------------------------------------------------------------- +def rank_p(M, p): + A = [[x % p for x in r] for r in M] + A = [r for r in A if r] + if not A or not A[0]: + return 0 + rk, n = 0, len(A) + for c in range(len(A[0])): + piv = next((i for i in range(rk, n) if A[i][c]), None) + if piv is None: + continue + A[rk], A[piv] = A[piv], A[rk] + inv = pow(A[rk][c], -1, p) + A[rk] = [x * inv % p for x in A[rk]] + for i in range(rk + 1, n): + f = A[i][c] + if f: + A[i] = [(x - f * y) % p for x, y in zip(A[i], A[rk])] + rk += 1 + if rk == n: + break + return rk + + +def mmT(A, B, p): + """A B^T mod p; A, B lists of rows of equal length.""" + return [[sum(a * b for a, b in zip(ra, rb)) % p for rb in B] for ra in A] + + +def mm(A, B, p): + Bt = list(zip(*B)) + return [[sum(a * b for a, b in zip(ra, cb)) % p for cb in Bt] for ra in A] + + +def ident(n): + return [[1 if i == j else 0 for j in range(n)] for i in range(n)] + + +def zeros(a, b): + return [[0] * b for _ in range(a)] + + +def madd(A, B, p, s=1): + return [[(x + s * y) % p for x, y in zip(ra, rb)] for ra, rb in zip(A, B)] + + +def hcat(A, B): + return [ra + rb for ra, rb in zip(A, B)] + + +def vcat(A, B): + return [list(r) for r in A] + [list(r) for r in B] + + +def inverse(M, p): + n = len(M) + A = [[x % p for x in r] + ident(n)[i] for i, r in enumerate(M)] + for c in range(n): + piv = next((i for i in range(c, n) if A[i][c]), None) + if piv is None: + return None + A[c], A[piv] = A[piv], A[c] + inv = pow(A[c][c], -1, p) + A[c] = [x * inv % p for x in A[c]] + for i in range(n): + if i != c and A[i][c]: + f = A[i][c] + A[i] = [(x - f * y) % p for x, y in zip(A[i], A[c])] + return [r[n:] for r in A] + + +def transpose(M): + return [list(r) for r in zip(*M)] + + +def solve_linear(rows, rhs, ncols, p, rng): + """One uniformly random solution of rows * u = rhs over F_p, or None.""" + A = [[x % p for x in r] + [b % p] for r, b in zip(rows, rhs)] + piv_cols, rk = [], 0 + for c in range(ncols): + piv = next((i for i in range(rk, len(A)) if A[i][c]), None) + if piv is None: + continue + A[rk], A[piv] = A[piv], A[rk] + inv = pow(A[rk][c], -1, p) + A[rk] = [x * inv % p for x in A[rk]] + for i in range(len(A)): + if i != rk and A[i][c]: + f = A[i][c] + A[i] = [(x - f * y) % p for x, y in zip(A[i], A[rk])] + piv_cols.append(c) + rk += 1 + if any(A[i][ncols] for i in range(rk, len(A))): + return None + u = [rng.randrange(p) for _ in range(ncols)] + for i, c in enumerate(piv_cols): + u[c] = (A[i][ncols] - sum(A[i][t] * u[t] for t in range(ncols) if t not in piv_cols)) % p + return u + + +# ---------------------------------------------------------------------------------------------------------- +# Ports, the three systems, orthogonal 8-sets +# ---------------------------------------------------------------------------------------------------------- +PORTS = load('ports_p104.json')['ports'] +DOT = [bytearray((a & b).bit_count() & 1 for b in range(512)) for a in range(512)] +dot = lambda a, b: DOT[a][b] +wt = lambda a: a.bit_count() +P120 = [x for x in range(512) if wt(x) % 4 == 3] + + +def orth_8sets(V): + """All sets of 8 pairwise orthogonal vectors of V (dot = 0); also reports whether a 9-set exists.""" + n = len(V) + nb = [0] * n + for i in range(n): + for j in range(n): + if i != j and dot(V[i], V[j]) == 0: + nb[i] |= 1 << j + out, nine = [], [False] + + def rec(cl, cand, size): + if size == 8: + out.append(cl) + if cand: + nine[0] = True + return + while cand: + low = cand & -cand + i = low.bit_length() - 1 + cand ^= low + rec(cl + [V[i]], cand & nb[i], size + 1) + rec([], (1 << n) - 1, 0) + return out, nine[0] + + +def edge_ports(V, K): + """Ports outside K with exactly two odd K-neighbours: list of (port, (i, j)) with i %d' % (c, G, k + xc - y - y2)) + st['Star-Y'] += 1 + if not G <= k + j - (y + y2): + viol.append('(Star, Y form) at point %d' % c) + st['Y<=j'] += 1 + if not (y <= xc <= j and y2 <= xc): + viol.append('Y_c <= x_c <= j at %d' % c) + # containment lemma, columns and rows, for every edge port at c + for P in Tl: + Q = gam[P] + XP = Xb(P, P) + st['containment'] += 1 + if not (rank_p(hcat(Q, XP), p) - g[(P, c)] <= y and rank_p(vcat(Q, XP), p) - g[(P, c)] <= y2): + viol.append('containment at port %d end %d' % (P, c)) + # --- (E') on every edge port + for i, (c, d) in enumerate(edges): + P = m + i + gc, gd = g[(P, c)], g[(P, d)] + ycs = [star[c]['y'], star[c]['y2'], star[d]['y'], star[d]['y2']] + Yc = Fr(star[c]['y'] + star[c]['y2'], 2) + Yd = Fr(star[d]['y'] + star[d]['y2'], 2) + st['(E-prime)'] += 1 + s4 = gc + gd + min(ycs) - k + sY = gc + gd + min(Yc, Yd) - k + if s4 < 0 or sY < 0: + viol.append("(E') at edge port %d: slack %s" % (i, min(s4, sY))) + if s4 == 0: + st['tight'] += 1 + # identity I = gamma(c) + gamma(d) - X (needs the diagonal and support premises) + lhs = madd(madd(star[c]['gam'][P], star[d]['gam'][P], p), Xb(P, P), p, -1) + if lhs != I: + prob.append('edge identity at port %d' % i) + if gc > 0 and Yc > 0: + st['gY'] += 1 + if gd > 0 and Yd > 0: + st['gY'] += 1 + # --- (LR) and its sub-lemmas + for c, s in star.items(): + Tl = s['Tl'] + L = {P: [Wx(P)[a] + Wc(P, c)[a] for a in range(k)] for P in Tl} + R = {P: [Ux(P)[a] + Uc(P, c)[a] for a in range(k)] for P in Tl} + Ls = [row for P in Tl for row in L[P]] + Rs = [row for P in Tl for row in R[P]] + ell, rho = rank_p(Ls, p), rank_p(Rs, p) + G = s['G'] + st['LR-sub'] += 1 + if rank_p(mmT(Ls, Rs, p), p) != G: + prob.append('rank(L R^T) != G at %d' % c) + if not ell - G <= j + k - rho: + viol.append('LR step 2 at %d' % c) + for P in Tl: + d = [x for x in edges[P - m] if x != c][0] + lam, rh = rank_p(L[P], p), rank_p(R[P], p) + gc, gd = g[(P, c)], g[(P, d)] + st['LR-sub'] += 1 + if not (lam - gc <= ell - G and rh - gc <= rho - G): + viol.append('LR step 3 at port %d end %d' % (P, c)) + if not (lam >= k - gd and rh >= k - gd): + viol.append('LR step 5 at port %d end %d' % (P, c)) + st['(LR)'] += 1 + sl = j + 2 * (gc + gd) - G - k + if sl < 0: + viol.append('(LR) at port %d end %d: slack %d' % (P, c, sl)) + if sl == 0: + st['tight'] += 1 + # --- Theorem 3' conclusions (only meaningful when the premises hold) + nz = [c for c in range(m) if deg[c] > 0] + E = len(edges) + if nz: + lam_sum = sum(max(Fr(deg[c], 2) - 2, 0) for c in nz) + st['general'] += 1 + if not Fr(j) * (len(nz) + lam_sum) >= k * (E - len(nz)): + viol.append("general bound j/k >= (E-n')/(n'+sum (Lambda-2)^+) fails") + if min(deg[c] for c in nz) >= 4: + st['mindeg4'] += 1 + if not j >= k: + viol.append("Theorem 3': j >= k fails with min degree >= 4 (j=%d, k=%d)" % (j, k)) + return dict(prob=prob, viol=viol, st=st, j=j, k=k) + + +def new_rep(p, k, m, j, edges, orth=None): + return dict(p=p, k=k, m=m, j=j, edges=list(edges), W={}, U={}, + orth=abstract_orth(m, edges) if orth is None else orth) + + +def point_labels(rep): + p, k, m, j = rep['p'], rep['k'], rep['m'], rep['j'] + r = m * k + j + for c in range(m): + e = [[1 if t == c * k + x else 0 for t in range(r)] for x in range(k)] + rep['W'][c] = [list(row) for row in e] + rep['U'][c] = [list(row) for row in e] + + +def gram_abstract(p, m, edges, k=1): + """Gram representation of the configuration: W_T = e_c + e_d + v, U_T = e_c + e_d - v (valid over every F_p); + tensored with I_k.""" + rep = new_rep(p, k, m, k, edges) + point_labels(rep) + r = m * k + k + for i, (c, d) in enumerate(edges): + W, U = [], [] + for x in range(k): + w = [0] * r + w[c * k + x] = w[d * k + x] = 1 + u = list(w) + w[m * k + x] = 1 + u[m * k + x] = p - 1 + W.append(w) + U.append(u) + rep['W'][m + i], rep['U'][m + i] = W, U + return rep + + +def cover_rep(p, m, edges, rng): + """0/1 clique-cover representation: every edge port sits in exactly one clique: the clique of an end point + (each point hosts at most one edge) or a coordinate x shared with pairwise disjoint edges.""" + host = {} + xc = [] # list of lists of edge indices (pairwise disjoint) + order = list(range(len(edges))) + rng.shuffle(order) + for i in order: + c, d = edges[i] + opts = [e for e in (c, d) if e not in host] + if opts and rng.random() < 0.6: + host[rng.choice(opts)] = i + continue + for cl in xc: + if all(not set(edges[i]) & set(edges[i2]) for i2 in cl) and rng.random() < 0.7: + cl.append(i) + break + else: + xc.append([i]) + placed = {} + for c, i in host.items(): + placed[i] = ('pt', c) + for q, cl in enumerate(xc): + for i in cl: + placed[i] = ('x', q) + j = len(xc) + rep = new_rep(p, 1, m, j, edges) + point_labels(rep) + r = m + j + for i in range(len(edges)): + kind, q = placed[i] + row = [0] * r + row[q if kind == 'pt' else m + q] = 1 + rep['W'][m + i] = [list(row)] + rep['U'][m + i] = [list(row)] + return rep + + +def dsum(r1, r2): + assert r1['p'] == r2['p'] and r1['m'] == r2['m'] and r1['edges'] == r2['edges'] + p, m = r1['p'], r1['m'] + k1, k2, j1, j2 = r1['k'], r2['k'], r1['j'], r2['j'] + k, j = k1 + k2, j1 + j2 + r = m * k + j + out = new_rep(p, k, m, j, r1['edges'], r1['orth']) + + def place(row, which): + new = [0] * r + kk, jj = (k1, j1) if which == 1 else (k2, j2) + off, xoff = (0, 0) if which == 1 else (k1, j1) + for c in range(m): + for t in range(kk): + new[c * k + off + t] = row[c * kk + t] + for t in range(jj): + new[m * k + xoff + t] = row[m * kk + t] + return new + for key in ('W', 'U'): + for P in r1[key]: + out[key][P] = [place(row, 1) for row in r1[key][P]] + [place(row, 2) for row in r2[key][P]] + return out + + +def scale_ports(rep, rng, which=None): + """(W_T, U_T) -> (M W_T, M^{-T} U_T) with M random invertible, for every edge port (a symmetry of all premises).""" + p, k, m = rep['p'], rep['k'], rep['m'] + out = dict(rep, W=dict(rep['W']), U=dict(rep['U'])) + for i in range(len(rep['edges'])): + P = m + i + while True: + M = [[rng.randrange(p) for _ in range(k)] for _ in range(k)] + Mi = inverse(M, p) + if Mi is not None: + break + out['W'][P] = mm(M, rep['W'][P], p) + out['U'][P] = mm(transpose(Mi), rep['U'][P], p) + return out + + +def swapped(rep): + return dict(rep, W=rep['U'], U=rep['W']) + + +def random_solved_rep(p, m, edges, k, j, rng, dens=0.7): + """Random W on the allowed supports, then each U_S solved from the linear conditions B_TS = 0 (T orthogonal + to S) and B_SS = I. Returns a rep or None if some system is unsolvable.""" + rep = new_rep(p, k, m, j, edges) + point_labels(rep) + r = m * k + j + nP = m + len(edges) + supp = {} + for i, (c, d) in enumerate(edges): + P = m + i + supp[P] = list(range(c * k, (c + 1) * k)) + list(range(d * k, (d + 1) * k)) + list(range(m * k, r)) + W = [[0] * r for _ in range(k)] + for a in range(k): + for t in supp[P]: + if rng.random() < dens: + W[a][t] = rng.randrange(1, p) + if rank_p(W, p) < k: + return None + rep['W'][P] = W + for P in range(m, nP): + U = [[0] * r for _ in range(k)] + S = supp[P] + for i in range(k): + rows, rhs = [], [] + for T in range(nP): + if T == P or (min(T, P), max(T, P)) in rep['orth']: + for a in range(k): + rows.append([rep['W'][T][a][t] for t in S]) + rhs.append(1 if (T == P and a == i) else 0) + sol = solve_linear(rows, rhs, len(S), p, rng) + if sol is None: + return None + for t, v in zip(S, sol): + U[i][t] = v + rep['U'][P] = U + return rep + + +def rep_from_ports(vecs_K, Ed, k, rng=None, scale=False): + """Gram representation of a real configuration in characteristic 2: the orthonormal basis K + v + (v = all-ones + sum K) turns dot into the standard form, so labels are coordinate vectors. Tensored with I_k + and, if scale, random invertible scalings of the edge ports (K ports stay in the gauge).""" + m = len(vecs_K) + v = 0x1FF + for c in vecs_K: + v ^= c + assert dot(v, v) == 1 and all(dot(v, c) == 0 for c in vecs_K) + edges = [A for _, A in Ed] + vecs = list(vecs_K) + [t for t, _ in Ed] + orth = {(a, b) for a in range(len(vecs)) for b in range(a + 1, len(vecs)) if dot(vecs[a], vecs[b]) == 0} + rep = new_rep(2, k, m, k, edges, orth) + point_labels(rep) + r = m * k + k + for idx, (t, A) in enumerate(Ed): + co = [dot(t, c) for c in vecs_K] + [dot(t, v)] + rows = [] + for x in range(k): + w = [0] * r + for c in range(m): + w[c * k + x] = co[c] + w[m * k + x] = co[m] + rows.append(w) + rep['W'][m + idx] = rows + rep['U'][m + idx] = [list(w) for w in rows] + return scale_ports(rep, rng) if scale else rep + + +def summarize(results): + tot = collections.Counter() + for res in results: + tot.update(res['st']) + return tot + + +# ---------------------------------------------------------------------------------------------------------- +# Section 1: port systems, K-types, hypotheses of Theorem 3' +# ---------------------------------------------------------------------------------------------------------- +def section_ports(): + claim(len(PORTS) == 104 and len(set(PORTS)) == 104 and all(wt(x) % 4 == 3 for x in PORTS), 'C', + 'P104: 104 distinct vectors of F_2^9, every weight 3 mod 4 (so dot(p,p)=1)') + claim(sorted(collections.Counter(wt(x) for x in PORTS).items()) == [(3, 70), (7, 34)] and set(PORTS) <= set(P120) + and len(P120) == 120, 'C', 'P104 has 70 ports of weight 3 and 34 of weight 7 and sits inside P120 (120 vectors)') + deleted = sorted(set(P120) - set(PORTS)) + fr = [c for c in itertools.combinations(deleted, 8) if all(dot(a, b) == 1 for a, b in itertools.combinations(c, 2))] + claim(len(deleted) == 16 and len(fr) == 2 and set(fr[0]) | set(fr[1]) == set(deleted), 'C', + 'the 16 vectors of P120 outside P104 are exactly two odd 8-cliques (P112 = P104 plus one of them)') + systems = {'P104': list(PORTS), 'P112a': list(PORTS) + list(fr[0]), 'P112b': list(PORTS) + list(fr[1]), 'P120': list(P120)} + want = {'P104': 1728, 'P112a': 4032, 'P112b': 4032, 'P120': 8640} + sets8 = {} + for name, V in systems.items(): + S, nine = orth_8sets(V) + sets8[name] = (V, S) + claim(len(S) == want[name] and not nine, 'C', '%s: %d orthogonal 8-sets, and no 9 pairwise orthogonal ports' % (name, len(S))) + types = {} + t_h = time.time() + for name, (V, S) in sets8.items(): + cnt = collections.Counter() + h1 = h2 = True + lam_ok = True + nonisolated8 = True + for K in S: + Ed, degs = gamma_data(V, K) + cnt[(len(Ed), tuple(sorted(degs)))] += 1 + pairs = [A for _, A in Ed] + h1 &= len(set(pairs)) == len(pairs) + for (s, A), (t, B) in itertools.combinations(Ed, 2): + if len(set(A) & set(B)) == 1 and dot(s, t) != 0: + h2 = False + lam_ok &= all(Fr(d, 2) >= 2 for d in degs) # lambda_T = 1/2 gives Lambda_c = d_c / 2 + nonisolated8 &= all(d > 0 for d in degs) + types[name] = cnt + claim(h1 and h2, 'P+C', '%s: on every orthogonal 8-set, edge ports have distinct pairs (H1) and edge ports sharing exactly one ' + 'vertex are orthogonal (H2)' % name) + mind = min(min(t[1]) for t in cnt) + claim(mind >= 4 and nonisolated8 and lam_ok, 'P+C', + "%s: every orthogonal 8-set has n'=8 and minimum degree %d >= 4, so lambda=1/2 gives every charge Lambda_c = d_c/2 >= 2" % (name, mind)) + p104 = types['P104'] + exp = {(22, (5, 5, 5, 5, 6, 6, 6, 6)): 960, (22, (5, 5, 5, 5, 5, 6, 6, 7)): 384, (21, (5, 5, 5, 5, 5, 5, 6, 6)): 384} + claim(dict(p104) == exp, 'C', 'P104 K-types (E; sorted degrees): (22;5,5,5,5,6,6,6,6) x 960, (22;5,5,5,5,5,6,6,7) x 384, ' + '(21;5,5,5,5,5,5,6,6) x 384; minimum degree 5 on all 1728') + p112 = {(25, (6, 6, 6, 6, 6, 6, 7, 7)): 3584, (24, (6,) * 8): 448} + claim(dict(types['P112a']) == p112 and dict(types['P112b']) == p112, 'C', + 'P112 K-types: (25;6^6,7,7) x 3584 and (24;6^8) x 448, for either choice of clique') + claim(dict(types['P120']) == {(28, (7,) * 8): 8640}, 'C', 'P120 K-type: (28;7^8) on all 8640 orthogonal 8-sets') + return systems, sets8 + + +# ---------------------------------------------------------------------------------------------------------- +# Section 2: inequalities on explicit representations +# ---------------------------------------------------------------------------------------------------------- +def report(tag, label, results, need_gY=False, need_tight=False): + tot = summarize(results) + bad = [v for res in results for v in res['viol']] + pr = [v for res in results for v in res['prob']] + ok = not bad and not pr + extra = '' + if need_gY: + ok &= tot['gY'] > 0 + extra += '; %d edge ends with g>0 and Y>0' % tot['gY'] + if need_tight: + ok &= tot['tight'] > 0 + claim(ok, tag, "%s: %d reps, premises hold, (E') x%d, (LR) x%d, (Star) x%d, containment x%d, no violation; %d tight cases%s" + % (label, len(results), tot["(E-prime)"], tot['(LR)'], tot['Star'], tot['containment'], tot['tight'], extra)) + if bad or pr: + print(' first problems:', (pr + bad)[:4], flush=True) + + +def section_reps(systems, sets8): + rng = random.Random(20251110) + # (a) Gram of P104 and of P120, k = 1, over F_2: one K of each type, plus a spread of K's + for name in ('P104', 'P120'): + V, S = sets8[name] + seen, picks = set(), [] + for K in S: + Ed, degs = gamma_data(V, K) + key = (len(Ed), tuple(sorted(degs))) + if key not in seen: + seen.add(key) + picks.append(K) + picks += S[::max(1, len(S) // 25)] + res = [analyse(rep_from_ports(K, gamma_data(V, K)[0], 1)) for K in picks] + res_j = {(r['j'], r['k']) for r in res} + claim(res_j == {(1, 1)}, 'C', '%s Gram representation at k=1 (inner dimension 9 = 8k + j): j = k = 1 on %d choices of K' % (name, len(res))) + report('P+C', '%s Gram, k=1, F_2' % name, res, need_tight=True) + # (b) Gram tensor I_3 with random port scalings + for name in ('P104', 'P120'): + V, S = sets8[name] + picks = S[::max(1, len(S) // 8)][:8] + res = [analyse(rep_from_ports(K, gamma_data(V, K)[0], 3, rng, scale=True)) for K in picks] + claim({(r['j'], r['k']) for r in res} == {(3, 3)}, 'C', '%s Gram tensor I_3 with random port scalings: j = k = 3' % name) + report('P+C', '%s Gram tensor I_3, random scalings, F_2' % name, res, need_tight=True) + # (c) the 14-port witness, k = 2, rank 17 (j = 1 < k): minimum degree < 4, so no contradiction + w = load('witness14.json') + Kw = [PORTS[i] for i in w['K']] + others = [PORTS[i] for i in w['others']] + Ed = edge_ports(Kw + others, Kw) + claim(len(Ed) == 6 and sorted(t for t, _ in Ed) == sorted(others), 'C', 'witness: the six extra ports are exactly the edge ports of K0') + edges = {t: A for t, A in Ed} + order = [t for t in others] + kk, jj, m = w['k'], 1, 8 + for p in (2, 3): + rep = new_rep(p, kk, m, jj, [edges[t] for t in order], + {(a, b) for a in range(14) for b in range(a + 1, 14) + if dot((Kw + order)[a], (Kw + order)[b]) == 0}) + r = m * kk + jj + for a, idx in enumerate(w['K'] + w['others']): + rows = [] + for cc in w['coords'][str(idx)]: + row = [0] * r + row[cc] = 1 + rows.append(row) + if a < m: + rep['W'][a], rep['U'][a] = rows, [list(x) for x in rows] + else: + rep['W'][a], rep['U'][a] = rows, [list(x) for x in rows] + # coordinates in the file: block of i-th K element is 2i, 2i+1; extra coordinate 16 (matches the gauge) + res = analyse(rep) + n_orth = 2 * len(rep['orth']) + Bfull = [[0] * 28 for _ in range(28)] + for a in range(14): + for b in range(14): + blk = mmT(rep['W'][a], rep['U'][b], p) + for x in range(2): + for y in range(2): + Bfull[2 * a + x][2 * b + y] = blk[x][y] + rk = rank_p(Bfull, p) + claim(rk == 17 and not res['prob'] and n_orth == 150, 'C', 'witness over F_%d: 14-port 2-block pattern, B 28x28 of rank %d < 18 = 9k, premises hold (gauge, supports, diagonal blocks I_2, zero blocks on all %d ordered orthogonal pairs)' % (p, rk, n_orth)) + report('P+C', "witness (k=2, j=1), F_%d" % p, [res], need_tight=True) + if p == 2: + scaled = [analyse(scale_ports(rep, rng)) for _ in range(5)] + report('P+C', 'witness with random port scalings, F_2', scaled) + # (d) random small-graph representations over F_2 and F_3 + graphs = {'triangle': (3, [(0, 1), (0, 2), (1, 2)]), 'star3': (4, [(0, 1), (0, 2), (0, 3)]), + 'path4': (4, [(0, 1), (1, 2), (2, 3)]), 'C4': (4, [(0, 1), (1, 2), (2, 3), (0, 3)]), + 'K4-e': (4, [(0, 1), (0, 2), (0, 3), (1, 2), (1, 3)]), + 'K4': (4, list(itertools.combinations(range(4), 2))), 'K5': (5, list(itertools.combinations(range(5), 2)))} + results, kinds = [], collections.Counter() + for p in (2, 3): + for gname, (m, edges) in graphs.items(): + reps = [] + for _ in range(2): + reps.append(('cover', cover_rep(p, m, edges, rng))) + reps.append(('gram', gram_abstract(p, m, edges))) + reps.append(('gram x I_2', gram_abstract(p, m, edges, 2))) + for _ in range(3): + reps.append(('gram + cover', dsum(gram_abstract(p, m, edges), cover_rep(p, m, edges, rng)))) + reps.append(('gram + cover + cover', dsum(dsum(gram_abstract(p, m, edges), cover_rep(p, m, edges, rng)), cover_rep(p, m, edges, rng)))) + if gname != 'K5': + for (k, j) in ((1, 2), (1, 3), (1, 4), (2, 2), (2, 3)): + for _ in range(8): + rr = random_solved_rep(p, m, edges, k, j, rng) + if rr is not None: + reps.append(('random solved', rr)) + for kind, rep in list(reps): + reps.append((kind + ', scaled', scale_ports(rep, rng))) + reps += [(kind + ', W<->U', swapped(rep)) for kind, rep in reps[:8]] + for kind, rep in reps: + results.append(analyse(rep)) + kinds[kind] += 1 + nrand = sum(v for k_, v in kinds.items() if k_.startswith('random solved')) + claim(nrand >= 20, 'C', 'random linear-solved representations found on the small graphs (F_2, F_3): %d (plus %d structured ones)' % (nrand, len(results) - nrand)) + report('P+C', 'small-graph representations over F_2 and F_3 (7 graphs, 0/1 covers, Gram, direct sums, scalings, random solved)', + results, need_gY=True, need_tight=True) + k5 = [r for r in results if r['st']['mindeg4']] + claim(len(k5) >= 20 and all(r['j'] >= r['k'] for r in k5), 'P+C', "Theorem 3': j >= k on all %d representations whose graph has minimum degree >= 4 (K5)" % len(k5)) + # (e) planted violations: the checker must be able to fail + planted_a = new_rep(3, 1, 5, 0, list(itertools.combinations(range(5), 2))) + point_labels(planted_a) + for i, (c, d) in enumerate(planted_a['edges']): + row = [0] * 5 + row[c] = row[d] = 1 + planted_a['W'][5 + i] = [row] + planted_a['U'][5 + i] = [[2 * x % 3 for x in row]] # B_TT = 2*2 = 1 mod 3, but the star zeros are gone + res_a = analyse(planted_a) + claim(res_a['prob'] and any('(LR)' in v for v in res_a['viol']) and any('Theorem 3' in v for v in res_a['viol']), 'C', + 'planted violation A (K5 over F_3, edge ports e_c+e_d with j=0, star zeros dropped): premises flagged, (LR) violated (%d times), j >= k fails' + % sum('(LR)' in v for v in res_a['viol'])) + b = cover_rep(2, 5, list(itertools.combinations(range(5), 2)), random.Random(5)) + planted_b = dict(b, W=dict(b['W']), U=dict(b['U'])) + target = 5 + b['edges'].index((0, 1)) + row = [0] * (5 + b['j']) + row[2] = 1 + planted_b['W'][target] = [list(row)] + planted_b['U'][target] = [list(row)] + res_b = analyse(planted_b) + claim(res_b['prob'] and any(v.startswith("(E')") or v.startswith('(LR)') or v.startswith('(Star') or 'containment' in v for v in res_b['viol']), 'C', + 'planted violation B (K5 cover representation with port T_01 moved onto the coordinate of point 2, mask broken): premises flagged, inequality violated (%s)' + % '; '.join(sorted({v.split(' at')[0].split(':')[0] for v in res_b['viol']})[:3])) + # a control: a valid rep with the same graph passes + ctl = analyse(dsum(gram_abstract(2, 5, list(itertools.combinations(range(5), 2))), cover_rep(2, 5, list(itertools.combinations(range(5), 2)), random.Random(5)))) + claim(not ctl['prob'] and not ctl['viol'], 'C', 'control: a valid K5 representation (Gram + cover, k=2) raises neither flags nor violations') + + +# ---------------------------------------------------------------------------------------------------------- +# Section 3: corollaries on the abstract graphs G_Gamma +# ---------------------------------------------------------------------------------------------------------- +def g_graph(m, edges): + """G_Gamma: points, pairs (edge ports); point ~ edge iff incident; edges ~ iff disjoint; points pairwise non-adjacent.""" + nP = m + len(edges) + orth = abstract_orth(m, edges) + adj = {a: set() for a in range(nP)} + for a in range(nP): + for b in range(nP): + if a != b and (min(a, b), max(a, b)) not in orth: + adj[a].add(b) + return adj + + +def f2_rank_I_plus_A(adj): + n = len(adj) + rows = [[1 if (a == b or b in adj[a]) else 0 for b in range(n)] for a in range(n)] + return rank_p(rows, 2) + + +def girth(adj): + best = 99 + for s in adj: + d, par, q = {s: 0}, {s: None}, [s] + for x in q: + for y in adj[x]: + if y not in d: + d[y], par[y] = d[x] + 1, x + q.append(y) + elif par[x] != y: + best = min(best, d[x] + d[y] + 1) + return best + + +def section_corollaries(): + for n in (5, 6, 7): + edges = list(itertools.combinations(range(n), 2)) + res = [] + for p in (2, 3, 5): + res.append(analyse(gram_abstract(p, n, edges))) + claim(all(not r['prob'] and not r['viol'] and r['j'] == 1 and r['k'] == 1 for r in res), 'P+C', + "G_{K_%d}: the Gram representation (vectors e_c, e_c+e_d+v, =-1) is valid over F_2, F_3, F_5 with rank %d = n+1; " + "Theorem 3' (n'=%d, E=%d, min degree %d >= 4) gives rank >= n+1 per block, so H_f(G_{K_%d}) = %d" + % (n, n + 1, n, len(edges), n - 1, n, n + 1)) + # Petersen = G_{K4} + m, edges = 4, list(itertools.combinations(range(4), 2)) + adj = g_graph(m, edges) + cubic = all(len(a) == 3 for a in adj.values()) + claim(len(adj) == 10 and cubic and girth(adj) == 5, 'C', 'G_{K4} has 10 vertices, is cubic and has girth 5') + # explicit isomorphism with Kneser K(5,2): point a -> {a,5}, pair {b,c} -> {1,2,3,4} minus {b,c} + img = {} + for a in range(4): + img[a] = frozenset((a + 1, 5)) + for i, (b, c) in enumerate(edges): + img[4 + i] = frozenset({1, 2, 3, 4} - {b + 1, c + 1}) + kn = {a: {b for b in img if a != b and not (img[a] & img[b])} for a in img} + claim(len(set(img.values())) == 10 and kn == adj, 'C', 'the map point a -> {a,5}, pair {b,c} -> {1,2,3,4} minus {b,c} is an isomorphism G_{K4} -> Kneser K(5,2) = Petersen graph') + claim(f2_rank_I_plus_A(adj) == 5, 'C', 'the F_2 rank of I + A(Petersen) is 5, so H(Petersen; F_2) <= 5, consistent with the proved k=1 floor 5') + # Theorem 3' general form for K4: Lambda = 3/2 < 2, E = 6, n' = 4 + E, n = 6, 4 + bound = Fr(E - n, n + sum(max(Fr(3, 2) - 2, 0) for _ in range(n))) + claim(bound == Fr(1, 2), 'P+C', "Petersen: Theorem 3' general form gives j/k >= (E-n')/(n'+sum (Lambda-2)^+) = 2/4, so rank >= 4.5 k and H_f(Petersen; F) >= 9/2 over every field") + res = [] + rng = random.Random(7) + for p in (2, 3): + for _ in range(6): + res.append(analyse(dsum(gram_abstract(p, m, edges), cover_rep(p, m, edges, rng)))) + res.append(analyse(gram_abstract(p, m, edges))) + report('P+C', 'Petersen (K4) representations, F_2 and F_3', res) + claim(all(Fr(r['j'], r['k']) >= Fr(1, 2) for r in res), 'P+C', 'every checked Petersen representation has j/k >= 1/2 (best seen: Gram, j/k = 1, ratio (4+1)/1 = 5)') + + +# ---------------------------------------------------------------------------------------------------------- +# Section 4: restriction of scalars (field-only dependence), F_4 over F_2 +# ---------------------------------------------------------------------------------------------------------- +def f4_mul(a, b): + r = 0 + for i in range(2): + if (b >> i) & 1: + r ^= a << i + if r & 4: + r ^= 0b111 + return r + + +def f4_inv(a): + return next(b for b in range(1, 4) if f4_mul(a, b) == 1) + + +def f4_rank(M): + A = [list(r) for r in M] + rk, n = 0, len(A) + for c in range(len(A[0])): + piv = next((i for i in range(rk, n) if A[i][c]), None) + if piv is None: + continue + A[rk], A[piv] = A[piv], A[rk] + inv = f4_inv(A[rk][c]) + A[rk] = [f4_mul(inv, x) for x in A[rk]] + for i in range(n): + if i != rk and A[i][c]: + f = A[i][c] + A[i] = [x ^ f4_mul(f, y) for x, y in zip(A[i], A[rk])] + rk += 1 + return rk + + +def rho_entry(a): + # multiplication by a in the F_2-basis {1, w}: columns a*1 and a*w; elements are 2-bit ints (bit 1 = w) + c1, c2 = a, f4_mul(a, 2) + return [[c1 & 1, c2 & 1], [(c1 >> 1) & 1, (c2 >> 1) & 1]] + + +def rho(M): + out = [] + for row in M: + blocks = [rho_entry(a) for a in row] + for t in range(2): + out.append([blocks[b][t][s] for b in range(len(row)) for s in range(2)]) + return out + + +def f4_mm(A, B): + return [[__import__('functools').reduce(lambda x, y: x ^ y, (f4_mul(A[i][t], B[t][j]) for t in range(len(B))), 0) + for j in range(len(B[0]))] for i in range(len(A))] + + +def section_scalars(): + rng = random.Random(4) + ok_hom = ok_rank = True + for _ in range(60): + n = rng.choice((2, 3, 4)) + A = [[rng.randrange(4) for _ in range(n)] for _ in range(n)] + Bm = [[rng.randrange(4) for _ in range(n)] for _ in range(n)] + ok_hom &= rho(f4_mm(A, Bm)) == mm(rho(A), rho(Bm), 2) + ok_rank &= rank_p(rho(A), 2) == 2 * f4_rank(A) + claim(ok_hom and ok_rank and rho([[1]]) == ident(2) and rho([[0]]) == zeros(2, 2), 'P+C', + 'restriction of scalars F_4 -> F_2: rho(AB) = rho(A) rho(B), rho(1) = I_2, rho(0) = 0, rank_F2 rho(A) = 2 rank_F4 A (60 random matrices)') + + +# ---------------------------------------------------------------------------------------------------------- +# Section 5: recorded solver rows (read from data/sat_rows.json; nothing is solved here) +# ---------------------------------------------------------------------------------------------------------- +def section_rows(): + rows = load('sat_rows.json') + inst = rows['instances'] + info = {} + for name, d in inst.items(): + K = [PORTS[i] for i in d['K']] + E = [PORTS[i] for i in d['edge_ports']] + Ed = [(t, tuple(i for i, c in enumerate(K) if dot(t, c))) for t in E] + deg = collections.Counter(c for _, A in Ed for c in A) + okcfg = (all(dot(a, b) == 0 for a, b in itertools.combinations(K, 2)) and all(len(A) == 2 for _, A in Ed) + and len({A for _, A in Ed}) == len(Ed) + and all(dot(s, t) == 0 for (s, A), (t, B) in itertools.combinations(Ed, 2) if len(set(A) & set(B)) == 1)) + nz = [c for c in range(len(K)) if deg[c] > 0] + npr, Ecount = len(nz), len(E) + lam = sum(max(Fr(deg[c], 2) - 2, 0) for c in nz) + thr = Fr(Ecount - npr) / (npr + lam) # Theorem 3' general form: j/k >= thr + info[name] = dict(n=len(K), thr=thr) + claim(okcfg and (len(K), npr, Ecount, min(deg[c] for c in nz)) == tuple(d['shape']), 'C', + "recorded instance %s: %d orthogonal points (%d non-isolated), %d edge ports with distinct pairs, minimum degree %d, " + "edge ports at one vertex orthogonal; Theorem 3' gives j/k >= %s" % (name, len(K), npr, Ecount, d['shape'][3], thr)) + decided = [r for r in rows['rows'] if r['result'] in ('SAT', 'UNSAT')] + for r in rows['rows']: + i = info[r['instance']] + r['_j'] = r['rank'] - i['n'] * r['k'] + r['_pred'] = Fr(r['_j']) < i['thr'] * r['k'] # theorem says infeasible + sat = [r for r in decided if r['result'] == 'SAT'] + claim(len(sat) >= 6 and not any(r['_pred'] for r in sat), 'R', + "recorded rows: none of the %d SAT rows lies below the Theorem 3' threshold" % len(sat)) + pred = [r for r in decided if r['_pred']] + claim(len(pred) >= 3 and all(r['result'] == 'UNSAT' for r in pred), 'R', + "recorded rows: every decided row that Theorem 3' predicts infeasible came back UNSAT (%d rows: %s)" % (len(pred), ', '.join(r['id'] for r in pred))) + claim(all(r['result'] == 'SAT' for r in decided if r.get('role') == 'control'), 'R', + 'recorded rows: every same-size control (decided) came back SAT (%d controls)' % sum(1 for r in decided if r.get('role') == 'control')) + probe = [r for r in decided if r.get('role') == 'probe'] + claim(len(probe) == 2 and all(r['result'] == 'UNSAT' and not r['_pred'] for r in probe), 'R', + "recorded sharpness probe (Petersen, k=2, rank 9, j/k = 1/2 = the threshold): allowed by Theorem 3', answered UNSAT with and without symmetry breaking") + und = [r for r in rows['rows'] if r['result'] not in ('SAT', 'UNSAT')] + claim(len(und) >= 3 and all(r.get('used') is False for r in und), 'R', + 'recorded undecided runs (k=6 rank 53 and its rank-54 control, k=4 rank 17 without symmetry breaking) are flagged not used (%d runs)' % len(und)) + + +def main(): + systems, sets8 = section_ports() + section_reps(systems, sets8) + section_corollaries() + section_scalars() + section_rows() + if FAILS: + print('FAILED %d claim(s) in %.1f s' % (len(FAILS), time.time() - T0)) + sys.exit(1) + print('PASS_P104_PORT_WINDOW_NINE (%.1f s)' % (time.time() - T0)) + + +if __name__ == '__main__': + main() diff --git a/research/p104-port-window-nine/data/ports_p104.json b/research/p104-port-window-nine/data/ports_p104.json new file mode 100644 index 0000000000..8037fd1087 --- /dev/null +++ b/research/p104-port-window-nine/data/ports_p104.json @@ -0,0 +1,109 @@ +{ +"description": "The 104 ports of P104 as vectors of F_2^9 (bit i of the integer is coordinate i), in a fixed order; two distinct ports are adjacent in the odd graph iff popcount(a & b) is odd.", +"ports": [ +11, +19, +35, +131, +259, +13, +21, +37, +69, +133, +261, +41, +73, +265, +49, +81, +145, +273, +161, +193, +321, +385, +14, +22, +38, +70, +134, +262, +26, +74, +138, +50, +146, +274, +98, +290, +194, +322, +386, +28, +44, +140, +268, +84, +148, +276, +100, +164, +292, +196, +324, +388, +56, +88, +152, +280, +168, +296, +200, +328, +392, +112, +176, +304, +208, +336, +400, +224, +352, +416, +508, +506, +502, +494, +478, +446, +382, +254, +505, +501, +493, +477, +445, +381, +253, +499, +475, +443, +379, +251, +487, +471, +439, +375, +247, +463, +431, +367, +239, +415, +351, +223, +319, +191 +] +} \ No newline at end of file diff --git a/research/p104-port-window-nine/data/sat_rows.json b/research/p104-port-window-nine/data/sat_rows.json new file mode 100644 index 0000000000..dfe9ab9e4e --- /dev/null +++ b/research/p104-port-window-nine/data/sat_rows.json @@ -0,0 +1,360 @@ +{ + "description": "Solver rows recorded for THEOREM.md section 8: F_2 block patterns in the gauge of the proof (K on blocks, labels supported on the blocks of the odd K-neighbours and on j extra coordinates x), unit diagonal blocks, zero blocks on all orthogonal pairs among the instance ports. rank = |K| k + j. SAT means a pattern of that rank exists; UNSAT means none does. Solver: kissat 4.0.4, 20-minute cap. No DRAT proofs were produced for these rows, so each UNSAT is the solver answer only [R]. The checks in check.py read this file, recompute each instance from data/ports_p104.json and compare each row with the threshold of Theorem 3; they do not run a solver. shape = [points, non-isolated points, edge ports, minimum degree].", + "instances": { + "petersen4": { + "description": "Four orthogonal ports of P104 and the six ports with exactly two odd neighbours among them (the abstract graph G_{K4}, the Petersen graph); 10 ports", + "K": [ + 0, + 1, + 3, + 50 + ], + "edge_ports": [ + 11, + 14, + 18, + 72, + 73, + 76 + ], + "shape": [ + 4, + 4, + 6, + 3 + ] + }, + "k5": { + "description": "Five orthogonal ports of P104 and the ten ports with exactly two odd neighbours among them (G_{K5}); 15 ports", + "K": [ + 1, + 2, + 78, + 82, + 84 + ], + "edge_ports": [ + 30, + 43, + 45, + 46, + 48, + 65, + 68, + 71, + 75, + 77 + ], + "shape": [ + 5, + 5, + 10, + 4 + ] + }, + "k8_30ports": { + "description": "An orthogonal 8-set of type (22; 5,5,5,5,6,6,6,6) and its 22 edge ports; 30 ports", + "K": [ + 0, + 1, + 2, + 3, + 50, + 71, + 75, + 77 + ], + "edge_ports": [ + 4, + 11, + 14, + 16, + 18, + 42, + 43, + 45, + 46, + 48, + 49, + 51, + 59, + 65, + 68, + 72, + 73, + 74, + 76, + 78, + 82, + 84 + ], + "shape": [ + 8, + 8, + 22, + 5 + ] + }, + "witness14": { + "description": "The 14-port subset carrying the 2-block pattern of rank 17: an orthogonal 8-set and six edge ports", + "K": [ + 62, + 63, + 69, + 74, + 81, + 86, + 91, + 99 + ], + "edge_ports": [ + 57, + 67, + 68, + 95, + 100, + 101 + ], + "shape": [ + 8, + 5, + 6, + 1 + ] + } + }, + "rows": [ + { + "id": "petersen_k4_r17_nosb", + "instance": "petersen4", + "k": 4, + "rank": 17, + "symmetry_breaking": false, + "result": "UNKNOWN", + "kissat_seconds": 1200.1, + "variables": 5520, + "clauses": 18048, + "dimacs_sha256": "cbbe0e7fd26e340e3a8804af1ee3aa4255e18542b74c3038552b8525fc8049c7", + "used": false, + "note": "undecided at the 20-minute cap; superseded by the symmetry-broken row" + }, + { + "id": "petersen_k4_r20_nosb", + "instance": "petersen4", + "k": 4, + "rank": 20, + "symmetry_breaking": false, + "result": "SAT", + "kissat_seconds": 0.0, + "variables": 8544, + "clauses": 28128, + "dimacs_sha256": "225c4bcb448e8258e19ec0ef0fda157e0cbce75aa3f8745cfd46b102a9a2269a", + "role": "control", + "used": true, + "note": "decoded pattern re-checked independently: rank 20, 0 violations, 160 diagonal entries, 960 forced zeros" + }, + { + "id": "petersen_k2_r9_nosb", + "instance": "petersen4", + "k": 2, + "rank": 9, + "symmetry_breaking": false, + "result": "UNSAT", + "kissat_seconds": 0.5, + "variables": 816, + "clauses": 2496, + "dimacs_sha256": "7474e69193ef2b87106fdd2b5b8755f34ff37377a0acfd79156543ac8d9ba491", + "role": "probe", + "used": true, + "note": "rank 9 = 4k+1, j/k = 1/2: at the threshold, allowed by the theorem" + }, + { + "id": "petersen_k2_r10_nosb", + "instance": "petersen4", + "k": 2, + "rank": 10, + "symmetry_breaking": false, + "result": "SAT", + "kissat_seconds": 0.0, + "variables": 1080, + "clauses": 3336, + "dimacs_sha256": "50718336a8eb4604a56312964840adc6452d9e9da97ff99917cb20187659f7c1", + "role": "control", + "used": true, + "note": "decoded pattern re-checked independently: rank 10, 0 violations, 40 diagonal entries, 240 forced zeros" + }, + { + "id": "petersen_k4_r17_sb", + "instance": "petersen4", + "k": 4, + "rank": 17, + "symmetry_breaking": true, + "result": "UNSAT", + "kissat_seconds": 8.5, + "variables": 5952, + "clauses": 20130, + "dimacs_sha256": "a569f2708782914ee7efcfa041eb15bb889ea2c6249ab8c5bc16db7d730cf785", + "used": true, + "note": "j = 1 is below the threshold 2 = k/2 of Theorem 3 (Lambda = 3/2, E = 6, n = 4): predicted infeasible" + }, + { + "id": "petersen_k4_r20_sb", + "instance": "petersen4", + "k": 4, + "rank": 20, + "symmetry_breaking": true, + "result": "SAT", + "kissat_seconds": 0.0, + "variables": 9120, + "clauses": 30912, + "dimacs_sha256": "1018a3af6e4ce6cb6aba5f486ea90d504bd4fa777d05fc42c55eddc25458f83a", + "role": "control", + "used": true, + "note": "decoded pattern re-checked independently: rank 20, 0 violations, 160 diagonal entries, 960 forced zeros" + }, + { + "id": "petersen_k2_r9_sb", + "instance": "petersen4", + "k": 2, + "rank": 9, + "symmetry_breaking": true, + "result": "UNSAT", + "kissat_seconds": 0.0, + "variables": 936, + "clauses": 2934, + "dimacs_sha256": "797f05873675bb530340fa021f06c928f9436947e85ab389149f57d9419bd831", + "role": "probe", + "used": true, + "note": "at the threshold, allowed by the theorem" + }, + { + "id": "petersen_k2_r10_sb", + "instance": "petersen4", + "k": 2, + "rank": 10, + "symmetry_breaking": true, + "result": "SAT", + "kissat_seconds": 0.0, + "variables": 1224, + "clauses": 3864, + "dimacs_sha256": "4d22e96b474d380b040ae1bca68d75a6b6c9291a9b485d58d4161eada090dd26", + "role": "control", + "used": true, + "note": "decoded pattern re-checked independently: rank 10, 0 violations, 40 diagonal entries, 240 forced zeros" + }, + { + "id": "k5_k3_r16_sb", + "instance": "k5", + "k": 3, + "rank": 16, + "symmetry_breaking": true, + "result": "UNSAT", + "kissat_seconds": 0.6, + "variables": 5790, + "clauses": 19430, + "dimacs_sha256": "2f32a3b823d67439d2cee15f61ae09d8d66757dfc9d13973ec27d1849ff34236", + "used": true + }, + { + "id": "k5_k3_r17_sb", + "instance": "k5", + "k": 3, + "rank": 17, + "symmetry_breaking": true, + "result": "UNSAT", + "kissat_seconds": 57.2, + "variables": 7170, + "clauses": 24100, + "dimacs_sha256": "1864aa9e79067219fb18fdd5a667c0a88b2359d814f74f496022083617d92836", + "used": true + }, + { + "id": "k5_k3_r18_sb", + "instance": "k5", + "k": 3, + "rank": 18, + "symmetry_breaking": true, + "result": "SAT", + "kissat_seconds": 689.7, + "variables": 8550, + "clauses": 28770, + "dimacs_sha256": "0577927916b3fc4aaaaca89f11c11381e6548ac86600dc6ab5ef52b187c79db3", + "role": "control", + "used": true, + "note": "decoded pattern re-checked independently: rank 18, 0 violations, 135 diagonal entries, 1260 forced zeros" + }, + { + "id": "witness14_k2_r17", + "instance": "witness14", + "k": 2, + "rank": 17, + "symmetry_breaking": false, + "result": "SAT", + "kissat_seconds": null, + "variables": 776, + "clauses": 2352, + "dimacs_sha256": "a2d0b92434db804eafb94816b37e183ebbbbfba695e9da61511f3c963d123d77", + "role": "control", + "used": true, + "note": "the encoder finds a pattern; decoded pattern re-checked independently: rank 17, 0 violations, 600 forced zeros, 56 diagonal entries; the recorded 14-port witness itself, planted as unit clauses, is also SAT; a mutant (one port given a coordinate of an orthogonal port) is rejected by the independent checker with 2 violations" + }, + { + "id": "k8_k6_r53_sb", + "instance": "k8_30ports", + "k": 6, + "rank": 53, + "symmetry_breaking": true, + "result": "UNKNOWN", + "kissat_seconds": 1200.0, + "variables": 186312, + "clauses": 651094, + "dimacs_sha256": "3ef31e7e4c5aa85ecb69ed4110e5d9b65b2e0c53efaf59dec95095a800e99a4b", + "used": false, + "note": "undecided at the 20-minute cap; not used" + }, + { + "id": "k8_k6_r54_sb_control", + "instance": "k8_30ports", + "k": 6, + "rank": 54, + "symmetry_breaking": true, + "result": "UNKNOWN", + "kissat_seconds": 1200.0, + "variables": 202824, + "clauses": 708600, + "dimacs_sha256": "54783e6a8b2ad1ef9a1406e21abfa3557fc085b5ec706dfdca20f35f18470834", + "role": "control", + "used": false, + "note": "the same-size feasible control (Gram tensor I_6) is also undecided at the cap, so the k=6 runs carry no information" + }, + { + "id": "k8_k6_r53_nosb", + "instance": "k8_30ports", + "k": 6, + "rank": 53, + "symmetry_breaking": false, + "result": "UNKNOWN", + "kissat_seconds": null, + "variables": 181824, + "clauses": 624672, + "dimacs_sha256": "0c6c62c86a9101926415cb92f2f0f15cb9812301f04e363bf94c0dcaa1436b52", + "used": false, + "note": "run without symmetry breaking; recorded as undecided at the 20-minute cap (no solver output file kept); not used" + }, + { + "id": "k8_k6_r54_nosb_control", + "instance": "k8_30ports", + "k": 6, + "rank": 54, + "symmetry_breaking": false, + "result": "UNKNOWN", + "kissat_seconds": 1200.0, + "variables": 198072, + "clauses": 680616, + "dimacs_sha256": "8b2704bafaf76b09508e4d8c92d444738ef249640d6147ae2d369831f094c026", + "role": "control", + "used": false, + "note": "undecided at the cap; not used" + } + ] +} \ No newline at end of file diff --git a/research/p104-port-window-nine/data/witness14.json b/research/p104-port-window-nine/data/witness14.json new file mode 100644 index 0000000000..6b9714bfca --- /dev/null +++ b/research/p104-port-window-nine/data/witness14.json @@ -0,0 +1,81 @@ +{ + "description": "A representation with k = 2 and inner dimension 17 on a 14-port subset of P104. Ports are given by index into ports_p104.json. K is an orthogonal 8-set; 'others' are six ports with exactly two odd neighbours in K. coords[t] lists the two coordinates (of 17) that the rows of W_t and U_t occupy: W_t = U_t has rows e_a and e_b for coords[t] = [a, b], so B_ST is the matrix of coordinate overlaps. Coordinates 2i, 2i+1 are the block of the i-th element of K; coordinate 16 is the one extra coordinate.", + "k": 2, + "inner_dim": 17, + "K": [ + 62, + 63, + 69, + 74, + 81, + 86, + 91, + 99 + ], + "others": [ + 57, + 67, + 68, + 95, + 100, + 101 + ], + "coords": { + "57": [ + 12, + 13 + ], + "62": [ + 0, + 1 + ], + "63": [ + 2, + 3 + ], + "67": [ + 14, + 15 + ], + "68": [ + 0, + 16 + ], + "69": [ + 4, + 5 + ], + "74": [ + 6, + 7 + ], + "81": [ + 8, + 9 + ], + "86": [ + 10, + 11 + ], + "91": [ + 12, + 13 + ], + "95": [ + 1, + 3 + ], + "99": [ + 14, + 15 + ], + "100": [ + 4, + 5 + ], + "101": [ + 16, + 2 + ] + } +} \ No newline at end of file