diff --git a/research/eisenstein-submatrix-copy-floor/AUTOMORPHISMS.json b/research/eisenstein-submatrix-copy-floor/AUTOMORPHISMS.json new file mode 100644 index 0000000000..1172ea1b06 --- /dev/null +++ b/research/eisenstein-submatrix-copy-floor/AUTOMORPHISMS.json @@ -0,0 +1 @@ +{"base_pair": [0, 1], "generators": [[0, 2, 1, 3, 4, 6, 5, 10, 9, 8, 7, 11, 20, 21, 23, 22, 27, 26, 25, 24, 12, 13, 15, 14, 19, 18, 17, 16, 29, 28, 30, 31, 34, 35, 32, 33, 37, 36, 38, 39], [0, 3, 13, 1, 20, 5, 18, 9, 16, 7, 14, 21, 12, 2, 10, 23, 8, 27, 6, 25, 4, 11, 26, 15, 24, 19, 22, 17, 28, 29, 37, 33, 38, 31, 36, 35, 34, 30, 32, 39], [0, 4, 12, 1, 21, 8, 15, 6, 19, 10, 17, 20, 13, 2, 5, 24, 9, 22, 7, 26, 3, 11, 23, 16, 27, 14, 25, 18, 29, 28, 36, 34, 37, 32, 38, 30, 31, 33, 35, 39], [0, 5, 15, 1, 22, 10, 13, 4, 16, 7, 19, 23, 14, 2, 3, 26, 8, 20, 9, 25, 6, 11, 21, 18, 24, 12, 27, 17, 30, 31, 37, 33, 36, 34, 39, 28, 29, 35, 32, 38], [1, 2, 0, 3, 4, 5, 6, 7, 8, 9, 10, 11, 29, 28, 31, 30, 33, 32, 35, 34, 13, 12, 15, 14, 17, 16, 19, 18, 20, 21, 22, 23, 24, 25, 26, 27, 36, 37, 38, 39]]} \ No newline at end of file diff --git a/research/eisenstein-submatrix-copy-floor/README.md b/research/eisenstein-submatrix-copy-floor/README.md new file mode 100644 index 0000000000..1c4f3f947f --- /dev/null +++ b/research/eisenstein-submatrix-copy-floor/README.md @@ -0,0 +1,138 @@ +# Eisenstein E8 decoder copy floor: 23, past the clique-method limit + +**Research note; no new supplier, no κ change, selected record untouched.** +In the abstract Eisenstein E8 scalar binary decoder model of +[`research/eisenstein-clique-copy-bound`](../eisenstein-clique-copy-bound/PROOF.md) +(Jonathan Lam, PR798), every fitting decomposition costs **at least 23** +Eisenstein pairing-rank units. PR798 proved 22 and showed that *no* weighting +of cliques can prove more. This package adds the ingredient that its PROOF.md +says is needed: rank bounds on non-clique principal submatrices. + +```sh +python3 -B research/eisenstein-submatrix-copy-floor/verify.py +``` + +Expected (about 35 s, standard library only, any CPython 3.10+): + +```text +PASS_EISENSTEIN_SUBMATRIX_COPY_FLOOR: C >= 23; objective 30200/1367; 296321 flat pairs; 540 S_uw sets minrank 10; 5 controls; no new kappa +``` + +The geometry (40 K-lines, orthogonality, all 772 flats, pairing ranks, all +cliques) is imported unchanged from PR798's pinned `geometry.py`. + +## Model (PR798, unchanged) + +`B` is a 40×40 matrix over F2 with `B_tt = 1` and `B_ts = 0` for distinct +nonorthogonal lines; entries on orthogonal pairs are free in both directions. +A decomposition `B = Σ_j 1_Rj 1_Aj^T` costs `C = Σ_j c(R_j, A_j)`, with +`c(R,A) = rank_Q(V_R V_A^T)/2`. `N[x]` is `x` plus its 27 nonorthogonal lines. + +## Proof + +**Lemma 1 (zero-cost totals can be dropped).** If `c(R,A) = 0` then +`X_R ⊥ X_A`, so every `(t,s) ∈ R×A` is an orthogonal pair of distinct lines +(the form is positive definite): a free entry. Deleting all zero-cost totals +leaves a fitting matrix `B'` and the same cost. + +**Lemma 2 (submatrix rank).** For a line set `S` let `m(S)` be the least F2 +rank of `B[S,S]` over all fitting `B`. For `B'` from Lemma 1, +`m(S) ≤ rank B'[S,S] ≤ #{j : c_j ≥ 1, R_j meets S, A_j meets S}`. Hence any +weights `λ_S ≥ 0` with + + Σ_S λ_S [F meets S][G meets S] ≤ c(F,G) for all flats F, G with c(F,G) ≥ 1 (★) + +prove `C ≥ Σ_S λ_S m(S)`. Closure keeps `c` and can only add hits, so flats +suffice, exactly as in PR798. Cliques (`m(Q) = |Q|`) are PR798's method. +Asymmetric row/column sets add nothing. Define `m(P,Q)` as the least rank +of `B[P,Q]` over fitting `B`. Every entry of `B[P,Q]` outside `(P∩Q)²` is off +the diagonal, so it is zero or free; setting the free ones to zero gives +`m(P,Q) = m(P∩Q)`, while the hit count for `(P,Q)` is at least that for `P∩Q`. + +**The new sets.** For distinct nonorthogonal `u, w`, let `S_uw = N[u] ∩ N[w]` +(20 lines; 540 sets). `u` and `w` are nonorthogonal to every line of `S_uw`, so +`B[S_uw,S_uw] = I_2 ⊕ B[core]` with an 18-line core, and `m(S_uw) = 2 + m(core)`. + +**Lemma 3 (m(core) = 8).** The core's largest clique `Q` has 5 lines. Any +factorization `B = U V^T` with 7 columns can be normalized to +`U[Q] = V[Q] = [I_5 | 0]` (since `U[Q] V[Q]^T = I_5`, transform by an invertible +`M` with `U[Q] M = [I_5|0]`, then by `[[I,0],[W^T,I]]` to clear the rest of +`V[Q]`). Then each other line `v` has `U[v] = (B[v,Q], s_v)`, +`V[v] = (B[Q,v]^T, t_v)` with `s_v, t_v ∈ F2²`, and every remaining entry is +`B[v,Q]·B[Q,w] + s_v·t_w`. The verifier enumerates all fixed-entry-respecting +choices by exhaustive backtracking and finds none: no fitting completion of +rank ≤ 7. A rank-8 completion exists and is rebuilt and rank-checked. So +`m(S_uw) = 10`. The greedy clique bound gives only 5 + 2 = 7, and the +chromatic (orthogonal-frame) bound gives 10: F2 cancellation does not help here. + +**Symmetry.** Five pinned permutations (`AUTOMORPHISMS.json`) preserve the +nonorthogonality graph and generate a group transitive on all 540 +nonorthogonal pairs (checked by orbit closure). An automorphism maps the fitting +pattern to itself and `S_uw` to `S_(gu)(gw)`, so the exhaustive search runs once. + +**Certificate.** Weights `184/6835` on each singleton, `13/13670` on each of +the 2,880 seven-cliques and `7/20505` on each `S_uw` satisfy (★) on all +296,321 flat pairs with positive cost (601 tight), checked in exact +arithmetic. The objective is + + 40·184/6835 + 2880·7·13/13670 + 540·10·7/20505 = 30200/1367 ≈ 22.0922. + +Costs are integers, so **C ≥ 23**. + +## Why this works, and how far it goes + +Under PR798's optimal clique dual (1/24 on the 240 pairs of twelve-line flats +with `c = 2`, 1/2 on full/full), a set `S` is "priced" at +`1/2 + e/24`, where `e` counts orthogonal pairs `(x,y)` with `S` meeting both +`x^⊥` and `y^⊥`. A set can lift the bound only if `m(S)` exceeds its price. +`S_uw` is priced at 9.5 and has `m = 10`; the whole pattern is priced at 10.5 +with minrank 10. + +Exploration (not part of the replay): we enumerated the 858,299 sets +`S = ⋂_{a∈A} N[a]` that are maximal for their hit pattern (every set has the +same price as such a set and at most its minrank), grouped them into 78 +classes by (|A|, |S|, price), computed one minrank per class by SAT with the +Lemma 3 normalization, and solved the class-uniform LP. Only the `S_uw` class +violates the clique dual, and the LP optimum is again 30200/1367. If those +classes are orbits of the graph's automorphism group (not checked), then +30200/1367 would be the exact optimum of the whole principal-submatrix method, +and pushing past 23 would need yet another ingredient. This is conditional. + +## Consequences and scope + +- The abstract optimum moves from [22,40] to **[23,40]**. PR1794's necessary + window for a beating Eisenstein supplier (C ≤ 31, ≤ 29 at the best window) + shrinks to 23..31. PR798's conditional Dfc three-stage window (C = 22..26) + becomes 23..26. Neither route is closed. +- Same model and premises as PR798: whole K-lines, scalar binary totals, the + stated fitting pattern, and PR446's pairing-rank premise for any physical + reading. Nonlinear messages (the separate `eisenstein-message-copy-bound` + package) and sub-line operations are not covered. +- This is a written proof with exhaustive finite premises, checked by a stdlib + replay; no proof assistant and no independent human review. + +## Open next questions + +1. **Is 30200/1367 the exact limit of principal-submatrix certificates?** + Why: it tells the next prover whether more set families can help. First + step: verify that the 78 classes are automorphism orbits (or give per-class + rank witnesses) and exhibit the dual. Blocker: none; about one session. +2. **A cost-aware ingredient.** The Gaussian planar theorem + (`gaussian-e8-asymmetric-copy`) charges a total by how its support's rank + deficit relates to support size. Adapting that idea to the 12-line Eisenstein + hyperplanes (the tight dual pairs here) might lift the bound further. First step: + restrict to decompositions whose totals have K-rank-≤3 joint support. + Blocker: the Eisenstein planes have up to four lines, so the matching + argument changes. +3. **Upper side.** No decoder cheaper than 40 is known. A SAT/ILP search over + non-clean supports at cost ≤ 31 would test PR1794's remaining window directly. + +## Credit + +Model, geometry, clique certificate and the method-limit theorem: Jonathan Lam +(@jonathanlam), PR798, with PR620's archived geometry (Joel Pulikkan / +GamingPuzzled). Weighted-clique method: Douglas R. Colkitt (PR703) and Sagar +Thakrar (PR738). Window and prize screen: Maximooch (PR1794). The pointer to +this target: DreamingOfClouds' note in discussion 1167. New material: Josie +Elliston, prepared with Claude Opus 5.5 (Anthropic) via Claude Code, which did +the search, proof and verifier. Apache-2.0. diff --git a/research/eisenstein-submatrix-copy-floor/RESULT.json b/research/eisenstein-submatrix-copy-floor/RESULT.json new file mode 100644 index 0000000000..a0417192e8 --- /dev/null +++ b/research/eisenstein-submatrix-copy-floor/RESULT.json @@ -0,0 +1,10 @@ +{ + "cliques7": 2880, + "controls": 5, + "copy_floor": 23, + "core_rank8_witness_rank": 8, + "flat_pairs_with_positive_cost": 296321, + "objective": "30200/1367", + "s20_sets": 540, + "tight": 601 +} diff --git a/research/eisenstein-submatrix-copy-floor/SOURCES.json b/research/eisenstein-submatrix-copy-floor/SOURCES.json new file mode 100644 index 0000000000..421b4794bc --- /dev/null +++ b/research/eisenstein-submatrix-copy-floor/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "06c96f5579bb67ed1b86d334e78fbed7da6945f1", + "sha256": "6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075" + }, + { + "path": "research/eisenstein-clique-copy-bound/PROOF.md", + "usage": "input", + "git_blob": "5c5fd2f87ce3c4e61ed782ceaa623edd80811349", + "sha256": "b75539c196ed45f23cf238413da9684dcba503f6630ad68a9648ecacf6aada3f" + }, + { + "path": "research/eisenstein-clique-copy-bound/geometry.py", + "usage": "input", + "git_blob": "a92c16295d6fcf2a7ffeb7d38444613f939db6cb", + "sha256": "248df3fb820b5165ca485ad4d43f0271043498c45a59ac1edc310a124073644c" + } + ] +} diff --git a/research/eisenstein-submatrix-copy-floor/TASK.json b/research/eisenstein-submatrix-copy-floor/TASK.json new file mode 100644 index 0000000000..ad2e4b6e65 --- /dev/null +++ b/research/eisenstein-submatrix-copy-floor/TASK.json @@ -0,0 +1,78 @@ +{ + "schema_version": 1, + "task_id": "complex-rank-shape-decoder", + "priority_revision": 3, + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "original_card": { + "id": "complex-rank-shape-decoder", + "question": "Can a decoder deliver the local paid mass in fewer, larger-rank children (block frame climbs instead of rank-1 to rank-3 steps)?", + "starting_points": [ + "research/complex-local-word-ceiling/README.md", + "research/complex-decoder-field-extension-seed44/README.md", + "research/complex-frame-pair-decoders/README.md" + ], + "methods": [ + "Find one exact small decoding identity whose frame path climbs in blocks, and price its complete per-call profile.", + "Bound the best effective child rank achievable for one fixed support alphabet, including copies, frames and restoration." + ], + "acceptance_gate": "A per-call local profile, with all copied information, frames and restoration counted, whose ceiling exceeds the selected word's by at least 5%; masked or overcomplete supports must change an assumption of the eight-term all-pairs bound.", + "first_step": { + "command": [ + "python3", + "-B", + "research/complex-local-word-ceiling/verify.py" + ], + "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING", + "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.", + "scope": "Positive control and planning budget only; this is not a new construction or full cold replay." + }, + "first_experiment": "Before any synthesis, write the candidate per-call local profile (and centre charge / unpaid coordinates if changed) and screen it with ceiling.ceiling(); reject it if even the ideal ceiling does not beat the selected word's by your stated margin. Ideal budget: rank-16 delivery is 2.31x (levers.py).", + "bottleneck_link": "Rank-1 children are about half of recursive cost; the selected word's effective child rank is about 3.9. Larger-rank delivery lowers recursive cost per unit of paid mass.", + "allowed_variations": [ + "One masked, overcomplete or block decoder family with exact labels and supports.", + "A scoped lower bound on effective rank for one alphabet.", + "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope." + ], + "scope_change_triggers": [ + "Repacking idle remainders of an unchanged word (covered by the packing ceiling).", + "Repeating the eight-term all-pairs search inside its proved scope." + ], + "overlap_terms": [ + "rank shape", + "block climb", + "masked decoder", + "overcomplete", + "effective rank" + ] + }, + "scope_status": "changed", + "actual_scope": "In the abstract Eisenstein E8 scalar binary decoder model of research/eisenstein-clique-copy-bound (PR798; optimum known in [22,40], clique certificates provably stop at 22), do rank bounds on non-clique principal submatrices of the fitting pattern lift the copy floor above 22?", + "scope_change_reason": "The card's diagonal-batch line is closed by PR679 and the diagonal-child-contract audit, and its live variants are claimed by other contributors. This decoder floor is the copy-cost side of the same card ('a scoped lower bound for one alphabet'): PR1794 shows an Eisenstein supplier beats the selected record only if C <= 31, and DreamingOfClouds' discussion-1167 note names it one of the sharper open decoder targets.", + "bottleneck_link": "Side result on an alternative complex unit: narrows PR1794's necessary window for an Eisenstein supplier from C in 22..31 to 23..31. No supplier, kappa or selected-record change.", + "budget_minutes": 60, + "stop_rule": "Stop after an exact certificate for the first integer above 22, plus a class-level exploration of whether principal-submatrix sets can go further; no decoder construction.", + "outcome": "completed", + "evidence": "verify.py (stdlib, exact): imports PR798's pinned geometry; exhaustive normalized search shows the 18-line core of S_uw = N[u] & N[w] has no fitting completion of rank <= 7 (rank-8 witness rebuilt), so minrank(S_uw) = 10 vs clique-dual price 9.5; five pinned automorphisms are transitive on the 540 nonorthogonal pairs; weights 184/6835, 13/13670, 7/20505 satisfy all 296,321 positive-cost flat-pair inequalities (601 tight); objective 30200/1367 > 22 so C >= 23; 5 rejection controls; RESULT.json pinned. Exploration (not replayed): class-uniform LP over 78 classes of hit-maximal sets also gives 30200/1367.", + "author": "Josie Elliston", + "ai_assistance": "Claude Code (Claude Opus 5.5) did the search, proof and verifier under the author's direction; one OpenAI Codex read-only review. Exploration used python-sat, networkx and scipy in a private venv; the replay is stdlib only.", + "open_questions": [ + { + "question": "Is 30200/1367 the exact limit of principal-submatrix certificates?", + "why_it_matters": "Tells the next prover whether more set families can help or a new ingredient is required.", + "first_step": "Check that the 78 hit-maximal classes are automorphism orbits (or give per-class rank witnesses) and exhibit the matching dual.", + "blocked_by": "Nothing; about one session." + }, + { + "question": "Can a cost-aware argument (like the Gaussian planar theorem) lift the bound past 23 on the 12-line Eisenstein hyperplanes?", + "why_it_matters": "The tight dual pairs are twelve-line hyperplane pairs; a bound >= 32 would close PR1794's window.", + "first_step": "Restrict to totals whose joint support has K-rank <= 3 and adapt the planar matching argument.", + "blocked_by": "Eisenstein planes hold up to four lines, so the matching step changes." + }, + { + "question": "Is there any fitting decoder cheaper than 40 (non-clean supports, C <= 31)?", + "why_it_matters": "Tests PR1794's remaining window from the upper side.", + "first_step": "SAT/ILP over flat-pair rectangles with parity constraints at cost <= 31.", + "blocked_by": "Parity constraints make LP relaxations weak; needs a good encoding." + } + ] +} diff --git a/research/eisenstein-submatrix-copy-floor/VERIFY.json b/research/eisenstein-submatrix-copy-floor/VERIFY.json new file mode 100644 index 0000000000..1a2df13abb --- /dev/null +++ b/research/eisenstein-submatrix-copy-floor/VERIFY.json @@ -0,0 +1,21 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/eisenstein-clique-copy-bound/PROOF.md", + "research/eisenstein-clique-copy-bound/geometry.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "exact C >= 23 certificate: minrank(S_uw)=10 by exhaustive normalized search plus rank-8 witness; automorphism transitivity on 540 pairs; 296,321 flat-pair inequalities; objective 30200/1367; 5 rejection controls; RESULT.json equality" + } + ] +} diff --git a/research/eisenstein-submatrix-copy-floor/verify.py b/research/eisenstein-submatrix-copy-floor/verify.py new file mode 100644 index 0000000000..0e3865fe72 --- /dev/null +++ b/research/eisenstein-submatrix-copy-floor/verify.py @@ -0,0 +1,357 @@ +#!/usr/bin/env python3 +"""Eisenstein E8 decoder copy floor C >= 23 by submatrix-minrank certificates. + +Standard library only. Reuses the frozen geometry of +research/eisenstein-clique-copy-bound (PR798) and checks: + +1. every 7-clique, and the 540 sets S_uw = N[u] & N[w] (u, w distinct + nonorthogonal lines; N[x] = x plus its 27 nonorthogonal neighbours); +2. minrank(S_uw) = 10: an exhaustive normalized search rules out every + fitting rank-<=7 completion of the base pair's 18-line core, an explicit + fitting rank-8 completion exists, and five pinned automorphisms of the + nonorthogonality graph (AUTOMORPHISMS.json) are transitive on all 540 + nonorthogonal pairs, so every S_uw has the same minrank; +3. the rational weights 184/6835 (singletons), 13/13670 (7-cliques) and + 7/20505 (S_uw) satisfy sum_S w_S [S meets F][S meets G] <= c(F,G) on all + 296,321 unordered flat pairs with c >= 1 (of 298,378 unordered pairs); +4. objective 30200/1367 > 22, so every fitting decomposition costs >= 23; +5. rejection controls. +""" +import hashlib +import json +import pathlib +import sys +from fractions import Fraction + +HERE = pathlib.Path(__file__).resolve().parent +ROOT = HERE.parents[1] +GEOM = ROOT / 'research' / 'eisenstein-clique-copy-bound' +sys.path.insert(0, str(GEOM)) +import geometry as g # noqa: E402 (frozen PR798 geometry, sha-pinned in SOURCES.json) + +W_SINGLE = Fraction(184, 6835) +W_CLIQUE7 = Fraction(13, 13670) +W_S20 = Fraction(7, 20505) +CORE_RANK_EXCLUDED = 7 + + +def require(cond, msg): + if not cond: + raise SystemExit('FAIL: ' + msg) + + +def pop(x): + return bin(x).count('1') + + +def check_sources(): + spec = json.loads((HERE / 'SOURCES.json').read_text()) + for item in spec['files']: + data = (ROOT / item['path']).read_bytes() + require(hashlib.sha256(data).hexdigest() == item['sha256'], 'source pin ' + item['path']) + + +class Pattern: + """Fitting pattern on 40 lines: diag 1, nonorthogonal off-diagonal 0, rest free.""" + + def __init__(self, adjacent): + self.adj = adjacent + + def entry(self, p, q): + if p == q: + return 1 + if self.adj[p] >> q & 1: + return 0 + return None + + +def max_clique(adj, mask): + best = [] + + def ext(chosen, poss): + nonlocal best + if not poss: + if len(chosen) > len(best): + best = chosen[:] + return + if len(chosen) + pop(poss) <= len(best): + return + v = (poss & -poss).bit_length() - 1 + ext(chosen + [v], poss & adj[v] & ~((1 << (v + 1)) - 1)) + ext(chosen, poss & ~(1 << v)) + + ext([], mask) + return best + + +def completion_exists(pat, lines, rank): + """Is there a fitting B on lines x lines with rank_F2(B) <= rank? + + Normalization (README, Lemma 2): with a clique Q in `lines`, B[Q,Q] = I, so + any factorization B = U V^T with `rank` columns can be changed to + U[Q] = V[Q] = [I_|Q| | 0]. Then for v outside Q, U[v] = (B[v,Q], s_v) and + V[v] = (B[Q,v]^T, t_v) with s_v, t_v in F2^(rank-|Q|), and every entry of + B between lines outside Q is x_v.y_w + s_v.t_w. Entries between Q and the + rest are the chosen x/y bits themselves, so the search enumerates exactly + the fixed-entry-respecting choices. Exhaustive backtracking. + Returns a witness dict or None. + """ + mask = sum(1 << v for v in lines) + Q = max_clique(pat.adj, mask) + q = len(Q) + if rank < q: + return None + extra = rank - q + rest = [v for v in lines if v not in Q] + + def choices(v, as_row): + fixed = [pat.entry(v, c) if as_row else pat.entry(c, v) for c in Q] + free = [i for i, f in enumerate(fixed) if f is None] + base = sum((f or 0) << i for i, f in enumerate(fixed)) + out = [] + for bits_ in range(1 << len(free)): + m = base + for k, i in enumerate(free): + if bits_ >> k & 1: + m |= 1 << i + out.append(m) + return out + + dom = {} + for v in rest: + opts = [] + for x in choices(v, True): + for y in choices(v, False): + for s in range(1 << extra): + for t in range(1 << extra): + if (pop(x & y) + pop(s & t)) % 2 == 1: # diagonal = 1 + opts.append((x, s, y, t)) + dom[v] = opts + order = sorted(rest, key=lambda v: len(dom[v])) + asg = {} + + def consistent(v, cand): + x, s, y, t = cand + for w, (xw, sw, yw, tw) in asg.items(): + e = pat.entry(v, w) + if e is not None and (pop(x & yw) + pop(s & tw)) % 2 != e: + return False + e = pat.entry(w, v) + if e is not None and (pop(xw & y) + pop(sw & t)) % 2 != e: + return False + return True + + def rec(i): + if i == len(order): + return True + v = order[i] + for cand in dom[v]: + if consistent(v, cand): + asg[v] = cand + if rec(i + 1): + return True + del asg[v] + return False + + if not rec(0): + return None + return {'Q': Q, 'extra': extra, 'rows': dict(asg)} + + +def matrix_from_witness(pat, lines, wit): + """Rebuild B from a normalized witness and check it fits and has the stated rank bound.""" + Q, extra = wit['Q'], wit['extra'] + U, V = {}, {} + for i, c in enumerate(Q): + U[c] = (1 << i, 0) + V[c] = (1 << i, 0) + for v, (x, s, y, t) in wit['rows'].items(): + U[v] = (x, s) + V[v] = (y, t) + B = {} + for p in lines: + for r in lines: + val = (pop(U[p][0] & V[r][0]) + pop(U[p][1] & V[r][1])) % 2 + e = pat.entry(p, r) + require(e is None or e == val, 'witness does not fit') + B[(p, r)] = val + rows = [sum(B[(p, r)] << j for j, r in enumerate(lines)) for p in lines] + return f2_rank(rows) + + +def f2_rank(rows): + rows = list(rows) + rank = 0 + for bit in range(64): + piv = next((i for i in range(rank, len(rows)) if rows[i] >> bit & 1), None) + if piv is None: + continue + rows[rank], rows[piv] = rows[piv], rows[rank] + for i in range(len(rows)): + if i != rank and rows[i] >> bit & 1: + rows[i] ^= rows[rank] + rank += 1 + return rank + + +def s20_minrank_bound(pat, u, w, nclosed): + """minrank(S_uw) >= 10: u, w are isolated (block I_2) and the 18-line core has no rank<=7 completion.""" + S = nclosed[u] & nclosed[w] + lines = [v for v in range(40) if S >> v & 1] + require(len(lines) == 20, 'S_uw size') + iso = [v for v in lines if all(pat.entry(v, x) is not None for x in lines)] + require(sorted(iso) == sorted([u, w]), 'S_uw isolated pair') + core = [v for v in lines if v not in (u, w)] + require(completion_exists(pat, core, CORE_RANK_EXCLUDED) is None, + 'core admits a rank-7 completion') + return S, core + + +def replay(controls=True): + check_sources() + reps, images, adjacent, _pairs, _orbits = g.geometry() + pat = Pattern(adjacent) + nclosed = [adjacent[u] | (1 << u) for u in range(40)] + flats = g.flats(reps, images) + require(len(flats) == 772, 'flat count') + masks = [m for m, _, _ in flats] + bases = [b for _, b, _ in flats] + + cliques = g.all_cliques(adjacent) + require(len(cliques) == 40054, 'clique count') + c7 = [c for c in cliques if pop(c) == 7] + require(len(c7) == 2880, '7-clique count') + for c in c7: + for v in range(40): + if c >> v & 1: + require(c & ~nclosed[v] == 0, '7-clique is a clique') + + pairs = [(u, w) for u in range(40) for w in range(u + 1, 40) if adjacent[u] >> w & 1] + require(len(pairs) == 540, 'nonorthogonal pair count') + aut = json.loads((HERE / 'AUTOMORPHISMS.json').read_text()) + base = tuple(aut['base_pair']) + gens = aut['generators'] + for gperm in gens: + require(is_automorphism(adjacent, gperm), 'generator is an automorphism') + require(pair_orbit(gens, base) == set(pairs), 'generators are transitive on nonorthogonal pairs') + # Exhaustive core search for the base pair only; automorphisms preserve the + # fitting pattern, map N[x] to N[g x] and hence S_uw to S_(gu)(gw), so all + # 540 sets have the same minrank (README, Lemma 3). + _S, core = s20_minrank_bound(pat, base[0], base[1], nclosed) + wit = completion_exists(pat, core, 8) + require(wit is not None, 'rank-8 core completion exists') + witness_rank = matrix_from_witness(pat, core, wit) + require(witness_rank == 8, 'rank-8 witness has F2 rank 8') + s20 = [nclosed[u] & nclosed[w] for u, w in pairs] + require(len(set(s20)) == 540 and all(pop(x) == 20 for x in s20), 'distinct 20-line S_uw') + + costs = {} + for i in range(len(masks)): + for j in range(i, len(masks)): + c = g.pairing_rank(bases[i], bases[j]) if bases[i] and bases[j] else 0 + if c: + costs[(i, j)] = c + + # hit bitsets per flat + def meet_bits(sets): + return [sum(1 << k for k, s in enumerate(sets) if s & f) for f in masks] + + m7 = meet_bits(c7) + m20 = meet_bits(s20) + checked = tight = 0 + min_slack = None + for (i, j), c in costs.items(): + lhs = (W_SINGLE * pop(masks[i] & masks[j]) + W_CLIQUE7 * pop(m7[i] & m7[j]) + + W_S20 * pop(m20[i] & m20[j])) + slack = c - lhs + require(slack >= 0, 'primal inequality at flats %d,%d' % (i, j)) + checked += 1 + tight += slack == 0 + min_slack = slack if min_slack is None else min(min_slack, slack) + objective = W_SINGLE * 40 + W_CLIQUE7 * 7 * len(c7) + W_S20 * 10 * len(s20) + require(objective == Fraction(30200, 1367), 'objective value') + require(objective > 22, 'objective exceeds 22') + floor = -(-objective.numerator // objective.denominator) + require(floor == 23, 'integer floor') + + ncontrols = 0 + if controls: + ncontrols = run_controls(pat, adjacent, nclosed, base, gens, c7, masks, costs, m7, m20) + return { + 'flat_pairs_with_positive_cost': checked, + 'tight': tight, + 'cliques7': len(c7), + 's20_sets': len(s20), + 'core_rank8_witness_rank': witness_rank, + 'objective': str(objective), + 'copy_floor': floor, + 'controls': ncontrols, + } + + +def run_controls(pat, adjacent, nclosed, base, gens, c7, masks, costs, m7, m20): + n = 0 + # 1. The completion search is not vacuous: a 7-clique has no rank-6 completion + # and has a rank-7 one. + clique = [v for v in range(40) if c7[0] >> v & 1] + require(completion_exists(pat, clique, 6) is None, 'control: clique rank 6') + require(completion_exists(pat, clique, 7) is not None, 'control: clique rank 7') + n += 1 + # 2. A transposition of the two base lines composed with a generator is still checked: + # swapping two lines of different neighbourhoods is rejected as an automorphism. + u, w = base + x = next(v for v in range(40) if nclosed[v] != nclosed[u] and v != u) + swap = list(range(40)) + swap[u], swap[x] = x, u + require(not is_automorphism(adjacent, swap), 'control: non-automorphism rejected') + n += 1 + # 3. Too few generators fail transitivity (the orbit check is not vacuous). + require(pair_orbit(gens[:1], base) != pair_orbit(gens, base), 'control: one generator not transitive') + n += 1 + # 4. Raising the S_uw weight by 1/20505 violates a primal inequality. + bad = W_S20 + Fraction(1, 20505) + require(any(W_SINGLE * pop(masks[i] & masks[j]) + W_CLIQUE7 * pop(m7[i] & m7[j]) + + bad * pop(m20[i] & m20[j]) > c for (i, j), c in costs.items()), + 'control: inflated S_uw weight is rejected') + n += 1 + # 5. Without the S_uw sets the same singleton/clique weights total less than 22. + require(W_SINGLE * 40 + W_CLIQUE7 * 7 * len(c7) < 22, 'control: cliques alone below 22') + n += 1 + return n + + +def is_automorphism(adj, perm): + if sorted(perm) != list(range(40)): + return False + return all((adj[perm[a]] >> perm[b] & 1) == (adj[a] >> b & 1) + for a in range(40) for b in range(40)) + + +def pair_orbit(gens, base): + seen = {tuple(sorted(base))} + stack = list(seen) + while stack: + a, b = stack.pop() + for gp in gens: + img = tuple(sorted((gp[a], gp[b]))) + if img not in seen: + seen.add(img) + stack.append(img) + return seen + + +def main(): + result = replay(controls='--no-controls' not in sys.argv) + expected = json.loads((HERE / 'RESULT.json').read_text()) if (HERE / 'RESULT.json').exists() else None + if '--write' in sys.argv: + (HERE / 'RESULT.json').write_text(json.dumps(result, indent=2, sort_keys=True) + '\n') + elif expected is not None: + require(expected == result, 'RESULT.json mismatch') + print('PASS_EISENSTEIN_SUBMATRIX_COPY_FLOOR: C >= %d; objective %s; %d flat pairs; ' + '%d S_uw sets minrank 10; %d controls; no new kappa' + % (result['copy_floor'], result['objective'], result['flat_pairs_with_positive_cost'], + result['s20_sets'], result['controls'])) + + +if __name__ == '__main__': + main()