Scoped negative result: PR589's bit word is exactly frame-optimal (no new kappa)

research/bit589-frame-optimum/README.md

@@ -0,0 +1,61 @@
+# PR589's bit word is exactly frame-optimal (scoped negative result, no new kappa)
+
+**Claim.** Keep PR589's gate sequence, scalar program, start/final frames and the retained totals' COPY frames
+(decoder constant 63) fixed. Then no reassignment of gate frames, however many gates change at once, raises the
+nine-stage bit saving c = 0.001733427039589844234749. The same holds for PR555's base word. PR589's tuner reached
+its word by greedy single-gate moves and makes no optimality claim. This closes the frame-only part of that question exactly.
+
+## Method (`frameopt.py`, standard library only)
+
+1. **Bounds.** A forward pass gives each gate's least legal frame (closure of its operands' current frames).
+   A backward pass gives its greatest legal frame (intersection of what its operands may hold later): the final
+   frames, targets at frame 0 before the scatter, and pinned COPY frames. Every legal assignment lies between the two.
+   The word's own frames do.
+2. **Freedom.** Only **159 of 5,472 gates** have any slack. Of those, 155 have exactly two options and the rest have
+   5, 6 or 17. Free gates couple only when they are consecutive on a register; a fixed gate in between pins the frame.
+   They form **133 independent components** of sizes 1 (119), 2 (4), 3 (9) and 5 (1).
+3. **Exact objective.** At z = c the moment is linear in the paid profile:
+   Σ_d n_d (d/(mW)) (m/d)^c with m = 64, and the global profile is 288 × local plus a fixed idle remainder.
+   So a change raises c only if it lowers Σ_d n_d·d·(64/d)^c. Each component is enumerated exhaustively
+   (398 assignments; 55 fail nesting) and scored by a full replay.
+
+## Result
+
+| word | start profile | improving components | smallest strict loss | same-profile alternatives |
+|---|---|---|---|---|
+| PR589 (`tune/bitE8mut-p111-tuned`) | `{1:1323,2:1342,3:79,4:44,5:102,6:11,7:19}` | **0** | 9.11e−4 | 10 |
+| PR555 (`data/bitE8mut-p111`) | `{1:1321,2:1342,3:80,4:47,5:102,6:10,7:18}` | **0** | 9.11e−4 | 9 |
+| **positive control**: PR589 with every free gate at its least frame | `{1:1446,2:1326,3:49,…}` | 37 | — | 8 |
+
+The replayed start profiles equal the recorded local histograms. The positive control recovers **exactly** PR589's
+profile. PR555 also being frame-optimal is consistent with PR589's gain coming from its two transports (gate-order
+changes), not from reframing alone.
+
+## Reproduce
+
+```sh
+bash research/bit589-frame-optimum/verify.sh     # ~16 s; last line PASS_BIT589_FRAME_OPTIMUM
+```
+
+Python 3.11+, standard library only (CPython 3.12.13 used). Base commit `f567884aeb8851b6e794af1184119a3bfbe1e631`.
+The inputs are the committed words `research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz` (PR589) and
+`research/e8-bit-p111-tuned/data/bitE8mut-p111.json.gz` (PR555). `verify.log` is the run's output.
+
+## Scope
+
+- **Search class: frame-only.** Gate order, gate operands, the scatter and the COPY frames are fixed.
+  Transports, Steinberg rewrites, new helpers, or different retained-total frames are outside this result.
+- **Model.** Frames are closed sets of live E8 lines, ranks are computed mod 2^31−1 over integer root-line
+  coordinates, as PR589's own tuner does, and the paid profile is PR589's (climbs plus COPY ranks). C gates may take
+  any legal frame here, although interface hypothesis H4 fixes them at the full frame. Relaxing that rule only enlarges
+  the search, so the negative result holds a fortiori. Hosting and record legality are not modelled for the same reason.
+- **κ.** The bit side does not bind the selected κ (complex b ≈ 0.0016644 < c), so this changes no κ.
+  It says that future bit headroom on this word must come from gate-order or structural changes.
+- This is a finite exhaustive computation on two words, not a statement about other bit words.
+
+## Credit
+
+The PR589 word and tuner are by DreamingOfClouds, on eumemic's PR555 and the PR543/545/510 lineage. Exact
+frame-optimality certificates for complex providers exist in #815 and #864; this is the bit-side counterpart with a
+different, component-enumeration method. Assignment seed 16 (bit-supplier track). Prepared with substantial AI
+assistance (Claude Code, Anthropic). Apache-2.0.

research/bit589-frame-optimum/frameopt.py

