diff --git a/research/p104-frame-host-minimum/README.md b/research/p104-frame-host-minimum/README.md new file mode 100644 index 0000000000..eb3817910a --- /dev/null +++ b/research/p104-frame-host-minimum/README.md @@ -0,0 +1,191 @@ +# P104 frame-host minimum: exact hosting charges of the frame-indicator rows (no κ) + +Result and claim type: **finite certificates** (exhaustive enumeration, direct +evaluation of every host) and a **scoped written proof** of the coset structure +(Lemma 1). No κ, no supplier admission, no selected-frontier change. This package +was produced by Nick Petalas. + +## Setting + +Open PR #7031 hosts frame 0 of the #7014 104-by-13 witness as a product of +root-line letters and charges its **40** monomials of degree at least 2 in the +simple-root chart; open PR #7047 asks (question 2) for the minimum charge among +the 2^16 functions of the four forms `p = 1 + x1 + x2 + x4`, `q = x0`, `r = x5`, +`s = x6 + x7`. This package keeps their charge model: a *host* of a row is a Boolean +function on `F_2^8` that equals the row's indicator on the root-line chart points; +its *charge* is the number of monomials of degree at least 2 in its algebraic normal +form (ANF); affine terms are free. A row is one of the 15 odd 8-cliques of #7014's +`frames.json` (13 P104 frames and the 2 excluded cliques). Scope is the 120 root +lines, or only the 104 P104 lines. + +## Results + +**1. Answer to #7047 question 2: exactly 16.** The 120 root lines attain only 15 of +the 16 values of `(p, q, r, s)`; the value `(0,0,0,1)` is missed, and each attained +value holds 8 lines. The frame-0 indicator is constant on every attained fibre, so +exactly two functions of the four forms host frame 0: the #7031 product +`(1+x0)(1+x1+x2+x4)(1+x5)(1+x6+x7)` with charge 40, and the product plus the +indicator of the missed fibre, + +```text +(1 + x0)(1 + x5)(1 + x1 + x2 + x4 + x6 + x7) charge 16, 24 monomials. +``` + +It is a product of three affine forms. Each is a sum of an odd number of letters, since +the 120 letters span every affine function, so its charge is 16 by the #7047 +convention that sums of letters are free. + +**2. Lemma 1 (structure of every row).** Let `Q = Σ x_i + Σ x_i x_j` over the 7 edges +`02, 13, 23, 34, 45, 56, 67` of the E8 diagram in the simple-root chart (the mod-2 +value of `(v, v)/2`). The 120 chart points are exactly `{x : Q(x) = 1}`. Each of the +15 cliques is a coset `F = a + W` of a 3-dimensional subspace `W`. Let `B` be the polar +form of `Q`; it is nondegenerate because the Cartan matrix is unimodular. Then: + +- the 32 cosets of `W` split as `F` itself with 8 lines, 28 cosets with exactly 4 lines + each, and 3 cosets with none (8 + 28·4 = 120); +- the 3 empty cosets and `F` make the 5-flat `a + W^⊥`, so `(a + W^⊥) ∩ lines = F`; +- hence exactly 8 functions invariant under `W` host the row, and exactly 5 flats + `G ⊇ F` meet the lines only in `F`: the subspaces between `W` and `W^⊥` + (`F`, three 4-flats and `a + W^⊥`). + +*Proof.* `Q = 1` on `F` gives `Q(a+w) = 1`, so `Q(w) = B(a,w)` on `W` and `W` is +totally isotropic. For a coset `c + W`, `Q(c+w) = Q(c) + B(a+c, w)`: constant when +`a + c ∈ W^⊥`, otherwise a non-constant affine function, which is 1 on exactly 4 of +the 8 points. `Q'(x) = Q(a+x) + Q(a)` has 120 zeros, so it is elliptic; `W` is totally +singular for `Q'`, hence maximal, and `W^⊥/W` is anisotropic, so `Q' = 1` on +`W^⊥ ∖ W`, i.e. `Q = 0` on the three other cosets of `a + W^⊥`. ∎ `verify.py` +checks every step on all 15 cliques. + +**3. No host of degree at most 2, for any row.** For each clique `verify.py` finds a +3-flat `S` inside the root lines with `|S ∩ F| = 1`. A polynomial of degree at most 2 +sums to 0 over a 3-flat, while the indicator sums to 1 over `S`, so no host of degree at +most 2 exists. The linear system over `F_2` agrees: it is inconsistent for degree 2 on +both scopes. Hosts of degree at most 3 form an affine space of dimension 9 on the +120-line scope (`f + (1+Q)·affine`, 512 hosts) and of dimension 11 on the 104-line scope. + +**4. Exact minima in named classes.** The classes are the `W`-invariant hosts (8 on the +120-line scope; the 5 flat indicators are among them) and all hosts of degree at most 3, +on both scopes. On the 120-line scope the minimum over the 5 flats equals the minimum over +all invariant hosts in every row. For frame 0 the minimum is 16 over invariant hosts and +14 over all cubic hosts (a unique minimiser). + +**5. Explicit sparser hosts (upper bounds).** A seeded randomized search +(`search.py`: information-set decoding over the 256 monomials, 3000 orders per row, +fixed seed) found hosts below the exact class minima in 10 of the 15 rows (F1, F2, F4, +F5, F7, F8, F9, F10, F12, X1) and equal to them in the other 5. Every host in +`data/hosts_*.json` is re-evaluated at every scope point by `verify.py`. The frame-0 host +of charge 14 is + +```text +1 + x0 + x1 + x2 + x0*x2 + x0*x3 + x0*x1*x3 + x0*x2*x3 + x4 + x0*x3*x4 + x5 + x1*x5 + +x0*x1*x5 + x2*x5 + x0*x2*x5 + x4*x5 + x6 + x5*x6 + x7 + x5*x7 + x0*x5*x7 + x0*x6*x7 +``` + +It has 8 free terms (the constant and `x0, x1, x2, x4, x5, x6, x7`) and 14 charged +terms (7 of degree 2 and 7 of degree 3). It is the same polynomial that `verify.py` +asserts. + +Charge of the best host by row (monomials of degree at least 2). F0 to F12 are the 13 P104 frames and X0, X1 the two excluded cliques. "Letter product" is the #7031 hosting word, the indicator of `span(F)`. The two exact columns are minima over the named classes on the 120-line scope. The last two columns are the explicit hosts in `data/hosts_T120.json` and `data/hosts_P104.json`; the 104-line run starts from the 120-line hosts, which also host on 104 lines. + +| row | letter product | exact flat/invariant min | exact cubic min | explicit host, 120 lines | explicit host, 104 lines | +|---|---:|---:|---:|---:|---:| +| F0 | 40 | 16 | 14 | 14 | 14 | +| F1 | 111 | 24 | 24 | 20 | 18 | +| F2 | 89 | 26 | 26 | 20 | 16 | +| F3 | 105 | 34 | 22 | 22 | 22 | +| F4 | 83 | 36 | 24 | 22 | 19 | +| F5 | 93 | 10 | 18 | 6 | 6 | +| F6 | 35 | 27 | 23 | 23 | 23 | +| F7 | 101 | 16 | 14 | 10 | 10 | +| F8 | 111 | 42 | 30 | 26 | 23 | +| F9 | 103 | 28 | 28 | 18 | 16 | +| F10 | 107 | 24 | 24 | 14 | 14 | +| F11 | 58 | 28 | 21 | 21 | 21 | +| F12 | 90 | 13 | 17 | 9 | 9 | +| X0 | 11 | 7 | 7 | 7 | - | +| X1 | 87 | 34 | 30 | 20 | - | + +Exact class minima on the 104-line scope, as (W-invariant, cubic) for frames F0 to F12: + +```text +[(15, 14), (24, 24), (26, 23), (34, 22), (36, 21), (10, 18), (27, 23), (16, 14), (42, 30), (28, 28), (24, 24), (28, 21), (13, 17)] +``` + + +The product-of-letters column is the charge of the indicator of `span(F) = F ∪ W`: +a letter of line `l` is `1 + B(l, x)`, it equals 1 on all of `F` only when `l ∈ F`, and +the common-1 set of the eight frame letters is `span(F)`. The column reproduces +#7031's 40 (frame 0) and #7046's 111 (frame 1) and totals **1126** over the 13 +frames. The best explicit hosts total **225** on the 120-line scope and **211** on +the 104-line scope. Rows are chosen independently, so these are separate bills, not a +joint minimisation. + +## Evidence and reproduction + +Python 3.12, standard library only. The verifier runs in under one second and each +generator command takes about 3 minutes. From the repository root: + +```sh +~/git/integer-mult-bounds/.venv/bin/python3.12 -B research/p104-frame-host-minimum/verify.py --table +~/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -B research/p104-frame-host-minimum/verify.py +~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/p104-frame-host-minimum +~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/p104-frame-host-minimum --check-source-history +# optional: regenerate the explicit hosts (deterministic; about 3 minutes each) +~/git/integer-mult-bounds/.venv/bin/python3.12 -B research/p104-frame-host-minimum/search.py --scope T120 --iterations 3000 --seed 20261110 --write /tmp/hosts_T120.json +~/git/integer-mult-bounds/.venv/bin/python3.12 -B research/p104-frame-host-minimum/search.py --scope P104 --iterations 3000 --seed 20261110 --incumbent /tmp/hosts_T120.json --write /tmp/hosts_P104.json +``` + +`verify.py` prints `PASS_P104_FRAME_HOST_MINIMUM` with the key numbers. Its failure +controls reject a corrupted host and a wrong form. The ANF of the two four-form +hosts is computed by polynomial multiplication and checked against the subset-sum +transform of their truth tables. Both must occur in the coset enumeration, and the +three-form host must also occur in the enumeration built from a linear system over `F_2` +(the degree-4 product must not). `data/frames.json` is #7014's witness as vendored by #7031 and +#7047 (sha256 `c75915c18fc06ac19cc90fb9911209517c071862fdf401b998d5075efc0cda0d`, +checked); the chart convention and the root-line map follow #7031 and #6933. + +## Limitations + +- The minimum over **all** Boolean functions is not claimed. The class minima are + exact only inside their classes, and the explicit hosts are the best found by a + heuristic of fixed budget (a failed search below them is not a lower bound). Several + rows' explicit hosts lie below every exact class minimum, so those minima are not + the true minima. +- The charge counts ANF monomials of degree at least 2 in the simple-root chart, as + in #7031 and #7047. It is not a signed invoice, a gate count or a supplier cost. + The 40 frame-0 monomials of #7031 and the hosts here are not named as primitives of + the selected #6030 invoice (open question of #7048), so no κ follows. +- Hosts here are Boolean functions, not shown to be realised by circuits of letters + beyond the three-form host in result 1. The joint thirteen-row bill with shared + monomials (#7046 question 2) is not minimised. +- No predecessor result is replayed; the 40 and 111 appear as outputs of this package's + own census. + +## Open next questions + +Structured copies are in [TASK.json](TASK.json). + +1. **True per-row minimum.** What is the minimum charge over all Boolean hosts? The + explicit hosts of frame 5 (6), frame 12 (9) and frame 7 (10) are below every exact class + minimum. First step: use exact branch-and-bound on the degree-at-most-4 + evaluation system for one row, or prove a coset-leader lower bound for excluded + clique X0 (best known 7). On the 120-line scope the degree-four system has 163 + monomial columns and rank 111, leaving 52 free coefficients and 2^52 hosts per + row. Direct enumeration is too large; no cheap lower-bound certificate is known. +2. **Joint thirteen-row bill.** If a shared monomial is charged once, what is the + smallest union over the rows? First step: take the 8 invariant and 512 cubic hosts + per row, which are exactly enumerable, and minimise the union of supports by exact + search. Blocked by the charging rule for a joint circuit (#7046 question 2). +3. **Invoice primitives.** Can the chart monomials of these hosts be named as + primitives of the selected #6030 invoice? First step: make one constructor read one + exponent and check the image of all monomials of the charge-14 host. Blocked as in + #7048: the present constructors read frame dimensions, idle lengths and a diagonal + popcount only. + +## Credit + +This package was produced by Nick Petalas. Predecessors, cited and not replayed: +unpaidmoon, #7031 (product hosting and the 40-monomial charge, the chart convention +and the four forms), #7046 (frame 1, 111 new monomials), #7047 (the question answered +in result 1) and #7014 (the 104-by-13 frame partition, `frames.json`); DreamingOfClouds, +#6933 (ports and the E8 line map, merged). New work is Apache-2.0. diff --git a/research/p104-frame-host-minimum/SOURCES.json b/research/p104-frame-host-minimum/SOURCES.json new file mode 100644 index 0000000000..c1adb0eb4e --- /dev/null +++ b/research/p104-frame-host-minimum/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "75d77b328ea02ded535e7f23aee5b1e55d0bb1a8", + "sha256": "154c3d30455d778fd3343b6b4851f0fa4665f0f7625b0adb3675e2bafbbf6bf1" + }, + { + "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-frame-host-minimum/TASK.json b/research/p104-frame-host-minimum/TASK.json new file mode 100644 index 0000000000..f9cb48473a --- /dev/null +++ b/research/p104-frame-host-minimum/TASK.json @@ -0,0 +1,87 @@ +{ + "schema_version": 1, + "task_id": "complex-rank-shape-decoder", + "priority_revision": 8, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "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": "Exact minimum monomial charge of a host of each P104 frame-indicator row (the 13 frames and the 2 excluded odd 8-cliques of the 104-by-13 witness of open PR #7014). Open question 2 of open PR #7047 (frame 0, functions of the four #7031 forms) is answered exactly; two wider named host classes (functions invariant under the clique's translation space, which contain the flat indicators, and all hosts of degree at most 3) are enumerated exactly on the 120-line scope and on the 104-line scope; sparser explicit hosts from a seeded randomized search are reported as upper bounds. Charge model of #7031/#7047: monomials of degree at least 2 of the algebraic normal form in the simple-root chart, with affine terms free.", + "scope_change_reason": "The card asks whether a decoder or coframe change improves the full signed moment. This package prices only the monomial-charge model that #7031 and #7047 introduced for hosting the frame-indicator rows. It prices no signed invoice, decoder or supplier, and answers open question 2 of #7047.", + "bottleneck_link": "Side result on the P104 frame-indicator hosting bill, not a mechanism change. It lowers the recorded frame-0 charge and gives each row's charge in the #7031 model. The open question of #7048 (naming the monomials as selected-invoice primitives) is unchanged, and no kappa follows.", + "budget_minutes": 60, + "stop_rule": "Stop after the exact census of the named classes on both scopes and the verified explicit hosts. No larger exhaustive class, no joint thirteen-row minimisation, no invoice pricing, no claim about the minimum over all Boolean functions.", + "outcome": "completed", + "evidence": "research/p104-frame-host-minimum/verify.py (exhaustive, standard library, under one second): chart and quadratic-form identification of the 120 lines, coset structure of the 15 cliques, degree-3 certificates, four-form fibre census, class minima, direct evaluation of every explicit host. research/p104-frame-host-minimum/search.py regenerates data/hosts_T120.json and data/hosts_P104.json deterministically. Upper bounds from the search are finite certificates; the exact minima hold only inside the named classes.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "What is the minimum charge over all Boolean hosts of one row, not only over the named classes?", + "why_it_matters": "The explicit hosts of several rows (frame 5: 6, frame 12: 9, frame 7: 10) lie below every exact class minimum, so the class minima are not the true minima and no lower bound beyond degree 3 is proved.", + "first_step": "Use exact branch-and-bound on the degree-at-most-4 evaluation system for one row on the 120-line scope (163 monomial columns, rank 111, 52 free coefficients), or prove a coset-leader lower bound for excluded clique X0, whose best known charge is 7.", + "blocked_by": "2^52 hosts per row is beyond direct enumeration in the standard-library verifier, and no cheap lower-bound certificate for the 247-coordinate coset problem is known." + }, + { + "question": "What is the joint charge of the thirteen rows when a monomial shared between rows is charged once?", + "why_it_matters": "Open question 2 of #7046 asks whether shared monomials can be charged once. The per-row hosts here are chosen independently, so their union is only an upper bound for one selection.", + "first_step": "List the near-optimal hosts per row (the 8 invariant and the 512 cubic hosts are exactly enumerable) and minimise the union of supports by exact search over the choice of host per row.", + "blocked_by": "No circuit is given that realises a joint host, so the charging rule for a shared monomial is the predecessor's open point." + }, + { + "question": "Can the chart monomials of these hosts be named as primitives of the selected #6030 invoice?", + "why_it_matters": "#7048 records that the 40 frame-0 monomials are not invoice primitives, so no kappa change follows from any charge in this model until a map to the invoice alphabet exists.", + "first_step": "Make one constructor of the selected invoice read one monomial exponent and check the image of all monomials of the frame-0 host of charge 14.", + "blocked_by": "The present constructors read frame dimensions, idle lengths and a diagonal popcount only, as #7048 records." + } + ] +} diff --git a/research/p104-frame-host-minimum/VERIFY.json b/research/p104-frame-host-minimum/VERIFY.json new file mode 100644 index 0000000000..88ed6b0656 --- /dev/null +++ b/research/p104-frame-host-minimum/VERIFY.json @@ -0,0 +1,49 @@ +{ + "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": "Quadratic-form identification of the 120 chart points, 28+3+1 coset structure of all 15 cliques, no host of degree 2 or less, the four-form fibre census (exactly two functions, charges 40 and 16), exact minima of three host classes on two scopes, letter-product baseline, and direct evaluation of every explicit host. Failure controls reject a corrupted host and a wrong form." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Same verifier under optimized isolated mode; checks are need() failures, so assertions stay active." + }, + { + "argv": [ + "{python}", + "-B", + "{package}/search.py", + "--scope", + "T120", + "--iterations", + "30", + "--seed", + "20261110", + "--rows", + "5,13" + ], + "timeout_seconds": 120, + "checks": "Smoke run of the host generator on two rows; it evaluates each host it emits on every scope point." + } + ] +} diff --git a/research/p104-frame-host-minimum/data/frames.json b/research/p104-frame-host-minimum/data/frames.json new file mode 100644 index 0000000000..793a32f489 --- /dev/null +++ b/research/p104-frame-host-minimum/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-frame-host-minimum/data/hosts_P104.json b/research/p104-frame-host-minimum/data/hosts_P104.json new file mode 100644 index 0000000000..922f14ec93 --- /dev/null +++ b/research/p104-frame-host-minimum/data/hosts_P104.json @@ -0,0 +1,322 @@ +[ + { + "scope": "P104", + "row": 0, + "charge": 14, + "monomials": [ + 0, + 1, + 2, + 4, + 5, + 9, + 11, + 13, + 16, + 25, + 32, + 34, + 35, + 36, + 37, + 48, + 64, + 96, + 128, + 160, + 161, + 193 + ] + }, + { + "scope": "P104", + "row": 1, + "charge": 18, + "monomials": [ + 11, + 42, + 90, + 94, + 129, + 131, + 136, + 149, + 160, + 162, + 169, + 180, + 204, + 209, + 216, + 218, + 222, + 240 + ] + }, + { + "scope": "P104", + "row": 2, + "charge": 16, + "monomials": [ + 42, + 44, + 56, + 87, + 96, + 99, + 100, + 104, + 112, + 114, + 158, + 163, + 166, + 168, + 224, + 235 + ] + }, + { + "scope": "P104", + "row": 3, + "charge": 22, + "monomials": [ + 9, + 11, + 27, + 29, + 33, + 35, + 46, + 60, + 88, + 90, + 91, + 93, + 130, + 134, + 137, + 146, + 161, + 162, + 193, + 200, + 209, + 228 + ] + }, + { + "scope": "P104", + "row": 4, + "charge": 19, + "monomials": [ + 4, + 5, + 11, + 14, + 25, + 28, + 37, + 38, + 43, + 45, + 74, + 89, + 106, + 109, + 137, + 164, + 193, + 196, + 227, + 235 + ] + }, + { + "scope": "P104", + "row": 5, + "charge": 6, + "monomials": [ + 41, + 43, + 105, + 165, + 171, + 177 + ] + }, + { + "scope": "P104", + "row": 6, + "charge": 23, + "monomials": [ + 0, + 2, + 4, + 8, + 10, + 12, + 16, + 18, + 22, + 28, + 32, + 33, + 37, + 44, + 48, + 50, + 54, + 56, + 68, + 100, + 128, + 129, + 133, + 146, + 152, + 160, + 164, + 168, + 198, + 212 + ] + }, + { + "scope": "P104", + "row": 7, + "charge": 10, + "monomials": [ + 21, + 29, + 52, + 60, + 85, + 90, + 118, + 121, + 204, + 216 + ] + }, + { + "scope": "P104", + "row": 8, + "charge": 23, + "monomials": [ + 16, + 17, + 24, + 52, + 53, + 60, + 76, + 80, + 85, + 102, + 103, + 120, + 134, + 153, + 170, + 178, + 183, + 188, + 194, + 195, + 197, + 203, + 209, + 210 + ] + }, + { + "scope": "P104", + "row": 9, + "charge": 16, + "monomials": [ + 3, + 15, + 23, + 33, + 39, + 41, + 75, + 103, + 131, + 152, + 155, + 161, + 171, + 200, + 215, + 239 + ] + }, + { + "scope": "P104", + "row": 10, + "charge": 14, + "monomials": [ + 34, + 35, + 50, + 55, + 76, + 99, + 100, + 107, + 140, + 162, + 166, + 169, + 178, + 215 + ] + }, + { + "scope": "P104", + "row": 11, + "charge": 21, + "monomials": [ + 5, + 7, + 9, + 11, + 32, + 34, + 48, + 50, + 72, + 74, + 96, + 98, + 130, + 131, + 133, + 134, + 137, + 146, + 160, + 176, + 200, + 224 + ] + }, + { + "scope": "P104", + "row": 12, + "charge": 9, + "monomials": [ + 33, + 37, + 41, + 49, + 97, + 103, + 107, + 115, + 169 + ] + } +] diff --git a/research/p104-frame-host-minimum/data/hosts_T120.json b/research/p104-frame-host-minimum/data/hosts_T120.json new file mode 100644 index 0000000000..0a677f7d46 --- /dev/null +++ b/research/p104-frame-host-minimum/data/hosts_T120.json @@ -0,0 +1,380 @@ +[ + { + "scope": "T120", + "row": 0, + "charge": 14, + "monomials": [ + 0, + 1, + 2, + 4, + 5, + 9, + 11, + 13, + 16, + 25, + 32, + 34, + 35, + 36, + 37, + 48, + 64, + 96, + 128, + 160, + 161, + 193 + ] + }, + { + "scope": "T120", + "row": 1, + "charge": 20, + "monomials": [ + 11, + 31, + 42, + 46, + 90, + 95, + 129, + 131, + 137, + 142, + 149, + 160, + 162, + 168, + 180, + 208, + 210, + 212, + 213, + 216 + ] + }, + { + "scope": "T120", + "row": 2, + "charge": 20, + "monomials": [ + 42, + 43, + 44, + 46, + 56, + 92, + 96, + 99, + 102, + 104, + 107, + 112, + 114, + 119, + 156, + 168, + 224, + 227, + 228, + 235 + ] + }, + { + "scope": "T120", + "row": 3, + "charge": 22, + "monomials": [ + 9, + 11, + 27, + 29, + 33, + 35, + 46, + 60, + 88, + 90, + 91, + 93, + 130, + 134, + 137, + 146, + 161, + 162, + 193, + 200, + 209, + 228 + ] + }, + { + "scope": "T120", + "row": 4, + "charge": 22, + "monomials": [ + 6, + 11, + 12, + 13, + 20, + 25, + 38, + 43, + 44, + 52, + 69, + 75, + 89, + 103, + 107, + 123, + 132, + 137, + 164, + 193, + 227, + 235 + ] + }, + { + "scope": "T120", + "row": 5, + "charge": 6, + "monomials": [ + 41, + 43, + 105, + 165, + 171, + 177 + ] + }, + { + "scope": "T120", + "row": 6, + "charge": 23, + "monomials": [ + 0, + 2, + 4, + 8, + 10, + 12, + 16, + 18, + 22, + 28, + 32, + 33, + 37, + 44, + 48, + 50, + 54, + 56, + 68, + 100, + 128, + 129, + 133, + 146, + 152, + 160, + 164, + 168, + 198, + 212 + ] + }, + { + "scope": "T120", + "row": 7, + "charge": 10, + "monomials": [ + 21, + 29, + 52, + 60, + 85, + 90, + 118, + 121, + 204, + 216 + ] + }, + { + "scope": "T120", + "row": 8, + "charge": 26, + "monomials": [ + 21, + 23, + 48, + 49, + 52, + 55, + 56, + 60, + 81, + 87, + 88, + 108, + 112, + 118, + 133, + 165, + 166, + 170, + 178, + 184, + 199, + 202, + 204, + 209, + 216, + 218 + ] + }, + { + "scope": "T120", + "row": 9, + "charge": 18, + "monomials": [ + 3, + 7, + 35, + 55, + 75, + 101, + 107, + 121, + 130, + 134, + 146, + 151, + 153, + 162, + 166, + 169, + 178, + 201 + ] + }, + { + "scope": "T120", + "row": 10, + "charge": 14, + "monomials": [ + 34, + 35, + 50, + 55, + 76, + 99, + 100, + 107, + 140, + 162, + 166, + 169, + 178, + 215 + ] + }, + { + "scope": "T120", + "row": 11, + "charge": 21, + "monomials": [ + 5, + 7, + 9, + 11, + 32, + 34, + 48, + 50, + 72, + 74, + 96, + 98, + 130, + 131, + 133, + 134, + 137, + 146, + 160, + 176, + 200, + 224 + ] + }, + { + "scope": "T120", + "row": 12, + "charge": 9, + "monomials": [ + 33, + 37, + 41, + 49, + 97, + 103, + 107, + 115, + 169 + ] + }, + { + "scope": "T120", + "row": 13, + "charge": 7, + "monomials": [ + 0, + 1, + 8, + 9, + 32, + 33, + 40, + 41, + 64, + 65, + 96, + 97 + ] + }, + { + "scope": "T120", + "row": 14, + "charge": 20, + "monomials": [ + 10, + 14, + 26, + 30, + 31, + 46, + 71, + 74, + 79, + 82, + 102, + 119, + 138, + 154, + 158, + 199, + 202, + 210, + 215, + 230 + ] + } +] diff --git a/research/p104-frame-host-minimum/search.py b/research/p104-frame-host-minimum/search.py new file mode 100644 index 0000000000..fa07089874 --- /dev/null +++ b/research/p104-frame-host-minimum/search.py @@ -0,0 +1,153 @@ +#!/usr/bin/env python3 +"""Randomized sparse-host search: the generator for data/hosts.json. + +For one row (an odd 8-clique F) and one scope (120 root lines, or the 104 P104 +lines) a *host* is a Boolean function f on F_2^8 whose algebraic normal form (ANF) +reproduces the indicator of F on the scope. This script looks for hosts with few +monomials of degree >= 2 by information-set decoding over the 256 square-free +monomials: + + * the nine affine monomials are always pivoted first (they are free), + * the other monomials are taken in a seeded random order, + * the pivot solution with all free monomials zero is a host, and so is that + solution with any one free monomial switched on, + * the sparsest host over a fixed number of random orders is kept. + +The outcome is an explicit upper bound for each row, checked afterwards by +verify.py on every scope point. It is not a minimum and carries no lower bound. + + python3 -B search.py --scope T120 --iterations 3000 --seed 20261110 \ + --write data/hosts_T120.json + python3 -B search.py --scope P104 --iterations 3000 --seed 20261110 \ + --incumbent data/hosts_T120.json --write data/hosts_P104.json + +The run is deterministic for fixed arguments (no clock, no threads). +""" + +import argparse +import json +import random +import sys +from pathlib import Path + +ROOT = Path(__file__).resolve().parent +sys.path.insert(0, str(ROOT)) +import verify as geo # noqa: E402 (shares the chart and the host checker) + +SIZE = geo.SIZE +GE2 = geo.GE2 + + +def system_rows(scope, clique_set): + """One row per scope point: monomial incidence bits, rhs bit at position SIZE.""" + rows = [] + for x in sorted(scope): + row = 0 + for m in range(SIZE): + if m & ~x == 0: + row |= 1 << m + if x in clique_set: + row |= 1 << SIZE + rows.append(row) + return rows + + +AFFINE = [m for m in range(SIZE) if bin(m).count("1") <= 1] +HIGHER = [m for m in range(SIZE) if bin(m).count("1") >= 2] + + +def eliminate(rows, order): + reduced = list(rows) + used = [False] * len(reduced) + pivot_row = {} + for col in order: + bit = 1 << col + found = -1 + for i, row in enumerate(reduced): + if not used[i] and row & bit: + found = i + break + if found < 0: + continue + used[found] = True + pivot = reduced[found] + for j, row in enumerate(reduced): + if j != found and row & bit: + reduced[j] = row ^ pivot + pivot_row[col] = found + if len(pivot_row) == len(reduced): + break + for i, row in enumerate(reduced): + geo.need(used[i] or not (row >> SIZE) & 1, "the host system is inconsistent") + return reduced, pivot_row + + +def best_host(scope, clique_set, rng, iterations, incumbent=None): + rows = system_rows(scope, clique_set) + best_weight, best_anf = incumbent if incumbent else (10 ** 9, 0) + for _ in range(iterations): + order = AFFINE + rng.sample(HIGHER, len(HIGHER)) + reduced, pivot_row = eliminate(rows, order) + solution = 0 + for col, i in pivot_row.items(): + if (reduced[i] >> SIZE) & 1: + solution |= 1 << col + weight = (solution & GE2).bit_count() + if weight < best_weight: + best_weight, best_anf = weight, solution + # switch on one free monomial: it flips every pivot whose reduced row contains it + flips = {} + for col, i in pivot_row.items(): + row = reduced[i] + for fc in HIGHER: + if fc not in pivot_row and (row >> fc) & 1: + flips[fc] = flips.get(fc, 0) ^ (1 << col) + for fc in HIGHER: + if fc in pivot_row: + continue + candidate = solution ^ flips.get(fc, 0) ^ (1 << fc) + weight = (candidate & GE2).bit_count() + if weight < best_weight: + best_weight, best_anf = weight, candidate + return best_weight, best_anf + + +def main(argv): + parser = argparse.ArgumentParser() + parser.add_argument("--scope", choices=("T120", "P104"), required=True) + parser.add_argument("--iterations", type=int, required=True) + parser.add_argument("--seed", type=int, required=True) + parser.add_argument("--rows", default="all", help="comma-separated row indices or 'all'") + parser.add_argument("--write", default=None) + parser.add_argument( + "--incumbent", default=None, + help="hosts file for a larger scope; its hosts also host on this scope and seed the search") + args = parser.parse_args(argv) + cartan, points, port_position, cliques = geo.load_geometry() + lines = set(points) + p104 = {points[port_position[p]] for c in cliques[:13] for p in c} + scope = lines if args.scope == "T120" else p104 + count = 15 if args.scope == "T120" else 13 + rows = range(count) if args.rows == "all" else [int(r) for r in args.rows.split(",")] + seeds = {} + if args.incumbent: + for entry in json.loads(Path(args.incumbent).read_text()): + anf = 0 + for m in entry["monomials"]: + anf ^= 1 << m + seeds[entry["row"]] = (entry["charge"], anf) + out = [] + for index in rows: + clique = geo.Clique({points[port_position[p]] for p in cliques[index]}) + rng = random.Random("%d/%s/%d" % (args.seed, args.scope, index)) + weight, anf = best_host(scope, clique.set, rng, args.iterations, seeds.get(index)) + geo.check_host(anf, clique, scope) + monomials = [m for m in range(SIZE) if (anf >> m) & 1] + out.append({"scope": args.scope, "row": index, "charge": weight, "monomials": monomials}) + print("scope=%s row=%d charge=%d" % (args.scope, index, weight), flush=True) + if args.write: + Path(args.write).write_text(json.dumps(out, indent=1) + "\n") + + +if __name__ == "__main__": + main(sys.argv[1:]) diff --git a/research/p104-frame-host-minimum/verify.py b/research/p104-frame-host-minimum/verify.py new file mode 100644 index 0000000000..356843555a --- /dev/null +++ b/research/p104-frame-host-minimum/verify.py @@ -0,0 +1,714 @@ +#!/usr/bin/env python3 +"""Exact minimum hosting charges of the P104 frame-indicator rows. + +Setting (inherited from PR #7031 / #7047): the 120 root lines of E8 carry chart +points in F_2^8 (simple-root coordinates mod 2). A *host* of a row is a Boolean +function f on F_2^8 that equals the row's indicator on the root-line points; its +*charge* is the number of monomials of degree >= 2 in its algebraic normal form +(ANF) in the chart coordinates x0..x7. Affine terms are free, as in #7031/#7047. + +Facts checked here, all by exhaustive enumeration: + * the 120 chart points are exactly {x : Q(x) = 1} for the chart's quadratic form; + * each of the 15 odd 8-cliques (13 P104 frames, 2 excluded) is a coset of a + 3-dimensional subspace W_F; + * no host of degree <= 2 exists for any row (a 3-flat inside the root lines meets + the row in one point, and every polynomial of degree <= 2 sums to 0 on a 3-flat); + * the four #7031 forms (p, q, r, s) miss exactly one of their 16 values on the 120 + lines, so exactly two functions of them host frame 0: charge 40 and charge 16; + * exact minima over W_F-invariant functions (the five flat indicators are among + them) and over all hosts of degree <= 3, on the 120-line scope and on the 104 + P104-line scope; the five flat charges are listed on the 120-line scope; + * a letter-product baseline and explicit sparser hosts (data/hosts_*.json), each + re-evaluated at every scope point. + +Checks are need() failures, so python -O still runs them. No claim is made about +the minimum over all Boolean functions, about sums of products, or about kappa. +""" + +import hashlib +import json +import sys +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" +N = 8 +SIZE = 1 << N +FRAME0_PORTS = (11, 21, 38, 56, 140, 146, 161, 191) + +# Expected exact results (each is recomputed below and compared). +# per clique index 0..14: (sorted (|G|, charge) of the five flat hosts, invariant min, cubic min) +EXPECT_T120 = { + 0: ([(8, 63), (16, 39), (16, 39), (16, 40), (32, 16)], 16, 14), + 1: ([(8, 46), (16, 24), (16, 60), (16, 111), (32, 51)], 24, 24), + 2: ([(8, 42), (16, 26), (16, 58), (16, 89), (32, 49)], 26, 26), + 3: ([(8, 40), (16, 34), (16, 46), (16, 105), (32, 51)], 34, 22), + 4: ([(8, 48), (16, 36), (16, 44), (16, 83), (32, 39)], 36, 24), + 5: ([(8, 18), (16, 10), (16, 54), (16, 93), (32, 45)], 10, 18), + 6: ([(8, 102), (16, 35), (16, 84), (16, 84), (32, 27)], 27, 23), + 7: ([(8, 16), (16, 20), (16, 40), (16, 101), (32, 41)], 16, 14), + 8: ([(8, 58), (16, 42), (16, 54), (16, 111), (32, 51)], 42, 30), + 9: ([(8, 28), (16, 30), (16, 36), (16, 103), (32, 53)], 28, 28), + 10: ([(8, 24), (16, 26), (16, 40), (16, 107), (32, 49)], 24, 24), + 11: ([(8, 89), (16, 57), (16, 58), (16, 59), (32, 28)], 28, 21), + 12: ([(8, 21), (16, 13), (16, 49), (16, 90), (32, 42)], 13, 17), + 13: ([(8, 60), (16, 11), (16, 44), (16, 48), (32, 7)], 7, 7), + 14: ([(8, 40), (16, 34), (16, 40), (16, 87), (32, 53)], 34, 30), +} +# The unique minimiser among frame 0's hosts of degree <= 3 (charge 14), monomials in mask order. +EXPECT_FRAME0_CUBIC = ( + "1 + x0 + x1 + x2 + x0*x2 + x0*x3 + x0*x1*x3 + x0*x2*x3 + x4 + x0*x3*x4 + x5 + x1*x5 + x0*x1*x5 + " + "x2*x5 + x0*x2*x5 + x4*x5 + x6 + x5*x6 + x7 + x5*x7 + x0*x5*x7 + x0*x6*x7" +) +# Product-of-letters hosting words of #7031: the charge of the indicator of span(F). +EXPECT_LETTER_BASELINE = [40, 111, 89, 105, 83, 93, 35, 101, 111, 103, 107, 58, 90, 11, 87] +# Charges of the explicit hosts in data/hosts_*.json (search.py, 3000 orders per row, seed 20261110). +EXPECT_SEARCHED_T120 = [14, 20, 20, 22, 22, 6, 23, 10, 26, 18, 14, 21, 9, 7, 20] +EXPECT_SEARCHED_P104 = [14, 18, 16, 22, 19, 6, 23, 10, 23, 16, 14, 21, 9] +# 104-line scope (frames 0..12 only): (invariant min, cubic min) +EXPECT_P104 = { + 0: (15, 14), 1: (24, 24), 2: (26, 23), 3: (34, 22), 4: (36, 21), 5: (10, 18), + 6: (27, 23), 7: (16, 14), 8: (42, 30), 9: (28, 28), 10: (24, 24), 11: (28, 21), + 12: (13, 17), +} + + +def need(condition, message): + if not condition: + raise SystemExit(message) + + +# --------------------------------------------------------------------------- chart +def e8_roots(): + roots = [] + for left, right in combinations(range(8), 2): + for sl in (1, -1): + for sr in (1, -1): + vector = [0] * 8 + vector[left] = 2 * sl + vector[right] = 2 * sr + 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 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][c] - factor * rows[column][c] for c 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 negate(vector): + return tuple(-entry for entry in vector) + + +def load_geometry(): + """Return (cartan, chart points of the 120 lines, port -> line position).""" + basis = simple_basis() + matrix = list(zip(*basis)) + cartan = [[dot(basis[i], basis[j]) for j in range(8)] for i in range(8)] + 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") + points = [] + for root in lines: + bits = 0 + for index, value in enumerate(solve_coordinates(matrix, root)): + if value & 1: + bits |= 1 << index + points.append(bits) + need(len(set(points)) == 120, "chart points of the root lines are not distinct") + line_map = json.loads((REPO / "research/p104-port-window-haemers/data/e8_line_map.json").read_text()) + ports_p104 = json.loads((REPO / "research/p104-port-window-haemers/data/ports_p104.json").read_text())["ports"] + need(len(ports_p104) == 104 and len(set(ports_p104)) == 104, "expected 104 distinct P104 ports") + index = {} + for position, root in enumerate(lines): + index[root] = position + index[negate(root)] = position + port_position = {} + for vector, root in zip(line_map["vectors"], line_map["roots2"]): + port_position[vector] = index[tuple(root)] + need(len(port_position) == 120 and len(set(port_position.values())) == 120, "line map is not a bijection") + frame_bytes = (ROOT / "data" / "frames.json").read_bytes() + need(hashlib.sha256(frame_bytes).hexdigest() == FRAMES_SHA256, "frames.json sha256 mismatch") + frames_doc = json.loads(frame_bytes.decode()) + frames = frames_doc["frames"] + excluded = frames_doc["excluded_odd_cliques"] + need(len(frames) == 13 and len(excluded) == 2, "expected 13 frames and 2 excluded cliques") + need(tuple(frames[0]) == FRAME0_PORTS, "frame 0 ports changed") + need(set(ports_p104) == {p for frame in frames for p in frame}, "frames do not partition the P104 ports") + cliques = [tuple(c) for c in frames] + [tuple(c) for c in excluded] + need(sorted(p for c in cliques for p in c) == sorted(line_map["vectors"]), "cliques do not partition 120 lines") + return cartan, points, port_position, cliques + + +# ------------------------------------------------------------- boolean functions +# A function on F_2^8 is a 256-bit integer truth table (bit x is f(x)); its ANF is +# a 256-bit integer whose bit m says that the square-free monomial prod_{i in m} x_i +# occurs. The two are related by the (involutive) subset-sum transform. +LOW = [sum(1 << m for m in range(SIZE) if not (m >> j) & 1) for j in range(N)] +GE2 = sum(1 << m for m in range(SIZE) if bin(m).count("1") >= 2) + + +def mobius(table): + for j in range(N): + table ^= (table & LOW[j]) << (1 << j) + return table + + +def table_of(points): + table = 0 + for point in points: + table |= 1 << point + return table + + +def charge(anf): + return (anf & GE2).bit_count() + + +def eval_anf(anf, point): + """f(point) read directly from the ANF (independent of the transform).""" + value = 0 + for m in range(SIZE): + if (anf >> m) & 1 and m & ~point == 0: + value ^= 1 + return value + + +def poly_mul(left, right): + """Product of two ANFs (sets of monomial masks) over F_2 with x_i^2 = x_i.""" + out = set() + for a in left: + for b in right: + out ^= {a | b} + return out + + +def anf_set(anf): + return {m for m in range(SIZE) if (anf >> m) & 1} + + +def anf_int(monomials): + value = 0 + for m in monomials: + value ^= 1 << m + return value + + +def monomial_name(mask): + return "1" if mask == 0 else "*".join("x%d" % i for i in range(N) if (mask >> i) & 1) + + +def f2_span(vectors): + span = {0} + for vector in vectors: + if vector not in span: + span |= {s ^ vector for s in span} + return span + + +def f2_rank(vectors): + basis = {} + for vector in vectors: + x = vector + while x: + top = x.bit_length() - 1 + if top in basis: + x ^= basis[top] + else: + basis[top] = x + break + return len(basis) + + +def quadratic_form(cartan): + edges = [(i, j) for i in range(8) for j in range(i + 1, 8) if cartan[i][j] & 1] + need(len(edges) == 7, "the E8 diagram has 7 edges") + def q(x): + return (bin(x).count("1") + sum(((x >> i) & (x >> j)) & 1 for i, j in edges)) & 1 + return q, edges + + +def all_subspaces(dimension): + subspaces = {frozenset([0])} + frontier = [frozenset([0])] + while frontier: + new = [] + for space in frontier: + for vector in range(1, 1 << dimension): + if vector not in space: + bigger = frozenset(space | {s ^ vector for s in space}) + if bigger not in subspaces: + subspaces.add(bigger) + new.append(bigger) + frontier = new + return subspaces + + +# ----------------------------------------------------------- per-clique analysis +class Clique: + """Quotient data of F_2^8 by the translation space W_F of a clique F.""" + + def __init__(self, points_of_clique): + self.points = sorted(points_of_clique) + self.set = set(self.points) + anchor = self.points[0] + self.anchor = anchor + self.direction = f2_span([x ^ anchor for x in self.points[1:]]) + need(len(self.direction) == 8, "a clique is not a coset of a 3-dimensional subspace") + need({anchor ^ w for w in self.direction} == self.set, "a clique is not a full coset") + reps = sorted({min(x ^ w for w in self.direction) for x in range(SIZE)}) + need(len(reps) == 32, "expected 32 cosets") + basis, span = [], set(self.direction) + for rep in reps: + if rep not in span: + basis.append(rep) + span |= {s ^ rep for s in span} + if len(basis) == 5: + break + need(len(span) == SIZE, "coset representatives do not span F_2^8") + self.coset_of = {} + for z in range(32): + vector = 0 + for i in range(5): + if (z >> i) & 1: + vector ^= basis[i] + for w in self.direction: + self.coset_of[vector ^ w] = z + self.cosets = {z: [x for x in range(SIZE) if self.coset_of[x] == z] for z in range(32)} + self.z0 = self.coset_of[anchor] + + +def invariant_class(clique, scope): + """All W_F-invariant hosts on `scope`: base indicator of F plus free cosets.""" + touched = Counter(clique.coset_of[x] for x in scope if x not in clique.set) + need(clique.z0 not in touched, "the clique's coset meets another scope point") + free = [z for z in range(32) if z != clique.z0 and z not in touched] + base = mobius(table_of(clique.cosets[clique.z0])) + deltas = [mobius(table_of(clique.cosets[z])) for z in free] + current, hosts = base, [base] + for index in range(1, 1 << len(free)): + current ^= deltas[(index & -index).bit_length() - 1] + hosts.append(current) + return free, hosts + + +def flat_hosts(clique, scope, subspaces5): + """Flat indicators G (containing F) with G meeting `scope` only inside F.""" + found = [] + for space in subspaces5: + flat = [x for z in space for x in clique.cosets[z ^ clique.z0]] + if all(x not in scope or x in clique.set for x in flat): + found.append((len(flat), charge(mobius(table_of(flat))), anf_set(mobius(table_of(flat))))) + found.sort(key=lambda item: (item[0], item[1])) + return found + + +def check_host(anf, clique, scope): + """Evaluate the ANF directly at every scope point and compare with the indicator.""" + monomials = [m for m in range(SIZE) if (anf >> m) & 1] + for x in scope: + value = 0 + for m in monomials: + if m & ~x == 0: + value ^= 1 + need(value == (1 if x in clique.set else 0), "a claimed host disagrees with the indicator") + + +def solve_f2(rows, rhs, unknowns): + """Return (particular solution, null-space basis) over F_2, or None if inconsistent.""" + pivots = {} + for row, value in zip(rows, rhs): + x, y = row, value + while x: + top = x.bit_length() - 1 + if top in pivots: + px, py = pivots[top] + x ^= px + y ^= py + else: + pivots[top] = (x, y) + break + else: + if y: + return None + for p in sorted(pivots): + xp, yp = pivots[p] + for q in list(pivots): + if q != p and (pivots[q][0] >> p) & 1: + pivots[q] = (pivots[q][0] ^ xp, pivots[q][1] ^ yp) + free = [c for c in range(unknowns) if c not in pivots] + particular = 0 + for p, (x, y) in pivots.items(): + if y: + particular |= 1 << p + null = [] + for f in free: + vector = 1 << f + for p, (x, y) in pivots.items(): + if (x >> f) & 1: + vector |= 1 << p + null.append(vector) + return particular, null + + +def low_degree_hosts(clique, scope, degree): + """All hosts of degree <= `degree` as ANF integers, or None if there is none.""" + monomials = [m for m in range(SIZE) if bin(m).count("1") <= degree] + column = {m: i for i, m in enumerate(monomials)} + rows, rhs = [], [] + for x in scope: + row = 0 + for m in monomials: + if m & ~x == 0: + row |= 1 << column[m] + rows.append(row) + rhs.append(1 if x in clique.set else 0) + solved = solve_f2(rows, rhs, len(monomials)) + if solved is None: + return None + particular, null = solved + + def lift(vector): + anf = 0 + for m, i in column.items(): + if (vector >> i) & 1: + anf |= 1 << m + return anf + + base = lift(particular) + deltas = [lift(v) for v in null] + current, hosts = base, [base] + for index in range(1, 1 << len(deltas)): + current ^= deltas[(index & -index).bit_length() - 1] + hosts.append(current) + return hosts, len(deltas) + + +def three_flat_certificate(clique, quad): + """A 3-flat S inside the 120 lines with |S ∩ F| = 1. + + S = a + U with a in F and U a 3-dimensional subspace, U ∩ W_F = {0}, on which + Q(a + u) = 1 for every u in U. Then sum_{x in S} 1_F(x) = 1, while every + polynomial of degree <= 2 sums to 0 over a 3-flat. + """ + a = clique.anchor + good = [w for w in range(1, SIZE) if quad(a ^ w) == 1] + good_set = set(good) + for d1 in good: + if d1 in clique.direction: + continue + for d2 in good: + if d2 <= d1 or (d1 ^ d2) not in good_set or d2 in clique.direction: + continue + if (d1 ^ d2) in clique.direction: + continue + for d3 in good: + if d3 <= d2: + continue + span = f2_span([d1, d2, d3]) + if len(span) != 8 or span & clique.direction != {0}: + continue + if all(w == 0 or w in good_set for w in span): + return a, (d1, d2, d3), sorted(a ^ w for w in span) + return None + + +def check_structure(quad, lines_t, clique_data): + """Lemma behind the 28 + 3 + 1 coset pattern, checked on every clique. + + Let F = a + W be an odd 8-clique and B(x, y) = Q(x+y) + Q(x) + Q(y). Since Q = 1 + on F, Q(a + w) = 1 for w in W, so W is totally isotropic and Q(w) = B(a, w). + For a coset c + W, Q(c + w) = Q(c) + B(a + c, w): constant if a + c lies in the + 5-dimensional space W-perp, otherwise a non-constant affine function that takes + each value on exactly 4 of the 8 points. The translate Q'(x) = Q(a + x) + Q(a) + has 120 zeros, so it is elliptic; W is totally singular for Q', hence maximal, + and W-perp / W is anisotropic, so Q' = 1 on W-perp minus W. Therefore the 4 + cosets inside a + W-perp are F (8 lines) and 3 cosets with no root line, and the + other 28 cosets hold 4 lines each: 8 + 28 * 4 = 120. + """ + def polar(x, y): + return quad(x ^ y) ^ quad(x) ^ quad(y) + + for index, clique in enumerate(clique_data): + a = clique.anchor + perp = [u for u in range(SIZE) if all(polar(u, w) == 0 for w in clique.direction)] + need(len(perp) == 32 and all(w in perp for w in clique.direction), "W-perp has the wrong size") + for w in clique.direction: + need(quad(a ^ w) == 1, "Q is not 1 on a clique") + need(all(polar(w, v) == 0 for v in clique.direction), "W is not totally isotropic") + need(sum(1 for x in range(SIZE) if quad(a ^ x) ^ quad(a) == 0) == 120, "Q' is not elliptic") + biggest = {a ^ u for u in perp} + need(biggest & lines_t == clique.set, "a + W-perp meets the lines outside the clique") + sizes = Counter(sum(1 for x in clique.cosets[z] if x in lines_t) for z in range(32)) + need(dict(sizes) == {8: 1, 4: 28, 0: 3}, "coset pattern changed for clique %d: %s" % (index, dict(sizes))) + inside = {clique.coset_of[x] for x in biggest} + need(len(inside) == 4 and all(sum(1 for x in clique.cosets[z] if x in lines_t) in (0, 8) for z in inside), + "the four cosets of a + W-perp are not F and three empty cosets") + for z in range(32): + if z not in inside: + ones = [quad(x) for x in clique.cosets[z]] + need(sorted(ones) == [0] * 4 + [1] * 4, "a coset outside W-perp is not balanced") + return True + + +def main(argv): + cartan, points, port_position, cliques = load_geometry() + quad, edges = quadratic_form(cartan) + lines_t = set(points) + need({x for x in range(SIZE) if quad(x)} == lines_t, "the 120 chart points are not {Q = 1}") + p104 = {points[port_position[p]] for c in cliques[:13] for p in c} + need(len(p104) == 104 and len(lines_t - p104) == 16, "P104 scope sizes changed") + clique_data = [Clique({points[port_position[p]] for p in c}) for c in cliques] + subspaces5 = all_subspaces(5) + need(len(subspaces5) == 374, "subspace count of F_2^5 changed") + check_structure(quad, lines_t, clique_data) + + # ---- frame 0 four-form class (open question 2 of #7047) + p_form = lambda x: 1 ^ ((x >> 1) & 1) ^ ((x >> 2) & 1) ^ ((x >> 4) & 1) + q_form = lambda x: x & 1 + r_form = lambda x: (x >> 5) & 1 + s_form = lambda x: ((x >> 6) & 1) ^ ((x >> 7) & 1) + image, fibres = {}, {} + frame0 = clique_data[0] + for x in lines_t: + key = (p_form(x), q_form(x), r_form(x), s_form(x)) + image.setdefault(key, set()).add(1 if x in frame0.set else 0) + fibres[key] = fibres.get(key, 0) + 1 + need(all(len(v) == 1 for v in image.values()), "the indicator is not constant on a four-form fibre") + missing = [(a, b, c, d) for a in (0, 1) for b in (0, 1) for c in (0, 1) for d in (0, 1) if (a, b, c, d) not in image] + need(missing == [(0, 0, 0, 1)], "missing four-form fibres changed: %s" % (missing,)) + need(set(fibres.values()) == {8}, "every attained four-form fibre should hold 8 lines") + # explicit expansions by polynomial multiplication (independent of the transform) + one = {0} + P = {0, 1 << 1, 1 << 2, 1 << 4} + Qf, R, S = {1}, {1 << 5}, {1 << 6, 1 << 7} + comp = lambda f: f ^ one + product_host = poly_mul(poly_mul(comp(Qf), P), poly_mul(comp(R), comp(S))) + delta_missing = poly_mul(poly_mul(comp(P), comp(Qf)), poly_mul(comp(R), S)) + three_form_host = product_host ^ delta_missing + direct = poly_mul(poly_mul(comp(Qf), comp(R)), P ^ S) + need(three_form_host == direct, "(1+q)(1+r)(p+s) is not the product plus the missing fibre") + four_form = sorted([charge(anf_int(product_host)), charge(anf_int(three_form_host))]) + need(four_form == [16, 40], "four-form charges changed: %s" % four_form) + for host in (product_host, three_form_host): + check_host(anf_int(host), frame0, lines_t) + # the same two hosts from the transform of the truth tables + tables = [] + for host in (product_host, three_form_host): + anf = anf_int(host) + tables.append(sum(1 << x for x in range(SIZE) if eval_anf(anf, x))) + need(mobius(tables[-1]) == anf, "transform and expansion disagree") + + # ---- degree-2 impossibility certificates, all 15 cliques + certificates = [] + for index, clique in enumerate(clique_data): + cert = three_flat_certificate(clique, quad) + need(cert is not None, "no 3-flat certificate for clique %d" % index) + a, dirs, flat = cert + need(all(x in lines_t for x in flat) and len(flat) == 8, "certificate flat leaves the lines") + need(sum(1 for x in flat if x in clique.set) == 1, "certificate flat meets the clique evenly") + for degree_mask in range(SIZE): + if bin(degree_mask).count("1") <= 2: + parity = 0 + for x in flat: + parity ^= 1 if degree_mask & ~x == 0 else 0 + need(parity == 0, "a monomial of degree <= 2 does not sum to 0 on a 3-flat") + certificates.append((index, a, dirs)) + + # ---- per-clique exact minima in the named classes, two scopes + results = {} + for scope_name, scope in (("T120", lines_t), ("P104", p104)): + for index, clique in enumerate(clique_data): + if scope_name == "P104" and index >= 13: + continue + low2 = low_degree_hosts(clique, scope, 2) + need(low2 is None, "a host of degree <= 2 exists (%s, clique %d)" % (scope_name, index)) + free, hosts = invariant_class(clique, scope) + for anf in hosts: + check_host(anf, clique, scope) + invariant_min = min(charge(h) for h in hosts) + flats = flat_hosts(clique, scope, subspaces5) + for _, _, mons in flats: + check_host(anf_int(mons), clique, scope) + cubic, nullity = low_degree_hosts(clique, scope, 3) + cubic_min = min(charge(h) for h in cubic) + best_cubic = min(cubic, key=lambda h: (charge(h), h)) + check_host(best_cubic, clique, scope) + best_invariant = min(hosts, key=lambda h: (charge(h), h)) + if scope_name == "T120": + results[index] = { + "free": len(free), "flats": [(g, c) for g, c, _ in flats], "invariant_min": invariant_min, + "cubic_min": cubic_min, "cubic_nullity": nullity, "cubic_min_count": sum(1 for h in cubic if charge(h) == cubic_min), + "invariant_best": best_invariant, "cubic_best": best_cubic, + } + else: + results[("P104", index)] = {"free": len(free), "invariant_min": invariant_min, "cubic_min": cubic_min, "cubic_nullity": nullity} + + # ---- compare with the expected tables + for index in range(15): + flats, inv_min, cubic_min = EXPECT_T120[index] + got = results[index] + need(got["flats"] == flats, "flat charges changed for clique %d: %s" % (index, got["flats"])) + need(got["invariant_min"] == inv_min and got["cubic_min"] == cubic_min, + "class minima changed for clique %d: %s" % (index, (got["invariant_min"], got["cubic_min"]))) + need(got["cubic_nullity"] == 9, "cubic host space should have dimension 9") + need(got["free"] == 3, "expected three free cosets on the 120-line scope") + need(min(c for _, c in flats) == inv_min, "the best W_F-invariant host is not a flat indicator") + for index in range(13): + inv_min, cubic_min = EXPECT_P104[index] + got = results[("P104", index)] + need((got["invariant_min"], got["cubic_min"]) == (inv_min, cubic_min), "P104-scope minima changed for frame %d" % index) + need(got["cubic_nullity"] == 11, "cubic host space on the 104 lines should have dimension 11") + + # baseline: the product-of-letters hosts of #7031. A letter of root line l is + # 1 + B(l, x); it equals 1 on a clique F exactly when l lies in F, because + # F-perp = span(F) = F + W_F meets the root lines only in F. A product of letters + # is the indicator of the common-1 set, here span(F), so the baseline charge of a + # row is the charge of span(F). + def polar(x, y): + return quad(x ^ y) ^ quad(x) ^ quad(y) + + letter_vectors = [sum(polar(l, 1 << i) << i for i in range(N)) | (1 << N) for l in lines_t] + need(f2_rank(letter_vectors) == 9, "the 120 letters do not span the affine functions") + letter_baseline = [] + for index, clique in enumerate(clique_data): + span = set(clique.points) | clique.direction + need(len(span) == 16 and span & lines_t == clique.set, "span(F) meets the lines outside F") + common = {x for x in range(SIZE) if all(polar(l, x) == 0 for l in clique.points)} + need(common == span, "the common-1 set of the frame letters is not span(F)") + ones = {l for l in lines_t if all(polar(l, f) == 0 for f in clique.points)} + need(ones == clique.set, "a non-frame letter equals 1 on the whole clique") + letter_baseline.append(charge(mobius(table_of(span)))) + need(any(g == 16 and c == letter_baseline[-1] for g, c in results[index]["flats"]), + "the letter-product host is not among the five flat hosts") + need(letter_baseline == EXPECT_LETTER_BASELINE, "letter-product baseline changed: %s" % letter_baseline) + need(letter_baseline[0] == 40 and letter_baseline[1] == 111, "baseline disagrees with #7031 / #7046") + + need(results[0]["cubic_min_count"] == 1, "frame 0 should have a unique cubic minimiser") + shown = " + ".join(monomial_name(m) for m in sorted(anf_set(results[0]["cubic_best"]))) + need(shown == EXPECT_FRAME0_CUBIC, "the frame-0 charge-14 host changed: %s" % shown) + + # the cubic hosts are f + (1+Q) * (affine function): verify the 9-dimensional kernel + quad_anf = {1 << i for i in range(N)} ^ {(1 << i) | (1 << j) for i, j in edges} + ideal_gens = [poly_mul(comp(quad_anf), {0 if k == 8 else (1 << k)}) for k in range(9)] + for gen in ideal_gens: + need(all(eval_anf(anf_int(gen), x) == 0 for x in lines_t), "(1+Q)*affine does not vanish on the lines") + need(f2_rank([anf_int(g) for g in ideal_gens]) == 9, "(1+Q)*affine generators are dependent") + need(all(max(bin(m).count("1") for m in g) <= 3 for g in ideal_gens), "an ideal generator has degree > 3") + + # cross-method checks: the hosts expanded by polynomial multiplication must occur in + # both enumerations (one built from cosets, one from the linear system) + free0, invariant0 = invariant_class(clique_data[0], lines_t) + cubic0, _ = low_degree_hosts(clique_data[0], lines_t, 3) + for host in (product_host, three_form_host): + need(anf_int(host) in set(invariant0), "a four-form host is missing from the invariant class") + need(anf_int(three_form_host) in set(cubic0), "the three-form host is missing from the cubic class") + need(anf_int(product_host) not in set(cubic0), "the 40-monomial product has degree 4, not 3") + + # failure controls: each deliberately wrong statement must be rejected + broken = set(three_form_host) + broken ^= {sorted(three_form_host)[-1]} + for rejected in (broken, product_host ^ {0b11}): + try: + check_host(anf_int(rejected), frame0, lines_t) + except SystemExit: + continue + raise SystemExit("a corrupted host was accepted") + wrong_forms = lambda x: (p_form(x) ^ ((x >> 3) & 1), q_form(x), r_form(x), s_form(x)) + wrong_image = {} + for x in lines_t: + wrong_image.setdefault(wrong_forms(x), set()).add(1 if x in frame0.set else 0) + need(any(len(v) > 1 for v in wrong_image.values()), "a wrong form should make the indicator non-constant on a fibre") + # an even-parity 3-flat (the clique itself) gives no obstruction to a quadratic host + need(sum(1 for x in frame0.points if x in frame0.set) % 2 == 0, "the clique is an even flat") + + # explicit sparse hosts from search.py (upper bounds): re-evaluate every one directly + searched = {} + for scope_name, scope in (("T120", lines_t), ("P104", p104)): + path = ROOT / "data" / ("hosts_%s.json" % scope_name) + entries = json.loads(path.read_text()) + need([e["row"] for e in entries] == list(range(15 if scope_name == "T120" else 13)), + "hosts_%s.json must list rows in order" % scope_name) + for entry in entries: + need(entry["scope"] == scope_name, "host entry has the wrong scope") + anf = anf_int(set(entry["monomials"])) + need(len(set(entry["monomials"])) == len(entry["monomials"]), "a host lists a monomial twice") + need(charge(anf) == entry["charge"], "recorded charge is wrong for %s row %d" % (scope_name, entry["row"])) + check_host(anf, clique_data[entry["row"]], scope) + searched[(scope_name, entry["row"])] = (entry["charge"], anf) + for index in range(15): + class_best = min(results[index]["invariant_min"], results[index]["cubic_min"]) + need(searched[("T120", index)][0] <= class_best, "the search missed a class optimum on row %d" % index) + for index in range(13): + need(searched[("P104", index)][0] <= searched[("T120", index)][0], "a 120-line host should also host on 104 lines") + class_best = min(results[("P104", index)]["invariant_min"], results[("P104", index)]["cubic_min"]) + need(searched[("P104", index)][0] <= class_best, "the search missed a P104 class optimum on row %d" % index) + searched_t120 = [searched[("T120", i)][0] for i in range(15)] + searched_p104 = [searched[("P104", i)][0] for i in range(13)] + need(searched_t120 == EXPECT_SEARCHED_T120, "explicit 120-line host charges changed: %s" % searched_t120) + need(searched_p104 == EXPECT_SEARCHED_P104, "explicit 104-line host charges changed: %s" % searched_p104) + need(sum(searched_t120[:13]) == 225 and sum(searched_p104) == 211, "explicit host totals changed") + below = [i for i in range(15) if searched_t120[i] < min(results[i]["invariant_min"], results[i]["cubic_min"])] + need(below == [1, 2, 4, 5, 7, 8, 9, 10, 12, 14], "rows below the exact class minima changed: %s" % below) + + if "--table" in argv: + print("| row | letter product | exact flat/invariant min | exact cubic min | explicit host, 120 lines | explicit host, 104 lines |") + for index in range(15): + r = results[index] + p104_cell = searched_p104[index] if index < 13 else "-" + print("| %s%d | %d | %d | %d | %d | %s |" % ( + "F" if index < 13 else "X", index if index < 13 else index - 13, + letter_baseline[index], r["invariant_min"], r["cubic_min"], searched_t120[index], p104_cell)) + print("exact P104-scope (invariant, cubic) per frame:", [EXPECT_P104[i] for i in range(13)]) + if "--show" in argv: + r = results[0] + print("frame 0 three-form host (charge 16): (1+x0)(1+x5)(1+x1+x2+x4+x6+x7)") + for name, anf in (("invariant best", r["invariant_best"]), ("cubic best", r["cubic_best"])): + print(name, charge(anf), " + ".join(monomial_name(m) for m in sorted(anf_set(anf)))) + print( + "PASS_P104_FRAME_HOST_MINIMUM frame0_four_form_min=16 frame0_product=40 frame0_cubic_min=14 " + "no_degree2_host=15 free_cosets=3 flats_per_row=5 rows=15 structure=28+3+1 " + "letter_baseline_sum_13=%d searched_t120=%s searched_p104=%s sum_t120_13=%d sum_p104_13=%d" + % (sum(letter_baseline[:13]), ",".join(map(str, searched_t120)), ",".join(map(str, searched_p104)), + sum(searched_t120[:13]), sum(searched_p104)) + ) + + +if __name__ == "__main__": + main(sys.argv[1:])