diff --git a/research/bit589-frame-optimum/README.md b/research/bit589-frame-optimum/README.md new file mode 100644 index 0000000000..6388f0c33c --- /dev/null +++ b/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. diff --git a/research/bit589-frame-optimum/frameopt.py b/research/bit589-frame-optimum/frameopt.py new file mode 100644 index 0000000000..735b489a69 --- /dev/null +++ b/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)) diff --git a/research/bit589-frame-optimum/verify.sh b/research/bit589-frame-optimum/verify.sh new file mode 100644 index 0000000000..4352170bc2 --- /dev/null +++ b/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