@@ -0,0 +1,183 @@
+"""Exact frame-only optimum of a bitE8/1+mut bit word with its gate sequence fixed.
+
+Every gate g puts all its operands on one frame f_g; each register's frames must nest from its start to its final
+frame. Targets stay at frame 0 until the scatter. Retained totals keep their scatter frames, so the COPY ranks and the
+decoder constant do not change. Frames are closed sets of live lines. The paid profile counts each climb by its rank step.
+
+1. Forward least frames lo_g and backward greatest frames hi_g bound every legal f_g. Every closed frame between
+   them is enumerated.
+2. Free gates (lo_g != hi_g) couple only through consecutive free gates on a register. A fixed gate in between pins
+   the frame there, so the components are independent in both legality and cost.
+3. At z = c the moment sum_d n_d (d/(mW)) (m/d)^z is linear in the profile. A frame change can raise c only if it
+   lowers sum_d n_d d (m/d)^c. Each component is enumerated exhaustively and its best combination kept.
+
+Usage: frameopt.py WORD.json.gz C [--degrade]
+--degrade is the positive control: every free gate starts at its least frame.
+"""
+import gzip, itertools, json, sys
+from collections import Counter
+from fractions import Fraction
+from functools import reduce
+from operator import or_, and_
+
+w = json.load(gzip.open(sys.argv[1], 'rt'))
+c = float(Fraction(sys.argv[2]))
+V, N, L = w['v'], 2 * w['v'] + w['R'], w['lines']
+P = 2147483647
+
+
+def rank(rows):
+    rows, rk = [[x % P for x in r] for r in rows], 0
+    for col in range(len(L[0])):
+        p = next((i for i in range(rk, len(rows)) if rows[i][col]), None)
+        if p is None:
+            continue
+        rows[rk], rows[p] = rows[p], rows[rk]
+        inv = pow(rows[rk][col], P - 2, P)
+        rows[rk] = [x * inv % P for x in rows[rk]]
+        for i in range(len(rows)):
+            if i != rk and rows[i][col]:
+                f = rows[i][col]
+                rows[i] = [(a - f * b) % P for a, b in zip(rows[i], rows[rk])]
+        rk += 1
+    return rk
+
+
+bits = lambda m: [i for i in range(V) if m >> i & 1]
+_close = {}
+
+
+def close(m):
+    """(closed line set spanned by mask m, its rank)"""
+    if m not in _close:
+        sel = [L[i] for i in bits(m)]
+        rk = rank(sel) if sel else 0
+        _close[m] = (sum(1 << i for i in range(V) if m >> i & 1 or (sel and rank(sel + [L[i]]) == rk)), rk)
+    return _close[m]
+
+
+dim = lambda m: close(m)[1]
+FM = [sum(1 << i for i in f) for f in w['frames']]
+assert all(close(m)[0] == m for m in FM), 'catalogue frame not closed'
+SCATTER = ('S', 0, [], None)
+gates = [(s, k, [g[1], *g[2]], FM[g[0]]) for s in 'DA' for k, g in enumerate(w[s])] + [SCATTER] + \
+        [(s, k, [g[1], *g[2]], FM[g[0]]) for s in 'BC' for k, g in enumerate(w[s])]
+start, final = [FM[f] for f in w['start']], [FM[f] for f in w['final']]
+word = {(s, k): f for s, k, _, f in gates if s != 'S'}
+
+cur = start.copy()
+for s, k, regs, f in gates[:gates.index(SCATTER)]:
+    for r in regs:
+        cur[r] = f
+pin = {q: cur[q] for q in w['ret']}
+
+# 1. bounds
+lo, cur = {}, start.copy()
+for s, k, regs, f in gates:
+    if s == 'S':
+        assert all(cur[q] & ~pin[q] == 0 for q in pin)
+        for q in pin:
+            cur[q] = pin[q]
+        continue
+    lo[s, k] = m = close(reduce(or_, (cur[r] for r in regs)))[0]
+    for r in regs:
+        cur[r] = m
+hi, ub = {}, final.copy()
+for s, k, regs, f in reversed(gates):
+    if s == 'S':
+        for t in range(V, 2 * V):
+            ub[t] = 0
+        for q in pin:
+            assert pin[q] & ~ub[q] == 0
+            ub[q] = pin[q]
+        continue
+    hi[s, k] = m = reduce(and_, (ub[r] for r in regs))  # an intersection of closed sets is closed
+    for r in regs:
+        ub[r] = m
+assert all(lo[x] & ~word[x] == 0 and word[x] & ~hi[x] == 0 for x in word), 'word frame outside its bounds'
+
+opts = {}
+for x in word:
+    if lo[x] != hi[x]:
+        seen, todo = {lo[x]}, [lo[x]]
+        while todo:
+            m = todo.pop()
+            for i in bits(hi[x] & ~m):
+                n = close(m | 1 << i)[0]
+                if n & ~hi[x] == 0 and n not in seen:
+                    seen.add(n)
+                    todo.append(n)
+        opts[x] = sorted(seen, key=dim)
+
+# 2. components of free gates
+parent = {x: x for x in opts}
+
+
+def find(x):
+    while parent[x] != x:
+        x = parent[x]
+    return x
+
+
+last = {}
+for s, k, regs, f in gates:
+    for r in regs:
+        if (s, k) in opts and last.get(r) in opts:
+            parent[find(last[r])] = find((s, k))
+        last[r] = (s, k)
+members = {}
+for x in opts:
+    members.setdefault(find(x), []).append(x)
+
+
+# 3. exact enumeration
+def profile(fr):
+    """paid profile (climbs plus COPY ranks) of a frame assignment, or None if some chain does not nest"""
+    cur, H = start.copy(), Counter()
+    for s, k, regs, _ in gates + [('F', 0, range(N), None)]:
+        if s == 'S':
+            H.update(dim(cur[q]) for q in pin)
+            continue
+        for r in regs:
+            m = final[r] if s == 'F' else fr[s, k]
+            if cur[r] != m:
+                if cur[r] & ~m:
+                    return None
+                H[dim(m) - dim(cur[r])] += 1
+                cur[r] = m
+    return H
+
+
+cost = lambda H: sum(n * d * (64 / d) ** c for d, n in H.items())
+base = dict(word)
+if '--degrade' in sys.argv:
+    base.update({x: lo[x] for x in opts})
+H0 = profile(base)
+best, tried, illegal, ties, margins = dict(base), 0, 0, 0, []
+for xs in members.values():
+    deltas = []
+    for combo in itertools.product(*(opts[x] for x in xs)):
+        fr = dict(base)
+        fr.update(zip(xs, combo))
+        H = profile(fr)
+        tried += 1
+        if H is None:
+            illegal += 1
+        elif H == H0:
+            ties += combo != tuple(base[x] for x in xs)
+        else:
+            deltas.append((cost(H) - cost(H0), combo))
+    if deltas:
+        d, combo = min(deltas)
+        margins.append(d)
+        if d < 0:
+            best.update(zip(xs, combo))
+H1 = profile(best)
+result = dict(
+    word=sys.argv[1].rsplit('/', 1)[-1], degraded_start='--degrade' in sys.argv, gates=len(word),
+    free_gates=len(opts), components=len(members), component_sizes=dict(Counter(map(len, members.values()))),
+    assignments_enumerated=tried, non_nesting_rejected=illegal, same_profile_alternatives=ties,
+    start_profile=dict(sorted(H0.items())), optimum_profile=dict(sorted(H1.items())),
+    improving_components=sum(d < 0 for d in margins),
+    smallest_alternative_delta=min(margins) if margins else None, weighted_cost_delta=cost(H1) - cost(H0))
+print(json.dumps(result))

