diff --git a/research/p104-e8-rank8-closure/LICENSE b/research/p104-e8-rank8-closure/LICENSE new file mode 100644 index 0000000000..261eeb9e9f --- /dev/null +++ b/research/p104-e8-rank8-closure/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-e8-rank8-closure/NOTICE b/research/p104-e8-rank8-closure/NOTICE new file mode 100644 index 0000000000..31a66f368c --- /dev/null +++ b/research/p104-e8-rank8-closure/NOTICE @@ -0,0 +1,5 @@ +Closure of the E8 line system under the complex label pattern: no 97 of the 120 E8 lines have a rank-8k realisation (no new kappa). +Prepared by DreamingOfClouds with Claude Opus 5.5 (Anthropic), via Claude Code. Apache-2.0. + +The 120 E8 lines are generated from coordinates by check.py; the package reads and copies nothing from the repository. +retained/local-lemma.drat.xz is the DRAT proof of the local SAT instance that check.py regenerates and pins by sha256. diff --git a/research/p104-e8-rank8-closure/PR_BODY.md b/research/p104-e8-rank8-closure/PR_BODY.md new file mode 100644 index 0000000000..c64f169f81 --- /dev/null +++ b/research/p104-e8-rank8-closure/PR_BODY.md @@ -0,0 +1,25 @@ +Title: Prove no subset of ≥97 E8 lines has a rank-8 complex realisation (minimum hitting set 24, spectral + local certificate; no κ) + +No κ claim. This adds `research/p104-e8-rank8-closure/`, a registered research package for the card `p104-side-correction`. It extends the 14-port +Hall obstruction of #6846 from the 104 ports of one word to every subset of the 120 E8 lines. + +**Result.** Assume the complex label pattern of #6846: each line `T` carries `k × d` label matrices `U_T, W_T` over a field, the pairing `W_S U_T^T` +vanishes on every non-orthogonal pair of lines, and every diagonal block is invertible. Then no set of 97 or more of the 120 E8 lines has a +realisation of inner dimension exactly `8k`, over any field. The minimum number of lines meeting every member of the 13-line witness family is exactly 24 +(the family has 1,209,600 members: an 8-clique of the forced-zero graph plus five pair lines on four of its coordinates, each Hall-deficient with `lam <= 4/5`). + +**Proof.** (1) The forced-zero graph is SRG(120,56,28,24) and `M = 2A + 8I − J` satisfies `M² = 24M`, so any 23-line set contains at least 87 forced-zero +edges. (2) A local lemma at one line (a CNF with 998 variables whose unsatisfiability is certified by a DRAT proof that `drat-trim` verifies) says that a hitting set of at +most 23 lines that avoids a line `x` contains at least 12 of `x`'s 56 neighbours; nine E8 reflections carry it to every line, and a direct run at each of the 120 lines agrees. +(3) Counting edges between a 23-line hitting set and its 97 complement lines gives `97·12 = 1164 > 56·23 − 2·87 = 1114`. A 24-line set meets every witness with equality in both bounds, so 24 is exact. + +**Checks.** `check.py` (standard library, about a minute) regenerates the lines, the graph, the spectral identity, all 1,209,600 witnesses with a Hall-deficiency test on +each instance (sha256 pinned), a `k = 1` exhaustive control over F2 and F3, the reflections, the local CNF (sha256 pinned) and the retained proof (sha256 pinned), the counting inequality and the +24-line set. `./verify.sh --drat` also runs `drat-trim` on the retained proof (`s VERIFIED`). + +**Scope.** The label pattern is a hypothesis. Only subsets of the 120 E8 lines with this mask are covered; ranks strictly between `8k` and `9k`, other masks, +and sets of at most 96 lines are not covered (a 96-line set avoiding the family exists). Nothing is priced. Open questions are listed in the package. + +Prepared by DreamingOfClouds with Claude Opus 5.5 (Anthropic), via Claude Code. + +🤖 Generated with [Claude Code](https://claude.com/claude-code) diff --git a/research/p104-e8-rank8-closure/README.md b/research/p104-e8-rank8-closure/README.md new file mode 100644 index 0000000000..bb5b6d3449 --- /dev/null +++ b/research/p104-e8-rank8-closure/README.md @@ -0,0 +1,87 @@ +# No subset of 97 or more E8 lines has a rank-8k complex realisation (no κ) + +**No new κ.** This package proves that, under a stated label pattern, no set of 97 or more of the 120 E8 lines has a realisation of inner +dimension exactly `8k`, over any field. The obstruction is the 14-port Hall deficiency of #6846 in a 13-line form, and the minimum number of +lines that meets every such configuration is exactly 24. + +## Statement + +**Hypothesis (complex label pattern; the one of #6846).** Let `S` be a set of the 120 E8 lines (one line per pair `±r` of roots). Each `T` in +`S` carries a pair of `k × d` matrices `U_T, W_T` over a field `F` (`k >= 1`), and the pairing `B_ST = W_S U_T^T` (`k × k`) satisfies + +* `B_ST = 0` for every pair `S != T` that is **non-orthogonal** (the "forced-zero" pairs: `|| = 1` for roots of norm 2); +* `B_TT` invertible for every `T`. + +`W != U` is allowed. The pattern is an assumption about how the pairing of labels is constrained at frame contacts; it is not proved here +for any word. + +**Theorem.** If `|S| >= 97` there is no realisation of inner dimension `d = 8k`, over any field, for any `k >= 1`. +Equivalently: every set of 97 lines contains one of `F13`, 1,209,600 specific 13-line sets, each of which is Hall-deficient; and the minimum +hitting set of `F13` has exactly 24 lines (so 96 lines can avoid `F13`, and nothing is claimed about them). + +**Scope.** Subsets of the 120 E8 lines with this mask only. Ranks `8k < d < 9k` (`k >= 2`), other masks, line systems that are not subsets +of the 120 lines, and any pricing are not covered. No claim is made for sets of at most 96 lines. + +## The 13-line obstruction + +The forced-zero graph `NO` on the 120 lines (adjacent = non-orthogonal) is strongly regular with parameters `(120, 56, 28, 24)`; its +clique number is 8 and it has 8,640 8-cliques. For a 8-clique `K` and a line `t` outside it, let `A(t)` be the members of `K` orthogonal +to `t` (not forced zero to `t`). Exactly one line has `A(t) = {a, b}` for each pair `{a, b}` that occurs. Take `C` a 4-subset of `K` +and `O` the five lines whose `A(t)` are five of the six pairs inside `C` (a K4 minus an edge). The 13-line set `K ∪ O` is a witness; +`F13` is the family of all of them. Two lines of `O` that share a coordinate of `C` are forced zero and share exactly that one coordinate. + +**Hall deficiency (the argument of #6846 with six lines on five coordinates replaced by five lines on four).** Suppose `K ∪ O ⊆ S` has a +realisation with `d = 8k`. + +1. *Gauge.* `K` is a forced-zero clique, so `B_KK` is block diagonal with invertible blocks and has rank `8k`; as `B_KK = W_K U_K^T` with both + factors `8k × 8k`, both are invertible. Replacing `U` by `U g`, `W` by `W h` with `g = U_K^{-1}`, `h = g^{-T}` leaves the pairing unchanged and gives `U_K = I`, `W_K = B_KK`; + multiplying each block row of `W_K` on the left by `B_kk^{-1}` keeps every zero block and every invertible diagonal block, so `U_K = W_K = I`. +2. *Support.* `B_{kT} = U_T[k]^T` and `B_{Tk} = W_T[k]`, so a forced-zero pair `(T, k)` gives `U_T[k] = W_T[k] = 0`; both are supported on `A(T)`. +3. *Block diagonal products.* Fix `c` in `C` and `O_c = {T in O : c in A(T)}`. Two distinct members of `O_c` are forced zero and share only `c`, so + `W_S[c] U_T[c]^T = 0`. The stacks `X = (W_T[c])` and `Y = (U_T[c])` over `O_c` give a block-diagonal `X Y^T` of rank at most `k`, so + `sum_{T in O_c} rank(W_T[c] U_T[c]^T) <= k`. +4. *Rank sum.* `B_TT = sum_{c in A(T)} W_T[c] U_T[c]^T` is invertible, so `sum_c rank(W_T[c] U_T[c]^T) >= k`. Summing over the five lines of `O`: + `5k <= sum_{c in C} sum_{T in O_c} rank(...) <= 4k`. Contradiction. + +For `k = 1` this is pigeonhole: five lines each need a coordinate where both entries are non-zero, no coordinate serves two of them, and `C` has four. +In the Hall (fractional matching) form the demand per line is `lam <= 4/5 < 1`. + +## Every 97-line set contains a witness + +Let `D` be a set of lines meeting every member of `F13`, and suppose `|D| <= 23`. + +1. **Spectral inequality (exact).** With `A` the adjacency matrix of `NO`, `A^2 = 32 I + 4 A + 24 J`, so `M = 2A + 8I - J` satisfies + `M^2 = 24 M` (checked entrywise). Hence `u^T M u = |Mu|^2 / 24 >= 0` for every vector `u`. For the indicator of any `k`-set `D`, `u^T A u = 2 e(D)`, so + `4 e(D) + 8k - k^2 >= 0`, i.e. `e(D) >= (k^2 - 8k)/4` for every `k`-set (not only for sets that hit anything). For `k = 23`: `e(D) >= 87`. +2. **Local lemma (SAT, DRAT).** Fix a line `x`, write `N(x)` for its 56 forced-zero neighbours. *There is no set `D` with `x` not in `D`, meeting + `w \ {x}` for every `w` in `F13` containing `x`, with `|D| <= 23` and `|D ∩ N(x)| <= 11`.* For `x = 0` this is a CNF with 998 variables and + 136,295 clauses (`retained/local-lemma.drat.xz` is a DRAT proof of its unsatisfiability; `check.py` regenerates the CNF and pins both by sha256). + Nine reflections in E8 roots preserve `NO`, hence the family `F13`, which is defined from `NO` alone, and move line 0 to every line, so the lemma + holds at every `x`. (The same instance was also solved directly at every one of the 120 lines, with no symmetry, and is unsatisfiable at each.) +3. **Count.** Enlarge `D` to exactly 23 lines and let `S` be its 97 complement lines. By step 2 each `x` in `S` has `|N(x) ∩ D| >= 12`. Counting + `NO`-edges between `S` and `D` two ways: + `97 * 12 = 1164 <= sum_{x in S} |N(x) ∩ D| = sum_{d in D} (56 - deg_D(d)) = 56*23 - 2 e(D) <= 1288 - 174 = 1114`. Contradiction. + +So every hitting set of `F13` has at least 24 lines. **Tightness.** The 24-line set printed in `check.py` (the nonsingular points of the perpendicular of a +totally singular 2-space of `E8/2E8`) meets every witness, has `e = 96 = (24^2 - 8*24)/4`, and sees exactly 12 of its lines from every outside line, so the minimum is exactly 24 and the +theorem is sharp for this family. + +## What `check.py` verifies (about one minute, standard library) + +* the 120 lines from coordinates; `NO` is SRG(120,56,28,24); `M^2 = 24 M`; +* all 1,209,600 witnesses, each instance passing the Hall-deficiency test (five lines supported on four coordinates, sharing pairs forced zero with one common coordinate); the family sha256; +* `k = 1` exhaustive search over `F_2` and `F_3` on sampled witnesses (the gauge-fixed system has no solution) and a control with one `O` line removed (solvable); +* the nine reflections preserve `NO` and have a transitive orbit on line 0; +* the local CNF at line 0 regenerated and compared with its sha256; the proof file compared with its sha256; +* `97*12 > 56*23 - 2*87`; the 24-line set meets all witnesses and has 96 internal edges. + +`./verify.sh --drat` additionally decompresses the proof and runs `drat-trim` (not part of the standard library; set `DRAT_TRIM` or put it on `PATH`); it reports `s VERIFIED`. +The CNF is satisfiable if either bound is relaxed (`|D| <= 23` with `|D ∩ N(0)| <= 14`, or `|D| <= 24` with `|D ∩ N(0)| <= 12`), so the bounds are not vacuous. + +## Open next questions + +1. **Sets of 96 lines.** Is there a rank-`8k` realisation of some 96-line set that avoids `F13`, for instance the complement of the 24-line extremal set? A realisation would make 96 sharp for realisability; a further obstruction would lower it. +2. **Ranks strictly between `8k` and `9k`** (`k >= 2`). The gauge needs `d = 8k`; with a free extra column the rank sum may or may not close. +3. **Break a forced zero.** Which mechanism forces the pairing to vanish on non-orthogonal pairs, and can a contact be routed through a paid helper so that one forced zero inside every `F13` witness is broken? + +See `TASK.json` for first steps and blockers. Credit: DreamingOfClouds. diff --git a/research/p104-e8-rank8-closure/SOURCES.json b/research/p104-e8-rank8-closure/SOURCES.json new file mode 100644 index 0000000000..e1996ec143 --- /dev/null +++ b/research/p104-e8-rank8-closure/SOURCES.json @@ -0,0 +1,31 @@ +{ + "schema_version": 1, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "files": [ + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "docs/research/research-family-status.md", + "usage": "provenance", + "git_blob": "3c19b18ef7225b47f0abcd9d51ae7c83d0cdfd15", + "sha256": "92c8010dfd9fc33e921f70526231f8689e06ea784f1b1387d895344b227f36d7" + }, + { + "path": "docs/research/current-priorities.md", + "usage": "provenance", + "git_blob": "6f5d40d13d8f3bdc12ce7954c8c3eb4ab1f8be91", + "sha256": "70f61c8d140ae6e892f2b8f065bba4eae3e76f7a8f55f632fd4e2f9f34039bdc" + }, + { + "path": "research/p104-designer-toolkit-v2/P104-LEMMAS.md", + "usage": "provenance", + "git_blob": "129f28dd10c9e1c43d29a9dd280e022070288a73", + "sha256": "54263ecdcabb067b1f77749ae60cb1f430c02fd720b63e5e39f358f6bfee78ec" + } + ], + "source_availability": "Every listed file is a blob of the base commit and is provenance only; check.py reads no repository file (the 120 E8 lines are generated from coordinates)." +} diff --git a/research/p104-e8-rank8-closure/TASK.json b/research/p104-e8-rank8-closure/TASK.json new file mode 100644 index 0000000000..cdf0826152 --- /dev/null +++ b/research/p104-e8-rank8-closure/TASK.json @@ -0,0 +1,135 @@ +{ + "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": "Prove that no set of 97 or more of the 120 E8 lines has a realisation of inner dimension exactly 8k under the complex label pattern (the pairing between line labels is forced zero exactly on non-orthogonal line pairs, with invertible diagonal blocks, stated as a hypothesis), over any field and for symmetric or asymmetric pairings. The obstruction is a 13-line Hall deficiency (an 8-clique of the forced-zero graph plus five pair lines on four of its coordinates); the minimum set of lines meeting every such configuration has exactly 24 lines. Ranks strictly between 8k and 9k for k >= 2, other masks, and line systems that are not subsets of the 120 E8 lines are not covered.", + "scope_change_reason": "The card asks for a helper-basis and causal-split construction on the complete invoice. This package is a rank obstruction for one label pattern on subsets of the 120 E8 lines; it constructs no word, prices nothing and splits nothing. It limits how many E8 lines a rank-8k route under that pattern can use.", + "bottleneck_link": "docs/research/research-family-status.md; the statement caps at 96 the number of E8 lines that any complete-invoice construction whose labels follow the stated pattern can carry at inner dimension 8k, so a construction needing 97 or more of them has to pay the next rank or change the pattern.", + "stop_rule": "No kappa claim. The theorem is conditional on the complex label pattern, which is a hypothesis about how labels pair, not something proved here for any word; it says nothing for ranks strictly between 8k and 9k when k >= 2, for other masks, for line systems outside the 120 E8 lines, or for any pricing of a word. The bound 96 is not claimed attainable.", + "evidence": "README.md (statement and self-contained proof), check.py (exact checks: strongly regular graph and spectral identity, the 13-line family with a Hall-deficiency test on every instance, reflections, the local SAT instance pinned by hash, counting, an explicit 24-line hitting set), retained/local-lemma.drat.xz (DRAT proof of the local instance).", + "author": "DreamingOfClouds", + "ai_assistance": "Prepared by DreamingOfClouds with Claude Opus 5.5 (Anthropic), via Claude Code.", + "outcome": "completed", + "open_questions": [ + { + "question": "Is there a rank-8k realisation, under the same pattern, of some set of exactly 96 E8 lines, for instance the complement of the 24-line extremal hitting set?", + "why_it_matters": "The theorem leaves 96 as the largest line count not excluded; a realisation would show the bound is sharp for realisability, and a further obstruction would lower it below the 97 that a 104-line construction would need anyway.", + "first_step": "Take the 96 lines outside the 24-line set listed in check.py (the complement of the nonsingular points of a totally singular 2-space's perpendicular), confirm it contains no F13 witness, and run the gauge-fixed k = 1 search over F_2 for that line set by fixing an 8-clique inside it and solving the remaining 88 lines' support systems with a SAT solver.", + "blocked_by": "None for the k = 1 search; no encoding of the full 96-line system has been written, and the Hall counting that closes F13 is not known to extend to a complete obstruction for larger configurations." + }, + { + "question": "Do ranks strictly between 8k and 9k (k >= 2) admit a realisation of 97 or more E8 lines under the same pattern?", + "why_it_matters": "The proof needs the gauge U_K = W_K = I, which exists only at inner dimension exactly 8k; a fractional saving per label block would be a different route from rank 9.", + "first_step": "For k = 2 and inner dimension 17, redo the gauge with one free extra column for one F13 witness (13 lines) and decide the resulting rank system over F_2 by exact linear algebra.", + "blocked_by": "The gauge needs invertible U_K, W_K, which holds only at inner dimension exactly 8k; the rank-sum argument has to be rewritten with an extra column." + }, + { + "question": "Which mechanism in a complex supplier forces the pairing to vanish on every non-orthogonal line pair, and can one forced zero inside each F13 witness be broken by a paid helper?", + "why_it_matters": "The theorem is only as strong as the label pattern; a route at rank 8k has to break a forced zero inside every one of the 1,209,600 witnesses, and the minimum number of lines that meets all of them is 24.", + "first_step": "For one witness, list the frame contacts that produce the five O-line zeros with the K lines and the 8 sharing pairs, then remove one sharing pair from the mask and record by the k = 1 search in check.py whether the system becomes satisfiable.", + "blocked_by": "The derivation of the pattern from the supplier rules has not been written as a statement; without it a mask change cannot be priced." + } + ], + "research_context": { + "sources": [ + "research/p104-rank8-hall-obstruction/README.md (the 14-port Hall obstruction this package generalises; pending as #6846 at the time of writing, so the argument is re-derived here)", + "research/p104-designer-toolkit-v2/P104-LEMMAS.md (arena and the related rank-8 statement for a different mask)" + ], + "credit": "DreamingOfClouds." + }, + "selected_frontier_changed": false +} diff --git a/research/p104-e8-rank8-closure/VERIFY.json b/research/p104-e8-rank8-closure/VERIFY.json new file mode 100644 index 0000000000..e770a11038 --- /dev/null +++ b/research/p104-e8-rank8-closure/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": 120, + "checks": "From the 120 E8 lines generated from coordinates: SRG(120,56,28,24) and (2A+8I-J)^2 = 24(2A+8I-J); all 1,209,600 13-line witnesses (8-clique plus K4-minus-an-edge of pair lines on four of its coordinates), each passing the Hall-deficiency test with the family sha256 pinned; an exhaustive k = 1 search over F_2 and F_3 on sampled witnesses (no solution) with a one-line-removed control; nine reflections preserving the graph and moving line 0 to all 120 lines; regeneration of the local SAT instance pinned by sha256 and the retained proof pinned by sha256; the counting inequality 97*12 > 56*23 - 2*87; and an explicit 24-line set meeting every witness." + } + ] +} diff --git a/research/p104-e8-rank8-closure/check.py b/research/p104-e8-rank8-closure/check.py new file mode 100755 index 0000000000..e072fad67d --- /dev/null +++ b/research/p104-e8-rank8-closure/check.py @@ -0,0 +1,235 @@ +#!/usr/bin/env python3 +"""Exact checks for: every set of >= 97 of the 120 E8 lines contains an F13 witness (a Hall-deficient 13-line +configuration), so no such set has a rank-8k realisation under the complex label pattern. Standard library only. + + python3.12 -I -B check.py # all steps (about 1 minute); the SAT proof is pinned by hash but not re-run + python3.12 -I -B check.py --drat # additionally decompress retained/local-lemma.drat.xz and run drat-trim + # (drat-trim on PATH or in $DRAT_TRIM) +Steps + 1 lines, forced-zero graph NO (non-orthogonal pairs), SRG(120,56,28,24), (2A+8I-J)^2 = 24(2A+8I-J) + 2 F13: all witnesses K u O built from the graph; every instance passes the Hall-deficiency test; k = 1 exhaustive control + 3 symmetry: 9 reflections preserve NO (F13 is defined from NO alone) and move line 0 to every line + 4 local lemma CNF at line 0, regenerated and pinned by sha256; proof pinned by sha256 + 5 counting; tightness: an explicit 24-line hitting set +""" +import sys, os, itertools, hashlib, random, lzma, subprocess, shutil, tempfile +HERE = os.path.dirname(os.path.abspath(__file__)) +CNF_SHA = '987af2501ed8c602b9d4e3606f0ab1c5888b9e860b726606a40ebc922545610f' +DRAT_SHA = 'fea6c9f3933039cd85c054146b2fb8b19bdecc716a627de0edaea480288db192' +F13_SHA = '86e9b8b48f053ec6dbbc26e2f75cd489bc51b8a1879ac187d7d3bf17cb43f838' +D24 = [0, 1, 2, 3, 12, 13, 14, 15, 24, 25, 34, 35, 36, 37, 38, 39, 40, 41, 44, 45, 46, 47, 50, 51] +KB, AMAX = 23, 11 # |D| <= 23 and |D cap N(0)| <= 11 in the local lemma + + +def ip(a, b): return sum(x * y for x, y in zip(a, b)) + + +def e8_lines(): + roots = [] + for i, j in itertools.combinations(range(8), 2): + for a in (2, -2): + for b in (2, -2): + v = [0] * 8; v[i] = a; v[j] = b; roots.append(tuple(v)) + for s in itertools.product((1, -1), repeat=8): + if s.count(-1) % 2 == 0: roots.append(s) # coordinates doubled: roots have norm 8 + assert len(roots) == 240 and all(ip(r, r) == 8 for r in roots) + seen, L = set(), [] + for r in roots: + if r in seen: continue + seen.add(r); seen.add(tuple(-x for x in r)); L.append(r) + assert len(L) == 120 + return L + + +def step1(L): + n = len(L) + NO = [[i != j and ip(L[i], L[j]) != 0 for j in range(n)] for i in range(n)] + assert all(ip(L[i], L[j]) in (0, 4, -4) for i in range(n) for j in range(n) if i != j) + assert all(sum(r) == 56 for r in NO) + nb = [sum(1 << j for j in range(n) if NO[i][j]) for i in range(n)] + for i in range(n): + for j in range(n): + if i != j: assert bin(nb[i] & nb[j]).count('1') == (28 if NO[i][j] else 24) + M = [[2 * NO[i][j] + (8 if i == j else 0) - 1 for j in range(n)] for i in range(n)] + cols = list(zip(*M)) + for i in range(n): + for j in range(n): + assert sum(a * b for a, b in zip(M[i], cols[j])) == 24 * M[i][j] + print('step1: SRG(120,56,28,24); M=2A+8I-J satisfies M^2=24M, so M is 24 times a projection (rank %d)' % (sum(M[i][i] for i in range(n)) // 24)) + return NO, nb + + +def build_f13(n, NO, nb): + cliques = [] + def rec(cur, cand): + if len(cur) == 8: cliques.append(tuple(cur)); return + while cand: + v = (cand & -cand).bit_length() - 1; cand &= cand - 1 + rec(cur + [v], cand & nb[v]) + rec([], (1 << n) - 1) + assert len(cliques) == 8640 + fam = {}; inst = 0 + for K in cliques: + Ks = set(K) + A = {t: tuple(c for c in K if not NO[t][c]) for t in range(n) if t not in Ks} + pl = {} + for t, a in A.items(): + if len(a) == 2: pl.setdefault(a, []).append(t) + assert all(len(v) == 1 for v in pl.values()) # at most one line per pair of K-coordinates + for C in itertools.combinations(K, 4): + ps = list(itertools.combinations(C, 2)) + for drop in range(6): # O = K4-minus-an-edge of pair lines on C + if any(p not in pl for p in ps): break + O = [pl[p][0] for k, p in enumerate(ps) if k != drop] + # Hall-deficiency test: |O| = 5 lines, supports A(t) inside the 4 coordinates of C, so at most 4k rank + assert len(O) == 5 and len(set(O)) == 5 and not (set(O) & Ks) + assert set().union(*[set(A[t]) for t in O]) <= set(C) and len(C) == 4 + for c in C: # lines of O sharing a coordinate are forced zero + g = [t for t in O if c in A[t]] + assert all(NO[s][t] for s, t in itertools.combinations(g, 2)) + for s, t in itertools.combinations(O, 2): # and share exactly one coordinate + assert len(set(A[s]) & set(A[t])) <= 1 + inst += 1 + fam[frozenset(K) | frozenset(O)] = (K, tuple(O), tuple(C)) + return fam, inst + + +def k1_control(fam, NO, seed=3, count=8): + """k = 1, gauge U_K = W_K = I. Line t of O carries W_t[c], U_t[c] on A(t) only (zero on the other K lines, since + forced zero), needs W_t.U_t != 0, and forced-zero pairs need W_s[c]U_t[c] = 0 = W_t[c]U_s[c] on shared c.""" + rnd = random.Random(seed) + keys = sorted(fam, key=lambda w: sorted(w)) + for w in rnd.sample(keys, count): + K, O, C = fam[w] + A = {t: tuple(c for c in K if not NO[t][c]) for t in O} + for p in (2, 3): + for drop in (None, O[0]): + Os = [t for t in O if t != drop] + states = {} + for t in Os: + cs = A[t]; st = [] + for v in itertools.product(range(p), repeat=4): + W = {cs[0]: v[0], cs[1]: v[1]}; U = {cs[0]: v[2], cs[1]: v[3]} + if sum(W[c] * U[c] for c in cs) % p: st.append((W, U)) + states[t] = st + asg = {} + def rec(i): + if i == len(Os): return True + t = Os[i] + for W, U in states[t]: + if all(not NO[t][s] or (not sum(W[c] * Us[c] for c in set(W) & set(Ws)) % p + and not sum(Ws[c] * U[c] for c in set(W) & set(Ws)) % p) + for s, (Ws, Us) in asg.items()): + asg[t] = (W, U) + if rec(i + 1): return True + del asg[t] + return False + found = rec(0) + assert found == (drop is not None), (p, drop) + print('step2b: k=1 exhaustive search over F_2, F_3 on %d witnesses: no solution; with one O line removed: solution' % count) + + +def step3(L, NO, fam): + n = len(L); idx = {} + for t, r in enumerate(L): idx[r] = t; idx[tuple(-x for x in r)] = t + def refl(r): # s_r(x) = x - (x.r/4) r on doubled coordinates + return tuple(idx[tuple(a - (ip(L[t], r) // 4) * b for a, b in zip(L[t], r))] for t in range(n)) + gens, orb = [], {0} + for r in L: + g = refl(r); new = set(orb); st = list(orb) + while st: + a = st.pop() + for h in gens + [g]: + b = h[a] + if b not in new: new.add(b); st.append(b) + if len(new) > len(orb): gens.append(g); orb = new + if len(orb) == n: break + assert len(orb) == n + for g in gens: + assert sorted(g) == list(range(n)) + assert all(NO[g[i]][g[j]] == NO[i][j] for i in range(n) for j in range(n)) + # F13 is defined from NO alone, so it is invariant under any automorphism of NO; also checked on a sample + keys = sorted(fam, key=lambda w: sorted(w)); rnd = random.Random(9) + for w in rnd.sample(keys, 3000): + for g in gens: assert frozenset(g[i] for i in w) in fam + print('step3: %d reflections preserve NO (and F13 on a 3000-set sample); orbit of line 0 = all 120 lines' % len(gens)) + + +def local_cnf(n, NO, fam, x=0, K=KB, A=AMAX): + W = sorted(sorted(i for i in w if i != x) for w in fam if x in w) + items = [i for i in range(n) if i != x]; vid = {i: t + 1 for t, i in enumerate(items)} + cl = [[vid[i] for i in w] for w in W]; nv = len(items) + def totalizer(lits, k): + nonlocal nv + def build(ls): + nonlocal nv + if len(ls) == 1: return [ls[0]] + m = len(ls) // 2; a = build(ls[:m]); b = build(ls[m:]) + cap = min(len(ls), k + 1); out = [] + for _ in range(cap): nv += 1; out.append(nv) + for i in range(len(a) + 1): + for j in range(len(b) + 1): + s = i + j + if s == 0: continue + c = [out[min(s, cap) - 1]] + if i > 0: c.append(-a[i - 1]) + if j > 0: c.append(-b[j - 1]) + cl.append(c) + return out + o = build(lits) + if len(o) > k: cl.append([-o[k]]) + totalizer([vid[i] for i in items], K) + Nx = [vid[i] for i in items if NO[x][i]]; assert len(Nx) == 56 + totalizer(Nx, A) + return len(W), nv, cl + + +def cnf_bytes(nv, cl): + return ('p cnf %d %d\n' % (nv, len(cl)) + ''.join(' '.join(map(str, c)) + ' 0\n' for c in cl)).encode() + + +def e_in(D, NO): return sum(1 for a, b in itertools.combinations(D, 2) if NO[a][b]) + + +def main(): + L = e8_lines(); n = 120 + NO, nb = step1(L) + fam, inst = build_f13(n, NO, nb) + h = hashlib.sha256() + for w in sorted(sorted(x) for x in fam): h.update((','.join(map(str, w)) + '\n').encode()) + print('step2: %d (K,O) instances, %d distinct 13-line sets, each passes the Hall-deficiency test (5 lines on 4 coordinates); sha256 %s' % (inst, len(fam), h.hexdigest())) + assert len(fam) == 1209600 and h.hexdigest() == F13_SHA + k1_control(fam, NO) + step3(L, NO, fam) + nW, nv, cl = local_cnf(n, NO, fam) + data = cnf_bytes(nv, cl); sha = hashlib.sha256(data).hexdigest() + print('step4: local CNF at line 0: %d witnesses through it, %d variables, %d clauses, sha256 %s' % (nW, nv, len(cl), sha)) + assert nW == 131040 and sha == CNF_SHA + pf = os.path.join(HERE, 'retained', 'local-lemma.drat.xz') + if os.path.exists(pf): + proof = lzma.decompress(open(pf, 'rb').read()); assert hashlib.sha256(proof).hexdigest() == DRAT_SHA + print('step4: retained proof matches its pinned sha256 (%d bytes)' % len(proof)) + if '--drat' in sys.argv: + dt = os.environ.get('DRAT_TRIM') or shutil.which('drat-trim'); assert dt, 'drat-trim not found' + with tempfile.TemporaryDirectory() as td: + a, b = os.path.join(td, 'l.cnf'), os.path.join(td, 'l.drat') + open(a, 'wb').write(data); open(b, 'wb').write(proof) + r = subprocess.run([dt, a, b, '-t', '20000'], capture_output=True, text=True) + assert 's VERIFIED' in r.stdout, r.stdout[-400:] + print('step4: drat-trim: s VERIFIED (the CNF is unsatisfiable)') + else: + print('step4: retained proof missing') + assert False + # step 5 + emin = -((-(KB * KB - 8 * KB)) // 4); assert emin == 87 + lhs, rhs = 97 * (AMAX + 1), 56 * KB - 2 * emin + print('step5: 97*12 = %d > 56*23 - 2*87 = %d: no hitting set of F13 has <= 23 lines' % (lhs, rhs)); assert lhs > rhs + masks = [sum(1 << i for i in w) for w in fam]; dm = sum(1 << i for i in D24) + assert len(set(D24)) == 24 and all(m & dm for m in masks) + assert e_in(D24, NO) == 96 == (24 * 24 - 8 * 24) // 4 + print('step5: the 24-line set %s hits all %d witnesses (e = 96): minimum hitting set of F13 is exactly 24' % (D24, len(fam))) + print('THEOREM CHECKED: every set of >= 97 of the 120 E8 lines contains an F13 witness.') + + +if __name__ == '__main__': + main() diff --git a/research/p104-e8-rank8-closure/retained/local-lemma.drat.xz b/research/p104-e8-rank8-closure/retained/local-lemma.drat.xz new file mode 100644 index 0000000000..6883cea7e9 Binary files /dev/null and b/research/p104-e8-rank8-closure/retained/local-lemma.drat.xz differ diff --git a/research/p104-e8-rank8-closure/verify.sh b/research/p104-e8-rank8-closure/verify.sh new file mode 100755 index 0000000000..1f0bc898e7 --- /dev/null +++ b/research/p104-e8-rank8-closure/verify.sh @@ -0,0 +1,5 @@ +#!/bin/sh +# Runs the exact checks (about a minute); run from anywhere. Needs python3.12 (standard library only). +# Add --drat to also run drat-trim on the retained proof (drat-trim on PATH or in $DRAT_TRIM). +set -e +exec python3.12 -I -B "$(dirname "$0")/check.py" "$@"