From 3dc2edc4044bad430581c1fafa6d472cab480b78 Mon Sep 17 00:00:00 2001 From: Joel Pulikkan Date: Sat, 24 Oct 2026 22:09:25 -0400 Subject: [PATCH] Encoded-output exit and structural levers: exact obstructions on the #5413 caller (no kappa claim) Co-Authored-By: Claude Opus 5.5 --- research/encoded-exit-obstructions/README.md | 53 ++++++ .../r16-structural-levers/README.md | 47 ++++++ .../r16-structural-levers/levers.txt | 12 ++ .../r16-structural-levers/modes_budget.txt | 12 ++ .../r16-structural-levers/split.txt | 2 + .../r16-structural-levers/split_ctl.txt | 2 + .../r16-structural-levers/tools/ends.py | 32 ++++ .../r16-structural-levers/tools/levers.py | 28 ++++ .../tools/modes_budget.py | 8 + .../r16-structural-levers/tools/price16.py | 28 ++++ .../r16-structural-levers/tools/split.py | 55 +++++++ .../r16-structural-levers/tools/split_ctl.py | 30 ++++ .../r16-structural-levers/tools/thread.py | 15 ++ .../r16-structural-levers/tools/zeroclimb.py | 18 ++ .../r16-structural-levers/tools/zqy_budget.py | 14 ++ .../tools/zqy_commute.py | 84 ++++++++++ .../r16-structural-levers/zeroclimb.txt | 2 + .../r16-structural-levers/zqy_budget.txt | 11 ++ .../r16-structural-levers/zqy_commute.txt | 12 ++ .../r17-zqy-producer-bound/README.md | 154 ++++++++++++++++++ .../r17-zqy-producer-bound/tools/exit_lb.json | 60 +++++++ .../r17-zqy-producer-bound/tools/exit_lb.py | 153 +++++++++++++++++ .../r17-zqy-producer-bound/tools/exit_lb.txt | 9 + .../r17-zqy-producer-bound/tools/lemma_sim.py | 69 ++++++++ .../tools/lemma_sim.txt | 3 + .../r17-zqy-producer-bound/tools/price17.py | 12 ++ .../r17-zqy-producer-bound/tools/price17.txt | 7 + 27 files changed, 932 insertions(+) create mode 100644 research/encoded-exit-obstructions/README.md create mode 100644 research/encoded-exit-obstructions/r16-structural-levers/README.md create mode 100644 research/encoded-exit-obstructions/r16-structural-levers/levers.txt create mode 100644 research/encoded-exit-obstructions/r16-structural-levers/modes_budget.txt create mode 100644 research/encoded-exit-obstructions/r16-structural-levers/split.txt create mode 100644 research/encoded-exit-obstructions/r16-structural-levers/split_ctl.txt create mode 100644 research/encoded-exit-obstructions/r16-structural-levers/tools/ends.py create mode 100644 research/encoded-exit-obstructions/r16-structural-levers/tools/levers.py create mode 100644 research/encoded-exit-obstructions/r16-structural-levers/tools/modes_budget.py create mode 100644 research/encoded-exit-obstructions/r16-structural-levers/tools/price16.py create mode 100644 research/encoded-exit-obstructions/r16-structural-levers/tools/split.py create mode 100644 research/encoded-exit-obstructions/r16-structural-levers/tools/split_ctl.py create mode 100644 research/encoded-exit-obstructions/r16-structural-levers/tools/thread.py create mode 100644 research/encoded-exit-obstructions/r16-structural-levers/tools/zeroclimb.py create mode 100644 research/encoded-exit-obstructions/r16-structural-levers/tools/zqy_budget.py create mode 100644 research/encoded-exit-obstructions/r16-structural-levers/tools/zqy_commute.py create mode 100644 research/encoded-exit-obstructions/r16-structural-levers/zeroclimb.txt create mode 100644 research/encoded-exit-obstructions/r16-structural-levers/zqy_budget.txt create mode 100644 research/encoded-exit-obstructions/r16-structural-levers/zqy_commute.txt create mode 100644 research/encoded-exit-obstructions/r17-zqy-producer-bound/README.md create mode 100644 research/encoded-exit-obstructions/r17-zqy-producer-bound/tools/exit_lb.json create mode 100644 research/encoded-exit-obstructions/r17-zqy-producer-bound/tools/exit_lb.py create mode 100644 research/encoded-exit-obstructions/r17-zqy-producer-bound/tools/exit_lb.txt create mode 100644 research/encoded-exit-obstructions/r17-zqy-producer-bound/tools/lemma_sim.py create mode 100644 research/encoded-exit-obstructions/r17-zqy-producer-bound/tools/lemma_sim.txt create mode 100644 research/encoded-exit-obstructions/r17-zqy-producer-bound/tools/price17.py create mode 100644 research/encoded-exit-obstructions/r17-zqy-producer-bound/tools/price17.txt diff --git a/research/encoded-exit-obstructions/README.md b/research/encoded-exit-obstructions/README.md new file mode 100644 index 0000000000..ee3374b55d --- /dev/null +++ b/research/encoded-exit-obstructions/README.md @@ -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. diff --git a/research/encoded-exit-obstructions/r16-structural-levers/README.md b/research/encoded-exit-obstructions/r16-structural-levers/README.md new file mode 100644 index 0000000000..6c8f2f85c2 --- /dev/null +++ b/research/encoded-exit-obstructions/r16-structural-levers/README.md @@ -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). diff --git a/research/encoded-exit-obstructions/r16-structural-levers/levers.txt b/research/encoded-exit-obstructions/r16-structural-levers/levers.txt new file mode 100644 index 0000000000..5db73a675f --- /dev/null +++ b/research/encoded-exit-obstructions/r16-structural-levers/levers.txt @@ -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 diff --git a/research/encoded-exit-obstructions/r16-structural-levers/modes_budget.txt b/research/encoded-exit-obstructions/r16-structural-levers/modes_budget.txt new file mode 100644 index 0000000000..46314d30ad --- /dev/null +++ b/research/encoded-exit-obstructions/r16-structural-levers/modes_budget.txt @@ -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 diff --git a/research/encoded-exit-obstructions/r16-structural-levers/split.txt b/research/encoded-exit-obstructions/r16-structural-levers/split.txt new file mode 100644 index 0000000000..16854d4147 --- /dev/null +++ b/research/encoded-exit-obstructions/r16-structural-levers/split.txt @@ -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 {} diff --git a/research/encoded-exit-obstructions/r16-structural-levers/split_ctl.txt b/research/encoded-exit-obstructions/r16-structural-levers/split_ctl.txt new file mode 100644 index 0000000000..04b577bfdb --- /dev/null +++ b/research/encoded-exit-obstructions/r16-structural-levers/split_ctl.txt @@ -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 diff --git a/research/encoded-exit-obstructions/r16-structural-levers/tools/ends.py b/research/encoded-exit-obstructions/r16-structural-levers/tools/ends.py new file mode 100644 index 0000000000..07ce7e827f --- /dev/null +++ b/research/encoded-exit-obstructions/r16-structural-levers/tools/ends.py @@ -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) diff --git a/research/encoded-exit-obstructions/r16-structural-levers/tools/levers.py b/research/encoded-exit-obstructions/r16-structural-levers/tools/levers.py new file mode 100644 index 0000000000..1b95e36de8 --- /dev/null +++ b/research/encoded-exit-obstructions/r16-structural-levers/tools/levers.py @@ -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}') diff --git a/research/encoded-exit-obstructions/r16-structural-levers/tools/modes_budget.py b/research/encoded-exit-obstructions/r16-structural-levers/tools/modes_budget.py new file mode 100644 index 0000000000..2a0f10eb15 --- /dev/null +++ b/research/encoded-exit-obstructions/r16-structural-levers/tools/modes_budget.py @@ -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) diff --git a/research/encoded-exit-obstructions/r16-structural-levers/tools/price16.py b/research/encoded-exit-obstructions/r16-structural-levers/tools/price16.py new file mode 100644 index 0000000000..0af5d25092 --- /dev/null +++ b/research/encoded-exit-obstructions/r16-structural-levers/tools/price16.py @@ -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())) diff --git a/research/encoded-exit-obstructions/r16-structural-levers/tools/split.py b/research/encoded-exit-obstructions/r16-structural-levers/tools/split.py new file mode 100644 index 0000000000..f070895338 --- /dev/null +++ b/research/encoded-exit-obstructions/r16-structural-levers/tools/split.py @@ -0,0 +1,55 @@ +"""R16 lever screen: free helper splits. A rank-k helper h can be split at an intermediate frame F +(two independent productive helpers of ranks dim F - start and final - dim F, same paid climbs) +for free only if, at some point while h sits at F with climbs still ahead, h's row is pure +(only its own input variable) AND no other register (incl. owned C0) holds h's input variable. +Exact rows replay (verify_buffers primitives; rows are frame-independent in the native semantics).""" +import sys, gzip, json +from collections import Counter, defaultdict +from fractions import Fraction as Q +from pathlib import Path +R13 = Path.home()/'imb-r13' +sys.path.insert(0, str(R13/'research/kappa-causal-continuation/buffer-borrowing')) +import verify_buffers as v +w = json.loads(gzip.decompress((R13/'research/kappa-round3-warp-20261022/ACTUAL-WORD.json.gz').read_bytes())) +c = w['canonical']; fr = c['frames'] +def dim(f): return len(fr[f]) +for side in ('forward', 'backward'): + back = side == 'backward'; prog = w['programs'][side] + rows = {('L', i): v.identity(('L', i)) for i in range(632)}; rows['C', 0] = v.identity(('C', 0)) + cur = {('L', i): f for i, f in enumerate(c['start'])} + inv = defaultdict(set) + for r, row in rows.items(): + for (var, wd) in row: inv[var].add(r) + def vars_of(row): return {var for (var, wd) in row} + # remaining climbs per register from each position + climbs_left = Counter(e[2] for e in prog if e[0] == 'climb') + def clean(h): + return vars_of(rows[h]) <= {h} and inv[h] <= {h} + found = defaultdict(set); ever_clean_mid = Counter() + for j, e in enumerate(prog): + k = e[0]; changed = [] + if k == 'scalar': + g, frame = e[1:]; t = tuple(g[1]) + old = vars_of(rows[t]) + if g[0] == 'clear': rows[t] = {} + elif g[0] == 'copy': rows[t] = dict(rows[tuple(g[2])]) + elif g[0] == 'add': v.add(rows[t], rows[tuple(g[2])], Q(g[3], g[4])) + else: q = Q(g[2], g[3]); rows[t] = {a: q*x for a, x in rows[t].items()} + new = vars_of(rows[t]) + for var in old - new: inv[var].discard(t) + for var in new - old: inv[var].add(t) + changed = [t] + [var for var in old - new] + elif k == 'warp': + _, r, op, old_f, new_f = e; t = tuple(r); rows[t] = v.warp(rows[t], op, back); cur[t] = new_f + elif k == 'climb': + i = e[2]; cur['L', i] = e[4]; climbs_left[i] -= 1 + changed = [('L', i)] + for h in changed: + if h[0] != 'L' or h[1] < 224: continue + i = h[1]; d = dim(cur[h]); d0 = dim(c['start'][i]); d1 = dim(c['final'][i]) + if d0 < d < d1 and climbs_left[i] > 0 and clean(h): + found[i].add(d) + tot = Counter(); + for i, ds in found.items(): + for d in ds: tot[(dim(c['start'][i]), d, dim(c['final'][i]))] += 1 + print(side, 'helpers with a free split point:', len(found), 'split options', sum(tot.values()), dict(sorted(tot.items()))) diff --git a/research/encoded-exit-obstructions/r16-structural-levers/tools/split_ctl.py b/research/encoded-exit-obstructions/r16-structural-levers/tools/split_ctl.py new file mode 100644 index 0000000000..d17ada749e --- /dev/null +++ b/research/encoded-exit-obstructions/r16-structural-levers/tools/split_ctl.py @@ -0,0 +1,30 @@ +exec(open(__file__.replace('split_ctl.py','split.py')).read().split("for side in ('forward', 'backward'):")[0]) +import itertools +for side in ('forward','backward'): + back = side=='backward'; prog = w['programs'][side] + rows = {('L', i): v.identity(('L', i)) for i in range(632)}; rows['C', 0] = v.identity(('C', 0)) + nsc=0; dirty_max=Counter(); cleanmid=Counter() + first = {}; last = {} + for j,e in enumerate(prog): + for r in ([tuple(x) for x in e[1][1:3] if isinstance(x,list)] if e[0]=='scalar' else []): + first.setdefault(r,j); last[r]=j + # evaluate cleanliness of every helper at every event index (slow path, sampled every 50 events) + for j,e in enumerate(prog): + if e[0]=='scalar': + g,frame=e[1:]; t=tuple(g[1]); nsc+=1 + if g[0]=='clear': rows[t]={} + elif g[0]=='copy': rows[t]=dict(rows[tuple(g[2])]) + elif g[0]=='add': v.add(rows[t], rows[tuple(g[2])], Q(g[3],g[4])) + else: q=Q(g[2],g[3]); rows[t]={a:q*x for a,x in rows[t].items()} + elif e[0]=='warp': + _,r,op,o,n=e; rows[tuple(r)]=v.warp(rows[tuple(r)],op,back) + if j%25==0: + holders=defaultdict(set) + for r,row in rows.items(): + for (var,wd) in row: holders[var].add(r) + for i in range(224,632): + h=('L',i) + if first.get(h,10**9) < j < last.get(h,-1): + if {var for (var,wd) in rows[h]}<={h} and holders[h]<={h}: cleanmid[i]+=1 + ok = all(rows['L',r]==v.expected(('L',r),[],back,False) for r in range(632)) + print(side,'scalar',nsc,'final rows == expected (positive control):',ok,'helpers clean strictly inside their op span (sampled):',len(cleanmid)) diff --git a/research/encoded-exit-obstructions/r16-structural-levers/tools/thread.py b/research/encoded-exit-obstructions/r16-structural-levers/tools/thread.py new file mode 100644 index 0000000000..a8f5643f8a --- /dev/null +++ b/research/encoded-exit-obstructions/r16-structural-levers/tools/thread.py @@ -0,0 +1,15 @@ +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']; fr = c['frames'] +side = sys.argv[1]; R = int(sys.argv[2]) +prog = w['programs'][side] +print('start', c['start'][R], 'dim', len(fr[c['start'][R]]) if isinstance(c['start'][R], int) else c['start'][R], 'final', c['final'][R]) +for i,e in enumerate(prog): + s = json.dumps(e) + if e[0]=='climb' and e[2]==R: print(i, 'CLIMB', e[3], '->', e[4], 'rank', e[5]) + elif e[0]=='scalar': + g=e[1]; regs=[r for r in g[1:3] if isinstance(r,list)] + if ['L',R] in regs: print(i, g, 'frame', e[2], 'dim', len(fr[e[2]])) + elif e[0]=='warp' and e[1]==['L',R]: print(i, e) diff --git a/research/encoded-exit-obstructions/r16-structural-levers/tools/zeroclimb.py b/research/encoded-exit-obstructions/r16-structural-levers/tools/zeroclimb.py new file mode 100644 index 0000000000..ba3b99d717 --- /dev/null +++ b/research/encoded-exit-obstructions/r16-structural-levers/tools/zeroclimb.py @@ -0,0 +1,18 @@ +"""Control screen: climbs (paid jobs) on registers whose exact row is identically zero (free zero_retag).""" +exec(open(__file__.replace('zeroclimb.py','split.py')).read().split("for side in ('forward', 'backward'):")[0]) +for side in ('forward','backward'): + back = side=='backward'; prog = w['programs'][side] + rows = {('L', i): v.identity(('L', i)) for i in range(632)}; rows['C', 0] = v.identity(('C', 0)) + z = Counter(); n = 0 + for e in prog: + if e[0]=='scalar': + g,frame=e[1:]; t=tuple(g[1]) + if g[0]=='clear': rows[t]={} + elif g[0]=='copy': rows[t]=dict(rows[tuple(g[2])]) + elif g[0]=='add': v.add(rows[t], rows[tuple(g[2])], Q(g[3],g[4])) + else: q=Q(g[2],g[3]); rows[t]={a:q*x for a,x in rows[t].items()} + elif e[0]=='warp': rows[tuple(e[1])]=v.warp(rows[tuple(e[1])],e[2],back) + elif e[0]=='climb': + n+=1 + if not rows['L',e[2]]: z[e[5]]+=1 + print(side,'climbs',n,'on identically-zero rows:',dict(z)) diff --git a/research/encoded-exit-obstructions/r16-structural-levers/tools/zqy_budget.py b/research/encoded-exit-obstructions/r16-structural-levers/tools/zqy_budget.py new file mode 100644 index 0000000000..37a4fac07f --- /dev/null +++ b/research/encoded-exit-obstructions/r16-structural-levers/tools/zqy_budget.py @@ -0,0 +1,14 @@ +"""Break-even H1 budget for buying the #5415 observation b=ZQY per backward FULL (16 applicable). +Supplied exit (#5415): +8 rank-9 targets and +8 H1 per FULL; purchase adds X more H1 per FULL.""" +import sys; sys.path.insert(0, __file__.rsplit('/',1)[0]) +from price16 import * +base = root(); U = D('0.00302728825') +for X in [0, 8, 16, 32, 48, 56, 60, 64, 72, 112]: + T = add(T0, {9: 16*8}); P = add(P0, {1: 16*(8+X)}) + r = root(T, P); print(f'X={X:4d} H1/FULL root {float(r):.10f} dC {float(r-base):+.3e} beats U {r>U}') +lo, hi = 0, 200 +while hi-lo > 1: + m = (lo+hi)//2 + if root(add(T0,{9:128}), add(P0,{1:16*(8+m)})) > U: lo = m + else: hi = m +print('largest integer X with root > U:', lo, 'H1 per backward FULL (vs 120 to buy full QY)') diff --git a/research/encoded-exit-obstructions/r16-structural-levers/tools/zqy_commute.py b/research/encoded-exit-obstructions/r16-structural-levers/tools/zqy_commute.py new file mode 100644 index 0000000000..c4e169b0da --- /dev/null +++ b/research/encoded-exit-obstructions/r16-structural-levers/tools/zqy_commute.py @@ -0,0 +1,84 @@ +"""R16 lever F screen: can b = Z Q Y (#5415) be bought with few paid rank-one jobs? +b_k = sum_j M_kj/2 Km_k^-1 Kp_j Q Y_j. If Km_k^-1 Kp_j conjugates Q to one common operator per mode +(or per class), b costs one H1 per (mode, class) instead of 112 H1 (Q on every Y_j). +Uses the repository's exact Clifford evaluator (tableau + absolute zero-state phase).""" +import json, sys, importlib.util +from pathlib import Path +from collections import Counter, defaultdict +ROOT = Path.home()/'imb-r16' +cp = ROOT/'research/coded-native-caller/clifford_exact.py' +spec = importlib.util.spec_from_file_location('ce', cp); ce = importlib.util.module_from_spec(spec); sys.modules['ce'] = ce; spec.loader.exec_module(ce) +normal = json.loads((ROOT/'research/coded-native-caller/NORMALIZERS.json').read_text()) +prov = json.loads((ROOT/'research/native-rank8-helper-provider/PROVIDER.json').read_text()) +M = normal['mode_columns'] +def literal(word): + op = ce.ident(9) + for e in word: + if e[0] == 'P': part = ce.perm(9, tuple(e[1])) + elif e[0] == 'D': part = ce.diag(9, tuple(e[1]), tuple(e[2])) + elif e[0] == 'X': part = ce.xgate(9, e[1]) + elif e[0] == 'phase': part = ce.Op(9, ce.identity(9), [('phase', e[1])]) + else: raise ValueError(e) + op = op.then(part) + return op +def equal(a, b): return a.tab == b.tab and a.zero_state() == b.zero_state() +def key(op): return (op.tab, tuple(map(tuple, op.zero_state()[0])) if False else repr(op.zero_state())) +canonical = json.loads(__import__('gzip').decompress((ROOT/'research/native-center-free-code/SOURCE-WORD.json.gz').read_bytes()))['canonical'] +R = ce.canonical_frame(9, canonical['frames'][1]) +Dop = ce.fourier(9, range(1, 9)) +Q1 = Dop.adjoint().then(R); Q2 = R.then(Dop.adjoint()) +print('Q well defined (D,Q commute in R):', equal(Q1, Q2), ' Q rank', ce.rank([x for x, _, _ in Q1.tab[9:]])) +Q = Q1 +Kp = [literal(r['K_word']) for r in normal['ports']] +Km = [None]*8 +for rec in prov['mode_boundaries']: + Km[rec['mode']] = literal(rec['input_K']['literal_word']) +print('Kp commute with Q:', sum(equal(k.then(Q), Q.then(k)) for k in Kp), '/112; with D:', sum(equal(k.then(Dop), Dop.then(k)) for k in Kp)) +print('Km commute with Q:', sum(equal(k.then(Q), Q.then(k)) for k in Km), '/8; with D:', sum(equal(k.then(Dop), Dop.then(k)) for k in Km)) +# conjugate classes per mode: C = Kp_j then Km_k^-1 (operator applied to Y_j); need C Q C^-1 +total = 0; per = [] +tabcls = Counter() +for k in range(8): + cls = defaultdict(list) + for j in range(112): + if not M[k][j]: continue + C = Kp[j].then(Km[k].adjoint()) + conj = C.adjoint().then(Q).then(C) # operator equal to C Q C^-1 in 'then' order + cls[(conj.tab, repr(conj.zero_state()))].append(j) + tabcls[conj.tab] += 1 + per.append(len(cls)); total += len(cls) +print('distinct conjugates of Q per mode:', per, 'total', total, '(break-even ~55 + 8 restore)') +print('distinct conjugate tableaux overall:', len(tabcls)) +# port-level: distinct Kp Q Kp^-1 (sharing Q Y_j across modes) +pc = Counter((lambda c: (c.tab, repr(c.zero_state())))(k.adjoint().then(Q).then(k)) for k in Kp) +print('distinct port conjugates Kp^-1 Q Kp:', len(pc)) +# coarser: Q_a, Q_b groupable (common left monomial E, right monomials free) iff Q_b^-1 Q_a is monomial +def rk(op): return ce.rank([x for x, _, _ in op.tab[9:]]) +tot2 = 0; per2 = [] +for k in range(8): + reps = [] + for j in range(112): + if not M[k][j]: continue + C = Kp[j].then(Km[k].adjoint()); conj = C.adjoint().then(Q).then(C) + for r in reps: + if rk(conj.then(r.adjoint())) == 0: break + else: reps.append(conj) + per2.append(len(reps)); tot2 += len(reps) +print('monomial-coset classes per mode:', per2, 'total', tot2) +reps = [] +for j in range(112): + conj = Kp[j].adjoint().then(Q).then(Kp[j]) + for r in reps: + if rk(conj.then(r.adjoint())) == 0: break + else: reps.append(conj) +print('port-level monomial-coset classes (shared over modes):', len(reps)) +# other composition order (left/right coset) and controls +for name, f in (('left', lambda a, r: r.adjoint().then(a)), ('right', lambda a, r: a.then(r.adjoint()))): + reps = [] + for j in range(112): + conj = Kp[j].adjoint().then(Q).then(Kp[j]) + if not any(rk(f(conj, r)) == 0 for r in reps): reps.append(conj) + print(name, 'coset classes over ports:', len(reps)) +print('control rank(Q Q^-1)=', rk(Q.then(Q.adjoint())), ' rank(Q)=', rk(Q), ' rank(R)=', rk(R), ' rank(D)=', rk(Dop)) +cj = [Kp[j].adjoint().then(Q).then(Kp[j]) for j in range(112)] +print('rank histogram of pairwise Q_a Q_b^-1 (first 20 ports):', Counter(rk(cj[a].then(cj[b].adjoint())) for a in range(20) for b in range(20) if a != b)) diff --git a/research/encoded-exit-obstructions/r16-structural-levers/zeroclimb.txt b/research/encoded-exit-obstructions/r16-structural-levers/zeroclimb.txt new file mode 100644 index 0000000000..03d203f026 --- /dev/null +++ b/research/encoded-exit-obstructions/r16-structural-levers/zeroclimb.txt @@ -0,0 +1,2 @@ +forward climbs 3290 on identically-zero rows: {} +backward climbs 3290 on identically-zero rows: {} diff --git a/research/encoded-exit-obstructions/r16-structural-levers/zqy_budget.txt b/research/encoded-exit-obstructions/r16-structural-levers/zqy_budget.txt new file mode 100644 index 0000000000..479d8d527c --- /dev/null +++ b/research/encoded-exit-obstructions/r16-structural-levers/zqy_budget.txt @@ -0,0 +1,11 @@ +X= 0 H1/FULL root 0.0071409936 dC +4.114e-03 beats U True +X= 8 H1/FULL root 0.0066188509 dC +3.592e-03 beats U True +X= 16 H1/FULL root 0.0060978902 dC +3.071e-03 beats U True +X= 32 H1/FULL root 0.0050594936 dC +2.032e-03 beats U True +X= 48 H1/FULL root 0.0040257617 dC +9.985e-04 beats U True +X= 56 H1/FULL root 0.0035106322 dC +4.833e-04 beats U True +X= 60 H1/FULL root 0.0032534992 dC +2.262e-04 beats U True +X= 64 H1/FULL root 0.0029966534 dC -3.063e-05 beats U False +X= 72 H1/FULL root 0.0024838202 dC -5.435e-04 beats U False +X= 112 H1/FULL root 0.0000000000 dC -3.027e-03 beats U False +largest integer X with root > U: 63 H1 per backward FULL (vs 120 to buy full QY) diff --git a/research/encoded-exit-obstructions/r16-structural-levers/zqy_commute.txt b/research/encoded-exit-obstructions/r16-structural-levers/zqy_commute.txt new file mode 100644 index 0000000000..f8505ccbab --- /dev/null +++ b/research/encoded-exit-obstructions/r16-structural-levers/zqy_commute.txt @@ -0,0 +1,12 @@ +Q well defined (D,Q commute in R): True Q rank 1 +Kp commute with Q: 0 /112; with D: 0 +Km commute with Q: 0 /8; with D: 0 +distinct conjugates of Q per mode: [56, 56, 56, 56, 56, 56, 56, 56] total 448 (break-even ~55 + 8 restore) +distinct conjugate tableaux overall: 124 +distinct port conjugates Kp^-1 Q Kp: 112 +monomial-coset classes per mode: [56, 56, 56, 56, 56, 56, 56, 56] total 448 +port-level monomial-coset classes (shared over modes): 112 +left coset classes over ports: 112 +right coset classes over ports: 112 +control rank(Q Q^-1)= 0 rank(Q)= 1 rank(R)= 9 rank(D)= 8 +rank histogram of pairwise Q_a Q_b^-1 (first 20 ports): Counter({2: 380}) diff --git a/research/encoded-exit-obstructions/r17-zqy-producer-bound/README.md b/research/encoded-exit-obstructions/r17-zqy-producer-bound/README.md new file mode 100644 index 0000000000..8ff691c3df --- /dev/null +++ b/research/encoded-exit-obstructions/r17-zqy-producer-bound/README.md @@ -0,0 +1,154 @@ +# R17: no structured producer of b = Z Q Y beats break-even (negative result, no κ claim) + +Question (from #5428 target 1 and #5415's encoded-output exit): can the backward FULL buy the observation +b = Z Q Y for at most break-even cost, using a producer that is **not** a termwise sum of conjugated queries? +The task listed several candidate shapes: shared higher-rank intermediate jobs, Hadamard/Fourier butterflies +over the 112 ports, block transforms, and reuse of data the controller already holds. + +**Answer: no, for every producer that reads post-return data.** Any such producer needs at least **112 paid +jobs** per backward FULL, of any rank and any operator type. Under concave pricing this costs at least 112 +H1-equivalents. Break-even is 63.52. The whole #5415 exit (b together with the 8 restoring calls) needs at +least **120** paid jobs, so #5415's constructive 120-H1 exit is optimal both in job count and in concave cost. +If the producer also reads a pre-return copy of y or h, the only producer known is D·Z·y at 8 H8, which buys +back the deleted centres. It costs 63.598 H1-equivalents per FULL and fails: its root is 0.0030223874, below +U. A lower bound for that wider class is open (see §5). + +## 1. Cost model (as the repository prices it) +- Pricing (R16 `price16.py`, #5428 PROFILE): M(C) = Σ_T n k^(1−C) − Σ_P n r^(1−C). b-free base: + T0+{9:128}, P0+{1:128} (8 exit H1 and 8 restored H9 targets per backward FULL, 16 FULLs). + A purchase adds its paid jobs ×16. Root > U = 0.00302728825 iff the purchase costs + Σ r^(1−U) < **τ = 63.5226717504634927** per FULL (`tools/price17.py`). So 63 H1 passes and 64 H1 fails. +- Fields and operations (#5415 PROOF §1, coded-native-caller/PHYSICAL.md "Universal scope"): + - Every field is a 9-axis address space at fiber width f. + - Physical maps are width-1 operators lifted as f-fold tensor powers. This includes absolute phase: i^γ lifts + to i^(fγ). + - Owner/scalar coefficients are applied once and do not depend on f. + - Identities must hold at every f ≥ 1. + - Ordinary (non-recursive) work: monomial field maps (P/D/X/phase, i.e. rank-0 Cliffords) plus scalar + ADD, SCALE, COPY, CLEAR and zero_retag. + - Paid work: recursive Gaussian children of rank r ≥ 1, each acting on one field. + - A producer is a finite straight-line program over these operations, independent of f. + +## 2. Two lemmas +**Lemma 1 (tensor-power independence).** Let x_1..x_m be distinct matrices and α_t scalars that do not depend +on f. If Σ α_t x_t^{⊗f} = 0 for every f ≥ 1, then every α_t = 0. + +Proof: pick vectors a, b with distinct nonzero values λ_t = ⟨a, x_t b⟩. Pairing with a^{⊗f}, b^{⊗f} gives +Σ α_t λ_t^f = 0 for all f ≥ 1, and the Vandermonde matrix is invertible. + +Consequence: give each field a *formal value* in C[G]^{vars}, a finite sum of (width-1 operator, +input-variable) terms. Free and paid operations act on formal values by left multiplication and linear +combination. Evaluation at width f is exact. A producer is correct at all widths iff its output's formal value +**equals** the target's formal value. + +**Lemma 2 (one vector per paid job).** +- Setup: group each formal value by right monomial cosets x·Mon. Here Mon is the group of invertible monomial + operators. The coset x·Mon is determined by the Lagrangian x(L_Z). The value at a coset c is the sum of the + coefficient vectors of the terms in c, and lies in C^{vars}. +- Free operations: + - A monomial m maps the value at c to m·c. + - It fixes the base class Mon and permutes the non-base classes. + - ADD, SCALE, COPY and CLEAR are linear. +- Potential: let S be the span of all values at non-base classes, taken over every field ever computed. + Free operations never enlarge S. +- Paid jobs: a job g acting on a field v (g any invertible operator, of any rank, Clifford or not) produces + values {v(g⁻¹c)}. Its non-base values are old non-base values plus at most the single vector v(Mon). So + dim S grows by at most 1. +- Conclusion: **#paid jobs ≥ dim(S_0 + S_target) − dim S_0**. Here S_0 is the span of the input data's non-base + values, and S_target is the span of the target's non-base values. +- Control (`tools/lemma_sim.py`): 300 random 3-qubit programs with random monomials, ADDs and random-rank + Clifford jobs give max(dim S − #jobs) = 0. One job per variable attains the bound. +- Mutation: treating one C gate as free gives dim S = 4 with 0 paid jobs. The lemma really depends on + Gaussians being paid. + +## 3. Theorem (post-return producers) +The FULL return holds X = Dx − Ry + RWh, Y = Dy, H = D(h − Zy), 400 autonomous helpers and owned zero fields. + +Change variables to ξ = X, η = Y, ζ = H. This change is invertible: x occurs only in X, h only in H and X, +and right multiplication by D is injective on C[G]. In these coordinates every available field is a base +variable, so S_0 = 0. Any other data that are formally independent of this FULL's inputs are also base +variables. + +Target: b_k = Σ_j (M_kj/2) Km_k⁻¹ Kp_j Q η_j. For a fixed mode k, the 56 classes Km_k⁻¹ Kp_j Q·Mon are pairwise +distinct and non-base: +- every term has rank 1; +- every quotient inside a mode has rank 2; +- this holds for all four Kp^±/Km^± conventions. + +So the value of b_k at class (k, j) is (M_kj/2) e_j, and S_target = span{e_j} = 112 dimensions (`tools/exit_lb.py`, +exact rational rank, repository `clifford_exact` with absolute phase): + +| target | dim S_target = paid-job lower bound | non-base classes | +|---|---:|---:| +| b = Z Q Y (each of 4 K conventions) | **112** | 448 (56 per mode) | +| whole #5415 exit (H_o = QH + b, X_o = X − W H_o, Y_o = Y) | **120** | 12,552 | +| control: port maps set to identity | 8 | — | +| control: same b in y-coordinates (pre-return y as base) | 8 | — | +| control: monomial target Z Y | 0 | — | + +Each paid job costs r^(1−U) ≥ 1. So any post-return producer costs ≥ 112 > τ = 63.52, and its root is 0 +(`price17.txt`). □ + +What the theorem covers: every mechanism in the task, at once. +- Shared higher-rank intermediates: one rank-r job still serves only one new port direction, whatever its + concave discount. +- Butterflies or Hadamard combinations over ports: the garbage cancellation they need is counted. +- Block transforms that put ports in a common coset: impossible, because the 56 classes per mode are pairwise + distinct. +- Joint diagonalisation by a common transform, followed by any post-processing. +- Producers in which several modes share jobs. +- Non-Clifford jobs. + +The R16 coset screen only covered termwise sums of conjugated queries. This bound covers all producers. + +## 4. Scope of #5427 (verified) +#5427 works in the formal free-word grammar of frozen words. Its result: b is not a *free* combination of +retained versions, and no paid response can be reused. It explicitly does not bound a new paid producer. +§3 supplies that bound for post-return data. + +#5427's caller-level test admits the whole caller history, which includes this FULL's input bank y. In that +wider data model a paid producer exists (§5). So "b absent from history" does not by itself imply that b is +expensive. + +## 5. Not covered: pre-return copies of y or h (open, but economically it is the centre lever) +If the caller keeps a copy of the FULL input y (or h), then b = Z R y = Q·(D Z y). Also Q H + b = Q(H + DZy) = Q D h. +So one producer is **8 H8** on D Z y (or on D h), with the exit's 8 Q calls merged. This is the deleted centre +transport bought back: +- cost 8·8^(1−U) = 63.598 > τ = 63.523; +- root 0.0030223873635, below U; +- 8 H9 on R Z y costs 71.52 and fails as well. + +In this data model the Lemma-2 bound becomes vacuous: y and Y = Dy are two views of one variable, so S_0 is +full. A sharp lower bound would need element-level reasoning, not class-level reasoning; this remains open. Any +gain would have to beat 8 rank-8 transforms of 8 generic independent fields by more than 0.076 H1-equivalent +per FULL. That is the centre-interface lever (#4694/#4698/#4700; merging the 8 H8 into one job is the +contested centre merge). It was out of scope for R16/R17. + +Other assumptions behind the theorem, each needed for a counterexample: +1. Exact producer. Approximate producers are not covered. +2. Every paid job acts on one standard-size field. Packing 512 fields into one field of width f+1 is a + different recursion size. +3. The purchase jobs carry no productive target credit. Crediting them would need a new target contract. +4. Free operations are monomial. If any non-monomial operation were free, the lemma would fail (see the + mutation control). + +## Reproduce +```sh +cd ~/imb-harness/r17/tools +OPENBLAS_NUM_THREADS=1 /opt/homebrew/bin/python3.12 -B exit_lb.py # ~20 s, reads ~/imb-r17 (upstream/main 32890bc5d) +OPENBLAS_NUM_THREADS=1 /opt/homebrew/bin/python3.12 -B lemma_sim.py # lemma control + mutation +/opt/homebrew/bin/python3.12 -B price17.py # break-even and route prices +``` +Outputs: `exit_lb.txt`, `exit_lb.json`, `lemma_sim.txt`, `price17.txt`. + +Credits: +- zxv: #5415 exit contract and the 120-H1 upper bound shown optimal here; #5428 targets; #4359 paradigm. +- Dillon Amburgey: #5402 provider and physical mode maps. +- Clear1nsight: #5413 selected caller. +- Ali Romman / aliromman: #5383/#5398 relations and caller. +- Matarener: #5427 retained-span result, whose scope is extended here. +- Dugongue, #4929/#4933 lineage: normalizers and code. +- Cao Yifan: #4610 native word. +- Cinna Davis: helper/controller lineage. + +Prepared with Claude Opus 5.5 (Anthropic) via Claude Code, directed by Joel Pulikkan (GamingPuzzled). diff --git a/research/encoded-exit-obstructions/r17-zqy-producer-bound/tools/exit_lb.json b/research/encoded-exit-obstructions/r17-zqy-producer-bound/tools/exit_lb.json new file mode 100644 index 0000000000..688c60de5c --- /dev/null +++ b/research/encoded-exit-obstructions/r17-zqy-producer-bound/tools/exit_lb.json @@ -0,0 +1,60 @@ +{ + "b=ZQY Kp^1 Km^-1": { + "dim_S_target": 112, + "nonbase_classes": 448, + "classes_per_mode": [ + 56, + 56, + 56, + 56, + 56, + 56, + 56, + 56 + ] + }, + "b=ZQY Kp^1 Km^1": { + "dim_S_target": 112, + "nonbase_classes": 448, + "classes_per_mode": [ + 56, + 56, + 56, + 56, + 56, + 56, + 56, + 56 + ] + }, + "b=ZQY Kp^-1 Km^-1": { + "dim_S_target": 112, + "nonbase_classes": 448, + "classes_per_mode": [ + 56, + 56, + 56, + 56, + 56, + 56, + 56, + 56 + ] + }, + "b=ZQY Kp^-1 Km^1": { + "dim_S_target": 112, + "nonbase_classes": 448, + "classes_per_mode": [ + 56, + 56, + 56, + 56, + 56, + 56, + 56, + 56 + ] + }, + "exit H_o only": 120, + "exit all outputs": 120 +} \ No newline at end of file diff --git a/research/encoded-exit-obstructions/r17-zqy-producer-bound/tools/exit_lb.py b/research/encoded-exit-obstructions/r17-zqy-producer-bound/tools/exit_lb.py new file mode 100644 index 0000000000..1dd0a9bbae --- /dev/null +++ b/research/encoded-exit-obstructions/r17-zqy-producer-bound/tools/exit_lb.py @@ -0,0 +1,153 @@ +"""R17: lower bound on the number of paid jobs in ANY producer of b = Z Q Y (and of the whole #5415 exit) +from post-return data. Uses the repository's exact Clifford evaluator (tableau + absolute phase). + +Potential (see ../notes/README.md, Lemma 2): track every field as a formal sum over (operator, input +variable); quotient each operator x by right monomial cosets x*Mon (key = x applied to the Z-Lagrangian). +Free operations (monomials, scalar ADD/SCALE/COPY/CLEAR) fix the base class Mon and permute the others; +a paid job (ANY invertible operator, any rank) adds at most one new vector to + S = span{ value at a non-base class : over all fields ever computed }. +So #paid jobs >= dim(S_target) - dim(S_target ∩ S_0); S_0 = 0 when every available field is a base +variable (true for X, Y, H, helpers, owned zeros at the FULL return in coordinates xi=X, eta=Y, zeta=H). +""" +import gzip, json, sys, importlib.util +from fractions import Fraction as F +from pathlib import Path +from collections import defaultdict + +ROOT = Path.home() / 'imb-r17' +cp = ROOT / 'research/coded-native-caller/clifford_exact.py' +spec = importlib.util.spec_from_file_location('ce', cp); ce = importlib.util.module_from_spec(spec) +sys.modules['ce'] = ce; spec.loader.exec_module(ce) +normal = json.loads((ROOT / 'research/coded-native-caller/NORMALIZERS.json').read_text()) +prov = json.loads((ROOT / 'research/native-rank8-helper-provider/PROVIDER.json').read_text()) +M = normal['mode_columns'] # 8 x 112, entries in {-1,0,1} +n = 9 + +def literal(word): + op = ce.ident(n) + for e in word: + if e[0] == 'P': part = ce.perm(n, tuple(e[1])) + elif e[0] == 'D': part = ce.diag(n, tuple(e[1]), tuple(e[2])) + elif e[0] == 'X': part = ce.xgate(n, e[1]) + elif e[0] == 'phase': part = ce.Op(n, ce.identity(n), [('phase', e[1])]) + else: raise ValueError(e) + op = op.then(part) + return op + +def after(*ops): + """Operator product in the rightmost-first convention: after(A, B, C) = A B C (C applied first).""" + out = ce.ident(n) + for o in reversed(ops): out = out.then(o) + return out + +def rank(op): return ce.rank([x for x, _, _ in op.tab[n:]]) + +def echelon(vecs): + piv = {} + for v in vecs: + while v: + b = v.bit_length() - 1 + if b not in piv: piv[b] = v; break + v ^= piv[b] + # fully reduce for a canonical basis + keys = sorted(piv, reverse=True) + for i, b in enumerate(keys): + for c in keys[:i]: + if piv[c] >> b & 1: piv[c] ^= piv[b] + return tuple(sorted(piv.values())) + +def cls(op): + """Right monomial coset x*Mon <-> the Lagrangian x(L_Z) (signs/phases forgotten).""" + return echelon([x | (z << n) for x, z, _ in op.tab[n:]]) + +BASE = cls(ce.ident(n)) + +def qrank(rows): + """Exact rank over Q of a list of dict-vectors.""" + rows = [dict(r) for r in rows if any(r.values())] + r = 0; cols = sorted({c for row in rows for c in row}) + for c in cols: + p = next((i for i in range(r, len(rows)) if rows[i].get(c, 0)), None) + if p is None: continue + rows[r], rows[p] = rows[p], rows[r] + pv = rows[r][c] + for i in range(len(rows)): + if i != r and rows[i].get(c, 0): + f = rows[i][c] / pv + for k, v in rows[r].items(): rows[i][k] = rows[i].get(k, 0) - f * v + r += 1 + return r + +def s_target(outputs): + """outputs: list of formal sums [(operator, variable, coefficient)]. Returns (dim S_target, #classes).""" + vals = [] + ncls = 0 + for terms in outputs: + per = defaultdict(lambda: defaultdict(F)) + for op, var, c in terms: + k = cls(op) + if k != BASE: per[k][var] += c + ncls += len(per) + vals += [dict(v) for v in per.values()] + return qrank(vals), ncls + +def main(): + global R, Dop, Q, Kp, Km + canonical = json.loads(gzip.decompress((ROOT / 'research/native-center-free-code/SOURCE-WORD.json.gz').read_bytes()))['canonical'] + R = ce.canonical_frame(n, canonical['frames'][1]) + Dop = ce.fourier(n, range(1, 9)) + Q = Dop.adjoint().then(R) + assert ce.rank([x for x, _, _ in R.tab[n:]]) == 9 and rank(Dop) == 8 and rank(Q) == 1 + RR = Dop.then(Q); assert RR.tab == R.tab and RR.zero_state() == R.zero_state() # R = Q D exactly (absolute phase) + Kp = [literal(r['K_word']) for r in normal['ports']] + Km = [None] * 8 + for rec in prov['mode_boundaries']: Km[rec['mode']] = literal(rec['input_K']['literal_word']) + inv = lambda o: o.adjoint() + assert all(rank(k) == 0 for k in Kp + Km), 'port/mode maps are monomial' + assert all(any(M[k][j] for k in range(8)) for j in range(112)), 'every port is supported' + + report = {} + # 1. b = Z Q Y, all four K conventions (b_k = sum_j M_kj/2 Km_k^{+-1} Kp_j^{+-1} Q eta_j). + for sp in (1, -1): + for sm in (1, -1): + kp = Kp if sp == 1 else [inv(k) for k in Kp] + km = [inv(k) for k in Km] if sm == 1 else Km + outs = [[(after(km[k], kp[j], Q), ('eta', j), F(M[k][j], 2)) for j in range(112) if M[k][j]] for k in range(8)] + dim, ncls = s_target(outs) + per_mode = [len({cls(after(km[k], kp[j], Q)) for j in range(112) if M[k][j]}) for k in range(8)] + report[f'b=ZQY Kp^{sp} Km^{-sm}'] = dict(dim_S_target=dim, nonbase_classes=ncls, classes_per_mode=per_mode) + print(f'b = Z Q Y (Kp^{sp:+d}, Km^{-sm:+d}): dim S_target = {dim} classes {ncls} per mode {per_mode}') + + # 2. whole #5415 exit from (xi=X, eta=Y, zeta=H): H_o = Q zeta + Z Q eta ; X_o = xi - W H_o ; Y_o = eta + # W = Kp^-1 M Km / 2 , Z = Km^-1 M^T Kp / 2. + Ho = [[(Q, ('zeta', k), F(1))] + [(after(inv(Km[k]), Kp[j], Q), ('eta', j), F(M[k][j], 2)) for j in range(112) if M[k][j]] for k in range(8)] + Xo = [] + for i in range(112): + t = [(ce.ident(n), ('xi', i), F(1))] + for k in range(8): + if not M[k][i]: continue + for op, var, c in Ho[k]: + t.append((after(inv(Kp[i]), Km[k], op), var, -F(M[k][i], 2) * c)) + Xo.append(t) + dimH, _ = s_target(Ho); dimAll, ncls = s_target(Ho + Xo) + report['exit H_o only'] = dimH; report['exit all outputs'] = dimAll + print('whole exit: dim S_target from H_o =', dimH, '; from (X_o, Y_o, H_o) =', dimAll, '(nonbase classes', ncls, ')') + + # 3. controls + # (a) if the port maps were trivial, the 56 terms of a mode share one class: bound collapses to 8 + outs = [[(after(inv(Km[k]), Q), ('eta', j), F(M[k][j], 2)) for j in range(112) if M[k][j]] for k in range(8)] + print('control trivial ports: dim S_target =', s_target(outs)[0], '(expect 8)') + # (b) same target in y-coordinates (pre-return y retained as a base variable): b = Km^-1 R Kp y -> 8 + outs = [[(after(inv(Km[k]), Kp[j], R), ('y', j), F(M[k][j], 2)) for j in range(112) if M[k][j]] for k in range(8)] + print('control y-coordinates (8 R jobs on Zy suffice): dim S_target =', s_target(outs)[0], '(expect 8)') + # (c) a monomial target has no non-base class: bound 0 + outs = [[(after(inv(Km[k]), Kp[j]), ('eta', j), F(M[k][j], 2)) for j in range(112) if M[k][j]] for k in range(8)] + print('control monomial target Z Y: dim S_target =', s_target(outs)[0], '(expect 0)') + # (d) rank of every target term and of pairwise quotients inside a mode + rk = {rank(after(inv(Km[k]), Kp[j], Q)) for k in range(8) for j in range(112) if M[k][j]} + q2 = {rank(after(inv(after(inv(Km[0]), Kp[a], Q)), inv(Km[0]), Kp[b], Q)) for a in range(112) for b in range(112) if a != b and M[0][a] and M[0][b]} + print('target term ranks', rk, '; quotient ranks inside mode 0', q2) + json.dump(report, open(Path(__file__).with_suffix('.json'), 'w'), indent=1) + +if __name__ == '__main__': + main() diff --git a/research/encoded-exit-obstructions/r17-zqy-producer-bound/tools/exit_lb.txt b/research/encoded-exit-obstructions/r17-zqy-producer-bound/tools/exit_lb.txt new file mode 100644 index 0000000000..95c05e6db3 --- /dev/null +++ b/research/encoded-exit-obstructions/r17-zqy-producer-bound/tools/exit_lb.txt @@ -0,0 +1,9 @@ +b = Z Q Y (Kp^+1, Km^-1): dim S_target = 112 classes 448 per mode [56, 56, 56, 56, 56, 56, 56, 56] +b = Z Q Y (Kp^+1, Km^+1): dim S_target = 112 classes 448 per mode [56, 56, 56, 56, 56, 56, 56, 56] +b = Z Q Y (Kp^-1, Km^-1): dim S_target = 112 classes 448 per mode [56, 56, 56, 56, 56, 56, 56, 56] +b = Z Q Y (Kp^-1, Km^+1): dim S_target = 112 classes 448 per mode [56, 56, 56, 56, 56, 56, 56, 56] +whole exit: dim S_target from H_o = 120 ; from (X_o, Y_o, H_o) = 120 (nonbase classes 12552 ) +control trivial ports: dim S_target = 8 (expect 8) +control y-coordinates (8 R jobs on Zy suffice): dim S_target = 8 (expect 8) +control monomial target Z Y: dim S_target = 0 (expect 0) +target term ranks {1} ; quotient ranks inside mode 0 {2} diff --git a/research/encoded-exit-obstructions/r17-zqy-producer-bound/tools/lemma_sim.py b/research/encoded-exit-obstructions/r17-zqy-producer-bound/tools/lemma_sim.py new file mode 100644 index 0000000000..5f54bca08c --- /dev/null +++ b/research/encoded-exit-obstructions/r17-zqy-producer-bound/tools/lemma_sim.py @@ -0,0 +1,69 @@ +"""Randomized control for the potential lemma on 3 qubits: random straight-line programs with free monomial +ops, scalar ADDs and paid jobs (random Cliffords, any rank). Checks dim S (span of values at non-base right-Mon +classes over all fields) never exceeds #jobs, and that the bound is attained by a constructive program.""" +import random, sys, importlib.util +from fractions import Fraction as F +from pathlib import Path +sys.path.insert(0, str(Path(__file__).parent)) +import exit_lb as E # reuses evaluator, cls(), qrank() +ce = E.ce; n = 3 +def rmono(): + while True: + G = tuple(random.randrange(1, 8) for _ in range(n)) + if ce.rank(list(G)) == n: break + Qd = [[0]*n for _ in range(n)] + for i in range(n): + for j in range(i, n): + b = random.randrange(2); Qd[i][j] = Qd[j][i] = b + Qr = tuple(sum(Qd[i][j] << j for j in range(n)) for i in range(n)) + alpha = tuple((Qd[i][i] + 2*random.randrange(2)) % 4 for i in range(n)) + return ce.perm(n, G).then(ce.diag(n, Qr, alpha)).then(ce.xgate(n, random.randrange(8))).then(ce.Op(n, ce.identity(n), [('phase', random.randrange(4))])) +def rjob(): + op = rmono() + for _ in range(random.randrange(1, 4)): op = op.then(ce.cgate(n, 1 << random.randrange(n), random.choice((1, -1)))).then(rmono()) + return op +key = lambda o: (o.tab, repr(o.zero_state())) +def act(g, val): # left multiplication of a formal value {key: (op, {var: coeff})} + out = {} + for op, vec in val.values(): + x = op.then(g); out[key(x)] = (x, dict(vec)) + return out +def add(a, b, c): + out = {k: (o, dict(v)) for k, (o, v) in a.items()} + for k, (o, v) in b.items(): + if k not in out: out[k] = (o, {}) + for var, x in v.items(): out[k][1][var] = out[k][1].get(var, 0) + c * x + return out +def S_dim(fields): + vals = [] + for f in fields: + per = {} + for op, vec in f.values(): + k = E.cls(op) + if k == E_BASE: continue + d = per.setdefault(k, {}) + for var, x in vec.items(): d[var] = d.get(var, 0) + x + vals += list(per.values()) + return E.qrank(vals) +E.n = n; E_BASE = E.cls(ce.ident(n)) +random.seed(17); worst = 0 +for trial in range(300): + V = random.randrange(2, 7) + I = ce.ident(n); fields = [{key(I): (I, {v: F(1)})} for v in range(V)] + jobs = 0 + for step in range(random.randrange(3, 14)): + r = random.random() + a = random.randrange(len(fields)) + if r < 0.35: fields.append(act(rmono(), fields[a])) + elif r < 0.7: fields.append(add(fields[a], act(rmono(), fields[random.randrange(len(fields))]), F(random.choice((1, -1, 2)), random.choice((1, 2))))) + else: fields.append(act(rjob(), fields[a])); jobs += 1 + s = S_dim(fields); assert s <= jobs, (trial, s, jobs); worst = max(worst, s - jobs) +print('300 random programs: max(dim S - #jobs) =', worst, '(lemma requires <= 0)') +# attainment: one job per variable on separate fields reaches dim S = V +I = ce.ident(n); fields = [{key(I): (I, {v: F(1)})} for v in range(4)] +fields += [act(rjob(), f) for f in list(fields)] +print('one job per variable: dim S =', S_dim(fields), 'with 4 jobs') +# negative control: if a rank-1 C gate were free, the potential can exceed the number of paid jobs +I = ce.ident(n); fields = [{key(I): (I, {v: F(1)})} for v in range(4)] +fields += [act(ce.cgate(n, 1), f) for f in list(fields)] +print('mutation (C gate treated as free): dim S =', S_dim(fields), 'with 0 paid jobs (lemma would be violated)') diff --git a/research/encoded-exit-obstructions/r17-zqy-producer-bound/tools/lemma_sim.txt b/research/encoded-exit-obstructions/r17-zqy-producer-bound/tools/lemma_sim.txt new file mode 100644 index 0000000000..a18f0b90ac --- /dev/null +++ b/research/encoded-exit-obstructions/r17-zqy-producer-bound/tools/lemma_sim.txt @@ -0,0 +1,3 @@ +300 random programs: max(dim S - #jobs) = 0 (lemma requires <= 0) +one job per variable: dim S = 4 with 4 jobs +mutation (C gate treated as free): dim S = 4 with 0 paid jobs (lemma would be violated) diff --git a/research/encoded-exit-obstructions/r17-zqy-producer-bound/tools/price17.py b/research/encoded-exit-obstructions/r17-zqy-producer-bound/tools/price17.py new file mode 100644 index 0000000000..8d28be6072 --- /dev/null +++ b/research/encoded-exit-obstructions/r17-zqy-producer-bound/tools/price17.py @@ -0,0 +1,12 @@ +"""Exact-Decimal price of b purchases on the R16 model (16 backward FULLs; base T0+{9:128}, P0+{1:128}).""" +import sys; sys.path.insert(0, str(__import__('pathlib').Path.home()/'imb-harness/r16/tools')) +from price16 import * +U = D('0.00302728825') +Tb, Pb = add(T0, {9: 128}), add(P0, {1: 128}) +tau = M(Tb, Pb, U) / 16 +print('break-even per backward FULL at C=U: purchase cost sum r^(1-U) <', tau) +for name, dp in [('b free', {}), ('63 H1', {1: 63}), ('64 H1', {1: 64}), ('112 H1 (lower bound, post-return)', {1: 112}), + ('8 H8 (pre-return y/h copy: D Z y, exit Q merged)', {8: 8}), ('8 H9 (R Z y)', {9: 8})]: + cost = sum(c * pw(r, 1 - U) for r, c in dp.items()) + r = root(Tb, add(Pb, {k: 16 * v for k, v in dp.items()})) + print(f'{name:52s} cost/FULL {float(cost):9.4f} root {float(r):.13f} beats U: {r > U}') diff --git a/research/encoded-exit-obstructions/r17-zqy-producer-bound/tools/price17.txt b/research/encoded-exit-obstructions/r17-zqy-producer-bound/tools/price17.txt new file mode 100644 index 0000000000..3ff4345049 --- /dev/null +++ b/research/encoded-exit-obstructions/r17-zqy-producer-bound/tools/price17.txt @@ -0,0 +1,7 @@ +break-even per backward FULL at C=U: purchase cost sum r^(1-U) < 63.52267175046349274247810787964427232762978590375 +b free cost/FULL 0.0000 root 0.0071409936172 beats U: True +63 H1 cost/FULL 63.0000 root 0.0030608379586 beats U: True +64 H1 cost/FULL 64.0000 root 0.0029966533629 beats U: False +112 H1 (lower bound, post-return) cost/FULL 112.0000 root 0.0000000000000 beats U: False +8 H8 (pre-return y/h copy: D Z y, exit Q merged) cost/FULL 63.5984 root 0.0030223873635 beats U: False +8 H9 (R Z y) cost/FULL 71.5227 root 0.0025091695234 beats U: False