From e44bdadecb2df21bd50bbda30c8f0b9b93f71fbd Mon Sep 17 00:00:00 2001 From: josie Date: Wed, 14 Oct 2026 01:30:03 -0400 Subject: [PATCH 1/5] WIP: full-family (G) without (D) counterexample package Co-Authored-By: Claude Opus 5.5 --- research/full-family-g-without-d/README.md | 35 +++ research/full-family-g-without-d/SOURCES.json | 18 ++ research/full-family-g-without-d/TASK.json | 72 ++++++ research/full-family-g-without-d/VERIFY.json | 19 ++ research/full-family-g-without-d/verify.py | 243 ++++++++++++++++++ 5 files changed, 387 insertions(+) create mode 100644 research/full-family-g-without-d/README.md create mode 100644 research/full-family-g-without-d/SOURCES.json create mode 100644 research/full-family-g-without-d/TASK.json create mode 100644 research/full-family-g-without-d/VERIFY.json create mode 100644 research/full-family-g-without-d/verify.py diff --git a/research/full-family-g-without-d/README.md b/research/full-family-g-without-d/README.md new file mode 100644 index 0000000000..b45445043f --- /dev/null +++ b/research/full-family-g-without-d/README.md @@ -0,0 +1,35 @@ +# full-family-g-without-d + +**Draft; no new bound claimed.** + +## Scope and evidence + +Original card: `complex-rank-shape-decoder`. Complete [TASK.json](TASK.json), including any scope +change and its connection to the bottleneck. Explain the result and limitations here. +Source commits, Git blobs and SHA256 pins are in [SOURCES.json](SOURCES.json). +The selected record and catalogue are historical provenance, so later priority +updates do not invalidate this package. Explicit --source files are live inputs +and must match their pins. Full Git history is needed to resolve provenance. + +## Reproduce + +After completing the verifier and marking VERIFY.json ready, from repo root: + +```sh +python3 scripts/research_package.py --package research/full-family-g-without-d --check-only +python3.12 scripts/research_package.py --package research/full-family-g-without-d +``` + +Declare all external inputs and pinned dependencies in VERIFY.json. The generic +hook is bounded; native/Lean or long replays need an explicit dedicated workflow. + +## Open next questions + +Complete the structured `open_questions` list in TASK.json and explain it here: +the question, why it matters, a feasible first step and any blocker. If no next +question is justified, say so rather than inventing one. + +## Credit + +Prepared by JosieElliston. Retain predecessor attribution and source-specific notices. +New work is Apache-2.0. Disclose substantial AI assistance in TASK.json. diff --git a/research/full-family-g-without-d/SOURCES.json b/research/full-family-g-without-d/SOURCES.json new file mode 100644 index 0000000000..546fbedf18 --- /dev/null +++ b/research/full-family-g-without-d/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "1f7a934975e5eacaf83511c9ac870263bf095e05", + "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" + } + ] +} diff --git a/research/full-family-g-without-d/TASK.json b/research/full-family-g-without-d/TASK.json new file mode 100644 index 0000000000..adf232aa13 --- /dev/null +++ b/research/full-family-g-without-d/TASK.json @@ -0,0 +1,72 @@ +{ + "schema_version": 1, + "task_id": "complex-rank-shape-decoder", + "priority_revision": 3, + "base_commit": "1f7a934975e5eacaf83511c9ac870263bf095e05", + "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": "PR1650 open question 1, in the masked (E-graph) model of PR1212 with PR1560's frame-incidence criterion: when the frame family is ALL live frames of P112 \\ X, does a pivot frame passing (W), nonempty blocks and (G) always pass (D)? Exact counterexamples at |X| = 8 (a P104 live set), plus scoped search evidence that none exists at |X| <= 7 in the searched domain.", + "scope_change_reason": "Revision 3 retired complex-masked-decoder into this card. The chooser drew recursive-interfaces (nonce 083eb6ba0dd52fa857761981ccb9156c), whose three cards were crowded on 2026-10-14 (plane-port lever claimed in Discussion 1587); this session instead answers a recorded open question of PR1650 on the masked-decoder rigidity line. It is a side result about a verification criterion: no decoder, profile or child-rank change.", + "bottleneck_link": "Side result, not a lever. It tells future rigidity replays (P105 and below) that the rank test (D) cannot be replaced by the counting conditions (W), nonempty blocks and (G) in general, even for full live families. No kappa change.", + "budget_minutes": 60, + "stop_rule": "Stop at an exact, locally minimal counterexample plus a bounded search at |X| <= 7; a structural lemma for |X| <= 7 is left open.", + "outcome": "completed", + "evidence": "verify.py (stdlib, ~3 s): two fixtures (X, F) with |X| = 8; all 784 live frames; nonempty blocks, (W), (G) hold; exact Fraction rank of the I_k incidence matrix is |I_k| - 8 = 44 < 45 at one pivot k (other k pass); fixture 1 carries a +-1 integer kernel vector on eight lines outside span(h_kl); restoring any one deleted line makes the pivot pass all four conditions; mutated-certificate and pivot-alone (G) controls. Unregistered search evidence in README (scratch scripts, numpy-free but importing PR1650's verify.py): deletion walks, random 8-10 line deletions, and a full every-frame census of the 1614 P107 units.", + "author": "JosieElliston (with Claude Opus 5.5 via Claude Code)", + "ai_assistance": "Claude Opus 5.5 via Claude Code: search, verifier and write-up. Submitted by the account holder.", + "open_questions": [ + { + "question": "For |X| <= 7 (P105 to P111), does every pivot passing (W), nonempty blocks and (G) on the full live family pass (D)?", + "why_it_matters": "PR1650's open question 1 is now false at |X| = 8; if it holds for |X| <= 7, the P105 replay could drop its rank computations, which are almost all of its 1200 s budget.", + "first_step": "Every-frame census of the 19295 P106 units (about 3.6 CPU-hours with PR1650's criterion), or a lemma explaining why the eight-line rank drop (two quadruples of lines met equally by every live frame) needs eight deletions.", + "blocked_by": "Compute for P106/P105 every-frame censuses; no candidate lemma." + }, + { + "question": "Which structure of X forces the rank drop?", + "why_it_matters": "Fixture 1's kernel vector is -1 on lines {2,5,7,10} and +1 on {30,31,40,41}: every live frame meets the two quadruples in equally many lines. A description of all such balanced pairs would give a cheap, exact test that could replace (D).", + "first_step": "Classify the minimized counterexamples found by the deletion walks under the FRAME0 stabiliser and read off the balanced quadruple pairs.", + "blocked_by": "None; not started." + } + ] +} diff --git a/research/full-family-g-without-d/VERIFY.json b/research/full-family-g-without-d/VERIFY.json new file mode 100644 index 0000000000..37014bc888 --- /dev/null +++ b/research/full-family-g-without-d/VERIFY.json @@ -0,0 +1,19 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Two exact fixtures: premises (W), nonempty blocks, (G) on the full live family; exact (D) failure (Fraction rank and an integer kernel certificate); eight restore controls each; mutated-certificate and pivot-alone (G) controls." + } + ] +} diff --git a/research/full-family-g-without-d/verify.py b/research/full-family-g-without-d/verify.py new file mode 100644 index 0000000000..c459bd4769 --- /dev/null +++ b/research/full-family-g-without-d/verify.py @@ -0,0 +1,243 @@ +#!/usr/bin/env python3 +"""(G) does not imply (D) even for the family of ALL live frames: an exact counterexample on an 8-line deletion of +P112 (a P104 live set), for PR1560's frame-incidence criterion as implemented in PR1650. + +Standard library only, exact integer/rational arithmetic. Self-contained: the E8 line model, frame enumeration +and the four conditions (D), (G), (W), nonempty blocks follow PR1650's `verify.py` (session 9, head d960f8a2), +re-typed here so this file does not depend on an unmerged package. Run from the repository root: + + python3 -I -B research/full-family-g-without-d/verify.py + +Checks, for each fixture (deleted set X, pivot frame F), with the family of all 784 live frames of P112 \\ X: + 1. F is a live frame; nonempty blocks, (W) and (G) hold; + 2. (D) fails: on I_k for one pivot k, the incidence matrix has exact rational rank |I_k| - 8 < |I_k| - 7 + (Fraction elimination), while the seven vectors h_kl are independent and lie in its kernel; + 3. fixture 1 also carries a sparse integer kernel vector x (entries +-1 on eight lines) with every live + frame's row orthogonal to x and rank [h; x] = 8, which certifies the rank drop without elimination; + 4. control: restoring any one of the eight deleted lines makes the same pivot pass all four conditions + (mod-p rank lower bound plus the h_kl kernel upper bound, as in PR1650); + 5. controls: a mutated certificate is rejected; the pivot-alone sub-family fails (G). +""" + +import itertools +import sys +from fractions import Fraction + +PRIME = 1000003 + + +def check(tag, cond, info=''): + print(f"{'PASS' if cond else 'FAIL'} {tag}" + (f': {info}' if info else ''), flush=True) + if not cond: + print(f'FAIL_FULL_FAMILY_G_WITHOUT_D: {tag}') + sys.exit(1) + + +# ---------------------------------------------------------------- E8 model (doubled coordinates, norm 8) + +def lines_e8(): + out = set() + for i, j in itertools.combinations(range(8), 2): + for sj in (2, -2): + v = [0] * 8 + v[i], v[j] = 2, sj + out.add(tuple(v)) + for s in itertools.product((1, -1), repeat=7): + v = (1,) + s + if v.count(-1) % 2 == 0: + out.add(v) + return sorted(out) + + +# Line IDs are positions in this sorted list; they agree with PR1560's and PR1650's IDs. +LINES = lines_e8() +NL = len(LINES) +IDX = {v: n for n, v in enumerate(LINES)} + + +def ip(x, y): + d = sum(a * b for a, b in zip(x, y)) + assert d % 4 == 0 + return d // 4 + + +G = [[ip(LINES[i], LINES[j]) for j in range(NL)] for i in range(NL)] +FRAME0 = (0, 1, 6, 11, 20, 29, 106, 119) +P112 = [i for i in range(NL) if i not in FRAME0] + + +def is_frame(S): + return len(S) == 8 and all(G[a][b] == 0 for a in S for b in S if a != b) + + +def frames_inside(live): + live = sorted(live) + out = [] + + def grow(cur, cand): + if len(cur) == 8: + out.append(tuple(cur)) + return + for n, j in enumerate(cand): + grow(cur + [j], [k for k in cand[n + 1:] if G[j][k] == 0]) + + grow([], live) + return out + + +FRAMES = frames_inside(range(NL)) + +# ---------------------------------------------------------------- fixtures (found by deletion walks, see README) + +FIXTURES = [ + dict(X=(3, 4, 8, 9, 107, 108, 117, 118), F=(19, 25, 37, 47, 67, 82, 94, 115), k=2, + cert={2: -1, 5: -1, 7: -1, 10: -1, 30: 1, 31: 1, 40: 1, 41: 1}), + dict(X=(13, 18, 22, 27, 34, 35, 36, 37), F=(17, 25, 38, 52, 61, 75, 98, 116), k=7, cert=None), +] + + +# ---------------------------------------------------------------- ranks + +def rank_fraction(rows): + """Exact rank over Q by Fraction Gaussian elimination.""" + basis = [] # (pivot column, row) + for r in rows: + v = [Fraction(x) for x in r] + for c, b in basis: + if v[c]: + a = v[c] + v = [x - a * y for x, y in zip(v, b)] + c = next((j for j, x in enumerate(v) if x), None) + if c is not None: + v = [x / v[c] for x in v] + basis.append((c, v)) + return len(basis) + + +def rank_mod(rows): + """Rank modulo PRIME (a lower bound on the rank over Q).""" + basis = {} + for row in rows: + v = [x % PRIME for x in row] + for j in sorted(basis): + if v[j]: + a, w = v[j], basis[j] + v = [(x - a * y) % PRIME for x, y in zip(v, w)] + j = next((j for j, x in enumerate(v) if x), None) + if j is not None: + inv = pow(v[j], -1, PRIME) + basis[j] = [x * inv % PRIME for x in v] + return len(basis) + + +# ---------------------------------------------------------------- PR1560's four conditions at one pivot + +def setup(X, F, frames=None): + dead = set(FRAME0) | set(X) + live_frames = [Fr for Fr in FRAMES if not dead & set(Fr)] if frames is None else frames + non = [i for i in P112 if i not in dead and i not in F] + odd = {i: tuple(n for n in range(8) if G[i][F[n]]) for i in non} + return live_frames, non, odd + + +def blocks_w(F, non, odd): + """(nonempty-blocks ok, W ok). Block of i = its odd pivot 4-set; class = parity of negative signs on it.""" + blocks = {} + for i in non: + t = odd[i] + assert len(t) == 4 + blocks.setdefault(t, [0, 0])[sum(G[i][F[n]] < 0 for n in t) % 2] += 1 + cov = set() + for t, (c0, c1) in blocks.items(): + if (c0 == 4 and c1) or (c1 == 4 and c0): + cov.update(itertools.combinations(t, 2)) + return len(blocks) == 14, len(cov) == 28 + + +def condition_g(non, odd, live_frames): + """For each pivot pair kl: the graph on I_kl (i, j joined when a live frame meets I_kl in exactly {i, j}) + is connected.""" + traces = {frozenset(Fr) & frozenset(non) for Fr in live_frames} + for p in itertools.combinations(range(8), 2): + I = {i for i in non if p[0] in odd[i] and p[1] in odd[i]} + par = {i: i for i in I} + + def find(a): + while par[a] != a: + a = par[a] + return a + + for s in traces: + e = s & I + if len(e) == 2: + a, b = sorted(e) + par[find(a)] = find(b) + if len({find(i) for i in I}) != 1: + return False + return True + + +def incidence(F, k, non, live_frames): + I = [i for i in non if G[i][F[k]]] + rows = sorted({tuple(1 if i in Fr else 0 for i in I) for Fr in live_frames}) + h = [[G[i][F[k]] * G[i][F[l]] for i in I] for l in range(8) if l != k] + return I, rows, h + + +def kernel_ok(rows, vecs): + return all(sum(a * b for a, b in zip(r, v)) == 0 for r in rows for v in vecs) + + +def condition_d_modp(F, non, live_frames): + """PR1650's (D) test: h_kl independent and in the kernel, incidence rank mod p reaches |I_k| - 7.""" + for k in range(8): + I, rows, h = incidence(F, k, non, live_frames) + if rank_mod(h) != 7 or not kernel_ok(rows, h) or rank_mod(rows) != len(I) - 7: + return False + return True + + +def main(): + check('model', NL == 120 and len(FRAMES) == 2025 and is_frame(FRAME0), f'{NL} lines, {len(FRAMES)} frames') + for n, fx in enumerate(FIXTURES, 1): + X, F, k = fx['X'], fx['F'], fx['k'] + tag = f'fixture{n}' + check(f'{tag}.pivot', is_frame(F) and not set(F) & (set(X) | set(FRAME0)) and len(set(X)) == 8 + and set(X) <= set(P112), f'X={X} F={F}') + live_frames, non, odd = setup(X, F) + nb, w = blocks_w(F, non, odd) + check(f'{tag}.premises', nb and w and condition_g(non, odd, live_frames), + f'{len(live_frames)} live frames (all of them); nonempty blocks, (W), (G) hold') + bad = [] + for kk in range(8): + I, rows, h = incidence(F, kk, non, live_frames) + check(f'{tag}.h{kk}', rank_fraction(h) == 7 and kernel_ok(rows, h)) + r = rank_fraction(rows) + if r != len(I) - 7: + bad.append((kk, len(I), r)) + check(f'{tag}.D-fails', [b[0] for b in bad] == [k] and bad[0][2] == bad[0][1] - 8, + f'exact rank over Q on I_{k}: {bad[0][2]} = |I_k| - 8 with |I_k| = {bad[0][1]}; other k pass') + if fx['cert']: + I, rows, h = incidence(F, k, non, live_frames) + x = [fx['cert'].get(i, 0) for i in I] + check(f'{tag}.certificate', set(fx['cert']) <= set(I) and kernel_ok(rows, [x]) and rank_fraction(h + [x]) == 8, + f'integer kernel vector {fx["cert"]} is orthogonal to every live frame and outside span(h)') + y = list(x) + y[I.index(next(iter(fx['cert'])))] *= -1 + check(f'{tag}.control.mutated-certificate', not kernel_ok(rows, [y])) + for x in X: + Y = tuple(i for i in X if i != x) + lf, nn, oo = setup(Y, F) + nb, w = blocks_w(F, nn, oo) + ok = nb and w and condition_g(nn, oo, lf) and condition_d_modp(F, nn, lf) + check(f'{tag}.control.restore-{x}', ok, f'{len(lf)} live frames; all four conditions pass') + lf, nn, oo = setup(X, F, frames=[F]) + check(f'{tag}.control.pivot-alone-fails-G', not condition_g(nn, oo, lf)) + print('PASS_FULL_FAMILY_G_WITHOUT_D fixtures=2: (W), nonempty blocks and (G) on the full live family do not ' + 'imply (D) (exact), and each counterexample needs all eight deletions') + + +if __name__ == '__main__': + if sys.flags.optimize: + sys.exit('refusing to run with -O') + main() From 556be1268d45c10b8517fc09da6ad1c5e7dfcedd Mon Sep 17 00:00:00 2001 From: josie Date: Wed, 14 Oct 2026 01:37:38 -0400 Subject: [PATCH 2/5] full-family-g-without-d: D4 certificates for both fixtures, search scripts, README Co-Authored-By: Claude Opus 5.5 --- research/full-family-g-without-d/README.md | 108 +++++++++++++++--- .../search/allframes.py | 45 ++++++++ .../full-family-g-without-d/search/mech.py | 61 ++++++++++ .../search/minimize.py | 47 ++++++++ .../full-family-g-without-d/search/walk.py | 49 ++++++++ research/full-family-g-without-d/verify.py | 49 +++++--- 6 files changed, 328 insertions(+), 31 deletions(-) create mode 100644 research/full-family-g-without-d/search/allframes.py create mode 100644 research/full-family-g-without-d/search/mech.py create mode 100644 research/full-family-g-without-d/search/minimize.py create mode 100644 research/full-family-g-without-d/search/walk.py diff --git a/research/full-family-g-without-d/README.md b/research/full-family-g-without-d/README.md index b45445043f..ed7c2cc4b9 100644 --- a/research/full-family-g-without-d/README.md +++ b/research/full-family-g-without-d/README.md @@ -1,35 +1,107 @@ -# full-family-g-without-d +# (G) does not imply (D) even for the full live family (no new κ) -**Draft; no new bound claimed.** +**Status: exact finite counterexample to a proposed shortcut, plus scoped search evidence. No κ claim, no +construction, and no change to any proved rigidity result.** -## Scope and evidence +[PR1650](https://github.com/CrocSwap/integer-mult-bounds/pull/1650) (head `d960f8a2`) checks +[PR1560](https://github.com/CrocSwap/integer-mult-bounds/pull/1560)'s frame-incidence criterion on every P105 +unit. Its open question 1 asks whether a pivot frame that passes the counting conditions (W), nonempty blocks +and (G) always passes the rank condition (D), when the family is **all** live frames. If so, the P105 replay could +drop every rank computation. Two earlier counterexamples (PR1650's `control.g-without-d` and navinor's +[PR1649](https://github.com/CrocSwap/integer-mult-bounds/pull/1649)) use *sub-families* of the live frames, so they +leave the full-family question open. -Original card: `complex-rank-shape-decoder`. Complete [TASK.json](TASK.json), including any scope -change and its connection to the bottleneck. Explain the result and limitations here. -Source commits, Git blobs and SHA256 pins are in [SOURCES.json](SOURCES.json). -The selected record and catalogue are historical provenance, so later priority -updates do not invalidate this package. Explicit --source files are live inputs -and must match their pins. Full Git history is needed to resolve provenance. +## Result -## Reproduce +**The implication fails for full live families once eight lines are deleted from P112.** `verify.py` checks two +exact fixtures. Fixture 1: + +- Deleted set X = (3, 4, 8, 9, 107, 108, 117, 118), live set P112 \ X (104 lines, a P104 live set). Pivot frame + F = (19, 25, 37, 47, 67, 82, 94, 115). All 784 live frames are used. +- Nonempty blocks, (W) and (G) hold. +- (D) fails at pivot k = 2. The incidence matrix of the live frames on I_2 (52 lines) has exact rank 44 over Q, + one short of 52 − 7 = 45. The seven vectors h_2l are independent and lie in its kernel, as #1560 requires. +- An integer certificate needs no elimination: x = +1 on lines {30, 31, 40, 41}, −1 on {2, 5, 7, 10}. Every live + frame is orthogonal to x, and x is outside the span of the h_2l. +- **Why it happens.** Every one of the 2025 E8 frames meets the two coordinate-half D4 subsystems equally: + Da (the 12 lines supported on coordinates 0–3) and Db (coordinates 4–7). The intersection counts are (0,0), + (1,1), (2,2) or (4,4). FRAME0 deletes 4 lines from each. X deletes 4 more from each, which leaves exactly the 4 + lines of each that are odd to F[2]. So x = 1(Da live) − 1(Db live) is orthogonal to every live frame. It is + supported on I_2, and it is not a combination of the h_2l. +- **Locally minimal.** Restoring any one of the eight deleted lines makes the same pivot pass all four conditions. + Each restored live set has 816 live frames. +- This unit is still rigid through other pivots: 674 of its live frames pass all four conditions. Of the rest, + 96 pass (W), blocks and (G) but fail (D), 4 fail (G) and 10 fail (W). + +Fixture 2, X = (13, 18, 22, 27, 34, 35, 36, 37) with pivot (17, 25, 38, 52, 61, 75, 98, 116), has the same +pattern at k = 7: rank 44 on 52 lines. Its certificate is +1 on {111, 112, 113, 114} and −1 on {12, 19, 21, 28}. +These come from a non-coordinate pair of orthogonal D4 subsystems, each containing 4 FRAME0 lines; the pair is an +image of the coordinate halves under the FRAME0 stabiliser (`search/mech.py`). + +So the conditions in PR1650's question cannot replace (D) in general. Whether they can on P105 to P111 +(|X| ≤ 7) is still open; the evidence below found no counterexample there. + +## Search evidence (unregistered) + +The scripts in `search/` import PR1650's `verify.py` (head `d960f8a2`), whose criterion is the one verified +above. Set `PR1650_PACKAGE` to that package's directory. Wall times are on a shared 10-core macOS host +(load 15–30). -After completing the verifier and marking VERIFY.json ready, from repo root: +| Search | Domain | Outcome | +|---|---|---| +| `walk.py --n 5000` (seeds 0–4999) | fix a random pivot F; delete random non-pivot lines one at a time, skipping any that break (W) or blocks at F; full criterion after each step | 176 walks reach a (G)-pass/(D)-fail step, first at 23–41 deletions. The first failure is usually (G). | +| `minimize.py` on those 176 | restore deleted lines greedily while the verdict stays (D)-fail | locally minimal sizes 8 (20 sets), 10 (48), 11–28 (the rest); **none below 8** | +| `mech.py` | all 7 D4⊕D4 splits that contain FRAME0 as 4+4 (closure of the coordinate splits under the stabiliser generators), all 1260 pivots disjoint from FRAME0, all k; X = the live split lines even to F[k] | sizes 4, 6, 8, 10. **(D) fails only at |X| = 8** (32256 cases). Every |X| = 4, 6 or 10 case passes or fails blocks. | +| `allframes.py random --size s --sample 100` | random X of size 8, 9 and 10 (seeds 8, 9, 10), every live frame | 189952 frames: none fails (G) or (D); only (W) fails | +| `allframes.py p107` | every live frame of all 1614 P107 units | P107_RESULT | + +The first two rows also give the fixtures: walk seeds 1023 and 1759 minimize to fixtures 1 and 2 (pivot indices +1765 and 1670 in PR1650's frame order). + +## Reproduce ```sh +python3 -I -B research/full-family-g-without-d/verify.py # about 3 s, standard library python3 scripts/research_package.py --package research/full-family-g-without-d --check-only python3.12 scripts/research_package.py --package research/full-family-g-without-d ``` -Declare all external inputs and pinned dependencies in VERIFY.json. The generic -hook is bounded; native/Lean or long replays need an explicit dedicated workflow. +Expected last line: `PASS_FULL_FAMILY_G_WITHOUT_D fixtures=2: ...`. `-O` is refused. + +## Scope and limits + +- The counterexamples are at |X| = 8, below P105. Nothing proved in PR1616 or PR1650 is affected, since those + verify (D) explicitly. The P104 units are not claimed non-rigid; fixture 1's unit has 674 passing pivots. +- "(W) and blocks imply (G)" also fails for full families: the same unit has 4 frames that pass (W) and blocks but + fail (G). +- No search covered every pivot of every P106 or P105 unit; see the open questions. +- #1560's Theorem 1 and Corollary 2 are cited, not re-derived. Ranks in the restore controls are mod-p lower bounds + matched by the h_kl kernel upper bound, as in PR1650. The (D) failures are exact over Q. ## Open next questions -Complete the structured `open_questions` list in TASK.json and explain it here: -the question, why it matters, a feasible first step and any blocker. If no next -question is justified, say so rather than inventing one. +1. **Does the shortcut hold for |X| ≤ 7 (P105 to P111)?** + - *Why it matters.* If it does, the P105 replay could drop the rank computations that take nearly all of its + 1200 s budget. + - *First step.* Run an every-frame census on the 19295 P106 units (about 3.6 CPU-hours with PR1650's criterion), + then on a P105 sample. Or prove that a balanced pair of line sets inside I_k needs eight deletions. + - *Blocker.* Compute, and no candidate lemma. The D4 mechanism needs exactly eight, and no mechanism with fewer + appeared in the searches above. +2. **Classify the balanced line pairs.** + - *Why it matters.* Fixture 1's kernel vector comes from the frame identity |Φ ∩ Da| = |Φ ∩ Db|. If every rank + drop has this form, an exact counting test could replace (D) after all. + - *First step.* Express the kernel vectors of the size-10 and size-11 minimized sets from `minimize.py` in + sparse form, and check whether each is a difference of D4 indicators. + - *Blocker.* None. Not started. ## Credit -Prepared by JosieElliston. Retain predecessor attribution and source-specific notices. -New work is Apache-2.0. Disclose substantial AI assistance in TASK.json. +- **an664 / Andrey Mas (PR1560):** the criterion and its conditions. +- **PR1650 / PR1616 (JosieElliston):** the implementation whose open question this answers. `verify.py` re-types + its E8 model and condition tests. +- **navinor / Aaron Wang (PR1649):** the P107 sub-family counterexample and the full-family boundary question. +- **burntout76 / Brett Halligan (PR1212), themilkman216 (PR968), DreamingOfClouds (PR717):** the E-graph model + and the floor this line verifies. + +Prepared by JosieElliston with substantial assistance from Claude Opus 5.5 (Anthropic) via Claude Code, covering +the search, verifier and write-up. Apache-2.0. diff --git a/research/full-family-g-without-d/search/allframes.py b/research/full-family-g-without-d/search/allframes.py new file mode 100644 index 0000000000..cf0dac4a15 --- /dev/null +++ b/research/full-family-g-without-d/search/allframes.py @@ -0,0 +1,45 @@ +"""Full-live-family (G)/(D) census: for each unit X (deleted lines besides FRAME0), run PR1650's criterion at +EVERY live frame and tally reasons. A counterexample is a frame failing D or D-kernel-vectors (G already passed).""" +import argparse, collections, gzip, json, os, random, sys, time +from concurrent.futures import ProcessPoolExecutor +sys.path.insert(0, os.environ['PR1650_PACKAGE']) # research/complex-rank8-rigidity-p105 at PR1650 head d960f8a2 +import verify as V + +def unit(X): + xm = V.F0MASK | sum(1 << i for i in X) + tally = collections.Counter(); bad = [] + for n, m in enumerate(V.FMASK): + if m & xm: + continue + r = V.criterion(tuple(X), V.FRAMES[n])[0] + tally[r] += 1 + if r in ('D', 'D-kernel-vectors', 'support'): + bad.append((list(X), n, r)) + return tally, bad + +def main(): + ap = argparse.ArgumentParser() + ap.add_argument('level'); ap.add_argument('--jobs', type=int, default=10) + ap.add_argument('--sample', type=int, default=0); ap.add_argument('--size', type=int, default=8) + ap.add_argument('--seed', type=int, default=1); ap.add_argument('--out') + a = ap.parse_args() + if a.level == 'random': + rng = random.Random(a.seed) + units = [sorted(rng.sample(V.P112, a.size)) for _ in range(a.sample)] + else: + units = json.loads(gzip.decompress(V.UNITS_FILE.read_bytes()))[a.level] + units = [u[:7] if a.level == 'p105' else u for u in units] + if a.sample: + units = random.Random(a.seed).sample(units, a.sample) + t0 = time.time(); tot = collections.Counter(); bads = []; passing = [] + with ProcessPoolExecutor(a.jobs) as ex: + for t, b in ex.map(unit, units, chunksize=8): + tot.update(t); bads += b; passing.append(t[None]) + print(f'{a.level} units {len(units)} time {time.time()-t0:.1f}s reasons {dict(sorted(tot.items(), key=lambda kv: str(kv[0])))}') + print(f'units with no passing frame {sum(p == 0 for p in passing)}; min/max passing frames {min(passing)}/{max(passing)}') + print(f'G-passing D-failures {len(bads)}', bads[:10]) + if a.out: + json.dump(dict(level=a.level, units=len(units), reasons={str(k): v for k, v in tot.items()}, bad=bads), open(a.out, 'w')) + +if __name__ == '__main__': + main() diff --git a/research/full-family-g-without-d/search/mech.py b/research/full-family-g-without-d/search/mech.py new file mode 100644 index 0000000000..bc3533a9a4 --- /dev/null +++ b/research/full-family-g-without-d/search/mech.py @@ -0,0 +1,61 @@ +"""Balanced-D4 mechanism census. Every E8 frame meets complementary coordinate D4 subsystems equally. For each +D4+D4 split S=(Da,Db) containing FRAME0 4+4 (the coordinate splits and their images under the FRAME0 stabiliser +generators), each pivot frame F disjoint from FRAME0 and each pivot k, take the smallest deletion X that makes every +live non-pivot line of Da u Db odd to F[k], and run PR1650's criterion at (X, F).""" +import os +import sys, collections, itertools +sys.path.insert(0, os.environ['PR1650_PACKAGE']) # research/complex-rank8-rigidity-p105 at PR1650 head d960f8a2 +import verify as V +from concurrent.futures import ProcessPoolExecutor + +def half(h): + return frozenset(i for i, v in enumerate(V.LINES) if all(v[j] == 0 for j in range(8) if j not in h)) + +pairs = [(0, 1), (2, 3), (4, 5), (6, 7)] +splits0 = set() +for a in itertools.combinations(range(4), 2): + ha = [c for p in a for c in pairs[p]]; hb = [c for c in range(8) if c not in ha] + splits0.add(frozenset([half(ha), half(hb)])) +def all_splits(): + gens = V.stabiliser(V.FRAME0) + seen = set(splits0); todo = list(splits0) + while todo: + s = todo.pop() + for g in gens: + t = frozenset(frozenset(g[i] for i in d) for d in s) + if t not in seen: + seen.add(t); todo.append(t) + return [tuple(s) for s in seen] + +def check_identity(splits): + for Da, Db in splits: + assert all(len(set(F) & Da) == len(set(F) & Db) for F in V.FRAMES) + assert len(V.FRAME0 & Da) == 4 and len(V.FRAME0 & Db) == 4 + +def job(arg): + splits, p = arg + F = V.FRAMES[p]; out = [] + for Da, Db in splits: + U = (Da | Db) - V.FRAME0 - set(F) + for k in range(8): + X = tuple(sorted(i for i in U if V.G[i][F[k]] == 0)) + if not X: + continue + r = V.criterion(X, F)[0] + out.append((len(X), r, p, k, X)) + return out + +if __name__ == '__main__': + S = all_splits(); check_identity(S) + print('splits', len(S)) + piv = [n for n, m in enumerate(V.FMASK) if not m & V.F0MASK] + print('pivots', len(piv)) + tally = collections.Counter(); best = {} + with ProcessPoolExecutor(6) as ex: + for out in ex.map(job, [(S, p) for p in piv], chunksize=16): + for n, r, p, k, X in out: + tally[(n, r)] += 1 + if r == 'D' and (n not in best): + best[n] = (p, k, X) + print(sorted(tally.items(), key=lambda kv: (kv[0][0], str(kv[0][1])))) + print('first D example per |X|', best) diff --git a/research/full-family-g-without-d/search/minimize.py b/research/full-family-g-without-d/search/minimize.py new file mode 100644 index 0000000000..285619a14a --- /dev/null +++ b/research/full-family-g-without-d/search/minimize.py @@ -0,0 +1,47 @@ +"""Replay walk(seed) to its first full-family G-pass D-fail step, then greedily restore deleted lines while the +criterion verdict stays 'D' (W, blocks, G pass; D fails mod p). Output locally minimal deletion sets.""" +import os +import json, random, sys, collections +from concurrent.futures import ProcessPoolExecutor +sys.path.insert(0, os.environ['PR1650_PACKAGE']) # research/complex-rank8-rigidity-p105 at PR1650 head d960f8a2 +import verify as V +sys.path.insert(0, os.path.dirname(os.path.abspath(__file__))) +from walk import PIVOTS + +def first_dev(seed): + rng = random.Random(seed) + p = rng.choice(PIVOTS); F = V.FRAMES[p] + X = [] + cand = [i for i in V.P112 if i not in F] + rng.shuffle(cand) + for i in cand: + r = V.criterion(tuple(X + [i]), F)[0] + if r in ('W', 'nonempty-blocks'): + continue + X.append(i) + if r == 'D': + return p, X + return None + +def minimize(seed): + fd = first_dev(seed) + if not fd: return None + p, X = fd; F = V.FRAMES[p] + changed = True + while changed: + changed = False + for i in sorted(X, key=lambda i: random.Random(seed * 1000 + i).random()): + Y = [j for j in X if j != i] + if V.criterion(tuple(Y), F)[0] == 'D': + X = Y; changed = True + return dict(seed=seed, pivot=p, X=sorted(X), n=len(X)) + +if __name__ == '__main__': + res = json.load(open(sys.argv[1])) + seeds = [r['seed'] for r in res if r['ndev']] + with ProcessPoolExecutor(10) as ex: + out = [m for m in ex.map(minimize, seeds) if m] + out.sort(key=lambda m: m['n']) + print('minimized', len(out), 'deletion sizes', collections.Counter(m['n'] for m in out).most_common()) + print(out[:3]) + json.dump(out, open(sys.argv[2], 'w')) diff --git a/research/full-family-g-without-d/search/walk.py b/research/full-family-g-without-d/search/walk.py new file mode 100644 index 0000000000..c95c5ddbbd --- /dev/null +++ b/research/full-family-g-without-d/search/walk.py @@ -0,0 +1,49 @@ +"""Adversarial deletion walks: fix a pivot frame F inside P112, delete random non-pivot live lines one at a time +while (W) and nonempty blocks still hold at F, and run PR1650's criterion (full live family) after each step. +Record the first step at which G or D fails; a 'D' verdict (G passed) is a full-family counterexample.""" +import os +import argparse, collections, json, random, sys, time +from concurrent.futures import ProcessPoolExecutor +sys.path.insert(0, os.environ['PR1650_PACKAGE']) # research/complex-rank8-rigidity-p105 at PR1650 head d960f8a2 +import verify as V + +PIVOTS = [n for n, m in enumerate(V.FMASK) if not m & V.F0MASK] + +def walk(seed): + rng = random.Random(seed) + p = rng.choice(PIVOTS); F = V.FRAMES[p] + X = [] + cand = [i for i in V.P112 if i not in F] + rng.shuffle(cand) + events = [] + first = None + for i in cand: + r = V.criterion(tuple(X + [i]), F)[0] + if r in ('W', 'nonempty-blocks'): + continue # deleting i breaks the premises at F: keep i + X.append(i) + if r is not None: + rd = V.criterion(tuple(X), F, skip_g=True)[0] # does D fail too? + events.append((len(X), r, rd)) + if first is None: + first = (len(X), r, rd, sorted(X)) + dev = [e for e in events if e[1] in ('D', 'D-kernel-vectors')] + return dict(seed=seed, pivot=p, final=len(X), first=first, events=events[:5], nevents=len(events), dev=dev[:3], ndev=len(dev), X=sorted(X) if dev else None) + +def main(): + ap = argparse.ArgumentParser(); ap.add_argument('--n', type=int, default=100); ap.add_argument('--start', type=int, default=0) + ap.add_argument('--jobs', type=int, default=10); ap.add_argument('--out') + a = ap.parse_args(); t0 = time.time(); res = [] + c = collections.Counter() + with ProcessPoolExecutor(a.jobs) as ex: + for r in ex.map(walk, range(a.start, a.start + a.n)): + res.append(r) + c[(r['first'][1], r['first'][2]) if r['first'] else None] += 1 + print(f'walks {a.n} time {time.time()-t0:.1f}s first-failure (criterion, D-only) {dict(c)}') + print('final deletion counts', collections.Counter(r['final'] for r in res).most_common(8)) + cex = [r for r in res if r['ndev']] + print('full-family G-pass D-fail first events', len(cex), [ (r['seed'], r['pivot'], r['dev']) for r in cex[:5]]) + if a.out: json.dump(res, open(a.out, 'w')) + +if __name__ == '__main__': + main() diff --git a/research/full-family-g-without-d/verify.py b/research/full-family-g-without-d/verify.py index c459bd4769..15f65fa7dd 100644 --- a/research/full-family-g-without-d/verify.py +++ b/research/full-family-g-without-d/verify.py @@ -12,11 +12,13 @@ 1. F is a live frame; nonempty blocks, (W) and (G) hold; 2. (D) fails: on I_k for one pivot k, the incidence matrix has exact rational rank |I_k| - 8 < |I_k| - 7 (Fraction elimination), while the seven vectors h_kl are independent and lie in its kernel; - 3. fixture 1 also carries a sparse integer kernel vector x (entries +-1 on eight lines) with every live + 3. each fixture carries a sparse integer kernel vector x (entries +-1 on eight lines) with every live frame's row orthogonal to x and rank [h; x] = 8, which certifies the rank drop without elimination; 4. control: restoring any one of the eight deleted lines makes the same pivot pass all four conditions (mod-p rank lower bound plus the h_kl kernel upper bound, as in PR1650); - 5. controls: a mutated certificate is rejected; the pivot-alone sub-family fails (G). + 5. controls: a mutated certificate is rejected; the pivot-alone sub-family fails (G); + 6. each certificate is explained: every one of the 2025 E8 frames meets two orthogonal 12-line D4 subsystems + Da, Db equally (fixture 1: the coordinate halves), and x is the difference of their live indicator vectors. """ import itertools @@ -89,13 +91,21 @@ def grow(cur, cand): # ---------------------------------------------------------------- fixtures (found by deletion walks, see README) +# split = (Da, Db): two disjoint 12-line D4 subsystems, each containing 4 FRAME0 lines. Fixture 1's are the +# coordinate halves (Da on coordinates 0-3, Db on 4-7); fixture 2's were found as an image of those under the +# FRAME0 stabiliser (search/mech.py); verify.py checks only the properties it uses. +# The certificate is x = 1 on the live lines of Da, -1 on the live lines of Db. FIXTURES = [ dict(X=(3, 4, 8, 9, 107, 108, 117, 118), F=(19, 25, 37, 47, 67, 82, 94, 115), k=2, - cert={2: -1, 5: -1, 7: -1, 10: -1, 30: 1, 31: 1, 40: 1, 41: 1}), - dict(X=(13, 18, 22, 27, 34, 35, 36, 37), F=(17, 25, 38, 52, 61, 75, 98, 116), k=7, cert=None), + split=((20, 29, 30, 31, 40, 41, 106, 107, 108, 117, 118, 119), tuple(range(12))), + cert={30: 1, 31: 1, 40: 1, 41: 1, 2: -1, 5: -1, 7: -1, 10: -1}), + dict(X=(13, 18, 22, 27, 34, 35, 36, 37), F=(17, 25, 38, 52, 61, 75, 98, 116), k=7, + split=((0, 1, 34, 35, 36, 37, 106, 111, 112, 113, 114, 119), (6, 11, 12, 13, 18, 19, 20, 21, 22, 27, 28, 29)), + cert={111: 1, 112: 1, 113: 1, 114: 1, 12: -1, 19: -1, 21: -1, 28: -1}), ] + # ---------------------------------------------------------------- ranks def rank_fraction(rows): @@ -217,14 +227,27 @@ def main(): bad.append((kk, len(I), r)) check(f'{tag}.D-fails', [b[0] for b in bad] == [k] and bad[0][2] == bad[0][1] - 8, f'exact rank over Q on I_{k}: {bad[0][2]} = |I_k| - 8 with |I_k| = {bad[0][1]}; other k pass') - if fx['cert']: - I, rows, h = incidence(F, k, non, live_frames) - x = [fx['cert'].get(i, 0) for i in I] - check(f'{tag}.certificate', set(fx['cert']) <= set(I) and kernel_ok(rows, [x]) and rank_fraction(h + [x]) == 8, - f'integer kernel vector {fx["cert"]} is orthogonal to every live frame and outside span(h)') - y = list(x) - y[I.index(next(iter(fx['cert'])))] *= -1 - check(f'{tag}.control.mutated-certificate', not kernel_ok(rows, [y])) + I, rows, h = incidence(F, k, non, live_frames) + x = [fx['cert'].get(i, 0) for i in I] + check(f'{tag}.certificate', set(fx['cert']) <= set(I) and kernel_ok(rows, [x]) and rank_fraction(h + [x]) == 8, + f'integer kernel vector {fx["cert"]} is orthogonal to every live frame and outside span(h)') + # Why: every E8 frame meets Da and Db in equally many lines; FRAME0 and X leave 4 live lines in each, all + # odd to F[k], so x = 1_(Da live) - 1_(Db live) is orthogonal to every live frame's trace on I_k. + Da, Db = (set(d) for d in fx['split']) + dead = set(X) | set(FRAME0) + check(f'{tag}.balanced-d4', len(Da) == len(Db) == 12 and not Da & Db + and len(Da & set(FRAME0)) == len(Db & set(FRAME0)) == 4 + and all(G[a][b] in (0, 1, -1) for a in Da for b in Da if a != b) and all(G[a][b] == 0 for a in Da for b in Db) + and all(len(Da & set(Fr)) == len(Db & set(Fr)) for Fr in FRAMES) + and fx['cert'] == {**{i: 1 for i in Da - dead}, **{i: -1 for i in Db - dead}}, + f'Da, Db orthogonal 12-line systems; all 2025 frames meet them equally; certificate = 1 on Da live ' + f'{sorted(Da - dead)}, -1 on Db live {sorted(Db - dead)}') + if n == 1: + check(f'{tag}.coordinate-halves', Da == {i for i, v in enumerate(LINES) if not any(v[4:])} + and Db == {i for i, v in enumerate(LINES) if not any(v[:4])}) + y = list(x) + y[I.index(next(iter(fx['cert'])))] *= -1 + check(f'{tag}.control.mutated-certificate', not kernel_ok(rows, [y])) for x in X: Y = tuple(i for i in X if i != x) lf, nn, oo = setup(Y, F) @@ -234,7 +257,7 @@ def main(): lf, nn, oo = setup(X, F, frames=[F]) check(f'{tag}.control.pivot-alone-fails-G', not condition_g(nn, oo, lf)) print('PASS_FULL_FAMILY_G_WITHOUT_D fixtures=2: (W), nonempty blocks and (G) on the full live family do not ' - 'imply (D) (exact), and each counterexample needs all eight deletions') + 'imply (D) (exact), and restoring any one deleted line makes the same pivot pass') if __name__ == '__main__': From 9ac70b1c3078c1de4c60d23652bb0792cb7db1ca Mon Sep 17 00:00:00 2001 From: josie Date: Wed, 14 Oct 2026 01:39:38 -0400 Subject: [PATCH 3/5] full-family-g-without-d: label unregistered counts, separate support verdicts in search Co-Authored-By: Claude Opus 5.5 --- research/full-family-g-without-d/README.md | 10 ++++++---- research/full-family-g-without-d/search/allframes.py | 2 +- 2 files changed, 7 insertions(+), 5 deletions(-) diff --git a/research/full-family-g-without-d/README.md b/research/full-family-g-without-d/README.md index ed7c2cc4b9..c29722bc68 100644 --- a/research/full-family-g-without-d/README.md +++ b/research/full-family-g-without-d/README.md @@ -30,13 +30,15 @@ exact fixtures. Fixture 1: supported on I_2, and it is not a combination of the h_2l. - **Locally minimal.** Restoring any one of the eight deleted lines makes the same pivot pass all four conditions. Each restored live set has 816 live frames. -- This unit is still rigid through other pivots: 674 of its live frames pass all four conditions. Of the rest, - 96 pass (W), blocks and (G) but fail (D), 4 fail (G) and 10 fail (W). +- This unit is still rigid through other pivots. Running PR1650's criterion at every live frame (`unit()` in + `search/allframes.py`; unregistered, reproduced independently by the Codex review): 674 pass all four + conditions, 96 pass (W), blocks and (G) but fail (D), 4 fail (G) and 10 fail (W). Fixture 2, X = (13, 18, 22, 27, 34, 35, 36, 37) with pivot (17, 25, 38, 52, 61, 75, 98, 116), has the same pattern at k = 7: rank 44 on 52 lines. Its certificate is +1 on {111, 112, 113, 114} and −1 on {12, 19, 21, 28}. -These come from a non-coordinate pair of orthogonal D4 subsystems, each containing 4 FRAME0 lines; the pair is an -image of the coordinate halves under the FRAME0 stabiliser (`search/mech.py`). +These come from a non-coordinate pair of orthogonal 12-line systems, each containing 4 FRAME0 lines. `verify.py` +checks those properties and the frame identity; that the pair is an image of the coordinate halves under the FRAME0 +stabiliser comes from `search/mech.py` and is not re-checked. So the conditions in PR1650's question cannot replace (D) in general. Whether they can on P105 to P111 (|X| ≤ 7) is still open; the evidence below found no counterexample there. diff --git a/research/full-family-g-without-d/search/allframes.py b/research/full-family-g-without-d/search/allframes.py index cf0dac4a15..2381fcb575 100644 --- a/research/full-family-g-without-d/search/allframes.py +++ b/research/full-family-g-without-d/search/allframes.py @@ -13,7 +13,7 @@ def unit(X): continue r = V.criterion(tuple(X), V.FRAMES[n])[0] tally[r] += 1 - if r in ('D', 'D-kernel-vectors', 'support'): + if r in ('D', 'D-kernel-vectors'): bad.append((list(X), n, r)) return tally, bad From cb8455ff476dafabfbe99857bb78ceb58b01ab48 Mon Sep 17 00:00:00 2001 From: josie Date: Wed, 14 Oct 2026 01:58:01 -0400 Subject: [PATCH 4/5] full-family-g-without-d: record the every-frame P107 census Co-Authored-By: Claude Opus 5.5 --- research/full-family-g-without-d/README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/research/full-family-g-without-d/README.md b/research/full-family-g-without-d/README.md index c29722bc68..7846da4ff4 100644 --- a/research/full-family-g-without-d/README.md +++ b/research/full-family-g-without-d/README.md @@ -55,7 +55,7 @@ above. Set `PR1650_PACKAGE` to that package's directory. Wall times are on a sha | `minimize.py` on those 176 | restore deleted lines greedily while the verdict stays (D)-fail | locally minimal sizes 8 (20 sets), 10 (48), 11–28 (the rest); **none below 8** | | `mech.py` | all 7 D4⊕D4 splits that contain FRAME0 as 4+4 (closure of the coordinate splits under the stabiliser generators), all 1260 pivots disjoint from FRAME0, all k; X = the live split lines even to F[k] | sizes 4, 6, 8, 10. **(D) fails only at |X| = 8** (32256 cases). Every |X| = 4, 6 or 10 case passes or fails blocks. | | `allframes.py random --size s --sample 100` | random X of size 8, 9 and 10 (seeds 8, 9, 10), every live frame | 189952 frames: none fails (G) or (D); only (W) fails | -| `allframes.py p107` | every live frame of all 1614 P107 units | P107_RESULT | +| `allframes.py p107` | every live frame of all 1614 P107 units (1807 s wall, 8 processes) | 1393377 frames: 1386438 pass all four, 6936 fail (W), 3 fail blocks; **none fails (G) or (D)** | The first two rows also give the fixtures: walk seeds 1023 and 1759 minimize to fixtures 1 and 2 (pivot indices 1765 and 1670 in PR1650's frame order). From 5c959793a63332f54e7436cd8ded0e979774117e Mon Sep 17 00:00:00 2001 From: josie Date: Wed, 14 Oct 2026 01:58:13 -0400 Subject: [PATCH 5/5] full-family-g-without-d: correct the P106 census cost estimate Co-Authored-By: Claude Opus 5.5 --- research/full-family-g-without-d/README.md | 2 +- research/full-family-g-without-d/TASK.json | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/research/full-family-g-without-d/README.md b/research/full-family-g-without-d/README.md index 7846da4ff4..50cb846dc4 100644 --- a/research/full-family-g-without-d/README.md +++ b/research/full-family-g-without-d/README.md @@ -85,7 +85,7 @@ Expected last line: `PASS_FULL_FAMILY_G_WITHOUT_D fixtures=2: ...`. `-O` is refu 1. **Does the shortcut hold for |X| ≤ 7 (P105 to P111)?** - *Why it matters.* If it does, the P105 replay could drop the rank computations that take nearly all of its 1200 s budget. - - *First step.* Run an every-frame census on the 19295 P106 units (about 3.6 CPU-hours with PR1650's criterion), + - *First step.* Run an every-frame census on the 19295 P106 units (about 40 CPU-hours with PR1650's criterion at the P107 rate of 9 CPU-s per unit), then on a P105 sample. Or prove that a balanced pair of line sets inside I_k needs eight deletions. - *Blocker.* Compute, and no candidate lemma. The D4 mechanism needs exactly eight, and no mechanism with fewer appeared in the searches above. diff --git a/research/full-family-g-without-d/TASK.json b/research/full-family-g-without-d/TASK.json index adf232aa13..0461729180 100644 --- a/research/full-family-g-without-d/TASK.json +++ b/research/full-family-g-without-d/TASK.json @@ -59,7 +59,7 @@ { "question": "For |X| <= 7 (P105 to P111), does every pivot passing (W), nonempty blocks and (G) on the full live family pass (D)?", "why_it_matters": "PR1650's open question 1 is now false at |X| = 8; if it holds for |X| <= 7, the P105 replay could drop its rank computations, which are almost all of its 1200 s budget.", - "first_step": "Every-frame census of the 19295 P106 units (about 3.6 CPU-hours with PR1650's criterion), or a lemma explaining why the eight-line rank drop (two quadruples of lines met equally by every live frame) needs eight deletions.", + "first_step": "Every-frame census of the 19295 P106 units (about 40 CPU-hours with PR1650's criterion at the P107 rate of 9 CPU-s per unit), or a lemma explaining why the eight-line rank drop (two quadruples of lines met equally by every live frame) needs eight deletions.", "blocked_by": "Compute for P106/P105 every-frame censuses; no candidate lemma." }, {