diff --git a/research/p104-frame0-letter-sum/PROOF.md b/research/p104-frame0-letter-sum/PROOF.md new file mode 100644 index 0000000000..603ff2b9fa --- /dev/null +++ b/research/p104-frame0-letter-sum/PROOF.md @@ -0,0 +1,189 @@ +# No sum of letters hosts the frame-0 indicator + +No new κ. The selected record stays `781451/250000000`. This note answers the +sum question left open by PR #7031. It does not redo that product census, it +does not host another frame, and it does not name monomials on the selected +invoice. + +## 1. Hypotheses + +Ports, the odd graph, and the simple-root chart are those of PR #7031. Frame 0 +of the #7014 witness is the ordered 8-tuple + +```text +11, 21, 38, 56, 140, 146, 161, 191. +``` + +A **letter** `λ_i` is the root-line functional `j ↦ ( + 1) mod 2`. +In the chart every label has ninth coordinate 1, and the accepted identity +`S9(u_i, u_j) = ( + 1) mod 2` makes each letter an affine function + +```text +λ_i = 1 + (linear form in x0, ..., x7). +``` + +A **sum of letters** is an `F_2` linear combination of these 120 functions. +Repetitions cancel in pairs, so every sum is the sum of a set of distinct +letters. The sum **hosts** the row when its value is 1 on the eight frame +lines and 0 on the other 112 root lines. Agreement on the 104 P104 lines is +the weaker condition used below; it is already impossible. + +The charge of a word is the set of square-free monomials in its algebraic +normal form, in this fixed chart, with `x_i^2 = x_i`. As in #7031, a +**new** monomial is one of degree at least 2. The constant and the eight +variables are not new. + +Sums in `Z`, thresholds, and sums of products are outside these hypotheses. + +## 2. The explicit sum + +**Proposition.** The sum of four frame letters cancels: + +```text +λ_11 + λ_21 + λ_38 + λ_56 = 0. +``` + +The chart polynomials, recomputed from the labels, are + +```text +λ_11 = 1 + x1 + x2 + x4 + x5, +λ_21 = 1 + x0 + x1 + x2 + x4 + x5, +λ_38 = 1 + x0 + x1 + x2 + x4, +λ_56 = 1 + x1 + x2 + x4. +``` + +Each of `1, x0, x1, x2, x4, x5` occurs an even number of times (`4, 2, 4, 4, +4, 2`), and `x3, x6, x7` do not occur. The sum is the zero polynomial. Its +monomial list is empty, so it has **zero** new monomials. On every root line +the value is 0, including the eight frame lines, so the sum does not host +the row. + +The same direct count gives thirteen further cancelling fours inside the +frame, and the sum of all eight frame letters is zero as well. No nonempty +subset of the eight of size other than 4 or 8 cancels. Deleting any one +letter from `λ_11 + λ_21 + λ_38 + λ_56` leaves a nonzero affine function. +None of the 255 nonempty subset-sums of the eight frame letters hosts the +row. That 255-count is an exhaustive census of a finite domain. It is not a +census of sums that use a letter from outside the frame. + +One single letter has the same new-monomial count and also fails. For +example `λ_11` expands to `1, x1, x2, x4, x5` (zero new monomials). It equals +1 on all eight frame lines and also equals 1 on a line outside the frame. + +## 3. Every sum is affine, and none hosts + +**Theorem.** Under the hypotheses in §1, every sum of letters has algebraic +normal form of degree at most 1, hence has zero new monomials. No such sum +agrees with the frame-0 indicator on the 104 P104 lines. In particular, no +sum hosts the #7031 row on all 120 root lines, and no sum hosts that row +with fewer than 40 new monomials. + +The degree bound is the sum of affine functions. It does not use a search. +The zero new-monomial count is the same degree cut #7031 uses for the +product charge. Every sum would be strictly below 40 on that cut. The +obstruction is that none of them hosts. + +**Four-line parity.** Let `v(j) ∈ F_2^9` be the eight chart coordinates of +root line `j`, followed by a constant coordinate 1. For an affine function +`f(x) = c + Σ a_i x_i`, the sum of `f` over a set of lines equals the +`F_2` dot product of `(a, c)` with the sum of their vectors `v(j)`. The four +P104 ports `478, 11, 14, 475` have chart coordinates + +```text +478: (0, 0, 1, 1, 0, 0, 0, 0), +11: (0, 1, 0, 1, 1, 0, 0, 0), +14: (1, 1, 1, 1, 0, 1, 0, 1), +475: (1, 0, 0, 1, 1, 1, 0, 1). +``` + +Each coordinate appears an even number of times, and the four constant +coordinates sum to 0. Therefore `v(478) + v(11) + v(14) + v(475) = 0`, and +every affine function has value-sum 0 on these four lines. Any three of the +four vectors already sum to something nonzero, so the dependence has size +exactly 4. + +Port 11 is in the frame. Ports 478, 14 and 475 are in P104 and are not in +the frame. The indicator therefore takes values `0, 1, 0, 0` and has +value-sum 1. No affine function can match it on these four lines, hence +none matches it on all 104 P104 lines, hence none matches it on all 120 +root lines. + +A second four, also inside P104, gives the same contradiction. Ports +`21, 13, 493, 501` have coordinates + +```text +21: (0, 0, 1, 1, 1, 0, 0, 0), +13: (0, 1, 0, 1, 1, 1, 0, 0), +493: (0, 1, 1, 1, 1, 0, 0, 0), +501: (0, 0, 0, 1, 1, 1, 0, 0), +``` + +which sum to 0, while the indicator is 1 only at port 21. + +The cancelling frame sum of §2 is a dependence of the other kind. The +evaluation labels of ports `11, 21, 38, 56` also sum to 0, but all four +ports are in the frame, so the indicator sum is 0 as well. That relation +does not separate the indicator from the affine functions. Clearing the +frame membership of port 11 in the first four would likewise make the +indicator sum even, and that altered row would not be obstructed by this +particular four. + +## 4. Finite censuses + +These domains are finite, every element is visited, and the counts are +checked by `verify.py`. They are not samples. + +1. **Chart identity.** All `120 × 120` pairings match + `( + 1) mod 2`. Every letter has constant term 1, and the 120 + letter vectors in `F_2^9` are distinct and have rank 9. Subset sums of + the letters are therefore exactly the 512 affine functions. The census + of affine functions is the census of sums. + +2. **Distances.** Evaluated on the 120 root lines, the 512 affine functions + have Hamming distances + + ```text + 8, 48, 56, 64, 72, 112 + with multiplicities + 1, 7, 248, 248, 7, 1. + ``` + + The unique function at distance 8 is the zero polynomial, which is the + explicit sum of §2. It matches the 112 non-frame lines and misses the + eight frame lines. Every other sum misses at least 48 lines. On the 104 + P104 lines the distances are + + ```text + 8, 36, 44, 48, 52, 56, 60, 68, 96 + with multiplicities + 1, 3, 12, 199, 82, 199, 12, 3, 1. + ``` + + Again the minimum is 8 and is achieved only by zero. No affine function + hosts on either domain. + +3. **Short obstructions.** No subset of 1, 2, or 3 of the 120 root lines has + augmented-label sum 0. Exactly 7168 subsets of size 4 have augmented-label + sum 0 and indicator sum 1. Each of those 7168 meets the frame in exactly + one line. Exactly 4384 of them lie entirely in the 104 P104 lines. The + two fours of §3 are in that list. This is why a one-line, two-line, or + three-line witness cannot exist, and why size 4 is the minimum. + +4. **Short syzygies.** No set of 1, 2, or 3 distinct letters sums to the + zero function. Exactly 32130 sets of four letters do. The explicit sum + of §2 is one of them. The zero function is therefore achieved by a + nonempty sum, not only by the empty combination. + +5. **Frame-letter sums.** Of the 255 nonempty subset-sums of the eight + frame letters, 15 are the zero polynomial (14 fours and the full eight) + and none hosts the row. + +## 5. What this does not say + +The product in #7031 is not a sum. Its 40 new monomials remain a +product-hosting charge. This note does not prove that 40 is minimal for +sums of products, for a different chart, or for a circuit that is not an +`F_2` sum of letters. It does not prove that the indicator is non-affine +as a function on all of `F_2^8`; the obstruction is only on root lines. A +failed search outside this alphabet would not be a minimality proof. No +selected-invoice histogram is computed, and κ is unchanged. diff --git a/research/p104-frame0-letter-sum/README.md b/research/p104-frame0-letter-sum/README.md new file mode 100644 index 0000000000..2649a41fe2 --- /dev/null +++ b/research/p104-frame0-letter-sum/README.md @@ -0,0 +1,110 @@ +# No sum of letters hosts one P104 frame indicator + +**No new κ.** The selected frontier stays `781451/250000000`. This package +answers open question 2 of PR #7031: whether an `F_2` sum of root-line letters +can host frame 0 with fewer than 40 new monomials. It does not redo the +product hosting, it does not host frame 1, and it does not price the selected +invoice. + +## Result + +Frame 0 is the odd-graph clique `11, 21, 38, 56, 140, 146, 161, 191`. A letter +is one root-line pairing. In the inherited simple-root chart every letter is +affine of the form `1 + (linear form)`, so every `F_2` sum has degree at most +1. The new-monomial count, using the same degree cut as #7031, is therefore 0 +for every sum. + +The explicit sum of four frame letters cancels: + +```text +λ_11 + λ_21 + λ_38 + λ_56 = 0. +``` + +Its monomial list is empty: zero monomials of degree at most 1 and **zero** +new monomials. The value is 0 on every root line, so the sum misses all eight +frame lines and does not host the row. A single letter such as `λ_11` expands +to `1, x1, x2, x4, x5`, also with zero new monomials, and equals 1 outside the +frame. + +No sum hosts the row. The four P104 ports `478, 11, 14, 475` have augmented +chart labels summing to 0, so every affine function has value-sum 0 there. +The indicator is 1 only at port 11, so its value-sum is 1. The same +contradiction holds for `21, 13, 493, 501`. The argument is written in +[PROOF.md](PROOF.md). It already fails on the 104 P104 lines, before the 16 +lines outside P104 are considered. + +The 120 letters span all 512 affine functions. On the 120 root lines their +Hamming distances from the indicator are `8, 48, 56, 64, 72, 112` with +multiplicities `1, 7, 248, 248, 7, 1`. The unique closest sum is the zero +polynomial, at distance 8. No subset of one, two, or three root lines gives +this parity obstruction; 7168 subsets of size 4 do, and 4384 of those lie +inside P104. + +## Evidence class + +The degree bound and the four-line parity are written proofs. The chart +identity, the rank-9 span, the distance histograms, the 7168 four-line +obstructions, the 32130 four-letter syzygies, and the 255 subset-sums of the +frame letters are exhaustive finite censuses. This is not a heuristic and not +an incomplete search inside the sum alphabet. + +It is not a proof that 40 is minimal for sums of products, for another chart, +or for a circuit that is not an `F_2` sum of letters. The #7031 product remains +a hosting with 40 new monomials. That product is not a sum. No selected-invoice +histogram is computed, and the result does not beat the selected profile. + +## Scope + +Catalogue card `complex-rank-shape-decoder`, priority revision 8, pinned at +`17469fff78c22941280f04d39dc5a1faee09c840`. The card asks whether a decoder or +coframe change improves the full signed moment. Scope is **changed** to open +question 2 of +[PR #7031](https://github.com/CrocSwap/integer-mult-bounds/pull/7031): the +product census there does not cover sums. The connection to the bottleneck is +recorded in [TASK.json](TASK.json). A joint bill cannot undercut the product +charge by replacing this row with a sum of letters, because no such sum hosts +the row. That is not a signed histogram and not a supplier admission. + +`data/frames.json` is the frame partition vendored by #7031 from PR #7014 +(head `949c0ada285aae619468ae49317c8d9f4df130f7`), byte hash +`c75915c18fc06ac19cc90fb9911209517c071862fdf401b998d5075efc0cda0d`. Only frame 0 +is evaluated. Ports and the E8 line map are the #6933 inputs pinned in +[SOURCES.json](SOURCES.json). + +## Reproduce + +From the repository root, Python 3.12, standard library only: + +```sh +python3 -B research/p104-frame0-letter-sum/verify.py +python3 -I -O -B research/p104-frame0-letter-sum/verify.py +python3 -B scripts/research_package.py --package research/p104-frame0-letter-sum +python3 -B scripts/check_research_commit.py --package research/p104-frame0-letter-sum --check-source-history +``` + +The verifier prints `PASS_P104_FRAME0_LETTER_SUM` with `explicit=11+21+38+56`, +`monomials=0`, `new=0`, and `hosts=0`. Failure controls delete one letter of +that sum, reject each proper subset of the obstructing four, keep a +frame-supported dependence with even indicator parity out of the obstruction +count, and reject the constant-1 function and the single letter `λ_11`. + +## Open next questions + +1. Can one explicit `F_2` sum of two products of root-line letters, each + product of length at least 2, host this same row with fewer than 40 + monomials of degree at least 2? Pure sums are affine and cannot host. One + product of four letters already hosts with 40. A sum of two products is the + first expression that neither census covers. One miss is not a minimum. +2. Among the `2^16` functions of the four #7031 forms + `p = 1 + x1 + x2 + x4`, `q = x0`, `r = x5`, and `s = x6 + x7`, what is the + minimum number of degree-at-least-2 monomials of a function that matches + the indicator on all 120 lines? This finite family contains the length-4 + product and every sum of letters inside its span. It does not decide a + general circuit. + +## Credit + +Frame partition: unpaidmoon, PR #7014, as vendored by PR #7031. The product +hosting and the 40-monomial charge: PR #7031. Ports and the odd-graph window: +PR #6933. Label pairing: the inherited simple-root chart. Prepared by +unpaidmoon with substantial Cursor Grok assistance. New work is Apache-2.0. diff --git a/research/p104-frame0-letter-sum/SOURCES.json b/research/p104-frame0-letter-sum/SOURCES.json new file mode 100644 index 0000000000..e0c65df5a4 --- /dev/null +++ b/research/p104-frame0-letter-sum/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "17469fff78c22941280f04d39dc5a1faee09c840", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/p104-port-window-haemers/data/e8_line_map.json", + "usage": "input", + "git_blob": "19ea2d553aff60e53af50dd9582ab70730e93450", + "sha256": "b37530e8e9b2b3bd5be418d5ed3060a42ceb66e60ed3789f8ee79f29dabde437" + }, + { + "path": "research/p104-port-window-haemers/data/ports_p104.json", + "usage": "input", + "git_blob": "8037fd10877f49063a1c8a530b40c27f2453dac0", + "sha256": "691c7b7d212112115b1bfc76db89f90d304ec448dc8c4a0c43d9a5954317146c" + } + ] +} diff --git a/research/p104-frame0-letter-sum/TASK.json b/research/p104-frame0-letter-sum/TASK.json new file mode 100644 index 0000000000..9f86d40426 --- /dev/null +++ b/research/p104-frame0-letter-sum/TASK.json @@ -0,0 +1,81 @@ +{ + "schema_version": 1, + "task_id": "complex-rank-shape-decoder", + "priority_revision": 8, + "base_commit": "17469fff78c22941280f04d39dc5a1faee09c840", + "original_card": { + "id": "complex-rank-shape-decoder", + "question": "Can a legal decoder or coframe change improve the full signed moment, including changed helper targets?", + "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", + "docs/research/recursive-invoice-preflight.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": "A source-bound arbitrary-input identity and legal producer/consumer boundary with the complete paid and productive target invoice, including restoration, ownership, native alignment and extra charges. Price under the actual current model; historical ceiling.py assumptions must be established before use. A favorable optimistic relaxation keeps a route open but is not a completed supplier. A scoped local result remains useful; expansion requires the family-level budget gate.", + "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": "Price one complete changed itinerary with both paid and productive histograms. Check #5693/#5698 for overlap and their exact hypotheses before another coframe search. Use the signed invoice preflight where its boundary contract agrees; an inconclusive concave comparison is not a power crossing. Stop if an optimistic complete budget fails at the chosen target or native delivery remains unspecified.", + "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": [ + "coframe", + "signed moment", + "5693", + "5698" + ], + "existing_checks": [ + { + "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": "Decide whether an F2 sum of root-line letters hosts frame 0 of the #7031 indicator with fewer than 40 new monomials.", + "scope_change_reason": "The catalogue card asks whether a decoder or coframe change improves the full signed moment. Open PR #7031 leaves a prior alphabet question: its 40-monomial charge is for products, and a sum of letters is not covered. This package answers that question for frame 0. It does not price a changed itinerary, so it cannot improve the signed moment.", + "bottleneck_link": "A joint bill cannot undercut the #7031 product charge by hosting this one row as a sum of letters, because no such sum matches the indicator. Removing that alphabet is a prerequisite for knowing which charges are still available. It is not itself a signed histogram or a supplier admission.", + "budget_minutes": 60, + "stop_rule": "Stop after the explicit four-letter sum, its empty monomial charge, and the proof that no F2 sum hosts frame 0. Do not census sums of products, do not host frame 1, do not name the 40 monomials on the #6030 invoice, and do not claim a kappa change.", + "outcome": "negative-result", + "evidence": "verify.py prints PASS_P104_FRAME0_LETTER_SUM explicit=11+21+38+56 monomials=0 new=0 hosts=0. Evidence class: a written degree bound and a written four-line parity obstruction on P104 ports 478, 11, 14, 475, plus exhaustive censuses of the 512 affine functions, the 7168 weight-4 obstructions, and the 255 frame-letter subset sums. Not a heuristic. Not a selected-profile comparison. Selected kappa remains 781451/250000000.", + "author": "unpaidmoon", + "ai_assistance": "Substantial Cursor Grok assistance. The four-line parity is written in PROOF.md; labels, rank, distances, and subset censuses are recomputed by verify.py.", + "open_questions": [ + { + "question": "Can one explicit F2 sum of two products of root-line letters, each of length at least 2, host frame 0 on all 120 lines with fewer than 40 monomials of degree at least 2?", + "why_it_matters": "Pure sums are affine and cannot host. One product of four letters already hosts with 40 new monomials. A sum of two products is the first expression that neither the #7031 product census nor this sum proof covers, and it is the first place a charge below 40 could still appear.", + "first_step": "Expand one sum of two distinct length-2 products of frame letters in the simple-root chart, count monomials of degree at least 2, and compare the values with the indicator on all 120 lines. A miss of that one sum is not a minimum.", + "blocked_by": "none for a single example; a minimum needs a finite domain and a complete enumeration" + }, + { + "question": "What is the minimum number of degree-at-least-2 monomials among the 2^16 functions of p=1+x1+x2+x4, q=x0, r=x5, and s=x6+x7 that match the frame-0 indicator on all 120 lines?", + "why_it_matters": "This finite family contains the #7031 length-4 product and every sum of letters in its span. A host in the family with fewer than 40 new monomials would undercut the product charge inside an explicitly bounded alphabet.", + "first_step": "Enumerate all functions of these four F2 values, keep those equal to the indicator on the 120 root lines, and report the minimum degree-at-least-2 count.", + "blocked_by": "this package stops at degree at most 1" + } + ] +} diff --git a/research/p104-frame0-letter-sum/VERIFY.json b/research/p104-frame0-letter-sum/VERIFY.json new file mode 100644 index 0000000000..b87de90bc9 --- /dev/null +++ b/research/p104-frame0-letter-sum/VERIFY.json @@ -0,0 +1,32 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/p104-port-window-haemers/data/e8_line_map.json", + "research/p104-port-window-haemers/data/ports_p104.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Charges the explicit sum λ_11+λ_21+λ_38+λ_56 as the zero polynomial (no new monomials) and checks that it misses the frame. Proves no affine function matches the indicator, using the P104 fours 478,11,14,475 and 21,13,493,501. Exhaustive censuses: 512 affine distances, 7168 weight-4 obstructions (4384 inside P104), no obstruction of size below 4, 32130 four-letter syzygies, and all 255 frame-letter subset sums. Failure controls delete one explicit letter, reject every proper subset of the first four, and reject constant 1 and λ_11. Prints PASS_P104_FRAME0_LETTER_SUM with new=0 and hosts=0. Does not rerun the #7031 product census and does not change kappa." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Same identity, parity proof, and censuses with isolated mode and assert stripping, confirming the checks are need() failures rather than assertions." + } + ] +} diff --git a/research/p104-frame0-letter-sum/data/frames.json b/research/p104-frame0-letter-sum/data/frames.json new file mode 100644 index 0000000000..793a32f489 --- /dev/null +++ b/research/p104-frame0-letter-sum/data/frames.json @@ -0,0 +1,157 @@ +{ + "description": "Disjoint 8-cliques of the odd graph. frames partition the 104 P104 ports. excluded_odd_cliques are the two 8-cliques in the 120 weight-3-mod-4 vectors that P104 omits; together with frames they partition those 120 vectors. Integers are F_2^9 ports, bit i coordinate i.", + "frames": [ + [ + 11, + 21, + 38, + 56, + 140, + 146, + 161, + 191 + ], + [ + 13, + 26, + 131, + 148, + 262, + 273, + 392, + 415 + ], + [ + 14, + 69, + 164, + 239, + 276, + 351, + 446, + 501 + ], + [ + 19, + 41, + 74, + 112, + 280, + 290, + 321, + 379 + ], + [ + 22, + 37, + 196, + 247, + 268, + 319, + 478, + 493 + ], + [ + 28, + 49, + 133, + 168, + 265, + 292, + 400, + 445 + ], + [ + 35, + 81, + 176, + 194, + 274, + 352, + 385, + 499 + ], + [ + 44, + 84, + 152, + 224, + 304, + 328, + 388, + 508 + ], + [ + 50, + 70, + 138, + 254, + 259, + 375, + 443, + 463 + ], + [ + 73, + 98, + 208, + 251, + 324, + 367, + 477, + 502 + ], + [ + 88, + 100, + 193, + 253, + 322, + 382, + 475, + 487 + ], + [ + 134, + 145, + 200, + 223, + 416, + 439, + 494, + 505 + ], + [ + 261, + 296, + 336, + 381, + 386, + 431, + 471, + 506 + ] + ], + "excluded_odd_cliques": [ + [ + 7, + 25, + 42, + 52, + 76, + 82, + 97, + 127 + ], + [ + 67, + 104, + 137, + 162, + 266, + 289, + 448, + 491 + ] + ] +} diff --git a/research/p104-frame0-letter-sum/verify.py b/research/p104-frame0-letter-sum/verify.py new file mode 100644 index 0000000000..3c81d87845 --- /dev/null +++ b/research/p104-frame0-letter-sum/verify.py @@ -0,0 +1,473 @@ +#!/usr/bin/env python3 +"""No F2 sum of root-line letters hosts the #7031 frame-0 indicator. + +The explicit sum is λ_11 + λ_21 + λ_38 + λ_56. In the inherited simple-root +chart those four letters cancel, so the sum is the zero polynomial: no +monomials at all, and therefore no monomial of degree at least 2. The zero +polynomial is 0 on the eight frame lines, so this sum does not host the row. + +Every F2 sum of the 120 letters is affine, and the letters span all 512 +affine functions. Ports 478, 11, 14 and 475 lie in P104 and their augmented +labels sum to 0, while the indicator sums to 1 on those four lines. No affine +function hosts the row on the 104 P104 lines, nor on all 120 root lines. + +This does not rerun the #7031 product census and does not change kappa. +Checks are need() failures, so python -O still runs them. +""" + +import hashlib +import json +from collections import Counter +from fractions import Fraction +from itertools import combinations, product +from pathlib import Path + +ROOT = Path(__file__).resolve().parent +REPO = ROOT.parents[1] +FRAMES_SHA256 = "c75915c18fc06ac19cc90fb9911209517c071862fdf401b998d5075efc0cda0d" +FRAME = (11, 21, 38, 56, 140, 146, 161, 191) +EXPLICIT_SUM = (11, 21, 38, 56) +FRAME_LETTERS = { + 11: (54, 1), + 21: (55, 1), + 38: (23, 1), + 56: (22, 1), + 140: (225, 1), + 146: (224, 1), + 161: (192, 1), + 191: (193, 1), +} +CANCEL_FOURS = ( + (11, 21, 38, 56), + (11, 21, 140, 146), + (11, 21, 161, 191), + (11, 38, 140, 161), + (11, 38, 146, 191), + (11, 56, 140, 191), + (11, 56, 146, 161), + (21, 38, 140, 191), + (21, 38, 146, 161), + (21, 56, 140, 161), + (21, 56, 146, 191), + (38, 56, 140, 146), + (38, 56, 161, 191), + (140, 146, 161, 191), +) +OBSTRUCTION = (478, 11, 14, 475) +OBSTRUCTION_BITS = {478: 12, 11: 26, 14: 175, 475: 185} +SECOND_OBSTRUCTION = (21, 13, 493, 501) +SECOND_BITS = {21: 28, 13: 58, 493: 30, 501: 56} +DISTANCE_120 = {8: 1, 48: 7, 56: 248, 64: 248, 72: 7, 112: 1} +DISTANCE_104 = {8: 1, 36: 3, 44: 12, 48: 199, 52: 82, 56: 199, 60: 12, 68: 3, 96: 1} +WEIGHT4_OBSTRUCTIONS = 7168 +WEIGHT4_OBSTRUCTIONS_P104 = 4384 +LETTER_SYZYGIES_SIZE4 = 32130 + + +def need(condition, message): + if not condition: + raise SystemExit(message) + + +def e8_roots(): + roots = [] + for left, right in combinations(range(8), 2): + for sign_left in (1, -1): + for sign_right in (1, -1): + vector = [0] * 8 + vector[left] = 2 * sign_left + vector[right] = 2 * sign_right + roots.append(tuple(vector)) + for signs in product((1, -1), repeat=8): + if signs.count(-1) % 2 == 0: + roots.append(tuple(signs)) + return roots + + +def simple_basis(): + basis = [ + (1, -1, -1, -1, -1, -1, -1, 1), + (2, 2, 0, 0, 0, 0, 0, 0), + (-2, 2, 0, 0, 0, 0, 0, 0), + ] + for index in range(1, 6): + vector = [0] * 8 + vector[index] = -2 + vector[index + 1] = 2 + basis.append(tuple(vector)) + return basis + + +def dot(left, right): + return sum(a * b for a, b in zip(left, right)) // 4 + + +def cartan_mod2(basis): + return [[dot(basis[i], basis[j]) & 1 for j in range(8)] for i in range(8)] + + +def solve_coordinates(matrix, target): + rows = [[Fraction(entry) for entry in matrix[i]] + [Fraction(target[i])] for i in range(8)] + for column in range(8): + pivot = next(row for row in range(column, 8) if rows[row][column]) + rows[column], rows[pivot] = rows[pivot], rows[column] + scale = 1 / rows[column][column] + rows[column] = [entry * scale for entry in rows[column]] + for row in range(8): + if row != column and rows[row][column]: + factor = rows[row][column] + rows[row] = [rows[row][col] - factor * rows[column][col] for col in range(9)] + solution = [rows[i][8] for i in range(8)] + need(all(entry.denominator == 1 for entry in solution), "root coordinates are not integral") + return tuple(int(entry) for entry in solution) + + +def pairing(form, left, right): + value = 0 + for i in range(8): + if (left >> i) & 1: + for j in range(8): + if (right >> j) & 1 and form[i][j]: + value ^= 1 + if (left >> 8) & 1 and (right >> 8) & 1: + value ^= 1 + return value + + +def label_of(root, matrix): + coordinates = solve_coordinates(matrix, root) + bits = 0 + for index, value in enumerate(coordinates): + if value & 1: + bits |= 1 << index + return bits | (1 << 8) + + +def negate(vector): + return tuple(-entry for entry in vector) + + +def root_lines(): + lines = [] + seen = set() + for root in e8_roots(): + key = root if root > negate(root) else negate(root) + if key not in seen: + seen.add(key) + lines.append(root) + need(len(lines) == 120, "expected 120 root lines") + return lines + + +def letter_form(label, form): + mask = 0 + for index in range(8): + if pairing(form, label, 1 << index): + mask |= 1 << index + return mask, pairing(form, label, 1 << 8) + + +def monomials(mask, constant): + exponents = [] + if constant: + exponents.append(0) + for index in range(8): + if (mask >> index) & 1: + exponents.append(1 << index) + return tuple(exponents) + + +def new_monomials(mask, constant): + return tuple(exponent for exponent in monomials(mask, constant) if exponent.bit_count() >= 2) + + +def evaluate_affine(mask, constant, bits): + return constant ^ ((bits & mask).bit_count() & 1) + + +def f2_rank(vectors): + basis = {} + for vector in vectors: + value = vector + while value: + pivot = value.bit_length() - 1 + if pivot in basis: + value ^= basis[pivot] + else: + basis[pivot] = value + break + return len(basis) + + +def load_geometry(): + frame_path = ROOT / "data" / "frames.json" + frame_bytes = frame_path.read_bytes() + need(hashlib.sha256(frame_bytes).hexdigest() == FRAMES_SHA256, "frames.json sha256 mismatch") + frames = json.loads(frame_bytes.decode())["frames"] + need(len(frames) == 13 and all(len(frame) == 8 for frame in frames), "expected 13 frames of size 8") + need(tuple(frames[0]) == FRAME, "frame 0 ports changed") + ports = json.loads((REPO / "research/p104-port-window-haemers/data/ports_p104.json").read_text())["ports"] + line_map = json.loads((REPO / "research/p104-port-window-haemers/data/e8_line_map.json").read_text()) + vector_to_root = {vector: tuple(root) for vector, root in zip(line_map["vectors"], line_map["roots2"])} + need(len(ports) == 104 and len(set(ports)) == 104, "expected 104 distinct P104 ports") + port_set = set(ports) + basis = simple_basis() + matrix = list(zip(*basis)) + form = cartan_mod2(basis) + lines = root_lines() + labels = [label_of(root, matrix) for root in lines] + need(len(set(labels)) == 120, "root-line labels are not distinct") + need(all((label >> 8) & 1 for label in labels), "a label is missing the ninth coordinate") + index = {} + for position, root in enumerate(lines): + index[root] = position + index[negate(root)] = position + mismatches = 0 + for left in range(120): + for right in range(120): + expected = (dot(lines[left], lines[right]) + 1) & 1 + if pairing(form, labels[left], labels[right]) != expected: + mismatches += 1 + need(mismatches == 0, "simple-root chart does not reproduce the label pairing") + root_to_port = {} + for vector, root in vector_to_root.items(): + root_to_port[root] = vector + root_to_port[negate(root)] = vector + return frames, port_set, vector_to_root, form, lines, labels, index, root_to_port + + +def position_of(port, vector_to_root, index): + root = vector_to_root[port] + if root not in index: + root = negate(root) + return index[root] + + +def main(): + _frames, ports, vector_to_root, form, lines, labels, index, root_to_port = load_geometry() + frame_positions = [position_of(port, vector_to_root, index) for port in FRAME] + need(len(set(frame_positions)) == 8, "frame 0 does not use eight root lines") + need(set(FRAME) <= ports, "frame 0 is not contained in P104") + for left, right in combinations(FRAME, 2): + need((left & right).bit_count() & 1, "frame 0 is not an odd-graph clique") + need(dot(vector_to_root[left], vector_to_root[right]) == 0, "frame 0 roots are not pairwise orthogonal") + frame_position_set = set(frame_positions) + p104_points = {position for position in range(120) if root_to_port[lines[position]] in ports} + need(len(p104_points) == 104, "expected 104 P104 root lines") + need(frame_position_set <= p104_points, "a frame line is outside P104") + + letter_vectors = [] + point_vectors = [] + point_bits = [] + for position, label in enumerate(labels): + mask, constant = letter_form(label, form) + need(constant == 1, "a letter does not have constant term 1") + letter_vectors.append(mask | (constant << 8)) + bits = label & 255 + point_bits.append(bits) + point_vectors.append(bits | (1 << 8)) + need(len(set(letter_vectors)) == 120, "letter vectors are not distinct") + need(f2_rank(letter_vectors) == 9, "the 120 letters do not span every affine function") + need(all(new_monomials(vector & 255, (vector >> 8) & 1) == () for vector in range(512)), + "an affine normal form has a monomial of degree at least 2") + + forms = {} + for port, position in zip(FRAME, frame_positions): + forms[port] = letter_form(labels[position], form) + need(forms == FRAME_LETTERS, "frame-letter polynomials changed: {0}".format(forms)) + explicit_mask = 0 + explicit_constant = 0 + for port in EXPLICIT_SUM: + mask, constant = forms[port] + explicit_mask ^= mask + explicit_constant ^= constant + need((explicit_mask, explicit_constant) == (0, 0), "the explicit four-letter sum is not zero") + need(monomials(explicit_mask, explicit_constant) == (), "the zero polynomial was given a monomial") + need(new_monomials(explicit_mask, explicit_constant) == (), "the explicit sum was charged a new monomial") + for port in EXPLICIT_SUM: + mask, constant = forms[port] + rest_mask = explicit_mask ^ mask + rest_constant = explicit_constant ^ constant + need((rest_mask, rest_constant) != (0, 0), "dropping {0} still cancels".format(port)) + + cancel_fours = [] + cancel_sizes = Counter() + for size in range(1, 9): + for choice in combinations(FRAME, size): + mask = 0 + constant = 0 + for port in choice: + bit, term = forms[port] + mask ^= bit + constant ^= term + if (mask, constant) == (0, 0): + cancel_sizes[size] += 1 + if size == 4: + cancel_fours.append(choice) + need(dict(cancel_sizes) == {4: 14, 8: 1}, "frame-letter cancellations changed: {0}".format(dict(cancel_sizes))) + need(tuple(cancel_fours) == CANCEL_FOURS, "the 14 cancelling fours changed") + hosted_frame_sums = 0 + for size in range(1, 9): + for choice in combinations(range(8), size): + mask = 0 + constant = 0 + for letter_index in choice: + bit, term = forms[FRAME[letter_index]] + mask ^= bit + constant ^= term + if all(evaluate_affine(mask, constant, point_bits[position]) == 1 for position in frame_positions): + if all(evaluate_affine(mask, constant, point_bits[position]) == 0 + for position in range(120) if position not in frame_position_set): + hosted_frame_sums += 1 + need(hosted_frame_sums == 0, "a sum of frame letters hosts the row") + + def bits_of(port): + return point_bits[position_of(port, vector_to_root, index)] + + for port, bits in OBSTRUCTION_BITS.items(): + need(bits_of(port) == bits, "label of port {0} changed".format(port)) + need(port in ports, "obstruction port {0} is outside P104".format(port)) + for port, bits in SECOND_BITS.items(): + need(bits_of(port) == bits, "label of port {0} changed".format(port)) + need(port in ports, "second obstruction port {0} is outside P104".format(port)) + need(OBSTRUCTION_BITS[478] ^ OBSTRUCTION_BITS[11] ^ OBSTRUCTION_BITS[14] ^ OBSTRUCTION_BITS[475] == 0, + "the four obstruction labels do not sum to 0") + need((1 << 8) ^ (1 << 8) ^ (1 << 8) ^ (1 << 8) == 0, "four constant coordinates failed to cancel") + need(sum(1 for port in OBSTRUCTION if port in set(FRAME)) == 1, "the obstruction should meet the frame once") + need(SECOND_BITS[21] ^ SECOND_BITS[13] ^ SECOND_BITS[493] ^ SECOND_BITS[501] == 0, + "the second obstruction labels do not sum to 0") + for kept in combinations(OBSTRUCTION, 3): + total = 0 + for port in kept: + total ^= OBSTRUCTION_BITS[port] | (1 << 8) + need(total != 0, "a proper subset of the obstruction is already dependent") + frame_four_bits = [bits_of(port) for port in EXPLICIT_SUM] + need(frame_four_bits[0] ^ frame_four_bits[1] ^ frame_four_bits[2] ^ frame_four_bits[3] == 0, + "the explicit sum's evaluation labels do not sum to 0") + need(sum(1 for port in EXPLICIT_SUM if port in set(FRAME)) == 4, "the explicit sum left the frame") + # All four ports lie in the frame, so this dependence has even indicator + # parity and must not be counted as an obstruction. + explicit_points = tuple(sorted(position_of(port, vector_to_root, index) for port in EXPLICIT_SUM)) + + target = [1 if position in frame_position_set else 0 for position in range(120)] + distances = Counter() + distances_104 = Counter() + hosts = 0 + hosts_104 = 0 + for coefficient in range(512): + mask = coefficient & 255 + constant = (coefficient >> 8) & 1 + wrong = 0 + wrong_104 = 0 + for position in range(120): + if evaluate_affine(mask, constant, point_bits[position]) != target[position]: + wrong += 1 + if position in p104_points: + wrong_104 += 1 + distances[wrong] += 1 + distances_104[wrong_104] += 1 + if wrong == 0: + hosts += 1 + if wrong_104 == 0: + hosts_104 += 1 + need(hosts == 0, "an affine function agrees with the indicator on all 120 lines") + need(hosts_104 == 0, "an affine function agrees with the indicator on the 104 P104 lines") + need(dict(distances) == DISTANCE_120, "120-line distances changed: {0}".format(dict(distances))) + need(dict(distances_104) == DISTANCE_104, "104-line distances changed: {0}".format(dict(distances_104))) + need(distances[8] == 1, "the distance-8 sum is not unique") + zero_wrong = sum(target) + need(zero_wrong == 8, "the zero polynomial does not miss exactly the eight frame lines") + + small_obstructions = 0 + small_dependencies = 0 + for size in range(1, 4): + for choice in combinations(range(120), size): + total = 0 + parity = 0 + for position in choice: + total ^= point_vectors[position] + parity ^= target[position] + if total == 0: + small_dependencies += 1 + if parity == 1: + small_obstructions += 1 + need(small_dependencies == 0, "an affine dependence of fewer than four root lines exists") + need(small_obstructions == 0, "an obstruction of fewer than four root lines exists") + weight4 = 0 + weight4_p104 = 0 + seen_primary = False + seen_second = False + seen_explicit = False + odd_frame_counts = Counter() + primary_points = tuple(sorted(position_of(port, vector_to_root, index) for port in OBSTRUCTION)) + second_points = tuple(sorted(position_of(port, vector_to_root, index) for port in SECOND_OBSTRUCTION)) + for choice in combinations(range(120), 4): + total = 0 + parity = 0 + frame_hits = 0 + for position in choice: + total ^= point_vectors[position] + parity ^= target[position] + frame_hits += target[position] + if total != 0 or parity != 1: + continue + weight4 += 1 + odd_frame_counts[frame_hits] += 1 + if all(position in p104_points for position in choice): + weight4_p104 += 1 + ordered = tuple(sorted(choice)) + if ordered == primary_points: + seen_primary = True + if ordered == second_points: + seen_second = True + if ordered == explicit_points: + seen_explicit = True + need(not seen_explicit, "the even frame dependence was counted as an obstruction") + need(weight4 == WEIGHT4_OBSTRUCTIONS, "weight-4 obstruction count changed: {0}".format(weight4)) + need(weight4_p104 == WEIGHT4_OBSTRUCTIONS_P104, + "P104 weight-4 obstruction count changed: {0}".format(weight4_p104)) + need(dict(odd_frame_counts) == {1: WEIGHT4_OBSTRUCTIONS}, + "a weight-4 obstruction meets the frame more than once") + need(seen_primary and seen_second, "a named obstruction was not found by the census") + + letter_small = 0 + letter_size4 = 0 + for size in range(1, 5): + for choice in combinations(range(120), size): + total = 0 + for position in choice: + total ^= letter_vectors[position] + if total == 0: + if size < 4: + letter_small += 1 + else: + letter_size4 += 1 + need(letter_small == 0, "fewer than four letters already sum to zero") + need(letter_size4 == LETTER_SYZYGIES_SIZE4, "four-letter syzygy count changed: {0}".format(letter_size4)) + + constant_one_wrong = 0 + for position in range(120): + if evaluate_affine(0, 1, point_bits[position]) != target[position]: + constant_one_wrong += 1 + need(constant_one_wrong == 112, "the constant-1 function does not miss the 112 non-frame lines") + one_letter_mask, one_letter_constant = forms[11] + need(new_monomials(one_letter_mask, one_letter_constant) == (), "one letter acquired a new monomial") + need(all(evaluate_affine(one_letter_mask, one_letter_constant, point_bits[position]) == 1 + for position in frame_positions), "λ_11 is not 1 on the whole frame") + need(any(evaluate_affine(one_letter_mask, one_letter_constant, point_bits[position]) == 1 + for position in range(120) if position not in frame_position_set), + "λ_11 does not spill outside the frame") + + print( + "PASS_P104_FRAME0_LETTER_SUM explicit=11+21+38+56 monomials=0 new=0 " + "hosts=0 hosts_p104=0 min_disagreements=8 closest=zero " + "obstruction=478,11,14,475 weight4=7168 weight4_p104=4384 " + "frame_sums=255 frame_sum_hosts=0 cancelling_fours=14" + ) + print("MONOMIALS") + print("NEW_MONOMIALS") + print("ONE_LETTER port=11 monomials=1,x1,x2,x4,x5 new=0 hosts=0") + + +if __name__ == "__main__": + main()