Research: (G) does not imply (D) for full live families at eight deletions (no new kappa)

research/full-family-g-without-d/README.md

@@ -0,0 +1,109 @@
+# (G) does not imply (D) even for the full live family (no new κ)
+
+**Status: exact finite counterexample to a proposed shortcut, plus scoped search evidence. No κ claim, no
+construction, and no change to any proved rigidity result.**
+
+[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.
+
+## Result
+
+**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. 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 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.
+
+## 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).
+
+| 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 (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).
+
+## 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
+```
+
+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
+
+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 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.
+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
+
+- **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.

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"
+    }
+  ]
+}

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 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."
+    },
+    {
+      "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."
+    }
+  ]
+}

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."
+    }
+  ]
+}

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'):
+            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()

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)