research/bit589-frame-optimum/verify.sh

@@ -0,0 +1,17 @@
+#!/usr/bin/env bash
+# Exact frame-only optimum of PR589's bit word, PR555's base word, and the degraded positive control.
+# Usage (repository root): bash research/bit589-frame-optimum/verify.sh   -> last line PASS_BIT589_FRAME_OPTIMUM
+set -euo pipefail
+PY=${PY:-python3}; HERE=$(cd "$(dirname "$0")" && pwd); W=$HERE/../e8-bit-p111-tuned
+C589=1733427039589844234749/1000000000000000000000000
+C555=1733052823330162099157/1000000000000000000000000
+run() { $PY -I -B "$HERE/frameopt.py" "$@"; }
+check() { $PY -I -c "import json,sys;r=json.loads(sys.argv[1]);assert $2,r;print('$1',r['improving_components'],r['optimum_profile'])" "$3"; }
+P589='{"1":1323,"2":1342,"3":79,"4":44,"5":102,"6":11,"7":19}'
+a=$(run "$W/tune/bitE8mut-p111-tuned.json.gz" $C589); echo "$a"
+check "PR589 frame-optimal" "r['improving_components']==0 and r['smallest_alternative_delta']>0" "$a"
+b=$(run "$W/data/bitE8mut-p111.json.gz" $C555); echo "$b"
+check "PR555 frame-optimal" "r['improving_components']==0 and r['smallest_alternative_delta']>0" "$b"
+d=$(run "$W/tune/bitE8mut-p111-tuned.json.gz" $C589 --degrade); echo "$d"
+check "degraded control recovers PR589" "r['improving_components']>0 and r['optimum_profile']==json.loads('$P589')" "$d"
+echo PASS_BIT589_FRAME_OPTIMUM