Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
53 changes: 53 additions & 0 deletions research/encoded-exit-obstructions/README.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,53 @@
# Structural levers and the encoded-output exit: exact obstructions (no κ claim)

This screens the structural targets of zxv's #5428 against the selected #5413 caller. The raw root is 0.00302728824993955878, and the fixed-profile ceiling is U = 0.00302728825, only 6·10⁻¹⁴ above it. So **any** legal paid-profile improvement would beat U. The obstacle is legality, not size.

## Main result: buying b = Z·Q·Y needs ≥ 112 paid jobs (`r17-zqy-producer-bound/`)

If the backward FULL could exit with the observation b = Z·Q·Y, the bound would rise to about 0.00714 (#5415, #5428 target 1). The break-even purchase cost is τ = 63.5226717504634927 H1-equivalents per backward FULL.

**Theorem.** Every exact, width-uniform producer of b from post-return data needs **at least 112 paid jobs per backward FULL**. Post-return data means X, Y, H, the helpers, owned zeros, and anything independent of the FULL's inputs. The bound holds for jobs of any rank or type (Clifford or not) and any sharing pattern, including:
- shared higher-rank intermediates;
- Hadamard or Fourier butterflies over ports;
- block transforms;
- joint diagonalisation.

The whole #5415 exit needs at least **120**. So #5415's constructive 120-H1 exit is **optimal**, and no producer reaches τ. This extends #5427, which shows b is not free, to paid producers.

- **Lemma 1:** tensor powers of distinct operators are linearly independent across fibre widths.
- **Lemma 2:** each paid job adds at most one vector to the span of non-base right-monomial-coset values.
- **Target:** the target needs 112 independent coset directions, 56 per mode. These are computed exactly over ℚ with the repository's `clifford_exact` evaluator, including absolute phase, in all four K conventions.
- **Controls:**
- identity port maps give 8;
- b written in y-coordinates gives 8;
- the monomial target Z·Y gives 0;
- 300 random programs never beat Lemma 2;
- making one C gate free breaks the lemma.

**Open:** a **pre-return** copy of y or h allows an 8×H8 producer. It costs 63.598, just above τ = 63.523, so its root is 0.0030223874 < U. Beating it means beating 8 rank-8 transforms by more than 0.076 H1-equivalents per FULL. That is the centre-interface lever (#4694/#4698/#4700), which is not covered here.

## Other levers (`r16-structural-levers/`)

| Lever | Value if legal | Result |
|---|---|---|
| Split rank-9 productive helpers into independent products | +1.358e-6 per split (0.00353 if all) | **no free split point in either orientation** (exact row replay on all 632 registers; positive control passes). A non-free split recreates the relation lever closed by #5462 |
| Encoded exit via conjugated queries (term by term) | up to 0.00714 | no port or mode map commutes with Q or D; the 112 port conjugates lie in 112 distinct monomial cosets, so ≥ 120 H1 (strengthened to every producer above) |
| Larger coupled provider with a bought exit | — | needs ≥ 15 modes per FULL; the #5402 family has 8 |
| Productive centre payload; query-shear deletion; query/local fusion | — | earns 0, breaks rank-mass balance, or is illegal |
| New helper factorization (defragmentation) | ceilings 0.00499 (helpers) / 0.00371 (mains) | closed at a fixed operation set (#5426/#5422/#5465); a new operation set means a new native word and a rebuilt #5383 → #5402 → #5413 pipeline |

**What a real gain still needs:** either a new native operation set whose helper threads read port lines at frames they already visit, or the centre-interface lever.

## Reproduce

Python 3.12. The tools expect a checkout of main as the working directory; see each README.

```sh
python3.12 -B research/encoded-exit-obstructions/r17-zqy-producer-bound/tools/exit_lb.py
python3.12 -B research/encoded-exit-obstructions/r17-zqy-producer-bound/tools/lemma_sim.py
python3.12 -B research/encoded-exit-obstructions/r17-zqy-producer-bound/tools/price17.py
```

Expected outputs are stored next to each script (`*.txt` / `*.json`).

**Credits.** zxv (#5428 targets, #4359 paradigm, coded-native caller and `clifford_exact`), the #5415 and #5427 authors, Dillon Amburgey (#5402), Clear1nsight (#5413), aliromman (#5398/#5383), Cao Yifan (#4610 word), and the reviewers of the p19 line (#5270/#5440): jwr404, zxv, Matarener and Clear1nsight. Prepared by Joel Pulikkan (GamingPuzzled) with Claude Opus 5.5 (Anthropic) via Claude Code. Apache-2.0.
47 changes: 47 additions & 0 deletions research/encoded-exit-obstructions/r16-structural-levers/README.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,47 @@
# R16 notes: structural levers against the fixed-profile ceiling U = 0.00302728825 (no κ claim)

Goal: a conditional κ above U = 0.00302728825 from a real change to the paid/target structure of the
supplier, not from compiler headroom. Base: selected #5413 profile (see `PROFILE.json` of #5428). Its raw
root is 0.00302728824993955878 and dM/dC = −246,768.15 (`tools/price16.py`, Decimal, 50 digits; this
matches #5428's bracket). U sits only 6×10⁻¹⁴ above that raw root. **So any genuine paid-profile
improvement beats U**, even a single 1+1→2 merge in one orientation of one local (about +1.7×10⁻⁸).
The bar is not size. It is whether the change is legal.

**Outcome: no lever survives.** Nothing was built. Two exact screens are new here: the helper-split
screen and the ZQY-observation screen. The rest are pricings with Decimal arithmetic of known blockers.

## Lever table (selected profile; float/Decimal screens unless marked exact)

| # | Lever | Optimistic ceiling (raw root) | Verdict / blocker |
|---|---|---:|---|
| 1 | Split a rank-9 productive helper into independent products (9→4+5) | +1.358e-6 per split (×18 locals); all rank-9 helpers split: 0.0035309 | **Dead on the #4610 word (exact screen, new).** A free split needs a moment, at an intermediate frame with climbs still ahead, when the helper's row is pure (only its own input) and no other register (C0 included) holds its input. `tools/split.py` finds **0** such points in both orientations. The positive control passes: the final rows equal the expected rows for all 632 registers in both orientations. 38 helpers are clean inside their op span, but only at end frames. A non-free split leaves the outputs coupled, e.g. (−x_b, G₉x_a + G_{9/F}x_b). Decoding those is the relation/coupled-output lever, which is exhausted (#5462: exact optimum is 8 per backward local). |
| 2 | New helper factorization so frames grow in large shared steps (defragmentation) | helpers one climb each: 0.0049895 (#5426 re-optimised controller: 0.0051074); mains one climb each: 0.0037079 (#5426: 0.0037103); Λ=0: 0.0081386 (#5426) | **Blocked: needs a new operation set.** At a fixed operation set it is closed: #5426 (exact, single-level drops, any order), #5422 (no H1+H1→H2 fusion by free rewiring), #5465 (reorder+reframe LP ≤ 0.003107; restricted MIPs gap 0; one-step correction rewrites 0 gains). There are also no end slack climbs: every helper and main register starts and ends at the frame of its first and last op (`tools/ends.py`). Helper threads are compute/uncompute chains: each reads a port line at a low frame and undoes the read at the full frame (e.g. h300: x19 at dim 1, x18 at dim 3, uncompute at dim 9). Fragmentation is set by the order in which those port lines climb. A redesign is a new native word with a new replay, new phases and a new caller pipeline; it does not fit in 3 hours. No ceiling smaller than 0.0049895 is proved for new operation sets. |
| 3 | Paid merges by local rewrites (1+1→2) | +3.06e-7 per merge (×18) | Closed by #5422/#5426/#5465 (see row 2). |
| 4 | Encoded-output exit of #5402's coupled modes by buying b = ZQY (#5428 target 1, #5415) | b free: 0.0071410 (+4.1e-3). Break-even: X ≤ **63** H1 per backward FULL (16 FULLs) on top of the 8 restoring H1 (`tools/zqy_budget.py`) | **Dead in the sum-then-query grammar (exact screen, new).** b_k = Σ_j M_kj/2 · Km_k⁻¹ Kp_j Q Y_j. Using the repository's `clifford_exact` evaluator with absolute phase: no Kp_j or Km_k commutes with Q or with D. The 112 port conjugates Kp_j⁻¹ Q Kp_j lie in 112 distinct monomial cosets, left and right (all pairwise quotients have rank 2). Per mode, the 56 supported ports give 56 distinct classes. So no two Y_j can share one rank-one query, even with free monomial maps on both sides. b needs ≥ 112 + 8 = 120 H1 per FULL, which is exactly #5415's constructive bound and far above 63. #5427 already shows that b is absent from every retained observation. Open: producing b by a non-termwise mixture of higher-rank jobs is not covered by this screen. |
| 5 | Larger coupled type (more modes sharing the port support), bought exit | needs ≥ **15** modes per FULL to pay at 112+m H1 (`tools/modes_budget.py`: m=14 gives 0.0029741, m=15 gives 0.0034798) | **Dead in the #5402 family:** the modes come from the 8 centre calls per local (one per centre-deletion cache), so m ≤ 8. |
| 6 | Free observation: delete query shears | delete all 1680: 0.0099; one H1 per local (×18): +7.3e-5 | Mass is not conserved, so this is not a real lever. Every thin query stays paid (#5415). No paid response can be reused (#5427: 0 of 3,298 climbs per orientation, 0 of 63 caller outputs). Control (`tools/zeroclimb.py`): no climb acts on an identically zero row in either orientation. |
| 7 | Query/local fusion (rank-1 query + adjacent rank-1 local climb) | 1680×(1+1→2): +2.88e-5 | Illegal without a new native interface: the query temporary shares no frame with the local climbs (R12 §5). |
| 8 | Centre: merge the 8 rank-8 transports of a centre index; remove the centre | merge: +4.10e-5 (illegal, #4698/#4700); removal: 0.0076685 | Contested (#4694/#4698/#4700/#4888). Out of scope by instruction. The uncontested variant is a productive centre payload. It fails because each of the 8 centre transports is a single 0↔rank-8 move (backward 0→8, forward 8→0; checked on the word), and owned C0 is CLEARed and COPY-filled before every use. No independent input survives a transport to earn credit, so the credit is 0. |
| 9 | Controller length / thinning / idles with the fixed local profile | — | Closed: #4658/#4659 (all p, all masks), #4664/#4666/#4674, #5405, #5429. |
| 10 | Multi-type recursive supplier (#5428 target 5), vector index code (#5428 target 3), decoder factorization (#5428 target 4) | not priceable without a concrete histogram | No candidate type pair or mask could be built and priced within this session. #5428 records the known failures: the 3\|7 macro is only a scheduling saving, and the phase-accumulator closure is critical before wrappers. |
| ref | p19 coded-reverse chain (#5270/#5440) | 0.0034 claimed | Failure modes (reviews by Matarener, zxv, gvconly, jwr404, Clear1nsight): the native call supplies D, not R = DQ. The missing Q costs 4,256 rank-1 jobs per unit, and the Q-conjugated terminal gauge is forced. The replay was compared against an operator different from the priced controller, and it reused the same nine axes while crediting fresh blocks. The compiler constants were inherited from the p7 unit shape. Lever 4's coset obstruction has the same form: Q does not pass through the port normalizers. |

## What would have to be true for a gain
- A new native operation set, not a reordering of the existing one, in which helper threads read port lines at
frames they already visit. Every 1+1→2 merge it buys is worth +3.06e-7. It must come with a complete replay
of all 632 columns and a new caller pipeline (#5383→#5402→#5413), because the owned relations are pinned
to helper rows.
- Or an observation producer for b = ZQY that is **not** a termwise sum of conjugated queries, costing
≤ 63 H1-equivalent rank mass per FULL. The coset screen rules out the termwise route.

## Tools (`../tools/`, run with /opt/homebrew/bin/python3.12; inputs read from ~/imb-r13 (#4610 word) and ~/imb-r16 (upstream main 32890bc5d))
- `price16.py`: Decimal pricer for the selected profile. `levers.py`: the ceiling table (output in `levers.txt`).
- `split.py` and `split_ctl.py`: exact row replay for the free-split screen and its controls (`split.txt`, `split_ctl.txt`).
- `ends.py`, `thread.py`: end-slack census and per-register thread dump.
- `zqy_budget.py`, `modes_budget.py`: exit purchase budgets. `zqy_commute.py`: Clifford coset screen (`zqy_commute.txt`).
- `zeroclimb.py`: control showing no climb on a zero row.

Credits: Cao Yifan (#4610 word), zxv (#4359 paradigm, #5415, #5428), Dillon Amburgey (#5402 provider),
Ali Romman (#5383/#5398 relations and caller), Chris R / Clear1nsight (#5413 caller, audits), Matarener
(#5422/#5426/#5427/#5433), Cinna Davis (controller line), reviewers of #5270/#5440. Prepared with Claude Opus 5.5
(Anthropic) via Claude Code, directed by Joel Pulikkan (GamingPuzzled).
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
base root 0.0030272882499395587812724555013848588705741016191552 U 0.00302728825
one helper split 9->4+5 (all 18 locals) root 0.0030286465 dC +1.358e-06 beats U: True
all rank-9 helpers split 4+5 root 0.0035309323 dC +5.036e-04 beats U: True
helpers credited per climb (helper defragmentation ceiling) root 0.0049894594 dC +1.962e-03 beats U: True
one 1+1->2 helper visit merge (all 18 locals) root 0.0030275941 dC +3.058e-07 beats U: True
main x/y single rank-8 climb (main defragmentation ceiling) root 0.0037079334 dC +6.806e-04 beats U: True
query/local fusion 1680 x (1+1->2) root 0.0030561027 dC +2.881e-05 beats U: True
free observation: delete all 1680 query shears root 0.0099385682 dC +6.911e-03 beats U: True
delete one rank-1 per local (18) root 0.0031002428 dC +7.295e-05 beats U: True
paid 4+4->3+5 once per local root 0.0030273436 dC +5.540e-08 beats U: True
centre: 8 rank-8 per local merged to rank-144 (contested) root 0.0030682474 dC +4.096e-05 beats U: True
centre removed (contested, #4659) root 0.0076685133 dC +4.641e-03 beats U: True
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
8 0.0000000000 False
9 0.0004432875 False
10 0.0009497575 False
11 0.0014560728 False
12 0.0019622326 False
13 0.0024682360 False
14 0.0029740823 False
15 0.0034797706 True
16 0.0039853002 True
17 0.0044906702 True
18 0.0049958798 True
19 0.0055009282 True
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
forward helpers with a free split point: 0 split options 0 {}
backward helpers with a free split point: 0 split options 0 {}
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
forward scalar 17453 final rows == expected (positive control): True helpers clean strictly inside their op span (sampled): 38
backward scalar 17453 final rows == expected (positive control): True helpers clean strictly inside their op span (sampled): 38
Original file line number Diff line number Diff line change
@@ -0,0 +1,32 @@
"""Helper/main end slack: frame dims of start, first op, last op, final per register (#4610 word)."""
import sys, gzip, json
from collections import Counter, defaultdict
from pathlib import Path
w = json.loads(gzip.decompress((Path.home()/'imb-r13/research/kappa-round3-warp-20261022/ACTUAL-WORD.json.gz').read_bytes()))
c = w['canonical']; print('keys', list(c)[:30]); fr = c['frames']
print('nstart', len(c['start']), 'v', c['v'])
for side in ('forward','backward'):
prog = w['programs'][side]
print(side, Counter(e[0] for e in prog))
print(' sample', [e for e in prog if e[0]=='scalar'][:2], [e for e in prog if e[0]=='climb'][:2], [e for e in prog if e[0]=='warp'][:1])
break
def dim(f): return len(fr[f])
for side in ('forward','backward'):
prog = w['programs'][side]
ev = defaultdict(list) # reg -> list of ('op',frame) / ('climb',a,b,rank)
for e in prog:
if e[0]=='climb': ev[e[2]].append(('climb',e[3],e[4],e[5]))
elif e[0]=='scalar':
g=e[1]
regs=[r[1] for r in ([g[1],g[2]] if g[0] in ('add','copy') else [g[1]]) if r[0]=='L']
for r in regs: ev[r].append(('op',e[2]))
elif e[0]=='warp': ev[e[1][1]].append(('warp',e[2],e[3]))
pre=Counter(); post=Counter(); kinds=Counter()
for r in range(632):
L=ev[r]; ops=[i for i,x in enumerate(L) if x[0]!='climb']
if not ops: kinds['noop']+=1; continue
a=[x[3] for x in L[:ops[0]] if x[0]=='climb']; b=[x[3] for x in L[ops[-1]+1:] if x[0]=='climb']
if len(a)>0: pre[(r<224, tuple(a))]+=1
if len(b)>0: post[(r<224, tuple(b))]+=1
print(side,'climbs before first op (main?,ranks):',sorted(pre.items())[:20], 'total',sum(pre.values()))
print(side,'climbs after last op:',sorted(post.items())[:20],'total',sum(post.values()), kinds)
Original file line number Diff line number Diff line change
@@ -0,0 +1,28 @@
"""R16 lever ceilings on the selected #5413 profile (numerical screens, Decimal 50 digits)."""
import sys; sys.path.insert(0, __file__.rsplit('/',1)[0])
from price16 import *
U = D('0.00302728825')
base = root()
HCL = {1:1513,2:201,3:432,4:50,5:12} # per-local helper climbs (#4610 word, r13 sec.3)
LOC = {1:2201,2:412,3:510,4:127,5:40} # per-local non-centre paid (centre = 8 x rank 8 separate)
MCL = {k: LOC.get(k,0)-HCL.get(k,0) for k in LOC} # main x/y climbs
assert sum(k*v for k,v in MCL.items()) == 224*8
HEL = {4:28,7:7,8:47,9:326}
def x18(h, s=1): return {k: s*18*v for k,v in h.items()}
cases = {
'one helper split 9->4+5 (all 18 locals)': (add(T0,{9:-18,4:18,5:18}), P0),
'all rank-9 helpers split 4+5': (add(T0,{9:-5724,4:5724,5:5724}), P0),
'helpers credited per climb (helper defragmentation ceiling)': (add(add(T0, x18(HEL,-1)), x18(HCL)), P0),
'one 1+1->2 helper visit merge (all 18 locals)': (T0, add(P0,{1:-36,2:18})),
'main x/y single rank-8 climb (main defragmentation ceiling)': (T0, add(add(P0, x18(MCL,-1)), {8:18*224})),
'query/local fusion 1680 x (1+1->2)': (T0, add(P0,{1:-3360,2:1680})),
'free observation: delete all 1680 query shears': (T0, add(P0,{1:-1680})),
'delete one rank-1 per local (18)': (T0, add(P0,{1:-18})),
'paid 4+4->3+5 once per local': (T0, add(P0,{4:-36,3:18,5:18})),
'centre: 8 rank-8 per local merged to rank-144 (contested)': (T0, add(P0,{8:-144,144:8})),
'centre removed (contested, #4659)': (T0, add(P0,{8:-144})),
}
print('base root', base, ' U', U)
for name,(T,P) in cases.items():
r = root(T,P)
print(f'{name:62s} root {float(r):.10f} dC {float(r-base):+.3e} beats U: {r>U}')
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
"""Coupled-type size needed for a bought exit (each of the 112 supported ports needs its own H1, by
zqy_commute.py) to pay: m modes regain 16m rank-9 targets, cost 16(m + 112) H1 over 16 backward FULLs."""
import sys; sys.path.insert(0, __file__.rsplit('/',1)[0])
from price16 import *
U = D('0.00302728825')
for m in range(8, 20):
r = root(add(T0, {9: 16*m}), add(P0, {1: 16*(m+112)}))
print(m, f'{float(r):.10f}', r > U)
Original file line number Diff line number Diff line change
@@ -0,0 +1,28 @@
"""R16 float/Decimal pricer for the selected #5413 profile and structural lever screens.
M(C) = sum_T n k^(1-C) - sum_P n r^(1-C). Numerical screens only (no outward rounding)."""
from decimal import Decimal as D, getcontext
import json, sys
getcontext().prec = 50
P0 = {1:41154,2:7416,3:9180,4:2286,5:720,8:144,16:448,24:448,32:448,40:448,48:448,56:448,64:448,72:224}
T0 = {4:504,7:126,8:990,9:5724,17:448,25:448,33:448,41:448,49:448,57:448,65:448,73:224,145:224}
def pw(x, e): return (D(x).ln()*e).exp()
def M(T, P, C):
e = 1-D(C)
return sum(n*pw(k,e) for k,n in T.items() if n) - sum(n*pw(r,e) for r,n in P.items() if n)
def root(T=T0, P=P0, lo='0', hi='0.05'):
lo, hi = D(lo), D(hi)
if M(T,P,lo) <= 0: return D(0)
while M(T,P,hi) > 0: hi *= 2
for _ in range(80):
m = (lo+hi)/2
if M(T,P,m) > 0: lo = m
else: hi = m
return lo
def add(h, d):
h = dict(h)
for k, v in d.items(): h[k] = h.get(k,0)+v
return h
if __name__ == '__main__':
r = root(); print('selected root', r)
eps = D('1e-12'); print('dM/dC', (M(T0,P0,r+eps)-M(T0,P0,r-eps))/(2*eps))
print('mass surplus', sum(k*n for k,n in T0.items())-sum(k*n for k,n in P0.items()))
Loading